diff options
Diffstat (limited to 'test')
51 files changed, 1259 insertions, 338 deletions
diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp index bd7be2ad0..c0366ce23 100644 --- a/test/api/issue6111.cpp +++ b/test/api/issue6111.cpp @@ -27,7 +27,7 @@ int main() solver.setLogic("QF_BV"); Sort bvsort12979 = solver.mkBitVectorSort(12979); Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); - Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + Term zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10); vector<Term> args1; args1.push_back(zero); diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py index 07a57a5c6..5126a481d 100644 --- a/test/python/unit/api/test_op.py +++ b/test/python/unit/api/test_op.py @@ -86,6 +86,9 @@ def test_get_num_indices(solver): assert 2 == floatingpoint_to_fp_generic.getNumIndices() assert 2 == regexp_loop.getNumIndices() +def test_op_indices_list(solver): + with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + assert 2 == with_list.getNumIndices() def test_get_indices_string(solver): x = Op(solver) diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index db49f8bea..6052a057f 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -381,15 +381,6 @@ def test_mk_rounding_mode(solver): solver.mkRoundingMode(pycvc5.RoundTowardZero) -def test_mk_uninterpreted_const(solver): - solver.mkUninterpretedConst(solver.getBooleanSort(), 1) - with pytest.raises(RuntimeError): - solver.mkUninterpretedConst(pycvc5.Sort(solver), 1) - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkUninterpretedConst(solver.getBooleanSort(), 1) - - def test_mk_abstract_value(solver): solver.mkAbstractValue("1") with pytest.raises(ValueError): @@ -653,6 +644,10 @@ def test_mk_regexp_sigma(solver): solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma()) +def test_mk_sep_emp(solver): + solver.mkSepEmp(); + + def test_mk_sep_nil(solver): solver.mkSepNil(solver.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index def539cf4..98cf76d76 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -60,6 +60,11 @@ def test_operators_comparison(solver): solver.getIntegerSort() > Sort(solver) solver.getIntegerSort() >= Sort(solver) +def test_is_null(solver): + x = Sort(solver) + assert x.isNull() + x = solver.getBooleanSort() + assert not x.isNull() def test_is_boolean(solver): assert solver.getBooleanSort().isBoolean() @@ -140,6 +145,12 @@ def test_is_tester(solver): assert cons_sort.isTester() Sort(solver).isTester() +def test_is_updater(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + updater_sort = dt[0][0].getUpdaterTerm().getSort() + assert updater_sort.isUpdater() + Sort(solver).isUpdater() def test_is_function(solver): fun_sort = solver.mkFunctionSort(solver.getRealSort(), @@ -438,26 +449,26 @@ def test_get_uninterpreted_sort_constructor_arity(solver): def test_get_bv_size(solver): bvSort = solver.mkBitVectorSort(32) - bvSort.getBVSize() + bvSort.getBitVectorSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getBVSize() + setSort.getBitVectorSize() def test_get_fp_exponent_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() + fpSort.getFloatingPointExponentSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + setSort.getFloatingPointExponentSize() def test_get_fp_significand_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() + fpSort.getFloatingPointSignificandSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + setSort.getFloatingPointSignificandSize() def test_get_datatype_paramsorts(solver): diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 907dc22d1..ca9ce349f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -479,6 +479,7 @@ set(regress_0_tests regress0/datatypes/coda_simp_model.smt2 regress0/datatypes/conqueue-dt-enum-iloop.smt2 regress0/datatypes/data-nested-codata.smt2 + regress0/datatypes/datatype-dump.cvc.smt2 regress0/datatypes/datatype.cvc.smt2 regress0/datatypes/datatype0.cvc.smt2 regress0/datatypes/datatype1.cvc.smt2 @@ -498,6 +499,7 @@ set(regress_0_tests regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 regress0/datatypes/issue2838.cvc.smt2 + regress0/datatypes/issue4393-cdt-model.smt2 regress0/datatypes/issue5280-no-nrec.smt2 regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/list-bool.smt2 @@ -557,6 +559,7 @@ set(regress_0_tests regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/echo.smt2 + regress0/eqrange0.smt2 regress0/eqrange1.smt2 regress0/eqrange2.smt2 regress0/eqrange3.smt2 @@ -765,10 +768,12 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 + regress0/options/interactive-mode.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 + regress0/options/stream-printing.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 @@ -779,6 +784,7 @@ set(regress_0_tests regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 regress0/parser/issue5163.smt2 + regress0/parser/issue6908-get-value-uc.smt2 regress0/parser/issue7274.smt2 regress0/parser/linear_arithmetic_err1.smt2 regress0/parser/linear_arithmetic_err2.smt2 @@ -828,6 +834,11 @@ set(regress_0_tests regress0/preprocess/preprocess_13.cvc.smt2 regress0/preprocess/preprocess_14.cvc.smt2 regress0/preprocess/preprocess_15.cvc.smt2 + regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 + regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 + regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 + regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 + regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 regress0/print_define_fun_internal.smt2 regress0/print_lambda.cvc.smt2 regress0/print_model.cvc.smt2 @@ -844,6 +855,7 @@ set(regress_0_tests regress0/proofs/open-pf-datatypes.smt2 regress0/proofs/open-pf-if-unordered-iff.smt2 regress0/proofs/open-pf-rederivation.smt2 + regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/scope.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 @@ -875,6 +887,7 @@ set(regress_0_tests regress0/push-pop/incremental-subst-bug.cvc.smt2 regress0/push-pop/issue1986.smt2 regress0/push-pop/issue2137.min.smt2 + regress0/push-pop/issue6535-inc-solve.smt2 regress0/push-pop/quant-fun-proc-unfd.smt2 regress0/push-pop/real-as-int-incremental.smt2 regress0/push-pop/simple_unsat_cores.smt2 @@ -917,10 +930,12 @@ set(regress_0_tests regress0/quantifiers/issue4576.smt2 regress0/quantifiers/issue5645-dt-cm-spurious.smt2 regress0/quantifiers/issue5693-prenex.smt2 + regress0/quantifiers/issue6475-rr-const.smt2 regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 regress0/quantifiers/issue6838-qpdt.smt2 regress0/quantifiers/issue6996-trivial-elim.smt2 regress0/quantifiers/issue6999-deq-elim.smt2 + regress0/quantifiers/issue7353-var-elim-par-dt.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 @@ -964,6 +979,7 @@ set(regress_0_tests regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/ufnia-fv-delta.smt2 + regress0/quantifiers/veqt-delta.smt2 regress0/rec-fun-const-parse-bug.smt2 regress0/rels/addr_book_0.cvc.smt2 regress0/rels/atom_univ2.cvc.smt2 @@ -1499,6 +1515,8 @@ set(regress_1_tests regress1/arith/issue3952-rew-eq.smt2 regress1/arith/issue4985-model-success.smt2 regress1/arith/issue4985b-model-success.smt2 + regress1/arith/issue6774-sanity-int-model.smt2 + regress1/arith/issue7252-arith-sanity.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc.smt2 regress1/arith/mod.02.smt2 @@ -1570,6 +1588,7 @@ set(regress_1_tests regress1/constarr3.cvc.smt2 regress1/constarr3.smt2 regress1/cores/issue5604.smt2 + regress1/cores/issue6988-arith-sanity.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 @@ -1638,8 +1657,11 @@ set(regress_1_tests regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue5738-dt-interp-finite.smt2 regress1/fmf/issue6690-re-enum.smt2 + regress1/fmf/issue6744-2-unc-bool-var.smt2 + regress1/fmf/issue6744-3-unc-bool-var.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 + regress1/fmf/ko-bound-set.cvc.smt2 regress1/fmf/loopy_coda.smt2 regress1/fmf/lst-no-self-rev-exp.smt2 regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 @@ -1661,6 +1683,7 @@ set(regress_1_tests regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 + regress1/ho/issue5741-3.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -1679,6 +1702,7 @@ set(regress_1_tests regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 + regress1/nl/approx-sqrt-unsat.smt2 regress1/nl/arctan2-expdef.smt2 regress1/nl/arrowsmith-050317.smt2 regress1/nl/bad-050217.smt2 @@ -1707,8 +1731,10 @@ set(regress_1_tests regress1/nl/issue3656.smt2 regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 + regress1/nl/issue3966-conf-coeff.smt2 regress1/nl/issue4791-llr.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 + regress1/nl/issue5660-mb-success.smt2 regress1/nl/issue5662-nl-tc.smt2 regress1/nl/issue5662-nl-tc-min.smt2 regress1/nl/metitarski-1025.smt2 @@ -1752,6 +1778,7 @@ set(regress_1_tests regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 + regress1/proofs/qgu-fuzz-1-strings-pp.smt2 regress1/proofs/quant-alpha-eq.smt2 regress1/proofs/sat-trivial-cycle.smt2 regress1/proofs/unsat-cores-proofs.smt2 @@ -1842,6 +1869,7 @@ set(regress_1_tests regress1/quantifiers/cee-npnt-dd.smt2 regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 + regress1/quantifiers/choice-move-delta-relt.smt2 regress1/quantifiers/const.cvc.smt2 regress1/quantifiers/constfunc.cvc.smt2 regress1/quantifiers/ddatv-delta2.smt2 @@ -1887,6 +1915,7 @@ set(regress_1_tests regress1/quantifiers/issue4849-nqe.smt2 regress1/quantifiers/issue5019-cegqi-i.smt2 regress1/quantifiers/issue5279-nqe.smt2 + regress1/quantifiers/issue5288-vts-real-int.smt2 regress1/quantifiers/issue5365-nqe.smt2 regress1/quantifiers/issue5378-witness.smt2 regress1/quantifiers/issue5469-aext.smt2 @@ -1898,9 +1927,16 @@ set(regress_1_tests regress1/quantifiers/issue5506-qe.smt2 regress1/quantifiers/issue5507-qe.smt2 regress1/quantifiers/issue5658-qe.smt2 + regress1/quantifiers/issue5735-subtypes.smt2 + regress1/quantifiers/issue5735-2-subtypes.smt2 regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 regress1/quantifiers/issue5899-qe.smt2 + regress1/quantifiers/issue6607-witness-te.smt2 + regress1/quantifiers/issue6638-sygus-inst.smt2 + regress1/quantifiers/issue6642-em-types.smt2 regress1/quantifiers/issue6699-nc-shadow.smt2 + regress1/quantifiers/issue6775-vts-int.smt2 + regress1/quantifiers/issue6845-nl-lemma-tc.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -1946,10 +1982,12 @@ set(regress_1_tests regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 regress1/quantifiers/qs-has-term.smt2 regress1/quantifiers/recfact.cvc.smt2 + regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 regress1/quantifiers/rew-to-0211-dd.smt2 regress1/quantifiers/ricart-agrawala6.smt2 regress1/quantifiers/set-choice-koikonomou.cvc.smt2 + regress1/quantifiers/set3.smt2 regress1/quantifiers/set8.smt2 regress1/quantifiers/seu169+1.smt2 regress1/quantifiers/seq-solved-enum.smt2 @@ -1960,6 +1998,7 @@ set(regress_1_tests regress1/quantifiers/smtlib46f14a.smt2 regress1/quantifiers/smtlibe99bbe.smt2 regress1/quantifiers/smtlibf957ea.smt2 + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 @@ -2178,6 +2217,7 @@ set(regress_1_tests regress1/strings/issue6101-2.smt2 regress1/strings/issue6132-non-unique-skolem.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 + regress1/strings/issue6184-unsat-core.smt2 regress1/strings/issue6191-replace-all.smt2 regress1/strings/issue6203-1-substr-ctn-strip.smt2 regress1/strings/issue6203-2-re-ccache.smt2 @@ -2194,11 +2234,13 @@ set(regress_1_tests regress1/strings/issue6604-2.smt2 regress1/strings/issue6635-rre.smt2 regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-3-seq.smt2 regress1/strings/issue6653-4-rre.smt2 regress1/strings/issue6653-rre.smt2 regress1/strings/issue6653-rre-small.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 + regress1/strings/issue6973-dup-lemma-conc.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 @@ -2250,6 +2292,7 @@ set(regress_1_tests regress1/strings/rev-ex5.smt2 regress1/strings/rew-020618.smt2 regress1/strings/rew-check1.smt2 + regress1/strings/seq-cardinality.smt2 regress1/strings/seq-quant-infinite-branch.smt2 regress1/strings/simple-re-consume.smt2 regress1/strings/stoi-400million.smt2 @@ -2289,6 +2332,7 @@ set(regress_1_tests regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy + regress1/sygus/array-uc.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/cegar1.sy regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -2523,6 +2567,7 @@ set(regress_2_tests regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 regress2/quantifiers/cee-event-wrong-sat.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2701,16 +2746,12 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # TODO: fix models (projects #276) - regress1/fmf/ko-bound-set.cvc.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/SYO056^1.p - # slow on some builds after changes to tangent planes - regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 # times out after update to tangent planes @@ -2727,12 +2768,6 @@ set(regression_disabled_tests regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build, ok with other builds: regress1/quantifiers/model_6_1_bv.smt2 - # timeout after changes to nonlinear on PR #5351 - regress1/quantifiers/rel-trigger-unusable.smt2 - # does not terminate/takes a long time when doing a coverage build with LFSC. - regress1/quantifiers/set3.smt2 - # changes to expand definitions, related to trigger selection for selectors - regress1/quantifiers/stream-x2014-09-18-unsat.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 @@ -2769,7 +2804,6 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 - regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 index f1aae6bb1..7d5495fcc 100644 --- a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 +++ b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 @@ -1,14 +1,11 @@ ; COMMAND-LINE: -o raw-benchmark -; EXPECT: OPTION "incremental" false; -; EXPECT: OPTION "logic" "ALL"; -; EXPECT: DATATYPE -; EXPECT: nat = succ(pred: nat) | zero -; EXPECT: END; -; EXPECT: x : nat; -; EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x)); +; EXPECT: (set-option :incremental false) +; EXPECT: (set-logic ALL) +; EXPECT: (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero)))) +; EXPECT: (declare-fun x () nat) +; EXPECT: (check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) )) ; EXPECT: sat (set-logic ALL) -(set-option :incremental false) (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero)))) (declare-fun x () nat) (check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) )) diff --git a/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 new file mode 100644 index 000000000..950cb61a9 --- /dev/null +++ b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_DTLIA) +(set-info :status sat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (distinct f (b 0 f))) +(assert (= e f)) +(check-sat) diff --git a/test/regress/regress0/eqrange0.smt2 b/test/regress/regress0/eqrange0.smt2 new file mode 100644 index 000000000..01713d18f --- /dev/null +++ b/test/regress/regress0/eqrange0.smt2 @@ -0,0 +1,6 @@ +; EXPECT: (error "Term of kind EQ_RANGE not supported in default mode, try --arrays-exp") +; EXIT: 1 +(set-logic QF_AUFLIA) +(declare-const a (Array Int Int)) +(assert (eqrange a a 0 0)) +(check-sat) diff --git a/test/regress/regress0/options/interactive-mode.smt2 b/test/regress/regress0/options/interactive-mode.smt2 new file mode 100644 index 000000000..549fdfd24 --- /dev/null +++ b/test/regress/regress0/options/interactive-mode.smt2 @@ -0,0 +1,10 @@ +; EXPECT: true +; EXPECT: true +; EXPECT: false +; EXPECT: false +(set-option :interactive-mode true) +(get-option :interactive-mode) +(get-option :produce-assertions) +(set-option :produce-assertions false) +(get-option :interactive-mode) +(get-option :produce-assertions)
\ No newline at end of file diff --git a/test/regress/regress0/options/stream-printing.smt2 b/test/regress/regress0/options/stream-printing.smt2 new file mode 100644 index 000000000..21ea85aa1 --- /dev/null +++ b/test/regress/regress0/options/stream-printing.smt2 @@ -0,0 +1,18 @@ +; EXPECT: stdout +; EXPECT: stderr +; EXPECT: stdin +; EXPECT-ERROR: stderr +; EXPECT-ERROR: stdout +; EXPECT-ERROR: stdin + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) + +(set-option :regular-output-channel stderr) +(set-option :diagnostic-output-channel stdout) +(set-option :in stdin) + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 new file mode 100644 index 000000000..b6825fe27 --- /dev/null +++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models +; EXPECT: sat +; EXPECT: (((f (as @uc_Foo_0 Foo)) 3)) +(set-logic ALL) +(set-option :produce-models true) +(declare-sort Foo 0) +(declare-fun f (Foo) Int) +(assert (exists ((x Foo)) (= (f x) 3))) +(check-sat) +(get-value ((f @uc_Foo_0))) diff --git a/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 new file mode 100644 index 000000000..9e4bd285c --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-const a Bool) +(declare-const b Bool) +(assert b) +(assert (xor b (not a))) +(check-sat) diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 new file mode 100644 index 000000000..6760bdf4d --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-const x Bool) +(declare-const y Bool) +(declare-const z Bool) +(assert y) +(assert (not z)) +(assert (ite x y z)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 new file mode 100644 index 000000000..fcb26054e --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert c) +(assert (not b)) +(assert (ite a b c)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 new file mode 100644 index 000000000..1765c32f1 --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (not (ite a b c))) +(assert b) +(assert (not c)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 new file mode 100644 index 000000000..b3b19f74b --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (not (ite a b c))) +(assert c) +(assert (not b)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/proofs/qgu-fuzz-1-bool-sat.smt2 b/test/regress/regress0/proofs/qgu-fuzz-1-bool-sat.smt2 new file mode 100644 index 000000000..d9b10e2b9 --- /dev/null +++ b/test/regress/regress0/proofs/qgu-fuzz-1-bool-sat.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic QF_UF) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (and (or d b) (= c d) (not (ite d c false)) (= (or b d) (= b d)))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 b/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 new file mode 100644 index 000000000..c4a9a770f --- /dev/null +++ b/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -i +; EXPECT: sat +(set-logic ALL) +(declare-fun f0_2 (Real Real) Real) +(declare-fun x8 () Real) +(assert (= 0.0 (f0_2 x8 1.0))) +(push) +(assert (= x8 1.0)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 b/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 new file mode 100644 index 000000000..11cc56547 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :macros-quant true) +(declare-sort I_fb 0) +(declare-fun fb_arg_0_1 (I_fb) Int) +(declare-fun name!0 (I_fb) Int) +(assert (forall ((?j I_fb)) (! (= (name!0 ?j) (fb_arg_0_1 ?j)) :qid k!9))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 new file mode 100644 index 000000000..8c9d9eb66 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatype Option (par (T) ((none) (some (extractSome T))))) +(assert + (forall ((x (Option Int))) + (=> (and ((_ is some) x) + (= (extractSome x) 0)) + (= x (some 0))))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/veqt-delta.smt2 b/test/regress/regress0/quantifiers/veqt-delta.smt2 new file mode 100644 index 000000000..dfac015c6 --- /dev/null +++ b/test/regress/regress0/quantifiers/veqt-delta.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL) +(declare-sort S 0) +(declare-fun f () S) +(assert (forall ((? S)) (= ? f))) +(assert (exists ((? S) (v S)) (distinct ? v))) +(check-sat) diff --git a/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 new file mode 100644 index 000000000..732b709f9 --- /dev/null +++ b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic ALIRA) +(declare-const x Real) +(declare-fun i () Int) +(declare-fun i1 () Int) +(push) +(assert (< 1 (- i))) +(check-sat) +(pop) +(push) +(assert (or (>= i1 (* 5 (- i))))) +(check-sat) +(pop) +(assert (or (> i1 1) (= x (to_real i)))) +(check-sat) +(assert (not (is_int x))) +(check-sat) diff --git a/test/regress/regress1/arith/issue7252-arith-sanity.smt2 b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 new file mode 100644 index 000000000..dd7a1fa2e --- /dev/null +++ b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(declare-fun e () Int) +(declare-fun f () Int) +(declare-fun g () Int) +(assert (> 0 (* a (mod 0 b)))) +(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0))) +(check-sat) diff --git a/test/regress/regress1/cores/issue6988-arith-sanity.smt2 b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 new file mode 100644 index 000000000..622d64375 --- /dev/null +++ b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +(set-logic ANIA) +(declare-const x Bool) +(set-option :produce-unsat-cores true) +(declare-fun i () Int) +(declare-fun i5 () Int) +(declare-fun i8 () Int) +(assert (or x (< i5 0))) +(push) +(assert (and (= i8 1) (= i5 (+ 1 i)) (= i8 (+ 1 i)))) +(push) +(check-sat) +(pop) +(pop) +(assert (= i8 (* i8 3 (+ i8 1)))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 index 50373fde4..6f0fb84f2 100644 --- a/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 +++ b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 @@ -1,4 +1,4 @@ -(set-logic UFLIA) +(set-logic UFDTLIA) (set-info :status sat) (set-option :finite-model-find true) (declare-sort a 0) diff --git a/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 new file mode 100644 index 000000000..024d5b6a3 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :finite-model-find true) +(set-info :status sat) +(declare-fun v () Bool) +(declare-fun v2 () Bool) +(assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q))))))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 new file mode 100644 index 000000000..eb0c35f68 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 @@ -0,0 +1,5 @@ +(set-logic UFC) +(set-info :status sat) +(declare-fun v () Bool) +(assert (and (forall ((q Bool)) (not (xor v (exists ((q Bool)) true) (and (not v) (not q))))))) +(check-sat) diff --git a/test/regress/regress1/ho/issue5741-3.smt2 b/test/regress/regress1/ho/issue5741-3.smt2 new file mode 100644 index 000000000..abc4b76a6 --- /dev/null +++ b/test/regress/regress1/ho/issue5741-3.smt2 @@ -0,0 +1,5 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool) +(assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1))))) +(check-sat) diff --git a/test/regress/regress1/nl/approx-sqrt-unsat.smt2 b/test/regress/regress1/nl/approx-sqrt-unsat.smt2 index 576fb1a67..cda24d098 100644 --- a/test/regress/regress1/nl/approx-sqrt-unsat.smt2 +++ b/test/regress/regress1/nl/approx-sqrt-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tplanes +; COMMAND-LINE: --nl-ext-tplanes --no-check-proofs ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress1/nl/issue3966-conf-coeff.smt2 b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 new file mode 100644 index 000000000..7bfbf4140 --- /dev/null +++ b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_UFNIA) +(set-info :status sat) +(set-option :nl-ext-ent-conf true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const i0 Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i9 Int) +(declare-const i10 Int) +(declare-const i12 Int) +(declare-const i13 Int) +(assert v0) +(declare-sort S0 0) +(declare-const v4 Bool) +(assert (xor v2 v1 (> i12 i2) (and v3 v3) (> i12 i2) v4 v2 v1 v0 v3)) +(assert (xor (<= 52 (div 15 (- i1 84 i0 99 i5))) v4 (=> v4 (>= i5 88)) (> i12 i2) (and v3 v3) (<= 52 (div 15 (- i1 84 i0 99 i5))) v1 (> i12 i2) (distinct i0 615) v0)) +(check-sat) diff --git a/test/regress/regress1/nl/issue5660-mb-success.smt2 b/test/regress/regress1/nl/issue5660-mb-success.smt2 new file mode 100644 index 000000000..6284b0580 --- /dev/null +++ b/test/regress/regress1/nl/issue5660-mb-success.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFNRA) +(set-info :status sat) +(declare-fun r2 () Real) +(declare-fun r9 () Real) +(declare-fun r13 () Real) +(declare-fun ufrb5 (Real Real Real Real Real) Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun arr0 () (Array Bool Real)) +(declare-fun arr1 () (Array Bool (Array Bool Real))) +(declare-fun v5 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(declare-fun v71 () Bool) +(declare-fun v81 () Bool) +(declare-fun v161 () Bool) +(assert (or v161 (and v3 (not v7)))) +(assert (or v8 (distinct v7 (and v7 v81) (ufrb5 0.0 1.0 0.0 1.0 (/ r13 r9))))) +(assert (or v161 (distinct v71 v8 (= v4 v81)))) +(assert (or v81 (= arr0 (store (select (store arr1 (xor v81 (and (= r2 1.0) (= r13 1))) arr0) v7) v81 (select (store arr0 v5 1.0) false))))) +(check-sat) diff --git a/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 new file mode 100644 index 000000000..c0c1f16f7 --- /dev/null +++ b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(assert (let ((_let_1 (str.to_re "B"))) (and (str.in_re x (re.++ re.allchar (str.to_re (str.++ "B" "A")))) (str.in_re x (re.* (re.union re.allchar (str.to_re "A")))) (str.in_re x (re.* (re.union re.allchar _let_1))) (str.in_re x (re.* (re.++ re.allchar _let_1)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 new file mode 100644 index 000000000..a8fd0d498 --- /dev/null +++ b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --relational-triggers --user-pat=use +; EXPECT: unsat +(set-logic ALL) +(declare-fun F (Int) Bool) +(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 b/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 new file mode 100644 index 000000000..b36b8cc94 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(assert + (forall ((a Int) (b Int)) + (or (< a (/ 3 b (- 2))) + (forall ((c Int)) (or (<= c b) (>= c a)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 b/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 new file mode 100644 index 000000000..76a58bdb7 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(set-info :status unsat) +(assert (forall ((a Real)) (exists ((b Int)) (= (exists ((c Int)) (<= a c (+ a 1))) (and (>= b (/ a (+ a 1))) (< 1 (+ a 1))))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 b/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 new file mode 100644 index 000000000..300819007 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Bool) +(assert (forall ((b Int) (c Bool) (d Int)) +(or (= d (/ 1 (ite c 9 0))) (<= (ite a 1 b) (/ 1 (ite c 9 0)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 new file mode 100644 index 000000000..ff426c139 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-info :status sat) +(assert (exists ((skoY Real)) (forall ((skoX Real)) (or (= 0.0 (* skoY skoY)) (and (< skoY 0.0) (or (= skoY skoX) (= 2 (* skoY skoY)))))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 new file mode 100644 index 000000000..b7cc50885 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --sygus-inst --no-check-models +; EXPECT: sat +(set-logic ALL) +(declare-fun b (Int) Int) +(assert (distinct 0 (ite (exists ((t Int)) (and (forall ((tt Int) (t Int)) (! (or (distinct 0 tt) (> 0 (+ tt t)) (> (+ tt t) 0) (= (b 0) (b t))) :qid k!7)))) 1 (b 0)))) +(check-sat) + +; check-models disabled due to intermediate terms from sygus-inst diff --git a/test/regress/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/regress1/quantifiers/issue6642-em-types.smt2 new file mode 100644 index 000000000..19dc11227 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6642-em-types.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic ALL) +(declare-fun b () String) +(assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 new file mode 100644 index 000000000..39b92a6ad --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: -i --no-check-models +; EXPECT: sat +; EXPECT: sat +(set-logic NIA) +(declare-const x43799 Bool) +(declare-const x32 Bool) +(declare-fun v11 () Bool) +(declare-fun i2 () Int) +(declare-fun i3 () Int) +(declare-fun i () Int) +(assert (or (< 0 i2) (not x32) (not v11))) +(assert (or x32 (exists ((q Int)) (not (= x32 (> q (abs i3))))))) +(assert (< i2 i)) +(check-sat) +(assert (or (not v11) x43799)) +(assert (= (+ 3 i (* 13 4 5 (abs i3))) (* 157 4 (- 1) (+ 1 1 i2 i)))) +(check-sat) + +; check-models disabled due to intermediate terms from sygus-inst diff --git a/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 new file mode 100644 index 000000000..087137653 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: -i +; EXPECT: sat +; EXPECT: sat +(set-logic NIRA) +(declare-const x Bool) +(declare-fun i () Int) +(declare-fun i1 () Int) +(assert (< 1.0 (to_real i))) +(assert (distinct 0 (/ 7 (to_real i)))) +(push) +(assert (or (exists ((q Int)) (= 0 (* i i1))))) +(check-sat) +(pop) +(assert (or (= i1 1) x)) +(check-sat) diff --git a/test/regress/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/regress1/strings/issue6184-unsat-core.smt2 new file mode 100644 index 000000000..6673dc3b9 --- /dev/null +++ b/test/regress/regress1/strings/issue6184-unsat-core.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(set-option :check-unsat-cores true) +(declare-fun i8 () Int) +(declare-fun st6 () (Set String)) +(declare-fun st8 () (Set String)) +(declare-fun str6 () String) +(declare-fun str7 () String) +(assert (= 0 (card st8))) +(assert (str.in_re str6 (re.opt re.none))) +(assert (str.in_re (str.substr str7 0 i8) re.allchar)) +(assert (xor true (subset st8 st6) (not (= str7 str6)) true)) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-3-seq.smt2 b/test/regress/regress1/strings/issue6653-3-seq.smt2 new file mode 100644 index 000000000..a48fc7664 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-3-seq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(declare-fun z () Int) +(declare-fun a () (Seq Int)) +(assert (not (= (seq.nth a 1) (seq.nth a z)))) +(assert (= z (- 1))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 new file mode 100644 index 000000000..4c6fe5c62 --- /dev/null +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun a () String) +(assert + (str.in_re "" + (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all))) + (str.to_re + (ite + (str.in_re "" + (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a "")) + (re.inter (str.to_re a) + (re.++ (str.to_re a) + (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all)))))) + a ""))))) +(check-sat) diff --git a/test/regress/regress1/strings/seq-cardinality.smt2 b/test/regress/regress1/strings/seq-cardinality.smt2 new file mode 100644 index 000000000..93a4985d4 --- /dev/null +++ b/test/regress/regress1/strings/seq-cardinality.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () (Seq (_ BitVec 1))) +(declare-fun y () (Seq (_ BitVec 1))) +(declare-fun z () (Seq (_ BitVec 1))) + +(assert (= (seq.len x) 1)) +(assert (= (seq.len y) 1)) +(assert (= (seq.len z) 1)) +(assert (distinct x y z)) +(check-sat) diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy new file mode 100644 index 000000000..b3d950436 --- /dev/null +++ b/test/regress/regress1/sygus/array-uc.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(synth-fun f ((x (Array U Int)) (y U)) Bool) + +(declare-var x (Array U Int)) +(declare-var y U) + +(constraint (= (f (store x y 0) y) true)) +(constraint (= (f (store x y 1) y) false)) + +; f can be (= (select x y) 0) +(check-synth) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 32ba6f6c2..edb45e4bd 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -11,36 +11,332 @@ # directory for licensing information. # ############################################################################# ## - """ Runs benchmark and checks for correct exit status and output. """ import argparse +import collections import difflib import os import re import shlex import subprocess import sys +import tempfile import threading class Color: - BLUE = '\033[94m' - GREEN = '\033[92m' - YELLOW = '\033[93m' - RED = '\033[91m' - ENDC = '\033[0m' + BLUE = "\033[94m" + GREEN = "\033[92m" + YELLOW = "\033[93m" + RED = "\033[91m" + ENDC = "\033[0m" + +class Tester: + def __init__(self): + pass -SCRUBBER = 'SCRUBBER:' -ERROR_SCRUBBER = 'ERROR-SCRUBBER:' -EXPECT = 'EXPECT:' -EXPECT_ERROR = 'EXPECT-ERROR:' -EXIT = 'EXIT:' -COMMAND_LINE = 'COMMAND-LINE:' -REQUIRES = 'REQUIRES:' + def applies(self, benchmark_info): + return True + + def run(self, benchmark_info): + exit_code = EXIT_OK + output, error, exit_status = run_benchmark(benchmark_info) + if exit_status == STATUS_TIMEOUT: + exit_code = EXIT_SKIP if skip_timeout else EXIT_FAILURE + print("Timeout - Flags: {}".format(command_line_args)) + elif output != benchmark_info.expected_output: + exit_code = EXIT_FAILURE + print("not ok - Flags: {}".format(benchmark_info.command_line_args)) + print() + print("Standard output difference") + print("=" * 80) + print_diff(output, benchmark_info.expected_output) + print("=" * 80) + print() + print() + if error: + print("Error output") + print("=" * 80) + print_colored(Color.YELLOW, error) + print("=" * 80) + print() + elif error != benchmark_info.expected_error: + exit_code = EXIT_FAILURE + print( + "not ok - Differences between expected and actual output on stderr - Flags: {}".format( + benchmark_info.command_line_args + ) + ) + print() + print("Error output difference") + print("=" * 80) + print_diff(error, benchmark_info.expected_error) + print("=" * 80) + print() + elif exit_status != benchmark_info.expected_exit_status: + exit_code = EXIT_FAILURE + print( + 'not ok - Expected exit status "{}" but got "{}" - Flags: {}'.format( + benchmark_info.expected_exit_status, + exit_status, + benchmark_info.command_line_args, + ) + ) + print() + print("Output:") + print("=" * 80) + print_colored(Color.BLUE, output) + print("=" * 80) + print() + print() + print("Error output:") + print("=" * 80) + print_colored(Color.YELLOW, error) + print("=" * 80) + print() + else: + print("ok - Flags: {}".format(benchmark_info.command_line_args)) + return exit_code + + +################################################################################ +# The testers +# +# Testers use `Tester` as a base class and implement `applies()` and `run()` +# methods. The `applies()` method returns `True` if a tester applies to a given +# benchmark and `run()` runs the actual test. Most testers can invoke the +# `run()` method in the base class, which calls the cvc5 binary with a set of +# arguments and checks the expected output (both stdout and stderr) as well as +# the exit status. +# +# To add a new tester, add a class and add it to the `g_tester` dictionary. +################################################################################ + + +class BaseTester(Tester): + def __init__(self): + pass + + def run(self, benchmark_info): + return super().run(benchmark_info) + + +class UnsatCoreTester(Tester): + def __init__(self): + pass + + def applies(self, benchmark_info): + return ( + benchmark_info.benchmark_ext != ".sy" + and ( + "unsat" in benchmark_info.expected_output.split() + or "entailed" in benchmark_info.expected_output.split() + ) + and "--no-produce-unsat-cores" not in benchmark_info.command_line_args + and "--no-check-unsat-cores" not in benchmark_info.command_line_args + and "--check-unsat-cores" not in benchmark_info.command_line_args + and "sygus-inference" not in benchmark_info.benchmark_content + and "--unconstrained-simp" not in benchmark_info.command_line_args + ) + + def run(self, benchmark_info): + return super().run( + benchmark_info._replace( + command_line_args=benchmark_info.command_line_args + + ["--check-unsat-cores"] + ) + ) + + +class ProofTester(Tester): + def __init__(self): + pass + + def applies(self, benchmark_info): + expected_output_lines = benchmark_info.expected_output.split() + return ( + benchmark_info.benchmark_ext != ".sy" + and ( + "unsat" in benchmark_info.expected_output.split() + or "entailed" in benchmark_info.expected_output.split() + ) + and "--no-produce-proofs" not in benchmark_info.command_line_args + and "--no-check-proofs" not in benchmark_info.command_line_args + and "--check-proofs" not in benchmark_info.command_line_args + ) + + def run(self, benchmark_info): + return super().run( + benchmark_info._replace( + command_line_args=benchmark_info.command_line_args + ["--check-proofs"] + ) + ) + + +class ModelTester(Tester): + def __init__(self): + pass + + def applies(self, benchmark_info): + expected_output_lines = benchmark_info.expected_output.split() + return ( + benchmark_info.benchmark_ext != ".sy" + and ("sat" in expected_output_lines or "unknown" in expected_output_lines) + and "--no-debug-check-models" not in benchmark_info.command_line_args + and "--no-check-models" not in benchmark_info.command_line_args + and "--debug-check-models" not in benchmark_info.command_line_args + ) + + def run(self, benchmark_info): + return super().run( + benchmark_info._replace( + command_line_args=benchmark_info.command_line_args + + ["--debug-check-models"] + ) + ) + + +class SynthTester(Tester): + def __init__(self): + pass + + def applies(self, benchmark_info): + return ( + benchmark_info.benchmark_ext == ".sy" + and "--no-check-synth-sol" not in benchmark_info.command_line_args + and "--sygus-rr" not in benchmark_info.command_line_args + and "--check-synth-sol" not in benchmark_info.command_line_args + ) + + def run(self, benchmark_info): + return super().run( + benchmark_info._replace( + command_line_args=benchmark_info.command_line_args + + ["--check-synth-sol"] + ) + ) + + +class AbductTester(Tester): + def __init__(self): + pass + + def applies(self, benchmark_info): + return ( + benchmark_info.benchmark_ext != ".sy" + and "--no-check-abducts" not in benchmark_info.command_line_args + and "--check-abducts" not in benchmark_info.command_line_args + and "get-abduct" in benchmark_info.benchmark_content + ) + + def run(self, benchmark_info): + return super().run( + benchmark_info._replace( + command_line_args=benchmark_info.command_line_args + ["--check-abducts"] + ) + ) + + +class DumpTester(Tester): + def applies(self, benchmark_info): + return benchmark_info.expected_exit_status == EXIT_OK + + def run(self, benchmark_info): + ext_to_lang = { + ".smt2": "smt2", + ".p": "tptp", + ".sy": "sygus", + } + + tmpf_name = None + with tempfile.NamedTemporaryFile(delete=False) as tmpf: + dump_args = [ + "--parse-only", + "-o", + "raw-benchmark", + f"--output-lang={ext_to_lang[benchmark_info.benchmark_ext]}", + ] + dump_output, _, _ = run_process( + [benchmark_info.cvc5_binary] + + benchmark_info.command_line_args + + dump_args + + [benchmark_info.benchmark_basename], + benchmark_info.benchmark_dir, + benchmark_info.timeout, + ) + + tmpf_name = tmpf.name + tmpf.write(dump_output) + + if not tmpf_name: + return EXIT_FAILURE + + exit_code = super().run( + benchmark_info._replace( + command_line_args=benchmark_info.command_line_args + + [ + "--parse-only", + f"--lang={ext_to_lang[benchmark_info.benchmark_ext]}", + ], + benchmark_basename=tmpf.name, + expected_output="", + ) + ) + os.remove(tmpf.name) + return exit_code + + +g_testers = { + "base": BaseTester(), + "unsat-core": UnsatCoreTester(), + "proof": ProofTester(), + "model": ModelTester(), + "synth": SynthTester(), + "abduct": AbductTester(), + "dump": DumpTester(), +} + +g_default_testers = [ + "base", + "unsat-core", + "proof", + "model", + "synth", + "abduct", +] + +################################################################################ + +BenchmarkInfo = collections.namedtuple( + "BenchmarkInfo", + [ + "wrapper", + "scrubber", + "error_scrubber", + "timeout", + "cvc5_binary", + "benchmark_dir", + "benchmark_basename", + "benchmark_ext", + "benchmark_content", + "expected_output", + "expected_error", + "expected_exit_status", + "command_line_args", + ], +) + +SCRUBBER = "SCRUBBER:" +ERROR_SCRUBBER = "ERROR-SCRUBBER:" +EXPECT = "EXPECT:" +EXPECT_ERROR = "EXPECT-ERROR:" +EXIT = "EXIT:" +COMMAND_LINE = "COMMAND-LINE:" +REQUIRES = "REQUIRES:" EXIT_OK = 0 EXIT_FAILURE = 1 @@ -58,14 +354,12 @@ def print_colored(color, text): def print_diff(actual, expected): """Prints the difference between `actual` and `expected`.""" - for line in difflib.unified_diff(expected.splitlines(), - actual.splitlines(), - 'expected', - 'actual', - lineterm=''): - if line.startswith('+'): + for line in difflib.unified_diff( + expected.splitlines(), actual.splitlines(), "expected", "actual", lineterm="" + ): + if line.startswith("+"): print_colored(Color.GREEN, line) - elif line.startswith('-'): + elif line.startswith("-"): print_colored(Color.RED, line) else: print(line) @@ -78,14 +372,16 @@ def run_process(args, cwd, timeout, s_input=None): output and the exit code of the process. If the process times out, the output and the error output are empty and the exit code is 124.""" - proc = subprocess.Popen(args, - cwd=cwd, - stdin=subprocess.PIPE, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE) + proc = subprocess.Popen( + args, + cwd=cwd, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) - out = '' - err = '' + out = "" + err = "" exit_status = STATUS_TIMEOUT try: if timeout: @@ -106,61 +402,60 @@ def run_process(args, cwd, timeout, s_input=None): def get_cvc5_features(cvc5_binary): """Returns a list of features supported by the cvc5 binary `cvc5_binary`.""" - output, _, _ = run_process([cvc5_binary, '--show-config'], None, None) + output, _, _ = run_process([cvc5_binary, "--show-config"], None, None) if isinstance(output, bytes): output = output.decode() features = [] disabled_features = [] - for line in output.split('\n'): - tokens = [t.strip() for t in line.split(':')] + for line in output.split("\n"): + tokens = [t.strip() for t in line.split(":")] if len(tokens) == 2: key, value = tokens - if value == 'yes': + if value == "yes": features.append(key) - elif value == 'no': + elif value == "no": disabled_features.append(key) return features, disabled_features -def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary, - command_line, benchmark_dir, benchmark_filename, timeout): - """Runs cvc5 on the file `benchmark_filename` in the directory - `benchmark_dir` using the binary `cvc5_binary` with the command line - options `command_line`. The output is scrubbed using `scrubber` and - `error_scrubber` for stdout and stderr, respectively. If dump is true, the - function first uses cvc5 to read in and dump the benchmark file and then - uses that as input.""" +def run_benchmark(benchmark_info): + """Runs cvc5 on a benchmark with the given `benchmark_info`. It runs on the + file `benchmark_basename` in the directory `benchmark_dir` using the binary + `cvc5_binary` with the command line options `command_line_args`. The output + is scrubbed using `scrubber` and `error_scrubber` for stdout and stderr, + respectively.""" - bin_args = wrapper[:] - bin_args.append(cvc5_binary) + bin_args = benchmark_info.wrapper[:] + bin_args.append(benchmark_info.cvc5_binary) output = None error = None exit_status = None - if dump: - dump_args = [ - '--parse-only', '-o', 'raw-benchmark', '--output-lang=smt2' - ] - dump_output, _, _ = run_process( - bin_args + command_line + dump_args + [benchmark_filename], - benchmark_dir, timeout) - output, error, exit_status = run_process( - bin_args + command_line + ['--lang=smt2', '-'], benchmark_dir, - timeout, dump_output) - else: - output, error, exit_status = run_process( - bin_args + command_line + [benchmark_filename], benchmark_dir, - timeout) + output, error, exit_status = run_process( + bin_args + + benchmark_info.command_line_args + + [benchmark_info.benchmark_basename], + benchmark_info.benchmark_dir, + benchmark_info.timeout, + ) # If a scrubber command has been specified then apply it to the output. - if scrubber: - output, _, _ = run_process(shlex.split(scrubber), benchmark_dir, - timeout, output) - if error_scrubber: - error, _, _ = run_process(shlex.split(error_scrubber), benchmark_dir, - timeout, error) + if benchmark_info.scrubber: + output, _, _ = run_process( + shlex.split(benchmark_info.scrubber), + benchmark_info.benchmark_dir, + benchmark_info.timeout, + output, + ) + if benchmark_info.error_scrubber: + error, _, _ = run_process( + shlex.split(benchmark_info.error_scrubber), + benchmark_info.benchmark_dir, + benchmark_info.timeout, + error, + ) # Popen in Python 3 returns a bytes object instead of a string for # stdout/stderr. @@ -168,22 +463,28 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary, output = output.decode() if isinstance(error, bytes): error = error.decode() - return (output.strip(), error.strip(), exit_status) - - -def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, - skip_timeout, wrapper, cvc5_binary, benchmark_path, - timeout): - """Determines the expected output for a benchmark, runs cvc5 on it and then - checks whether the output corresponds to the expected output. Optionally - uses a wrapper `wrapper`, tests unsat cores (if check_unsat_cores is true), - checks proofs (if check_proofs is true), or dumps a benchmark and uses that as - the input (if dump is true). `use_skip_return_code` enables/disables - returning 77 when a test is skipped.""" + output = re.sub(r"^[ \t]*", "", output.strip(), flags=re.MULTILINE) + error = re.sub(r"^[ \t]*", "", error.strip(), flags=re.MULTILINE) + return (output, error, exit_status) + + +def run_regression( + testers, + use_skip_return_code, + skip_timeout, + wrapper, + cvc5_binary, + benchmark_path, + timeout, +): + """Determines the expected output for a benchmark, runs cvc5 on it using + all the specified `testers` and then checks whether the output corresponds + to the expected output. Optionally uses a wrapper `wrapper`. + `use_skip_return_code` enables/disables returning 77 when a test is + skipped.""" if not os.access(cvc5_binary, os.X_OK): - sys.exit( - '"{}" does not exist or is not executable'.format(cvc5_binary)) + sys.exit('"{}" does not exist or is not executable'.format(cvc5_binary)) if not os.path.isfile(benchmark_path): sys.exit('"{}" does not exist or is not a file'.format(benchmark_path)) @@ -194,38 +495,34 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, benchmark_basename = os.path.basename(benchmark_path) benchmark_filename, benchmark_ext = os.path.splitext(benchmark_basename) benchmark_dir = os.path.dirname(benchmark_path) - comment_char = '%' + comment_char = "%" status_regex = None status_to_output = lambda s: s - if benchmark_ext == '.smt': - status_regex = r':status\s*(sat|unsat)' - comment_char = ';' - elif benchmark_ext == '.smt2': - status_regex = r'set-info\s*:status\s*(sat|unsat)' - comment_char = ';' - elif benchmark_ext == '.p': - status_regex = r'% Status\s*:\s*(Theorem|Unsatisfiable|CounterSatisfiable|Satisfiable)' - status_to_output = lambda s: '% SZS status {} for {}'.format( - s, benchmark_filename) - elif benchmark_ext == '.sy': - comment_char = ';' - # Do not check proofs/unsat-cores with .sy files - check_unsat_cores = False - check_proofs = False + if benchmark_ext == ".smt2": + status_regex = r"set-info\s*:status\s*(sat|unsat)" + comment_char = ";" + elif benchmark_ext == ".p": + status_regex = ( + r"% Status\s*:\s*(Theorem|Unsatisfiable|CounterSatisfiable|Satisfiable)" + ) + status_to_output = lambda s: "% SZS status {} for {}".format( + s, benchmark_filename + ) + elif benchmark_ext == ".sy": + comment_char = ";" else: - sys.exit('"{}" must be *.smt2 or *.p or *.sy'.format( - benchmark_basename)) + sys.exit('"{}" must be *.smt2 or *.p or *.sy'.format(benchmark_basename)) benchmark_lines = None - with open(benchmark_path, 'r') as benchmark_file: + with open(benchmark_path, "r") as benchmark_file: benchmark_lines = benchmark_file.readlines() - benchmark_content = ''.join(benchmark_lines) + benchmark_content = "".join(benchmark_lines) # Extract the metadata for the benchmark. scrubber = None error_scrubber = None - expected_output = '' - expected_error = '' + expected_output = "" + expected_error = "" expected_exit_status = None command_lines = [] requires = [] @@ -236,31 +533,31 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, line = line[1:].lstrip() if line.startswith(SCRUBBER): - scrubber = line[len(SCRUBBER):].strip() + scrubber = line[len(SCRUBBER) :].strip() elif line.startswith(ERROR_SCRUBBER): - error_scrubber = line[len(ERROR_SCRUBBER):].strip() + error_scrubber = line[len(ERROR_SCRUBBER) :].strip() elif line.startswith(EXPECT): - expected_output += line[len(EXPECT):].strip() + '\n' + expected_output += line[len(EXPECT) :].strip() + "\n" elif line.startswith(EXPECT_ERROR): - expected_error += line[len(EXPECT_ERROR):].strip() + '\n' + expected_error += line[len(EXPECT_ERROR) :].strip() + "\n" elif line.startswith(EXIT): - expected_exit_status = int(line[len(EXIT):].strip()) + expected_exit_status = int(line[len(EXIT) :].strip()) elif line.startswith(COMMAND_LINE): - command_lines.append(line[len(COMMAND_LINE):].strip()) + command_lines.append(line[len(COMMAND_LINE) :].strip()) elif line.startswith(REQUIRES): - requires.append(line[len(REQUIRES):].strip()) + requires.append(line[len(REQUIRES) :].strip()) expected_output = expected_output.strip() expected_error = expected_error.strip() # Expected output/expected error has not been defined in the metadata for # the benchmark. Try to extract the information from the benchmark itself. - if expected_output == '' and expected_error == '': + if expected_output == "" and expected_error == "": match = None if status_regex: match = re.findall(status_regex, benchmark_content) if match: - expected_output = status_to_output('\n'.join(match)) + expected_output = status_to_output("\n".join(match)) elif expected_exit_status is None: # If there is no expected output/error and the exit status has not # been set explicitly, the benchmark is invalid. @@ -268,156 +565,77 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, if expected_exit_status is None: expected_exit_status = 0 - if 'CVC5_REGRESSION_ARGS' in os.environ: - basic_command_line_args += shlex.split( - os.environ['CVC5_REGRESSION_ARGS']) - - if not check_unsat_cores and ('(get-unsat-core)' in benchmark_content - or '(get-unsat-assumptions)' in benchmark_content): - print( - '1..0 # Skipped regression: unsat cores not supported without proof support' - ) - return (EXIT_SKIP if use_skip_return_code else EXIT_OK) + if "CVC5_REGRESSION_ARGS" in os.environ: + basic_command_line_args += shlex.split(os.environ["CVC5_REGRESSION_ARGS"]) for req_feature in requires: is_negative = False if req_feature.startswith("no-"): - req_feature = req_feature[len("no-"):] + req_feature = req_feature[len("no-") :] is_negative = True if req_feature not in (cvc5_features + cvc5_disabled_features): print( - 'Illegal requirement in regression: {}\nAllowed requirements: {}' - .format(req_feature, - ' '.join(cvc5_features + cvc5_disabled_features))) + "Illegal requirement in regression: {}\nAllowed requirements: {}".format( + req_feature, " ".join(cvc5_features + cvc5_disabled_features) + ) + ) return EXIT_FAILURE if is_negative: if req_feature in cvc5_features: - print('1..0 # Skipped regression: not valid with {}'.format( - req_feature)) - return (EXIT_SKIP if use_skip_return_code else EXIT_OK) + print( + "1..0 # Skipped regression: not valid with {}".format(req_feature) + ) + return EXIT_SKIP if use_skip_return_code else EXIT_OK elif req_feature not in cvc5_features: - print('1..0 # Skipped regression: {} not supported'.format( - req_feature)) - return (EXIT_SKIP if use_skip_return_code else EXIT_OK) + print("1..0 # Skipped regression: {} not supported".format(req_feature)) + return EXIT_SKIP if use_skip_return_code else EXIT_OK if not command_lines: - command_lines.append('') + command_lines.append("") + tests = [] + expected_output_lines = expected_output.split() command_line_args_configs = [] for command_line in command_lines: args = shlex.split(command_line) all_args = basic_command_line_args + args - if not check_unsat_cores and ('--check-unsat-cores' in all_args): - print( - '# Skipped command line options ({}): unsat cores not supported without proof support' - .format(all_args)) - continue - if not check_proofs and '--dump-proofs' in all_args: - print( - '# Skipped command line options ({}): proof production not supported' - .format(all_args)) - continue - command_line_args_configs.append(all_args) - expected_output_lines = expected_output.split() - extra_command_line_args = [] - if benchmark_ext == '.sy' and \ - '--no-check-synth-sol' not in all_args and \ - '--sygus-rr' not in all_args and \ - '--check-synth-sol' not in all_args: - all_args += ['--check-synth-sol'] - if ('sat' in expected_output_lines or \ - 'unknown' in expected_output_lines) and \ - '--no-debug-check-models' not in all_args and \ - '--no-check-models' not in all_args and \ - '--debug-check-models' not in all_args: - extra_command_line_args += ['--debug-check-models'] - if 'unsat' in expected_output_lines in expected_output_lines: - if check_unsat_cores and \ - '--no-produce-unsat-cores' not in all_args and \ - '--no-check-unsat-cores' not in all_args and \ - '--check-unsat-cores' not in all_args and \ - 'sygus-inference' not in benchmark_content and \ - '--unconstrained-simp' not in all_args: - extra_command_line_args += ['--check-unsat-cores'] - if check_proofs and \ - '--no-produce-proofs' not in all_args and \ - '--no-check-proofs' not in all_args and \ - '--check-proofs' not in all_args: - extra_command_line_args += ['--check-proofs'] - if '--no-check-abducts' not in all_args and \ - '--check-abducts' not in all_args and \ - 'get-abduct' in benchmark_content: - all_args += ['--check-abducts'] - - # Create a test case for each extra argument - for extra_arg in extra_command_line_args: - command_line_args_configs.append(all_args + [extra_arg]) - - # Run cvc5 on the benchmark with the different option sets and check - # whether the exit status, stdout output, stderr output are as expected. - print('1..{}'.format(len(command_line_args_configs))) - print('# Starting') + benchmark_info = BenchmarkInfo( + wrapper=wrapper, + scrubber=scrubber, + error_scrubber=error_scrubber, + timeout=timeout, + cvc5_binary=cvc5_binary, + benchmark_dir=benchmark_dir, + benchmark_basename=benchmark_basename, + benchmark_ext=benchmark_ext, + benchmark_content=benchmark_content, + expected_output=expected_output, + expected_error=expected_error, + expected_exit_status=expected_exit_status, + command_line_args=all_args, + ) + for tester_name, tester in g_testers.items(): + if tester_name in testers and tester.applies(benchmark_info): + tests.append((tester, benchmark_info)) + + if len(tests) == 0: + print("1..0 # Skipped regression: no tests to run") + return EXIT_SKIP if use_skip_return_code else EXIT_OK + + print("1..{}".format(len(tests))) + print("# Starting") + # Run cvc5 on the benchmark with the different testers and check whether + # the exit status, stdout output, stderr output are as expected. exit_code = EXIT_OK - for command_line_args in command_line_args_configs: - output, error, exit_status = run_benchmark(dump, wrapper, scrubber, - error_scrubber, cvc5_binary, - command_line_args, - benchmark_dir, - benchmark_basename, timeout) - output = re.sub(r'^[ \t]*', '', output, flags=re.MULTILINE) - error = re.sub(r'^[ \t]*', '', error, flags=re.MULTILINE) - if exit_status == STATUS_TIMEOUT: - exit_code = EXIT_SKIP if skip_timeout else EXIT_FAILURE - print('Timeout - Flags: {}'.format(command_line_args)) - elif output != expected_output: - exit_code = EXIT_FAILURE - print('not ok - Flags: {}'.format(command_line_args)) - print() - print('Standard output difference') - print('=' * 80) - print_diff(output, expected_output) - print('=' * 80) - print() - print() - if error: - print('Error output') - print('=' * 80) - print_colored(Color.YELLOW, error) - print('=' * 80) - print() - elif error != expected_error: - exit_code = EXIT_FAILURE - print( - 'not ok - Differences between expected and actual output on stderr - Flags: {}' - .format(command_line_args)) - print() - print('Error output difference') - print('=' * 80) - print_diff(error, expected_error) - print('=' * 80) - print() - elif expected_exit_status != exit_status: + for tester, benchmark_info in tests: + test_exit_code = tester.run(benchmark_info) + if exit_code == EXIT_FAILURE or test_exit_code == EXIT_FAILURE: exit_code = EXIT_FAILURE - print( - 'not ok - Expected exit status "{}" but got "{}" - Flags: {}'. - format(expected_exit_status, exit_status, command_line_args)) - print() - print('Output:') - print('=' * 80) - print_colored(Color.BLUE, output) - print('=' * 80) - print() - print() - print('Error output:') - print('=' * 80) - print_colored(Color.YELLOW, error) - print('=' * 80) - print() else: - print('ok - Flags: {}'.format(command_line_args)) + exit_code = test_exit_code return exit_code @@ -427,40 +645,43 @@ def main(): script.""" parser = argparse.ArgumentParser( - description= - 'Runs benchmark and checks for correct exit status and output.') - parser.add_argument('--dump', action='store_true') - parser.add_argument('--use-skip-return-code', action='store_true') - parser.add_argument('--skip-timeout', action='store_true') - parser.add_argument('--check-unsat-cores', action='store_true', - default=True) - parser.add_argument('--no-check-unsat-cores', dest='check_unsat_cores', - action='store_false') - parser.add_argument('--check-proofs', action='store_true', default=True) - parser.add_argument('--no-check-proofs', dest='check_proofs', - action='store_false') - parser.add_argument('wrapper', nargs='*') - parser.add_argument('cvc5_binary') - parser.add_argument('benchmark') + description="Runs benchmark and checks for correct exit status and output." + ) + parser.add_argument("--use-skip-return-code", action="store_true") + parser.add_argument("--skip-timeout", action="store_true") + parser.add_argument("--tester", choices=g_testers.keys(), action="append") + parser.add_argument("wrapper", nargs="*") + parser.add_argument("cvc5_binary") + parser.add_argument("benchmark") argv = sys.argv[1:] # Append options passed via RUN_REGRESSION_ARGS to argv - if os.environ.get('RUN_REGRESSION_ARGS'): - argv.extend(shlex.split(os.getenv('RUN_REGRESSION_ARGS'))) + if os.environ.get("RUN_REGRESSION_ARGS"): + argv.extend(shlex.split(os.getenv("RUN_REGRESSION_ARGS"))) args = parser.parse_args(argv) cvc5_binary = os.path.abspath(args.cvc5_binary) wrapper = args.wrapper - if os.environ.get('VALGRIND') == '1' and not wrapper: - wrapper = ['libtool', '--mode=execute', 'valgrind'] - - timeout = float(os.getenv('TEST_TIMEOUT', '600')) - - return run_regression(args.check_unsat_cores, args.check_proofs, args.dump, - args.use_skip_return_code, args.skip_timeout, - wrapper, cvc5_binary, args.benchmark, timeout) + if os.environ.get("VALGRIND") == "1" and not wrapper: + wrapper = ["libtool", "--mode=execute", "valgrind"] + + timeout = float(os.getenv("TEST_TIMEOUT", "600")) + + testers = args.tester + if not testers: + testers = g_default_testers + + return run_regression( + testers, + args.use_skip_return_code, + args.skip_timeout, + wrapper, + cvc5_binary, + args.benchmark, + timeout, + ) if __name__ == "__main__": diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index d153b8a91..971be58cc 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -19,11 +19,11 @@ import static cvc5.Kind.*; import static cvc5.RoundingMode.*; import static org.junit.jupiter.api.Assertions.*; +import java.math.BigInteger; import java.util.*; import java.util.concurrent.atomic.AtomicReference; -import org.junit.jupiter.api.AfterEach; -import org.junit.jupiter.api.BeforeEach; -import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.*; +import org.junit.jupiter.api.function.Executable; class SolverTest { @@ -623,6 +623,11 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } + @Test void mkSepEmp() + { + assertDoesNotThrow(() -> d_solver.mkSepEmp()); + } + @Test void mkSepNil() { assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -1341,6 +1346,75 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getOption("asdf")); } + @Test void getOptionNames() + { + String[] names = d_solver.getOptionNames(); + assertTrue(names.length > 100); + assertTrue(Arrays.asList(names).contains("verbose")); + assertFalse(Arrays.asList(names).contains("foobar")); + } + + @Test void getOptionInfo() + { + List<Executable> assertions = new ArrayList<>(); + { + assertions.add( + () -> assertThrows(CVC5ApiException.class, () -> d_solver.getOptionInfo("asdf-invalid"))); + } + { + OptionInfo info = d_solver.getOptionInfo("verbose"); + assertions.add(() -> assertEquals("verbose", info.getName())); + assertions.add( + () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases()))); + assertions.add(() -> assertTrue(info.getBaseInfo() instanceof OptionInfo.VoidInfo)); + } + { + // int64 type with default + OptionInfo info = d_solver.getOptionInfo("verbosity"); + assertions.add(() -> assertEquals("verbosity", info.getName())); + assertions.add( + () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases()))); + assertions.add( + () -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class)); + OptionInfo.NumberInfo<BigInteger> numInfo = + (OptionInfo.NumberInfo<BigInteger>) info.getBaseInfo(); + assertions.add(() -> assertEquals(0, numInfo.getDefaultValue().intValue())); + assertions.add(() -> assertEquals(0, numInfo.getCurrentValue().intValue())); + assertions.add( + () -> assertFalse(numInfo.getMinimum() != null || numInfo.getMaximum() != null)); + assertions.add(() -> assertEquals(info.intValue().intValue(), 0)); + } + assertAll(assertions); + { + OptionInfo info = d_solver.getOptionInfo("random-freq"); + assertEquals(info.getName(), "random-freq"); + assertEquals( + Arrays.asList(info.getAliases()), Arrays.asList(new String[] {"random-frequency"})); + assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class); + OptionInfo.NumberInfo<Double> ni = (OptionInfo.NumberInfo<Double>) info.getBaseInfo(); + assertEquals(ni.getCurrentValue(), 0.0); + assertEquals(ni.getDefaultValue(), 0.0); + assertTrue(ni.getMinimum() != null && ni.getMaximum() != null); + assertEquals(ni.getMinimum(), 0.0); + assertEquals(ni.getMaximum(), 1.0); + assertEquals(info.doubleValue(), 0.0); + } + { + // mode option + OptionInfo info = d_solver.getOptionInfo("output"); + assertions.clear(); + assertions.add(() -> assertEquals("output", info.getName())); + assertions.add( + () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases()))); + assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class)); + OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo(); + assertions.add(() -> assertEquals("NONE", modeInfo.getDefaultValue())); + assertions.add(() -> assertEquals("OutputTag::NONE", modeInfo.getCurrentValue())); + assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("NONE"))); + } + assertAll(assertions); + } + @Test void getUnsatAssumptions1() { d_solver.setOption("incremental", "false"); @@ -1383,17 +1457,17 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore()); } - @Test void getUnsatCore3() + @Test void getUnsatCoreAndProof() { d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-cores", "true"); + d_solver.setOption("produce-proofs", "true"); Sort uSort = d_solver.mkUninterpretedSort("u"); Sort intSort = d_solver.getIntegerSort(); Sort boolSort = d_solver.getBooleanSort(); Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort); Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort); - Term[] unsat_core; Term x = d_solver.mkConst(uSort, "x"); Term y = d_solver.mkConst(uSort, "y"); @@ -1401,21 +1475,21 @@ class SolverTest Term p = d_solver.mkConst(intPredSort, "p"); Term zero = d_solver.mkInteger(0); Term one = d_solver.mkInteger(1); - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + Term f_x = d_solver.mkTerm(Kind.APPLY_UF, f, x); + Term f_y = d_solver.mkTerm(Kind.APPLY_UF, f, y); + Term sum = d_solver.mkTerm(Kind.PLUS, f_x, f_y); + Term p_0 = d_solver.mkTerm(Kind.APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); - d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x)); - d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_y)); - d_solver.assertFormula(d_solver.mkTerm(GT, sum, one)); + d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_x)); + d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_y)); + d_solver.assertFormula(d_solver.mkTerm(Kind.GT, sum, one)); d_solver.assertFormula(p_0); d_solver.assertFormula(p_f_y.notTerm()); assertTrue(d_solver.checkSat().isUnsat()); - AtomicReference<Term[]> atomic = new AtomicReference<>(); - assertDoesNotThrow(() -> atomic.set(d_solver.getUnsatCore())); - unsat_core = atomic.get(); + Term[] unsat_core = d_solver.getUnsatCore(); + + assertDoesNotThrow(() -> d_solver.getProof()); d_solver.resetAssertions(); for (Term t : unsat_core) @@ -1424,6 +1498,42 @@ class SolverTest } Result res = d_solver.checkSat(); assertTrue(res.isUnsat()); + assertDoesNotThrow(() -> d_solver.getProof()); + } + + @Test void getDifficulty() + { + d_solver.setOption("produce-difficulty", "true"); + // cannot ask before a check sat + assertThrows(CVC5ApiException.class, () -> d_solver.getDifficulty()); + d_solver.checkSat(); + assertDoesNotThrow(() -> d_solver.getDifficulty()); + } + + @Test void getDifficulty2() + { + d_solver.checkSat(); + // option is not set + assertThrows(CVC5ApiException.class, () -> d_solver.getDifficulty()); + } + + @Test void getDifficulty3() throws CVC5ApiException + { + d_solver.setOption("produce-difficulty", "true"); + Sort intSort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(intSort, "x"); + Term zero = d_solver.mkInteger(0); + Term ten = d_solver.mkInteger(10); + Term f0 = d_solver.mkTerm(GEQ, x, ten); + Term f1 = d_solver.mkTerm(GEQ, zero, x); + d_solver.checkSat(); + Map<Term, Term> dmap = d_solver.getDifficulty(); + // difficulty should map assertions to integer values + for (Map.Entry<Term, Term> t : dmap.entrySet()) + { + assertTrue(t.getKey() == f0 || t.getKey() == f1); + assertTrue(t.getValue().getKind() == Kind.CONST_RATIONAL); + } } @Test void getValue1() @@ -1483,6 +1593,95 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> slv.getValue(x)); } + @Test void getModelDomainElements() + { + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Sort intSort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + Term z = d_solver.mkConst(uSort, "z"); + Term f = d_solver.mkTerm(DISTINCT, x, y, z); + d_solver.assertFormula(f); + d_solver.checkSat(); + assertDoesNotThrow(() -> d_solver.getModelDomainElements(uSort)); + assertTrue(d_solver.getModelDomainElements(uSort).length >= 3); + assertThrows(CVC5ApiException.class, () -> d_solver.getModelDomainElements(intSort)); + } + + @Test void getModelDomainElements2() + { + d_solver.setOption("produce-models", "true"); + d_solver.setOption("finite-model-find", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(uSort, "x"); + Term y = d_solver.mkVar(uSort, "y"); + Term eq = d_solver.mkTerm(EQUAL, x, y); + Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y); + Term f = d_solver.mkTerm(FORALL, bvl, eq); + d_solver.assertFormula(f); + d_solver.checkSat(); + assertDoesNotThrow(() -> d_solver.getModelDomainElements(uSort)); + // a model for the above must interpret u as size 1 + assertTrue(d_solver.getModelDomainElements(uSort).length == 1); + } + + @Test void isModelCoreSymbol() + { + d_solver.setOption("produce-models", "true"); + d_solver.setOption("model-cores", "simple"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + Term z = d_solver.mkConst(uSort, "z"); + Term zero = d_solver.mkInteger(0); + Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y)); + d_solver.assertFormula(f); + d_solver.checkSat(); + assertTrue(d_solver.isModelCoreSymbol(x)); + assertTrue(d_solver.isModelCoreSymbol(y)); + assertFalse(d_solver.isModelCoreSymbol(z)); + assertThrows(CVC5ApiException.class, () -> d_solver.isModelCoreSymbol(zero)); + } + + @Test void getModel() + { + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + Term z = d_solver.mkConst(uSort, "z"); + Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y)); + d_solver.assertFormula(f); + d_solver.checkSat(); + Sort[] sorts = new Sort[] {uSort}; + Term[] terms = new Term[] {x, y}; + assertDoesNotThrow(() -> d_solver.getModel(sorts, terms)); + Term nullTerm = d_solver.getNullTerm(); + Term[] terms2 = new Term[] {x, y, nullTerm}; + assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms2)); + } + + @Test void getModel2() + { + d_solver.setOption("produce-models", "true"); + Sort[] sorts = new Sort[] {}; + Term[] terms = new Term[] {}; + assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms)); + } + + @Test void getModel3() + { + d_solver.setOption("produce-models", "true"); + Sort[] sorts = new Sort[] {}; + final Term[] terms = new Term[] {}; + d_solver.checkSat(); + assertDoesNotThrow(() -> d_solver.getModel(sorts, terms)); + Sort integer = d_solver.getIntegerSort(); + Sort[] sorts2 = new Sort[] {integer}; + assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts2, terms)); + } + @Test void getQuantifierElimination() { Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); @@ -2180,6 +2379,20 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm)); } + @Test void addSygusAssume() + { + Term nullTerm = d_solver.getNullTerm(); + Term boolTerm = d_solver.mkBoolean(false); + Term intTerm = d_solver.mkInteger(1); + + assertDoesNotThrow(() -> d_solver.addSygusAssume(boolTerm)); + assertThrows(CVC5ApiException.class, () -> d_solver.addSygusAssume(nullTerm)); + assertThrows(CVC5ApiException.class, () -> d_solver.addSygusAssume(intTerm)); + + Solver slv = new Solver(); + assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm)); + } + @Test void addSygusInvConstraint() throws CVC5ApiException { Sort bool = d_solver.getBooleanSort(); @@ -2342,4 +2555,4 @@ class SolverTest + "\"Z\")))", projection.toString()); } -}
\ No newline at end of file +} diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java index f2f9edaed..1ea703268 100644 --- a/test/unit/api/java/cvc5/SortTest.java +++ b/test/unit/api/java/cvc5/SortTest.java @@ -458,28 +458,28 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity()); } - @Test void getBVSize() throws CVC5ApiException + @Test void getBitVectorSize() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); - assertDoesNotThrow(() -> bvSort.getBVSize()); + assertDoesNotThrow(() -> bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getBVSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize()); } - @Test void getFPExponentSize() throws CVC5ApiException + @Test void getFloatingPointExponentSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPExponentSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize()); } - @Test void getFPSignificandSize() throws CVC5ApiException + @Test void getFloatingPointSignificandSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPSignificandSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize()); } @Test void getDatatypeParamSorts() throws CVC5ApiException diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..8dcb0fde6 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,15 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkAbstractValue) { ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); @@ -419,6 +410,17 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint) ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException); } +TEST_F(TestApiBlackSolver, mkCardinalityConstraint) +{ + Sort su = d_solver.mkUninterpretedSort("u"); + Sort si = d_solver.getIntegerSort(); + ASSERT_NO_THROW(d_solver.mkCardinalityConstraint(su, 3)); + ASSERT_THROW(d_solver.mkCardinalityConstraint(si, 3), CVC5ApiException); + ASSERT_THROW(d_solver.mkCardinalityConstraint(su, 0), CVC5ApiException); + Solver slv; + ASSERT_THROW(slv.mkCardinalityConstraint(su, 3), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, mkEmptySet) { Solver slv; @@ -606,6 +608,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } +TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } + TEST_F(TestApiBlackSolver, mkSepNil) { ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -1234,6 +1238,23 @@ TEST_F(TestApiBlackSolver, getAbduct) ASSERT_EQ(output2, truen); } +TEST_F(TestApiBlackSolver, getAbduct2) +{ + d_solver.setLogic("QF_LIA"); + d_solver.setOption("incremental", "false"); + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + // Assumptions for abduction: x > 0 + d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + // Conjecture for abduction: y > 0 + Term conj = d_solver.mkTerm(GT, y, zero); + Term output; + // Fails due to option not set + ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); @@ -2536,5 +2557,21 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } + +TEST_F(TestApiBlackSolver, issue7000) +{ + Sort s1 = d_solver.getIntegerSort(); + Sort s2 = d_solver.mkFunctionSort(s1, s1); + Sort s3 = d_solver.getRealSort(); + Term t4 = d_solver.mkPi(); + Term t7 = d_solver.mkConst(s3, "_x5"); + Term t37 = d_solver.mkConst(s2, "_x32"); + Term t59 = d_solver.mkConst(s2, "_x51"); + Term t72 = d_solver.mkTerm(EQUAL, t37, t59); + Term t74 = d_solver.mkTerm(GT, t4, t7); + // throws logic exception since logic is not higher order by default + ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException); +} + } // namespace test } // namespace cvc5 diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 757bacad6..d0c755cf7 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -61,6 +61,14 @@ TEST_F(TestApiBlackSort, operators_comparison) ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort()); } +TEST_F(TestApiBlackSort, isNull) +{ + Sort x; + ASSERT_TRUE(x.isNull()); + x = d_solver.getBooleanSort(); + ASSERT_FALSE(x.isNull()); +} + TEST_F(TestApiBlackSort, isBoolean) { ASSERT_TRUE(d_solver.getBooleanSort().isBoolean()); @@ -470,28 +478,28 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getBVSize) +TEST_F(TestApiBlackSort, getBitVectorSize) { Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_NO_THROW(bvSort.getBVSize()); + ASSERT_NO_THROW(bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getBVSize(), CVC5ApiException); + ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPExponentSize) +TEST_F(TestApiBlackSort, getFloatingPointExponentSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPExponentSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointExponentSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPSignificandSize) +TEST_F(TestApiBlackSort, getFloatingPointSignificandSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPSignificandSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeParamSorts) |