Enable new justification heuristic by default (#6613)

This enables the new implementation of justification heuristic by default.

Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index e891cf8cf1801ee2587bc45a819351ae5521b90c..ea3b2dde10eb4739ce74563e28bcd2fa368fb2fc 100755 (executable)
--- 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 4116ba90d6986caa9b016679bc2b3d618b058516..d439f33a68508fae47a38fa227e68fb75d46e3b6 100644 (file)
--- 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 de88d656e4fd5d09aba3aea41474c256da9d519e..e54e1fc3c42998a9d34005fc881f8dd19df0c6ca 100644 (file)
--- 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 80fca23d5189d17ad96ac4403b365127781b4152..b73b24bd08815e42baf5213450a4a00d494141ce 100644 (file)
--- 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 2fa216487c3b13ff566f5c4eddc178ff0a2b5c7f..667f531157a86b61d99e4e3701167d6b9eaf9406 100644 (file)
--- 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 4f3f91ba53327f895b33efd2a97ab2cc1b3bbd6d..796fd26fa8ff2c3ba96dfead8c9247456c7e8dfc 100644 (file)
--- 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 41019d58ee7645208764ff58ad2efe5bd873f72b..fd86d3a42e214e64426fbaf05f698dde522c91a9 100644 (file)
--- 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 605c75a14cda149b2c284922a60af58ac9f1d5a7..b0eab66e914ec83a2e131c8eb3520c2bb59b10fa 100644 (file)
--- 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 89006d154d0a8a895ce409d2c00a1a10c248483e..7176126fbe0a9642c6336c9c80469fd71a4bb741 100644 (file)
--- 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 01deeaedef4dbb526f5ca7b1113043193aaf4c9e..a3244ff4a752e4f63d1d1be267afdc31edfd83d7 100644 (file)
--- 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 99e6b04d5cc00032d1b97528ce02525af9339d0b..0342fc90cdd1a9a69f2d946b3d07b97887db8db7 100644 (file)
--- 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 55269e123fc63ffc23c52a616e58a0ffa5ae4371..3e0858035eafa36be1795cac6ec5d244b60eb632 100644 (file)
--- 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 5c39abc5f5abc0bf0ec5203a1160705fc95ef44a..6a516a3ca3e23bbdabcbba688fab929637befb45 100644 (file)
--- 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 2bd27093fb4e0b3d3fd6851504bc378590c0e107..9feada28088bbc838513f3e22528b8b4dcde162c 100644 (file)
--- 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 (file)
index 0000000..d943a00
--- /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 (file)
index 0000000..5c8c826
--- /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 (file)
index 0000000..0eadf34
--- /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 (file)
index 0000000..1bf48a1
--- /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 (file)
index 0000000..31b72e7
--- /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 (file)
index 0000000..9bdcf56
--- /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 (file)
index 0000000..d833565
--- /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 (file)
index 0000000..3cfb154
--- /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 (file)
index 0000000..6095a49
--- /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 (file)
index 0000000..fbd200f
--- /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 (file)
index 0000000..8497a66
--- /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 61f0f207be0f0093903d89bbd7602fd9696d80ac..21405dfdbcd53f0809781678c0e7d86829c7443d 100644 (file)
--- 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 45727743fd1939e20dc4b450e7c4a22a15c2abd1..796d7e753fd050c4619d0cd86f83f444dd24ed9a 100644 (file)
--- 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 3ee748d276d78da45af58ddb7e2dd4fc9ca96e3b..a86ce1fe5a3438f3a41eb69324b33e5cb20eee7e 100644 (file)
--- 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 c01d3f2350c371c2666892d4da3074b38d33a7e2..b9537fd0e13d585e5bc037da3da421dc09458e70 100644 (file)
--- 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,(