From b685ed411b6814f0810ce8f61d07aa49bd75ea3b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 29 Jul 2021 11:11:05 -0500 Subject: [PATCH] Integrate central equality engine approach into theory engine, add option and regressions (#6943) This commit makes TheoryEngine take into account whether theories are using the central equality engine. With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`. --- src/options/theory_options.toml | 3 ++ src/smt/set_defaults.cpp | 8 ++++ src/theory/combination_engine.cpp | 14 +++++- src/theory/theory.cpp | 22 ++++++++-- src/theory/theory.h | 4 +- src/theory/theory_engine.cpp | 40 ++++++++++++----- test/regress/CMakeLists.txt | 11 +++++ .../regress0/aufbv/cee-small-shared-eq.smt2 | 8 ++++ .../datatypes/canExp-dtPendingMerge.smt2 | 10 +++++ test/regress/regress0/sets/sets-deq-dd.smt2 | 8 ++++ .../regress1/cee-bug0909-dd-scope.smt2 | 23 ++++++++++ .../regress1/datatypes/cee-prs-small-dd2.smt2 | 12 ++++++ .../regress1/push-pop/cee-prs-small.smt2 | 14 ++++++ .../regress1/quantifiers/cee-npnt-dd.smt2 | 14 ++++++ .../regress1/quantifiers/cee-os-delta.smt2 | 9 ++++ .../strings/cee-norn-aes-trivially.smt2 | 9 ++++ .../quantifiers/cee-event-wrong-sat.smt2 | 43 +++++++++++++++++++ .../quantifiers/exp-trivially-dd3.smt2 | 41 ++++++++++++++++++ 18 files changed, 278 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/aufbv/cee-small-shared-eq.smt2 create mode 100644 test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 create mode 100644 test/regress/regress0/sets/sets-deq-dd.smt2 create mode 100644 test/regress/regress1/cee-bug0909-dd-scope.smt2 create mode 100644 test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 create mode 100644 test/regress/regress1/push-pop/cee-prs-small.smt2 create mode 100644 test/regress/regress1/quantifiers/cee-npnt-dd.smt2 create mode 100644 test/regress/regress1/quantifiers/cee-os-delta.smt2 create mode 100644 test/regress/regress1/strings/cee-norn-aes-trivially.smt2 create mode 100644 test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 create mode 100644 test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index f47907683..87869beb3 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -51,6 +51,9 @@ name = "Theory Layer" [[option.mode.DISTRIBUTED]] name = "distributed" help = "Each theory maintains its own equality engine." +[[option.mode.CENTRAL]] + name = "central" + help = "All applicable theories use the central equality engine." [[option]] name = "tcMode" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e12d3eb1d..c7a2c8916 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -970,6 +970,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set up of central equality engine + if (opts.theory.eeMode == options::EqEngineMode::CENTRAL) + { + if (!opts.arith.arithEqSolverWasSetByUser) + { + // use the arithmetic equality solver by default + opts.arith.arithEqSolver = true; + } + } if (opts.arith.arithEqSolver) { if (!opts.arith.arithCongManWasSetByUser) diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index da7f0a548..609f8d9d6 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -18,10 +18,10 @@ #include "expr/node_visitor.h" #include "proof/eager_proof_generator.h" #include "theory/care_graph.h" +#include "theory/ee_manager_central.h" #include "theory/ee_manager_distributed.h" #include "theory/model_manager.h" #include "theory/model_manager_distributed.h" -#include "theory/shared_solver.h" #include "theory/shared_solver_distributed.h" #include "theory/theory_engine.h" @@ -56,6 +56,18 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, d_mmanager.reset( new ModelManagerDistributed(d_te, d_env, *d_eemanager.get())); } + else if (options::eeMode() == options::EqEngineMode::CENTRAL) + { + // for now, the shared solver is the same in both approaches; use the + // distributed one for now + d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm)); + // make the central equality engine manager + d_eemanager.reset( + new EqEngineManagerCentral(d_te, *d_sharedSolver.get(), d_pnm)); + // make the distributed model manager + d_mmanager.reset( + new ModelManagerDistributed(d_te, d_env, *d_eemanager.get())); + } else { Unhandled() << "CombinationEngine::finishInit: equality engine mode " diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 891a3ca08..07920ecc6 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -22,6 +22,8 @@ #include "base/check.h" #include "expr/node_algorithm.h" +#include "options/arith_options.h" +#include "options/bv_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "smt/smt_statistics_registry.h" @@ -368,7 +370,7 @@ std::unordered_set Theory::currentlySharedTerms() const bool Theory::collectModelInfo(TheoryModel* m, const std::set& termSet) { // if we are using an equality engine, assert it to the model - if (d_equalityEngine != nullptr) + if (d_equalityEngine != nullptr && !termSet.empty()) { Trace("model-builder") << "Assert Equality engine for " << d_id << std::endl; @@ -613,10 +615,24 @@ bool Theory::usesCentralEqualityEngine(TheoryId id) { return false; } - // Below are all theories with an equality engine except id ==THEORY_ARITH + if (id == THEORY_ARITH) + { + // conditional on whether we are using the equality solver + return options::arithEqSolver(); + } + if (id == THEORY_BV) + { + // the internal bitblast BV solver doesnt use an equality engine + return options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL; + } return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS - || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; + || id == THEORY_SEP || id == THEORY_ARRAYS; +} + +bool Theory::expUsingCentralEqualityEngine(TheoryId id) +{ + return id != THEORY_ARITH && usesCentralEqualityEngine(id); } } // namespace theory diff --git a/src/theory/theory.h b/src/theory/theory.h index 7149d8e3f..41f35601b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -877,10 +877,12 @@ class Theory { */ virtual std::pair entailmentCheck(TNode lit); - /** uses central equality engine */ + /** Return true if this theory uses central equality engine */ bool usesCentralEqualityEngine() const; /** uses central equality engine (static) */ static bool usesCentralEqualityEngine(TheoryId id); + /** Explains/propagates via central equality engine only */ + static bool expUsingCentralEqualityEngine(TheoryId id); };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 58014b06b..63fd6d9b7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -909,13 +909,16 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo return; } - // If sending to the shared terms database, it's also simple + // determine the actual theory that will process/explain the fact, which is + // THEORY_BUILTIN if the theory uses the central equality engine + TheoryId toTheoryIdProp = (Theory::expUsingCentralEqualityEngine(toTheoryId)) + ? THEORY_BUILTIN + : toTheoryId; + // If sending to the shared solver, it's also simple if (toTheoryId == THEORY_BUILTIN) { - Assert(assertion.getKind() == kind::EQUAL - || (assertion.getKind() == kind::NOT - && assertion[0].getKind() == kind::EQUAL)) - << "atom should be an EQUALity, not `" << assertion << "'"; - if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { + if (markPropagation( + assertion, originalAssertion, toTheoryIdProp, fromTheoryId)) + { // assert to the shared solver bool polarity = assertion.getKind() != kind::NOT; TNode atom = polarity ? assertion : assertion[0]; @@ -928,7 +931,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // directly to the apropriate theory if (fromTheoryId == THEORY_SAT_SOLVER) { // We know that this is normalized, so just send it off to the theory - if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { + if (markPropagation( + assertion, originalAssertion, toTheoryIdProp, fromTheoryId)) + { // Is it preregistered bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId; // We assert it @@ -942,6 +947,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // Propagations to the SAT solver are just enqueued for pickup by // the SAT solver later if (toTheoryId == THEORY_SAT_SOLVER) { + Assert(toTheoryIdProp == toTheoryId); if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // Enqueue for propagation to the SAT solver d_propagatedLiterals.push_back(assertion); @@ -971,7 +977,11 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo if (normalizedLiteral.isConst()) { if (!normalizedLiteral.getConst()) { // Mark the propagation for explanations - if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) { + if (markPropagation(normalizedLiteral, + originalAssertion, + toTheoryIdProp, + fromTheoryId)) + { // special case, trust node has no proof generator TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral); // Get the explanation (conflict will figure out where it came from) @@ -984,7 +994,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo } // Try and assert (note that we assert the non-normalized one) - if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { + if (markPropagation( + assertion, originalAssertion, toTheoryIdProp, fromTheoryId)) + { // Check if has been pre-registered with the theory bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId; // Assert away @@ -1509,6 +1521,12 @@ TrustNode TheoryEngine::getExplanation( { Assert(explanationVector.size() == 1); Node conclusion = explanationVector[0].d_node; + // if the theory explains using the central equality engine, we always start + // with THEORY_BUILTIN. + if (Theory::expUsingCentralEqualityEngine(explanationVector[0].d_theory)) + { + explanationVector[0].d_theory = THEORY_BUILTIN; + } std::shared_ptr lcp; if (isProofEnabled()) { @@ -1668,7 +1686,9 @@ TrustNode TheoryEngine::getExplanation( << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.d_theory << endl; Assert(explanation != toExplain.d_node) - << "wasn't sent to you, so why are you explaining it trivially"; + << "wasn't sent to you, so why are you explaining it trivially, for " + "fact " + << explanation; // Mark the explanation NodeTheoryPair newExplain( explanation, toExplain.d_theory, toExplain.d_timestamp); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 151e01088..902037088 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -120,6 +120,7 @@ set(regress_0_tests regress0/aufbv/bug493.smtv1.smt2 regress0/aufbv/bug509.smtv1.smt2 regress0/aufbv/bug580.delta.smt2 + regress0/aufbv/cee-small-shared-eq.smt2 regress0/aufbv/diseqprop.01.smtv1.smt2 regress0/aufbv/dubreva005ue.delta01.smtv1.smt2 regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2 @@ -468,6 +469,7 @@ set(regress_0_tests regress0/datatypes/bug597-rbt.smt2 regress0/datatypes/bug604.smt2 regress0/datatypes/bug625.smt2 + regress0/datatypes/canExp-dtPendingMerge.smt2 regress0/datatypes/cdt-model-cade15.smt2 regress0/datatypes/cdt-non-canon-stream.smt2 regress0/datatypes/coda_simp_model.smt2 @@ -1084,6 +1086,7 @@ set(regress_0_tests regress0/sets/pre-proc-univ.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 + regress0/sets/sets-deq-dd.smt2 regress0/sets/sets-equal.smt2 regress0/sets/sets-extr.smt2 regress0/sets/sets-inter.smt2 @@ -1542,10 +1545,12 @@ set(regress_1_tests regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 + regress1/cee-bug0909-dd-scope.smt2 regress1/constarr3.cvc regress1/constarr3.smt2 regress1/cores/issue5604.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 + regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 regress1/datatypes/dt-param-card4-unsat.smt2 regress1/datatypes/error.cvc @@ -1734,6 +1739,7 @@ set(regress_1_tests regress1/push-pop/arith_lra_02.smt2 regress1/push-pop/bug-fmf-fun-skolem.smt2 regress1/push-pop/bug216.smt2 + regress1/push-pop/cee-prs-small.smt2 regress1/push-pop/fuzz_1.smt2 regress1/push-pop/fuzz_10.smt2 regress1/push-pop/fuzz_11.smt2 @@ -1813,6 +1819,8 @@ set(regress_1_tests regress1/quantifiers/burns13.smt2 regress1/quantifiers/burns4.smt2 regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 + regress1/quantifiers/cee-npnt-dd.smt2 + regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 regress1/quantifiers/const.cvc regress1/quantifiers/constfunc.cvc @@ -2088,6 +2096,7 @@ set(regress_1_tests regress1/strings/bug686dd.smt2 regress1/strings/bug768.smt2 regress1/strings/bug799-min.smt2 + regress1/strings/cee-norn-aes-trivially.smt2 regress1/strings/chapman150408.smt2 regress1/strings/cmu-2db2-extf-reg.smt2 regress1/strings/cmu-5042-0707-2.smt2 @@ -2482,6 +2491,7 @@ set(regress_2_tests regress2/piVC_5581bd.smt2 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 + regress2/quantifiers/cee-event-wrong-sat.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2722,6 +2732,7 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 diff --git a/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 new file mode 100644 index 000000000..fa91fe7de --- /dev/null +++ b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () (Array (_ BitVec 1) (_ BitVec 16))) +(assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1))))))) +(check-sat) diff --git a/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 new file mode 100644 index 000000000..d81c3723d --- /dev/null +++ b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) )))) +(declare-fun w () T) +(declare-fun u () T) +(assert (= w (B (D u) (B (D u) (C w))))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-deq-dd.smt2 b/test/regress/regress0/sets/sets-deq-dd.smt2 new file mode 100644 index 000000000..17ca1fce2 --- /dev/null +++ b/test/regress/regress0/sets/sets-deq-dd.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun S () (Set (_ BitVec 1))) +(assert (not (= S (as emptyset (Set (_ BitVec 1)))))) +(check-sat) diff --git a/test/regress/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/regress1/cee-bug0909-dd-scope.smt2 new file mode 100644 index 000000000..6ce621a98 --- /dev/null +++ b/test/regress/regress1/cee-bug0909-dd-scope.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((x5 0)) (((x3) (x4)))) +(declare-sort x 0) +(declare-sort x1 0) +(declare-datatypes ((x22 0)) (((x2)))) +(declare-datatypes ((x2 0)) (((x2 (x2 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int))))) +(declare-sort x30 0) +(declare-sort x3 0) +(declare-datatypes ((x4 0)) (((x44 (x43 x3))))) +(declare-fun x46 (x3) x1) +(declare-datatypes ((x54 0)) (((x49 (x48 x22)) (x5 (x5 x2)) (d (s x1))))) +(declare-fun x5 (x22) x2) +(declare-fun x67 () (Array x x54)) +(declare-fun x6 () (Array x x54)) +(declare-fun x7 () (Array x30 x4)) +(declare-fun x63 () x30) +(declare-fun x () x) +(assert (distinct x3 (ite (or (distinct x6 (store x67 x (d (x46 (x43 (select x7 x63)))))) (= x67 (store x67 x (x5 (x2 x4 x3 (x25 (x5 (x48 (select x67 x)))) (x26 (x5 (x48 (select x67 x)))) (x27 (x5 (x48 (select x6 x))))))))) x3 x4))) +(check-sat) diff --git a/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 new file mode 100644 index 000000000..fe422d9e4 --- /dev/null +++ b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((r 0)) (((R (x Int))))) +(declare-datatype t ((M (t1 (Array Int Int)) (t2 (Array Int Int))))) +(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y t))))) +(declare-fun z () q) +(assert (= z (R ((as const (Array Int r)) (R 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0))))) +(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1))) +(check-sat) diff --git a/test/regress/regress1/push-pop/cee-prs-small.smt2 b/test/regress/regress1/push-pop/cee-prs-small.smt2 new file mode 100644 index 000000000..4c0b06764 --- /dev/null +++ b/test/regress/regress1/push-pop/cee-prs-small.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -i --ee-mode=distributed +; COMMAND-LINE: -i --ee-mode=central +; EXPECT: sat +; EXPECT: unsat +(set-logic ALL) +(declare-datatypes ((r 0)) (((r_ctor (x Int))))) +(declare-datatype tup ((mkt (t1 (Array Int Int)) (t2 (Array Int Int))))) +(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y tup))))) +(declare-fun z () q) +(assert (not (= 1 (select (t2 (y z)) 1)))) +(assert (= z (R ((as const (Array Int r)) (r_ctor 0)) (mkt ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0))))) +(check-sat) +(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 new file mode 100644 index 000000000..15727589d --- /dev/null +++ b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(set-option :fmf-bound true) +(declare-datatype N ((o) (f) (s))) +(declare-datatype P ((P))) +(declare-fun G (N P Int) Bool) +(declare-datatype c ((c (_p P)))) +(declare-fun g (N Int Int) c) +(assert (forall ((x N)) (not (G x P 0)))) +(assert (forall ((t Int)) (or (< t 0) (> t 1) (and (forall ((p P)) (or (exists ((y N)) (and (G y (_p (g y 0 0)) t))))))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/cee-os-delta.smt2 b/test/regress/regress1/quantifiers/cee-os-delta.smt2 new file mode 100644 index 000000000..803291aa3 --- /dev/null +++ b/test/regress/regress1/quantifiers/cee-os-delta.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed +; COMMAND-LINE: --full-saturate-quant --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(declare-fun o (Int) Int) +(declare-fun f (Int Int) Int) +(assert (forall ((x Int)) (forall ((y Int)) (! (= 1 (* y (div y y))) :pattern ((f x y)))))) +(assert (= 0 (f (o 0) (o 1)))) +(check-sat) diff --git a/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 new file mode 100644 index 000000000..2f8d9904d --- /dev/null +++ b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed +; COMMAND-LINE: --arith-eq-solver --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(declare-fun v () String) +(assert (str.in_re (str.++ "" v) (re.* (str.to_re "z")))) +(assert (str.in_re v (re.* (re.range "a" "u")))) +(assert (not (str.in_re v (str.to_re "")))) +(check-sat) diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 new file mode 100644 index 000000000..c0b3aac7c --- /dev/null +++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed +; COMMAND-LINE: --full-saturate-quant --ee-mode=central +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T)))) +(declare-datatypes ((T@$Location 0)) (((P) (G (|t# | T@$TypeValue) (|a#G| Int))))) +(declare-sort |T@[Int]$Value| 0) +(declare-datatypes ((T@$Value 0) (T@R 0)) (((E) ($Boolean (|b#$Boolean| Bool)) (I (|i#I| Int)) (D (|a#D| Int)) (V (|v#V| T@R))) ((R (|v#R| |T@[Int]$Value|) (|l#R| Int))))) +(declare-sort b 0) +(declare-sort l 0) +(declare-datatypes ((T@M 0)) (((M (|domain#M| b) (|contents#M| l))))) +(declare-fun $EmptyValueArray () T@R) +(declare-fun m (T@$Value) |T@[Int]$Value|) +(declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool) +(declare-fun sel (|T@[Int]$Value| Int) T@$Value) +(declare-fun st (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|) +(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?x2 T@$Value)) (= ?x2 (sel (st ?x0 ?x1 ?x2) ?x1)))) +(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?y1 Int) (?x2 T@$Value)) (= (sel ?x0 ?y1) (sel (st ?x0 ?x1 ?x2) ?y1)))) +(declare-fun $LibraAccount_T_type_value () T@$TypeValue) +(declare-fun s (l T@$Location) T@$Value) +(declare-fun $Event_EventHandleGenerator_counter () Int) +(declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue) +(assert (= 0 (|l#R| $EmptyValueArray))) +(assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i)))))))) +(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid))) +(declare-fun |Select_[$Location]$bool| (b T@$Location) Bool) +(declare-fun $m@@0 () T@M) +(declare-fun $abort_flag@2 () Bool) +(declare-fun $m@3 () T@M) +(declare-fun mv () T@$TypeValue) +(declare-fun inline$$MoveToRaw$0$a@0 () Int) +(declare-fun |Store_[$Location]$bool| (b T@$Location Bool) b) +(assert (forall ((?x0 b) (?x1 T@$Location) (?y1 T@$Location) (?x2 Bool)) (or (= ?x1 ?y1) (= (|Select_[$Location]$bool| ?x0 ?y1) (|Select_[$Location]$bool| (|Store_[$Location]$bool| ?x0 ?x1 ?x2) ?y1))))) +(declare-fun inline$$MoveToRaw$0$l@1 () T@$Location) +(declare-fun |Store_[$Location]$Value| (l T@$Location T@$Value) l) +(assert (forall ((?x0 l) (?x1 T@$Location) (?x2 T@$Value)) (= ?x2 (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?x1)))) +(assert (forall ((?x0 l) (?x1 T@$Location) (?y1 T@$Location) (?x2 T@$Value)) (= (s ?x0 ?y1) (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?y1)))) +(declare-fun inline$$Event_EventHandleGenerator_pack$0$$struct@1 () T@$Value) +(declare-fun inline$$Event_publish_generator$0$$tmp@1 () T@$Value) +(declare-fun i () T@$Value) +(assert (and (not $abort_flag@2) (= inline$$Event_publish_generator$0$$tmp@1 (I 0)) (|b#$Boolean| ($Boolean (forall ((addr@@9 T@$Value)) (or (is-D addr@@9) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@9))))))))))) (or (not (=> $abort_flag@2 (|b#$Boolean| ($Boolean (forall ((addr@@4 T@$Value)) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@4)))))))))))))))) (and (= inline$$Event_EventHandleGenerator_pack$0$$struct@1 (V (R (st (st (m E) 0 inline$$Event_publish_generator$0$$tmp@1) 1 i) 1))) (not (=> (= inline$$MoveToRaw$0$a@0 (|a#D| i)) (= inline$$MoveToRaw$0$l@1 (G mv inline$$MoveToRaw$0$a@0)) (or (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| i))))) (not (= $m@3 (M (|Store_[$Location]$bool| (|domain#M| $m@@0) inline$$MoveToRaw$0$l@1 true) (|Store_[$Location]$Value| (|contents#M| $m@@0) inline$$MoveToRaw$0$l@1 inline$$Event_EventHandleGenerator_pack$0$$struct@1)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (|v#R| $EmptyValueArray) 0)) 1))))) (or (not (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (st (|v#R| $EmptyValueArray) (|l#R| $EmptyValueArray) (I 0)) 1)) 0)))))) (and (|b#$Boolean| ($Boolean (forall ((addr@@1 T@$Value)) (|b#$Boolean| ($Boolean (or (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@1)))))) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean ($IsEqual_stratified (sel (|v#R| (|v#V| (s (|contents#M| $m@3) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter)))))))))))) (|b#$Boolean| ($Boolean (forall ((addr@@3 T@$Value)) (|b#$Boolean| ($Boolean (or (|b#$Boolean| ($Boolean ($IsEqual_stratified (I 0) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| addr@@3))))) $Event_EventHandleGenerator_counter)))) (not (|b#$Boolean| ($Boolean (and (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@3) (G mv (|a#D| addr@@3))))) (|b#$Boolean| ($Boolean (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G $LibraAccount_T_type_value (|a#D| addr@@3)))))))))))))))))))))))))))) +(check-sat) diff --git a/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 new file mode 100644 index 000000000..7f2e3084f --- /dev/null +++ b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --ee-mode=distributed --no-check-unsat-cores +; COMMAND-LINE: --ee-mode=central --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((dA 0)) (((A)))) +(declare-datatypes ((Loc 0)) (((G (g dA) (ag Int))))) +(declare-sort v 0) +(declare-datatypes ((T 0) (U 0)) (((E) (I (ii Int)) (D (d Int)) (V (vv U))) ((R (rr v))))) +(declare-sort b 0) +(declare-sort l 0) +(declare-datatypes ((T@M 0)) (((M (dom b) (cnt l))))) +(declare-fun e () U) +(declare-fun m (T) v) +(declare-fun iseq (T T) Bool) +(declare-fun sel (v Int) T) +(declare-fun st (v) v) +(declare-fun s (l Loc) T) +(declare-fun sb (Loc) Bool) +(declare-fun m0 () T@M) +(declare-fun a () Bool) +(declare-fun im () Loc) +(declare-fun o (Loc T) l) +(declare-fun i () T) +(assert (forall ((?x0 v) (?x1 Int) (?x2 T)) (= ?x2 (sel (st ?x0) ?x1)))) +(assert (forall ((v1 T) (v2 T)) (= (iseq v1 v2) (forall ((i Int)) (iseq (sel (rr (vv v1)) i) (sel (rr (vv v2)) i)))))) +(assert (forall ((?x1 Loc) (?x2 T)) (= ?x2 (s (o ?x1 ?x2) ?x1)))) +(assert (and +(not a) +(forall ((?a9 T)) (or (is-D ?a9) (sb (G A (d ?a9))))) +(or +(not (=> a (forall (($a T)) (sb (G A (d $a)))))) +(and + (not (sb (G A (d i)))) + (= im (G A (d (I 0)))) + (= m0 (M (dom m0) (o im (V (R (st (m E))))))) + (iseq (s (cnt m0) (G A (d i))) (V (R (rr e)))) + (or + (exists ((?a1 T)) (not (iseq (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0) (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0)))) + (forall ((?a3 T)) (sb (G A (d ?a3))))))))) +(check-sat) -- 2.30.2