From acdffc72bd559fa4b64da2ee2b3373208354e7a1 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 30 Nov 2020 18:42:19 -0800 Subject: fix metadata for a test (#5546) A COMMAND was used instead of COMMAND-LINE. --- test/regress/regress0/bv/bv_to_int_5281.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2 index 4d0da1dbb..dc2cb7f35 100644 --- a/test/regress/regress0/bv/bv_to_int_5281.smt2 +++ b/test/regress/regress0/bv/bv_to_int_5281.smt2 @@ -1,4 +1,4 @@ -; COMMAND: --check-models --incremental +; COMMAND-LINE: --check-models --incremental ; EXPECT: sat (set-logic ALL) (set-option :check-models true) -- cgit v1.2.3 From 6489cf590b441aeb5e1bdf9800c9718d06842149 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 22:22:24 -0600 Subject: More fixes for quantifier elimination (#5533) Fixes #5506, fixes #5507. --- src/smt/quant_elim_solver.cpp | 14 ++++++++++++-- src/smt/quant_elim_solver.h | 13 ++++++++++++- src/smt/smt_engine.cpp | 3 ++- src/theory/quantifiers_engine.cpp | 2 ++ test/regress/CMakeLists.txt | 2 ++ test/regress/regress1/quantifiers/issue5506-qe.smt2 | 6 ++++++ test/regress/regress1/quantifiers/issue5507-qe.smt2 | 19 +++++++++++++++++++ 7 files changed, 55 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5506-qe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5507-qe.smt2 (limited to 'test') diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e5ecafd4a..4636cf17a 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -14,6 +14,7 @@ #include "smt/quant_elim_solver.h" +#include "expr/skolem_manager.h" #include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/cegqi/nested_qe.h" @@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {} Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, - bool doFull) + bool doFull, + bool isInternalSubsolver) { Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) @@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, throw ModalException( "Expecting a quantified formula as argument to get-qe."); } + NodeManager* nm = NodeManager::currentNM(); + // ensure the body is rewritten + q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary q = quantifiers::NestedQe::doNestedQe(q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " << q << std::endl; - NodeManager* nm = NodeManager::currentNM(); // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); @@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // do extended rewrite to minimize the size of the formula aggressively theory::quantifiers::ExtendedRewriter extr(true); ret = extr.extendedRewrite(ret); + // if we are not an internal subsolver, convert to witness form, since + // internally generated skolems should not escape + if (!isInternalSubsolver) + { + ret = SkolemManager::getWitnessForm(ret); + } return ret; } // otherwise, just true/false diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 96ed1f73d..ca55fc618 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -79,8 +79,19 @@ class QuantElimSolver * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. + * + * @param as The assertions of the SmtEngine + * @param q The quantified formula we are eliminating quantifiers from + * @param doFull Whether we are doing full quantifier elimination on q + * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * internal subsolver. If it is not, then we convert the final result to + * witness form. + * @return The result of eliminating quantifiers from q. */ - Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + Node getQuantifierElimination(Assertions& as, + Node q, + bool doFull, + bool isInternalSubsolver); private: /** The SMT solver, which is used during doQuantifierElimination. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 722f6a080..d3ba676fc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1498,7 +1498,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); } bool SmtEngine::getInterpol(const Node& conj, diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 297f11690..da9fdd022 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; + d_lemmas_waiting.clear(); + d_phase_req_waiting.clear(); for( unsigned i=0; ipresolve(); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 816202fa9..4445a28d0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1622,6 +1622,8 @@ set(regress_1_tests regress1/quantifiers/issue5482-rtf-no-fv.smt2 regress1/quantifiers/issue5484-qe.smt2 regress1/quantifiers/issue5484b-qe.smt2 + regress1/quantifiers/issue5506-qe.smt2 + regress1/quantifiers/issue5507-qe.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2 new file mode 100644 index 000000000..3839f2d75 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2 @@ -0,0 +1,6 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(get-qe (forall ((b Int)) (= a 0))) diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2 new file mode 100644 index 000000000..3b7ddbcf3 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2 @@ -0,0 +1,19 @@ +; EXPECT: false +; EXIT: 0 +(set-logic LIA) +(declare-fun v0 () Bool) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v9 () Bool) +(declare-fun v10 () Bool) +(declare-fun v15 () Bool) +(declare-fun v16 () Bool) +(declare-fun i0 () Int) +(declare-fun i2 () Int) +(declare-fun i9 () Int) +(declare-fun v26 () Bool) +(declare-fun v33 () Bool) +(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0))) -- cgit v1.2.3 From d452621ef035a0127d691618e85a4fa2ab6fa027 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 15:03:50 +0100 Subject: Add regressions for #4707. (#5555) The error from #4707 has been fixed in the meantime, this PR adds the example inputs as regressions. Closes #4707. --- test/regress/CMakeLists.txt | 2 + .../regress0/issue4707-bv-to-bool-small.smt2 | 13 +++ .../regress2/issue4707-bv-to-bool-large.smt2 | 129 +++++++++++++++++++++ 3 files changed, 144 insertions(+) create mode 100644 test/regress/regress0/issue4707-bv-to-bool-small.smt2 create mode 100644 test/regress/regress2/issue4707-bv-to-bool-large.smt2 (limited to 'test') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4445a28d0..9662ea094 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -584,6 +584,7 @@ set(regress_0_tests regress0/issue2832-qualId.smt2 regress0/issue4010-sort-inf-var.smt2 regress0/issue4469-unc-no-reuse-var.smt2 + regress0/issue4707-bv-to-bool-small.smt2 regress0/issue5144-resetAssertions.smt2 regress0/ite.cvc regress0/ite2.smt2 @@ -2169,6 +2170,7 @@ set(regress_2_tests regress2/hole7.cvc regress2/hole8.cvc regress2/instance_1444.smtv1.smt2 + regress2/issue4707-bv-to-bool-large.smt2 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 regress2/javafe.ast.WhileStmt.447_no_forall.smt2 regress2/ooo.rf6.smt2 diff --git a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 b/test/regress/regress0/issue4707-bv-to-bool-small.smt2 new file mode 100644 index 000000000..c2f0a58ad --- /dev/null +++ b/test/regress/regress0/issue4707-bv-to-bool-small.smt2 @@ -0,0 +1,13 @@ +; EXPECT: sat +(set-logic ALL) +(declare-fun b () (Array (_ BitVec 10) (_ BitVec 1))) +(declare-fun c () (Array (_ BitVec 10) (_ BitVec 1))) +(declare-fun ae () (_ BitVec 10)) +(declare-fun ag () (_ BitVec 10)) +(declare-fun ak () (_ BitVec 10)) +(assert (= (_ bv1 1) (bvand (bvcomp ae ((_ zero_extend 9) (select b (_ bv0 + 10)))) (bvsdiv (bvcomp ae ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (bvshl ((_ + zero_extend 9) (select c (bvadd ae (_ bv3 10)))) (_ bv8 10)))) (_ bv1 1) (_ + bv0 1)) (ite (= b (store (store c (bvadd ae (_ bv3 10)) ((_ extract 0 0) + (bvlshr ag (_ bv8 10)))) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1))))))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress2/issue4707-bv-to-bool-large.smt2 b/test/regress/regress2/issue4707-bv-to-bool-large.smt2 new file mode 100644 index 000000000..bb4e9794c --- /dev/null +++ b/test/regress/regress2/issue4707-bv-to-bool-large.smt2 @@ -0,0 +1,129 @@ +; EXPECT: sat +(set-logic ALL) +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun aa () (_ BitVec 1)) +(declare-fun e () (_ BitVec 1)) +(declare-fun f () (_ BitVec 1)) +(declare-fun ab () (_ BitVec 1)) +(declare-fun g () (_ BitVec 1)) +(declare-fun h () (_ BitVec 1)) +(declare-fun i () (_ BitVec 1)) +(declare-fun j () (_ BitVec 1)) +(declare-fun k () (_ BitVec 1)) +(declare-fun l () (_ BitVec 1)) +(declare-fun m () (_ BitVec 1)) +(declare-fun n () (_ BitVec 1)) +(declare-fun o () (_ BitVec 1)) +(declare-fun p () (_ BitVec 1)) +(declare-fun q () (_ BitVec 1)) +(declare-fun r () (_ BitVec 1)) +(declare-fun s () (_ BitVec 1)) +(declare-fun t () (_ BitVec 1)) +(declare-fun u () (_ BitVec 1)) +(declare-fun v () (_ BitVec 1)) +(declare-fun w () (_ BitVec 1)) +(declare-fun x () (_ BitVec 1)) +(declare-fun y () (_ BitVec 1)) +(declare-fun z () (_ BitVec 1)) +(declare-fun ac () (_ BitVec 1)) +(declare-fun ad () (_ BitVec 32)) +(declare-fun ae () (_ BitVec 32)) +(declare-fun af () (_ BitVec 32)) +(declare-fun ag () (_ BitVec 32)) +(declare-fun ah () (_ BitVec 32)) +(declare-fun ai () (_ BitVec 32)) +(declare-fun aj () (_ BitVec 32)) +(declare-fun ak () (_ BitVec 32)) +(declare-fun al () (_ BitVec 32)) +(declare-fun am () (_ BitVec 32)) +(declare-fun an () (_ BitVec 32)) +(declare-fun ao () (_ BitVec 1)) +(declare-fun ap () (_ BitVec 32)) +(declare-fun aq () (_ BitVec 1)) +(declare-fun ar () (_ BitVec 32)) +(declare-fun au () (_ BitVec 32)) +(declare-fun av () (_ BitVec 32)) +(declare-fun aw () (_ BitVec 32)) +(declare-fun ax () (_ BitVec 32)) +(declare-fun ay () (_ BitVec 32)) +(assert + (let ((?as (bvadd av (_ bv4 32))) + (?at (bvadd av (_ bv12 32)))) + (= (_ bv1 1) (bvand (bvand (ite (= ac (ite (= an ai) (_ bv1 1) (_ + bv0 1))) (_ bv1 1) (_ bv0 1)) (bvmul (ite (= z (ite (= ai aj) (_ + bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= y (ite (= aj + (bvor (bvnand (bvor (concat (_ bv0 24) (select d (bvadd ak (_ bv0 + 32)))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv1 32)))) + (_ bv8 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv2 + 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak + (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= x (ite (= ak ?as) (_ bv1 1) (_ bv0 1))) (_ bv1 + 1) (_ bv0 1)) (bvand (ite (= w (ite (= d (store (store (store + (store c (bvadd (_ bv134533664 32) (_ bv3 32)) ((_ extract 7 0) + (bvlshr al (_ bv24 32)))) (bvadd (_ bv134533664 32) (_ bv2 32)) ((_ + extract 7 0) (bvlshr al (_ bv16 32)))) (bvadd (_ bv134533664 32) (_ + bv1 32)) ((_ extract 7 0) (bvlshr al (_ bv8 32)))) (bvadd (_ + bv134533664 32) (_ bv0 32)) ((_ extract 7 0) al))) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= v (ite (= al (bvor (bvor + (bvor (concat (_ bv0 24) (select c (bvadd am (_ bv0 32)))) (bvshl + (concat (_ bv0 24) (select c (bvadd am (_ bv1 32)))) (_ bv8 32))) + (bvshl (concat (_ bv0 24) (select c (bvadd am (_ bv2 32)))) (_ bv16 + 32))) (bvshl (concat (_ bv0 24) (select c (bvsub am (_ bv3 32)))) + (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand + (ite (= u (ite (= am ?at) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= t ao) (_ bv1 1) (_ bv0 1)) (bvand (ite (= s (ite + (= an ad) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= + r (ite (= ad ae) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand + (ite (= q (ite (= ae (bvor (bvor (bvor (concat (_ bv0 24) (select b + (bvadd af (_ bv0 32)))) (bvxor (concat (_ bv0 24) (select b (bvadd + af (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select b + (bvadd af (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) + (select b (bvadd af (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvsdiv (ite (= p (ite (= af ?as) (_ bv1 + 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= o (ite (= b + (store (store (store (store c (bvadd ar (_ bv3 32)) ((_ extract 7 + 0) (bvlshr ag (_ bv24 32)))) (bvadd ar (_ bv2 32)) ((_ extract 7 0) + (bvlshr ag (_ bv16 32)))) (bvand ar (_ bv1 32)) ((_ extract 7 0) + (bvlshr ag (_ bv8 32)))) (bvadd ar (_ bv0 32)) ((_ extract 7 0) + ag))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= n + (ite (= ag (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd ah + (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select c (bvadd ah (_ bv1 + 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvurem ah + (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c + (bvadd ah (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 + 1) (_ bv0 1)) (bvand (ite (= m (ite (= ah ?at) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= l ao ) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= k (bvor (bvand t (bvand u (bvand v (bvand w + (bvand x (bvand y (bvand z ac))))))) (bvand l (bvand m (bvand n + (bvand o (bvand p (bvand q (bvand r s))))))))) (_ bv1 1) (_ bv0 1)) + (bvand (ite (= j (ite (= ao ((_ extract 0 0) ap)) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= i (ite (= ap (concat (_ + bv0 31) aq)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite + (= h (ite (= aq (ite (= ar (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 + 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= g (ite (= ar + (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd au (_ bv0 + 32)))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv1 32)))) + (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv2 + 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au + (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= ab (ite (= au (bvadd av (_ bv8 32))) (_ bv1 1) + (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= f (ite (= c (store + (store (store (store a (bvadd av (_ bv3 32)) ((_ extract 7 0) + (bvlshr ay (_ bv24 32)))) (bvadd av (_ bv2 32)) ((_ extract 7 0) + (bvlshr ay (_ bv16 32)))) (bvadd av (_ bv1 32)) ((_ extract 7 0) + (bvlshr ay (_ bv8 32)))) (bvadd av (_ bv0 32)) ((_ extract 7 0) + ay))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= e + (ite (= av (bvsub ax (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) + (_ bv0 1)) (ite (= aa (ite (= aw (bvor (bvor (bvor (concat (_ bv0 + 24) (select a (bvadd ax (_ bv0 32)))) (bvshl (concat (_ bv0 24) + (select a (bvadd ax (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ + bv0 24) (select a (bvadd ax (_ bv2 32)))) (_ bv16 32))) (bvshl + (concat (_ bv0 24) (select a (bvadd ax (_ bv3 32)))) (_ bv24 32)))) + (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))) + (bvand (bvnot (_ bv0 1)) (bvand (bvand aa (bvand e (bvand f (bvand + ab (bvand g (bvand h (bvand i (bvand j k)))))))) (ite (= aw an) (_ + bv1 1) (_ bv0 1)))))))) +(check-sat) \ No newline at end of file -- cgit v1.2.3 From 7fb5354114c7e17260b3ff520decf340734d52fe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 15:36:37 +0100 Subject: Add regression for #4335. (#5554) The error from #4335 has been fixed in the meantime, this PR adds a regression for this issue. Closes #4335. --- test/regress/CMakeLists.txt | 1 + test/regress/regress1/issue4335-unsat-core.smt2 | 187 ++++++++++++++++++++++++ 2 files changed, 188 insertions(+) create mode 100644 test/regress/regress1/issue4335-unsat-core.smt2 (limited to 'test') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9662ea094..6c064833a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1417,6 +1417,7 @@ set(regress_1_tests regress1/issue3970-nl-ext-purify.smt2 regress1/issue3990-sort-inference.smt2 regress1/issue4273-ext-rew-cache.smt2 + regress1/issue4335-unsat-core.smt2 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2 regress1/lemmas/pursuit-safety-8.smtv1.smt2 regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 diff --git a/test/regress/regress1/issue4335-unsat-core.smt2 b/test/regress/regress1/issue4335-unsat-core.smt2 new file mode 100644 index 000000000..11e689515 --- /dev/null +++ b/test/regress/regress1/issue4335-unsat-core.smt2 @@ -0,0 +1,187 @@ +; SCRUBBER: sed -e 's/IP_[0-9]*/IP/' +; EXPECT: unsat +; EXPECT: ( +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: ) +(set-logic ALL) +(set-option :produce-unsat-cores true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const v4 Bool) +(declare-const i1 Int) +(declare-const r1 Real) +(declare-const r2 Real) +(declare-const r3 Real) +(declare-const r7 Real) +(declare-const r10 Real) +(declare-const r14 Real) +(declare-const r16 Real) +(declare-const r17 Real) +(declare-const r18 Real) +(declare-const v5 Bool) +(declare-const r20 Real) +(declare-const arr-5074471134850140881_778238581772319464-0 (Array Bool Int)) +(assert (! (exists ((q0 Int) (q1 Real) (q2 Int)) (not (> (- i1) (select (store arr-5074471134850140881_778238581772319464-0 v0 60) (= v0 v4 v3 v3 v4))))) :named IP_1)) +(assert (! (or (forall ((q0 Int) (q1 Real) (q2 Int)) (=> (>= r20 q1 q1 26271062.0) (<= q2 q2))) (exists ((q0 Int) (q1 Real) (q2 Int)) (=> (>= (- i1) q2) (< q1 q1 5851734.0)))) :named IP_2)) +(declare-const arr-778238581772319464_-3713212254555730767-0 (Array Int (_ BitVec 8))) +(declare-const v6 Bool) +(declare-const v7 Bool) +(declare-const arr--5101604640448673848_-3713212254554648242-0 (Array Real (_ BitVec 9))) +(declare-const arr--3713212254557895817_-5101604640448673848-0 (Array (_ BitVec 10) Real)) +(assert (! (or (distinct (- i1) 35) (not v4) (= v0 v4 v3 v3 v4)) :named IP_3)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (= v0 v4 v3 v3 v4)) :named IP_4)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_5)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (= v0 v4 v3 v3 v4)) :named IP_6)) +(assert (! (or (= v0 v4 v3 v3 v4) v3 (= v0 v4 v3 v3 v4)) :named IP_7)) +(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_8)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) v0) :named IP_9)) +(assert (! (or (< 397 (div (- i1) 60)) v3 (= v0 v4 v3 v3 v4)) :named IP_10)) +(assert (! (or v3 v3 v3) :named IP_11)) +(assert (! (or (is_int 1193124502.0) (not v4) (= v0 v4 v3 v3 v4)) :named IP_12)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_13)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_14)) +(assert (! (or (is_int 1193124502.0) v0 (not v4)) :named IP_15)) +(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_16)) +(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_17)) +(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_18)) +(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_19)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_20)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_21)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_22)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_23)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_24)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_25)) +(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_26)) +(assert (! (or v0 (not v4) (= v0 v4 v3 v3 v4)) :named IP_27)) +(assert (! (or (= v0 v4 v3 v3 v4) v3 v3) :named IP_28)) +(assert (! (or v3 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_29)) +(assert (! (or (is_int 1193124502.0) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_30)) +(assert (! (or (distinct (- i1) 35) (not v4) (distinct (- i1) 35)) :named IP_31)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) v3) :named IP_32)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (not v4)) :named IP_33)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_34)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (< 397 (div (- i1) 60))) :named IP_35)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (not v4)) :named IP_36)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) v0) :named IP_37)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_38)) +(assert (! (or (distinct (- i1) 35) v3 (= v0 v4 v3 v3 v4)) :named IP_39)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_40)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_41)) +(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_42)) +(assert (! (or (not v4) v0 (not v4)) :named IP_43)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) (= v0 v4 v3 v3 v4)) :named IP_44)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_45)) +(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_46)) +(assert (! (or (= v0 v4 v3 v3 v4) v0 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_47)) +(assert (! (or (is_int 1193124502.0) v0 (= v0 v4 v3 v3 v4)) :named IP_48)) +(assert (! (or v0 (< 397 (div (- i1) 60)) v3) :named IP_49)) +(assert (! (or v0 v3 (is_int 1193124502.0)) :named IP_50)) +(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_51)) +(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_52)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_53)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_54)) +(assert (! (or (distinct (- i1) 35) v3 (not v4)) :named IP_55)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_56)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_57)) +(assert (! (or (not v4) v0 (< 397 (div (- i1) 60))) :named IP_58)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_59)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_60)) +(assert (! (or (is_int 1193124502.0) v0 (distinct (- i1) 35)) :named IP_61)) +(assert (! (or (not v4) (< 397 (div (- i1) 60)) v3) :named IP_62)) +(assert (! (or (not v4) (distinct (- i1) 35) v0) :named IP_63)) +(assert (! (or (distinct (- i1) 35) (is_int 1193124502.0) v3) :named IP_64)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_65)) +(assert (! (or (< 397 (div (- i1) 60)) v3 v3) :named IP_66)) +(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_67)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 v3) :named IP_68)) +(assert (! (or (distinct (- i1) 35) (distinct (- i1) 35) v0) :named IP_69)) +(assert (! (or v3 (not v4) (< 397 (div (- i1) 60))) :named IP_70)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_71)) +(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_72)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_73)) +(assert (! (or v0 v0 (is_int 1193124502.0)) :named IP_74)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_75)) +(assert (! (or v3 (not v4) v0) :named IP_76)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_77)) +(assert (! (or v3 (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_78)) +(assert (! (or (is_int 1193124502.0) (not v4) v0) :named IP_79)) +(assert (! (or (not v4) v3 (not v4)) :named IP_80)) +(assert (! (or v3 v0 v0) :named IP_81)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_82)) +(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_83)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0) v0) :named IP_84)) +(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_85)) +(assert (! (or (= v0 v4 v3 v3 v4) v0 (= v0 v4 v3 v3 v4)) :named IP_86)) +(assert (! (or v3 (distinct (- i1) 35) (not v4)) :named IP_87)) +(assert (! (or (distinct (- i1) 35) v0 (not v4)) :named IP_88)) +(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_89)) +(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (not v4)) :named IP_90)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_91)) +(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_92)) +(assert (! (or v0 (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_93)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_94)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_95)) +(assert (! (or v3 (not v4) (is_int 1193124502.0)) :named IP_96)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_97)) +(assert (! (or (= v0 v4 v3 v3 v4) v3 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_98)) +(assert (! (or (distinct (- i1) 35) (distinct v4 (= v0 v4 v3 v3 v4)) v3) :named IP_99)) +(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_100)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_101)) +(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_102)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_103)) +(assert (! (or (not v4) (not v4) (= v0 v4 v3 v3 v4)) :named IP_104)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_105)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (is_int 1193124502.0)) :named IP_106)) +(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_107)) +(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_108)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_109)) +(assert (! (or (= v0 v4 v3 v3 v4) v0 (not v4)) :named IP_110)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_111)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct (- i1) 35)) :named IP_112)) +(assert (! (or v0 (not v4) (< 397 (div (- i1) 60))) :named IP_113)) +(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_114)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_115)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_116)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_117)) +(assert (! (or v0 (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_118)) +(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_119)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_120)) +(assert (! (or v3 v3 v3) :named IP_121)) +(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) v3) :named IP_122)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_123)) +(assert (! (or (not v4) (= v0 v4 v3 v3 v4) v3) :named IP_124)) +(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_125)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_126)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_127)) +(assert (! (or (is_int 1193124502.0) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_128)) +(assert (! (or v0 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_129)) +(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_130)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_131)) +(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_132)) +(assert (! (or v0 (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4)) :named IP_133)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60))) :named IP_134)) +(assert (! (or v0 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_135)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_136)) +(assert (! (or v3 (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60))) :named IP_137)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_138)) +(assert (! (or v3 (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_139)) +(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) v3) :named IP_140)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) v0) :named IP_141)) +(assert (! (or (< 397 (div (- i1) 60)) (not v4) v3) :named IP_142)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_143)) +(assert (! (or v3 (is_int 1193124502.0) v3) :named IP_144)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (< 397 (div (- i1) 60))) :named IP_145)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) v3) :named IP_146)) +(check-sat-assuming (IP_107 IP_133)) +(get-unsat-core) +(exit) \ No newline at end of file -- cgit v1.2.3 From 75359f120b1cdfa77add48ef11c776f530783c31 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 16:08:07 +0100 Subject: Add regressions from #5099 (#5557) The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions. Closes #5099. --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/issue5099-model-1.smt2 | 10 ++++++++++ test/regress/regress0/issue5099-model-2.smt2 | 9 +++++++++ 3 files changed, 21 insertions(+) create mode 100644 test/regress/regress0/issue5099-model-1.smt2 create mode 100644 test/regress/regress0/issue5099-model-2.smt2 (limited to 'test') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6c064833a..1a2451147 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -585,6 +585,8 @@ set(regress_0_tests regress0/issue4010-sort-inf-var.smt2 regress0/issue4469-unc-no-reuse-var.smt2 regress0/issue4707-bv-to-bool-small.smt2 + regress0/issue5099-model-1.smt2 + regress0/issue5099-model-2.smt2 regress0/issue5144-resetAssertions.smt2 regress0/ite.cvc regress0/ite2.smt2 diff --git a/test/regress/regress0/issue5099-model-1.smt2 b/test/regress/regress0/issue5099-model-1.smt2 new file mode 100644 index 000000000..dd422ab3b --- /dev/null +++ b/test/regress/regress0/issue5099-model-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -m +; EXPECT: sat +; EXPECT: ((baz true)) +(set-logic QF_NIRA) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (! (or (= a (div 0 b))) :named baz)) +(assert (and (> b 5))) +(check-sat) +(get-assignment) diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2 new file mode 100644 index 000000000..2bd27093f --- /dev/null +++ b/test/regress/regress0/issue5099-model-2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -m +; EXPECT: sat +; EXPECT: ((IP true)) +(set-logic QF_NRA) +(declare-const r11 Real) +(declare-const r16 Real) +(assert (! (distinct (/ 1 r16) r11) :named IP)) +(check-sat) +(get-assignment) \ No newline at end of file -- cgit v1.2.3 From 41554fa3d4a8258bbc842aedad87cd218460ee0a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Dec 2020 08:58:06 -0800 Subject: Improve rewriting of str.<= (#4848) This commit improves our rewriting of str.<= slightly. If we have constant prefixes that are different, we can always rewrite the term to a constant. Previously, we were only doing so when the result was false. --- src/theory/strings/strings_rewriter.cpp | 14 +++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/leq.smt2 | 10 ++++ test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/strings_rewriter_white.h | 89 +++++++++++++++++++++++++++++++ 5 files changed, 107 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/strings/leq.smt2 create mode 100644 test/unit/theory/strings_rewriter_white.h (limited to 'test') diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 932b5c8cc..575c33501 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n) { String s = n1[0].getConst(); String t = n2[0].getConst(); - // only need to truncate if s is longer - if (s.size() > t.size()) + size_t prefixLen = std::min(s.size(), t.size()); + s = s.prefix(prefixLen); + t = t.prefix(prefixLen); + // if the prefixes are not the same, then we can already decide the outcome + if (s != t) { - s = s.prefix(t.size()); - } - // if prefix is not leq, then entire string is not leq - if (!s.isLeq(t)) - { - Node ret = nm->mkConst(false); + Node ret = nm->mkConst(s.isLeq(t)); return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1a2451147..fb8914a36 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1019,6 +1019,7 @@ set(regress_0_tests regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 + regress0/strings/leq.smt2 regress0/strings/loop001.smt2 regress0/strings/loop-wrong-sem.smt2 regress0/strings/model001.smt2 diff --git a/test/regress/regress0/strings/leq.smt2 b/test/regress/regress0/strings/leq.smt2 new file mode 100644 index 000000000..b3bd40739 --- /dev/null +++ b/test/regress/regress0/strings/leq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-const x String) +(declare-const y String) +(assert (or + (not (str.<= (str.++ "A" x) (str.++ "B" y))) + (not (str.<= (str.++ "A" x) (str.++ "BC" y))) + (str.<= (str.++ "A" "D" x) (str.++ "AC" y)))) +(set-info :status unsat) +(check-sat) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 8cfd43989..0eccbf436 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -13,6 +13,7 @@ cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(sequences_rewriter_white theory) +cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_unit_test_white(theory_bags_rewriter_white theory) diff --git a/test/unit/theory/strings_rewriter_white.h b/test/unit/theory/strings_rewriter_white.h new file mode 100644 index 000000000..f5c7cced8 --- /dev/null +++ b/test/unit/theory/strings_rewriter_white.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file strings_rewriter_white.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Unit tests for the strings rewriter + ** + ** Unit tests for the strings rewriter. + **/ + +#include + +#include +#include +#include + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" +#include "theory/strings/strings_rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +class StringsRewriterWhite : public CxxTest::TestSuite +{ + public: + StringsRewriterWhite() {} + + void setUp() override + { + Options opts; + opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); + d_em = new ExprManager; + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); + d_scope = new SmtScope(d_smt); + d_smt->finishInit(); + } + + void tearDown() override + { + delete d_scope; + delete d_smt; + delete d_em; + } + + void testRewriteLeq() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node a = d_nm->mkConst(::CVC4::String("A")); + Node bc = d_nm->mkConst(::CVC4::String("BC")); + Node x = d_nm->mkVar("x", strType); + Node y = d_nm->mkVar("y", strType); + + Node ax = d_nm->mkNode(STRING_CONCAT, a, x); + Node bcy = d_nm->mkNode(STRING_CONCAT, bc, y); + + { + Node leq = d_nm->mkNode(STRING_LEQ, ax, bcy); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(true)); + } + + { + Node leq = d_nm->mkNode(STRING_LEQ, bcy, ax); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(false)); + } + } + + private: + ExprManager* d_em; + SmtEngine* d_smt; + SmtScope* d_scope; + + NodeManager* d_nm; +}; -- cgit v1.2.3 From 798644e64f438f320577a444110744041e39d1ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Dec 2020 18:00:49 -0600 Subject: Fix issues related to model declarations (#5560) This corrects two issues related to model declarations: (1) model declaration terms were mistaken not cleared, (2) the model needs to be explicitly destructed before the node manager because it contains references to Node. Fixes #5540 --- src/smt/model.cpp | 6 +++++- src/smt/smt_engine.cpp | 1 + test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/issue5540-2-dump-model.smt2 | 9 +++++++++ test/regress/regress0/issue5540-model-decls.smt2 | 19 +++++++++++++++++++ 5 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/issue5540-2-dump-model.smt2 create mode 100644 test/regress/regress0/issue5540-model-decls.smt2 (limited to 'test') diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 8a9f944d2..ccf73dda0 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -49,7 +49,11 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } -void Model::clearModelDeclarations() { d_declareSorts.clear(); } +void Model::clearModelDeclarations() +{ + d_declareTerms.clear(); + d_declareSorts.clear(); +} void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3ba676fc..2faad7961 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -332,6 +332,7 @@ SmtEngine::~SmtEngine() d_absValues.reset(nullptr); d_asserts.reset(nullptr); d_dumpm.reset(nullptr); + d_model.reset(nullptr); d_sygusSolver.reset(nullptr); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fb8914a36..fda5c69eb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -588,6 +588,8 @@ set(regress_0_tests regress0/issue5099-model-1.smt2 regress0/issue5099-model-2.smt2 regress0/issue5144-resetAssertions.smt2 + regress0/issue5540-2-dump-model.smt2 + regress0/issue5540-model-decls.smt2 regress0/ite.cvc regress0/ite2.smt2 regress0/ite3.smt2 diff --git a/test/regress/regress0/issue5540-2-dump-model.smt2 b/test/regress/regress0/issue5540-2-dump-model.smt2 new file mode 100644 index 000000000..56d3b2458 --- /dev/null +++ b/test/regress/regress0/issue5540-2-dump-model.smt2 @@ -0,0 +1,9 @@ +; SCRUBBER: sed -e 's/Bool.*$/Bool/' +; COMMAND-LINE: --dump-models +; EXPECT: sat +; EXPECT: ( +; EXPECT: (define-fun v16 () Bool +; EXPECT: ) +(set-logic UFLIA) +(declare-fun v16 () Bool) +(check-sat) diff --git a/test/regress/regress0/issue5540-model-decls.smt2 b/test/regress/regress0/issue5540-model-decls.smt2 new file mode 100644 index 000000000..714159c9f --- /dev/null +++ b/test/regress/regress0/issue5540-model-decls.smt2 @@ -0,0 +1,19 @@ +; SCRUBBER: sed -e 's/Bool.*$/Bool/' +; COMMAND-LINE: --dump-models -i +; EXPECT:sat +; EXPECT: ( +; EXPECT: (define-fun a () Bool +; EXPECT: ) +; EXPECT: sat +; EXPECT: ( +; EXPECT: (define-fun a () Bool +; EXPECT: ) +; EXPECT: sat +; EXPECT: ( +; EXPECT: (define-fun a () Bool +; EXPECT: ) +(set-logic ALL) +(declare-fun a () Bool) +(check-sat) +(check-sat) +(check-sat) -- cgit v1.2.3 From a87df2bb60a8739d4eb24b60efca79f8d2b7d806 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 1 Dec 2020 16:30:33 -0800 Subject: google test: Infrastructure and first api test. (#5548) This sets up the infrastructure for migrating unit tests from CxxTest to Google Test. It further migrates api/datatype_api_black to the new infrastructure. --- .github/workflows/ci.yml | 6 + CMakeLists.txt | 2 +- INSTALL.md | 8 +- test/unit/CMakeLists.txt | 51 ++- test/unit/api/CMakeLists.txt | 12 +- test/unit/api/datatype_api_black.cpp | 540 +++++++++++++++++++++++++++++++ test/unit/api/datatype_api_black.h | 576 --------------------------------- test/unit/base/CMakeLists.txt | 2 +- test/unit/context/CMakeLists.txt | 14 +- test/unit/expr/CMakeLists.txt | 34 +- test/unit/main/CMakeLists.txt | 2 +- test/unit/parser/CMakeLists.txt | 4 +- test/unit/preprocessing/CMakeLists.txt | 2 +- test/unit/printer/CMakeLists.txt | 2 +- test/unit/prop/CMakeLists.txt | 2 +- test/unit/test_api.h | 27 ++ test/unit/theory/CMakeLists.txt | 42 +-- test/unit/util/CMakeLists.txt | 36 +-- 18 files changed, 707 insertions(+), 655 deletions(-) create mode 100644 test/unit/api/datatype_api_black.cpp delete mode 100644 test/unit/api/datatype_api_black.h create mode 100644 test/unit/test_api.h (limited to 'test') diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index acc13c2ee..5da6b4208 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -61,10 +61,12 @@ jobs: run: | sudo apt-get update sudo apt-get install -y \ + build-essential \ ccache \ cxxtest \ libcln-dev \ libgmp-dev \ + libgtest-dev \ libedit-dev \ flex \ libfl-dev \ @@ -72,6 +74,10 @@ jobs: python3 -m pip install toml python3 -m pip install setuptools python3 -m pip install pexpect + cd /usr/src/googletest + sudo cmake . + sudo cmake --build . --target install + cd - echo "/usr/lib/ccache" >> $GITHUB_PATH # Note: macOS comes with a libedit; it does not need to brew-installed diff --git a/CMakeLists.txt b/CMakeLists.txt index 8eab22e4a..6c3ed4bbc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -8,7 +8,7 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cmake_minimum_required(VERSION 3.4) +cmake_minimum_required(VERSION 3.9) #-----------------------------------------------------------------------------# # Project configuration diff --git a/INSTALL.md b/INSTALL.md index b3308726b..5693dbc1c 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -46,7 +46,7 @@ compatible. - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org) or [Clang](https://clang.llvm.org) (reasonably recent versions) -- [CMake >= 3.1](https://cmake.org) +- [CMake >= 3.9](https://cmake.org) - [GNU Bash](https://www.gnu.org/software/bash/) - [Python >= 2.7](https://www.python.org) + module [toml](https://pypi.org/project/toml/) @@ -195,6 +195,12 @@ provided with CVC4. See [Testing CVC4](#Testing-CVC4) below for more details. +### Google Test Unit Testing Framework (Unit Tests) + +[Google Test](https://github.com/google/googletest) is required to optionally +run CVC4's unit tests (included with the distribution). +See [Testing CVC4](#Testing-CVC4) below for more details. + ## Language bindings CVC4 provides a complete and flexible C++ API (see `examples/api` for diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index bb53c15b0..d65e022c9 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -13,6 +13,8 @@ # custom finder modules). set(CxxTest_HOME ${CXXTEST_DIR}) find_package(CxxTest REQUIRED) +find_package(GTest REQUIRED) +include(GoogleTest) include_directories(.) include_directories(${PROJECT_SOURCE_DIR}/src) @@ -35,10 +37,48 @@ set(CVC4_CXXTEST_FLAGS_BLACK -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK}) +# Generate and add unit test. +macro(cvc4_add_unit_test is_white name output_dir) + set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp) + add_executable(${name} ${test_src}) + gtest_add_tests(TARGET ${name}) + target_link_libraries(${name} main-test) + target_link_libraries(${name} GTest::GTest) + target_link_libraries(${name} GTest::Main) + if(USE_LFSC) + # We don't link against LFSC, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR}) + endif() + if(USE_POLY) + # We don't link against libpoly, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) + endif() + if(${is_white}) + target_compile_options(${name} PRIVATE -fno-access-control) + endif() + add_dependencies(build-units ${name}) + # Generate into bin/test/unit/. + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) + set_target_properties(${name} + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) + # The test target is prefixed with test identifier 'unit/' and the path, + # e.g., for '/myunittest.h' + # we create test target 'unit//myunittest' + # and run it with 'ctest -R "example//myunittest"'. + if("${output_dir}" STREQUAL "") + set(test_name unit/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() + add_test(${test_name} ${test_bin_dir}/${name}) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") +endmacro() + # Generate and add unit test. # Note: we do not use cxxtest_add_test from the FindCxxTest module since it # does not allow test names containing '/'. -macro(cvc4_add_unit_test is_white name output_dir) +# !! This macro will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test is_white name output_dir) # generate the test sources set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp) set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h) @@ -110,6 +150,15 @@ macro(cvc4_add_unit_test_white name output_dir) cvc4_add_unit_test(TRUE ${name} ${output_dir}) endmacro() +# !! Will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test_black name output_dir) + cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir}) +endmacro() +# !! Will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test_white name output_dir) + cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir}) +endmacro() + add_subdirectory(api) add_subdirectory(base) add_subdirectory(context) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 1412c7f66..9fcf881a8 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -12,10 +12,10 @@ # Add unit tests cvc4_add_unit_test_black(datatype_api_black api) -cvc4_add_unit_test_black(op_black api) -cvc4_add_unit_test_black(result_black api) -cvc4_add_unit_test_black(solver_black api) -cvc4_add_unit_test_black(sort_black api) -cvc4_add_unit_test_black(term_black api) -cvc4_add_unit_test_black(grammar_black api) +cvc4_add_cxx_unit_test_black(op_black api) +cvc4_add_cxx_unit_test_black(result_black api) +cvc4_add_cxx_unit_test_black(solver_black api) +cvc4_add_cxx_unit_test_black(sort_black api) +cvc4_add_cxx_unit_test_black(term_black api) +cvc4_add_cxx_unit_test_black(grammar_black api) diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp new file mode 100644 index 000000000..f61637221 --- /dev/null +++ b/test/unit/api/datatype_api_black.cpp @@ -0,0 +1,540 @@ +/********************* */ +/*! \file datatype_api_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Aina Niemetz, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the datatype classes of the C++ API. + ** + ** Black box testing of the datatype classes of the C++ API. + **/ + +#include "test_api.h" + +using namespace CVC4::api; + +TEST_F(TestApi, mkDatatypeSort) +{ + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", d_solver.getIntegerSort()); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype d = listSort.getDatatype(); + DatatypeConstructor consConstr = d[0]; + DatatypeConstructor nilConstr = d[1]; + EXPECT_THROW(d[2], CVC4ApiException); + ASSERT_NO_THROW(consConstr.getConstructorTerm()); + ASSERT_NO_THROW(nilConstr.getConstructorTerm()); +} + +TEST_F(TestApi, mkDatatypeSorts) +{ + /* Create two mutual datatypes corresponding to this definition + * block: + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(data: list), + * list = cons(car: tree, cdr: list) | nil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresTree = d_solver.mkUninterpretedSort("tree"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + unresTypes.insert(unresTree); + unresTypes.insert(unresList); + + DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); + DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); + node.addSelector("left", unresTree); + node.addSelector("right", unresTree); + tree.addConstructor(node); + + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + tree.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresTree); + cons.addSelector("cdr", unresTree); + list.addConstructor(cons); + + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + std::vector dtdecls; + dtdecls.push_back(tree); + dtdecls.push_back(list); + std::vector dtsorts; + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), dtdecls.size()); + for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++) + { + ASSERT_TRUE(dtsorts[i].isDatatype()); + EXPECT_FALSE(dtsorts[i].getDatatype().isFinite()); + EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName()); + } + // verify the resolution was correct + Datatype dtTree = dtsorts[0].getDatatype(); + DatatypeConstructor dtcTreeNode = dtTree[0]; + EXPECT_EQ(dtcTreeNode.getName(), "node"); + DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; + EXPECT_EQ(dtsTreeNodeLeft.getName(), "left"); + // argument type should have resolved to be recursive + EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); + EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); + + // fails due to empty datatype + std::vector dtdeclsBad; + DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); + dtdeclsBad.push_back(emptyD); + EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); +} + +TEST_F(TestApi, datatypeStructs) +{ + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); + Sort nullSort; + EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + EXPECT_FALSE(dt.isCodatatype()); + EXPECT_FALSE(dt.isTuple()); + EXPECT_FALSE(dt.isRecord()); + EXPECT_FALSE(dt.isFinite()); + EXPECT_TRUE(dt.isWellFounded()); + // get constructor + DatatypeConstructor dcons = dt[0]; + Term consTerm = dcons.getConstructorTerm(); + EXPECT_EQ(dcons.getNumSelectors(), 2); + + // create datatype sort to test + DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); + DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); + dtypeSpecEnum.addConstructor(ca); + DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); + dtypeSpecEnum.addConstructor(cb); + DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C"); + dtypeSpecEnum.addConstructor(cc); + Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); + Datatype dtEnum = dtypeSortEnum.getDatatype(); + EXPECT_FALSE(dtEnum.isTuple()); + EXPECT_TRUE(dtEnum.isFinite()); + + // create codatatype + DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); + DatatypeConstructorDecl consStream = + d_solver.mkDatatypeConstructorDecl("cons"); + consStream.addSelector("head", intSort); + consStream.addSelectorSelf("tail"); + dtypeSpecStream.addConstructor(consStream); + Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); + Datatype dtStream = dtypeSortStream.getDatatype(); + EXPECT_TRUE(dtStream.isCodatatype()); + EXPECT_FALSE(dtStream.isFinite()); + // codatatypes may be well-founded + EXPECT_TRUE(dtStream.isWellFounded()); + + // create tuple + Sort tupSort = d_solver.mkTupleSort({boolSort}); + Datatype dtTuple = tupSort.getDatatype(); + EXPECT_TRUE(dtTuple.isTuple()); + EXPECT_FALSE(dtTuple.isRecord()); + EXPECT_TRUE(dtTuple.isFinite()); + EXPECT_TRUE(dtTuple.isWellFounded()); + + // create record + std::vector> fields = { + std::make_pair("b", boolSort), std::make_pair("i", intSort)}; + Sort recSort = d_solver.mkRecordSort(fields); + EXPECT_TRUE(recSort.isDatatype()); + Datatype dtRecord = recSort.getDatatype(); + EXPECT_FALSE(dtRecord.isTuple()); + EXPECT_TRUE(dtRecord.isRecord()); + EXPECT_FALSE(dtRecord.isFinite()); + EXPECT_TRUE(dtRecord.isWellFounded()); +} + +TEST_F(TestApi, datatypeNames) +{ + Sort intSort = d_solver.getIntegerSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + ASSERT_NO_THROW(dtypeSpec.getName()); + EXPECT_EQ(dtypeSpec.getName(), std::string("list")); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + EXPECT_EQ(dt.getName(), std::string("list")); + ASSERT_NO_THROW(dt.getConstructor("nil")); + ASSERT_NO_THROW(dt["cons"]); + ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException); + ASSERT_THROW(dt.getConstructor(""), CVC4ApiException); + + DatatypeConstructor dcons = dt[0]; + EXPECT_EQ(dcons.getName(), std::string("cons")); + ASSERT_NO_THROW(dcons.getSelector("head")); + ASSERT_NO_THROW(dcons["tail"]); + ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException); + + // get selector + DatatypeSelector dselTail = dcons[1]; + EXPECT_EQ(dselTail.getName(), std::string("tail")); + EXPECT_EQ(dselTail.getRangeSort(), dtypeSort); + + // possible to construct null datatype declarations if not using solver + ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException); +} + +TEST_F(TestApi, parametricDatatype) +{ + std::vector v; + Sort t1 = d_solver.mkParamSort("T1"); + Sort t2 = d_solver.mkParamSort("T2"); + v.push_back(t1); + v.push_back(t2); + DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v); + + DatatypeConstructorDecl mkpair = + d_solver.mkDatatypeConstructorDecl("mk-pair"); + mkpair.addSelector("first", t1); + mkpair.addSelector("second", t2); + pairSpec.addConstructor(mkpair); + + Sort pairType = d_solver.mkDatatypeSort(pairSpec); + + EXPECT_TRUE(pairType.getDatatype().isParametric()); + + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairIntInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getRealSort()); + Sort pairRealReal = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairRealInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getRealSort()); + Sort pairIntReal = pairType.instantiate(v); + + EXPECT_NE(pairIntInt, pairRealReal); + EXPECT_NE(pairIntReal, pairRealReal); + EXPECT_NE(pairRealInt, pairRealReal); + EXPECT_NE(pairIntInt, pairIntReal); + EXPECT_NE(pairIntInt, pairRealInt); + EXPECT_NE(pairIntReal, pairRealInt); + + EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt)); + EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal)); + EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt)); + EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt)); + + EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt)); + EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal)); + EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt)); + EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt)); +} + +TEST_F(TestApi, datatypeSimplyRec) +{ + /* Create mutual datatypes corresponding to this definition block: + * + * DATATYPE + * wlist = leaf(data: list), + * list = cons(car: wlist, cdr: list) | nil, + * ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresWList = d_solver.mkUninterpretedSort("wlist"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + Sort unresNs = d_solver.mkUninterpretedSort("ns"); + unresTypes.insert(unresWList); + unresTypes.insert(unresList); + unresTypes.insert(unresNs); + + DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + wlist.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresWList); + cons.addSelector("cdr", unresList); + list.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + DatatypeDecl ns = d_solver.mkDatatypeDecl("ns"); + DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem"); + elem.addSelector("ndata", d_solver.mkSetSort(unresWList)); + ns.addConstructor(elem); + DatatypeConstructorDecl elemArray = + d_solver.mkDatatypeConstructorDecl("elemArray"); + elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList)); + ns.addConstructor(elemArray); + + std::vector dtdecls; + dtdecls.push_back(wlist); + dtdecls.push_back(list); + dtdecls.push_back(ns); + // this is well-founded and has no nested recursion + std::vector dtsorts; + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 3); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded()); + EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion()); + EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * ns2 = elem2(ndata: array(int,ns2)) | nil2 + * END; + */ + unresTypes.clear(); + Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); + unresTypes.insert(unresNs2); + + DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); + DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); + elem2.addSelector("ndata", + d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2)); + ns2.addConstructor(elem2); + DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2"); + ns2.addConstructor(nil2); + + dtdecls.clear(); + dtdecls.push_back(ns2); + + dtsorts.clear(); + // this is not well-founded due to non-simple recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); + EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(), + dtsorts[0]); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list3 = cons3(car: ns3, cdr: list3) | nil3, + * ns3 = elem3(ndata: set(list3)) + * END; + */ + unresTypes.clear(); + Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); + unresTypes.insert(unresNs3); + Sort unresList3 = d_solver.mkUninterpretedSort("list3"); + unresTypes.insert(unresList3); + + DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); + DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); + cons3.addSelector("car", unresNs3); + cons3.addSelector("cdr", unresList3); + list3.addConstructor(cons3); + DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3"); + list3.addConstructor(nil3); + + DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3"); + DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem3.addSelector("ndata", d_solver.mkSetSort(unresList3)); + ns3.addConstructor(elem3); + + dtdecls.clear(); + dtdecls.push_back(list3); + dtdecls.push_back(ns3); + + dtsorts.clear(); + // both are well-founded and have nested recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 2); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list4 = cons(car: set(ns4), cdr: list4) | nil, + * ns4 = elem(ndata: list4) + * END; + */ + unresTypes.clear(); + Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); + unresTypes.insert(unresNs4); + Sort unresList4 = d_solver.mkUninterpretedSort("list4"); + unresTypes.insert(unresList4); + + DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); + DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); + cons4.addSelector("car", d_solver.mkSetSort(unresNs4)); + cons4.addSelector("cdr", unresList4); + list4.addConstructor(cons4); + DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4"); + list4.addConstructor(nil4); + + DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4"); + DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem4.addSelector("ndata", unresList4); + ns4.addConstructor(elem4); + + dtdecls.clear(); + dtdecls.push_back(list4); + dtdecls.push_back(ns4); + + dtsorts.clear(); + // both are well-founded and have nested recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 2); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + * END; + */ + unresTypes.clear(); + Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); + unresTypes.insert(unresList5); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); + + std::vector args; + args.push_back(x); + Sort urListX = unresList5.instantiate(args); + args[0] = urListX; + Sort urListListX = unresList5.instantiate(args); + + DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5"); + cons5.addSelector("car", x); + cons5.addSelector("cdr", urListListX); + list5.addConstructor(cons5); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5"); + list5.addConstructor(nil5); + + dtdecls.clear(); + dtdecls.push_back(list5); + + // well-founded and has nested recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); +} + +TEST_F(TestApi, datatypeSpecializedCons) +{ + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * plist[X] = pcons(car: X, cdr: plist[X]) | pnil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresList = d_solver.mkSortConstructorSort("plist", 1); + unresTypes.insert(unresList); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); + + std::vector args; + args.push_back(x); + Sort urListX = unresList.instantiate(args); + + DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons"); + pcons.addSelector("car", x); + pcons.addSelector("cdr", urListX); + plist.addConstructor(pcons); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil"); + plist.addConstructor(nil5); + + std::vector dtdecls; + dtdecls.push_back(plist); + + std::vector dtsorts; + // make the datatype sorts + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + Datatype d = dtsorts[0].getDatatype(); + DatatypeConstructor nilc = d[0]; + + Sort isort = d_solver.getIntegerSort(); + std::vector iargs; + iargs.push_back(isort); + Sort listInt = dtsorts[0].instantiate(iargs); + + Term testConsTerm; + // get the specialized constructor term for list[Int] + ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); + EXPECT_NE(testConsTerm, nilc.getConstructorTerm()); + // error to get the specialized constructor term for Int + EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); +} diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h deleted file mode 100644 index 4564b261a..000000000 --- a/test/unit/api/datatype_api_black.h +++ /dev/null @@ -1,576 +0,0 @@ -/********************* */ -/*! \file datatype_api_black.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the datatype classes of the C++ API. - ** - ** Black box testing of the datatype classes of the C++ API. - **/ - -#include - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class DatatypeBlack : public CxxTest::TestSuite -{ - public: - void setUp() override; - void tearDown() override; - - void testMkDatatypeSort(); - void testMkDatatypeSorts(); - - void testDatatypeStructs(); - void testDatatypeNames(); - - void testParametricDatatype(); - - void testDatatypeSimplyRec(); - - void testDatatypeSpecializedCons(); - - private: - Solver d_solver; -}; - -void DatatypeBlack::setUp() {} - -void DatatypeBlack::tearDown() {} - -void DatatypeBlack::testMkDatatypeSort() -{ - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", d_solver.getIntegerSort()); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); - Datatype d = listSort.getDatatype(); - DatatypeConstructor consConstr = d[0]; - DatatypeConstructor nilConstr = d[1]; - TS_ASSERT_THROWS(d[2], CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); - TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); -} - -void DatatypeBlack::testMkDatatypeSorts() -{ - /* Create two mutual datatypes corresponding to this definition - * block: - * - * DATATYPE - * tree = node(left: tree, right: tree) | leaf(data: list), - * list = cons(car: tree, cdr: list) | nil - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresTree = d_solver.mkUninterpretedSort("tree"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - unresTypes.insert(unresTree); - unresTypes.insert(unresList); - - DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); - DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); - node.addSelector("left", unresTree); - node.addSelector("right", unresTree); - tree.addConstructor(node); - - DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); - leaf.addSelector("data", unresList); - tree.addConstructor(leaf); - - DatatypeDecl list = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("car", unresTree); - cons.addSelector("cdr", unresTree); - list.addConstructor(cons); - - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - list.addConstructor(nil); - - std::vector dtdecls; - dtdecls.push_back(tree); - dtdecls.push_back(list); - std::vector dtsorts; - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == dtdecls.size()); - for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++) - { - TS_ASSERT(dtsorts[i].isDatatype()); - TS_ASSERT(!dtsorts[i].getDatatype().isFinite()); - TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName()); - } - // verify the resolution was correct - Datatype dtTree = dtsorts[0].getDatatype(); - DatatypeConstructor dtcTreeNode = dtTree[0]; - TS_ASSERT(dtcTreeNode.getName() == "node"); - DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; - TS_ASSERT(dtsTreeNodeLeft.getName() == "left"); - // argument type should have resolved to be recursive - TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype()); - TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]); - - // fails due to empty datatype - std::vector dtdeclsBad; - DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); - dtdeclsBad.push_back(emptyD); - TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&); -} - -void DatatypeBlack::testDatatypeStructs() -{ - Sort intSort = d_solver.getIntegerSort(); - Sort boolSort = d_solver.getBooleanSort(); - - // create datatype sort to test - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", intSort); - cons.addSelectorSelf("tail"); - Sort nullSort; - TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - Datatype dt = dtypeSort.getDatatype(); - TS_ASSERT(!dt.isCodatatype()); - TS_ASSERT(!dt.isTuple()); - TS_ASSERT(!dt.isRecord()); - TS_ASSERT(!dt.isFinite()); - TS_ASSERT(dt.isWellFounded()); - // get constructor - DatatypeConstructor dcons = dt[0]; - Term consTerm = dcons.getConstructorTerm(); - TS_ASSERT(dcons.getNumSelectors() == 2); - - // create datatype sort to test - DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); - DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); - dtypeSpecEnum.addConstructor(ca); - DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); - dtypeSpecEnum.addConstructor(cb); - DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C"); - dtypeSpecEnum.addConstructor(cc); - Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); - Datatype dtEnum = dtypeSortEnum.getDatatype(); - TS_ASSERT(!dtEnum.isTuple()); - TS_ASSERT(dtEnum.isFinite()); - - // create codatatype - DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); - DatatypeConstructorDecl consStream = - d_solver.mkDatatypeConstructorDecl("cons"); - consStream.addSelector("head", intSort); - consStream.addSelectorSelf("tail"); - dtypeSpecStream.addConstructor(consStream); - Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); - Datatype dtStream = dtypeSortStream.getDatatype(); - TS_ASSERT(dtStream.isCodatatype()); - TS_ASSERT(!dtStream.isFinite()); - // codatatypes may be well-founded - TS_ASSERT(dtStream.isWellFounded()); - - // create tuple - Sort tupSort = d_solver.mkTupleSort({boolSort}); - Datatype dtTuple = tupSort.getDatatype(); - TS_ASSERT(dtTuple.isTuple()); - TS_ASSERT(!dtTuple.isRecord()); - TS_ASSERT(dtTuple.isFinite()); - TS_ASSERT(dtTuple.isWellFounded()); - - // create record - std::vector> fields = { - std::make_pair("b", boolSort), std::make_pair("i", intSort)}; - Sort recSort = d_solver.mkRecordSort(fields); - TS_ASSERT(recSort.isDatatype()); - Datatype dtRecord = recSort.getDatatype(); - TS_ASSERT(!dtRecord.isTuple()); - TS_ASSERT(dtRecord.isRecord()); - TS_ASSERT(!dtRecord.isFinite()); - TS_ASSERT(dtRecord.isWellFounded()); -} - -void DatatypeBlack::testDatatypeNames() -{ - Sort intSort = d_solver.getIntegerSort(); - - // create datatype sort to test - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); - TS_ASSERT(dtypeSpec.getName() == std::string("list")); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", intSort); - cons.addSelectorSelf("tail"); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - Datatype dt = dtypeSort.getDatatype(); - TS_ASSERT(dt.getName() == std::string("list")); - TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil")); - TS_ASSERT_THROWS_NOTHING(dt["cons"]); - TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&); - TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&); - - DatatypeConstructor dcons = dt[0]; - TS_ASSERT(dcons.getName() == std::string("cons")); - TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head")); - TS_ASSERT_THROWS_NOTHING(dcons["tail"]); - TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&); - - // get selector - DatatypeSelector dselTail = dcons[1]; - TS_ASSERT(dselTail.getName() == std::string("tail")); - TS_ASSERT(dselTail.getRangeSort() == dtypeSort); - - // possible to construct null datatype declarations if not using solver - TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); -} - -void DatatypeBlack::testParametricDatatype() -{ - std::vector v; - Sort t1 = d_solver.mkParamSort("T1"); - Sort t2 = d_solver.mkParamSort("T2"); - v.push_back(t1); - v.push_back(t2); - DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v); - - DatatypeConstructorDecl mkpair = - d_solver.mkDatatypeConstructorDecl("mk-pair"); - mkpair.addSelector("first", t1); - mkpair.addSelector("second", t2); - pairSpec.addConstructor(mkpair); - - Sort pairType = d_solver.mkDatatypeSort(pairSpec); - - TS_ASSERT(pairType.getDatatype().isParametric()); - - v.clear(); - v.push_back(d_solver.getIntegerSort()); - v.push_back(d_solver.getIntegerSort()); - Sort pairIntInt = pairType.instantiate(v); - v.clear(); - v.push_back(d_solver.getRealSort()); - v.push_back(d_solver.getRealSort()); - Sort pairRealReal = pairType.instantiate(v); - v.clear(); - v.push_back(d_solver.getRealSort()); - v.push_back(d_solver.getIntegerSort()); - Sort pairRealInt = pairType.instantiate(v); - v.clear(); - v.push_back(d_solver.getIntegerSort()); - v.push_back(d_solver.getRealSort()); - Sort pairIntReal = pairType.instantiate(v); - - TS_ASSERT_DIFFERS(pairIntInt, pairRealReal); - TS_ASSERT_DIFFERS(pairIntReal, pairRealReal); - TS_ASSERT_DIFFERS(pairRealInt, pairRealReal); - TS_ASSERT_DIFFERS(pairIntInt, pairIntReal); - TS_ASSERT_DIFFERS(pairIntInt, pairRealInt); - TS_ASSERT_DIFFERS(pairIntReal, pairRealInt); - - TS_ASSERT(pairRealReal.isComparableTo(pairRealReal)); - TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal)); - TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal)); - TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal)); - TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt)); - TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt)); - TS_ASSERT(pairRealInt.isComparableTo(pairRealInt)); - TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt)); - TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal)); - TS_ASSERT(pairIntReal.isComparableTo(pairIntReal)); - TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal)); - TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal)); - TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt)); - TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt)); - TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt)); - TS_ASSERT(pairIntInt.isComparableTo(pairIntInt)); - - TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt)); - TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt)); - TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt)); - TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt)); - TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal)); - TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal)); - TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal)); - TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal)); - TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt)); - TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt)); - TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt)); - TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt)); -} - -void DatatypeBlack::testDatatypeSimplyRec() -{ - /* Create mutual datatypes corresponding to this definition block: - * - * DATATYPE - * wlist = leaf(data: list), - * list = cons(car: wlist, cdr: list) | nil, - * ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresWList = d_solver.mkUninterpretedSort("wlist"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - Sort unresNs = d_solver.mkUninterpretedSort("ns"); - unresTypes.insert(unresWList); - unresTypes.insert(unresList); - unresTypes.insert(unresNs); - - DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); - DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); - leaf.addSelector("data", unresList); - wlist.addConstructor(leaf); - - DatatypeDecl list = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("car", unresWList); - cons.addSelector("cdr", unresList); - list.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - list.addConstructor(nil); - - DatatypeDecl ns = d_solver.mkDatatypeDecl("ns"); - DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem"); - elem.addSelector("ndata", d_solver.mkSetSort(unresWList)); - ns.addConstructor(elem); - DatatypeConstructorDecl elemArray = - d_solver.mkDatatypeConstructorDecl("elemArray"); - elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList)); - ns.addConstructor(elemArray); - - std::vector dtdecls; - dtdecls.push_back(wlist); - dtdecls.push_back(list); - dtdecls.push_back(ns); - // this is well-founded and has no nested recursion - std::vector dtsorts; - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 3); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[2].getDatatype().isWellFounded()); - TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion()); - TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion()); - TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * ns2 = elem2(ndata: array(int,ns2)) | nil2 - * END; - */ - unresTypes.clear(); - Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); - unresTypes.insert(unresNs2); - - DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); - DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); - elem2.addSelector("ndata", - d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2)); - ns2.addConstructor(elem2); - DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2"); - ns2.addConstructor(nil2); - - dtdecls.clear(); - dtdecls.push_back(ns2); - - dtsorts.clear(); - // this is not well-founded due to non-simple recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); - TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() - == dtsorts[0]); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * list3 = cons3(car: ns3, cdr: list3) | nil3, - * ns3 = elem3(ndata: set(list3)) - * END; - */ - unresTypes.clear(); - Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); - unresTypes.insert(unresNs3); - Sort unresList3 = d_solver.mkUninterpretedSort("list3"); - unresTypes.insert(unresList3); - - DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); - DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); - cons3.addSelector("car", unresNs3); - cons3.addSelector("cdr", unresList3); - list3.addConstructor(cons3); - DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3"); - list3.addConstructor(nil3); - - DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3"); - DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3"); - elem3.addSelector("ndata", d_solver.mkSetSort(unresList3)); - ns3.addConstructor(elem3); - - dtdecls.clear(); - dtdecls.push_back(list3); - dtdecls.push_back(ns3); - - dtsorts.clear(); - // both are well-founded and have nested recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 2); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); - TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * list4 = cons(car: set(ns4), cdr: list4) | nil, - * ns4 = elem(ndata: list4) - * END; - */ - unresTypes.clear(); - Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); - unresTypes.insert(unresNs4); - Sort unresList4 = d_solver.mkUninterpretedSort("list4"); - unresTypes.insert(unresList4); - - DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); - DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); - cons4.addSelector("car", d_solver.mkSetSort(unresNs4)); - cons4.addSelector("cdr", unresList4); - list4.addConstructor(cons4); - DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4"); - list4.addConstructor(nil4); - - DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4"); - DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3"); - elem4.addSelector("ndata", unresList4); - ns4.addConstructor(elem4); - - dtdecls.clear(); - dtdecls.push_back(list4); - dtdecls.push_back(ns4); - - dtsorts.clear(); - // both are well-founded and have nested recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 2); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); - TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil - * END; - */ - unresTypes.clear(); - Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); - unresTypes.insert(unresList5); - - std::vector v; - Sort x = d_solver.mkParamSort("X"); - v.push_back(x); - DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); - - std::vector args; - args.push_back(x); - Sort urListX = unresList5.instantiate(args); - args[0] = urListX; - Sort urListListX = unresList5.instantiate(args); - - DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5"); - cons5.addSelector("car", x); - cons5.addSelector("cdr", urListListX); - list5.addConstructor(cons5); - DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5"); - list5.addConstructor(nil5); - - dtdecls.clear(); - dtdecls.push_back(list5); - - // well-founded and has nested recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); -} - -void DatatypeBlack::testDatatypeSpecializedCons() -{ - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * plist[X] = pcons(car: X, cdr: plist[X]) | pnil - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresList = d_solver.mkSortConstructorSort("plist", 1); - unresTypes.insert(unresList); - - std::vector v; - Sort x = d_solver.mkParamSort("X"); - v.push_back(x); - DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); - - std::vector args; - args.push_back(x); - Sort urListX = unresList.instantiate(args); - - DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons"); - pcons.addSelector("car", x); - pcons.addSelector("cdr", urListX); - plist.addConstructor(pcons); - DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil"); - plist.addConstructor(nil5); - - std::vector dtdecls; - dtdecls.push_back(plist); - - std::vector dtsorts; - // make the datatype sorts - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - Datatype d = dtsorts[0].getDatatype(); - DatatypeConstructor nilc = d[0]; - - Sort isort = d_solver.getIntegerSort(); - std::vector iargs; - iargs.push_back(isort); - Sort listInt = dtsorts[0].instantiate(iargs); - - Term testConsTerm; - // get the specialized constructor term for list[Int] - TS_ASSERT_THROWS_NOTHING(testConsTerm = - nilc.getSpecializedConstructorTerm(listInt)); - TS_ASSERT(testConsTerm != nilc.getConstructorTerm()); - // error to get the specialized constructor term for Int - TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&); -} diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt index 81d27c040..8274a5a46 100644 --- a/test/unit/base/CMakeLists.txt +++ b/test/unit/base/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(map_util_black base) +cvc4_add_cxx_unit_test_black(map_util_black base) diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 6752f0e78..51465c622 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -11,10 +11,10 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(cdlist_black context) -cvc4_add_unit_test_black(cdmap_black context) -cvc4_add_unit_test_white(cdmap_white context) -cvc4_add_unit_test_black(cdo_black context) -cvc4_add_unit_test_black(context_black context) -cvc4_add_unit_test_black(context_mm_black context) -cvc4_add_unit_test_white(context_white context) +cvc4_add_cxx_unit_test_black(cdlist_black context) +cvc4_add_cxx_unit_test_black(cdmap_black context) +cvc4_add_cxx_unit_test_white(cdmap_white context) +cvc4_add_cxx_unit_test_black(cdo_black context) +cvc4_add_cxx_unit_test_black(context_black context) +cvc4_add_cxx_unit_test_black(context_mm_black context) +cvc4_add_cxx_unit_test_white(context_white context) diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index c10648c03..6c0abc4ab 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -11,20 +11,20 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(attribute_black expr) -cvc4_add_unit_test_white(attribute_white expr) -cvc4_add_unit_test_black(expr_manager_public expr) -cvc4_add_unit_test_black(expr_public expr) -cvc4_add_unit_test_black(kind_black expr) -cvc4_add_unit_test_black(kind_map_black expr) -cvc4_add_unit_test_black(node_black expr) -cvc4_add_unit_test_black(node_algorithm_black expr) -cvc4_add_unit_test_black(node_builder_black expr) -cvc4_add_unit_test_black(node_manager_black expr) -cvc4_add_unit_test_white(node_manager_white expr) -cvc4_add_unit_test_black(node_self_iterator_black expr) -cvc4_add_unit_test_black(node_traversal_black expr) -cvc4_add_unit_test_white(node_white expr) -cvc4_add_unit_test_black(symbol_table_black expr) -cvc4_add_unit_test_black(type_cardinality_public expr) -cvc4_add_unit_test_white(type_node_white expr) +cvc4_add_cxx_unit_test_black(attribute_black expr) +cvc4_add_cxx_unit_test_white(attribute_white expr) +cvc4_add_cxx_unit_test_black(expr_manager_public expr) +cvc4_add_cxx_unit_test_black(expr_public expr) +cvc4_add_cxx_unit_test_black(kind_black expr) +cvc4_add_cxx_unit_test_black(kind_map_black expr) +cvc4_add_cxx_unit_test_black(node_black expr) +cvc4_add_cxx_unit_test_black(node_algorithm_black expr) +cvc4_add_cxx_unit_test_black(node_builder_black expr) +cvc4_add_cxx_unit_test_black(node_manager_black expr) +cvc4_add_cxx_unit_test_white(node_manager_white expr) +cvc4_add_cxx_unit_test_black(node_self_iterator_black expr) +cvc4_add_cxx_unit_test_black(node_traversal_black expr) +cvc4_add_cxx_unit_test_white(node_white expr) +cvc4_add_cxx_unit_test_black(symbol_table_black expr) +cvc4_add_cxx_unit_test_black(type_cardinality_public expr) +cvc4_add_cxx_unit_test_white(type_node_white expr) diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index 55307db95..59c197f04 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(interactive_shell_black main) +cvc4_add_cxx_unit_test_black(interactive_shell_black main) diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index 1bdcbd5f5..4202ea0c9 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -11,5 +11,5 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(parser_black parser) -cvc4_add_unit_test_black(parser_builder_black parser) +cvc4_add_cxx_unit_test_black(parser_black parser) +cvc4_add_cxx_unit_test_black(parser_builder_black parser) diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index 7e142f404..a2381ba90 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing) +cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing) diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt index 3b040d1fc..93c241af9 100644 --- a/test/unit/printer/CMakeLists.txt +++ b/test/unit/printer/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(smt2_printer_black printer) +cvc4_add_cxx_unit_test_black(smt2_printer_black printer) diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index bed0575c6..f866e5ffa 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(cnf_stream_white prop) +cvc4_add_cxx_unit_test_white(cnf_stream_white prop) diff --git a/test/unit/test_api.h b/test/unit/test_api.h new file mode 100644 index 000000000..72d0658a7 --- /dev/null +++ b/test/unit/test_api.h @@ -0,0 +1,27 @@ +/********************* */ +/*! \file datatype_api_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Common header for API unit test. + **/ + +#ifndef CVC4__TEST__UNIT__TEST_API_H +#define CVC4__TEST__UNIT__TEST_API_H + +#include "api/cvc4cpp.h" +#include "gtest/gtest.h" + +class TestApi : public ::testing::Test +{ + protected: + CVC4::api::Solver d_solver; +}; + +#endif diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 0eccbf436..334ded2d1 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -8,24 +8,24 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cvc4_add_unit_test_black(regexp_operation_black theory) -cvc4_add_unit_test_black(theory_black theory) -cvc4_add_unit_test_white(evaluator_white theory) -cvc4_add_unit_test_white(logic_info_white theory) -cvc4_add_unit_test_white(sequences_rewriter_white theory) -cvc4_add_unit_test_white(strings_rewriter_white theory) -cvc4_add_unit_test_white(theory_arith_white theory) -cvc4_add_unit_test_white(theory_bags_normal_form_white theory) -cvc4_add_unit_test_white(theory_bags_rewriter_white theory) -cvc4_add_unit_test_white(theory_bags_type_rules_white theory) -cvc4_add_unit_test_white(theory_bv_rewriter_white theory) -cvc4_add_unit_test_white(theory_bv_white theory) -cvc4_add_unit_test_white(theory_engine_white theory) -cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) -cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) -cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) -cvc4_add_unit_test_white(theory_sets_type_rules_white theory) -cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) -cvc4_add_unit_test_white(theory_strings_word_white theory) -cvc4_add_unit_test_white(theory_white theory) -cvc4_add_unit_test_white(type_enumerator_white theory) +cvc4_add_cxx_unit_test_black(regexp_operation_black theory) +cvc4_add_cxx_unit_test_black(theory_black theory) +cvc4_add_cxx_unit_test_white(evaluator_white theory) +cvc4_add_cxx_unit_test_white(logic_info_white theory) +cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory) +cvc4_add_cxx_unit_test_white(strings_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_arith_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory) +cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_bv_white theory) +cvc4_add_cxx_unit_test_white(theory_engine_white theory) +cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory) +cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory) +cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory) +cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory) +cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) +cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) +cvc4_add_cxx_unit_test_white(theory_white theory) +cvc4_add_cxx_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 0fd7894fe..148ae9910 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -11,25 +11,25 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(array_store_all_white util) -cvc4_add_unit_test_white(assert_white util) -cvc4_add_unit_test_black(binary_heap_black util) -cvc4_add_unit_test_black(bitvector_black util) -cvc4_add_unit_test_black(boolean_simplification_black util) -cvc4_add_unit_test_black(cardinality_public util) -cvc4_add_unit_test_white(check_white util) -cvc4_add_unit_test_black(configuration_black util) -cvc4_add_unit_test_black(datatype_black util) -cvc4_add_unit_test_black(exception_black util) +cvc4_add_cxx_unit_test_white(array_store_all_white util) +cvc4_add_cxx_unit_test_white(assert_white util) +cvc4_add_cxx_unit_test_black(binary_heap_black util) +cvc4_add_cxx_unit_test_black(bitvector_black util) +cvc4_add_cxx_unit_test_black(boolean_simplification_black util) +cvc4_add_cxx_unit_test_black(cardinality_public util) +cvc4_add_cxx_unit_test_white(check_white util) +cvc4_add_cxx_unit_test_black(configuration_black util) +cvc4_add_cxx_unit_test_black(datatype_black util) +cvc4_add_cxx_unit_test_black(exception_black util) if(CVC4_USE_SYMFPU) -cvc4_add_unit_test_black(floatingpoint_black util) +cvc4_add_cxx_unit_test_black(floatingpoint_black util) endif() -cvc4_add_unit_test_black(integer_black util) -cvc4_add_unit_test_white(integer_white util) -cvc4_add_unit_test_black(output_black util) -cvc4_add_unit_test_black(rational_black util) -cvc4_add_unit_test_white(rational_white util) +cvc4_add_cxx_unit_test_black(integer_black util) +cvc4_add_cxx_unit_test_white(integer_white util) +cvc4_add_cxx_unit_test_black(output_black util) +cvc4_add_cxx_unit_test_black(rational_black util) +cvc4_add_cxx_unit_test_white(rational_white util) if(CVC4_USE_POLY_IMP) -cvc4_add_unit_test_black(real_algebraic_number_black util) +cvc4_add_cxx_unit_test_black(real_algebraic_number_black util) endif() -cvc4_add_unit_test_black(stats_black util) +cvc4_add_cxx_unit_test_black(stats_black util) -- cgit v1.2.3 From 558efa2593fda09235c5f2163836771680d3442a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 1 Dec 2020 18:24:21 -0800 Subject: google test: api: Migrate result_black. (#5569) google test: api: Migrate result_black. --- test/unit/api/CMakeLists.txt | 2 +- test/unit/api/result_black.cpp | 115 +++++++++++++++++++++++++++++++++++ test/unit/api/result_black.h | 132 ----------------------------------------- 3 files changed, 116 insertions(+), 133 deletions(-) create mode 100644 test/unit/api/result_black.cpp delete mode 100644 test/unit/api/result_black.h (limited to 'test') diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 9fcf881a8..a8c696c00 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -13,7 +13,7 @@ cvc4_add_unit_test_black(datatype_api_black api) cvc4_add_cxx_unit_test_black(op_black api) -cvc4_add_cxx_unit_test_black(result_black api) +cvc4_add_unit_test_black(result_black api) cvc4_add_cxx_unit_test_black(solver_black api) cvc4_add_cxx_unit_test_black(sort_black api) cvc4_add_cxx_unit_test_black(term_black api) diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp new file mode 100644 index 000000000..260845495 --- /dev/null +++ b/test/unit/api/result_black.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file result_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the Result class + **/ + +#include "test_api.h" + +using namespace CVC4::api; + +class TestApiResultBlack : public TestApi +{ +}; + +TEST_F(TestApiResultBlack, isNull) +{ + Result res_null; + ASSERT_TRUE(res_null.isNull()); + ASSERT_FALSE(res_null.isSat()); + ASSERT_FALSE(res_null.isUnsat()); + ASSERT_FALSE(res_null.isSatUnknown()); + ASSERT_FALSE(res_null.isEntailed()); + ASSERT_FALSE(res_null.isNotEntailed()); + ASSERT_FALSE(res_null.isEntailmentUnknown()); + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res = d_solver.checkSat(); + ASSERT_FALSE(res.isNull()); +} + +TEST_F(TestApiResultBlack, eq) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res; + Result res2 = d_solver.checkSat(); + Result res3 = d_solver.checkSat(); + res = res2; + EXPECT_EQ(res, res2); + EXPECT_EQ(res3, res2); +} + +TEST_F(TestApiResultBlack, isSat) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res = d_solver.checkSat(); + ASSERT_TRUE(res.isSat()); + ASSERT_FALSE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isUnsat) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkSat(); + ASSERT_TRUE(res.isUnsat()); + ASSERT_FALSE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isSatUnknown) +{ + d_solver.setLogic("QF_NIA"); + d_solver.setOption("incremental", "false"); + d_solver.setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver.getIntegerSort(); + Term x = d_solver.mkVar(int_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkSat(); + ASSERT_FALSE(res.isSat()); + ASSERT_TRUE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isEntailed) +{ + d_solver.setOption("incremental", "true"); + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(u_sort, "x"); + Term y = d_solver.mkConst(u_sort, "y"); + Term a = x.eqTerm(y).notTerm(); + Term b = x.eqTerm(y); + d_solver.assertFormula(a); + Result entailed = d_solver.checkEntailed(a); + ASSERT_TRUE(entailed.isEntailed()); + ASSERT_FALSE(entailed.isEntailmentUnknown()); + Result not_entailed = d_solver.checkEntailed(b); + ASSERT_TRUE(not_entailed.isNotEntailed()); + ASSERT_FALSE(not_entailed.isEntailmentUnknown()); +} + +TEST_F(TestApiResultBlack, isEntailmentUnknown) +{ + d_solver.setLogic("QF_NIA"); + d_solver.setOption("incremental", "false"); + d_solver.setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver.getIntegerSort(); + Term x = d_solver.mkVar(int_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkEntailed(x.eqTerm(x)); + ASSERT_FALSE(res.isEntailed()); + ASSERT_TRUE(res.isEntailmentUnknown()); + EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON"); +} diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h deleted file mode 100644 index aaa59e506..000000000 --- a/test/unit/api/result_black.h +++ /dev/null @@ -1,132 +0,0 @@ -/********************* */ -/*! \file result_black.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the Result class - **/ - -#include - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class ResultBlack : public CxxTest::TestSuite -{ - public: - void setUp() { d_solver.reset(new Solver()); } - void tearDown() override { d_solver.reset(nullptr); } - - void testIsNull(); - void testEq(); - void testIsSat(); - void testIsUnsat(); - void testIsSatUnknown(); - void testIsEntailed(); - void testIsEntailmentUnknown(); - - private: - std::unique_ptr d_solver; -}; - -void ResultBlack::testIsNull() -{ - Result res_null; - TS_ASSERT(res_null.isNull()); - TS_ASSERT(!res_null.isSat()); - TS_ASSERT(!res_null.isUnsat()); - TS_ASSERT(!res_null.isSatUnknown()); - TS_ASSERT(!res_null.isEntailed()); - TS_ASSERT(!res_null.isNotEntailed()); - TS_ASSERT(!res_null.isEntailmentUnknown()); - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkSat(); - TS_ASSERT(!res.isNull()); -} - -void ResultBlack::testEq() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res; - Result res2 = d_solver->checkSat(); - Result res3 = d_solver->checkSat(); - res = res2; - TS_ASSERT_EQUALS(res, res2); - TS_ASSERT_EQUALS(res3, res2); -} - -void ResultBlack::testIsSat() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkSat(); - TS_ASSERT(res.isSat()); - TS_ASSERT(!res.isSatUnknown()); -} - -void ResultBlack::testIsUnsat() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkSat(); - TS_ASSERT(res.isUnsat()); - TS_ASSERT(!res.isSatUnknown()); -} - -void ResultBlack::testIsSatUnknown() -{ - d_solver->setLogic("QF_NIA"); - d_solver->setOption("incremental", "false"); - d_solver->setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver->getIntegerSort(); - Term x = d_solver->mkVar(int_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkSat(); - TS_ASSERT(!res.isSat()); - TS_ASSERT(res.isSatUnknown()); -} - -void ResultBlack::testIsEntailed() -{ - d_solver->setOption("incremental", "true"); - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkConst(u_sort, "x"); - Term y = d_solver->mkConst(u_sort, "y"); - Term a = x.eqTerm(y).notTerm(); - Term b = x.eqTerm(y); - d_solver->assertFormula(a); - Result entailed = d_solver->checkEntailed(a); - TS_ASSERT(entailed.isEntailed()); - TS_ASSERT(!entailed.isEntailmentUnknown()); - Result not_entailed = d_solver->checkEntailed(b); - TS_ASSERT(not_entailed.isNotEntailed()); - TS_ASSERT(!not_entailed.isEntailmentUnknown()); -} - -void ResultBlack::testIsEntailmentUnknown() -{ - d_solver->setLogic("QF_NIA"); - d_solver->setOption("incremental", "false"); - d_solver->setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver->getIntegerSort(); - Term x = d_solver->mkVar(int_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkEntailed(x.eqTerm(x)); - TS_ASSERT(!res.isEntailed()); - TS_ASSERT(res.isEntailmentUnknown()); - TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON"); -} - -- cgit v1.2.3 From 901cea314c4dc3be411c345e42c858063fe5aa1b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Dec 2020 06:22:56 +0100 Subject: Add regressions from #3687. (#5553) The error from #3687 has been fixed in the meantime. This PR adds the two examples from this issue as regressions. Closes #3687 --- test/regress/CMakeLists.txt | 2 + .../aufbv/issue3687-check-models-small.smt2 | 8 ++++ test/regress/regress2/issue3687-check-models.smt2 | 51 ++++++++++++++++++++++ 3 files changed, 61 insertions(+) create mode 100644 test/regress/regress0/aufbv/issue3687-check-models-small.smt2 create mode 100644 test/regress/regress2/issue3687-check-models.smt2 (limited to 'test') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fda5c69eb..1826b3156 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -126,6 +126,7 @@ set(regress_0_tests regress0/aufbv/fuzz14.smtv1.smt2 regress0/aufbv/fuzz15.smtv1.smt2 regress0/aufbv/issue3737.smt2 + regress0/aufbv/issue3687-check-models-small.smt2 regress0/aufbv/rewrite_bug.smtv1.smt2 regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2 regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2 @@ -2176,6 +2177,7 @@ set(regress_2_tests regress2/hole7.cvc regress2/hole8.cvc regress2/instance_1444.smtv1.smt2 + regress2/issue3687-check-models.smt2 regress2/issue4707-bv-to-bool-large.smt2 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 regress2/javafe.ast.WhileStmt.447_no_forall.smt2 diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 new file mode 100644 index 000000000..88cbd8a0b --- /dev/null +++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --check-models +; EXPECT: sat +(set-logic QF_AUFBV) +(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2))) +(declare-fun b () (_ BitVec 2)) +(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a + #b00))) #b10 #b00) b))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2 new file mode 100644 index 000000000..02f7754cf --- /dev/null +++ b/test/regress/regress2/issue3687-check-models.smt2 @@ -0,0 +1,51 @@ +; COMMAND-LINE: --check-models +; EXPECT: sat +(set-logic QF_ABV) +(declare-fun c () (_ BitVec 32)) +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun b () (_ BitVec 32)) +(assert (let ((a!1 (bvxnor (concat #x000000 (select a (bvadd c #x00000001))) #x00000008)) + (a!3 (bvsdiv (concat #x000000 (select a (bvadd c #x00000002))) #x00000010)) + (a!4 (bvudiv (concat #x000000 (select a (bvashr c #x00000003))) + #x00000018)) + (a!5 (select a + (bvxor (bvsub (bvnand c #x00000004) #x00000004) #x00000000))) + (a!6 (select a + (bvsdiv (bvsub (bvnand c #x00000004) #x00000004) #x00000001))) + (a!7 (select a + (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000002))) + (a!9 (store a + (bvashr (bvurem (bvnand c #x00000004) #x00000004) #x00000001) + ((_ extract 7 0) (bvxnor b #x00000008)))) + (a!11 (bvnand (bvurem (bvsub (bvnand c #x00000004) #x00000004) #x00000004) + #x00000008))) +(let ((a!2 (bvnor (concat #x000000 (select a (bvsmod c #x00000000))) a!1)) + (a!8 (bvlshr (bvor (concat #x000000 a!5) + (bvmul (concat #x000000 a!6) #x00000008)) + (bvand (concat #x000000 a!7) #x00000010))) + (a!10 (store a!9 + (bvshl (bvurem (bvnand c #x00000004) #x00000004) #x00000000) + ((_ extract 7 0) b))) + (a!12 (bvsub (concat #x000000 (select a (bvashr a!11 #x00000001))) + #x00000008)) + (a!14 (bvxnor (concat #x000000 (select a (bvxnor a!11 #x00000002))) + #x00000010)) + (a!15 (bvxor (concat #x000000 (select a (bvsub a!11 #x00000003))) + #x00000018))) +(let ((a!13 (bvor (concat #x000000 (select a (bvmul a!11 #x00000000))) a!12))) +(let ((a!16 ((_ extract 7 0) + (bvmul (bvurem (bvurem a!13 a!14) a!15) #x00000018))) + (a!17 ((_ extract 7 0) (bvor (bvurem (bvurem a!13 a!14) a!15) #x00000010))) + (a!18 ((_ extract 7 0) + (bvnor (bvurem (bvurem a!13 a!14) a!15) #x00000008)))) +(let ((a!19 (store (store (store (store a!10 #x08053e77 a!16) #x08053e76 a!17) + #x08053e75 + a!18) + #x08053e74 + ((_ extract 7 0) (bvurem (bvurem a!13 a!14) a!15))))) +(let ((a!20 (select a!19 + (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000003)))) +(let ((a!21 (distinct (bvsdiv (bvsmod a!2 a!3) a!4) + (bvshl a!8 (bvshl (concat #x000000 a!20) #x00000018))))) + (= #b1 (bvashr (ite (or a!21) #b1 #b0) #b1)))))))))) +(check-sat) -- cgit v1.2.3