diff options
29 files changed, 240 insertions, 21 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index e891cf8cf..ea3b2dde1 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -162,8 +162,8 @@ QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) - trywith 300 --strings-exp --rewrite-divk --strings-fmf - finishwith --strings-exp --rewrite-divk + trywith 300 --strings-exp --rewrite-divk --strings-fmf --no-jh-rlv-order + finishwith --strings-exp --rewrite-divk --no-jh-rlv-order ;; QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 4116ba90d..d439f33a6 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -27,8 +27,9 @@ DecisionEngine::DecisionEngine(context::Context* c, prop::SkolemDefManager* skdm, ResourceManager* rm) : d_decEngineOld(new DecisionEngineOld(c, u)), + d_jstrat(new JustificationStrategy(c, u, skdm)), d_resourceManager(rm), - d_useOld(true) + d_useOld(options::decisionMode() != options::DecisionMode::JUSTIFICATION) { } @@ -41,9 +42,16 @@ void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss, d_decEngineOld->setCnfStream(cs); return; } + d_jstrat->finishInit(ss, cs); } -void DecisionEngine::presolve() {} +void DecisionEngine::presolve() +{ + if (!d_useOld) + { + d_jstrat->presolve(); + } +} prop::SatLiteral DecisionEngine::getNext(bool& stopSearch) { @@ -52,7 +60,7 @@ prop::SatLiteral DecisionEngine::getNext(bool& stopSearch) { return d_decEngineOld->getNext(stopSearch); } - return undefSatLiteral; + return d_jstrat->getNext(stopSearch); } bool DecisionEngine::isDone() @@ -61,7 +69,7 @@ bool DecisionEngine::isDone() { return d_decEngineOld->isDone(); } - return false; + return d_jstrat->isDone(); } void DecisionEngine::addAssertion(TNode assertion) @@ -71,6 +79,7 @@ void DecisionEngine::addAssertion(TNode assertion) d_decEngineOld->addAssertion(assertion); return; } + d_jstrat->addAssertion(assertion); } void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) @@ -79,6 +88,10 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) { d_decEngineOld->addSkolemDefinition(lem, skolem); } + else + { + d_jstrat->addSkolemDefinition(lem, skolem); + } } void DecisionEngine::notifyAsserted(TNode n) @@ -87,6 +100,8 @@ void DecisionEngine::notifyAsserted(TNode n) { return; } + // old implementation does not use this + d_jstrat->notifyAsserted(n); } } // namespace decision diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index de88d656e..e54e1fc3c 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -18,6 +18,7 @@ #ifndef CVC5__DECISION__DECISION_ENGINE_H #define CVC5__DECISION__DECISION_ENGINE_H +#include "decision/justification_strategy.h" #include "expr/node.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" @@ -60,7 +61,7 @@ class DecisionEngine */ void addAssertion(TNode assertion); /** - * TODO: remove this interface + * !!!! temporary until the old justification implementation is deleted. * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ @@ -74,6 +75,8 @@ class DecisionEngine private: /** The old implementation */ std::unique_ptr<DecisionEngineOld> d_decEngineOld; + /** The new implementation */ + std::unique_ptr<JustificationStrategy> d_jstrat; /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; /** using old implementation? */ diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index 80fca23d5..b73b24bd0 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -64,12 +64,13 @@ void JustificationStrategy::presolve() d_stack.clear(); } -SatLiteral JustificationStrategy::getNext() +SatLiteral JustificationStrategy::getNext(bool& stopSearch) { // ensure we have an assertion if (!refreshCurrentAssertion()) { Trace("jh-process") << "getNext, already finished" << std::endl; + stopSearch = true; return undefSatLiteral; } Assert(d_stack.hasCurrentAssertion()); @@ -210,6 +211,7 @@ SatLiteral JustificationStrategy::getNext() } while (d_stack.hasCurrentAssertion()); // we exhausted all assertions Trace("jh-process") << "...exhausted all assertions" << std::endl; + stopSearch = true; return undefSatLiteral; } @@ -482,6 +484,7 @@ bool JustificationStrategy::isDone() { return !refreshCurrentAssertion(); } void JustificationStrategy::addAssertion(TNode assertion) { + Trace("jh-assert") << "addAssertion " << assertion << std::endl; std::vector<TNode> toProcess; toProcess.push_back(assertion); insertToAssertionList(toProcess, false); @@ -489,6 +492,8 @@ void JustificationStrategy::addAssertion(TNode assertion) void JustificationStrategy::addSkolemDefinition(TNode lem, TNode skolem) { + Trace("jh-assert") << "addSkolemDefinition " << lem << " / " << skolem + << std::endl; if (d_jhSkRlvMode == options::JutificationSkolemRlvMode::ALWAYS) { // just add to main assertions list @@ -565,6 +570,7 @@ void JustificationStrategy::insertToAssertionList(std::vector<TNode>& toProcess, bool JustificationStrategy::refreshCurrentAssertion() { + Trace("jh-process") << "refreshCurrentAssertion" << std::endl; // if we already have a current assertion, nothing to be done TNode curr = d_stack.getCurrentAssertion(); if (!curr.isNull()) @@ -601,6 +607,7 @@ bool JustificationStrategy::refreshCurrentAssertionFromList(bool useSkolemList) SatValue currValue; while (!curr.isNull()) { + Trace("jh-process") << "Check assertion " << curr << std::endl; // we never add theory literals to our assertions lists Assert(!isTheoryLiteral(curr)); currValue = lookupValue(curr); diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h index 2fa216487..667f53115 100644 --- a/src/decision/justification_strategy.h +++ b/src/decision/justification_strategy.h @@ -137,9 +137,10 @@ class JustificationStrategy * all relevant input assertions are already propositionally satisfied by * the current assignment. * + * @param stopSearch Set to true if we can stop the search * @return The next SAT literal to decide on. */ - prop::SatLiteral getNext(); + prop::SatLiteral getNext(bool& stopSearch); /** * Are we finished assigning values to literals? diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index 4f3f91ba5..796fd26fa 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -17,6 +17,9 @@ name = "Decision Heuristics" [[option.mode.JUSTIFICATION]] name = "justification" help = "An ATGP-inspired justification heuristic." +[[option.mode.JUSTIFICATION_OLD]] + name = "justification-old" + help = "Older implementation of an ATGP-inspired justification heuristic." [[option.mode.RELEVANCY]] name = "justification-stoponly" help = "Use the justification heuristic only to stop early, not for decisions." @@ -89,7 +92,7 @@ name = "Decision Heuristics" category = "expert" long = "jh-rlv-order" type = "bool" - default = "false" + default = "true" help = "maintain activity-based ordering for decision justification heuristic" [[option]] diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 41019d58e..fd86d3a42 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1606,7 +1606,10 @@ lbool Solver::search(int nof_conflicts) // If this was a final check, we are satisfiable if (check_type == CHECK_FINAL) { - bool decisionEngineDone = d_proxy->isDecisionEngineDone(); + // Note that we are done making decisions when there are no pending decisions + // on assumptions, and the decision engine indicates it is done. + bool decisionEngineDone = (decisionLevel() >= assumptions.size()) + && d_proxy->isDecisionEngineDone(); // Unless a lemma has added more stuff to the queues if (!decisionEngineDone && (!order_heap.empty() || qhead < trail.size())) diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 605c75a14..b0eab66e9 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -77,6 +77,7 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { TNode assertion = d_queue.front(); d_queue.pop(); d_theoryEngine->assertFact(assertion); + d_decisionEngine->notifyAsserted(assertion); } d_theoryEngine->check(effort); } diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 89006d154..7176126fb 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -930,13 +930,12 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } // should give a proof, if not, then tcpg does not agree with the // substitution. - Assert(pfn != nullptr); if (pfn == nullptr) { - AlwaysAssert(false) << "resort to TRUST_SUBS" << std::endl - << eq << std::endl - << eqq << std::endl - << "from " << children << " applied to " << t; + Warning() << "resort to TRUST_SUBS" << std::endl + << eq << std::endl + << eqq << std::endl + << "from " << children << " applied to " << t << std::endl; cdp->addStep(eqq, PfRule::TRUST_SUBS, {}, {eqq}); } else diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 01deeaede..a3244ff4a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1511,7 +1511,18 @@ set(regress_1_tests regress1/datatypes/tuple_projection.smt2 regress1/decision/bug374a.smtv1.smt2 regress1/decision/error3.smtv1.smt2 + regress1/decision/issue5454-2.smt2 + regress1/decision/issue5454-3.smt2 + regress1/decision/issue5454.smt2 + regress1/decision/issue5785.smt2 + regress1/decision/jh-test1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 + regress1/decision/wishue114.smt2 + regress1/decision/wishue115.smt2 + regress1/decision/wishue116.smt2 + regress1/decision/wishue149-2.smt2 + regress1/decision/wishue149-3.smt2 + regress1/decision/wishue160.smt2 regress1/error.cvc regress1/errorcrash.smt2 regress1/fp/rti_3_5_bug_report.smt2 @@ -2635,6 +2646,8 @@ set(regression_disabled_tests regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 regress2/nl/dumortier-050317.smt2 + # timeout after refactoring justification heuristic + regress2/ho/SYO362^5.p # time out regress3/unifpi-solve-car_1.lus.sy regress3/issue4476-ext-rew.smt2 diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2 index 99e6b04d5..0342fc90c 100644 --- a/test/regress/regress0/arith/div.05.smt2 +++ b/test/regress/regress0/arith/div.05.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_NRA) (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2 index 55269e123..3e0858035 100644 --- a/test/regress/regress0/fp/issue3619.smt2 +++ b/test/regress/regress0/fp/issue3619.smt2 @@ -1,5 +1,5 @@ ; REQUIRES: symfpu -; COMMAND-LINE: +; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FPLRA) (set-info :status sat) diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2 index 5c39abc5f..6a516a3ca 100644 --- a/test/regress/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/regress0/fp/issue4277-assign-func.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat ; REQUIRES: symfpu (set-logic ALL) (set-option :uf-ho true) diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2 index 2bd27093f..9feada280 100644 --- a/test/regress/regress0/issue5099-model-2.smt2 +++ b/test/regress/regress0/issue5099-model-2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -m +; COMMAND-LINE: -m -q ; EXPECT: sat ; EXPECT: ((IP true)) (set-logic QF_NRA) @@ -6,4 +6,4 @@ (declare-const r16 Real) (assert (! (distinct (/ 1 r16) r11) :named IP)) (check-sat) -(get-assignment)
\ No newline at end of file +(get-assignment) diff --git a/test/regress/regress1/decision/issue5454-2.smt2 b/test/regress/regress1/decision/issue5454-2.smt2 new file mode 100644 index 000000000..d943a0020 --- /dev/null +++ b/test/regress/regress1/decision/issue5454-2.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ANIA) +(declare-fun i () Int) +(declare-fun a () (Array Int Bool)) +(declare-fun b () (Array Bool (Array Int Bool))) +(assert (= (store b (>= i 0) a) (store b false (store (store a 0 true) i true)))) +(check-sat) diff --git a/test/regress/regress1/decision/issue5454-3.smt2 b/test/regress/regress1/decision/issue5454-3.smt2 new file mode 100644 index 000000000..5c8c826f2 --- /dev/null +++ b/test/regress/regress1/decision/issue5454-3.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLIA) +(declare-fun v () Bool) +(declare-fun i () Int) +(declare-fun i8 () Int) +(declare-fun u (Int Int Int Int Int Int) Bool) +(declare-fun ar () (Array Bool Bool)) +(declare-fun a () (Array Int Int)) +(declare-fun arr-- () (Array Bool Int)) +(declare-fun arr () (Array Bool (Array Int Bool))) +(declare-fun arr- () (Array Bool (Array Bool (Array Int Bool)))) +(assert (= arr- (store (store arr- false arr) (or (u (- 1) (select a i8) i (- 1) (select arr-- (select ar (= ar (store ar v true)))) 0) (not (u (- 1) (select a i8) i (- 1) (select arr-- (select ar (= ar (store ar v true)))) 0))) arr))) +(check-sat) diff --git a/test/regress/regress1/decision/issue5454.smt2 b/test/regress/regress1/decision/issue5454.smt2 new file mode 100644 index 000000000..0eadf3412 --- /dev/null +++ b/test/regress/regress1/decision/issue5454.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFNIA) +(declare-fun _substvar_298_ () (Array Int Bool)) +(declare-fun _substvar_379_ () (Array Bool (Array Int Bool))) +(declare-fun _substvar_400_ () (Array Bool (Array Int Bool))) +(declare-fun i0 () Int) +(declare-fun arr--325748303185799905_1467848600759014513-0 () (Array Int Bool)) +(declare-fun arr-1467848600759014513_3143370635870088364-0 () (Array Bool (Array Int Bool))) +(assert (= _substvar_400_ (store arr-1467848600759014513_3143370635870088364-0 false (store (store arr--325748303185799905_1467848600759014513-0 776 true) i0 true)) (store arr-1467848600759014513_3143370635870088364-0 (>= i0 776) _substvar_298_) _substvar_379_)) +(check-sat) diff --git a/test/regress/regress1/decision/issue5785.smt2 b/test/regress/regress1/decision/issue5785.smt2 new file mode 100644 index 000000000..1bf48a1b2 --- /dev/null +++ b/test/regress/regress1/decision/issue5785.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fmf-fun -i --decision=justification +; EXPECT: sat +(set-logic ALRA) +(set-option :fmf-fun true) +(declare-fun v2 () Bool) +(declare-sort S0 0) +(declare-fun arr--1494941102250395870_2811598136228140380-0 () (Array Bool S0)) +(declare-fun arr-2811598136228140380_-1494941102250395870-0 () (Array S0 Bool)) +(push) +(assert (select arr-2811598136228140380_-1494941102250395870-0 (select arr--1494941102250395870_2811598136228140380-0 false))) +(push) +(pop) +(pop) +(assert (select arr-2811598136228140380_-1494941102250395870-0 (select (store arr--1494941102250395870_2811598136228140380-0 v2 (select arr--1494941102250395870_2811598136228140380-0 true)) true))) +(check-sat) diff --git a/test/regress/regress1/decision/jh-test1.smt2 b/test/regress/regress1/decision/jh-test1.smt2 new file mode 100644 index 000000000..31b72e787 --- /dev/null +++ b/test/regress/regress1/decision/jh-test1.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ALL) +(declare-const size4 String) +(declare-const p2_size Int) +(assert (= 1 (+ 1 (ite (= 1 p2_size) (str.to_code size4) 0)))) +(check-sat) diff --git a/test/regress/regress1/decision/wishue114.smt2 b/test/regress/regress1/decision/wishue114.smt2 new file mode 100644 index 000000000..9bdcf562d --- /dev/null +++ b/test/regress/regress1/decision/wishue114.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(check-sat) +(assert (and (and v1 v2) (and (or true (and (or false v1) v1)) (or (and false v1) v3)))) +(assert true) +(assert (or (and (or (and (or v4 v4) false) v2) (and true (or (and v5 true) (and v6 v5)))) v2)) +(assert v3) +(check-sat) +(assert false) +(assert true) +(assert (and (or (and v7 (and (and v2 v6) (and false v8))) (and (or (and v8 false) true) (and v6 true))) (and true v3))) +(push) +(assert v7) +(check-sat) +(assert true) +(pop) +(push) +(check-sat) +(check-sat) diff --git a/test/regress/regress1/decision/wishue115.smt2 b/test/regress/regress1/decision/wishue115.smt2 new file mode 100644 index 000000000..d8335654a --- /dev/null +++ b/test/regress/regress1/decision/wishue115.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(check-sat) +(assert (or (not (and (or v1 (and v1 true)) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (and v1 false)))) false)) +(assert (or (or (not true) (and (and (not v1) (or v1 v1)) v1)) (or (and (not (not v2)) (forall ((q0_1 Bool) (q0_2 Bool)) (and q0_2 q0_2))) (and (not (and true v3)) (or (not v1) v2))))) +(check-sat) +(check-sat) +(assert (not (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (and (not (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool) (q1_4 Bool)) false)) (not (forall ((q1_1 Bool)) q0_2)))))) +(assert (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool) (q0_5 Bool)) (not v1))) +(push) +(check-sat) +(assert (and (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool) (q1_4 Bool)) (not (forall ((q2_1 Bool)) true)))) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (not (or q0_3 (forall ((q1_1 Bool)) v4)))))) +(assert (or (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (forall ((q1_1 Bool) (q1_2 Bool) (q1_3 Bool)) (not q1_1))) v1)) +(assert v5) +(check-sat) +(assert (not (forall ((q0_1 Bool)) (and (or (or true q0_1) (and false q0_1)) (not true))))) +(pop) diff --git a/test/regress/regress1/decision/wishue116.smt2 b/test/regress/regress1/decision/wishue116.smt2 new file mode 100644 index 000000000..3cfb1540b --- /dev/null +++ b/test/regress/regress1/decision/wishue116.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(assert (and (or (or (and (or false v1) v2) (not (not v3))) (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool)) (forall ((q1_1 Bool)) q1_1))) true)) +(check-sat) +(assert (or (not v2) (or (and (or (and v4 true) v2) (forall ((q0_1 Bool)) (not true))) (not (forall ((q0_1 Bool) (q0_2 Bool) (q0_3 Bool) (q0_4 Bool)) (forall ((q1_1 Bool) (q1_2 Bool)) v1)))))) +(push) +(assert (not v5)) +(assert (not true)) +(pop) +(push) +(check-sat) +(pop) +(assert true) diff --git a/test/regress/regress1/decision/wishue149-2.smt2 b/test/regress/regress1/decision/wishue149-2.smt2 new file mode 100644 index 000000000..6095a4940 --- /dev/null +++ b/test/regress/regress1/decision/wishue149-2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLIA) +(declare-const v4 Bool) +(declare-const v6 Bool) +(declare-const arr0 (Array Bool Int)) +(declare-const arr1 (Array Bool (Array Bool Int))) +(assert (= (store arr1 v6 (store arr0 true 0)) (store arr1 true (store (store (store arr0 true 0) v4 0) true 96)) arr1 arr1)) +(check-sat) diff --git a/test/regress/regress1/decision/wishue149-3.smt2 b/test/regress/regress1/decision/wishue149-3.smt2 new file mode 100644 index 000000000..fbd200f66 --- /dev/null +++ b/test/regress/regress1/decision/wishue149-3.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic AUFLRA) +(declare-fun _substvar_323_ () Bool) +(declare-sort S0 0) +(declare-const arr-8825057447867329665_7821057345541224443-0 (Array Bool S0)) +(declare-const arr--3985848114402943554_-2673408464765268945-0 (Array Real (Array Bool S0))) +(assert (not (= (select arr--3985848114402943554_-2673408464765268945-0 0.0) (store (store arr-8825057447867329665_7821057345541224443-0 _substvar_323_ (select arr-8825057447867329665_7821057345541224443-0 true)) false (select arr-8825057447867329665_7821057345541224443-0 false)) arr-8825057447867329665_7821057345541224443-0 arr-8825057447867329665_7821057345541224443-0))) +(check-sat) diff --git a/test/regress/regress1/decision/wishue160.smt2 b/test/regress/regress1/decision/wishue160.smt2 new file mode 100644 index 000000000..8497a66fc --- /dev/null +++ b/test/regress/regress1/decision/wishue160.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat +(set-logic ALIA) +(set-option :repeat-simp true) +(set-option :sygus-rr-synth-check true) +(declare-fun v6 () Bool) +(declare-const arr-7579056739068271278_-8074447279386590332-0 (Array Bool Int)) +(assert (= false false false (= arr-7579056739068271278_-8074447279386590332-0 (store arr-7579056739068271278_-8074447279386590332-0 v6 746)) false false false)) +(check-sat) diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 61f0f207b..21405dfdb 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ho --finite-model-find -q +; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 index 45727743f..796d7e753 100644 --- a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 +++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-jh-rlv-order ; REQUIRES: symfpu ; EXPECT: unsat (set-logic AUFBVFPDTNIRA) diff --git a/test/regress/regress2/strings/issue6483.smt2 b/test/regress/regress2/strings/issue6483.smt2 index 3ee748d27..a86ce1fe5 100644 --- a/test/regress/regress2/strings/issue6483.smt2 +++ b/test/regress/regress2/strings/issue6483.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: unsat (set-logic QF_SLIA) (declare-fun a () String) (assert diff --git a/test/regress/regress3/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p index c01d3f235..b9537fd0e 100644 --- a/test/regress/regress3/ho/SYO362^5.p +++ b/test/regress/regress3/ho/SYO362^5.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --decision=justification-old % EXPECT: % SZS status Theorem for SYO362^5 thf(cK,type,( |