This PR translates some of the API tests from here to Python. The other tests are translated in a private branch and will be added in a separate PR.
add_subdirectory(regress)
add_subdirectory(api EXCLUDE_FROM_ALL)
+add_subdirectory(binary EXCLUDE_FROM_ALL)
if(ENABLE_UNIT_TESTING)
add_subdirectory(unit EXCLUDE_FROM_ALL)
# The build system configuration.
##
-include_directories(.)
-include_directories(${PROJECT_SOURCE_DIR}/src)
-include_directories(${PROJECT_SOURCE_DIR}/src/include)
-include_directories(${CMAKE_BINARY_DIR}/src)
-
-#-----------------------------------------------------------------------------#
-# Add target 'apitests', builds and runs
-# > api tests
-
-add_custom_target(build-apitests)
-add_dependencies(build-tests build-apitests)
-
-add_custom_target(apitests
- COMMAND ctest --output-on-failure -L "api" -j${CTEST_NTHREADS} $$ARGS
- DEPENDS build-apitests)
-
-set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST)
-
-macro(cvc5_add_api_test name)
- set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/)
- add_executable(${name} ${name}.cpp)
- target_link_libraries(${name} PUBLIC main-test)
- target_compile_definitions(${name} PRIVATE ${CVC5_API_TEST_FLAGS})
- set_target_properties(${name}
- PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
- add_test(api/${name} ${test_bin_dir}/${name})
- set_tests_properties(api/${name} PROPERTIES LABELS "api")
- add_dependencies(build-apitests ${name})
-endmacro()
-
-cvc5_add_api_test(boilerplate)
-cvc5_add_api_test(ouroborous)
-cvc5_add_api_test(reset_assertions)
-cvc5_add_api_test(sep_log_api)
-cvc5_add_api_test(smt2_compliance)
-cvc5_add_api_test(two_solvers)
-cvc5_add_api_test(issue5074)
-cvc5_add_api_test(issue4889)
-cvc5_add_api_test(issue6111)
-cvc5_add_api_test(proj-issue306)
-cvc5_add_api_test(proj-issue334)
-
-# if we've built using libedit, then we want the interactive shell tests
-if (USE_EDITLINE)
-
- # Check for pexpect -- zero return code is success
- execute_process(
- COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect"
- RESULT_VARIABLE PEXPECT_RC
- ERROR_QUIET
- )
-
- # Add the test if we have pexpect
- if(PEXPECT_RC EQUAL 0)
- add_test(
- NAME interactive_shell
- COMMAND
- "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/api/interactive_shell.py"
- WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
- )
- endif()
+add_subdirectory(cpp)
+if (BUILD_BINDINGS_PYTHON)
+ add_subdirectory(python)
endif()
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Andres Noetzli, 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 start-up/tear-down test for cvc5.
- *
- * This simple test just makes sure that the public interface is
- * minimally functional. It is useful as a template to use for other
- * system tests.
- */
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-using namespace std;
-
-int main() {
- Solver slv;
- Result r = slv.checkEntailed(slv.mkBoolean(true));
- return r.isEntailed() ? 0 : 1;
-}
-
--- /dev/null
+###############################################################################
+# Top contributors (to current version):
+# Aina Niemetz, Andrew V. Jones, Gereon Kremer
+#
+# 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.
+##
+
+include_directories(.)
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
+
+#-----------------------------------------------------------------------------#
+# Add target 'apitests', builds and runs
+# > api tests
+
+add_custom_target(build-apitests)
+add_dependencies(build-tests build-apitests)
+
+add_custom_target(apitests
+ COMMAND ctest --output-on-failure -L "api" -j${CTEST_NTHREADS} $$ARGS
+ DEPENDS build-apitests)
+
+set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST)
+
+macro(cvc5_add_api_test name)
+ set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/cpp)
+ add_executable(${name} ${name}.cpp)
+ target_link_libraries(${name} PUBLIC main-test)
+ target_compile_definitions(${name} PRIVATE ${CVC5_API_TEST_FLAGS})
+ set_target_properties(${name}
+ PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
+ add_test(api/cpp/${name} ${test_bin_dir}/${name})
+ set_tests_properties(api/cpp/${name} PROPERTIES LABELS "api")
+ add_dependencies(build-apitests ${name})
+endmacro()
+
+cvc5_add_api_test(boilerplate)
+cvc5_add_api_test(ouroborous)
+cvc5_add_api_test(reset_assertions)
+cvc5_add_api_test(sep_log_api)
+cvc5_add_api_test(smt2_compliance)
+cvc5_add_api_test(two_solvers)
+cvc5_add_api_test(issue5074)
+cvc5_add_api_test(issue4889)
+cvc5_add_api_test(issue6111)
+cvc5_add_api_test(proj-issue306)
+cvc5_add_api_test(proj-issue334)
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Andres Noetzli, 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 start-up/tear-down test for cvc5.
+ *
+ * This simple test just makes sure that the public interface is
+ * minimally functional. It is useful as a template to use for other
+ * system tests.
+ */
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+int main() {
+ Solver slv;
+ Result r = slv.checkEntailed(slv.mkBoolean(true));
+ return r.isEntailed() ? 0 : 1;
+}
+
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Test for issue #4889
+ */
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main()
+{
+ Solver slv;
+ Sort sort_int = slv.getIntegerSort();
+ Sort sort_array = slv.mkArraySort(sort_int, sort_int);
+ Sort sort_fp128 = slv.mkFloatingPointSort(15, 113);
+ Sort sort_fp32 = slv.mkFloatingPointSort(8, 24);
+ Sort sort_bool = slv.getBooleanSort();
+ Term const0 = slv.mkConst(sort_fp32, "_c0");
+ Term const1 = slv.mkConst(sort_fp32, "_c2");
+ Term const2 = slv.mkConst(sort_bool, "_c4");
+ Term ite = slv.mkTerm(ITE, const2, const1, const0);
+ Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
+ Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
+ slv.checkSatAssuming(isnan);
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * Test for issue #5074
+ */
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main()
+{
+ Solver slv;
+ Term c1 = slv.mkConst(slv.getIntegerSort());
+ Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, c1);
+ Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6);
+ Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6});
+ Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14});
+ slv.checkEntailed(t16);
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mathias Preiner
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Test for issue #6111
+ *
+ */
+#include <iostream>
+#include <vector>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+int main()
+{
+ Solver solver;
+ solver.setLogic("QF_BV");
+ Sort bvsort12979 = solver.mkBitVectorSort(12979);
+ Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1");
+ Term zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10);
+
+ vector<Term> args1;
+ args1.push_back(zero);
+ args1.push_back(input2_1);
+ Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1);
+ solver.assertFormula(bvult_res);
+
+ Sort bvsort4 = solver.mkBitVectorSort(4);
+ Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42");
+ Sort bvsort8 = solver.mkBitVectorSort(8);
+ Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43");
+
+ vector<Term> args2;
+ args2.push_back(concat_result_42);
+ args2.push_back(
+ solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43}));
+ solver.assertFormula(solver.mkTerm(EQUAL, args2));
+
+ vector<Term> args3;
+ args3.push_back(concat_result_42);
+ args3.push_back(
+ solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43}));
+ solver.assertFormula(solver.mkTerm(EQUAL, args3));
+
+ cout << solver.checkSat() << endl;
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * "Ouroborous" test: does cvc5 read its own output?
+ *
+ * The "Ouroborous" test, named after the serpent that swallows its
+ * own tail, ensures that cvc5 can parse some input, output it again
+ * (in any of its languages) and then parse it again. The result of
+ * the first parse must be equal to the result of the second parse;
+ * both strings and expressions are compared for equality.
+ *
+ * To add a new test, simply add a call to runTestString() under
+ * runTest(), below. If you don't specify an input language,
+ * LANG_SMTLIB_V2 is used. If your example depends on variables,
+ * you'll need to declare them in the "declarations" global, just
+ * below, in SMT-LIBv2 form (but they're good for all languages).
+ */
+
+#include <cassert>
+#include <iostream>
+#include <string>
+
+#include "api/cpp/cvc5.h"
+#include "options/set_language.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "smt/command.h"
+
+using namespace cvc5;
+using namespace cvc5::parser;
+using namespace cvc5::language;
+
+int runTest();
+
+int main()
+{
+ try
+ {
+ return runTest();
+ }
+ catch (api::CVC5ApiException& e)
+ {
+ std::cerr << e.getMessage() << std::endl;
+ }
+ catch (parser::ParserException& e)
+ {
+ std::cerr << e.getMessage() << std::endl;
+ }
+ catch (...)
+ {
+ std::cerr << "non-cvc5 exception thrown" << std::endl;
+ }
+ return 1;
+}
+
+std::string parse(std::string instr,
+ std::string input_language,
+ std::string output_language)
+{
+ assert(input_language == "smt2");
+ assert(output_language == "smt2");
+
+ std::string declarations;
+
+ declarations =
+ "\
+ (declare-sort U 0)\n\
+ (declare-fun f (U) U)\n\
+ (declare-fun x () U)\n\
+ (declare-fun y () U)\n\
+ (assert (= (f x) x))\n\
+ (declare-fun a () (Array U (Array U U)))\n\
+ ";
+
+ api::Solver solver;
+ std::string ilang = "LANG_SMTLIB_V2_6";
+
+ solver.setOption("input-language", input_language);
+ solver.setOption("output-language", output_language);
+ SymbolManager symman(&solver);
+ std::unique_ptr<Parser> parser(
+ ParserBuilder(&solver, &symman, false)
+ .withInputLanguage(solver.getOption("input-language"))
+ .build());
+ parser->setInput(
+ Input::newStringInput(ilang, declarations, "internal-buffer"));
+ // we don't need to execute the commands, but we DO need to parse them to
+ // get the declarations
+ while (Command* c = parser->nextCommand())
+ {
+ delete c;
+ }
+ assert(parser->done()); // parser should be done
+ parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer"));
+ api::Term e = parser->nextExpression();
+ std::string s = e.toString();
+ assert(parser->nextExpression().isNull()); // next expr should be null
+ return s;
+}
+
+std::string translate(std::string instr,
+ std::string input_language,
+ std::string output_language)
+{
+ assert(input_language == "smt2");
+ assert(output_language == "smt2");
+
+ std::cout << "==============================================" << std::endl
+ << "translating from " << Language::LANG_SMTLIB_V2_6 << " to "
+ << Language::LANG_SMTLIB_V2_6 << " this string:" << std::endl
+ << instr << std::endl;
+ std::string outstr = parse(instr, input_language, output_language);
+ std::cout << "got this:" << std::endl
+ << outstr << std::endl
+ << "reparsing as " << Language::LANG_SMTLIB_V2_6 << std::endl;
+ std::string poutstr = parse(outstr, output_language, output_language);
+ assert(outstr == poutstr);
+ std::cout << "got same expressions " << outstr << " and " << poutstr
+ << std::endl
+ << "==============================================" << std::endl;
+ return outstr;
+}
+
+void runTestString(std::string instr, std::string instr_language)
+{
+ std::cout << std::endl
+ << "starting with: " << instr << std::endl
+ << " in language " << Language::LANG_SMTLIB_V2_6 << std::endl;
+ std::string smt2str = translate(instr, instr_language, "smt2");
+ std::cout << "in SMT2 : " << smt2str << std::endl;
+ std::string outstr = translate(smt2str, "smt2", "smt2");
+ std::cout << "to SMT2 : " << outstr << std::endl << std::endl;
+
+ assert(outstr == smt2str); // differences in output
+}
+
+int32_t runTest()
+{
+ runTestString("(= (f (f y)) x)", "smt2");
+ runTestString("(= ((_ extract 2 1) (bvnot (bvadd #b000 #b011))) #b10)",
+ "smt2");
+ runTestString("((_ extract 2 0) (bvnot (bvadd (bvmul #b001 #b011) #b011)))",
+ "smt2");
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * 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.
+ * ****************************************************************************
+ *
+ * Test for project issue #306
+ *
+ */
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+ Solver slv;
+ slv.setOption("check-proofs", "true");
+ slv.setOption("proof-check", "eager");
+ Sort s1 = slv.getBooleanSort();
+ Sort s3 = slv.getStringSort();
+ Term t1 = slv.mkConst(s3, "_x0");
+ Term t3 = slv.mkConst(s1, "_x2");
+ Term t11 = slv.mkString("");
+ Term t14 = slv.mkConst(s3, "_x11");
+ Term t42 = slv.mkTerm(Kind::ITE, t3, t14, t1);
+ Term t58 = slv.mkTerm(Kind::STRING_LEQ, t14, t11);
+ Term t95 = slv.mkTerm(Kind::EQUAL, t14, t42);
+ slv.assertFormula(t95);
+ slv.checkSatAssuming({t58});
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * 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.
+ * ****************************************************************************
+ *
+ * Test for project issue #334
+ *
+ */
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+ Solver slv;
+ slv.setOption("produce-unsat-cores", "true");
+ Sort s1 = slv.mkBitVectorSort(1);
+ Sort s2 = slv.mkFloatingPointSort(8, 24);
+ Term val = slv.mkBitVector(32, "10000000110010111010111011000101", 2);
+ Term t1 = slv.mkFloatingPoint(8, 24, val);
+ Term t2 = slv.mkConst(s1);
+ Term t4 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, t2);
+ Term t5 = slv.mkTerm(Kind::STRING_FROM_CODE, t4);
+ Term t6 = slv.simplify(t5);
+ Term t7 = slv.mkTerm(Kind::STRING_LEQ, t5, t6);
+ slv.assertFormula(t7);
+ slv.simplify(t1);
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andres Noetzli, 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 test for SolverEngine::resetAssertions()
+ *
+ * This program indirectly also tests some corner cases w.r.t.
+ * context-dependent datastructures: resetAssertions() pops the contexts to
+ * zero but some context-dependent datastructures are created at leevel 1,
+ * which the datastructure needs to handle properly problematic.
+ */
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main()
+{
+ Solver slv;
+ slv.setOption("incremental", "true");
+
+ Sort real = slv.getRealSort();
+ Term x = slv.mkConst(real, "x");
+ Term four = slv.mkInteger(4);
+ Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
+ slv.assertFormula(xEqFour);
+ std::cout << slv.checkSat() << std::endl;
+
+ slv.resetAssertions();
+
+ Sort elementType = slv.getIntegerSort();
+ Sort indexType = slv.getIntegerSort();
+ Sort arrayType = slv.mkArraySort(indexType, elementType);
+ Term array = slv.mkConst(arrayType, "array");
+ Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
+ Term ten = slv.mkInteger(10);
+ Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
+ slv.assertFormula(arrayAtFour_eq_ten);
+ std::cout << slv.checkSat() << std::endl;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew V. Jones, Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * Two tests to validate the use of the separation logic API.
+ *
+ * First test validates that we cannot use the API if not using separation
+ * logic.
+ *
+ * Second test validates that the expressions returned from the API are
+ * correct and can be interrogated.
+ *
+ ****************************************************************************/
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+/**
+ * Test function to validate that we *cannot* obtain the heap/nil expressions
+ * when *not* using the separation logic theory
+ */
+int validate_exception(void)
+{
+ Solver slv;
+
+ /*
+ * Setup some options for cvc5 -- we explictly want to use a simplistic
+ * theory (e.g., QF_IDL)
+ */
+ slv.setLogic("QF_IDL");
+ slv.setOption("produce-models", "true");
+ slv.setOption("incremental", "false");
+
+ /* Our integer type */
+ Sort integer = slv.getIntegerSort();
+
+ /** we intentionally do not set the separation logic heap */
+
+ /* Our SMT constants */
+ Term x = slv.mkConst(integer, "x");
+ Term y = slv.mkConst(integer, "y");
+
+ /* y > x */
+ Term y_gt_x(slv.mkTerm(Kind::GT, y, x));
+
+ /* assert it */
+ slv.assertFormula(y_gt_x);
+
+ /* check */
+ Result r(slv.checkSat());
+
+ /* If this is UNSAT, we have an issue; so bail-out */
+ if (!r.isSat())
+ {
+ return -1;
+ }
+
+ /*
+ * We now try to obtain our separation logic expressions from the solver --
+ * we want to validate that we get our expected exceptions.
+ */
+ bool caught_on_heap(false);
+ bool caught_on_nil(false);
+
+ /* The exception message we expect to obtain */
+ std::string expected(
+ "Cannot obtain separation logic expressions if not using the separation "
+ "logic theory.");
+
+ /* test the heap expression */
+ try
+ {
+ Term heap_expr = slv.getValueSepHeap();
+ }
+ catch (const CVC5ApiException& e)
+ {
+ caught_on_heap = true;
+
+ /* Check we get the correct exception string */
+ if (e.what() != expected)
+ {
+ return -1;
+ }
+ }
+
+ /* test the nil expression */
+ try
+ {
+ Term nil_expr = slv.getValueSepNil();
+ }
+ catch (const CVC5ApiException& e)
+ {
+ caught_on_nil = true;
+
+ /* Check we get the correct exception string */
+ if (e.what() != expected)
+ {
+ return -1;
+ }
+ }
+
+ if (!caught_on_heap || !caught_on_nil)
+ {
+ return -1;
+ }
+
+ /* All tests pass! */
+ return 0;
+}
+
+/**
+ * Test function to demonstrate the use of, and validate the capability, of
+ * obtaining the heap/nil expressions when using separation logic.
+ */
+int validate_getters(void)
+{
+ Solver slv;
+
+ /* Setup some options for cvc5 */
+ slv.setLogic("QF_ALL");
+ slv.setOption("produce-models", "true");
+ slv.setOption("incremental", "false");
+
+ /* Our integer type */
+ Sort integer = slv.getIntegerSort();
+
+ /** Declare the separation logic heap types */
+ slv.declareSepHeap(integer, integer);
+
+ /* A "random" constant */
+ Term random_constant = slv.mkInteger(0xDEADBEEF);
+
+ /* Another random constant */
+ Term expr_nil_val = slv.mkInteger(0xFBADBEEF);
+
+ /* Our nil term */
+ Term nil = slv.mkSepNil(integer);
+
+ /* Our SMT constants */
+ Term x = slv.mkConst(integer, "x");
+ Term y = slv.mkConst(integer, "y");
+ Term p1 = slv.mkConst(integer, "p1");
+ Term p2 = slv.mkConst(integer, "p2");
+
+ /* Constraints on x and y */
+ Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant);
+ Term y_gt_x = slv.mkTerm(Kind::GT, y, x);
+
+ /* Points-to expressions */
+ Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x);
+ Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y);
+
+ /* Heap -- the points-to have to be "starred"! */
+ Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y);
+
+ /* Constain "nil" to be something random */
+ Term fix_nil = slv.mkTerm(Kind::EQUAL, nil, expr_nil_val);
+
+ /* Add it all to the solver! */
+ slv.assertFormula(x_equal_const);
+ slv.assertFormula(y_gt_x);
+ slv.assertFormula(heap);
+ slv.assertFormula(fix_nil);
+
+ /*
+ * Incremental is disabled due to using separation logic, so don't query
+ * twice!
+ */
+ Result r(slv.checkSat());
+
+ /* If this is UNSAT, we have an issue; so bail-out */
+ if (!r.isSat())
+ {
+ return -1;
+ }
+
+ /* Obtain our separation logic terms from the solver */
+ Term heap_expr = slv.getValueSepHeap();
+ Term nil_expr = slv.getValueSepNil();
+
+ /* If the heap is not a separating conjunction, bail-out */
+ if (heap_expr.getKind() != Kind::SEP_STAR)
+ {
+ return -1;
+ }
+
+ /* If nil is not a direct equality, bail-out */
+ if (nil_expr.getKind() != Kind::EQUAL)
+ {
+ return -1;
+ }
+
+ /* Obtain the values for our "pointers" */
+ Term val_for_p1 = slv.getValue(p1);
+ Term val_for_p2 = slv.getValue(p2);
+
+ /* We need to make sure we find both pointers in the heap */
+ bool checked_p1(false);
+ bool checked_p2(false);
+
+ /* Walk all the children */
+ for (const Term& child : heap_expr)
+ {
+ /* If we don't have a PTO operator, bail-out */
+ if (child.getKind() != Kind::SEP_PTO)
+ {
+ return -1;
+ }
+
+ /* Find both sides of the PTO operator */
+ Term addr = slv.getValue(child[0]);
+ Term value = slv.getValue(child[1]);
+
+ /* If the current address is the value for p1 */
+ if (addr == val_for_p1)
+ {
+ checked_p1 = true;
+
+ /* If it doesn't match the random constant, we have a problem */
+ if (value != random_constant)
+ {
+ return -1;
+ }
+ continue;
+ }
+
+ /* If the current address is the value for p2 */
+ if (addr == val_for_p2)
+ {
+ checked_p2 = true;
+
+ /*
+ * Our earlier constraint was that what p2 points to must be *greater*
+ * than the random constant -- if we get a value that is LTE, then
+ * something has gone wrong!
+ */
+ if (std::stoll(value.toString())
+ <= std::stoll(random_constant.toString()))
+ {
+ return -1;
+ }
+ continue;
+ }
+
+ /*
+ * We should only have two addresses in heap, so if we haven't hit the
+ * "continue" for p1 or p2, then bail-out
+ */
+ return -1;
+ }
+
+ /*
+ * If we complete the loop and we haven't validated both p1 and p2, then we
+ * have a problem
+ */
+ if (!checked_p1 || !checked_p2)
+ {
+ return -1;
+ }
+
+ /* We now get our value for what nil is */
+ Term value_for_nil = slv.getValue(nil_expr[1]);
+
+ /*
+ * The value for nil from the solver should be the value we originally tied
+ * nil to
+ */
+ if (value_for_nil != expr_nil_val)
+ {
+ return -1;
+ }
+
+ /* All tests pass! */
+ return 0;
+}
+
+int main(void)
+{
+ /* check that we get an exception when we should */
+ int check_exception(validate_exception());
+
+ if (check_exception)
+ {
+ return check_exception;
+ }
+
+ /* check the getters */
+ int check_getters(validate_getters());
+
+ if (check_getters)
+ {
+ return check_getters;
+ }
+
+ return 0;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Morgan Deters, 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 test of SMT-LIBv2 commands, checks for compliant output.
+ */
+
+#include <cassert>
+#include <iostream>
+#include <sstream>
+
+#include "api/cpp/cvc5.h"
+#include "options/set_language.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "smt/command.h"
+#include "smt/solver_engine.h"
+
+using namespace cvc5;
+using namespace cvc5::parser;
+using namespace std;
+
+void testGetInfo(api::Solver* solver, const char* s);
+
+int main()
+{
+ cout << language::SetLanguage(Language::LANG_SMTLIB_V2_6);
+
+ std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
+ solver->setOption("input-language", "smtlib2");
+ solver->setOption("output-language", "smtlib2");
+ testGetInfo(solver.get(), ":error-behavior");
+ testGetInfo(solver.get(), ":name");
+ testGetInfo(solver.get(), ":authors");
+ testGetInfo(solver.get(), ":version");
+ testGetInfo(solver.get(), ":status");
+ testGetInfo(solver.get(), ":reason-unknown");
+ testGetInfo(solver.get(), ":arbitrary-undefined-keyword");
+ testGetInfo(solver.get(), ":56"); // legal
+ testGetInfo(solver.get(), ":<="); // legal
+ testGetInfo(solver.get(), ":->"); // legal
+ testGetInfo(solver.get(), ":all-statistics");
+
+ return 0;
+}
+
+void testGetInfo(api::Solver* solver, const char* s)
+{
+ std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
+
+ std::unique_ptr<Parser> p(ParserBuilder(solver, symman.get(), true).build());
+ p->setInput(Input::newStringInput(
+ "LANG_SMTLIB_V2_6", string("(get-info ") + s + ")", "<internal>"));
+ assert(p != NULL);
+ Command* c = p->nextCommand();
+ assert(c != NULL);
+ cout << c << endl;
+ stringstream ss;
+ c->invoke(solver, symman.get(), ss);
+ assert(p->nextCommand() == NULL);
+ delete c;
+ cout << ss.str() << endl << endl;
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andres Noetzli, Morgan Deters, 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 test of multiple SmtEngines.
+ */
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+int main() {
+ Solver s1;
+ Solver s2;
+ Result r = s1.checkEntailed(s1.mkBoolean(true));
+ Result r2 = s2.checkEntailed(s2.mkBoolean(true));
+ return r.isEntailed() && r2.isEntailed() ? 0 : 1;
+}
+
+++ /dev/null
-#!/usr/bin/env python3
-###############################################################################
-# Top contributors (to current version):
-# Andrew V. Jones
-#
-# 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 test file to interact with cvc5 with line editing
-##
-
-import sys
-import pexpect
-
-def check_iteractive_shell():
- """
- Interacts with cvc5's interactive shell and checks that things such a tab
- completion and "pressing up" works.
- """
-
- # Open cvc5
- child = pexpect.spawnu("bin/cvc5", timeout=1)
-
- # We expect to see the cvc5 prompt
- child.expect("cvc5>")
-
- # If we send a line with just 'BOOLE' ...
- child.sendline("(set-log")
-
- # ... then we get an error
- child.expect("Parse Error: <shell>:1.7: expected SMT-LIBv2 command, got `set-log\'")
-
- # Start sending 'BOOL' (without an E)
- child.send("(declare-data")
-
- # Send tab twice
- child.sendcontrol("i")
- child.sendcontrol("i")
-
- # We expect to see the completion
- child.expect("declare-datatype.*declare-datatypes")
-
- # NOTE: the double tab has completed our '(declare-data' to '(declare-datatype'!
-
- # Now send enter (which submits '(declare-datatype')
- child.send(")")
- child.sendcontrol("m")
-
- # So we expect to see an error for 'BOOLE'
- child.expect("Parse Error: <shell>:1.17: Unexpected token: '\)'.")
-
- # Send enter
- child.sendcontrol("m")
-
- # We expect to see the cvc5 prompt
- child.expect("cvc5>")
-
- # Now send an up key
- child.send("\033[A")
-
- # Send enter
- child.sendcontrol("m")
-
- # We expect to see the previous error again
- child.expect("Parse Error: <shell>:1.17: Unexpected token: '\)'.")
-
- return 0
-
-
-def main():
- """
- Runs our interactive shell test
-
- Caveats:
-
- * If we don't have the "pexpect" model, the test doesn't get run, but
- passes
-
- * We expect pexpect to raise and exit with a non-zero exit code if any
- of the steps fail
- """
-
- # If any of the "steps" fail, the pexpect will raise a Python will exit
- # with a non-zero error code
- sys.exit(check_iteractive_shell())
-
-if __name__ == "__main__":
- main()
-
-# EOF
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, 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.
- * ****************************************************************************
- *
- * Test for issue #4889
- */
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-
-int main()
-{
- Solver slv;
- Sort sort_int = slv.getIntegerSort();
- Sort sort_array = slv.mkArraySort(sort_int, sort_int);
- Sort sort_fp128 = slv.mkFloatingPointSort(15, 113);
- Sort sort_fp32 = slv.mkFloatingPointSort(8, 24);
- Sort sort_bool = slv.getBooleanSort();
- Term const0 = slv.mkConst(sort_fp32, "_c0");
- Term const1 = slv.mkConst(sort_fp32, "_c2");
- Term const2 = slv.mkConst(sort_bool, "_c4");
- Term ite = slv.mkTerm(ITE, const2, const1, const0);
- Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
- Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
- slv.checkSatAssuming(isnan);
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andres Noetzli, 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.
- * ****************************************************************************
- *
- * Test for issue #5074
- */
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-
-int main()
-{
- Solver slv;
- Term c1 = slv.mkConst(slv.getIntegerSort());
- Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, c1);
- Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6);
- Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6});
- Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14});
- slv.checkEntailed(t16);
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mathias Preiner
- *
- * 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.
- * ****************************************************************************
- *
- * Test for issue #6111
- *
- */
-#include <iostream>
-#include <vector>
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-using namespace std;
-
-int main()
-{
- Solver solver;
- solver.setLogic("QF_BV");
- Sort bvsort12979 = solver.mkBitVectorSort(12979);
- Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1");
- Term zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10);
-
- vector<Term> args1;
- args1.push_back(zero);
- args1.push_back(input2_1);
- Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1);
- solver.assertFormula(bvult_res);
-
- Sort bvsort4 = solver.mkBitVectorSort(4);
- Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42");
- Sort bvsort8 = solver.mkBitVectorSort(8);
- Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43");
-
- vector<Term> args2;
- args2.push_back(concat_result_42);
- args2.push_back(
- solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43}));
- solver.assertFormula(solver.mkTerm(EQUAL, args2));
-
- vector<Term> args3;
- args3.push_back(concat_result_42);
- args3.push_back(
- solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43}));
- solver.assertFormula(solver.mkTerm(EQUAL, args3));
-
- cout << solver.checkSat() << endl;
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Aina Niemetz, Morgan Deters
- *
- * 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.
- * ****************************************************************************
- *
- * "Ouroborous" test: does cvc5 read its own output?
- *
- * The "Ouroborous" test, named after the serpent that swallows its
- * own tail, ensures that cvc5 can parse some input, output it again
- * (in any of its languages) and then parse it again. The result of
- * the first parse must be equal to the result of the second parse;
- * both strings and expressions are compared for equality.
- *
- * To add a new test, simply add a call to runTestString() under
- * runTest(), below. If you don't specify an input language,
- * LANG_SMTLIB_V2 is used. If your example depends on variables,
- * you'll need to declare them in the "declarations" global, just
- * below, in SMT-LIBv2 form (but they're good for all languages).
- */
-
-#include <cassert>
-#include <iostream>
-#include <string>
-
-#include "api/cpp/cvc5.h"
-#include "options/set_language.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-
-using namespace cvc5;
-using namespace cvc5::parser;
-using namespace cvc5::language;
-
-int runTest();
-
-int main()
-{
- try
- {
- return runTest();
- }
- catch (api::CVC5ApiException& e)
- {
- std::cerr << e.getMessage() << std::endl;
- }
- catch (parser::ParserException& e)
- {
- std::cerr << e.getMessage() << std::endl;
- }
- catch (...)
- {
- std::cerr << "non-cvc5 exception thrown" << std::endl;
- }
- return 1;
-}
-
-std::string parse(std::string instr,
- std::string input_language,
- std::string output_language)
-{
- assert(input_language == "smt2");
- assert(output_language == "smt2");
-
- std::string declarations;
-
- declarations =
- "\
- (declare-sort U 0)\n\
- (declare-fun f (U) U)\n\
- (declare-fun x () U)\n\
- (declare-fun y () U)\n\
- (assert (= (f x) x))\n\
- (declare-fun a () (Array U (Array U U)))\n\
- ";
-
- api::Solver solver;
- std::string ilang = "LANG_SMTLIB_V2_6";
-
- solver.setOption("input-language", input_language);
- solver.setOption("output-language", output_language);
- SymbolManager symman(&solver);
- std::unique_ptr<Parser> parser(
- ParserBuilder(&solver, &symman, false)
- .withInputLanguage(solver.getOption("input-language"))
- .build());
- parser->setInput(
- Input::newStringInput(ilang, declarations, "internal-buffer"));
- // we don't need to execute the commands, but we DO need to parse them to
- // get the declarations
- while (Command* c = parser->nextCommand())
- {
- delete c;
- }
- assert(parser->done()); // parser should be done
- parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer"));
- api::Term e = parser->nextExpression();
- std::string s = e.toString();
- assert(parser->nextExpression().isNull()); // next expr should be null
- return s;
-}
-
-std::string translate(std::string instr,
- std::string input_language,
- std::string output_language)
-{
- assert(input_language == "smt2");
- assert(output_language == "smt2");
-
- std::cout << "==============================================" << std::endl
- << "translating from " << Language::LANG_SMTLIB_V2_6 << " to "
- << Language::LANG_SMTLIB_V2_6 << " this string:" << std::endl
- << instr << std::endl;
- std::string outstr = parse(instr, input_language, output_language);
- std::cout << "got this:" << std::endl
- << outstr << std::endl
- << "reparsing as " << Language::LANG_SMTLIB_V2_6 << std::endl;
- std::string poutstr = parse(outstr, output_language, output_language);
- assert(outstr == poutstr);
- std::cout << "got same expressions " << outstr << " and " << poutstr
- << std::endl
- << "==============================================" << std::endl;
- return outstr;
-}
-
-void runTestString(std::string instr, std::string instr_language)
-{
- std::cout << std::endl
- << "starting with: " << instr << std::endl
- << " in language " << Language::LANG_SMTLIB_V2_6 << std::endl;
- std::string smt2str = translate(instr, instr_language, "smt2");
- std::cout << "in SMT2 : " << smt2str << std::endl;
- std::string outstr = translate(smt2str, "smt2", "smt2");
- std::cout << "to SMT2 : " << outstr << std::endl << std::endl;
-
- assert(outstr == smt2str); // differences in output
-}
-
-int32_t runTest()
-{
- runTestString("(= (f (f y)) x)", "smt2");
- runTestString("(= ((_ extract 2 1) (bvnot (bvadd #b000 #b011))) #b10)",
- "smt2");
- runTestString("((_ extract 2 0) (bvnot (bvadd (bvmul #b001 #b011) #b011)))",
- "smt2");
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * 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.
- * ****************************************************************************
- *
- * Test for project issue #306
- *
- */
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-
-int main(void)
-{
- Solver slv;
- slv.setOption("check-proofs", "true");
- slv.setOption("proof-check", "eager");
- Sort s1 = slv.getBooleanSort();
- Sort s3 = slv.getStringSort();
- Term t1 = slv.mkConst(s3, "_x0");
- Term t3 = slv.mkConst(s1, "_x2");
- Term t11 = slv.mkString("");
- Term t14 = slv.mkConst(s3, "_x11");
- Term t42 = slv.mkTerm(Kind::ITE, t3, t14, t1);
- Term t58 = slv.mkTerm(Kind::STRING_LEQ, t14, t11);
- Term t95 = slv.mkTerm(Kind::EQUAL, t14, t42);
- slv.assertFormula(t95);
- slv.checkSatAssuming({t58});
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * 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.
- * ****************************************************************************
- *
- * Test for project issue #334
- *
- */
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-
-int main(void)
-{
- Solver slv;
- slv.setOption("produce-unsat-cores", "true");
- Sort s1 = slv.mkBitVectorSort(1);
- Sort s2 = slv.mkFloatingPointSort(8, 24);
- Term val = slv.mkBitVector(32, "10000000110010111010111011000101", 2);
- Term t1 = slv.mkFloatingPoint(8, 24, val);
- Term t2 = slv.mkConst(s1);
- Term t4 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, t2);
- Term t5 = slv.mkTerm(Kind::STRING_FROM_CODE, t4);
- Term t6 = slv.simplify(t5);
- Term t7 = slv.mkTerm(Kind::STRING_LEQ, t5, t6);
- slv.assertFormula(t7);
- slv.simplify(t1);
-}
--- /dev/null
+###############################################################################
+# Top contributors (to current version):
+# Yoni Zohar, Aina Niemetz, Mathias Preiner
+#
+# 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.
+##
+
+# Add Python bindings API tests.
+macro(cvc5_add_python_api_test name filename)
+# We create test target 'api/python/myapitest' and run it with
+# 'ctest -R "api/python/myapitest"'.
+ set(test_name api/python/${name})
+ add_test (NAME ${test_name}
+ COMMAND ${PYTHON_EXECUTABLE}
+ ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+ # directory for importing the python bindings
+ WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
+ set_tests_properties(${test_name}
+ PROPERTIES LABELS "api"
+ ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
+endmacro()
+
+# add specific test files
+cvc5_add_python_api_test(pyapi_boilerplate boilerplate.py)
+cvc5_add_python_api_test(pyapi_issue4889 issue4889.py)
+cvc5_add_python_api_test(pyapi_issue5074 issue5074.py)
+cvc5_add_python_api_test(pyapi_issue6111 issue6111.py)
--- /dev/null
+##############################################################################
+# Top contributors (to current version):
+# Yoni Zohar
+#
+# 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 start-up/tear-down test for cvc5.
+#
+# This simple test just makes sure that the public interface is
+# minimally functional. It is useful as a template to use for other
+# system tests.
+##
+
+import pycvc5
+
+slv = pycvc5.Solver()
+r = slv.checkEntailed(slv.mkBoolean(True))
+r.isEntailed()
--- /dev/null
+##############################################################################
+# Top contributors (to current version):
+# Yoni Zohar
+#
+# 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.
+# ############################################################################
+#
+# Test for issue #4889
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+slv = pycvc5.Solver()
+sort_int = slv.getIntegerSort()
+sort_array = slv.mkArraySort(sort_int, sort_int)
+sort_fp128 = slv.mkFloatingPointSort(15, 113)
+sort_fp32 = slv.mkFloatingPointSort(8, 24)
+sort_bool = slv.getBooleanSort()
+const0 = slv.mkConst(sort_fp32, "_c0")
+const1 = slv.mkConst(sort_fp32, "_c2")
+const2 = slv.mkConst(sort_bool, "_c4")
+ite = slv.mkTerm(kinds.Ite, const2, const1, const0)
+rem = slv.mkTerm(kinds.FPRem, ite, const1)
+isnan = slv.mkTerm(kinds.FPIsNan, rem)
+slv.checkSatAssuming(isnan)
--- /dev/null
+##############################################################################
+# Top contributors (to current version):
+# Yoni Zohar
+#
+# 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.
+# ############################################################################
+#
+# Test for issue #5074
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+slv = pycvc5.Solver()
+c1 = slv.mkConst(slv.getIntegerSort())
+t6 = slv.mkTerm(kinds.StringFromCode, c1)
+t12 = slv.mkTerm(kinds.StringToRegexp, t6)
+t14 = slv.mkTerm(kinds.StringReplaceRe, [t6, t12, t6])
+t16 = slv.mkTerm(kinds.StringContains, [t14, t14])
+slv.checkEntailed(t16)
--- /dev/null
+##############################################################################
+# Top contributors (to current version):
+# Yoni Zohar
+#
+# 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.
+# ############################################################################
+#
+# Test for issue #6111
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+solver = pycvc5.Solver()
+solver.setLogic("QF_BV")
+bvsort12979 = solver.mkBitVectorSort(12979)
+input2_1 = solver.mkConst(bvsort12979, "intpu2_1")
+zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10)
+
+args1 = []
+args1.append(zero)
+args1.append(input2_1)
+bvult_res = solver.mkTerm(kinds.BVUlt, args1)
+solver.assertFormula(bvult_res)
+
+bvsort4 = solver.mkBitVectorSort(4)
+concat_result_42 = solver.mkConst(bvsort4, "concat_result_42")
+bvsort8 = solver.mkBitVectorSort(8)
+concat_result_43 = solver.mkConst(bvsort8, "concat_result_43")
+
+args2 = []
+args2.append(concat_result_42)
+args2.append(
+ solver.mkTerm(solver.mkOp(kinds.BVExtract, 7, 4), [concat_result_43]))
+solver.assertFormula(solver.mkTerm(kinds.Equal, args2))
+
+args3 = []
+args3.append(concat_result_42)
+args3.append(
+ solver.mkTerm(solver.mkOp(kinds.BVExtract, 3, 0), [concat_result_43]))
+solver.assertFormula(solver.mkTerm(kinds.Equal, args3))
+
+print(solver.checkSat())
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andres Noetzli, 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 test for SolverEngine::resetAssertions()
- *
- * This program indirectly also tests some corner cases w.r.t.
- * context-dependent datastructures: resetAssertions() pops the contexts to
- * zero but some context-dependent datastructures are created at leevel 1,
- * which the datastructure needs to handle properly problematic.
- */
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-
-int main()
-{
- Solver slv;
- slv.setOption("incremental", "true");
-
- Sort real = slv.getRealSort();
- Term x = slv.mkConst(real, "x");
- Term four = slv.mkInteger(4);
- Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
- slv.assertFormula(xEqFour);
- std::cout << slv.checkSat() << std::endl;
-
- slv.resetAssertions();
-
- Sort elementType = slv.getIntegerSort();
- Sort indexType = slv.getIntegerSort();
- Sort arrayType = slv.mkArraySort(indexType, elementType);
- Term array = slv.mkConst(arrayType, "array");
- Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
- Term ten = slv.mkInteger(10);
- Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
- slv.assertFormula(arrayAtFour_eq_ten);
- std::cout << slv.checkSat() << std::endl;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew V. Jones, Andres Noetzli, 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.
- * ****************************************************************************
- *
- * Two tests to validate the use of the separation logic API.
- *
- * First test validates that we cannot use the API if not using separation
- * logic.
- *
- * Second test validates that the expressions returned from the API are
- * correct and can be interrogated.
- *
- ****************************************************************************/
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-using namespace std;
-
-/**
- * Test function to validate that we *cannot* obtain the heap/nil expressions
- * when *not* using the separation logic theory
- */
-int validate_exception(void)
-{
- Solver slv;
-
- /*
- * Setup some options for cvc5 -- we explictly want to use a simplistic
- * theory (e.g., QF_IDL)
- */
- slv.setLogic("QF_IDL");
- slv.setOption("produce-models", "true");
- slv.setOption("incremental", "false");
-
- /* Our integer type */
- Sort integer = slv.getIntegerSort();
-
- /** we intentionally do not set the separation logic heap */
-
- /* Our SMT constants */
- Term x = slv.mkConst(integer, "x");
- Term y = slv.mkConst(integer, "y");
-
- /* y > x */
- Term y_gt_x(slv.mkTerm(Kind::GT, y, x));
-
- /* assert it */
- slv.assertFormula(y_gt_x);
-
- /* check */
- Result r(slv.checkSat());
-
- /* If this is UNSAT, we have an issue; so bail-out */
- if (!r.isSat())
- {
- return -1;
- }
-
- /*
- * We now try to obtain our separation logic expressions from the solver --
- * we want to validate that we get our expected exceptions.
- */
- bool caught_on_heap(false);
- bool caught_on_nil(false);
-
- /* The exception message we expect to obtain */
- std::string expected(
- "Cannot obtain separation logic expressions if not using the separation "
- "logic theory.");
-
- /* test the heap expression */
- try
- {
- Term heap_expr = slv.getValueSepHeap();
- }
- catch (const CVC5ApiException& e)
- {
- caught_on_heap = true;
-
- /* Check we get the correct exception string */
- if (e.what() != expected)
- {
- return -1;
- }
- }
-
- /* test the nil expression */
- try
- {
- Term nil_expr = slv.getValueSepNil();
- }
- catch (const CVC5ApiException& e)
- {
- caught_on_nil = true;
-
- /* Check we get the correct exception string */
- if (e.what() != expected)
- {
- return -1;
- }
- }
-
- if (!caught_on_heap || !caught_on_nil)
- {
- return -1;
- }
-
- /* All tests pass! */
- return 0;
-}
-
-/**
- * Test function to demonstrate the use of, and validate the capability, of
- * obtaining the heap/nil expressions when using separation logic.
- */
-int validate_getters(void)
-{
- Solver slv;
-
- /* Setup some options for cvc5 */
- slv.setLogic("QF_ALL");
- slv.setOption("produce-models", "true");
- slv.setOption("incremental", "false");
-
- /* Our integer type */
- Sort integer = slv.getIntegerSort();
-
- /** Declare the separation logic heap types */
- slv.declareSepHeap(integer, integer);
-
- /* A "random" constant */
- Term random_constant = slv.mkInteger(0xDEADBEEF);
-
- /* Another random constant */
- Term expr_nil_val = slv.mkInteger(0xFBADBEEF);
-
- /* Our nil term */
- Term nil = slv.mkSepNil(integer);
-
- /* Our SMT constants */
- Term x = slv.mkConst(integer, "x");
- Term y = slv.mkConst(integer, "y");
- Term p1 = slv.mkConst(integer, "p1");
- Term p2 = slv.mkConst(integer, "p2");
-
- /* Constraints on x and y */
- Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant);
- Term y_gt_x = slv.mkTerm(Kind::GT, y, x);
-
- /* Points-to expressions */
- Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x);
- Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y);
-
- /* Heap -- the points-to have to be "starred"! */
- Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y);
-
- /* Constain "nil" to be something random */
- Term fix_nil = slv.mkTerm(Kind::EQUAL, nil, expr_nil_val);
-
- /* Add it all to the solver! */
- slv.assertFormula(x_equal_const);
- slv.assertFormula(y_gt_x);
- slv.assertFormula(heap);
- slv.assertFormula(fix_nil);
-
- /*
- * Incremental is disabled due to using separation logic, so don't query
- * twice!
- */
- Result r(slv.checkSat());
-
- /* If this is UNSAT, we have an issue; so bail-out */
- if (!r.isSat())
- {
- return -1;
- }
-
- /* Obtain our separation logic terms from the solver */
- Term heap_expr = slv.getValueSepHeap();
- Term nil_expr = slv.getValueSepNil();
-
- /* If the heap is not a separating conjunction, bail-out */
- if (heap_expr.getKind() != Kind::SEP_STAR)
- {
- return -1;
- }
-
- /* If nil is not a direct equality, bail-out */
- if (nil_expr.getKind() != Kind::EQUAL)
- {
- return -1;
- }
-
- /* Obtain the values for our "pointers" */
- Term val_for_p1 = slv.getValue(p1);
- Term val_for_p2 = slv.getValue(p2);
-
- /* We need to make sure we find both pointers in the heap */
- bool checked_p1(false);
- bool checked_p2(false);
-
- /* Walk all the children */
- for (const Term& child : heap_expr)
- {
- /* If we don't have a PTO operator, bail-out */
- if (child.getKind() != Kind::SEP_PTO)
- {
- return -1;
- }
-
- /* Find both sides of the PTO operator */
- Term addr = slv.getValue(child[0]);
- Term value = slv.getValue(child[1]);
-
- /* If the current address is the value for p1 */
- if (addr == val_for_p1)
- {
- checked_p1 = true;
-
- /* If it doesn't match the random constant, we have a problem */
- if (value != random_constant)
- {
- return -1;
- }
- continue;
- }
-
- /* If the current address is the value for p2 */
- if (addr == val_for_p2)
- {
- checked_p2 = true;
-
- /*
- * Our earlier constraint was that what p2 points to must be *greater*
- * than the random constant -- if we get a value that is LTE, then
- * something has gone wrong!
- */
- if (std::stoll(value.toString())
- <= std::stoll(random_constant.toString()))
- {
- return -1;
- }
- continue;
- }
-
- /*
- * We should only have two addresses in heap, so if we haven't hit the
- * "continue" for p1 or p2, then bail-out
- */
- return -1;
- }
-
- /*
- * If we complete the loop and we haven't validated both p1 and p2, then we
- * have a problem
- */
- if (!checked_p1 || !checked_p2)
- {
- return -1;
- }
-
- /* We now get our value for what nil is */
- Term value_for_nil = slv.getValue(nil_expr[1]);
-
- /*
- * The value for nil from the solver should be the value we originally tied
- * nil to
- */
- if (value_for_nil != expr_nil_val)
- {
- return -1;
- }
-
- /* All tests pass! */
- return 0;
-}
-
-int main(void)
-{
- /* check that we get an exception when we should */
- int check_exception(validate_exception());
-
- if (check_exception)
- {
- return check_exception;
- }
-
- /* check the getters */
- int check_getters(validate_getters());
-
- if (check_getters)
- {
- return check_getters;
- }
-
- return 0;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Aina Niemetz, Morgan Deters, 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 test of SMT-LIBv2 commands, checks for compliant output.
- */
-
-#include <cassert>
-#include <iostream>
-#include <sstream>
-
-#include "api/cpp/cvc5.h"
-#include "options/set_language.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-#include "smt/solver_engine.h"
-
-using namespace cvc5;
-using namespace cvc5::parser;
-using namespace std;
-
-void testGetInfo(api::Solver* solver, const char* s);
-
-int main()
-{
- cout << language::SetLanguage(Language::LANG_SMTLIB_V2_6);
-
- std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
- solver->setOption("input-language", "smtlib2");
- solver->setOption("output-language", "smtlib2");
- testGetInfo(solver.get(), ":error-behavior");
- testGetInfo(solver.get(), ":name");
- testGetInfo(solver.get(), ":authors");
- testGetInfo(solver.get(), ":version");
- testGetInfo(solver.get(), ":status");
- testGetInfo(solver.get(), ":reason-unknown");
- testGetInfo(solver.get(), ":arbitrary-undefined-keyword");
- testGetInfo(solver.get(), ":56"); // legal
- testGetInfo(solver.get(), ":<="); // legal
- testGetInfo(solver.get(), ":->"); // legal
- testGetInfo(solver.get(), ":all-statistics");
-
- return 0;
-}
-
-void testGetInfo(api::Solver* solver, const char* s)
-{
- std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
-
- std::unique_ptr<Parser> p(ParserBuilder(solver, symman.get(), true).build());
- p->setInput(Input::newStringInput(
- "LANG_SMTLIB_V2_6", string("(get-info ") + s + ")", "<internal>"));
- assert(p != NULL);
- Command* c = p->nextCommand();
- assert(c != NULL);
- cout << c << endl;
- stringstream ss;
- c->invoke(solver, symman.get(), ss);
- assert(p->nextCommand() == NULL);
- delete c;
- cout << ss.str() << endl << endl;
-}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andres Noetzli, Morgan Deters, 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 test of multiple SmtEngines.
- */
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cpp/cvc5.h"
-
-using namespace cvc5::api;
-using namespace std;
-
-int main() {
- Solver s1;
- Solver s2;
- Result r = s1.checkEntailed(s1.mkBoolean(true));
- Result r2 = s2.checkEntailed(s2.mkBoolean(true));
- return r.isEntailed() && r2.isEntailed() ? 0 : 1;
-}
-
--- /dev/null
+###############################################################################
+# Top contributors (to current version):
+# Aina Niemetz, Andrew V. Jones, Gereon Kremer
+#
+# 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.
+##
+include_directories(.)
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
+
+# if we've built using libedit, (--editline) then we want the interactive shell tests
+if (USE_EDITLINE)
+
+ # Check for pexpect -- zero return code is success
+ execute_process(
+ COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect"
+ RESULT_VARIABLE PEXPECT_RC
+ ERROR_QUIET
+ )
+
+ # Add the test if we have pexpect
+ if(PEXPECT_RC EQUAL 0)
+ add_custom_target(binarytests
+ COMMAND ctest --output-on-failure -L "binary" -j${CTEST_NTHREADS} $$ARGS)
+ add_test(
+ NAME interactive_shell
+ COMMAND
+ "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/binary/interactive_shell.py"
+ WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
+ )
+ set_tests_properties(interactive_shell PROPERTIES LABELS "binary")
+ endif()
+endif()
--- /dev/null
+#!/usr/bin/env python3
+###############################################################################
+# Top contributors (to current version):
+# Andrew V. Jones
+#
+# 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 test file to interact with cvc5 with line editing
+##
+
+import sys
+import pexpect
+
+def check_iteractive_shell():
+ """
+ Interacts with cvc5's interactive shell and checks that things such a tab
+ completion and "pressing up" works.
+ """
+
+ # Open cvc5
+ child = pexpect.spawnu("bin/cvc5", timeout=1)
+
+ # We expect to see the cvc5 prompt
+ child.expect("cvc5>")
+
+ # If we send a line with just 'BOOLE' ...
+ child.sendline("(set-log")
+
+ # ... then we get an error
+ child.expect("Parse Error: <shell>:1.7: expected SMT-LIBv2 command, got `set-log\'")
+
+ # Start sending 'BOOL' (without an E)
+ child.send("(declare-data")
+
+ # Send tab twice
+ child.sendcontrol("i")
+ child.sendcontrol("i")
+
+ # We expect to see the completion
+ child.expect("declare-datatype.*declare-datatypes")
+
+ # NOTE: the double tab has completed our '(declare-data' to '(declare-datatype'!
+
+ # Now send enter (which submits '(declare-datatype')
+ child.send(")")
+ child.sendcontrol("m")
+
+ # So we expect to see an error for 'BOOLE'
+ child.expect("Parse Error: <shell>:1.17: Unexpected token: '\)'.")
+
+ # Send enter
+ child.sendcontrol("m")
+
+ # We expect to see the cvc5 prompt
+ child.expect("cvc5>")
+
+ # Now send an up key
+ child.send("\033[A")
+
+ # Send enter
+ child.sendcontrol("m")
+
+ # We expect to see the previous error again
+ child.expect("Parse Error: <shell>:1.17: Unexpected token: '\)'.")
+
+ return 0
+
+
+def main():
+ """
+ Runs our interactive shell test
+
+ Caveats:
+
+ * If we don't have the "pexpect" model, the test doesn't get run, but
+ passes
+
+ * We expect pexpect to raise and exit with a non-zero exit code if any
+ of the steps fail
+ """
+
+ # If any of the "steps" fail, the pexpect will raise a Python will exit
+ # with a non-zero error code
+ sys.exit(check_iteractive_shell())
+
+if __name__ == "__main__":
+ main()
+
+# EOF
# Check if the pytest Python module is installed.
check_python_module("pytest")
-# Add Python bindings API tests.
+# Add Python bindings API unit tests.
macro(cvc5_add_python_api_unit_test name filename)
-# We create test target 'python/unit/api/myapitest' and run it with
-# 'ctest -R "python/unit/api/myapitest"'.
+# We create test target 'unit/api/python/myapitest' and run it with
+# 'ctest -R "unit/api/python/myapitest"'.
set(test_name unit/api/python/${name})
add_test (NAME ${test_name}
COMMAND ${PYTHON_EXECUTABLE}
-m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
# directory for importing the python bindings
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
- set_tests_properties(${test_name} PROPERTIES LABELS "unit")
+ set_tests_properties(${test_name} PROPERTIES LABELS "unit python")
endmacro()
# add specific test files
projects / cvc5.git / commitdiff