summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
Diffstat (limited to 'examples')
-rw-r--r--examples/CMakeLists.txt39
-rw-r--r--examples/api/java/CMakeLists.txt29
-rw-r--r--examples/simple_vc_cxx.cpp45
-rw-r--r--examples/simple_vc_quant_cxx.cpp79
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback