diff options
Diffstat (limited to 'examples')
66 files changed, 876 insertions, 1802 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 893ea5c95..cd74698d7 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -58,31 +58,39 @@ endmacro() cvc4_add_example(simple_vc_cxx "" "") cvc4_add_example(simple_vc_quant_cxx "" "") -cvc4_add_example(translator "" "" - # argument to binary (for testing) - ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) +# TODO(project issue $206): Port example to new API +# cvc4_add_example(translator "" "" +# # argument to binary (for testing) +# ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) add_subdirectory(api) -add_subdirectory(hashsmt) -add_subdirectory(nra-translate) -add_subdirectory(sets-translate) +# TODO(project issue $206): Port example to new API +# add_subdirectory(hashsmt) +# add_subdirectory(nra-translate) +# add_subdirectory(sets-translate) if(TARGET CVC4::cvc4jar) find_package(Java REQUIRED) include(UseJava) - get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE) - - add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}") - - add_test( - NAME java/SimpleVC - COMMAND - ${Java_JAVA_EXECUTABLE} - -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar" - -Djava.library.path=${CVC4_JNI_PATH} - SimpleVC - ) + ## disabled until bindings for the new API are in place (issue #2284) + # get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE) + # + # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}") + # + # add_test( + # NAME java/SimpleVC + # COMMAND + # ${Java_JAVA_EXECUTABLE} + # -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar" + # -Djava.library.path=${CVC4_JNI_PATH} + # SimpleVC + # ) add_subdirectory(api/java) endif() + +if(CVC4_BINDINGS_PYTHON) + # If legacy Python API has been built + add_subdirectory(api/python) +endif() diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 798dc08af..81e7a1f64 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -2,9 +2,9 @@ /*! \file SimpleVC.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Aina Niemetz, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -52,8 +52,7 @@ public class SimpleVC { Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three); Expr formula = - new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)). - impExpr(new Expr(twox_plus_y_geq_3)); + em.mkExpr(Kind.AND, x_positive, y_positive).impExpr(twox_plus_y_geq_3); System.out.println( "Checking entailment of formula " + formula + " with CVC4."); diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml deleted file mode 100644 index d9d78586b..000000000 --- a/examples/SimpleVC.ml +++ /dev/null @@ -1,91 +0,0 @@ -(********************* ** -**! \file SimpleVC.ml -*** \verbatim -*** Original author: mdeters -*** Major contributors: none -*** Minor contributors (to current version): none -*** This file is part of the CVC4 prototype. -*** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) -*** Courant Institute of Mathematical Sciences -*** New York University -*** See the file COPYING in the top-level source directory for licensing -*** information.\endverbatim -*** -*** \brief A simple demonstration of the OCaml interface -*** -*** A simple demonstration of the OCaml interface. Compare to the -*** C++ interface in simple_vc_cxx.cpp; they are quite similar. -*** -*** To run, use something like: -*** -*** LD_LIBRARY_PATH=../builds/src/bindings/ocaml/.libs \ -*** ../builds/src/bindings/cvc4_ocaml_top -I ../builds/src/bindings/ocaml \ -*** SimpleVC.ml -*** -*** After you "make install" CVC4, it's much easier; the cvc4_ocaml_top goes in -*** $prefix/bin, and it's automatically set up the load the .cmo and .cmi files -*** from $prefix/lib/ocaml/cvc4, in which they get installed. Then you just -*** have to: cvc4_ocaml_top -I $prefix/lib/ocaml/cvc4 -***) - -open Swig -open CVC4 - -let em = new_ExprManager '() -let smt = new_SmtEngine(em) - -(* Prove that for integers x and y: - * x > 0 AND y > 0 => 2x + y >= 3 *) - -let integer = em->integerType() - -let x = em->mkVar(integer) (* em->mkVar("x", integer) *) -let y = em->mkVar(integer) (* em->mkVar("y", integer) *) -let integerZero = new_Integer '("0", 10) -let zero = em->mkConst(integerZero) - -(* OK, this is really strange. We can call mkExpr(36, ...) for - * example, with the int value of the operator Kind we want, - * or we can compute it. But if we compute it, we have to rip - * it out of its C_int, then wrap it again a C_int, in order - * for the parser to make it go through. *) -let geq = C_int (get_int (enum_to_int `Kind_t (``GEQ))) -let gt = C_int (get_int (enum_to_int `Kind_t (``GT))) -let mult = C_int (get_int (enum_to_int `Kind_t (``MULT))) -let plus = C_int (get_int (enum_to_int `Kind_t (``PLUS))) -let and_kind = C_int (get_int (enum_to_int `Kind_t (``AND))) -let implies = C_int (get_int (enum_to_int `Kind_t (``IMPLIES))) - -(* gt = 35, but the parser screws up if we put "geq" what follows *) -let x_positive = em->mkExpr(gt, x, zero) -let y_positive = em->mkExpr(gt, y, zero) - -let integerTwo = new_Integer '("2", 10) -let two = em->mkConst(integerTwo) -let twox = em->mkExpr(mult, two, x) -let twox_plus_y = em->mkExpr(plus, twox, y) - -let integerThree = new_Integer '("3", 10) -let three = em->mkConst(integerThree) -let twox_plus_y_geq_3 = em->mkExpr(geq, twox_plus_y, three) - -let lhs = em->mkExpr(and_kind, x_positive, y_positive) - -(* This fails for some reason. *) -(* let rhs = new_Expr(twox_plus_y_geq_3) - let formula = new_Expr(lhs)->impExpr(rhs) *) - -let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3) - -let bformula = new_Expr(formula) in - -print_string "Checking entailment of formula " ; -print_string (get_string (formula->toString ())) ; -print_string " with CVC4." ; -print_newline () ; -print_string "CVC4 should report ENTAILED." ; -print_newline () ; -print_string "Result from CVC4 is: " ; -print_string (get_string (smt->checkEntailed(bformula)->toString ())) ; -print_newline () -;; diff --git a/examples/SimpleVC.php b/examples/SimpleVC.php deleted file mode 100755 index 031c0a1c5..000000000 --- a/examples/SimpleVC.php +++ /dev/null @@ -1,56 +0,0 @@ -#! /usr/bin/php -##! \file SimpleVC.php -### \verbatim -### Original author: mdeters -### Major contributors: none -### Minor contributors (to current version): none -### This file is part of the CVC4 prototype. -### Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) -### Courant Institute of Mathematical Sciences -### New York University -### See the file COPYING in the top-level source directory for licensing -### information.\endverbatim -### -### \brief A simple demonstration of the PHP interface -### -### A simple demonstration of the PHP interface. Compare to the -### C++ interface in simple_vc_cxx.cpp; they are quite similar. -### -### To run, use something like: -### -### ln -s ../builds/src/bindings/php/.libs/CVC4.so CVC4.so -### ln -s ../builds/src/bindings/php/CVC4.php CVC4.php -### ./SimpleVC.php -#### - -use strict; -use CVC4; - -my $em = new CVC4::ExprManager(); -my $smt = new CVC4::SmtEngine($em); - -# Prove that for integers x and y: -# x > 0 AND y > 0 => 2x + y >= 3 - -my $integer = $em->integerType(); - -my $x = $em->mkVar("x", $integer); -my $y = $em->mkVar("y", $integer); -my $zero = $em->mkConst(new CVC4::Integer(0)); - -my $x_positive = $em->mkExpr($CVC4::GT, $x, $zero); -my $y_positive = $em->mkExpr($CVC4::GT, $y, $zero); - -my $two = $em->mkConst(new CVC4::Integer(2)); -my $twox = $em->mkExpr($CVC4::MULT, $two, $x); -my $twox_plus_y = $em->mkExpr($CVC4::PLUS, $twox, $y); - -my $three = $em->mkConst(new CVC4::Integer(3)); -my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three); - -my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3)); - -print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n"; -print "CVC4 should report ENTAILED.\n"; -print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n"; - diff --git a/examples/SimpleVC.pl b/examples/SimpleVC.pl deleted file mode 100755 index 20ad6c737..000000000 --- a/examples/SimpleVC.pl +++ /dev/null @@ -1,56 +0,0 @@ -#! /usr/bin/perl -w -##! \file SimpleVC.pl -### \verbatim -### Original author: mdeters -### Major contributors: none -### Minor contributors (to current version): none -### This file is part of the CVC4 prototype. -### Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) -### Courant Institute of Mathematical Sciences -### New York University -### See the file COPYING in the top-level source directory for licensing -### information.\endverbatim -### -### \brief A simple demonstration of the Perl interface -### -### A simple demonstration of the Perl interface. Compare to the -### C++ interface in simple_vc_cxx.cpp; they are quite similar. -### -### To run, use something like: -### -### ln -s ../builds/src/bindings/perl/.libs/CVC4.so CVC4.so -### ln -s ../builds/src/bindings/perl/CVC4.pm CVC4.pm -### ./SimpleVC.pl -#### - -use strict; -use CVC4; - -my $em = new CVC4::ExprManager(); -my $smt = new CVC4::SmtEngine($em); - -# Prove that for integers x and y: -# x > 0 AND y > 0 => 2x + y >= 3 - -my $integer = $em->integerType(); - -my $x = $em->mkVar("x", $integer); -my $y = $em->mkVar("y", $integer); -my $zero = $em->mkConst(new CVC4::Integer(0)); - -my $x_positive = $em->mkExpr($CVC4::GT, $x, $zero); -my $y_positive = $em->mkExpr($CVC4::GT, $y, $zero); - -my $two = $em->mkConst(new CVC4::Integer(2)); -my $twox = $em->mkExpr($CVC4::MULT, $two, $x); -my $twox_plus_y = $em->mkExpr($CVC4::PLUS, $twox, $y); - -my $three = $em->mkConst(new CVC4::Integer(3)); -my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three); - -my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3)); - -print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n"; -print "CVC4 should report ENTAILED.\n"; -print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n"; - diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py index 5550974c9..50c52868b 100755 --- a/examples/SimpleVC.py +++ b/examples/SimpleVC.py @@ -16,11 +16,9 @@ ### A simple demonstration of the Python interface. Compare to the ### C++ interface in simple_vc_cxx.cpp; they are quite similar. ### -### To run, use something like: +### To run from a build directory, use something like: ### -### ln -s ../builds/src/bindings/python/CVC4.py CVC4.py -### ln -s ../builds/src/bindings/python/.libs/CVC4.so _CVC4.so -### ./SimpleVC.py +### PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py #### import CVC4 @@ -61,4 +59,3 @@ def main(): if __name__ == '__main__': sys.exit(main()) - diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb deleted file mode 100755 index 4f289d34f..000000000 --- a/examples/SimpleVC.rb +++ /dev/null @@ -1,57 +0,0 @@ -#! /usr/bin/ruby -##! \file SimpleVC.rb -### \verbatim -### Original author: mdeters -### Major contributors: none -### Minor contributors (to current version): none -### This file is part of the CVC4 prototype. -### Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) -### Courant Institute of Mathematical Sciences -### New York University -### See the file COPYING in the top-level source directory for licensing -### information.\endverbatim -### -### \brief A simple demonstration of the Ruby interface -### -### A simple demonstration of the Ruby interface. Compare to the -### C++ interface in simple_vc_cxx.cpp; they are quite similar. -### -### To run, use something like: -### -### ln -s ../builds/src/bindings/ruby/.libs/CVC4.so CVC4.so -### ./SimpleVC.rb -#### - -require 'CVC4' -include CVC4 # CVC4::Integer still has to be qualified - -em = ExprManager.new -smt = SmtEngine.new(em) - -# Prove that for integers x and y: -# x > 0 AND y > 0 => 2x + y >= 3 - -integer = em.integerType - -x = em.mkVar("x", integer) -y = em.mkVar("y", integer) -zero = em.mkConst(CVC4::Integer.new(0)) - -x_positive = em.mkExpr(GT, x, zero) -y_positive = em.mkExpr(GT, y, zero) - -two = em.mkConst(CVC4::Integer.new(2)) -twox = em.mkExpr(MULT, two, x) -twox_plus_y = em.mkExpr(PLUS, twox, y) - -three = em.mkConst(CVC4::Integer.new(3)) -twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three) - -formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3)) - -puts "Checking entailment of formula " + formula.toString + " with CVC4." -puts "CVC4 should report ENTAILED." -puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString - -exit - diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl deleted file mode 100755 index 4e1c76c5a..000000000 --- a/examples/SimpleVC.tcl +++ /dev/null @@ -1,54 +0,0 @@ -#! /usr/bin/tclsh -##! \file SimpleVC.tcl -### \verbatim -### Original author: mdeters -### Major contributors: none -### Minor contributors (to current version): none -### This file is part of the CVC4 prototype. -### Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) -### Courant Institute of Mathematical Sciences -### New York University -### See the file COPYING in the top-level source directory for licensing -### information.\endverbatim -### -### \brief A simple demonstration of the Tcl interface -### -### A simple demonstration of the Tcl interface. Compare to the -### C++ interface in simple_vc_cxx.cpp; they are quite similar. -### -### To run, use something like: -### -### ln -s ../builds/src/bindings/tcl/.libs/CVC4.so CVC4.so -### ./SimpleVC.tcl -#### - -load CVC4.so CVC4 - -ExprManager em -SmtEngine smt em - -# Prove that for integers x and y: -# x > 0 AND y > 0 => 2x + y >= 3 - -set integer [ExprManager_integerType em] - -set x [ExprManager_mkVar em "x" $integer] -set y [ExprManager_mkVar em "y" $integer] -set zero [ExprManager_mkConst em [Integer _ 0]] - -set x_positive [ExprManager_mkExpr em $GT $x $zero] -set y_positive [ExprManager_mkExpr em $GT $y $zero] - -set two [ExprManager_mkConst em [Integer _ 2]] -set twox [ExprManager_mkExpr em $MULT $two $x] -set twox_plus_y [ExprManager_mkExpr em $PLUS $twox $y] - -set three [ExprManager_mkConst em [Integer _ 3]] -set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three] - -set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]] - -puts "Checking entailment of formula [Expr_toString $formula] with CVC4." -puts "CVC4 should report ENTAILED." -puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]" - diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index 3ced5681c..6421a3263 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -1,22 +1,13 @@ set(CVC4_EXAMPLES_API bitvectors - bitvectors-new bitvectors_and_arrays - bitvectors_and_arrays-new combination - combination-new datatypes - datatypes-new extract - extract-new helloworld - helloworld-new linear_arith - linear_arith-new sets - sets-new strings - strings-new sygus-fun sygus-grammar sygus-inv diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp deleted file mode 100644 index ebb8ee7ee..000000000 --- a/examples/api/bitvectors-new.cpp +++ /dev/null @@ -1,127 +0,0 @@ -/********************* */ -/*! \file bitvectors-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector solver. - ** - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace std; -using namespace CVC4::api; - -int main() -{ - Solver slv; - slv.setLogic("QF_BV"); // Set the logic - - // The following example has been adapted from the book A Hacker's Delight by - // Henry S. Warren. - // - // Given a variable x that can only have two values, a or b. We want to - // assign to x a value other than the current one. The straightforward code - // to do that is: - // - //(0) if (x == a ) x = b; - // else x = a; - // - // Two more efficient yet equivalent methods are: - // - //(1) x = a ⊕ b ⊕ x; - // - //(2) x = a + b - x; - // - // We will use CVC4 to prove that the three pieces of code above are all - // equivalent by encoding the problem in the bit-vector theory. - - // Creating a bit-vector type of width 32 - Sort bitvector32 = slv.mkBitVectorSort(32); - - // Variables - Term x = slv.mkConst(bitvector32, "x"); - Term a = slv.mkConst(bitvector32, "a"); - Term b = slv.mkConst(bitvector32, "b"); - - // First encode the assumption that x must be equal to a or b - Term x_eq_a = slv.mkTerm(EQUAL, x, a); - Term x_eq_b = slv.mkTerm(EQUAL, x, b); - Term assumption = slv.mkTerm(OR, x_eq_a, x_eq_b); - - // Assert the assumption - slv.assertFormula(assumption); - - // Introduce a new variable for the new value of x after assignment. - Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0) - Term new_x_ = - slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2) - - // Encoding code (0) - // new_x = x == a ? b : a; - Term ite = slv.mkTerm(ITE, x_eq_a, b, a); - Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); - - // Assert the encoding of code (0) - cout << "Asserting " << assignment0 << " to CVC4 " << endl; - slv.assertFormula(assignment0); - cout << "Pushing a new context." << endl; - slv.push(); - - // Encoding code (1) - // new_x_ = a xor b xor x - Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); - Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); - - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment1 << " to CVC4 " << endl; - slv.assertFormula(assignment1); - Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); - - cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; - cout << " Popping context. " << endl; - slv.pop(); - - // Encoding code (2) - // new_x_ = a + b - x - Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b); - Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); - Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); - - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment2 << " to CVC4 " << endl; - slv.assertFormula(assignment2); - - cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; - - Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); - std::vector<Term> v{new_x_eq_new_x_, x_neq_x}; - cout << " Check entailment assuming: " << v << endl; - cout << " Expect NOT_ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(v) << endl; - - // Assert that a is odd - Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); - Term lsb_of_a = slv.mkTerm(extract_op, a); - cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; - Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); - cout << "Assert " << a_odd << endl; - cout << "Check satisfiability." << endl; - slv.assertFormula(a_odd); - cout << " Expect sat. " << endl; - cout << " CVC4: " << slv.checkSat() << endl; - return 0; -} diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 494a45abc..ab1e8ce07 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -2,9 +2,9 @@ /*! \file bitvectors.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Morgan Deters + ** Aina Niemetz, Makai Mann ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,15 +16,15 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setLogic("QF_BV"); // Set the logic +int main() +{ + Solver slv; + slv.setLogic("QF_BV"); // Set the logic // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. @@ -46,81 +46,82 @@ int main() { // equivalent by encoding the problem in the bit-vector theory. // Creating a bit-vector type of width 32 - Type bitvector32 = em.mkBitVectorType(32); + Sort bitvector32 = slv.mkBitVectorSort(32); // Variables - Expr x = em.mkVar("x", bitvector32); - Expr a = em.mkVar("a", bitvector32); - Expr b = em.mkVar("b", bitvector32); + Term x = slv.mkConst(bitvector32, "x"); + Term a = slv.mkConst(bitvector32, "a"); + Term b = slv.mkConst(bitvector32, "b"); // First encode the assumption that x must be equal to a or b - Expr x_eq_a = em.mkExpr(kind::EQUAL, x, a); - Expr x_eq_b = em.mkExpr(kind::EQUAL, x, b); - Expr assumption = em.mkExpr(kind::OR, x_eq_a, x_eq_b); + Term x_eq_a = slv.mkTerm(EQUAL, x, a); + Term x_eq_b = slv.mkTerm(EQUAL, x, b); + Term assumption = slv.mkTerm(OR, x_eq_a, x_eq_b); // Assert the assumption - smt.assertFormula(assumption); + slv.assertFormula(assumption); // Introduce a new variable for the new value of x after assignment. - Expr new_x = em.mkVar("new_x", bitvector32); // x after executing code (0) - Expr new_x_ = em.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0) + Term new_x_ = + slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; - Expr ite = em.mkExpr(kind::ITE, x_eq_a, b, a); - Expr assignment0 = em.mkExpr(kind::EQUAL, new_x, ite); + Term ite = slv.mkTerm(ITE, x_eq_a, b, a); + Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); // Assert the encoding of code (0) cout << "Asserting " << assignment0 << " to CVC4 " << endl; - smt.assertFormula(assignment0); + slv.assertFormula(assignment0); cout << "Pushing a new context." << endl; - smt.push(); + slv.push(); // Encoding code (1) // new_x_ = a xor b xor x - Expr a_xor_b_xor_x = em.mkExpr(kind::BITVECTOR_XOR, a, b, x); - Expr assignment1 = em.mkExpr(kind::EQUAL, new_x_, a_xor_b_xor_x); + Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); + Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); // Assert encoding to CVC4 in current context; cout << "Asserting " << assignment1 << " to CVC4 " << endl; - smt.assertFormula(assignment1); - Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_); + slv.assertFormula(assignment1); + Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); - cout << " Querying: " << new_x_eq_new_x_ << endl; - cout << " Expect entailed. " << endl; - cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl; + cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; - smt.pop(); + slv.pop(); // Encoding code (2) // new_x_ = a + b - x - Expr a_plus_b = em.mkExpr(kind::BITVECTOR_PLUS, a, b); - Expr a_plus_b_minus_x = em.mkExpr(kind::BITVECTOR_SUB, a_plus_b, x); - Expr assignment2 = em.mkExpr(kind::EQUAL, new_x_, a_plus_b_minus_x); + Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b); + Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); + Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); // Assert encoding to CVC4 in current context; cout << "Asserting " << assignment2 << " to CVC4 " << endl; - smt.assertFormula(assignment2); + slv.assertFormula(assignment2); - cout << " Querying: " << new_x_eq_new_x_ << endl; + cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl; + cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; - Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr(); - std::vector<Expr> v{new_x_eq_new_x_, x_neq_x}; - cout << " Querying: " << v << endl; + Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); + std::vector<Term> v{new_x_eq_new_x_, x_neq_x}; + cout << " Check entailment assuming: " << v << endl; cout << " Expect NOT_ENTAILED. " << endl; - cout << " CVC4: " << smt.checkEntailed(v) << endl; + cout << " CVC4: " << slv.checkEntailed(v) << endl; - // Assert that a is odd - Expr extract_op = em.mkConst(BitVectorExtract(0, 0)); - Expr lsb_of_a = em.mkExpr(extract_op, a); - cout << "Type of " << lsb_of_a << " is " << lsb_of_a.getType() << endl; - Expr a_odd = em.mkExpr(kind::EQUAL, lsb_of_a, em.mkConst(BitVector(1u, 1u))); + // Assert that a is odd + Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term lsb_of_a = slv.mkTerm(extract_op, a); + cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; + Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); cout << "Assert " << a_odd << endl; cout << "Check satisfiability." << endl; - smt.assertFormula(a_odd); + slv.assertFormula(a_odd); cout << " Expect sat. " << endl; - cout << " CVC4: " << smt.checkSat() << endl; + cout << " CVC4: " << slv.checkSat() << endl; return 0; } diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp deleted file mode 100644 index 44b5aa018..000000000 --- a/examples/api/bitvectors_and_arrays-new.cpp +++ /dev/null @@ -1,96 +0,0 @@ -/********************* */ -/*! \file bitvectors_and_arrays-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector and array solvers. - ** - **/ - -#include <iostream> -#include <cmath> - -#include <cvc4/api/cvc4cpp.h> - -using namespace std; -using namespace CVC4::api; - -int main() -{ - Solver slv; - slv.setOption("produce-models", "true"); // Produce Models - slv.setOption("output-language", "smtlib"); // output-language - slv.setLogic("QF_AUFBV"); // Set the logic - - // Consider the following code (where size is some previously defined constant): - // - // - // Assert (current_array[0] > 0); - // for (unsigned i = 1; i < k; ++i) { - // current_array[i] = 2 * current_array[i - 1]; - // Assert (current_array[i-1] < current_array[i]); - // } - // - // We want to check whether the assertion in the body of the for loop holds - // throughout the loop. - - // Setting up the problem parameters - unsigned k = 4; // number of unrollings (should be a power of 2) - unsigned index_size = log2(k); // size of the index - - - // Sorts - Sort elementSort = slv.mkBitVectorSort(32); - Sort indexSort = slv.mkBitVectorSort(index_size); - Sort arraySort = slv.mkArraySort(indexSort, elementSort); - - // Variables - Term current_array = slv.mkConst(arraySort, "current_array"); - - // Making a bit-vector constant - Term zero = slv.mkBitVector(index_size, 0u); - - // Asserting that current_array[0] > 0 - Term current_array0 = slv.mkTerm(SELECT, current_array, zero); - Term current_array0_gt_0 = slv.mkTerm( - BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0u)); - slv.assertFormula(current_array0_gt_0); - - // Building the assertions in the loop unrolling - Term index = slv.mkBitVector(index_size, 0u); - Term old_current = slv.mkTerm(SELECT, current_array, index); - Term two = slv.mkBitVector(32, 2u); - - std::vector<Term> assertions; - for (unsigned i = 1; i < k; ++i) { - index = slv.mkBitVector(index_size, i); - Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current); - // current[i] = 2 * current[i-1] - current_array = slv.mkTerm(STORE, current_array, index, new_current); - // current[i-1] < current [i] - Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current); - assertions.push_back(current_slt_new_current); - - old_current = slv.mkTerm(SELECT, current_array, index); - } - - Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); - - cout << "Asserting " << query << " to CVC4 " << endl; - slv.assertFormula(query); - cout << "Expect sat. " << endl; - cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; - - // Getting the model - cout << "The satisfying model is: " << endl; - cout << " current_array = " << slv.getValue(current_array) << endl; - cout << " current_array[0] = " << slv.getValue(current_array0) << endl; - return 0; -} diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index 1820712bd..2c98d4f8a 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -2,9 +2,9 @@ /*! \file bitvectors_and_arrays.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,17 +17,17 @@ #include <iostream> #include <cmath> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setOption("produce-models", true); // Produce Models - smt.setOption("output-language", "smtlib"); // output-language - smt.setLogic("QF_AUFBV"); // Set the logic +int main() +{ + Solver slv; + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "smtlib"); // output-language + slv.setLogic("QF_AUFBV"); // Set the logic // Consider the following code (where size is some previously defined constant): // @@ -46,50 +46,51 @@ int main() { unsigned index_size = log2(k); // size of the index - // Types - Type elementType = em.mkBitVectorType(32); - Type indexType = em.mkBitVectorType(index_size); - Type arrayType = em.mkArrayType(indexType, elementType); + // Sorts + Sort elementSort = slv.mkBitVectorSort(32); + Sort indexSort = slv.mkBitVectorSort(index_size); + Sort arraySort = slv.mkArraySort(indexSort, elementSort); // Variables - Expr current_array = em.mkVar("current_array", arrayType); + Term current_array = slv.mkConst(arraySort, "current_array"); // Making a bit-vector constant - Expr zero = em.mkConst(BitVector(index_size, 0u)); + Term zero = slv.mkBitVector(index_size, 0u); // Asserting that current_array[0] > 0 - Expr current_array0 = em.mkExpr(kind::SELECT, current_array, zero); - Expr current_array0_gt_0 = em.mkExpr(kind::BITVECTOR_SGT, current_array0, em.mkConst(BitVector(32, 0u))); - smt.assertFormula(current_array0_gt_0); + Term current_array0 = slv.mkTerm(SELECT, current_array, zero); + Term current_array0_gt_0 = slv.mkTerm( + BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0u)); + slv.assertFormula(current_array0_gt_0); // Building the assertions in the loop unrolling - Expr index = em.mkConst(BitVector(index_size, 0u)); - Expr old_current = em.mkExpr(kind::SELECT, current_array, index); - Expr two = em.mkConst(BitVector(32, 2u)); + Term index = slv.mkBitVector(index_size, 0u); + Term old_current = slv.mkTerm(SELECT, current_array, index); + Term two = slv.mkBitVector(32, 2u); - std::vector<Expr> assertions; + std::vector<Term> assertions; for (unsigned i = 1; i < k; ++i) { - index = em.mkConst(BitVector(index_size, Integer(i))); - Expr new_current = em.mkExpr(kind::BITVECTOR_MULT, two, old_current); + index = slv.mkBitVector(index_size, i); + Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current); // current[i] = 2 * current[i-1] - current_array = em.mkExpr(kind::STORE, current_array, index, new_current); + current_array = slv.mkTerm(STORE, current_array, index, new_current); // current[i-1] < current [i] - Expr current_slt_new_current = em.mkExpr(kind::BITVECTOR_SLT, old_current, new_current); + Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current); assertions.push_back(current_slt_new_current); - old_current = em.mkExpr(kind::SELECT, current_array, index); + old_current = slv.mkTerm(SELECT, current_array, index); } - Expr query = em.mkExpr(kind::NOT, em.mkExpr(kind::AND, assertions)); + Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); cout << "Asserting " << query << " to CVC4 " << endl; - smt.assertFormula(query); + slv.assertFormula(query); cout << "Expect sat. " << endl; - cout << "CVC4: " << smt.checkSat(em.mkConst(true)) << endl; + cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; // Getting the model cout << "The satisfying model is: " << endl; - cout << " current_array = " << smt.getValue(current_array) << endl; - cout << " current_array[0] = " << smt.getValue(current_array0) << endl; + cout << " current_array = " << slv.getValue(current_array) << endl; + cout << " current_array[0] = " << slv.getValue(current_array0) << endl; return 0; } diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp deleted file mode 100644 index 111f71852..000000000 --- a/examples/api/combination-new.cpp +++ /dev/null @@ -1,139 +0,0 @@ -/********************* */ -/*! \file combination-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the capabilities of CVC4 - ** - ** A simple demonstration of how to use uninterpreted functions, combining this - ** with arithmetic, and extracting a model at the end of a satisfiable query. - ** The model is displayed using getValue(). - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace std; -using namespace CVC4::api; - -void prefixPrintGetValue(Solver& slv, Term t, int level = 0) -{ - cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl; - - for (const Term& c : t) - { - prefixPrintGetValue(slv, c, level + 1); - } -} - -int main() -{ - Solver slv; - slv.setOption("produce-models", "true"); // Produce Models - slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's - slv.setOption("dag-thresh", "0"); // Disable dagifying the output - slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language - slv.setLogic(string("QF_UFLIRA")); - - // Sorts - Sort u = slv.mkUninterpretedSort("u"); - Sort integer = slv.getIntegerSort(); - Sort boolean = slv.getBooleanSort(); - Sort uToInt = slv.mkFunctionSort(u, integer); - Sort intPred = slv.mkFunctionSort(integer, boolean); - - // Variables - Term x = slv.mkConst(u, "x"); - Term y = slv.mkConst(u, "y"); - - // Functions - Term f = slv.mkConst(uToInt, "f"); - Term p = slv.mkConst(intPred, "p"); - - // Constants - Term zero = slv.mkReal(0); - Term one = slv.mkReal(1); - - // Terms - Term f_x = slv.mkTerm(APPLY_UF, f, x); - Term f_y = slv.mkTerm(APPLY_UF, f, y); - Term sum = slv.mkTerm(PLUS, f_x, f_y); - Term p_0 = slv.mkTerm(APPLY_UF, p, zero); - Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y); - - // Construct the assertions - Term assertions = slv.mkTerm(AND, - vector<Term>{ - slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x) - slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y) - slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notTerm(), // not p(0) - p_f_y // p(f(y)) - }); - slv.assertFormula(assertions); - - cout << "Given the following assertions:" << endl - << assertions << endl << endl; - - cout << "Prove x /= y is entailed. " << endl - << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." - << endl - << endl; - - cout << "Call checkSat to show that the assertions are satisfiable. " - << endl - << "CVC4: " - << slv.checkSat() << "."<< endl << endl; - - cout << "Call slv.getValue(...) on terms of interest." - << endl; - cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl; - cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl; - cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl; - cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl; - cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y) - << endl << endl; - - cout << "Alternatively, iterate over assertions and call slv.getValue(...) " - << "on all terms." - << endl; - prefixPrintGetValue(slv, assertions); - - cout << endl << endl << "Alternatively, print the model." << endl << endl; - - slv.printModel(cout); - - cout << endl; - cout << "You can also use nested loops to iterate over terms." << endl; - for (Term::const_iterator it = assertions.begin(); - it != assertions.end(); - ++it) - { - cout << "term: " << *it << endl; - for (Term::const_iterator it2 = (*it).begin(); - it2 != (*it).end(); - ++it2) - { - cout << " + child: " << *it2 << std::endl; - } - } - cout << endl; - cout << "Alternatively, you can also use for-each loops." << endl; - for (const Term& t : assertions) - { - cout << "term: " << t << endl; - for (const Term& c : t) - { - cout << " + child: " << c << endl; - } - } - - return 0; -} diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index a3d25d7f0..817ed6f65 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -2,9 +2,9 @@ /*! \file combination.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Makai Mann + ** Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,86 +18,122 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -void prefixPrintGetValue(SmtEngine& smt, Expr e, int level = 0){ - for(int i = 0; i < level; ++i){ cout << '-'; } - cout << "smt.getValue(" << e << ") -> " << smt.getValue(e) << endl; +void prefixPrintGetValue(Solver& slv, Term t, int level = 0) +{ + cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl; - if(e.hasOperator() && e.getOperator().getKind() != kind::BUILTIN){ - prefixPrintGetValue(smt, e.getOperator(), level + 1); - } - - for(Expr::const_iterator term_i = e.begin(), term_end = e.end(); - term_i != term_end; ++term_i) + for (const Term& c : t) { - Expr curr = *term_i; - prefixPrintGetValue(smt, curr, level + 1); + prefixPrintGetValue(slv, c, level + 1); } } - -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setOption("produce-models", true); // Produce Models - smt.setOption("output-language", "cvc4"); // Set the output-language to CVC's - smt.setOption("dag-thresh", 0); //Disable dagifying the output - smt.setLogic(string("QF_UFLIRA")); +int main() +{ + Solver slv; + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's + slv.setOption("dag-thresh", "0"); // Disable dagifying the output + slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language + slv.setLogic(string("QF_UFLIRA")); // Sorts - SortType u = em.mkSort("u"); - Type integer = em.integerType(); - Type boolean = em.booleanType(); - Type uToInt = em.mkFunctionType(u, integer); - Type intPred = em.mkFunctionType(integer, boolean); + Sort u = slv.mkUninterpretedSort("u"); + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + Sort uToInt = slv.mkFunctionSort(u, integer); + Sort intPred = slv.mkFunctionSort(integer, boolean); // Variables - Expr x = em.mkVar("x", u); - Expr y = em.mkVar("y", u); + Term x = slv.mkConst(u, "x"); + Term y = slv.mkConst(u, "y"); // Functions - Expr f = em.mkVar("f", uToInt); - Expr p = em.mkVar("p", intPred); + Term f = slv.mkConst(uToInt, "f"); + Term p = slv.mkConst(intPred, "p"); // Constants - Expr zero = em.mkConst(Rational(0)); - Expr one = em.mkConst(Rational(1)); + Term zero = slv.mkReal(0); + Term one = slv.mkReal(1); // Terms - Expr f_x = em.mkExpr(kind::APPLY_UF, f, x); - Expr f_y = em.mkExpr(kind::APPLY_UF, f, y); - Expr sum = em.mkExpr(kind::PLUS, f_x, f_y); - Expr p_0 = em.mkExpr(kind::APPLY_UF, p, zero); - Expr p_f_y = em.mkExpr(kind::APPLY_UF, p, f_y); - - // Construct the assumptions - Expr assumptions = - em.mkExpr(kind::AND, - em.mkExpr(kind::LEQ, zero, f_x), // 0 <= f(x) - em.mkExpr(kind::LEQ, zero, f_y), // 0 <= f(y) - em.mkExpr(kind::LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notExpr(), // not p(0) - p_f_y); // p(f(y)) - smt.assertFormula(assumptions); - - cout << "Given the following assumptions:" << endl - << assumptions << endl - << "Prove x /= y is entailed. " - << "CVC4 says: " << smt.checkEntailed(em.mkExpr(kind::DISTINCT, x, y)) - << "." << endl; - - cout << "Now we call checksat on a trivial query to show that" << endl - << "the assumptions are satisfiable: " - << smt.checkSat(em.mkConst(true)) << "."<< endl; - - cout << "Finally, after a SAT call, we recursively call smt.getValue(...) on " - << "all of the assumptions to see what the satisfying model looks like." + Term f_x = slv.mkTerm(APPLY_UF, f, x); + Term f_y = slv.mkTerm(APPLY_UF, f, y); + Term sum = slv.mkTerm(PLUS, f_x, f_y); + Term p_0 = slv.mkTerm(APPLY_UF, p, zero); + Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y); + + // Construct the assertions + Term assertions = slv.mkTerm(AND, + vector<Term>{ + slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x) + slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y) + slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) + }); + slv.assertFormula(assertions); + + cout << "Given the following assertions:" << endl + << assertions << endl << endl; + + cout << "Prove x /= y is entailed. " << endl + << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." + << endl + << endl; + + cout << "Call checkSat to show that the assertions are satisfiable. " + << endl + << "CVC4: " + << slv.checkSat() << "."<< endl << endl; + + cout << "Call slv.getValue(...) on terms of interest." + << endl; + cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl; + cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl; + cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl; + cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl; + cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y) + << endl << endl; + + cout << "Alternatively, iterate over assertions and call slv.getValue(...) " + << "on all terms." << endl; - prefixPrintGetValue(smt, assumptions); + prefixPrintGetValue(slv, assertions); + + cout << endl << endl << "Alternatively, print the model." << endl << endl; + + slv.printModel(cout); + + cout << endl; + cout << "You can also use nested loops to iterate over terms." << endl; + for (Term::const_iterator it = assertions.begin(); + it != assertions.end(); + ++it) + { + cout << "term: " << *it << endl; + for (Term::const_iterator it2 = (*it).begin(); + it2 != (*it).end(); + ++it2) + { + cout << " + child: " << *it2 << std::endl; + } + } + cout << endl; + cout << "Alternatively, you can also use for-each loops." << endl; + for (const Term& t : assertions) + { + cout << "term: " << t << endl; + for (const Term& c : t) + { + cout << " + child: " << c << endl; + } + } return 0; } diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp deleted file mode 100644 index 9cfc7992c..000000000 --- a/examples/api/datatypes-new.cpp +++ /dev/null @@ -1,179 +0,0 @@ -/********************* */ -/*! \file datatypes-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An example of using inductive datatypes in CVC4 - ** - ** An example of using inductive datatypes in CVC4. - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace CVC4::api; - -void test(Solver& slv, Sort& consListSort) -{ - // Now our old "consListSpec" is useless--the relevant information - // has been copied out, so we can throw that spec away. We can get - // the complete spec for the datatype from the DatatypeSort, and - // this Datatype object has constructor symbols (and others) filled in. - - const Datatype& consList = consListSort.getDatatype(); - - // t = cons 0 nil - // - // Here, consList["cons"] gives you the DatatypeConstructor. To get - // the constructor symbol for application, use .getConstructor("cons"), - // which is equivalent to consList["cons"].getConstructor(). Note that - // "nil" is a constructor too, so it needs to be applied with - // APPLY_CONSTRUCTOR, even though it has no arguments. - Term t = slv.mkTerm( - APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - slv.mkReal(0), - slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); - - std::cout << "t is " << t << std::endl - << "sort of cons is " - << consList.getConstructorTerm("cons").getSort() << std::endl - << "sort of nil is " << consList.getConstructorTerm("nil").getSort() - << std::endl; - - // t2 = head(cons 0 nil), and of course this can be evaluated - // - // Here we first get the DatatypeConstructor for cons (with - // consList["cons"]) in order to get the "head" selector symbol - // to apply. - Term t2 = - slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); - - std::cout << "t2 is " << t2 << std::endl - << "simplify(t2) is " << slv.simplify(t2) << std::endl - << std::endl; - - // You can also iterate over a Datatype to get all its constructors, - // and over a DatatypeConstructor to get all its "args" (selectors) - for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i) - { - std::cout << "ctor: " << *i << std::endl; - for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end(); - ++j) - { - std::cout << " + arg: " << *j << std::endl; - } - } - std::cout << std::endl; - - // Alternatively, you can use for each loops. - for (const auto& c : consList) - { - std::cout << "ctor: " << c << std::endl; - for (const auto& s : c) - { - std::cout << " + arg: " << s << std::endl; - } - } - std::cout << std::endl; - - // You can also define parameterized datatypes. - // This example builds a simple parameterized list of sort T, with one - // constructor "cons". - Sort sort = slv.mkParamSort("T"); - DatatypeDecl paramConsListSpec = - slv.mkDatatypeDecl("paramlist", - sort); // give the datatype a name - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); - paramCons.addSelector("head", sort); - paramCons.addSelectorSelf("tail"); - paramConsListSpec.addConstructor(paramCons); - paramConsListSpec.addConstructor(paramNil); - - Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); - Sort paramConsIntListSort = - paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); - - const Datatype& paramConsList = paramConsListSort.getDatatype(); - - std::cout << "parameterized datatype sort is " << std::endl; - for (const DatatypeConstructor& ctor : paramConsList) - { - std::cout << "ctor: " << ctor << std::endl; - for (const DatatypeSelector& stor : ctor) - { - std::cout << " + arg: " << stor << std::endl; - } - } - - Term a = slv.mkConst(paramConsIntListSort, "a"); - std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - - Term head_a = slv.mkTerm( - APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); - std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() - << std::endl - << "sort of cons is " - << paramConsList.getConstructorTerm("cons").getSort() << std::endl - << std::endl; - Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50)); - std::cout << "Assert " << assertion << std::endl; - slv.assertFormula(assertion); - std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << slv.checkSat() << std::endl; -} - -int main() -{ - Solver slv; - // This example builds a simple "cons list" of integers, with - // two constructors, "cons" and "nil." - - // Building a datatype consists of two steps. - // First, the datatype is specified. - // Second, it is "resolved" to an actual sort, at which point function - // symbols are assigned to its constructors, selectors, and testers. - - DatatypeDecl consListSpec = - slv.mkDatatypeDecl("list"); // give the datatype a name - DatatypeConstructorDecl cons("cons"); - cons.addSelector("head", slv.getIntegerSort()); - cons.addSelectorSelf("tail"); - consListSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - consListSpec.addConstructor(nil); - - std::cout << "spec is:" << std::endl << consListSpec << std::endl; - - // Keep in mind that "DatatypeDecl" is the specification class for - // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. - // Now that our Datatype is fully specified, we can get a Sort for it. - // This step resolves the "SelfSort" reference and creates - // symbols for all the constructors, etc. - - Sort consListSort = slv.mkDatatypeSort(consListSpec); - - test(slv, consListSort); - - std::cout << std::endl - << ">>> Alternatively, use declareDatatype" << std::endl; - std::cout << std::endl; - - DatatypeConstructorDecl cons2("cons"); - cons2.addSelector("head", slv.getIntegerSort()); - cons2.addSelectorSelf("tail"); - DatatypeConstructorDecl nil2("nil"); - std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; - Sort consListSort2 = slv.declareDatatype("list2", ctors); - test(slv, consListSort2); - - return 0; -} diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index a749f0a0f..dd2c2695d 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -2,9 +2,9 @@ /*! \file datatypes.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz + ** Aina Niemetz, Andrew Reynolds, Makai Mann ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,135 +16,164 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; - -int main() { - ExprManager em; - SmtEngine smt(&em); - - // This example builds a simple "cons list" of integers, with - // two constructors, "cons" and "nil." - - // Building a datatype consists of two steps. First, the datatype - // is specified. Second, it is "resolved"---at which point function - // symbols are assigned to its constructors, selectors, and testers. - - Datatype consListSpec(&em, "list"); // give the datatype a name - DatatypeConstructor cons("cons"); - cons.addArg("head", em.integerType()); - cons.addArg("tail", DatatypeSelfType()); // a list - consListSpec.addConstructor(cons); - DatatypeConstructor nil("nil"); - consListSpec.addConstructor(nil); - - std::cout << "spec is:" << std::endl - << consListSpec << std::endl; - - // Keep in mind that "Datatype" is the specification class for - // datatypes---"Datatype" is not itself a CVC4 Type. Now that - // our Datatype is fully specified, we can get a Type for it. - // This step resolves the "SelfType" reference and creates - // symbols for all the constructors, etc. - - DatatypeType consListType = em.mkDatatypeType(consListSpec); +using namespace CVC4::api; +void test(Solver& slv, Sort& consListSort) +{ // Now our old "consListSpec" is useless--the relevant information // has been copied out, so we can throw that spec away. We can get - // the complete spec for the datatype from the DatatypeType, and + // the complete spec for the datatype from the DatatypeSort, and // this Datatype object has constructor symbols (and others) filled in. - const Datatype& consList = consListType.getDatatype(); + const Datatype& consList = consListSort.getDatatype(); - // e = cons 0 nil + // t = cons 0 nil // // Here, consList["cons"] gives you the DatatypeConstructor. To get // the constructor symbol for application, use .getConstructor("cons"), // which is equivalent to consList["cons"].getConstructor(). Note that // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. - Expr e = em.mkExpr(kind::APPLY_CONSTRUCTOR, - consList.getConstructor("cons"), - em.mkConst(Rational(0)), - em.mkExpr(kind::APPLY_CONSTRUCTOR, - consList.getConstructor("nil"))); - - std::cout << "e is " << e << std::endl - << "type of cons is " << consList.getConstructor("cons").getType() - << std::endl - << "type of nil is " << consList.getConstructor("nil").getType() + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + + std::cout << "t is " << t << std::endl + << "sort of cons is " + << consList.getConstructorTerm("cons").getSort() << std::endl + << "sort of nil is " << consList.getConstructorTerm("nil").getSort() << std::endl; - // e2 = head(cons 0 nil), and of course this can be evaluated + // t2 = head(cons 0 nil), and of course this can be evaluated // // Here we first get the DatatypeConstructor for cons (with // consList["cons"]) in order to get the "head" selector symbol // to apply. - Expr e2 = em.mkExpr(kind::APPLY_SELECTOR, - consList["cons"].getSelector("head"), - e); + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); - std::cout << "e2 is " << e2 << std::endl - << "simplify(e2) is " << smt.simplify(e2) - << std::endl << std::endl; + std::cout << "t2 is " << t2 << std::endl + << "simplify(t2) is " << slv.simplify(t2) << std::endl + << std::endl; // You can also iterate over a Datatype to get all its constructors, // and over a DatatypeConstructor to get all its "args" (selectors) - for(Datatype::iterator i = consList.begin(); i != consList.end(); ++i) { + for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i) + { std::cout << "ctor: " << *i << std::endl; - for(DatatypeConstructor::iterator j = (*i).begin(); j != (*i).end(); ++j) { + for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end(); + ++j) + { std::cout << " + arg: " << *j << std::endl; } } std::cout << std::endl; + // Alternatively, you can use for each loops. + for (const auto& c : consList) + { + std::cout << "ctor: " << c << std::endl; + for (const auto& s : c) + { + std::cout << " + arg: " << s << std::endl; + } + } + std::cout << std::endl; + // You can also define parameterized datatypes. // This example builds a simple parameterized list of sort T, with one // constructor "cons". - Type sort = em.mkSort("T", ExprManager::SORT_FLAG_PLACEHOLDER); - Datatype paramConsListSpec(&em, "list", std::vector<Type>{sort}); - DatatypeConstructor paramCons("cons"); - DatatypeConstructor paramNil("nil"); - paramCons.addArg("head", sort); - paramCons.addArg("tail", DatatypeSelfType()); + Sort sort = slv.mkParamSort("T"); + DatatypeDecl paramConsListSpec = + slv.mkDatatypeDecl("paramlist", + sort); // give the datatype a name + DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil"); + paramCons.addSelector("head", sort); + paramCons.addSelectorSelf("tail"); paramConsListSpec.addConstructor(paramCons); paramConsListSpec.addConstructor(paramNil); - DatatypeType paramConsListType = em.mkDatatypeType(paramConsListSpec); - Type paramConsIntListType = paramConsListType.instantiate(std::vector<Type>{em.integerType()}); + Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); + Sort paramConsIntListSort = + paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); - const Datatype& paramConsList = paramConsListType.getDatatype(); + const Datatype& paramConsList = paramConsListSort.getDatatype(); std::cout << "parameterized datatype sort is " << std::endl; for (const DatatypeConstructor& ctor : paramConsList) { std::cout << "ctor: " << ctor << std::endl; - for (const DatatypeConstructorArg& stor : ctor) + for (const DatatypeSelector& stor : ctor) { std::cout << " + arg: " << stor << std::endl; } } - Expr a = em.mkVar("a", paramConsIntListType); - std::cout << "Expr " << a << " is of type " << a.getType() << std::endl; + Term a = slv.mkConst(paramConsIntListSort, "a"); + std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Expr head_a = em.mkExpr( - kind::APPLY_SELECTOR, - paramConsList["cons"].getSelector("head"), - a); - std::cout << "head_a is " << head_a << " of type " << head_a.getType() + Term head_a = slv.mkTerm( + APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); + std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl - << "type of cons is " - << paramConsList.getConstructor("cons").getType() << std::endl + << "sort of cons is " + << paramConsList.getConstructorTerm("cons").getSort() << std::endl << std::endl; - - Expr assertion = em.mkExpr(kind::GT, head_a, em.mkConst(Rational(50))); + Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50)); std::cout << "Assert " << assertion << std::endl; - smt.assertFormula(assertion); - + slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << smt.checkSat()<< std::endl; + std::cout << "CVC4: " << slv.checkSat() << std::endl; +} + +int main() +{ + Solver slv; + // This example builds a simple "cons list" of integers, with + // two constructors, "cons" and "nil." + + // Building a datatype consists of two steps. + // First, the datatype is specified. + // Second, it is "resolved" to an actual sort, at which point function + // symbols are assigned to its constructors, selectors, and testers. + + DatatypeDecl consListSpec = + slv.mkDatatypeDecl("list"); // give the datatype a name + DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", slv.getIntegerSort()); + cons.addSelectorSelf("tail"); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil"); + consListSpec.addConstructor(nil); + + std::cout << "spec is:" << std::endl << consListSpec << std::endl; + + // Keep in mind that "DatatypeDecl" is the specification class for + // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + // Now that our Datatype is fully specified, we can get a Sort for it. + // This step resolves the "SelfSort" reference and creates + // symbols for all the constructors, etc. + + Sort consListSort = slv.mkDatatypeSort(consListSpec); + + test(slv, consListSort); + + std::cout << std::endl + << ">>> Alternatively, use declareDatatype" << std::endl; + std::cout << std::endl; + + DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); + cons2.addSelector("head", slv.getIntegerSort()); + cons2.addSelectorSelf("tail"); + DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil"); + std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; + Sort consListSort2 = slv.declareDatatype("list2", ctors); + test(slv, consListSort2); return 0; } diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp deleted file mode 100644 index 705cdd90f..000000000 --- a/examples/api/extract-new.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file extract-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector solver. - ** - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace std; -using namespace CVC4::api; - -int main() -{ - Solver slv; - slv.setLogic("QF_BV"); // Set the logic - - Sort bitvector32 = slv.mkBitVectorSort(32); - - Term x = slv.mkConst(bitvector32, "a"); - - Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); - Term x_31_1 = slv.mkTerm(ext_31_1, x); - - Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); - Term x_30_0 = slv.mkTerm(ext_30_0, x); - - Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); - Term x_31_31 = slv.mkTerm(ext_31_31, x); - - Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); - Term x_0_0 = slv.mkTerm(ext_0_0, x); - - Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); - cout << " Asserting: " << eq << endl; - slv.assertFormula(eq); - - Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); - cout << " Check entailment assuming: " << eq2 << endl; - cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(eq2) << endl; - - return 0; -} diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index e2558df28..6ff0db10d 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -2,9 +2,9 @@ /*! \file extract.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett + ** Aina Niemetz, Makai Mann ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,40 +16,40 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setLogic("QF_BV"); // Set the logic +int main() +{ + Solver slv; + slv.setLogic("QF_BV"); // Set the logic - Type bitvector32 = em.mkBitVectorType(32); + Sort bitvector32 = slv.mkBitVectorSort(32); - Expr x = em.mkVar("a", bitvector32); + Term x = slv.mkConst(bitvector32, "a"); - Expr ext_31_1 = em.mkConst(CVC4::BitVectorExtract(31,1)); - Expr x_31_1 = em.mkExpr(ext_31_1, x); + Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); - Expr ext_30_0 = em.mkConst(CVC4::BitVectorExtract(30,0)); - Expr x_30_0 = em.mkExpr(ext_30_0, x); + Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); - Expr ext_31_31 = em.mkConst(CVC4::BitVectorExtract(31,31)); - Expr x_31_31 = em.mkExpr(ext_31_31, x); + Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); - Expr ext_0_0 = em.mkConst(CVC4::BitVectorExtract(0,0)); - Expr x_0_0 = em.mkExpr(ext_0_0, x); + Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); - Expr eq = em.mkExpr(kind::EQUAL, x_31_1, x_30_0); + Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); cout << " Asserting: " << eq << endl; - smt.assertFormula(eq); + slv.assertFormula(eq); - Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0); - cout << " Querying: " << eq2 << endl; - cout << " Expect entailed. " << endl; - cout << " CVC4: " << smt.checkEntailed(eq2) << endl; + Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); + cout << " Check entailment assuming: " << eq2 << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(eq2) << endl; return 0; } diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp deleted file mode 100644 index f442c1412..000000000 --- a/examples/api/helloworld-new.cpp +++ /dev/null @@ -1,30 +0,0 @@ -/********************* */ -/*! \file helloworld-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A very simple CVC4 example - ** - ** A very simple CVC4 tutorial example. - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace CVC4::api; - -int main() -{ - Solver slv; - Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); - std::cout << helloworld << " is " << slv.checkEntailed(helloworld) - << std::endl; - return 0; -} diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 49a334504..873947522 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -2,9 +2,9 @@ /*! \file helloworld.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,14 +16,15 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; -int main() { - ExprManager em; - Expr helloworld = em.mkVar("Hello World!", em.booleanType()); - SmtEngine smt(&em); - std::cout << helloworld << " is " << smt.checkEntailed(helloworld) +using namespace CVC4::api; + +int main() +{ + Solver slv; + Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); + std::cout << helloworld << " is " << slv.checkEntailed(helloworld) << std::endl; return 0; } diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index bb2245a6f..e340a0b91 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -2,9 +2,9 @@ /*! \file BitVectors.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean + ** Morgan Deters, Liana Hadarean, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index 05232b8ab..6adb2a61d 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -2,9 +2,9 @@ /*! \file BitVectorsAndArrays.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean + ** Morgan Deters, Liana Hadarean, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -69,7 +69,7 @@ public class BitVectorsAndArrays { Expr old_current = em.mkExpr(Kind.SELECT, current_array, index); Expr two = em.mkConst(new BitVector(32, 2)); - vectorExpr assertions = new vectorExpr(); + vectorExpr assertions = new vectorExpr(em); for (int i = 1; i < k; ++i) { index = em.mkConst(new BitVector(index_size, new edu.stanford.CVC4.Integer(i))); Expr new_current = em.mkExpr(Kind.BITVECTOR_MULT, two, old_current); diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 108ae3cd3..0afcec0e4 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -1,19 +1,19 @@ set(EXAMPLES_API_JAVA - BitVectors - BitVectorsAndArrays ## disabled until bindings for the new API are in place (issue #2284) - #CVC4Streams - Combination - Datatypes - FloatingPointArith - HelloWorld - LinearArith - ## disabled until bindings for the new API are in place (issue #2284) - #PipedInput - Relations - Statistics - Strings - UnsatCores + # BitVectors + # BitVectorsAndArrays + # CVC4Streams + # Combination + # Datatypes + # Exceptions + # FloatingPointArith + # HelloWorld + # LinearArith + # PipedInput + # Relations + # Statistics + # Strings + # UnsatCores ) foreach(example ${EXAMPLES_API_JAVA}) diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java index e09c1b6f7..0ee3f98b2 100644 --- a/examples/api/java/CVC4Streams.java +++ b/examples/api/java/CVC4Streams.java @@ -2,9 +2,9 @@ /*! \file CVC4Streams.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 1299e2928..915aed78b 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -2,9 +2,9 @@ /*! \file Combination.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index 21f4a651e..5c9b0ef72 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -2,9 +2,9 @@ /*! \file Datatypes.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -32,11 +32,11 @@ public class Datatypes { // symbols are assigned to its constructors, selectors, and testers. Datatype consListSpec = new Datatype(em, "list"); // give a name - DatatypeConstructor cons = new DatatypeConstructor("cons"); + DatatypeConstructor cons = new DatatypeConstructor(em, "cons"); cons.addArg("head", em.integerType()); cons.addArg("tail", new DatatypeSelfType()); // a list consListSpec.addConstructor(cons); - DatatypeConstructor nil = new DatatypeConstructor("nil"); + DatatypeConstructor nil = new DatatypeConstructor(em, "nil"); consListSpec.addConstructor(nil); System.out.println("spec is:"); diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java new file mode 100644 index 000000000..f6b9d557c --- /dev/null +++ b/examples/api/java/Exceptions.java @@ -0,0 +1,56 @@ +/********************* */ +/*! \file Exceptions.java + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Catching CVC4 exceptions via the Java API. + ** + ** A simple demonstration of catching CVC4 execptions via the Java API. + **/ + +import edu.stanford.CVC4.*; + +public class Exceptions { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + smt.setOption("produce-models", new SExpr(true)); + + // Setting an invalid option + try { + smt.setOption("non-existing", new SExpr(true)); + System.exit(1); + } catch (edu.stanford.CVC4.Exception e) { + System.out.println(e.toString()); + } + + // Creating a term with an invalid type + try { + Type integer = em.integerType(); + Expr x = em.mkVar("x", integer); + Expr invalidExpr = em.mkExpr(Kind.AND, x, x); + smt.checkSat(invalidExpr); + System.exit(1); + } catch (edu.stanford.CVC4.Exception e) { + System.out.println(e.toString()); + } + + // Asking for a model after unsat result + try { + smt.checkSat(em.mkConst(false)); + smt.getModel(); + System.exit(1); + } catch (edu.stanford.CVC4.Exception e) { + System.out.println(e.toString()); + } + } +} diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index 9d2ceb1ae..c296a3fb1 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index a08f3d452..86e0c4da3 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -2,9 +2,9 @@ /*! \file HelloWorld.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index e060263b4..474a481f2 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -2,9 +2,9 @@ /*! \file LinearArith.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java index 0ab807e5d..42bea34cc 100644 --- a/examples/api/java/PipedInput.java +++ b/examples/api/java/PipedInput.java @@ -2,9 +2,9 @@ /*! \file PipedInput.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index 86a394062..f5c5db8a7 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -2,7 +2,7 @@ /*! \file Relations.java ** \verbatim ** Top contributors (to current version): - ** Mudathir Mahgoub + ** Mudathir Mohamed, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -64,13 +64,9 @@ This file uses the API to make a sat call equivalent to the following benchmark: (get-model) */ -public -class Relations -{ - public - static void main(String[] args) - { - System.load("/usr/local/lib/libcvc4jni.so"); +public class Relations { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); ExprManager manager = new ExprManager(); SmtEngine smtEngine = new SmtEngine(manager); @@ -86,7 +82,7 @@ class Relations // (declare-sort Person 0) Type personType = manager.mkSort("Person", 0); - vectorType vector1 = new vectorType(); + vectorType vector1 = new vectorType(manager); vector1.add(personType); // (Tuple Person) @@ -94,7 +90,7 @@ class Relations // (Set (Tuple Person)) SetType relationArity1 = manager.mkSetType(tupleArity1); - vectorType vector2 = new vectorType(); + vectorType vector2 = new vectorType(manager); vector2.add(personType); vector2.add(personType); // (Tuple Person Person) @@ -103,11 +99,11 @@ class Relations SetType relationArity2 = manager.mkSetType(tupleArity2); // empty set - EmptySet emptySet = new EmptySet(relationArity1); + EmptySet emptySet = new EmptySet(manager, relationArity1); Expr emptySetExpr = manager.mkConst(emptySet); // empty relation - EmptySet emptyRelation = new EmptySet(relationArity2); + EmptySet emptyRelation = new EmptySet(manager, relationArity2); Expr emptyRelationExpr = manager.mkConst(emptyRelation); // universe set @@ -134,9 +130,12 @@ class Relations // (assert (not (= females (as emptyset (Set (Tuple Person)))))) Expr femaleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty2); - // (assert (= (intersection males females) (as emptyset (Set (Tuple Person))))) - Expr malesFemalesIntersection = manager.mkExpr(Kind.INTERSECTION, males, females); - Expr malesAndFemalesAreDisjoint = manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr); + // (assert (= (intersection males females) (as emptyset (Set (Tuple + // Person))))) + Expr malesFemalesIntersection = + manager.mkExpr(Kind.INTERSECTION, males, females); + Expr malesAndFemalesAreDisjoint = + manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr); // (assert (not (= father (as emptyset (Set (Tuple Person Person)))))) // (assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) @@ -157,11 +156,13 @@ class Relations // (assert (= parent (union father mother))) Expr unionFatherMother = manager.mkExpr(Kind.UNION, father, mother); - Expr parentIsFatherOrMother = manager.mkExpr(Kind.EQUAL, parent, unionFatherMother); + Expr parentIsFatherOrMother = + manager.mkExpr(Kind.EQUAL, parent, unionFatherMother); // (assert (= parent (union father mother))) Expr transitiveClosure = manager.mkExpr(Kind.TCLOSURE, parent); - Expr descendantFormula = manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure); + Expr descendantFormula = + manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure); // (assert (= parent (union father mother))) Expr transpose = manager.mkExpr(Kind.TRANSPOSE, descendant); @@ -173,31 +174,32 @@ class Relations Expr xxTuple = manager.mkExpr(Kind.APPLY_CONSTRUCTOR, constructor, x, x); Expr member = manager.mkExpr(Kind.MEMBER, xxTuple, ancestor); Expr notMember = manager.mkExpr(Kind.NOT, member); - vectorExpr vectorExpr = new vectorExpr(); + vectorExpr vectorExpr = new vectorExpr(manager); vectorExpr.add(x); Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x); - Expr noSelfAncestor = manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember); + Expr noSelfAncestor = + manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember); // formulas Expr formula1 = manager.mkExpr(Kind.AND, - peopleAreTheUniverse, - maleSetIsNotEmpty, - femaleSetIsNotEmpty, - malesAndFemalesAreDisjoint); + peopleAreTheUniverse, + maleSetIsNotEmpty, + femaleSetIsNotEmpty, + malesAndFemalesAreDisjoint); Expr formula2 = manager.mkExpr(Kind.AND, - formula1, - fatherIsNotEmpty, - motherIsNotEmpty, - fathersAreMales, - mothersAreFemales); + formula1, + fatherIsNotEmpty, + motherIsNotEmpty, + fathersAreMales, + mothersAreFemales); Expr formula3 = manager.mkExpr(Kind.AND, - formula2, - parentIsFatherOrMother, - descendantFormula, - ancestorFormula, - noSelfAncestor); + formula2, + parentIsFatherOrMother, + descendantFormula, + ancestorFormula, + noSelfAncestor); // check sat Result result = smtEngine.checkSat(formula3); diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 8bf0effef..1f5264b5f 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java index 4a87c0a14..1d5594c67 100644 --- a/examples/api/java/Strings.java +++ b/examples/api/java/Strings.java @@ -2,9 +2,9 @@ /*! \file Strings.java ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang + ** Tianyi Liang, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index 6478aea5c..648e7f1d3 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -1,10 +1,10 @@ /********************* */ -/*! \file UnsatCore.java +/*! \file UnsatCores.java ** \verbatim ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp deleted file mode 100644 index 887c35d24..000000000 --- a/examples/api/linear_arith-new.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/********************* */ -/*! \file linear_arith-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 - ** - ** A simple demonstration of the linear arithmetic solving capabilities and - ** the push pop of CVC4. This also gives an example option. - **/ - -#include <iostream> - -#include "cvc4/api/cvc4cpp.h" - -using namespace std; -using namespace CVC4::api; - -int main() -{ - Solver slv; - slv.setLogic("QF_LIRA"); // Set the logic - - // Prove that if given x (Integer) and y (Real) then - // the maximum value of y - x is 2/3 - - // Sorts - Sort real = slv.getRealSort(); - Sort integer = slv.getIntegerSort(); - - // Variables - Term x = slv.mkConst(integer, "x"); - Term y = slv.mkConst(real, "y"); - - // Constants - Term three = slv.mkReal(3); - Term neg2 = slv.mkReal(-2); - Term two_thirds = slv.mkReal(2, 3); - - // Terms - Term three_y = slv.mkTerm(MULT, three, y); - Term diff = slv.mkTerm(MINUS, y, x); - - // Formulas - Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); - Term x_leq_y = slv.mkTerm(LEQ, x, y); - Term neg2_lt_x = slv.mkTerm(LT, neg2, x); - - Term assertions = - slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); - - cout << "Given the assertions " << assertions << endl; - slv.assertFormula(assertions); - - - slv.push(); - Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); - cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report ENTAILED." << endl; - cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds) - << endl; - slv.pop(); - - cout << endl; - - slv.push(); - Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); - slv.assertFormula(diff_is_two_thirds); - cout << "Show that the assertions are consistent with " << endl; - cout << diff_is_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report SAT." << endl; - cout << "Result from CVC4 is: " << slv.checkSat() << endl; - slv.pop(); - - cout << "Thus the maximum value of (y - x) is 2/3."<< endl; - - return 0; -} diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 9e605f85c..c60e17f85 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -2,9 +2,9 @@ /*! \file linear_arith.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,66 +17,66 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include "cvc4/api/cvc4cpp.h" using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setLogic("QF_LIRA"); // Set the logic +int main() +{ + Solver slv; + slv.setLogic("QF_LIRA"); // Set the logic // Prove that if given x (Integer) and y (Real) then // the maximum value of y - x is 2/3 - // Types - Type real = em.realType(); - Type integer = em.integerType(); + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); // Variables - Expr x = em.mkVar("x", integer); - Expr y = em.mkVar("y", real); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(real, "y"); // Constants - Expr three = em.mkConst(Rational(3)); - Expr neg2 = em.mkConst(Rational(-2)); - Expr two_thirds = em.mkConst(Rational(2,3)); + Term three = slv.mkReal(3); + Term neg2 = slv.mkReal(-2); + Term two_thirds = slv.mkReal(2, 3); // Terms - Expr three_y = em.mkExpr(kind::MULT, three, y); - Expr diff = em.mkExpr(kind::MINUS, y, x); + Term three_y = slv.mkTerm(MULT, three, y); + Term diff = slv.mkTerm(MINUS, y, x); // Formulas - Expr x_geq_3y = em.mkExpr(kind::GEQ, x, three_y); - Expr x_leq_y = em.mkExpr(kind::LEQ, x, y); - Expr neg2_lt_x = em.mkExpr(kind::LT, neg2, x); + Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); + Term x_leq_y = slv.mkTerm(LEQ, x, y); + Term neg2_lt_x = slv.mkTerm(LT, neg2, x); - Expr assumptions = - em.mkExpr(kind::AND, x_geq_3y, x_leq_y, neg2_lt_x); + Term assertions = + slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); - cout << "Given the assumptions " << assumptions << endl; - smt.assertFormula(assumptions); + cout << "Given the assertions " << assertions << endl; + slv.assertFormula(assertions); - smt.push(); - Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds); + slv.push(); + Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; cout << "CVC4 should report ENTAILED." << endl; - cout << "Result from CVC4 is: " << smt.checkEntailed(diff_leq_two_thirds) + cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds) << endl; - smt.pop(); + slv.pop(); cout << endl; - smt.push(); - Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds); - smt.assertFormula(diff_is_two_thirds); - cout << "Show that the asserts are consistent with " << endl; + slv.push(); + Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); + slv.assertFormula(diff_is_two_thirds); + cout << "Show that the assertions are consistent with " << endl; cout << diff_is_two_thirds << " with CVC4." << endl; cout << "CVC4 should report SAT." << endl; - cout << "Result from CVC4 is: " << smt.checkSat(em.mkConst(true)) << endl; - smt.pop(); + cout << "Result from CVC4 is: " << slv.checkSat() << endl; + slv.pop(); cout << "Thus the maximum value of (y - x) is 2/3."<< endl; diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt new file mode 100644 index 000000000..6e255c5b1 --- /dev/null +++ b/examples/api/python/CMakeLists.txt @@ -0,0 +1,27 @@ +set(EXAMPLES_API_PYTHON + exceptions +) + +find_package(PythonInterp REQUIRED) + +# Find Python bindings in the corresponding python-*/site-packages directory. +# Lookup Python module directory and store path in PYTHON_MODULE_PATH. +execute_process(COMMAND + ${PYTHON_EXECUTABLE} -c + "from distutils.sysconfig import get_python_lib;\ + print(get_python_lib(plat_specific=True,\ + prefix='${CMAKE_PREFIX_PATH}/../..'))" + OUTPUT_VARIABLE PYTHON_MODULE_PATH + OUTPUT_STRIP_TRAILING_WHITESPACE) + +foreach(example ${EXAMPLES_API_PYTHON}) + set(example_test example/api/python/${example}) + add_test( + NAME ${example_test} + COMMAND + "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/api/python/${example}.py" + ) + set_tests_properties(${example_test} PROPERTIES + LABELS "example" + ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}) +endforeach() diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 8e4e1b682..f12e79541 100755 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -84,7 +84,7 @@ if __name__ == "__main__": print("Checking entailment assuming:", new_x_eq_new_x_) print("Expect ENTAILED.") - print("CVC4:", slv.checkEntailment(new_x_eq_new_x_)) + print("CVC4:", slv.checkEntailed(new_x_eq_new_x_)) print("Popping context.") slv.pop() diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index ded268d69..1a67f5661 100755 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -65,8 +65,8 @@ def test(slv, consListSort): # constructor "cons". sort = slv.mkParamSort("T") paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort) - paramCons = pycvc4.DatatypeConstructorDecl("cons") - paramNil = pycvc4.DatatypeConstructorDecl("nil") + paramCons = slv.mkDatatypeConstructorDecl("cons") + paramNil = slv.mkDatatypeConstructorDecl("nil") paramCons.addSelector("head", sort) paramCons.addSelectorSelf("tail") paramConsListSpec.addConstructor(paramCons) @@ -102,11 +102,11 @@ if __name__ == "__main__": # symbols are assigned to its constructors, selectors, and testers. consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name - cons = pycvc4.DatatypeConstructorDecl("cons") + cons = slv.mkDatatypeConstructorDecl("cons") cons.addSelector("head", slv.getIntegerSort()) cons.addSelectorSelf("tail") consListSpec.addConstructor(cons) - nil = pycvc4.DatatypeConstructorDecl("nil") + nil = slv.mkDatatypeConstructorDecl("nil") consListSpec.addConstructor(nil) print("spec is {}".format(consListSpec)) @@ -122,10 +122,10 @@ if __name__ == "__main__": print("### Alternatively, use declareDatatype") - cons2 = pycvc4.DatatypeConstructorDecl("cons") + cons2 = slv.mkDatatypeConstructorDecl("cons") cons2.addSelector("head", slv.getIntegerSort()) cons2.addSelectorSelf("tail") - nil2 = pycvc4.DatatypeConstructorDecl("nil") + nil2 = slv.mkDatatypeConstructorDecl("nil") ctors = [cons2, nil2] consListSort2 = slv.declareDatatype("list2", ctors) test(slv, consListSort2) diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py new file mode 100644 index 000000000..780f75bf7 --- /dev/null +++ b/examples/api/python/exceptions.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python + +##################### +## \file exceptions.py +## \verbatim +## Top contributors (to current version): +## Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief Catching CVC4 exceptions with the legacy Python API. +## +## A simple demonstration of catching CVC4 execptions with the legacy Python +## API. + +import CVC4 +import sys + + +def main(): + em = CVC4.ExprManager() + smt = CVC4.SmtEngine(em) + + smt.setOption("produce-models", CVC4.SExpr("true")) + + # Setting an invalid option + try: + smt.setOption("non-existing", CVC4.SExpr("true")) + return 1 + except CVC4.Exception as e: + print(e.toString()) + + # Creating a term with an invalid type + try: + integer = em.integerType() + x = em.mkVar("x", integer) + invalidExpr = em.mkExpr(CVC4.AND, x, x) + smt.checkSat(invalidExpr) + return 1 + except CVC4.Exception as e: + print(e.toString()) + + # Asking for a model after unsat result + try: + smt.checkSat(em.mkBoolConst(False)) + smt.getModel() + return 1 + except CVC4.Exception as e: + print(e.toString()) + + return 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py new file mode 100755 index 000000000..c92666c0b --- /dev/null +++ b/examples/api/python/floating_point.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python + +##################### +#! \file floating_point.py + ## \verbatim + ## Top contributors (to current version): + ## Eva Darulova, Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## floating point solver through the Python API contributed by Eva + ## Darulova. This requires building CVC4 with symfpu. + +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setOption("produce-models", "true") + slv.setLogic("FP") + + # single 32-bit precision + fp32 = slv.mkFloatingPointSort(8, 24) + + # the standard rounding mode + rm = slv.mkRoundingMode(pycvc4.RoundNearestTiesToEven) + + # create a few single-precision variables + x = slv.mkConst(fp32, 'x') + y = slv.mkConst(fp32, 'y') + z = slv.mkConst(fp32, 'z') + + # check floating-point arithmetic is commutative, i.e. x + y == y + x + commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPPlus, rm, x, y), slv.mkTerm(kinds.FPPlus, rm, y, x)) + + slv.push() + slv.assertFormula(slv.mkTerm(kinds.Not, commutative)) + print("Checking floating-point commutativity") + print("Expect SAT (property does not hold for NaN and Infinities).") + print("CVC4:", slv.checkSat()) + print("Model for x:", slv.getValue(x)) + print("Model for y:", slv.getValue(y)) + + # disallow NaNs and Infinities + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, x))) + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, x))) + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, y))) + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, y))) + + print("Checking floating-point commutativity assuming x and y are not NaN or Infinity") + print("Expect UNSAT.") + print("CVC4:", slv.checkSat()) + + # check floating-point arithmetic is not associative + slv.pop() + + # constrain x, y, z between -3.14 and 3.14 (also disallows NaN and infinity) + a = slv.mkFloatingPoint(8, 24, slv.mkBitVector("11000000010010001111010111000011", 2)) # -3.14 + b = slv.mkFloatingPoint(8, 24, slv.mkBitVector("01000000010010001111010111000011", 2)) # 3.14 + + bounds_x = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, x), slv.mkTerm(kinds.FPLeq, x, b)) + bounds_y = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, y), slv.mkTerm(kinds.FPLeq, y, b)) + bounds_z = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, z), slv.mkTerm(kinds.FPLeq, z, b)) + slv.assertFormula(slv.mkTerm(kinds.And, slv.mkTerm(kinds.And, bounds_x, bounds_y), bounds_z)) + + # (x + y) + z == x + (y + z) + lhs = slv.mkTerm(kinds.FPPlus, rm, slv.mkTerm(kinds.FPPlus, rm, x, y), z) + rhs = slv.mkTerm(kinds.FPPlus, rm, x, slv.mkTerm(kinds.FPPlus, rm, y, z)) + associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs)) + + slv.assertFormula(associative) + + print("Checking floating-point associativity") + print("Expect SAT.") + print("CVC4:", slv.checkSat()) + print("Model for x:", slv.getValue(x)) + print("Model for y:", slv.getValue(y)) + print("Model for z:", slv.getValue(z)) diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp deleted file mode 100644 index 21ef925df..000000000 --- a/examples/api/sets-new.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/********************* */ -/*! \file sets-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Reasoning about sets with CVC4. - ** - ** A simple demonstration of reasoning about sets with CVC4. - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace std; -using namespace CVC4::api; - -int main() -{ - Solver slv; - - // Optionally, set the logic. We need at least UF for equality predicate, - // integers (LIA) and sets (FS). - slv.setLogic("QF_UFLIAFS"); - - // Produce models - slv.setOption("produce-models", "true"); - slv.setOption("output-language", "smt2"); - - Sort integer = slv.getIntegerSort(); - Sort set = slv.mkSetSort(integer); - - // Verify union distributions over intersection - // (A union B) intersection C = (A intersection C) union (B intersection C) - { - Term A = slv.mkConst(set, "A"); - Term B = slv.mkConst(set, "B"); - Term C = slv.mkConst(set, "C"); - - Term unionAB = slv.mkTerm(UNION, A, B); - Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); - - Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); - Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); - Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); - - Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) - << "." << endl; - } - - // Verify emptset is a subset of any set - { - Term A = slv.mkConst(set, "A"); - Term emptyset = slv.mkEmptySet(set); - - Term theorem = slv.mkTerm(SUBSET, emptyset, A); - - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) - << "." << endl; - } - - // Find me an element in {1, 2} intersection {2, 3}, if there is one. - { - Term one = slv.mkReal(1); - Term two = slv.mkReal(2); - Term three = slv.mkReal(3); - - Term singleton_one = slv.mkTerm(SINGLETON, one); - Term singleton_two = slv.mkTerm(SINGLETON, two); - Term singleton_three = slv.mkTerm(SINGLETON, three); - Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); - Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); - Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); - - Term x = slv.mkConst(integer, "x"); - - Term e = slv.mkTerm(MEMBER, x, intersection); - - Result result = slv.checkSatAssuming(e); - cout << "CVC4 reports: " << e << " is " << result << "." << endl; - - if (result.isSat()) - { - cout << "For instance, " << slv.getValue(x) << " is a member." << endl; - } - } -} diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index eb6a5a350..aa70b4ee4 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -2,9 +2,9 @@ /*! \file sets.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,82 +16,80 @@ #include <iostream> -#include <cvc4/cvc4.h> -#include <cvc4/options/set_language.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); +int main() +{ + Solver slv; // Optionally, set the logic. We need at least UF for equality predicate, // integers (LIA) and sets (FS). - smt.setLogic("QF_UFLIAFS"); + slv.setLogic("QF_UFLIAFS"); // Produce models - smt.setOption("produce-models", true); + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); - // Set output language to SMTLIB2 - cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); - - Type integer = em.integerType(); - Type set = em.mkSetType(integer); + Sort integer = slv.getIntegerSort(); + Sort set = slv.mkSetSort(integer); // Verify union distributions over intersection // (A union B) intersection C = (A intersection C) union (B intersection C) { - Expr A = em.mkVar("A", set); - Expr B = em.mkVar("B", set); - Expr C = em.mkVar("C", set); + Term A = slv.mkConst(set, "A"); + Term B = slv.mkConst(set, "B"); + Term C = slv.mkConst(set, "C"); - Expr unionAB = em.mkExpr(kind::UNION, A, B); - Expr lhs = em.mkExpr(kind::INTERSECTION, unionAB, C); + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); - Expr intersectionAC = em.mkExpr(kind::INTERSECTION, A, C); - Expr intersectionBC = em.mkExpr(kind::INTERSECTION, B, C); - Expr rhs = em.mkExpr(kind::UNION, intersectionAC, intersectionBC); + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); - Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs); + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem) + cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } // Verify emptset is a subset of any set { - Expr A = em.mkVar("A", set); - Expr emptyset = em.mkConst(EmptySet(set)); + Term A = slv.mkConst(set, "A"); + Term emptyset = slv.mkEmptySet(set); - Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A); + Term theorem = slv.mkTerm(SUBSET, emptyset, A); - cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem) + cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } // Find me an element in {1, 2} intersection {2, 3}, if there is one. { - Expr one = em.mkConst(Rational(1)); - Expr two = em.mkConst(Rational(2)); - Expr three = em.mkConst(Rational(3)); + Term one = slv.mkReal(1); + Term two = slv.mkReal(2); + Term three = slv.mkReal(3); - Expr singleton_one = em.mkExpr(kind::SINGLETON, one); - Expr singleton_two = em.mkExpr(kind::SINGLETON, two); - Expr singleton_three = em.mkExpr(kind::SINGLETON, three); - Expr one_two = em.mkExpr(kind::UNION, singleton_one, singleton_two); - Expr two_three = em.mkExpr(kind::UNION, singleton_two, singleton_three); - Expr intersection = em.mkExpr(kind::INTERSECTION, one_two, two_three); + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); + Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); - Expr x = em.mkVar("x", integer); + Term x = slv.mkConst(integer, "x"); - Expr e = em.mkExpr(kind::MEMBER, x, intersection); + Term e = slv.mkTerm(MEMBER, x, intersection); - Result result = smt.checkSat(e); + Result result = slv.checkSatAssuming(e); cout << "CVC4 reports: " << e << " is " << result << "." << endl; - if(result == Result::SAT) { - cout << "For instance, " << smt.getValue(x) << " is a member." << endl; + if (result.isSat()) + { + cout << "For instance, " << slv.getValue(x) << " is a member." << endl; } } } diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp deleted file mode 100644 index e83ab89ff..000000000 --- a/examples/api/strings-new.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/********************* */ -/*! \file strings-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Reasoning about strings with CVC4 via C++ API. - ** - ** A simple demonstration of reasoning about strings with CVC4 via C++ API. - **/ - -#include <iostream> - -#include <cvc4/api/cvc4cpp.h> - -using namespace CVC4::api; - -int main() -{ - Solver slv; - - // Set the logic - slv.setLogic("S"); - // Produce models - slv.setOption("produce-models", "true"); - // The option strings-exp is needed - slv.setOption("strings-exp", "true"); - // Set output language to SMTLIB2 - slv.setOption("output-language", "smt2"); - - // String type - Sort string = slv.getStringSort(); - - // std::string - std::string str_ab("ab"); - // String constants - Term ab = slv.mkString(str_ab); - Term abc = slv.mkString("abc"); - // String variables - Term x = slv.mkConst(string, "x"); - Term y = slv.mkConst(string, "y"); - Term z = slv.mkConst(string, "z"); - - // String concatenation: x.ab.y - Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); - // String concatenation: abc.z - Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); - // x.ab.y = abc.z - Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); - - // Length of y: |y| - Term leny = slv.mkTerm(STRING_LENGTH, y); - // |y| >= 0 - Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0)); - - // Regular expression: (ab[c-e]*f)|g|h - Term r = slv.mkTerm(REGEXP_UNION, - slv.mkTerm(REGEXP_CONCAT, - slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")), - slv.mkTerm(REGEXP_STAR, - slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))), - slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))), - slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")), - slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h"))); - - // String variables - Term s1 = slv.mkConst(string, "s1"); - Term s2 = slv.mkConst(string, "s2"); - // String concatenation: s1.s2 - Term s = slv.mkTerm(STRING_CONCAT, s1, s2); - - // s1.s2 in (ab[c-e]*f)|g|h - Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); - - // Make a query - Term q = slv.mkTerm(AND, - formula1, - formula2, - formula3); - - // check sat - Result result = slv.checkSatAssuming(q); - std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; - - if(result.isSat()) - { - std::cout << " x = " << slv.getValue(x) << std::endl; - std::cout << " s1.s2 = " << slv.getValue(s) << std::endl; - } -} diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 661ae0e77..6a0e10918 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -2,9 +2,9 @@ /*! \file strings.cpp ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Tim King + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,86 +16,80 @@ #include <iostream> -#include <cvc4/cvc4.h> -#include <cvc4/options/set_language.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); +int main() +{ + Solver slv; // Set the logic - smt.setLogic("S"); - + slv.setLogic("S"); // Produce models - smt.setOption("produce-models", true); - + slv.setOption("produce-models", "true"); // The option strings-exp is needed - smt.setOption("strings-exp", true); - + slv.setOption("strings-exp", "true"); // Set output language to SMTLIB2 - std::cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); + slv.setOption("output-language", "smt2"); // String type - Type string = em.stringType(); + Sort string = slv.getStringSort(); // std::string - std::string std_str_ab("ab"); - // CVC4::String - CVC4::String cvc4_str_ab(std_str_ab); - CVC4::String cvc4_str_abc("abc"); + std::string str_ab("ab"); // String constants - Expr ab = em.mkConst(cvc4_str_ab); - Expr abc = em.mkConst(CVC4::String("abc")); + Term ab = slv.mkString(str_ab); + Term abc = slv.mkString("abc"); // String variables - Expr x = em.mkVar("x", string); - Expr y = em.mkVar("y", string); - Expr z = em.mkVar("z", string); + Term x = slv.mkConst(string, "x"); + Term y = slv.mkConst(string, "y"); + Term z = slv.mkConst(string, "z"); // String concatenation: x.ab.y - Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y); + Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); // String concatenation: abc.z - Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z); + Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); // x.ab.y = abc.z - Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs); + Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); // Length of y: |y| - Expr leny = em.mkExpr(kind::STRING_LENGTH, y); + Term leny = slv.mkTerm(STRING_LENGTH, y); // |y| >= 0 - Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0))); + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0)); // Regular expression: (ab[c-e]*f)|g|h - Expr r = em.mkExpr(kind::REGEXP_UNION, - em.mkExpr(kind::REGEXP_CONCAT, - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))), - em.mkExpr(kind::REGEXP_STAR, - em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))), - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))), - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))), - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h")))); + Term r = slv.mkTerm(REGEXP_UNION, + slv.mkTerm(REGEXP_CONCAT, + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")), + slv.mkTerm(REGEXP_STAR, + slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h"))); // String variables - Expr s1 = em.mkVar("s1", string); - Expr s2 = em.mkVar("s2", string); + Term s1 = slv.mkConst(string, "s1"); + Term s2 = slv.mkConst(string, "s2"); // String concatenation: s1.s2 - Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2); + Term s = slv.mkTerm(STRING_CONCAT, s1, s2); // s1.s2 in (ab[c-e]*f)|g|h - Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r); + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); // Make a query - Expr q = em.mkExpr(kind::AND, + Term q = slv.mkTerm(AND, formula1, formula2, formula3); // check sat - Result result = smt.checkSat(q); + Result result = slv.checkSatAssuming(q); std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; - if(result == Result::SAT) { - std::cout << " x = " << smt.getValue(x) << std::endl; - std::cout << " s1.s2 = " << smt.getValue(s) << std::endl; + if(result.isSat()) + { + std::cout << " x = " << slv.getValue(x) << std::endl; + std::cout << " s1.s2 = " << slv.getValue(s) << std::endl; } } diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index 449d8d060..1d1794a1a 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -2,9 +2,9 @@ /*! \file sygus-fun.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Andrew Reynolds + ** Abdalrhman Mohamed ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 8536706ce..cc139d2e5 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -2,9 +2,9 @@ /*! \file sygus-grammar.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Andrew Reynolds + ** Abdalrhman Mohamed ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 7deb5cc83..3638a78db 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -2,9 +2,9 @@ /*! \file sygus-inv.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Andrew Reynolds + ** Abdalrhman Mohamed ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp index a09da39c4..0d7da9e8b 100644 --- a/examples/hashsmt/sha1.hpp +++ b/examples/hashsmt/sha1.hpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index ea93db144..1a89058a7 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index b53f4b149..e9d967b96 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Aina Niemetz, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index b26e3b4d3..f44dec6b8 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h index ad08a63ae..9674a66ce 100644 --- a/examples/hashsmt/word.h +++ b/examples/hashsmt/word.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index 2ad1ea84e..84cdfe6c4 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index dfbde05f5..ac325e57d 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 8ea3cf862..f09a0abce 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index cf6377d98..8094aae36 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 916ada0d9..ccc1e558b 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index 2750ee191..9e42418f9 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 638f7c452..0d84aec13 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 0d263cb97..5db33892f 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Kshitij Bansal, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -341,16 +341,26 @@ int main(int argc, char* argv[]) DefineFunctionCommand* definefun = dynamic_cast<DefineFunctionCommand*>(cmd); Command* new_cmd = NULL; - if(assert) { + if (assert) + { Expr newexpr = m.collectSortsExpr(assert->getExpr()); new_cmd = new AssertCommand(newexpr); - } else if(declarefun) { + } + else if (declarefun) + { Expr newfunc = m.collectSortsExpr(declarefun->getFunction()); - new_cmd = new DeclareFunctionCommand(declarefun->getSymbol(), newfunc, declarefun->getType()); - } else if(definefun) { + new_cmd = new DeclareFunctionCommand( + declarefun->getSymbol(), newfunc, declarefun->getType()); + } + else if (definefun) + { Expr newfunc = m.collectSortsExpr(definefun->getFunction()); Expr newformula = m.collectSortsExpr(definefun->getFormula()); - new_cmd = new DefineFunctionCommand(definefun->getSymbol(), newfunc, definefun->getFormals(), newformula); + new_cmd = new DefineFunctionCommand(definefun->getSymbol(), + newfunc, + definefun->getFormals(), + newformula, + false); } if(new_cmd == NULL) { diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index cfd14b089..64c2b12c1 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -2,9 +2,9 @@ /*! \file simple_vc_cxx.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic + ** Morgan Deters, Dejan Jovanovic, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,43 +16,42 @@ ** identical. **/ -#include <iostream> +#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> +#include <iostream> -using namespace std; -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); + Solver slv; // Prove that for integers x and y: // x > 0 AND y > 0 => 2x + y >= 3 - Type integer = em.integerType(); + Sort integer = slv.getIntegerSort(); - Expr x = em.mkVar("x", integer); - Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(Rational(0)); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(integer, "y"); + Term zero = slv.mkReal(0); - Expr x_positive = em.mkExpr(kind::GT, x, zero); - Expr y_positive = em.mkExpr(kind::GT, y, zero); + Term x_positive = slv.mkTerm(Kind::GT, x, zero); + Term y_positive = slv.mkTerm(Kind::GT, y, zero); - Expr two = em.mkConst(Rational(2)); - Expr twox = em.mkExpr(kind::MULT, two, x); - Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); + Term two = slv.mkReal(2); + Term twox = slv.mkTerm(Kind::MULT, two, x); + Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y); - Expr three = em.mkConst(Rational(3)); - Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); + Term three = slv.mkReal(3); + Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); - Expr formula = - em.mkExpr(kind::AND, x_positive, y_positive). - impExpr(twox_plus_y_geq_3); + Term formula = + slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); - cout << "Checking entailment of formula " << formula << " with CVC4." << endl; - cout << "CVC4 should report ENTAILED." << endl; - cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl; + std::cout << "Checking entailment of formula " << formula << " with CVC4." + << std::endl; + std::cout << "CVC4 should report ENTAILED." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula) + << std::endl; return 0; } diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 11bbe01e0..4d5767ebb 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,64 +14,63 @@ ** A simple demonstration of the C++ interface for quantifiers. **/ -#include <iostream> +#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> +#include <iostream> -using namespace std; -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); + Solver slv; // Prove that the following is unsatisfiable: // forall x. P( x ) ^ ~P( 5 ) - Type integer = em.integerType(); - Type boolean = em.booleanType(); - Type integerPredicate = em.mkFunctionType(integer, boolean); - - Expr p = em.mkVar("P", integerPredicate); - Expr x = em.mkBoundVar("x", integer); - + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + Sort integerPredicate = slv.mkFunctionSort(integer, boolean); + + Term p = slv.mkConst(integerPredicate, "P"); + Term x = slv.mkVar(integer, "x"); + // make forall x. P( x ) - Expr var_list = em.mkExpr(kind::BOUND_VAR_LIST, x); - Expr px = em.mkExpr(kind::APPLY_UF, p, x); - Expr quantpospx = em.mkExpr(kind::FORALL, var_list, px); - cout << "Made expression : " << quantpospx << endl; - + Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x); + Term px = slv.mkTerm(Kind::APPLY_UF, p, x); + Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px); + std::cout << "Made expression : " << quantpospx << std::endl; + //make ~P( 5 ) - Expr five = em.mkConst(Rational(5)); - Expr pfive = em.mkExpr(kind::APPLY_UF, p, five); - Expr negpfive = em.mkExpr(kind::NOT, pfive); - cout << "Made expression : " << negpfive << endl; - - Expr formula = em.mkExpr(kind::AND, quantpospx, negpfive); + Term five = slv.mkReal(5); + Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five); + Term negpfive = slv.mkTerm(Kind::NOT, pfive); + std::cout << "Made expression : " << negpfive << std::endl; - smt.assertFormula(formula); + Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive); - cout << "Checking SAT after asserting " << formula << " to CVC4." << endl; - cout << "CVC4 should report unsat." << endl; - cout << "Result from CVC4 is: " << smt.checkSat() << endl; + slv.assertFormula(formula); + std::cout << "Checking SAT after asserting " << formula << " to CVC4." + << std::endl; + std::cout << "CVC4 should report unsat." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; - SmtEngine smtp(&em); - - // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) - Expr pattern = em.mkExpr(kind::INST_PATTERN, px); - Expr pattern_list = em.mkExpr(kind::INST_PATTERN_LIST, pattern); - Expr quantpospx_pattern = em.mkExpr(kind::FORALL, var_list, px, pattern_list); - cout << "Made expression : " << quantpospx_pattern << endl; + slv.resetAssertions(); - Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive); + // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) + Term pattern = slv.mkTerm(Kind::INST_PATTERN, px); + Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern); + Term quantpospx_pattern = + slv.mkTerm(Kind::FORALL, var_list, px, pattern_list); + std::cout << "Made expression : " << quantpospx_pattern << std::endl; - smtp.assertFormula(formula_pattern); + Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive); - cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl; - cout << "CVC4 should report unsat." << endl; - cout << "Result from CVC4 is: " << smtp.checkSat() << endl; + slv.assertFormula(formula_pattern); + std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." + << std::endl; + std::cout << "CVC4 should report unsat." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; return 0; } diff --git a/examples/translator.cpp b/examples/translator.cpp index 4bdecf7ef..a76eda4b8 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -2,9 +2,9 @@ /*! \file translator.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Aina Niemetz + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim |