From: Gereon Kremer Date: Wed, 26 May 2021 06:30:45 +0000 (+0200) Subject: Add more examples to the documentation (#6569) X-Git-Tag: cvc5-1.0.0~1694 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7440f0568b99842d87cb1f86eec21aed9f46b92a;p=cvc5.git Add more examples to the documentation (#6569) This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary) --- diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst new file mode 100644 index 000000000..d28beab14 --- /dev/null +++ b/docs/binary/binary.rst @@ -0,0 +1,7 @@ +Binary Documentation +==================== + +.. toctree:: + :maxdepth: 2 + + options diff --git a/docs/binary/options.rst b/docs/binary/options.rst new file mode 100644 index 000000000..6f9c613e7 --- /dev/null +++ b/docs/binary/options.rst @@ -0,0 +1,5 @@ +Commandline Options +=================== + +.. include-build-file:: options_generated.rst + diff --git a/docs/conf.py.in b/docs/conf.py.in index 9dc5255bd..6a23ff759 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -70,6 +70,7 @@ html_css_files = ['custom.css'] # -- Breathe configuration --------------------------------------------------- breathe_default_project = "cvc5" breathe_domain_by_extension = {"h" : "cpp"} +cpp_index_common_prefix = ["cvc5::api::"] # where to look for include-build-file ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}'] diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst index a2e928927..8d302d60c 100644 --- a/docs/cpp/cpp.rst +++ b/docs/cpp/cpp.rst @@ -1,3 +1,5 @@ +.. _cpp-api: + C++ API Documentation ===================== diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst new file mode 100644 index 000000000..354c86751 --- /dev/null +++ b/docs/examples/bitvectors.rst @@ -0,0 +1,8 @@ +Theory of Bit-Vectors +===================== + + +.. api-examples:: + ../../examples/api/cpp/bitvectors.cpp + ../../examples/api/java/BitVectors.java + ../../examples/api/python/bitvectors.py diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst new file mode 100644 index 000000000..9d63f36bd --- /dev/null +++ b/docs/examples/bitvectors_and_arrays.rst @@ -0,0 +1,8 @@ +Theory of Bit-Vectors and Arrays +================================ + + +.. api-examples:: + ../../examples/api/cpp/bitvectors_and_arrays.cpp + ../../examples/api/java/BitVectorsAndArrays.java + ../../examples/api/python/bitvectors_and_arrays.py diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst new file mode 100644 index 000000000..5f301a14f --- /dev/null +++ b/docs/examples/combination.rst @@ -0,0 +1,8 @@ +Theory Combination +================== + + +.. api-examples:: + ../../examples/api/cpp/combination.cpp + ../../examples/api/java/Combination.java + ../../examples/api/python/combination.py diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index 8200ebb14..abbb16964 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -1,8 +1,8 @@ -Datatypes -=========== +Theory of Datatypes +=================== .. api-examples:: - ../../examples/api/datatypes.cpp + ../../examples/api/cpp/datatypes.cpp ../../examples/api/java/Datatypes.java ../../examples/api/python/datatypes.py diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index ff3651857..528566a3e 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -1,9 +1,25 @@ Examples =========== +The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) and input languages can be used. +For every example, the same problem is constructed and solved using different input mechanisms. + + .. toctree:: :maxdepth: 2 helloworld + exceptions + bitvectors + bitvectors_and_arrays + extract datatypes - lineararith \ No newline at end of file + floatingpoint + lineararith + sequences + sets + strings + combination + sygus-fun + sygus-grammar + sygus-inv \ No newline at end of file diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst new file mode 100644 index 000000000..6598e8fb0 --- /dev/null +++ b/docs/examples/exceptions.rst @@ -0,0 +1,7 @@ +Exception Handling +====================================== + + +.. api-examples:: + ../../examples/api/java/Exceptions.java + ../../examples/api/python/exceptions.py diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst new file mode 100644 index 000000000..0108de948 --- /dev/null +++ b/docs/examples/extract.rst @@ -0,0 +1,7 @@ +Theory of Bit-Vectors: :code:`extract` +====================================== + + +.. api-examples:: + ../../examples/api/cpp/extract.cpp + ../../examples/api/python/extract.py diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst new file mode 100644 index 000000000..1b09102b2 --- /dev/null +++ b/docs/examples/floatingpoint.rst @@ -0,0 +1,7 @@ +Theory of Floating-Points +====================================== + + +.. api-examples:: + ../../examples/api/java/FloatingPointArith.java + ../../examples/api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index 202952bb6..cdc424dfa 100644 --- a/docs/examples/helloworld.rst +++ b/docs/examples/helloworld.rst @@ -5,6 +5,7 @@ This example shows the very basic usage of the API. We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver). .. api-examples:: - ../../examples/api/helloworld.cpp + ../../examples/api/cpp/helloworld.cpp ../../examples/api/java/HelloWorld.java ../../examples/api/python/helloworld.py + ../../examples/api/smtlib/helloworld.smt2 diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst index d772edbb3..29d84cae5 100644 --- a/docs/examples/lineararith.rst +++ b/docs/examples/lineararith.rst @@ -1,8 +1,13 @@ -Linear Arithmetic -================= +Theory of Linear Arithmetic +=========================== +This example asserts three constraints over an integer variable :code:`x` and a real variable :code:`y`. +Firstly, it checks that these constraints entail an upper bound on the difference :code:`y - x <= 2/3`. +Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` and checking for satisfiability. +The two checks are separated by using :code:`push` and :code:`pop`. .. api-examples:: - ../../examples/api/linear_arith.cpp + ../../examples/api/cpp/linear_arith.cpp ../../examples/api/java/LinearArith.java ../../examples/api/python/linear_arith.py + ../../examples/api/smtlib/linear_arith.smt2 diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst new file mode 100644 index 000000000..a6f9e2238 --- /dev/null +++ b/docs/examples/sequences.rst @@ -0,0 +1,7 @@ +Theory of Sequences +=================== + + +.. api-examples:: + ../../examples/api/cpp/sequences.cpp + ../../examples/api/python/sequences.py diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst new file mode 100644 index 000000000..71a6843c3 --- /dev/null +++ b/docs/examples/sets.rst @@ -0,0 +1,7 @@ +Theory of Sets +================= + + +.. api-examples:: + ../../examples/api/cpp/sets.cpp + ../../examples/api/python/sets.py diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst new file mode 100644 index 000000000..87f566363 --- /dev/null +++ b/docs/examples/strings.rst @@ -0,0 +1,8 @@ +Theory of Strings +================= + + +.. api-examples:: + ../../examples/api/cpp/strings.cpp + ../../examples/api/java/Strings.java + ../../examples/api/python/strings.py diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst new file mode 100644 index 000000000..3d5bddff1 --- /dev/null +++ b/docs/examples/sygus-fun.rst @@ -0,0 +1,7 @@ +SyGuS: Functions +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-fun.cpp + ../../examples/api/python/sygus-fun.py diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst new file mode 100644 index 000000000..3733fe2c3 --- /dev/null +++ b/docs/examples/sygus-grammar.rst @@ -0,0 +1,7 @@ +SyGuS: Grammars +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-grammar.cpp + ../../examples/api/python/sygus-grammar.py diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst new file mode 100644 index 000000000..f9698a720 --- /dev/null +++ b/docs/examples/sygus-inv.rst @@ -0,0 +1,7 @@ +SyGuS: Invariants +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-inv.cpp + ../../examples/api/python/sygus-inv.py diff --git a/docs/ext/examples.py b/docs/ext/examples.py index befb6c175..003726de4 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -22,6 +22,7 @@ class APIExamples(Directive): '.cpp': {'title': 'C++', 'lang': 'c++'}, '.java': {'title': 'Java', 'lang': 'java'}, '.py': {'title': 'Python', 'lang': 'python'}, + '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'}, } # The "arguments" are actually the content of the directive diff --git a/docs/genindex.rst b/docs/genindex.rst new file mode 100644 index 000000000..9e530fa2f --- /dev/null +++ b/docs/genindex.rst @@ -0,0 +1,2 @@ +Index +===== diff --git a/docs/index.rst b/docs/index.rst index 8d77790fb..fc82111e2 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -6,17 +6,13 @@ cvc5 API Documentation ====================== - -* :ref:`genindex` - - ---------------- - .. toctree:: :maxdepth: 1 + installation/installation + binary/binary cpp/cpp python/python - references examples/examples - options + references + genindex diff --git a/docs/installation/installation.rst b/docs/installation/installation.rst new file mode 100644 index 000000000..e50cd8d4b --- /dev/null +++ b/docs/installation/installation.rst @@ -0,0 +1,2 @@ +Installation +============ \ No newline at end of file diff --git a/docs/options.rst b/docs/options.rst deleted file mode 100644 index 6f9c613e7..000000000 --- a/docs/options.rst +++ /dev/null @@ -1,5 +0,0 @@ -Commandline Options -=================== - -.. include-build-file:: options_generated.rst - diff --git a/docs/python/python.rst b/docs/python/python.rst index 50d9077df..c3e425a7f 100644 --- a/docs/python/python.rst +++ b/docs/python/python.rst @@ -1,3 +1,5 @@ +.. _python-api: + Python API Documentation ======================== diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index a7ca31a7a..076715f2e 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -78,7 +78,7 @@ cvc5_add_example(simple_vc_quant_cxx "" "") # # argument to binary (for testing) # ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) -add_subdirectory(api) +add_subdirectory(api/cpp) # TODO(project issue $206): Port example to new API # add_subdirectory(nra-translate) # add_subdirectory(sets-translate) diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt deleted file mode 100644 index bff7caa4d..000000000 --- a/examples/api/CMakeLists.txt +++ /dev/null @@ -1,41 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Mathias Preiner, Abdalrhman Mohamed, Aina Niemetz -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 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. -# ############################################################################# -# -# The build system configuration. -## - -set(CVC5_EXAMPLES_API - bitvectors - bitvectors_and_arrays - combination - datatypes - extract - helloworld - linear_arith - sets - sequences - strings -) - -foreach(example ${CVC5_EXAMPLES_API}) - cvc5_add_example(${example} "" "api") -endforeach() - -set(SYGUS_EXAMPLES_API - sygus-fun - sygus-grammar - sygus-inv -) - -foreach(example ${SYGUS_EXAMPLES_API}) - cvc5_add_example(${example} "${example}.cpp utils.h utils.cpp" "api") -endforeach() diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp deleted file mode 100644 index 8768bd996..000000000 --- a/examples/api/bitvectors.cpp +++ /dev/null @@ -1,128 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Liana Hadarean, Makai Mann - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the solving capabilities of the CVC4 - * bit-vector solver. - * - */ - -#include - -#include - -using namespace std; -using namespace cvc5::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_ADD, 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 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_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp deleted file mode 100644 index 547b294a0..000000000 --- a/examples/api/bitvectors_and_arrays.cpp +++ /dev/null @@ -1,97 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Liana Hadarean - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the solving capabilities of the CVC4 - * bit-vector and array solvers. - * - */ - -#include - -#include -#include - -using namespace std; -using namespace cvc5::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 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/combination.cpp b/examples/api/combination.cpp deleted file mode 100644 index d47897a7c..000000000 --- a/examples/api/combination.cpp +++ /dev/null @@ -1,136 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Tim King, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the capabilities of cvc5 - * - * 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 - -#include - -using namespace std; -using namespace cvc5::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", "cvc"); // 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.mkInteger(0); - Term one = slv.mkInteger(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{ - 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 - << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." - << endl - << endl; - - cout << "Call checkSat to show that the assertions are satisfiable. " - << endl - << "cvc5: " - << 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; - 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/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt new file mode 100644 index 000000000..bff7caa4d --- /dev/null +++ b/examples/api/cpp/CMakeLists.txt @@ -0,0 +1,41 @@ +############################################################################### +# Top contributors (to current version): +# Mathias Preiner, Abdalrhman Mohamed, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################# +# +# The build system configuration. +## + +set(CVC5_EXAMPLES_API + bitvectors + bitvectors_and_arrays + combination + datatypes + extract + helloworld + linear_arith + sets + sequences + strings +) + +foreach(example ${CVC5_EXAMPLES_API}) + cvc5_add_example(${example} "" "api") +endforeach() + +set(SYGUS_EXAMPLES_API + sygus-fun + sygus-grammar + sygus-inv +) + +foreach(example ${SYGUS_EXAMPLES_API}) + cvc5_add_example(${example} "${example}.cpp utils.h utils.cpp" "api") +endforeach() diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp new file mode 100644 index 000000000..8768bd996 --- /dev/null +++ b/examples/api/cpp/bitvectors.cpp @@ -0,0 +1,128 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Liana Hadarean, Makai Mann + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the CVC4 + * bit-vector solver. + * + */ + +#include + +#include + +using namespace std; +using namespace cvc5::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_ADD, 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 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/cpp/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp new file mode 100644 index 000000000..547b294a0 --- /dev/null +++ b/examples/api/cpp/bitvectors_and_arrays.cpp @@ -0,0 +1,97 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the CVC4 + * bit-vector and array solvers. + * + */ + +#include + +#include +#include + +using namespace std; +using namespace cvc5::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 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/cpp/combination.cpp b/examples/api/cpp/combination.cpp new file mode 100644 index 000000000..d47897a7c --- /dev/null +++ b/examples/api/cpp/combination.cpp @@ -0,0 +1,136 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the capabilities of cvc5 + * + * 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 + +#include + +using namespace std; +using namespace cvc5::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", "cvc"); // 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.mkInteger(0); + Term one = slv.mkInteger(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{ + 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 + << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." + << endl + << endl; + + cout << "Call checkSat to show that the assertions are satisfiable. " + << endl + << "cvc5: " + << 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; + 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/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp new file mode 100644 index 000000000..76c6da0f0 --- /dev/null +++ b/examples/api/cpp/datatypes.cpp @@ -0,0 +1,178 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * An example of using inductive datatypes in CVC4. + */ + +#include + +#include + +using namespace cvc5::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.mkInteger(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 = slv.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("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{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.mkInteger(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 = 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 ctors = {cons2, nil2}; + Sort consListSort2 = slv.declareDatatype("list2", ctors); + test(slv, consListSort2); + + return 0; +} diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp new file mode 100644 index 000000000..d21c59d59 --- /dev/null +++ b/examples/api/cpp/extract.cpp @@ -0,0 +1,56 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Makai Mann, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the CVC4 + * bit-vector solver. + * + */ + +#include + +#include + +using namespace std; +using namespace cvc5::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/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp new file mode 100644 index 000000000..21eb8e8fc --- /dev/null +++ b/examples/api/cpp/helloworld.cpp @@ -0,0 +1,29 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A very simple CVC4 example. + */ + +#include + +#include + +using namespace cvc5::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/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp new file mode 100644 index 000000000..02ddd956c --- /dev/null +++ b/examples/api/cpp/linear_arith.cpp @@ -0,0 +1,83 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the linear arithmetic solving capabilities and + * the push pop of CVC4. This also gives an example option. + */ + +#include + +#include + +using namespace std; +using namespace cvc5::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.mkInteger(3); + Term neg2 = slv.mkInteger(-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/cpp/sequences.cpp b/examples/api/cpp/sequences.cpp new file mode 100644 index 000000000..5ee66048f --- /dev/null +++ b/examples/api/cpp/sequences.cpp @@ -0,0 +1,67 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Aina Niemetz, Tianyi Liang + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of reasoning about sequences with CVC4 via C++ API. + */ + +#include + +#include + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // Set the logic + slv.setLogic("QF_SLIA"); + // 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"); + + // Sequence sort + Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); + + // Sequence variables + Term x = slv.mkConst(intSeq, "x"); + Term y = slv.mkConst(intSeq, "y"); + + // Empty sequence + Term empty = slv.mkEmptySequence(slv.getIntegerSort()); + // Sequence concatenation: x.y.empty + Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty); + // Sequence length: |x.y.empty| + Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); + // |x.y.empty| > 1 + Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); + // Sequence unit: seq(1) + Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); + // x = seq(1) + Term formula2 = slv.mkTerm(EQUAL, x, unit); + + // Make a query + Term q = slv.mkTerm(AND, formula1, formula2); + + // 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 << " y = " << slv.getValue(y) << std::endl; + } +} diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp new file mode 100644 index 000000000..5c9652707 --- /dev/null +++ b/examples/api/cpp/sets.cpp @@ -0,0 +1,94 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Kshitij Bansal, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of reasoning about sets with CVC4. + */ + +#include + +#include + +using namespace std; +using namespace cvc5::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.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(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/cpp/strings.cpp b/examples/api/cpp/strings.cpp new file mode 100644 index 000000000..a952b31d1 --- /dev/null +++ b/examples/api/cpp/strings.cpp @@ -0,0 +1,94 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tianyi Liang, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of reasoning about strings with CVC4 via C++ API. + */ + +#include + +#include + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // Set the logic + slv.setLogic("QF_SLIA"); + // 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.mkInteger(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/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp new file mode 100644 index 000000000..0f96e72a7 --- /dev/null +++ b/examples/api/cpp/sygus-fun.cpp @@ -0,0 +1,142 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use the Sygus API to synthesize max and min + * functions. Here is the same problem written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-fun max ((x Int) (y Int)) Int + * ((Start Int) (StartBool Bool)) + * ((Start Int (0 1 x y + * (+ Start Start) + * (- Start Start) + * (ite StartBool Start Start))) + * (StartBool Bool ((and StartBool StartBool) + * (not StartBool) + * (<= Start Start))))) + * + * (synth-fun min ((x Int) (y Int)) Int) + * + * (declare-var x Int) + * (declare-var y Int) + * + * (constraint (>= (max x y) x)) + * (constraint (>= (max x y) y)) + * (constraint (or (= x (max x y)) + * (= y (max x y)))) + * (constraint (= (+ (max x y) (min x y)) + * (+ x y))) + * + * (check-synth) + * + * The printed output for this example should be equivalent to: + * ( + * (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + * (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + * ) + */ + +#include + +#include + +#include "utils.h" + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + + // declare input variables for the functions-to-synthesize + Term x = slv.mkVar(integer, "x"); + Term y = slv.mkVar(integer, "y"); + + // declare the grammar non-terminals + Term start = slv.mkVar(integer, "Start"); + Term start_bool = slv.mkVar(boolean, "StartBool"); + + // define the rules + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + + Term plus = slv.mkTerm(PLUS, start, start); + Term minus = slv.mkTerm(MINUS, start, start); + Term ite = slv.mkTerm(ITE, start_bool, start, start); + + Term And = slv.mkTerm(AND, start_bool, start_bool); + Term Not = slv.mkTerm(NOT, start_bool); + Term leq = slv.mkTerm(LEQ, start, start); + + // create the grammar object + Grammar g = slv.mkSygusGrammar({x, y}, {start, start_bool}); + + // bind each non-terminal to its rules + g.addRules(start, {zero, one, x, y, plus, minus, ite}); + g.addRules(start_bool, {And, Not, leq}); + + // declare the functions-to-synthesize. Optionally, provide the grammar + // constraints + Term max = slv.synthFun("max", {x, y}, integer, g); + Term min = slv.synthFun("min", {x, y}, integer); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + Term varY = slv.mkSygusVar(integer, "y"); + + Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY); + Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY); + + // add semantic constraints + // (constraint (>= (max x y) x)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX)); + + // (constraint (>= (max x y) y)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY)); + + // (constraint (or (= x (max x y)) + // (= y (max x y)))) + slv.addSygusConstraint(slv.mkTerm( + OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY))); + + // (constraint (= (+ (max x y) (min x y)) + // (+ x y))) + slv.addSygusConstraint(slv.mkTerm( + EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // ( + // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + // ) + std::vector terms = {max, min}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + + return 0; +} diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp new file mode 100644 index 000000000..ce5a1bc8b --- /dev/null +++ b/examples/api/cpp/sygus-grammar.cpp @@ -0,0 +1,132 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use Grammar to add syntax constraints to + * the Sygus solution for the identity function. Here is the same problem + * written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-fun id1 ((x Int)) Int + * ((Start Int)) ((Start Int ((- x) (+ x Start))))) + * + * (synth-fun id2 ((x Int)) Int + * ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) + * + * (synth-fun id3 ((x Int)) Int + * ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) + * + * (synth-fun id4 ((x Int)) Int + * ((Start Int)) ((Start Int ((- x) (+ x Start))))) + * + * (declare-var x Int) + * + * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + * + * (check-synth) + * + * The printed output for this example should look like: + * ( + * (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + * (define-fun id2 ((x Int)) Int x) + * (define-fun id3 ((x Int)) Int (+ x 0)) + * (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + * ) + */ + +#include + +#include + +#include "utils.h" + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + + // declare input variable for the function-to-synthesize + Term x = slv.mkVar(integer, "x"); + + // declare the grammar non-terminal + Term start = slv.mkVar(integer, "Start"); + + // define the rules + Term zero = slv.mkInteger(0); + Term neg_x = slv.mkTerm(UMINUS, x); + Term plus = slv.mkTerm(PLUS, x, start); + + // create the grammar object + Grammar g1 = slv.mkSygusGrammar({x}, {start}); + + // bind each non-terminal to its rules + g1.addRules(start, {neg_x, plus}); + + // copy the first grammar with all of its non-termainals and their rules + Grammar g2 = g1; + Grammar g3 = g1; + + // add parameters as rules for the start symbol. Similar to "(Variable Int)" + g2.addAnyVariable(start); + + // declare the functions-to-synthesize + Term id1 = slv.synthFun("id1", {x}, integer, g1); + Term id2 = slv.synthFun("id2", {x}, integer, g2); + + g3.addRule(start, zero); + + Term id3 = slv.synthFun("id3", {x}, integer, g3); + + // g1 is reusable as long as it remains unmodified after first use + Term id4 = slv.synthFun("id4", {x}, integer, g1); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + + Term id1_x = slv.mkTerm(APPLY_UF, id1, varX); + Term id2_x = slv.mkTerm(APPLY_UF, id2, varX); + Term id3_x = slv.mkTerm(APPLY_UF, id3, varX); + Term id4_x = slv.mkTerm(APPLY_UF, id4, varX); + + // add semantic constraints + // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + slv.addSygusConstraint(slv.mkTerm(EQUAL, {id1_x, id2_x, id3_x, id4_x, varX})); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // ( + // (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + // (define-fun id2 ((x Int)) Int x) + // (define-fun id3 ((x Int)) Int (+ x 0)) + // (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + // ) + std::vector terms = {id1, id2, id3, id4}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + + return 0; +} diff --git a/examples/api/cpp/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp new file mode 100644 index 000000000..f658fa33a --- /dev/null +++ b/examples/api/cpp/sygus-inv.cpp @@ -0,0 +1,97 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use the Sygus API to synthesize a simple + * invariant. Here is the same problem written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-inv inv-f ((x Int))) + * + * (define-fun pre-f ((x Int)) Bool + * (= x 0)) + * (define-fun trans-f ((x Int) (xp Int)) Bool + * (ite (< x 10) (= xp (+ x 1)) (= xp x))) + * (define-fun post-f ((x Int)) Bool + * (<= x 10)) + * + * (inv-constraint inv-f pre-f trans-f post-f) + * + * (check-synth) + * + * The printed output for this example should be equivalent to: + * ( + * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + * ) + */ + +#include + +#include + +#include "utils.h" + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + Term ten = slv.mkInteger(10); + + // declare input variables for functions + Term x = slv.mkVar(integer, "x"); + Term xp = slv.mkVar(integer, "xp"); + + // (ite (< x 10) (= xp (+ x 1)) (= xp x)) + Term ite = slv.mkTerm(ITE, + slv.mkTerm(LT, x, ten), + slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), + slv.mkTerm(EQUAL, xp, x)); + + // define the pre-conditions, transition relations, and post-conditions + Term pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(EQUAL, x, zero)); + Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite); + Term post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, x, ten)); + + // declare the invariant-to-synthesize + Term inv_f = slv.synthInv("inv-f", {x}); + + slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // ( + // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + // ) + std::vector terms = {inv_f}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + + return 0; +} diff --git a/examples/api/cpp/utils.cpp b/examples/api/cpp/utils.cpp new file mode 100644 index 000000000..69676819a --- /dev/null +++ b/examples/api/cpp/utils.cpp @@ -0,0 +1,69 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementations of utility methods. + */ + +#include "utils.h" + +#include + +/** + * Get the string version of define-fun command. + * @param f the function to print + * @param params the function parameters + * @param body the function body + * @return a string version of define-fun + */ +std::string defineFunToString(const cvc5::api::Term& f, + const std::vector params, + const cvc5::api::Term body) +{ + + cvc5::api::Sort sort = f.getSort(); + if (sort.isFunction()) + { + sort = sort.getFunctionCodomainSort(); + } + std::stringstream ss; + ss << "(define-fun " << f << " ("; + for (size_t i = 0, n = params.size(); i < n; ++i) + { + if (i > 0) + { + ss << ' '; + } + ss << '(' << params[i] << ' ' << params[i].getSort() << ')'; + } + ss << ") " << sort << ' ' << body << ')'; + return ss.str(); +} + +void printSynthSolutions(const std::vector& terms, + const std::vector& sols) +{ + std::cout << '(' << std::endl; + + for (size_t i = 0, n = terms.size(); i < n; ++i) + { + std::vector params; + cvc5::api::Term body; + if (sols[i].getKind() == cvc5::api::LAMBDA) + { + params.insert(params.end(), sols[i][0].begin(), sols[i][0].end()); + body = sols[i][1]; + } + std::cout << " " << defineFunToString(terms[i], params, body) + << std::endl; + } + std::cout << ')' << std::endl; +} diff --git a/examples/api/cpp/utils.h b/examples/api/cpp/utils.h new file mode 100644 index 000000000..69cddee26 --- /dev/null +++ b/examples/api/cpp/utils.h @@ -0,0 +1,29 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utility methods. + */ + +#ifndef CVC5__UTILS_H +#define CVC5__UTILS_H + +#include + +/** + * Print solutions for synthesis conjecture to the standard output stream. + * @param terms the terms for which the synthesis solutions were retrieved + * @param sols the synthesis solutions of the given terms + */ +void printSynthSolutions(const std::vector& terms, + const std::vector& sols); + +#endif // CVC5__UTILS_H diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp deleted file mode 100644 index 76c6da0f0..000000000 --- a/examples/api/datatypes.cpp +++ /dev/null @@ -1,178 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * An example of using inductive datatypes in CVC4. - */ - -#include - -#include - -using namespace cvc5::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.mkInteger(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 = slv.mkDatatypeConstructorDecl("cons"); - DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("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{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.mkInteger(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 = 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 ctors = {cons2, nil2}; - Sort consListSort2 = slv.declareDatatype("list2", ctors); - test(slv, consListSort2); - - return 0; -} diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp deleted file mode 100644 index d21c59d59..000000000 --- a/examples/api/extract.cpp +++ /dev/null @@ -1,56 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Makai Mann, Clark Barrett - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the solving capabilities of the CVC4 - * bit-vector solver. - * - */ - -#include - -#include - -using namespace std; -using namespace cvc5::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/helloworld.cpp b/examples/api/helloworld.cpp deleted file mode 100644 index 21eb8e8fc..000000000 --- a/examples/api/helloworld.cpp +++ /dev/null @@ -1,29 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A very simple CVC4 example. - */ - -#include - -#include - -using namespace cvc5::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/linear_arith.cpp b/examples/api/linear_arith.cpp deleted file mode 100644 index 02ddd956c..000000000 --- a/examples/api/linear_arith.cpp +++ /dev/null @@ -1,83 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Tim King, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the linear arithmetic solving capabilities and - * the push pop of CVC4. This also gives an example option. - */ - -#include - -#include - -using namespace std; -using namespace cvc5::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.mkInteger(3); - Term neg2 = slv.mkInteger(-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/sequences.cpp b/examples/api/sequences.cpp deleted file mode 100644 index 5ee66048f..000000000 --- a/examples/api/sequences.cpp +++ /dev/null @@ -1,67 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andres Noetzli, Aina Niemetz, Tianyi Liang - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of reasoning about sequences with CVC4 via C++ API. - */ - -#include - -#include - -using namespace cvc5::api; - -int main() -{ - Solver slv; - - // Set the logic - slv.setLogic("QF_SLIA"); - // 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"); - - // Sequence sort - Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); - - // Sequence variables - Term x = slv.mkConst(intSeq, "x"); - Term y = slv.mkConst(intSeq, "y"); - - // Empty sequence - Term empty = slv.mkEmptySequence(slv.getIntegerSort()); - // Sequence concatenation: x.y.empty - Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty); - // Sequence length: |x.y.empty| - Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); - // |x.y.empty| > 1 - Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); - // Sequence unit: seq(1) - Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); - // x = seq(1) - Term formula2 = slv.mkTerm(EQUAL, x, unit); - - // Make a query - Term q = slv.mkTerm(AND, formula1, formula2); - - // 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 << " y = " << slv.getValue(y) << std::endl; - } -} diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp deleted file mode 100644 index 5c9652707..000000000 --- a/examples/api/sets.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Kshitij Bansal, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of reasoning about sets with CVC4. - */ - -#include - -#include - -using namespace std; -using namespace cvc5::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.mkInteger(1); - Term two = slv.mkInteger(2); - Term three = slv.mkInteger(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/smtlib/helloworld.smt2 b/examples/api/smtlib/helloworld.smt2 new file mode 100644 index 000000000..b33689bb7 --- /dev/null +++ b/examples/api/smtlib/helloworld.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_UF) +(declare-const |Hello World!| Bool) +(assert (not |Hello World!|)) +(check-sat) diff --git a/examples/api/smtlib/linear_arith.smt2 b/examples/api/smtlib/linear_arith.smt2 new file mode 100644 index 000000000..ede655b0e --- /dev/null +++ b/examples/api/smtlib/linear_arith.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_LIRA) +(declare-const x Int) +(declare-const y Real) +(assert + (and + (>= x (* 3 y)) + (<= x y) + (< (- 2) x) + ) +) +(push 1) +(echo "Checking entailement by asserting the negation") +(echo "Unsat == ENTAILED") +(assert (not (<= (- y x) (/ 2 3)))) +(check-sat) +(pop 1) +(push 1) +(echo "Checking that the assertions are consistent") +(assert (= (- y x) (/ 2 3))) +(check-sat) +(pop 1) diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp deleted file mode 100644 index a952b31d1..000000000 --- a/examples/api/strings.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Tianyi Liang, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of reasoning about strings with CVC4 via C++ API. - */ - -#include - -#include - -using namespace cvc5::api; - -int main() -{ - Solver slv; - - // Set the logic - slv.setLogic("QF_SLIA"); - // 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.mkInteger(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/sygus-fun.cpp b/examples/api/sygus-fun.cpp deleted file mode 100644 index 0f96e72a7..000000000 --- a/examples/api/sygus-fun.cpp +++ /dev/null @@ -1,142 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the Sygus API. - * - * A simple demonstration of how to use the Sygus API to synthesize max and min - * functions. Here is the same problem written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-fun max ((x Int) (y Int)) Int - * ((Start Int) (StartBool Bool)) - * ((Start Int (0 1 x y - * (+ Start Start) - * (- Start Start) - * (ite StartBool Start Start))) - * (StartBool Bool ((and StartBool StartBool) - * (not StartBool) - * (<= Start Start))))) - * - * (synth-fun min ((x Int) (y Int)) Int) - * - * (declare-var x Int) - * (declare-var y Int) - * - * (constraint (>= (max x y) x)) - * (constraint (>= (max x y) y)) - * (constraint (or (= x (max x y)) - * (= y (max x y)))) - * (constraint (= (+ (max x y) (min x y)) - * (+ x y))) - * - * (check-synth) - * - * The printed output for this example should be equivalent to: - * ( - * (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) - * (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) - * ) - */ - -#include - -#include - -#include "utils.h" - -using namespace cvc5::api; - -int main() -{ - Solver slv; - - // required options - slv.setOption("lang", "sygus2"); - slv.setOption("incremental", "false"); - - // set the logic - slv.setLogic("LIA"); - - Sort integer = slv.getIntegerSort(); - Sort boolean = slv.getBooleanSort(); - - // declare input variables for the functions-to-synthesize - Term x = slv.mkVar(integer, "x"); - Term y = slv.mkVar(integer, "y"); - - // declare the grammar non-terminals - Term start = slv.mkVar(integer, "Start"); - Term start_bool = slv.mkVar(boolean, "StartBool"); - - // define the rules - Term zero = slv.mkInteger(0); - Term one = slv.mkInteger(1); - - Term plus = slv.mkTerm(PLUS, start, start); - Term minus = slv.mkTerm(MINUS, start, start); - Term ite = slv.mkTerm(ITE, start_bool, start, start); - - Term And = slv.mkTerm(AND, start_bool, start_bool); - Term Not = slv.mkTerm(NOT, start_bool); - Term leq = slv.mkTerm(LEQ, start, start); - - // create the grammar object - Grammar g = slv.mkSygusGrammar({x, y}, {start, start_bool}); - - // bind each non-terminal to its rules - g.addRules(start, {zero, one, x, y, plus, minus, ite}); - g.addRules(start_bool, {And, Not, leq}); - - // declare the functions-to-synthesize. Optionally, provide the grammar - // constraints - Term max = slv.synthFun("max", {x, y}, integer, g); - Term min = slv.synthFun("min", {x, y}, integer); - - // declare universal variables. - Term varX = slv.mkSygusVar(integer, "x"); - Term varY = slv.mkSygusVar(integer, "y"); - - Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY); - Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY); - - // add semantic constraints - // (constraint (>= (max x y) x)) - slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX)); - - // (constraint (>= (max x y) y)) - slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY)); - - // (constraint (or (= x (max x y)) - // (= y (max x y)))) - slv.addSygusConstraint(slv.mkTerm( - OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY))); - - // (constraint (= (+ (max x y) (min x y)) - // (+ x y))) - slv.addSygusConstraint(slv.mkTerm( - EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); - - // print solutions if available - if (slv.checkSynth().isUnsat()) - { - // Output should be equivalent to: - // ( - // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) - // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) - // ) - std::vector terms = {max, min}; - printSynthSolutions(terms, slv.getSynthSolutions(terms)); - } - - return 0; -} diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp deleted file mode 100644 index ce5a1bc8b..000000000 --- a/examples/api/sygus-grammar.cpp +++ /dev/null @@ -1,132 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the Sygus API. - * - * A simple demonstration of how to use Grammar to add syntax constraints to - * the Sygus solution for the identity function. Here is the same problem - * written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-fun id1 ((x Int)) Int - * ((Start Int)) ((Start Int ((- x) (+ x Start))))) - * - * (synth-fun id2 ((x Int)) Int - * ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) - * - * (synth-fun id3 ((x Int)) Int - * ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) - * - * (synth-fun id4 ((x Int)) Int - * ((Start Int)) ((Start Int ((- x) (+ x Start))))) - * - * (declare-var x Int) - * - * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) - * - * (check-synth) - * - * The printed output for this example should look like: - * ( - * (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) - * (define-fun id2 ((x Int)) Int x) - * (define-fun id3 ((x Int)) Int (+ x 0)) - * (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) - * ) - */ - -#include - -#include - -#include "utils.h" - -using namespace cvc5::api; - -int main() -{ - Solver slv; - - // required options - slv.setOption("lang", "sygus2"); - slv.setOption("incremental", "false"); - - // set the logic - slv.setLogic("LIA"); - - Sort integer = slv.getIntegerSort(); - Sort boolean = slv.getBooleanSort(); - - // declare input variable for the function-to-synthesize - Term x = slv.mkVar(integer, "x"); - - // declare the grammar non-terminal - Term start = slv.mkVar(integer, "Start"); - - // define the rules - Term zero = slv.mkInteger(0); - Term neg_x = slv.mkTerm(UMINUS, x); - Term plus = slv.mkTerm(PLUS, x, start); - - // create the grammar object - Grammar g1 = slv.mkSygusGrammar({x}, {start}); - - // bind each non-terminal to its rules - g1.addRules(start, {neg_x, plus}); - - // copy the first grammar with all of its non-termainals and their rules - Grammar g2 = g1; - Grammar g3 = g1; - - // add parameters as rules for the start symbol. Similar to "(Variable Int)" - g2.addAnyVariable(start); - - // declare the functions-to-synthesize - Term id1 = slv.synthFun("id1", {x}, integer, g1); - Term id2 = slv.synthFun("id2", {x}, integer, g2); - - g3.addRule(start, zero); - - Term id3 = slv.synthFun("id3", {x}, integer, g3); - - // g1 is reusable as long as it remains unmodified after first use - Term id4 = slv.synthFun("id4", {x}, integer, g1); - - // declare universal variables. - Term varX = slv.mkSygusVar(integer, "x"); - - Term id1_x = slv.mkTerm(APPLY_UF, id1, varX); - Term id2_x = slv.mkTerm(APPLY_UF, id2, varX); - Term id3_x = slv.mkTerm(APPLY_UF, id3, varX); - Term id4_x = slv.mkTerm(APPLY_UF, id4, varX); - - // add semantic constraints - // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) - slv.addSygusConstraint(slv.mkTerm(EQUAL, {id1_x, id2_x, id3_x, id4_x, varX})); - - // print solutions if available - if (slv.checkSynth().isUnsat()) - { - // Output should be equivalent to: - // ( - // (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) - // (define-fun id2 ((x Int)) Int x) - // (define-fun id3 ((x Int)) Int (+ x 0)) - // (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) - // ) - std::vector terms = {id1, id2, id3, id4}; - printSynthSolutions(terms, slv.getSynthSolutions(terms)); - } - - return 0; -} diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp deleted file mode 100644 index f658fa33a..000000000 --- a/examples/api/sygus-inv.cpp +++ /dev/null @@ -1,97 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A simple demonstration of the Sygus API. - * - * A simple demonstration of how to use the Sygus API to synthesize a simple - * invariant. Here is the same problem written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-inv inv-f ((x Int))) - * - * (define-fun pre-f ((x Int)) Bool - * (= x 0)) - * (define-fun trans-f ((x Int) (xp Int)) Bool - * (ite (< x 10) (= xp (+ x 1)) (= xp x))) - * (define-fun post-f ((x Int)) Bool - * (<= x 10)) - * - * (inv-constraint inv-f pre-f trans-f post-f) - * - * (check-synth) - * - * The printed output for this example should be equivalent to: - * ( - * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) - * ) - */ - -#include - -#include - -#include "utils.h" - -using namespace cvc5::api; - -int main() -{ - Solver slv; - - // required options - slv.setOption("lang", "sygus2"); - slv.setOption("incremental", "false"); - - // set the logic - slv.setLogic("LIA"); - - Sort integer = slv.getIntegerSort(); - Sort boolean = slv.getBooleanSort(); - - Term zero = slv.mkInteger(0); - Term one = slv.mkInteger(1); - Term ten = slv.mkInteger(10); - - // declare input variables for functions - Term x = slv.mkVar(integer, "x"); - Term xp = slv.mkVar(integer, "xp"); - - // (ite (< x 10) (= xp (+ x 1)) (= xp x)) - Term ite = slv.mkTerm(ITE, - slv.mkTerm(LT, x, ten), - slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), - slv.mkTerm(EQUAL, xp, x)); - - // define the pre-conditions, transition relations, and post-conditions - Term pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(EQUAL, x, zero)); - Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite); - Term post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, x, ten)); - - // declare the invariant-to-synthesize - Term inv_f = slv.synthInv("inv-f", {x}); - - slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); - - // print solutions if available - if (slv.checkSynth().isUnsat()) - { - // Output should be equivalent to: - // ( - // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) - // ) - std::vector terms = {inv_f}; - printSynthSolutions(terms, slv.getSynthSolutions(terms)); - } - - return 0; -} diff --git a/examples/api/utils.cpp b/examples/api/utils.cpp deleted file mode 100644 index 69676819a..000000000 --- a/examples/api/utils.cpp +++ /dev/null @@ -1,69 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementations of utility methods. - */ - -#include "utils.h" - -#include - -/** - * Get the string version of define-fun command. - * @param f the function to print - * @param params the function parameters - * @param body the function body - * @return a string version of define-fun - */ -std::string defineFunToString(const cvc5::api::Term& f, - const std::vector params, - const cvc5::api::Term body) -{ - - cvc5::api::Sort sort = f.getSort(); - if (sort.isFunction()) - { - sort = sort.getFunctionCodomainSort(); - } - std::stringstream ss; - ss << "(define-fun " << f << " ("; - for (size_t i = 0, n = params.size(); i < n; ++i) - { - if (i > 0) - { - ss << ' '; - } - ss << '(' << params[i] << ' ' << params[i].getSort() << ')'; - } - ss << ") " << sort << ' ' << body << ')'; - return ss.str(); -} - -void printSynthSolutions(const std::vector& terms, - const std::vector& sols) -{ - std::cout << '(' << std::endl; - - for (size_t i = 0, n = terms.size(); i < n; ++i) - { - std::vector params; - cvc5::api::Term body; - if (sols[i].getKind() == cvc5::api::LAMBDA) - { - params.insert(params.end(), sols[i][0].begin(), sols[i][0].end()); - body = sols[i][1]; - } - std::cout << " " << defineFunToString(terms[i], params, body) - << std::endl; - } - std::cout << ')' << std::endl; -} diff --git a/examples/api/utils.h b/examples/api/utils.h deleted file mode 100644 index 69cddee26..000000000 --- a/examples/api/utils.h +++ /dev/null @@ -1,29 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Utility methods. - */ - -#ifndef CVC5__UTILS_H -#define CVC5__UTILS_H - -#include - -/** - * Print solutions for synthesis conjecture to the standard output stream. - * @param terms the terms for which the synthesis solutions were retrieved - * @param sols the synthesis solutions of the given terms - */ -void printSynthSolutions(const std::vector& terms, - const std::vector& sols); - -#endif // CVC5__UTILS_H