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