From 9dc2d55ce20f4b69b651ac75e28d3de0704b3520 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 28 Apr 2022 11:30:46 -0700 Subject: [PATCH] Move tests around (#8670) This PR moves two tests that dealt with particular issues out of unit/api/cpp (which should only have generic unit tests). They are now in unit/theory and api/cpp/. --- test/api/cpp/CMakeLists.txt | 3 + test/api/cpp/proj-issue388.cpp | 62 +++++++++++++ test/api/cpp/proj-issue421.cpp | 37 ++++++++ .../cpp/proj-issue455.cpp} | 87 ++----------------- test/unit/api/cpp/CMakeLists.txt | 2 - test/unit/theory/CMakeLists.txt | 1 + .../cpp => theory}/theory_uf_ho_black.cpp | 0 7 files changed, 112 insertions(+), 80 deletions(-) create mode 100644 test/api/cpp/proj-issue388.cpp create mode 100644 test/api/cpp/proj-issue421.cpp rename test/{unit/api/cpp/theory_arith_nl_black.cpp => api/cpp/proj-issue455.cpp} (54%) rename test/unit/{api/cpp => theory}/theory_uf_ho_black.cpp (100%) diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index fffb93ce3..bea15a3a0 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -57,7 +57,10 @@ cvc5_add_api_test(proj-issue334) cvc5_add_api_test(proj-issue344) cvc5_add_api_test(proj-issue345) cvc5_add_api_test(proj-issue377) +cvc5_add_api_test(proj-issue388) cvc5_add_api_test(proj-issue395) cvc5_add_api_test(proj-issue399) +cvc5_add_api_test(proj-issue421) cvc5_add_api_test(proj-issue445) +cvc5_add_api_test(proj-issue455) cvc5_add_api_test(proj-issue484) diff --git a/test/api/cpp/proj-issue388.cpp b/test/api/cpp/proj-issue388.cpp new file mode 100644 index 000000000..87638147b --- /dev/null +++ b/test/api/cpp/proj-issue388.cpp @@ -0,0 +1,62 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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 #388 + * + */ + +#include "api/cpp/cvc5.h" +#include "base/configuration.h" +#include + +using namespace cvc5; + +int main(void) +{ + if (!internal::Configuration::isBuiltWithPoly()) + { + return 0; + } + { // Original + Solver slv; + slv.setLogic("QF_NRA"); + Sort s = slv.getRealSort(); + Term t1 = slv.mkConst(s, "a"); + Term t2 = slv.mkConst(s, "b"); + Term t3 = slv.mkConst(s, "c"); + Term t4 = slv.mkTerm(Kind::DIVISION, {t1, t2}); + Term t5 = slv.mkTerm(Kind::GT, {t4, t3}); + Term t6 = slv.mkTerm(Kind::DIVISION, {t1, t3}); + Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t6}); + Term t8 = slv.mkTerm(Kind::AND, {t5, t7, t5}); + Term t9 = slv.mkTerm(Kind::NOT, {t8}); + slv.assertFormula(t9); + slv.checkSat(); + } + { // Minimized + Solver slv; + slv.setOption("nl-cov", "true"); + slv.setOption("nl-cov-var-elim", "true"); + slv.setOption("nl-ext", "none"); + slv.setLogic("QF_NIRA"); + Sort s = slv.getRealSort(); + Term t1 = slv.mkConst(s, "a"); + Term t2 = slv.mkConst(s, "b"); + Term t3 = slv.mkReal(0); + Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t1}); + Term t4 = slv.mkTerm(Kind::DIVISION, {t2, t1}); + Term t5 = slv.mkTerm(Kind::DISTINCT, {t3, t4}); + Term t8 = slv.mkTerm(Kind::OR, {t7, t5}); + slv.assertFormula(t8); + slv.checkSat(); + } +} diff --git a/test/api/cpp/proj-issue421.cpp b/test/api/cpp/proj-issue421.cpp new file mode 100644 index 000000000..3a152673e --- /dev/null +++ b/test/api/cpp/proj-issue421.cpp @@ -0,0 +1,37 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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 #421 + * + */ + +#include "api/cpp/cvc5.h" +#include + +using namespace cvc5; + +int main(void) +{ + Solver slv; + slv.setLogic("QF_ALL"); + Sort s1 = slv.mkBitVectorSort(4); + Sort s4 = slv.getRealSort(); + Sort s5 = slv.mkSequenceSort(s1); + Term t8 = slv.mkConst(s5, "_x49"); + Term t10 = slv.mkConst(s4, "_x51"); + Term t65 = slv.mkTerm(Kind::SEQ_REV, {t8}); + Term t69 = slv.mkTerm(Kind::TANGENT, {t10}); + Term t77 = slv.mkTerm(Kind::LEQ, {t69, t10}); + Term t128 = slv.mkTerm(Kind::SEQ_PREFIX, {t65, t8}); + slv.assertFormula({t77}); + slv.checkSatAssuming(t128.notTerm()); +} diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/api/cpp/proj-issue455.cpp similarity index 54% rename from test/unit/api/cpp/theory_arith_nl_black.cpp rename to test/api/cpp/proj-issue455.cpp index bf461ef66..c47247db9 100644 --- a/test/unit/api/cpp/theory_arith_nl_black.cpp +++ b/test/api/cpp/proj-issue455.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Gereon Kremer, Andrew Reynolds + * Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * @@ -10,87 +10,21 @@ * directory for licensing information. * **************************************************************************** * - * Blackbox tests using the API targeting nonlinear arithmetic. + * Test for project issue #455 + * */ -#include "test_api.h" +#include "api/cpp/cvc5.h" #include "base/configuration.h" +#include -namespace cvc5::internal { - -namespace test { - -class TestTheoryBlackArithNl : public TestApi -{ -}; +using namespace cvc5; -TEST_F(TestTheoryBlackArithNl, cvc5Projects388) +int main(void) { - if (!Configuration::isBuiltWithPoly()) + if (!internal::Configuration::isBuiltWithPoly()) { - return; - } - Solver slv; - slv.setLogic("QF_NRA"); - Sort s = slv.getRealSort(); - Term t1 = slv.mkConst(s, "a"); - Term t2 = slv.mkConst(s, "b"); - Term t3 = slv.mkConst(s, "c"); - Term t4 = slv.mkTerm(Kind::DIVISION, {t1, t2}); - Term t5 = slv.mkTerm(Kind::GT, {t4, t3}); - Term t6 = slv.mkTerm(Kind::DIVISION, {t1, t3}); - Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t6}); - Term t8 = slv.mkTerm(Kind::AND, {t5, t7, t5}); - Term t9 = slv.mkTerm(Kind::NOT, {t8}); - slv.assertFormula(t9); - slv.checkSat(); -} - -TEST_F(TestTheoryBlackArithNl, cvc5Projects388Min) -{ - if (!Configuration::isBuiltWithPoly()) - { - return; - } - Solver slv; - slv.setOption("nl-cov", "true"); - slv.setOption("nl-cov-var-elim", "true"); - slv.setOption("nl-ext", "none"); - slv.setLogic("QF_NIRA"); - Sort s = slv.getRealSort(); - Term t1 = slv.mkConst(s, "a"); - Term t2 = slv.mkConst(s, "b"); - Term t3 = slv.mkReal(0); - Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t1}); - Term t4 = slv.mkTerm(Kind::DIVISION, {t2, t1}); - Term t5 = slv.mkTerm(Kind::DISTINCT, {t3, t4}); - Term t8 = slv.mkTerm(Kind::OR, {t7, t5}); - slv.assertFormula(t8); - slv.checkSat(); -} - -TEST_F(TestTheoryBlackArithNl, proj_issue421) -{ - Solver slv; - slv.setLogic("QF_ALL"); - Sort s1 = slv.mkBitVectorSort(4); - Sort s4 = slv.getRealSort(); - Sort s5 = slv.mkSequenceSort(s1); - Term t8 = slv.mkConst(s5, "_x49"); - Term t10 = slv.mkConst(s4, "_x51"); - Term t65 = slv.mkTerm(Kind::SEQ_REV, {t8}); - Term t69 = slv.mkTerm(Kind::TANGENT, {t10}); - Term t77 = slv.mkTerm(Kind::LEQ, {t69, t10}); - Term t128 = slv.mkTerm(Kind::SEQ_PREFIX, {t65, t8}); - slv.assertFormula({t77}); - slv.checkSatAssuming(t128.notTerm()); -} - -TEST_F(TestTheoryBlackArithNl, cvc5Projects455) -{ - if (!Configuration::isBuiltWithPoly()) - { - return; + return 0; } Solver slv; slv.setLogic("QF_UFNRA"); @@ -139,6 +73,3 @@ TEST_F(TestTheoryBlackArithNl, cvc5Projects455) slv.assertFormula({t33}); slv.checkSatAssuming({t18.notTerm()}); } - -} // namespace test -} // namespace cvc5::internal diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt index 7d2657ea1..ca6fce4c3 100644 --- a/test/unit/api/cpp/CMakeLists.txt +++ b/test/unit/api/cpp/CMakeLists.txt @@ -21,8 +21,6 @@ cvc5_add_unit_test_black(result_black api/cpp) cvc5_add_unit_test_black(solver_black api/cpp) cvc5_add_unit_test_black(sort_black api/cpp) cvc5_add_unit_test_black(term_black api/cpp) -cvc5_add_unit_test_black(theory_arith_nl_black api/cpp) -cvc5_add_unit_test_black(theory_uf_ho_black api/cpp) cvc5_add_unit_test_white(op_white api/cpp) cvc5_add_unit_test_white(solver_white api/cpp) cvc5_add_unit_test_black(synth_result_black api/cpp) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index ea6730179..7381cab55 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -14,6 +14,7 @@ ## # Add unit tests. +cvc5_add_unit_test_black(theory_uf_ho_black theory) cvc5_add_unit_test_black(regexp_operation_black theory) cvc5_add_unit_test_black(theory_black theory) cvc5_add_unit_test_white(evaluator_white theory) diff --git a/test/unit/api/cpp/theory_uf_ho_black.cpp b/test/unit/theory/theory_uf_ho_black.cpp similarity index 100% rename from test/unit/api/cpp/theory_uf_ho_black.cpp rename to test/unit/theory/theory_uf_ho_black.cpp -- 2.30.2