--decision=justification-stoponly : use decision engine only for stopping

search early, not to make decisions

new options.h :)

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 93f8c0a5d3a61bb9a5050cf6c0c49091158f4eb1..15a383d92bae561157889691432c0e5d1175b1ac 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -92,7 +92,7 @@ SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
   if(stopSearch) {
     Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
   }
-  return ret;
+  return Options::current()->decisionOptions.stopOnly ? undefSatLiteral : ret;
 }
 
 bool TheoryProxy::theoryNeedCheck() const {

diff --git a/src/util/options.cpp b/src/util/options.cpp
index c912023ad35eb63250fe252d2cf4d116443f402e..b9291f59c873930219d41878950dd33e075654f2 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -64,6 +64,7 @@ const Options::DecisionOptions defaultDecOpt = {
   1000,                         // maxRelTimeAsPermille
   true,                         // computeRelevancy
   false,                        // mustRelevancy
+  false,                        // stopOnly
 };
 
 Options::Options() :
@@ -355,6 +356,9 @@ internal (default)\n\
 justification\n\
 + An ATGP-inspired justification heuristic\n\
 \n\
+justification-stoponly\n\
++ Use the justification heuristic only to stop early, not for decisions\n\
+\n\
 relevancy\n\
 + Under development may-relevancy\n\
 \n\
@@ -1012,12 +1016,17 @@ throw(OptionException) {
       }
       break;
     case DECISION_MODE:
+      decisionOptions = defaultDecOpt;  // reset all options
       if(!strcmp(optarg, "internal")) {
         decisionMode = DECISION_STRATEGY_INTERNAL;
         decisionModeSetByUser = true;
       } else if(!strcmp(optarg, "justification")) {
         decisionMode = DECISION_STRATEGY_JUSTIFICATION;
         decisionModeSetByUser = true;
+      } else if(!strcmp(optarg, "justification-stoponly")) {
+        decisionMode = DECISION_STRATEGY_JUSTIFICATION;
+        decisionModeSetByUser = true;
+        decisionOptions.stopOnly = true;
       } else if(!strcmp(optarg, "relevancy")) {
         decisionMode = DECISION_STRATEGY_RELEVANCY;
         decisionModeSetByUser = true;

diff --git a/src/util/options.h b/src/util/options.h
index bc99b5febbf1c4489b12c3adbde47d6822195cad..ac95c99cae3b16b52f09d96febaf2b3f040c7841 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -156,6 +156,7 @@ struct CVC4_PUBLIC Options {
     unsigned short maxRelTimeAsPermille;  /* permille = part per thousand */
     bool computeRelevancy;    /* if false, do justification stuff using relevancy.h */
     bool mustRelevancy;       /* use the must be relevant */
+    bool stopOnly;            /* only use decision stuff to stop early, not to decide */
   };
   DecisionOptions decisionOptions;