About CVC4 - Revision history

Ajreynol at 13:57, 8 May 2018

2018-05-08T13:57:04Z

Ajreynol at 13:56, 8 May 2018

2018-05-08T13:56:43Z

Ajreynol: /* Decision Procedures */

2018-05-01T19:58:52Z

‎Decision Procedures

Ajreynol: /* Decision Procedures */

2018-05-01T19:57:58Z

‎Decision Procedures

Ajreynol: /* Decision Procedures */

2018-05-01T19:56:58Z

‎Decision Procedures

Ajreynol: /* Decision Procedures */

2018-05-01T19:54:00Z

‎Decision Procedures

Ajreynol: /* Decision Procedures */

2018-05-01T19:52:08Z

‎Decision Procedures

Tinelli at 21:55, 24 April 2018

2018-04-24T21:55:35Z

Clark Barrett at 17:19, 27 January 2017

2017-01-27T17:19:47Z

Clark Barrett at 00:16, 27 January 2017

2017-01-27T00:16:56Z

@@ Line 7: / Line 7: @@
 * bit-vectors
 * arrays
-* [[tuples|datatypes]]
+* [[Datatypes|tuples]]
-* [[records|datatypes]]
+* [[Datatypes|records]]
 * user-defined inductive [[Datatypes|datatypes]]
 * [[Strings|strings]]

@@ Line 7: / Line 7: @@
 * bit-vectors
 * arrays
-* tuples
+* [[tuples|datatypes]]
-* records
+* [[records|datatypes]]
 * user-defined inductive [[Datatypes|datatypes]]
 * [[Strings|strings]]

@@ Line 53: / Line 53: @@
 ** Automated induction for datatypes [http://homepage.cs.uiowa.edu/~ajreynol/vmcai15.pdf].
 ** A decision procedure for quantified linear integer and real arithmetic [http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf].
 ** Support for syntax-guided synthesis, as described in [http://homepage.cs.uiowa.edu/~ajreynol/cav15a.pdf].
 * Relations

@@ Line 45: / Line 45: @@
 ** CVC4 implements [http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-JSAT-07.pdf An Abstract Decision Procedure for a Theory of Inductive Data Types].
 ** This procedure has been extended to incorporate coinductive datatypes [http://homepage.cs.uiowa.edu/~ajreynol/cade15.pdf].
 * Quantifiers
 ** E-matching and conflict-based quantifier instantiation [http://homepage.cs.uiowa.edu/~ajreynol/fmcad14.pdf].

@@ Line 35: / Line 35: @@
 ** Integers are currently handled by first solving the real relaxation of the constraints, and then using a combination of [http://www.cs.wm.edu/~idillig/cav2009.pdf Cuts from Proofs] and branching to ensure integer solutions.  This approach and the equational solver  used are described in [https://es.fbk.eu/people/griggio/papers/jsat12.pdf A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic].
 ** A technical report is planned to explain a number of small details and extensions including analysis to improve simplex's conflicts, handling disequalities, supporting model generation in CVC4's combination framework, heuristically propagating equalities over sharing terms, tableau row based propagation, and terminating simplex with unknown.
-** Non-linear arithmetic support is currently rudimentary to non-existent. In CVC4 v1.0, non-linearity is handled by abstracting monomials as unique new variables.  We plan on implementing [http://cs.nyu.edu/~dejan/papers/jovanovic-ijcar2012.pdf Solving Non-Linear Arithmetic] this spring.
+** A heuristic approach non-linear arithmetic is supported based on this paper [https://es-static.fbk.eu/people/griggio/papers/tacas17.pdf].
 * Arrays
 ** Arrays are implemented in a manner inspired by the [http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad09.pdf Generalized, efficient array decision procedures] paper with a few major modifications.

@@ Line 52: / Line 52: @@
 ** A decision procedure for quantified linear arithmetic with one alternation [http://homepage.cs.uiowa.edu/~ajreynol/report-inst-la15.pdf].
 ** Support for syntax-guided synthesis, as described in [http://homepage.cs.uiowa.edu/~ajreynol/cav15a.pdf].
 * SAT Solver
 ** The main sat solver is based on [http://minisat.se/ minisat v2.2.0].

@@ Line 11: / Line 11: @@
 * user-defined inductive [[Datatypes|datatypes]]
 * [[Strings|strings]]
-* [[Sets|finite sets]]
+* [[Sets|finite sets and relations]]
 * [[Separation Logic|separation logic]]

@@ Line 60: / Line 60: @@
 ** Adaptation of tableau-based decision procedure described [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5176 here].
 * Strings
-** Original approach described in our [http://www.cs.nyu.edu/~barrett/pubs/LRT+14.pdf CAV 2014 paper: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions].
+** Original approach described in our [http://www.cs.stanford.edu/~barrett/pubs/LRT+14.pdf CAV 2014 paper: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions].
 ** Decision procedure for regular memberships with length [http://homepage.cs.uiowa.edu/~ajreynol/frocos15.pdf].
 * Uninterpreted functions

@@ Line 1: / Line 1: @@
-CVC4 is an automatic theorem prover for [http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisifiability Modulo Theories (SMT)] (for a more formal introduction to SMT see the following book chapter [https://cs.nyu.edu/~barrett/pubs/BSST09.pdf Satisfiability Modulo Theories] ). Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories.
+CVC4 is an automatic theorem prover for [http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisifiability Modulo Theories (SMT)] (for a more formal introduction to SMT see the following book chapter [https://cs.stanford.edu/~barrett/pubs/BSST09.pdf Satisfiability Modulo Theories] ). Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories.
 It can be used to prove the validity (or, dually, the satisfiability) of a formula with respect to several built-in logical theories and their combination.
@@ Line 18: / Line 18: @@
 * support for quantifiers through heuristic instantiation;
 * an interactive text-based interface;
-* a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ C++ API] for embedding in other systems;
+* a rich [http://cvc4.cs.stanford.edu/cvc4-builds/documentation/public/latest/ C++ API] for embedding in other systems;
 * model generation abilities;
 * source compatibility with much of the CVC3 API via a "compatibility library";
-* essentially no limit on its use for research or commercial purposes (see [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest-unstable/copying.html license]).
+* essentially no limit on its use for research or commercial purposes (see [https://github.com/CVC4/CVC4/blob/master/COPYING license]).
 =Web site=