From: Aina Niemetz Date: Tue, 15 Sep 2020 04:21:03 +0000 (-0700) Subject: Rename system tests to api tests and remove obsolete Java test. (#5066) X-Git-Tag: cvc5-1.0.0~2861 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cdb338bb5c0fc033f6788549985c5a60ab1323b3;p=cvc5.git Rename system tests to api tests and remove obsolete Java test. (#5066) --- diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 8c11acf3b..5138d79b5 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -31,8 +31,8 @@ add_dependencies(main cvc4 cvc4parser gen-tokens) 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_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index cc05aff43..4c8b9d156 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -2,11 +2,11 @@ # 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) @@ -24,7 +24,7 @@ add_custom_target(check 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) diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt new file mode 100644 index 000000000..8d9110e9f --- /dev/null +++ b/test/api/CMakeLists.txt @@ -0,0 +1,57 @@ +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() diff --git a/test/api/boilerplate.cpp b/test/api/boilerplate.cpp new file mode 100644 index 000000000..315cec7bf --- /dev/null +++ b/test/api/boilerplate.cpp @@ -0,0 +1,32 @@ +/********************* */ +/*! \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 +#include + +#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; +} + diff --git a/test/api/interactive_shell.py b/test/api/interactive_shell.py new file mode 100755 index 000000000..3cc9953ee --- /dev/null +++ b/test/api/interactive_shell.py @@ -0,0 +1,94 @@ +#!/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: :...: 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: :...: 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: :...: 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 diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp new file mode 100644 index 000000000..ef360628a --- /dev/null +++ b/test/api/ouroborous.cpp @@ -0,0 +1,138 @@ +/********************* */ +/*! \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 +#include +#include + +#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 solver = + std::unique_ptr(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; +} diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp new file mode 100644 index 000000000..dc9bd24f6 --- /dev/null +++ b/test/api/reset_assertions.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \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 +#include + +#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; +} diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp new file mode 100644 index 000000000..9341310a3 --- /dev/null +++ b/test/api/sep_log_api.cpp @@ -0,0 +1,303 @@ +/********************* */ +/*! \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 +#include + +#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; +} diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp new file mode 100644 index 000000000..340326e40 --- /dev/null +++ b/test/api/smt2_compliance.cpp @@ -0,0 +1,76 @@ +/********************* */ +/*! \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 +#include +#include + +#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 solver = + std::unique_ptr(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, "", 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; +} diff --git a/test/api/statistics.cpp b/test/api/statistics.cpp new file mode 100644 index 000000000..234246112 --- /dev/null +++ b/test/api/statistics.cpp @@ -0,0 +1,77 @@ +/********************* */ +/*! \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 +#include + +#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; +} diff --git a/test/api/two_solvers.cpp b/test/api/two_solvers.cpp new file mode 100644 index 000000000..c5bea4860 --- /dev/null +++ b/test/api/two_solvers.cpp @@ -0,0 +1,32 @@ +/********************* */ +/*! \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 +#include + +#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; +} + diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt deleted file mode 100644 index a9c1a80db..000000000 --- a/test/system/CMakeLists.txt +++ /dev/null @@ -1,59 +0,0 @@ -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) diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java deleted file mode 100644 index c38cfab3d..000000000 --- a/test/system/CVC4JavaTest.java +++ /dev/null @@ -1,70 +0,0 @@ -/********************* */ -/*! \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); - } - } -} - diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp deleted file mode 100644 index 315cec7bf..000000000 --- a/test/system/boilerplate.cpp +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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; -} - diff --git a/test/system/interactive_shell.py b/test/system/interactive_shell.py deleted file mode 100755 index 3cc9953ee..000000000 --- a/test/system/interactive_shell.py +++ /dev/null @@ -1,94 +0,0 @@ -#!/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: :...: 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: :...: 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: :...: 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 diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp deleted file mode 100644 index ef360628a..000000000 --- a/test/system/ouroborous.cpp +++ /dev/null @@ -1,138 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#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 solver = - std::unique_ptr(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; -} diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp deleted file mode 100644 index dc9bd24f6..000000000 --- a/test/system/reset_assertions.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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; -} diff --git a/test/system/sep_log_api.cpp b/test/system/sep_log_api.cpp deleted file mode 100644 index 9341310a3..000000000 --- a/test/system/sep_log_api.cpp +++ /dev/null @@ -1,303 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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; -} diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp deleted file mode 100644 index 340326e40..000000000 --- a/test/system/smt2_compliance.cpp +++ /dev/null @@ -1,76 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#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 solver = - std::unique_ptr(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, "", 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; -} diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp deleted file mode 100644 index 234246112..000000000 --- a/test/system/statistics.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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; -} diff --git a/test/system/two_solvers.cpp b/test/system/two_solvers.cpp deleted file mode 100644 index c5bea4860..000000000 --- a/test/system/two_solvers.cpp +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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; -} -