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)
--- /dev/null
+Binary Documentation
+====================
+
+.. toctree::
+ :maxdepth: 2
+
+ options
--- /dev/null
+Commandline Options
+===================
+
+.. include-build-file:: options_generated.rst
+
# -- 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}']
+.. _cpp-api:
+
C++ API Documentation
=====================
--- /dev/null
+Theory of Bit-Vectors
+=====================
+
+
+.. api-examples::
+ ../../examples/api/cpp/bitvectors.cpp
+ ../../examples/api/java/BitVectors.java
+ ../../examples/api/python/bitvectors.py
--- /dev/null
+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
--- /dev/null
+Theory Combination
+==================
+
+
+.. api-examples::
+ ../../examples/api/cpp/combination.cpp
+ ../../examples/api/java/Combination.java
+ ../../examples/api/python/combination.py
-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
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
--- /dev/null
+Exception Handling
+======================================
+
+
+.. api-examples::
+ ../../examples/api/java/Exceptions.java
+ ../../examples/api/python/exceptions.py
--- /dev/null
+Theory of Bit-Vectors: :code:`extract`
+======================================
+
+
+.. api-examples::
+ ../../examples/api/cpp/extract.cpp
+ ../../examples/api/python/extract.py
--- /dev/null
+Theory of Floating-Points
+======================================
+
+
+.. api-examples::
+ ../../examples/api/java/FloatingPointArith.java
+ ../../examples/api/python/floating_point.py
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
-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
--- /dev/null
+Theory of Sequences
+===================
+
+
+.. api-examples::
+ ../../examples/api/cpp/sequences.cpp
+ ../../examples/api/python/sequences.py
--- /dev/null
+Theory of Sets
+=================
+
+
+.. api-examples::
+ ../../examples/api/cpp/sets.cpp
+ ../../examples/api/python/sets.py
--- /dev/null
+Theory of Strings
+=================
+
+
+.. api-examples::
+ ../../examples/api/cpp/strings.cpp
+ ../../examples/api/java/Strings.java
+ ../../examples/api/python/strings.py
--- /dev/null
+SyGuS: Functions
+===================
+
+
+.. api-examples::
+ ../../examples/api/cpp/sygus-fun.cpp
+ ../../examples/api/python/sygus-fun.py
--- /dev/null
+SyGuS: Grammars
+===================
+
+
+.. api-examples::
+ ../../examples/api/cpp/sygus-grammar.cpp
+ ../../examples/api/python/sygus-grammar.py
--- /dev/null
+SyGuS: Invariants
+===================
+
+
+.. api-examples::
+ ../../examples/api/cpp/sygus-inv.cpp
+ ../../examples/api/python/sygus-inv.py
'.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
--- /dev/null
+Index
+=====
cvc5 API Documentation
======================
-
-* :ref:`genindex`
-
-
----------------
-
.. toctree::
:maxdepth: 1
+ installation/installation
+ binary/binary
cpp/cpp
python/python
- references
examples/examples
- options
+ references
+ genindex
--- /dev/null
+Installation
+============
\ No newline at end of file
+++ /dev/null
-Commandline Options
-===================
-
-.. include-build-file:: options_generated.rst
-
+.. _python-api:
+
Python API Documentation
========================
# # 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)
+++ /dev/null
-###############################################################################
-# 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()
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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<Term> v{new_x_eq_new_x_, x_neq_x};
- cout << " Check entailment assuming: " << v << endl;
- cout << " Expect NOT_ENTAILED. " << endl;
- cout << " CVC4: " << slv.checkEntailed(v) << endl;
-
- // Assert that a is odd
- Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
- Term lsb_of_a = slv.mkTerm(extract_op, a);
- cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
- Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
- cout << "Assert " << a_odd << endl;
- cout << "Check satisfiability." << endl;
- slv.assertFormula(a_odd);
- cout << " Expect sat. " << endl;
- cout << " CVC4: " << slv.checkSat() << endl;
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <cmath>
-#include <iostream>
-
-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<Term> assertions;
- for (unsigned i = 1; i < k; ++i) {
- index = slv.mkBitVector(index_size, i);
- Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current);
- // current[i] = 2 * current[i-1]
- current_array = slv.mkTerm(STORE, current_array, index, new_current);
- // current[i-1] < current [i]
- Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current);
- assertions.push_back(current_slt_new_current);
-
- old_current = slv.mkTerm(SELECT, current_array, index);
- }
-
- Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions));
-
- cout << "Asserting " << query << " to CVC4 " << endl;
- slv.assertFormula(query);
- cout << "Expect sat. " << endl;
- cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl;
-
- // Getting the model
- cout << "The satisfying model is: " << endl;
- cout << " current_array = " << slv.getValue(current_array) << endl;
- cout << " current_array[0] = " << slv.getValue(current_array0) << endl;
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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<Term>{
- slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
- slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
- slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
- p_0.notTerm(), // not p(0)
- p_f_y // p(f(y))
- });
- slv.assertFormula(assertions);
-
- cout << "Given the following assertions:" << endl
- << assertions << endl << endl;
-
- cout << "Prove x /= y is entailed. " << endl
- << "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;
-}
--- /dev/null
+###############################################################################
+# 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()
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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<Term> v{new_x_eq_new_x_, x_neq_x};
+ cout << " Check entailment assuming: " << v << endl;
+ cout << " Expect NOT_ENTAILED. " << endl;
+ cout << " CVC4: " << slv.checkEntailed(v) << endl;
+
+ // Assert that a is odd
+ Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+ Term lsb_of_a = slv.mkTerm(extract_op, a);
+ cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
+ Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
+ cout << "Assert " << a_odd << endl;
+ cout << "Check satisfiability." << endl;
+ slv.assertFormula(a_odd);
+ cout << " Expect sat. " << endl;
+ cout << " CVC4: " << slv.checkSat() << endl;
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <cmath>
+#include <iostream>
+
+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<Term> assertions;
+ for (unsigned i = 1; i < k; ++i) {
+ index = slv.mkBitVector(index_size, i);
+ Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current);
+ // current[i] = 2 * current[i-1]
+ current_array = slv.mkTerm(STORE, current_array, index, new_current);
+ // current[i-1] < current [i]
+ Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current);
+ assertions.push_back(current_slt_new_current);
+
+ old_current = slv.mkTerm(SELECT, current_array, index);
+ }
+
+ Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions));
+
+ cout << "Asserting " << query << " to CVC4 " << endl;
+ slv.assertFormula(query);
+ cout << "Expect sat. " << endl;
+ cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl;
+
+ // Getting the model
+ cout << "The satisfying model is: " << endl;
+ cout << " current_array = " << slv.getValue(current_array) << endl;
+ cout << " current_array[0] = " << slv.getValue(current_array0) << endl;
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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<Term>{
+ slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
+ slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
+ slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
+ p_0.notTerm(), // not p(0)
+ p_f_y // p(f(y))
+ });
+ slv.assertFormula(assertions);
+
+ cout << "Given the following assertions:" << endl
+ << assertions << endl << endl;
+
+ cout << "Prove x /= y is entailed. " << endl
+ << "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;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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<Sort>{slv.getIntegerSort()});
+
+ const Datatype& paramConsList = paramConsListSort.getDatatype();
+
+ std::cout << "parameterized datatype sort is " << std::endl;
+ for (const DatatypeConstructor& ctor : paramConsList)
+ {
+ std::cout << "ctor: " << ctor << std::endl;
+ for (const DatatypeSelector& stor : ctor)
+ {
+ std::cout << " + arg: " << stor << std::endl;
+ }
+ }
+
+ Term a = slv.mkConst(paramConsIntListSort, "a");
+ std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
+
+ Term head_a = slv.mkTerm(
+ APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
+ std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
+ << std::endl
+ << "sort of cons is "
+ << paramConsList.getConstructorTerm("cons").getSort() << std::endl
+ << std::endl;
+ Term assertion = slv.mkTerm(GT, head_a, slv.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<DatatypeConstructorDecl> ctors = {cons2, nil2};
+ Sort consListSort2 = slv.declareDatatype("list2", ctors);
+ test(slv, consListSort2);
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <iostream>
+
+#include <cvc5/cvc5.h>
+
+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;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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;
+ }
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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;
+ }
+ }
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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;
+ }
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+#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<Term> terms = {max, min};
+ printSynthSolutions(terms, slv.getSynthSolutions(terms));
+ }
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+#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<Term> terms = {id1, id2, id3, id4};
+ printSynthSolutions(terms, slv.getSynthSolutions(terms));
+ }
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+#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<Term> terms = {inv_f};
+ printSynthSolutions(terms, slv.getSynthSolutions(terms));
+ }
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <iostream>
+
+/**
+ * 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<cvc5::api::Term> 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<cvc5::api::Term>& terms,
+ const std::vector<cvc5::api::Term>& sols)
+{
+ std::cout << '(' << std::endl;
+
+ for (size_t i = 0, n = terms.size(); i < n; ++i)
+ {
+ std::vector<cvc5::api::Term> 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;
+}
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+/**
+ * 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<cvc5::api::Term>& terms,
+ const std::vector<cvc5::api::Term>& sols);
+
+#endif // CVC5__UTILS_H
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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<Sort>{slv.getIntegerSort()});
-
- const Datatype& paramConsList = paramConsListSort.getDatatype();
-
- std::cout << "parameterized datatype sort is " << std::endl;
- for (const DatatypeConstructor& ctor : paramConsList)
- {
- std::cout << "ctor: " << ctor << std::endl;
- for (const DatatypeSelector& stor : ctor)
- {
- std::cout << " + arg: " << stor << std::endl;
- }
- }
-
- Term a = slv.mkConst(paramConsIntListSort, "a");
- std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
-
- Term head_a = slv.mkTerm(
- APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
- std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
- << std::endl
- << "sort of cons is "
- << paramConsList.getConstructorTerm("cons").getSort() << std::endl
- << std::endl;
- Term assertion = slv.mkTerm(GT, head_a, slv.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<DatatypeConstructorDecl> ctors = {cons2, nil2};
- Sort consListSort2 = slv.declareDatatype("list2", ctors);
- test(slv, consListSort2);
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <iostream>
-
-#include <cvc5/cvc5.h>
-
-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;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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;
- }
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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;
- }
- }
-}
--- /dev/null
+(set-logic QF_UF)
+(declare-const |Hello World!| Bool)
+(assert (not |Hello World!|))
+(check-sat)
--- /dev/null
+(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)
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-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;
- }
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-#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<Term> terms = {max, min};
- printSynthSolutions(terms, slv.getSynthSolutions(terms));
- }
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-#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<Term> terms = {id1, id2, id3, id4};
- printSynthSolutions(terms, slv.getSynthSolutions(terms));
- }
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <iostream>
-
-#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<Term> terms = {inv_f};
- printSynthSolutions(terms, slv.getSynthSolutions(terms));
- }
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <iostream>
-
-/**
- * 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<cvc5::api::Term> 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<cvc5::api::Term>& terms,
- const std::vector<cvc5::api::Term>& sols)
-{
- std::cout << '(' << std::endl;
-
- for (size_t i = 0, n = terms.size(); i < n; ++i)
- {
- std::vector<cvc5::api::Term> 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;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-/**
- * 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<cvc5::api::Term>& terms,
- const std::vector<cvc5::api::Term>& sols);
-
-#endif // CVC5__UTILS_H
projects / cvc5.git / commitdiff