get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES)
target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
-# main-test library is only used for linking against system and unit tests so
-# that we don't have to include all object files of main into each unit/system
+# main-test library is only used for linking against api and unit tests so
+# that we don't have to include all object files of main into each api/unit
# test. Do not link against main-test in any other case.
add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>)
target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER)
# Add target 'check', builds and runs
# > unit tests
# > regression tests of levels 0 and 1
-# > system tests
+# > api tests
add_custom_target(build-tests)
-# Note: Do not add custom targets for running tests (regress, systemtests,
+# Note: Do not add custom targets for running tests (regress, apitests,
# units) as dependencies to other run targets. This will result in executing
# tests multiple times. For example, if check would depend on regress it would
# first run the command of the regress target (i.e., run all regression tests)
if (NOT BUILD_LIB_ONLY)
add_subdirectory(regress)
endif()
-add_subdirectory(system EXCLUDE_FROM_ALL)
+add_subdirectory(api EXCLUDE_FROM_ALL)
if(ENABLE_UNIT_TESTING)
add_subdirectory(unit EXCLUDE_FROM_ALL)
--- /dev/null
+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(CVC4_API_TEST_FLAGS
+ -D__BUILDING_CVC4_API_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
+
+macro(cvc4_add_api_test name)
+ add_executable(${name} ${name}.cpp)
+ target_link_libraries(${name} main-test)
+ target_compile_definitions(${name} PRIVATE ${CVC4_API_TEST_FLAGS})
+ add_test(api/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name})
+ set_tests_properties(api/${name} PROPERTIES LABELS "api")
+ add_dependencies(build-apitests ${name})
+endmacro()
+
+cvc4_add_api_test(boilerplate)
+cvc4_add_api_test(ouroborous)
+cvc4_add_api_test(reset_assertions)
+cvc4_add_api_test(sep_log_api)
+cvc4_add_api_test(smt2_compliance)
+# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API
+# cvc4_add_api_test(statistics)
+cvc4_add_api_test(two_solvers)
+
+# 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()
+endif()
--- /dev/null
+/********************* */
+/*! \file boilerplate.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief A simple start-up/tear-down test for CVC4.
+ **
+ ** 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/cvc4cpp.h"
+
+using namespace CVC4::api;
+using namespace std;
+
+int main() {
+ Solver slv;
+ Result r = slv.checkEntailed(slv.mkBoolean(true));
+ return r.isEntailed() ? 0 : 1;
+}
+
--- /dev/null
+#!/usr/bin/env python3
+
+#####################
+#! \file interactive_shell.py
+## \verbatim
+## Top contributors (to current version):
+## Andrew V. Jones
+## This file is part of the CVC4 project.
+## Copyright (c) 2020 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.\endverbatim
+##
+## \brief A simple test file to interact with CVC4 with line editing
+#####################
+
+import sys
+import pexpect
+
+def check_iteractive_shell():
+ """
+ Interacts with CVC4's interactive shell and checks that things such a tab
+ completion and "pressing up" works.
+ """
+
+ # Open CVC4
+ child = pexpect.spawnu("bin/cvc4", timeout=1)
+
+ # We expect to see the CVC4 prompt
+ child.expect("CVC4>")
+
+ # If we send a line with just 'BOOLE' ...
+ child.sendline("BOOLE")
+
+ # ... then we get an error
+ child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
+
+ # Start sending 'BOOL' (without an E)
+ child.send("BOOL")
+
+ # Send tab twice
+ child.sendcontrol("i")
+ child.sendcontrol("i")
+
+ # We expect to see the completion
+ child.expect("BOOL.*BOOLEAN.*BOOLEXTRACT")
+
+ # NOTE: the double tab has completed our 'BOOL' to 'BOOLE'!
+
+ # Now send enter (which submits 'BOOLE')
+ child.sendcontrol("m")
+
+ # So we expect to see an error for 'BOOLE'
+ child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
+
+ # Send enter
+ child.sendcontrol("m")
+
+ # We expect to see the CVC4 prompt
+ child.expect("CVC4>")
+
+ # Now send an up key
+ child.send("\033[A")
+
+ # Send enter
+ child.sendcontrol("m")
+
+ # We expect to see an error on 'BOOLE' again
+ child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
+
+ 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
+/********************* */
+/*! \file ouroborous.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Aina Niemetz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief "Ouroborous" test: does CVC4 read its own output?
+ **
+ ** The "Ouroborous" test, named after the serpent that swallows its
+ ** own tail, ensures that CVC4 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 <iostream>
+#include <sstream>
+#include <string>
+
+#include "api/cvc4cpp.h"
+#include "expr/expr.h"
+#include "expr/expr_iomanip.h"
+#include "options/set_language.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "smt/command.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::language;
+using namespace std;
+
+const string 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\
+";
+
+Parser* psr = NULL;
+
+int runTest();
+
+int main() {
+ try {
+ return runTest();
+ } catch(Exception& e) {
+ cerr << e << endl;
+ } catch(...) {
+ cerr << "non-cvc4 exception thrown." << endl;
+ }
+ return 1;
+}
+
+string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
+ cout << "==============================================" << endl
+ << "translating from " << inlang << " to " << outlang << " this string:" << endl
+ << in << endl;
+ psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
+ Expr e = psr->nextExpression().getExpr();
+ stringstream ss;
+ ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e;
+ assert(psr->nextExpression().isNull());// next expr should be null
+ assert(psr->done());// parser should be done
+ string s = ss.str();
+ cout << "got this:" << endl
+ << s << endl
+ << "reparsing as " << outlang << endl;
+
+ psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer"));
+ Expr f = psr->nextExpression().getExpr();
+ assert(e == f);
+ cout << "got same expressions " << e.getId() << " and " << f.getId() << endl
+ << "==============================================" << endl;
+
+ return s;
+}
+
+void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTLIB_V2) {
+ cout << endl
+ << "starting with: " << instr << endl
+ << " in language " << instrlang << endl;
+ string smt2 = translate(instr, instrlang, output::LANG_SMTLIB_V2);
+ cout << "in SMT2 : " << smt2 << endl;
+ /* -- SMT-LIBv1 doesn't have a functional printer yet
+ string smt1 = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
+ cout << "in SMT1 : " << smt1 << endl;
+ */
+ string cvc = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_CVC4);
+ cout << "in CVC : " << cvc << endl;
+ string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
+ cout << "back to SMT2 : " << out << endl << endl;
+
+ assert(out == smt2);// differences in output
+}
+
+
+int runTest() {
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(new api::Solver());
+ psr = ParserBuilder(solver.get(), "internal-buffer")
+ .withStringInput(declarations)
+ .withInputLanguage(input::LANG_SMTLIB_V2)
+ .build();
+
+ // we don't need to execute them, but we DO need to parse them to
+ // get the declarations
+ while(Command* c = psr->nextCommand()) {
+ delete c;
+ }
+
+ assert(psr->done());// parser should be done
+
+ cout << expr::ExprSetDepth(-1);
+
+ runTestString("(= (f (f y)) x)");
+ runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
+ runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4);
+ runTestString("a[x][y] = a[y][x]", input::LANG_CVC4);
+
+ delete psr;
+ psr = NULL;
+
+ return 0;
+}
--- /dev/null
+/********************* */
+/*! \file reset_assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief A simple test for SmtEngine::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/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+int main()
+{
+ Solver slv;
+ slv.setOption("incremental", "true");
+
+ Sort real = slv.getRealSort();
+ Term x = slv.mkConst(real, "x");
+ Term four = slv.mkReal(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.mkReal(10);
+ Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
+ slv.assertFormula(arrayAtFour_eq_ten);
+ std::cout << slv.checkSat() << std::endl;
+}
--- /dev/null
+/********************* */
+/*! \file sep_log_api.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew V. Jones
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief 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/cvc4cpp.h"
+
+using namespace CVC4::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 CVC4 -- 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();
+
+ /* 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.getSeparationHeap();
+ }
+ catch (const CVC4ApiException& 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.getSeparationNilTerm();
+ }
+ catch (const CVC4ApiException& 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 CVC4 */
+ slv.setLogic("QF_ALL_SUPPORTED");
+ slv.setOption("produce-models", "true");
+ slv.setOption("incremental", "false");
+
+ /* Our integer type */
+ Sort integer = slv.getIntegerSort();
+
+ /* A "random" constant */
+ Term random_constant = slv.mkReal(0xDEADBEEF);
+
+ /* Another random constant */
+ Term expr_nil_val = slv.mkReal(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.getSeparationHeap();
+ Term nil_expr = slv.getSeparationNilTerm();
+
+ /* 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
+/********************* */
+/*! \file smt2_compliance.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief A test of SMT-LIBv2 commands, checks for compliant output
+ **
+ ** A test of SMT-LIBv2 commands, checks for compliant output.
+ **/
+
+#include <cassert>
+#include <iostream>
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+#include "expr/expr_manager.h"
+#include "options/options.h"
+#include "options/set_language.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "smt/command.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+void testGetInfo(api::Solver* solver, const char* s);
+
+int main()
+{
+ Options opts;
+ opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
+ opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+
+ cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(new api::Solver(&opts));
+
+ 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)
+{
+ ParserBuilder pb(solver, "<internal>", solver->getOptions());
+ Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
+ assert(p != NULL);
+ Command* c = p->nextCommand();
+ assert(c != NULL);
+ cout << c << endl;
+ stringstream ss;
+ c->invoke(solver->getSmtEngine(), ss);
+ assert(p->nextCommand() == NULL);
+ delete p;
+ delete c;
+ cout << ss.str() << endl << endl;
+}
--- /dev/null
+/********************* */
+/*! \file statistics.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Aina Niemetz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief A simple statistics test for CVC4.
+ **
+ ** This simple test just makes sure that the statistics interface is
+ ** minimally functional.
+ **/
+
+#include "util/statistics.h"
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+#include "util/sexpr.h"
+
+using namespace CVC4;
+using namespace std;
+
+int main() {
+ api::Solver slv;
+ ExprManager* em = slv.getExprManager();
+ SmtEngine* smt = slv.getSmtEngine();
+ smt->setOption("incremental", SExpr("true"));
+ Expr x = em->mkVar("x", em->integerType());
+ Expr y = em->mkVar("y", em->integerType());
+ smt->assertFormula(em->mkExpr(
+ kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5))));
+ Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0)));
+ Result r = smt->checkEntailed(q);
+
+ if (r != Result::NOT_ENTAILED)
+ {
+ exit(1);
+ }
+
+ Statistics stats = smt->getStatistics();
+ for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
+ cout << "stat " << (*i).first << " is " << (*i).second << endl;
+ }
+
+ smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5))));
+ r = smt->checkEntailed(q);
+ Statistics stats2 = smt->getStatistics();
+ bool different = false;
+ for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
+ cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
+ cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
+ if (smt->getStatistic((*i).first) != (*i).second)
+ {
+ cout << "SMT engine reports different value for statistic " << (*i).first
+ << ": " << smt->getStatistic((*i).first) << endl;
+ exit(1);
+ }
+ different = different || stats.getStatistic((*i).first) != (*i).second;
+ }
+
+#ifdef CVC4_STATISTICS_ON
+ if(!different) {
+ cout << "stats are the same! bailing.." << endl;
+ exit(1);
+ }
+#endif /* CVC4_STATISTICS_ON */
+
+ return r == Result::ENTAILED ? 0 : 1;
+}
--- /dev/null
+/********************* */
+/*! \file two_smt_engines.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief A simple test of multiple SmtEngines
+ **
+ ** A simple test of multiple SmtEngines.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::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
-include_directories(.)
-include_directories(${PROJECT_SOURCE_DIR}/src)
-include_directories(${PROJECT_SOURCE_DIR}/src/include)
-include_directories(${CMAKE_BINARY_DIR}/src)
-
-#-----------------------------------------------------------------------------#
-# Add target 'systemtests', builds and runs
-# > system tests
-
-add_custom_target(build-systemtests)
-add_dependencies(build-tests build-systemtests)
-
-add_custom_target(systemtests
- COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $$ARGS
- DEPENDS build-systemtests)
-
-set(CVC4_SYSTEM_TEST_FLAGS
- -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
-
-macro(cvc4_add_system_test name)
- add_executable(${name} ${name}.cpp)
- target_link_libraries(${name} main-test)
- target_compile_definitions(${name} PRIVATE ${CVC4_SYSTEM_TEST_FLAGS})
- add_test(system/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name})
- set_tests_properties(system/${name} PROPERTIES LABELS "system")
- add_dependencies(build-systemtests ${name})
-endmacro()
-
-cvc4_add_system_test(boilerplate)
-cvc4_add_system_test(ouroborous)
-cvc4_add_system_test(reset_assertions)
-cvc4_add_system_test(sep_log_api)
-cvc4_add_system_test(smt2_compliance)
-# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API
-# cvc4_add_system_test(statistics)
-cvc4_add_system_test(two_solvers)
-
-# 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/system/interactive_shell.py"
- WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
- )
- endif()
-endif()
-
-# TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration)
+++ /dev/null
-/********************* */
-/*! \file CVC4JavaTest.java
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-import edu.nyu.acsys.CVC4.CVC4;
-
-import edu.nyu.acsys.CVC4.SmtEngine;
-import edu.nyu.acsys.CVC4.ExprManager;
-import edu.nyu.acsys.CVC4.Expr;
-import edu.nyu.acsys.CVC4.Type;
-import edu.nyu.acsys.CVC4.Kind;
-import edu.nyu.acsys.CVC4.Result;
-import edu.nyu.acsys.CVC4.Configuration;
-
-//import edu.nyu.acsys.CVC4.Exception;
-
-import edu.nyu.acsys.CVC4.Parser;
-import edu.nyu.acsys.CVC4.ParserBuilder;
-
-public class CVC4JavaTest {
- public static void main(String[] args) {
- try {
- System.loadLibrary("cvc4jni");
-
- //CVC4.getDebugChannel().on("current");
-
- System.out.println(Configuration.about());
-
- String[] tags = Configuration.getDebugTags();
- System.out.print("available debug tags:");
- for(int i = 0; i < tags.length; ++i) {
- System.out.print(" " + tags[i]);
- }
- System.out.println();
-
- ExprManager em = new ExprManager();
- SmtEngine smt = new SmtEngine(em);
-
- Type t = em.booleanType();
- Expr a = em.mkVar("a", em.booleanType());
- Expr b = em.mkVar("b", em.booleanType());
- Expr e = new Expr(em.mkExpr(Kind.AND, a, b, new Expr(a).notExpr()));
- System.out.println("==> " + e);
-
- Result r = smt.checkSat(e);
- boolean correct = r.isSat() == Result.Sat.UNSAT;
-
- System.out.println(smt.getStatistics());
-
- System.exit(correct ? 0 : 1);
- } catch(Exception e) {
- System.err.println(e);
- System.exit(1);
- }
- }
-}
-
+++ /dev/null
-/********************* */
-/*! \file boilerplate.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief A simple start-up/tear-down test for CVC4.
- **
- ** 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/cvc4cpp.h"
-
-using namespace CVC4::api;
-using namespace std;
-
-int main() {
- Solver slv;
- Result r = slv.checkEntailed(slv.mkBoolean(true));
- return r.isEntailed() ? 0 : 1;
-}
-
+++ /dev/null
-#!/usr/bin/env python3
-
-#####################
-#! \file interactive_shell.py
-## \verbatim
-## Top contributors (to current version):
-## Andrew V. Jones
-## This file is part of the CVC4 project.
-## Copyright (c) 2020 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.\endverbatim
-##
-## \brief A simple test file to interact with CVC4 with line editing
-#####################
-
-import sys
-import pexpect
-
-def check_iteractive_shell():
- """
- Interacts with CVC4's interactive shell and checks that things such a tab
- completion and "pressing up" works.
- """
-
- # Open CVC4
- child = pexpect.spawnu("bin/cvc4", timeout=1)
-
- # We expect to see the CVC4 prompt
- child.expect("CVC4>")
-
- # If we send a line with just 'BOOLE' ...
- child.sendline("BOOLE")
-
- # ... then we get an error
- child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
-
- # Start sending 'BOOL' (without an E)
- child.send("BOOL")
-
- # Send tab twice
- child.sendcontrol("i")
- child.sendcontrol("i")
-
- # We expect to see the completion
- child.expect("BOOL.*BOOLEAN.*BOOLEXTRACT")
-
- # NOTE: the double tab has completed our 'BOOL' to 'BOOLE'!
-
- # Now send enter (which submits 'BOOLE')
- child.sendcontrol("m")
-
- # So we expect to see an error for 'BOOLE'
- child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
-
- # Send enter
- child.sendcontrol("m")
-
- # We expect to see the CVC4 prompt
- child.expect("CVC4>")
-
- # Now send an up key
- child.send("\033[A")
-
- # Send enter
- child.sendcontrol("m")
-
- # We expect to see an error on 'BOOLE' again
- child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
-
- 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
-/********************* */
-/*! \file ouroborous.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Aina Niemetz, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief "Ouroborous" test: does CVC4 read its own output?
- **
- ** The "Ouroborous" test, named after the serpent that swallows its
- ** own tail, ensures that CVC4 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 <iostream>
-#include <sstream>
-#include <string>
-
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
-#include "options/set_language.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::language;
-using namespace std;
-
-const string 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\
-";
-
-Parser* psr = NULL;
-
-int runTest();
-
-int main() {
- try {
- return runTest();
- } catch(Exception& e) {
- cerr << e << endl;
- } catch(...) {
- cerr << "non-cvc4 exception thrown." << endl;
- }
- return 1;
-}
-
-string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
- cout << "==============================================" << endl
- << "translating from " << inlang << " to " << outlang << " this string:" << endl
- << in << endl;
- psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
- Expr e = psr->nextExpression().getExpr();
- stringstream ss;
- ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e;
- assert(psr->nextExpression().isNull());// next expr should be null
- assert(psr->done());// parser should be done
- string s = ss.str();
- cout << "got this:" << endl
- << s << endl
- << "reparsing as " << outlang << endl;
-
- psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer"));
- Expr f = psr->nextExpression().getExpr();
- assert(e == f);
- cout << "got same expressions " << e.getId() << " and " << f.getId() << endl
- << "==============================================" << endl;
-
- return s;
-}
-
-void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTLIB_V2) {
- cout << endl
- << "starting with: " << instr << endl
- << " in language " << instrlang << endl;
- string smt2 = translate(instr, instrlang, output::LANG_SMTLIB_V2);
- cout << "in SMT2 : " << smt2 << endl;
- /* -- SMT-LIBv1 doesn't have a functional printer yet
- string smt1 = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
- cout << "in SMT1 : " << smt1 << endl;
- */
- string cvc = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_CVC4);
- cout << "in CVC : " << cvc << endl;
- string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
- cout << "back to SMT2 : " << out << endl << endl;
-
- assert(out == smt2);// differences in output
-}
-
-
-int runTest() {
- std::unique_ptr<api::Solver> solver =
- std::unique_ptr<api::Solver>(new api::Solver());
- psr = ParserBuilder(solver.get(), "internal-buffer")
- .withStringInput(declarations)
- .withInputLanguage(input::LANG_SMTLIB_V2)
- .build();
-
- // we don't need to execute them, but we DO need to parse them to
- // get the declarations
- while(Command* c = psr->nextCommand()) {
- delete c;
- }
-
- assert(psr->done());// parser should be done
-
- cout << expr::ExprSetDepth(-1);
-
- runTestString("(= (f (f y)) x)");
- runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
- runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4);
- runTestString("a[x][y] = a[y][x]", input::LANG_CVC4);
-
- delete psr;
- psr = NULL;
-
- return 0;
-}
+++ /dev/null
-/********************* */
-/*! \file reset_assertions.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief A simple test for SmtEngine::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/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-int main()
-{
- Solver slv;
- slv.setOption("incremental", "true");
-
- Sort real = slv.getRealSort();
- Term x = slv.mkConst(real, "x");
- Term four = slv.mkReal(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.mkReal(10);
- Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
- slv.assertFormula(arrayAtFour_eq_ten);
- std::cout << slv.checkSat() << std::endl;
-}
+++ /dev/null
-/********************* */
-/*! \file sep_log_api.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew V. Jones
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief 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/cvc4cpp.h"
-
-using namespace CVC4::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 CVC4 -- 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();
-
- /* 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.getSeparationHeap();
- }
- catch (const CVC4ApiException& 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.getSeparationNilTerm();
- }
- catch (const CVC4ApiException& 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 CVC4 */
- slv.setLogic("QF_ALL_SUPPORTED");
- slv.setOption("produce-models", "true");
- slv.setOption("incremental", "false");
-
- /* Our integer type */
- Sort integer = slv.getIntegerSort();
-
- /* A "random" constant */
- Term random_constant = slv.mkReal(0xDEADBEEF);
-
- /* Another random constant */
- Term expr_nil_val = slv.mkReal(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.getSeparationHeap();
- Term nil_expr = slv.getSeparationNilTerm();
-
- /* 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
-/********************* */
-/*! \file smt2_compliance.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief A test of SMT-LIBv2 commands, checks for compliant output
- **
- ** A test of SMT-LIBv2 commands, checks for compliant output.
- **/
-
-#include <cassert>
-#include <iostream>
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-#include "expr/expr_manager.h"
-#include "options/options.h"
-#include "options/set_language.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "smt/command.h"
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace std;
-
-void testGetInfo(api::Solver* solver, const char* s);
-
-int main()
-{
- Options opts;
- opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
- opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-
- cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
-
- std::unique_ptr<api::Solver> solver =
- std::unique_ptr<api::Solver>(new api::Solver(&opts));
-
- 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)
-{
- ParserBuilder pb(solver, "<internal>", solver->getOptions());
- Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
- assert(p != NULL);
- Command* c = p->nextCommand();
- assert(c != NULL);
- cout << c << endl;
- stringstream ss;
- c->invoke(solver->getSmtEngine(), ss);
- assert(p->nextCommand() == NULL);
- delete p;
- delete c;
- cout << ss.str() << endl << endl;
-}
+++ /dev/null
-/********************* */
-/*! \file statistics.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Aina Niemetz, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief A simple statistics test for CVC4.
- **
- ** This simple test just makes sure that the statistics interface is
- ** minimally functional.
- **/
-
-#include "util/statistics.h"
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
-#include "util/sexpr.h"
-
-using namespace CVC4;
-using namespace std;
-
-int main() {
- api::Solver slv;
- ExprManager* em = slv.getExprManager();
- SmtEngine* smt = slv.getSmtEngine();
- smt->setOption("incremental", SExpr("true"));
- Expr x = em->mkVar("x", em->integerType());
- Expr y = em->mkVar("y", em->integerType());
- smt->assertFormula(em->mkExpr(
- kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5))));
- Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0)));
- Result r = smt->checkEntailed(q);
-
- if (r != Result::NOT_ENTAILED)
- {
- exit(1);
- }
-
- Statistics stats = smt->getStatistics();
- for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
- cout << "stat " << (*i).first << " is " << (*i).second << endl;
- }
-
- smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5))));
- r = smt->checkEntailed(q);
- Statistics stats2 = smt->getStatistics();
- bool different = false;
- for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
- cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
- cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
- if (smt->getStatistic((*i).first) != (*i).second)
- {
- cout << "SMT engine reports different value for statistic " << (*i).first
- << ": " << smt->getStatistic((*i).first) << endl;
- exit(1);
- }
- different = different || stats.getStatistic((*i).first) != (*i).second;
- }
-
-#ifdef CVC4_STATISTICS_ON
- if(!different) {
- cout << "stats are the same! bailing.." << endl;
- exit(1);
- }
-#endif /* CVC4_STATISTICS_ON */
-
- return r == Result::ENTAILED ? 0 : 1;
-}
+++ /dev/null
-/********************* */
-/*! \file two_smt_engines.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief A simple test of multiple SmtEngines
- **
- ** A simple test of multiple SmtEngines.
- **/
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::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;
-}
-
projects / cvc5.git / commitdiff