diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-29 15:35:44 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 17:35:44 -0500 |
commit | 19054b3b1d427e662d30d4322df2b2f2361353da (patch) | |
tree | 1ee878fd6c2c36b78ea33607a5668e6a6d8f7144 /examples | |
parent | 5cd6f0e5e910ad61ebc5045170842078818a3b80 (diff) |
Make ExprManager constructor private (#4669)
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
Diffstat (limited to 'examples')
-rw-r--r-- | examples/CMakeLists.txt | 39 | ||||
-rw-r--r-- | examples/api/java/CMakeLists.txt | 29 | ||||
-rw-r--r-- | examples/simple_vc_cxx.cpp | 45 | ||||
-rw-r--r-- | examples/simple_vc_quant_cxx.cpp | 79 |
4 files changed, 96 insertions, 96 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 6168a8e22..cd74698d7 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -58,31 +58,34 @@ 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() diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 31f62db56..0afcec0e4 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -1,20 +1,19 @@ set(EXAMPLES_API_JAVA - BitVectors - BitVectorsAndArrays ## disabled until bindings for the new API are in place (issue #2284) - #CVC4Streams - Combination - Datatypes - Exceptions - 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/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 26d785edc..64c2b12c1 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -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 83d011993..4d5767ebb 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -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; } |