Tutorials - Revision history

Makaim at 18:28, 8 February 2017

2017-02-08T18:28:27Z

Makaim at 18:26, 8 February 2017

2017-02-08T18:26:59Z

Clark Barrett at 16:25, 23 December 2015

2015-12-23T16:25:29Z

Clark Barrett at 16:24, 23 December 2015

2015-12-23T16:24:12Z

Clark Barrett at 15:40, 23 December 2015

2015-12-23T15:40:02Z

Tianyi: /* C++ API */

2015-01-14T21:40:33Z

‎C++ API

Kshitij: /* Union and Intersection */

2014-06-30T19:58:45Z

‎Union and Intersection

Kshitij: /* Union and Intersection */

2014-06-30T19:56:29Z

‎Union and Intersection

Kshitij: /* C++ API */ Sets API examples

2014-06-30T19:09:22Z

‎C++ API: Sets API examples

Mdeters: /* bitvectors */

2014-05-02T23:16:13Z

‎bitvectors

@@ Line 410: / Line 410: @@
 =Parallel Solving=
 ===Obtaining===
-* Download a statically built binary supporting parallel solving: [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-opt Optimized build]
+* Download a statically built binary supporting parallel solving: [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/ Optimized build]
 * If compiling from source, specify by '''--with-portfolio''' option to the configure script. This will create an additional binary '''pcvc4''' which supports parallel solving.
   ./configure --with-portfolio [...]

@@ Line 5: / Line 5: @@
 ==Finding these examples==
-Except where noted below, tutorial code appearing in this section is kept in the <code>examples/cvc</code> directory of the CVC4 source distribution.  However, tutorial material on this page might be more recent than your CVC4 download.  Please refer to the [http://cvc4.cs.nyu.edu/builds/src/ most recent nightly build] for the most recent tutorial code.
+Except where noted below, tutorial code appearing in this section is kept in the <code>examples/cvc</code> directory of the CVC4 source distribution.  However, tutorial material on this page might be more recent than your CVC4 download.  Please refer to the [http://cvc4.cs.stanford.edu/downloads/ most recent nightly build] for the most recent tutorial code.
 =SMT-LIB=
@@ Line 11: / Line 11: @@
 We recommend [http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf David Cok's excellent tutorial on SMT-LIB].  When running examples from this tutorial, we recommend using CVC4's ''--smtlib-strict'' command line option, which enters a stricter compliance mode.
-CVC4 should be compliant with [http://www.smtlib.org/ the standard], and thus also with David Cok's tutorial, except for some unsupported functionality as noted in the [[SMT-LIB_Compliance|SMT-LIB compliance section of this wiki]].  If you find something that you believe to be nonconformant, please [http://cvc4.cs.nyu.edu/bugs/ report it as a bug].
+CVC4 should be compliant with [http://www.smtlib.org/ the standard], and thus also with David Cok's tutorial, except for some unsupported functionality as noted in the [[SMT-LIB_Compliance|SMT-LIB compliance section of this wiki]].  If you find something that you believe to be nonconformant, please [http://cvc4.cs.stanford.edu/bugs/ report it as a bug].
 =C++ API=
@@ Line 24: / Line 24: @@
 ==Finding and compiling these examples==
-Except where noted below, tutorial code appearing in this section is kept in the <code>examples/api</code> directory of the CVC4 source distribution.  However, tutorial material on this page might be more recent than your CVC4 download.  Please refer to the [http://cvc4.cs.nyu.edu/builds/src/ most recent nightly build] for the most recent tutorial code.
+Except where noted below, tutorial code appearing in this section is kept in the <code>examples/api</code> directory of the CVC4 source distribution.  However, tutorial material on this page might be more recent than your CVC4 download.  Please refer to the [http://cvc4.cs.stanford.edu/downloads/ most recent nightly build] for the most recent tutorial code.
 To compile everything in the <code>examples/</code> directory, you can issue the command <code>make examples</code> from the top-level of the source distribution.  This will first build CVC4 (if it isn't already built) and then the examples.  Some examples from the directory may not be compiled, if (for instance) you haven't built with support for Java, or if you haven't built with support for the compatibility interface; however, all native C++ API examples should be, and those are the only ones appearing in this section.

@@ Line 238: / Line 238: @@
    SmtEngine smt(&em);
    smt.setLogic("QF_BV"); // Set the logic
-−
    Type bitvector32 = em.mkBitVectorType(32);
-−
    Expr x = em.mkVar("a", bitvector32);
-−
    Expr ext_31_1 = em.mkConst(CVC4::BitVectorExtract(31,1));
    Expr x_31_1 = em.mkExpr(ext_31_1, x);
-−
    Expr ext_30_0 = em.mkConst(CVC4::BitVectorExtract(30,0));
    Expr x_30_0 = em.mkExpr(ext_30_0, x);
-−
    Expr ext_31_31 = em.mkConst(CVC4::BitVectorExtract(31,31));
    Expr x_31_31 = em.mkExpr(ext_31_31, x);
-−
    Expr ext_0_0 = em.mkConst(CVC4::BitVectorExtract(0,0));
    Expr x_0_0 = em.mkExpr(ext_0_0, x);
-−
    Expr eq = em.mkExpr(kind::EQUAL, x_31_1, x_30_0);
    cout << " Asserting: " << eq << endl;
    smt.assertFormula(eq);
-−
    Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0);
    cout << " Querying: " << eq2 << endl;

@@ Line 232: / Line 232: @@
    cout << " Expect valid. " << endl;
    cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
 ==Sets==

@@ Line 9: / Line 9: @@
 =SMT-LIB=
-We recommend [http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf David Cok's excellent tutorial on SMT-LIB].  When running examples from this tutorial, we recommend using CVC4's ''--smtlib-strict'' command line option, which enters a stricter compliance mode.
+We recommend [http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf David Cok's excellent tutorial on SMT-LIB].  When running examples from this tutorial, we recommend using CVC4's ''--smtlib-strict'' command line option, which enters a stricter compliance mode.
 CVC4 should be compliant with [http://www.smtlib.org/ the standard], and thus also with David Cok's tutorial, except for some unsupported functionality as noted in the [[SMT-LIB_Compliance|SMT-LIB compliance section of this wiki]].  If you find something that you believe to be nonconformant, please [http://cvc4.cs.nyu.edu/bugs/ report it as a bug].

@@ Line 20: / Line 20: @@
 * bitvectors_and_arrays : integer and uninterpreted function example
 * quantifiers
 ==Finding and compiling these examples==
@@ Line 307: / Line 308: @@
+     }
 </pre>
 =Java API=

@@ Line 243: / Line 243: @@
 ===Union and Intersection===
-Verify union distributions over intersection. Checks the validity of (A union B) intersection C = (A intersection C) union (B intersection C) for all sets A, B, C of type integers.
+Verify union distributions over intersection. Checks the validity of (A union B) intersection C = (A intersection C) union (B intersection C) for all sets A, B, C of integers.
 <pre>
      Expr A = em.mkVar("A", set);

@@ Line 226: / Line 226: @@
    // Assert encoding to CVC4 in current context;
    cout << "Asserting " << assignment2 << " to CVC4 " << endl;
-   smt.assertFormula(assignment1);
+   smt.assertFormula(assignment2);
    cout << " Querying: " << new_x_eq_new_x_ << endl;