Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Relational Constraint Solving in SMT

Authors : Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Relational logic is useful for reasoning about computational problems with relational structures, including high-level system design, architectural configurations of network systems, ontologies, and verification of programs with linked data structures. We present a modular extension of an earlier calculus for the theory of finite sets to a theory of finite relations with such operations as transpose, product, join, and transitive closure. We implement this extension as a theory solver of the SMT solver CVC4. Combining this new solver with the finite model finding features of CVC4 enables several compelling use cases. For instance, native support for relations enables a natural mapping from Alloy, a declarative modeling language based on first-order relational logic, to SMT constraints. It also enables a natural encoding of several description logics with concrete domains, allowing the use of an SMT solver to analyze, for instance, Web Ontology Language (OWL) models. We provide an initial evaluation of our solver on a number of Alloy and OWL models which shows promising results.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Short Proofs Without New Variables
next chapter Decision Procedures for Theories of Sets with Measures
Footnotes
1
A further extension of the theory to cardinality constraints is planned for future work.
 
2
Note that this theory has all the function symbols of \({\varSigma _{R}}\), not just the tuple constructors \(\langle \_, \ldots , \_\rangle \). The extra symbols are treated as uninterpreted.
 
3
All proofs of the propositions below can be found in a longer version of this paper available at http://​cvc4.​cs.​stanford.​edu/​papers/​CADE2017-relations/​.
 
4
The Alloy Analyzer currently has built-in support for bounded integers. Any other data types need to be axiomatized in the specification.
 
5
The translation is sound only if all Alloy signatures are assumed to be finite. A full account of the translation and a proof of its soundness are beyond the scope of this paper.
 
6
Free constants have the same effect as free variables for satisfiability purposes.
 
7
Some of those domains in OWL correspond to built-in sorts in cvc4. A full translation from OWL concrete domains to cvc4 built-in sorts is beyond the scope of this work.
 
8
Detailed results and all benchmarks are available at http://​cvc4.​cs.​stanford.​edu/​papers/​CADE2017-relations/​.
 
Literature
1.
Baader, F.: The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)MATH
2.
Baader, F., Horrocks, I., Sattler, U.: Description logics. In: Frank van Harmelen, V.L., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 3. Foundations of Artificial Intelligence, pp. 135–179. Elsevier (2008)
3.
Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 82–98. Springer, Cham (2016). doi:10.​1007/​978-3-319-40229-1_​7
4.
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​14 CrossRef
5.
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard–version 2.6. In: Gupta, A., Kroening, D. (eds.) SMT 2010 (2010)
6.
Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, chap. 26, pp. 825–885. IOS Press, February 2009
7.
Dutertre, B., Moura, L.D.: The YICES SMT solver. Technical report, SRI International (2006)
8.
Ghazi, A.A.E., Taghdiri, M.: Analyzing alloy constraints using an SMT solver: a case study. In: 5th International Workshop on Automated Formal Methods (AFM) (2010)
9.
10.
El Ghazi, A.A., Taghdiri, M., Herda, M.: First-order transitive closure axiomatization via iterative invariant injections. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 143–157. Springer, Cham (2015). doi:10.​1007/​978-3-319-17524-9_​11
11.
Horrocks, I., Sattler, U.: Decidability of SHIQ with complex role inclusion axioms. Artif. Intell. 160(1–2), 79–104 (2004)CrossRefMATH
12.
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRef
13.
Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006)
14.
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)MathSciNetCrossRefMATH
15.
16.
Steigmiller, A., Liebig, T., Glimm, B.: Konclude: System description. Web Semant. Sci. Serv. Agents World Wide Web 27(1), 1–86 (2014)
17.
18.
Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292–297. Springer, Heidelberg (2006). doi:10.​1007/​11814771_​26 CrossRef
19.
Tsarkov, D., Palmisano, I.: Chainsaw: a metareasoner for large ontologies. In: Horrocks, I., Yatskevich, M., Jiménez-Ruiz, E. (eds.) ORE (2012)
20.
Metadata
Title
Relational Constraint Solving in SMT
Authors
Baoluo Meng
Andrew Reynolds
Cesare Tinelli
Clark Barrett
Copyright Year
2017
Book
Automated Deduction – CADE 26

Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63046-5_10

Premium Partner

    Image Credits