Support context-(in)dependent decision strategies. (#3281)

9 files changed, 134 insertions, 22 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9f06950bd..003bb0d68 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -112,7 +112,8 @@ TheoryArrays::TheoryArrays(context::Context* c,
       d_arrayMerges(c),
       d_inCheckModel(false),
       d_proofReconstruction(&d_equalityEngine),
-      d_dstrat(new TheoryArraysDecisionStrategy(this))
+      d_dstrat(new TheoryArraysDecisionStrategy(this)),
+      d_dstratInit(false)
 {
   smtStatisticsRegistry()->registerStat(&d_numRow);
   smtStatisticsRegistry()->registerStat(&d_numExt);
@@ -1252,9 +1253,15 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
 void TheoryArrays::presolve()
 {
   Trace("arrays")<<"Presolving \n";
-  // add the decision strategy
-  getDecisionManager()->registerStrategy(DecisionManager::STRAT_ARRAYS,
-                                         d_dstrat.get());
+  if (!d_dstratInit)
+  {
+    d_dstratInit = true;
+    // add the decision strategy, which is user-context-independent
+    getDecisionManager()->registerStrategy(
+        DecisionManager::STRAT_ARRAYS,
+        d_dstrat.get(),
+        DecisionManager::STRAT_SCOPE_CTX_INDEPENDENT);
+  }
 }
 
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index be80a081d..3d6d0692e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -474,6 +474,8 @@ class TheoryArrays : public Theory {
   };
   /** an instance of the above decision strategy */
   std::unique_ptr<TheoryArraysDecisionStrategy> d_dstrat;
+  /** Have we registered the above strategy? (context-independent) */
+  bool d_dstratInit;
   /** get the next decision request
    *
    * If the "arrays-eager-index" option is enabled, then whenever a
diff --git a/src/theory/decision_manager.cpp b/src/theory/decision_manager.cpp
index 3eda45b00..a2aee5d40 100644
--- a/src/theory/decision_manager.cpp
+++ b/src/theory/decision_manager.cpp
@@ -22,27 +22,68 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-DecisionManager::DecisionManager(context::Context* satContext) {}
+DecisionManager::DecisionManager(context::Context* userContext)
+    : d_strategyCacheC(userContext)
+{
+}
 
-void DecisionManager::reset()
+void DecisionManager::presolve()
 {
-  Trace("dec-manager") << "DecisionManager: reset." << std::endl;
+  Trace("dec-manager") << "DecisionManager: presolve." << std::endl;
+  // remove the strategies that are not in this user context
+  std::unordered_set<DecisionStrategy*> active;
+  for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin();
+       i != d_strategyCacheC.end();
+       ++i)
+  {
+    active.insert(*i);
+  }
+  active.insert(d_strategyCache.begin(), d_strategyCache.end());
+  std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy;
   d_reg_strategy.clear();
+  for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp)
+  {
+    for (DecisionStrategy* ds : rs.second)
+    {
+      if (active.find(ds) != active.end())
+      {
+        // if its active, we keep it
+        d_reg_strategy[rs.first].push_back(ds);
+      }
+    }
+  }
 }
 
-void DecisionManager::registerStrategy(StrategyId id, DecisionStrategy* ds)
+void DecisionManager::registerStrategy(StrategyId id,
+                                       DecisionStrategy* ds,
+                                       StrategyScope sscope)
 {
   Trace("dec-manager") << "DecisionManager: Register strategy : "
                        << ds->identify() << ", id = " << id << std::endl;
   ds->initialize();
   d_reg_strategy[id].push_back(ds);
+  if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT)
+  {
+    // store it in the user-context-dependent list
+    d_strategyCacheC.push_back(ds);
+  }
+  else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT)
+  {
+    // it is context independent
+    d_strategyCache.insert(ds);
+  }
+  else
+  {
+    // it is local to this call, we don't cache it
+    Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE);
+  }
 }
 
 Node DecisionManager::getNextDecisionRequest()
 {
   Trace("dec-manager-debug")
       << "DecisionManager: Get next decision..." << std::endl;
-  for (const std::pair<StrategyId, std::vector<DecisionStrategy*> >& rs :
+  for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs :
        d_reg_strategy)
   {
     for (unsigned i = 0, size = rs.second.size(); i < size; i++)
diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h
index 6825c1cf4..da040a7f7 100644
--- a/src/theory/decision_manager.h
+++ b/src/theory/decision_manager.h
@@ -19,6 +19,7 @@
 #define CVC4__THEORY__DECISION_MANAGER__H
 
 #include <map>
+#include "context/cdlist.h"
 #include "theory/decision_strategy.h"
 
 namespace CVC4 {
@@ -46,6 +47,8 @@ namespace theory {
  */
 class DecisionManager
 {
+  typedef context::CDList<DecisionStrategy*> DecisionStrategyList;
+
  public:
   enum StrategyId
   {
@@ -83,21 +86,42 @@ class DecisionManager
 
     STRAT_LAST
   };
-  DecisionManager(context::Context* satContext);
+  /** The scope of a strategy, used in registerStrategy below */
+  enum StrategyScope
+  {
+    // The strategy is user-context dependent, that is, it is cleared when
+    // the user context is popped.
+    STRAT_SCOPE_USER_CTX_DEPENDENT,
+    // The strategy is local to a check-sat call, that is, it is cleared on
+    // a call to presolve.
+    STRAT_SCOPE_LOCAL_SOLVE,
+    // The strategy is context-independent.
+    STRAT_SCOPE_CTX_INDEPENDENT,
+  };
+  DecisionManager(context::Context* userContext);
   ~DecisionManager() {}
-  /** reset the strategy
+  /** presolve
    *
-   * This clears all decision strategies that are registered to this manager.
+   * This clears all decision strategies that are registered to this manager
+   * that no longer exist in the current user context.
    * We require that each satisfiability check beyond the first calls this
-   * function exactly once. Currently, it is called during
-   * TheoryEngine::postSolve.
+   * function exactly once. It is called during TheoryEngine::presolve.
    */
-  void reset();
+  void presolve();
   /**
    * Registers the strategy ds with this manager. The id specifies when the
-   * strategy should be run.
+   * strategy should be run. The argument sscope indicates the scope of the
+   * strategy, i.e. how long it persists.
+   *
+   * Typically, strategies that are user-context-dependent are those that are
+   * in response to an assertion (e.g. a strategy that decides that a sygus
+   * conjecture is feasible). An example of a strategy that is context
+   * independent is the combined cardinality decision strategy for finite model
+   * finding for UF, which is not specific to any formula/type.
    */
-  void registerStrategy(StrategyId id, DecisionStrategy* ds);
+  void registerStrategy(StrategyId id,
+                        DecisionStrategy* ds,
+                        StrategyScope sscope = STRAT_SCOPE_USER_CTX_DEPENDENT);
   /** Get the next decision request
    *
    * If this method returns a non-null node n, then n is a literal corresponding
@@ -111,6 +135,10 @@ class DecisionManager
  private:
   /** Map containing all strategies registered to this manager */
   std::map<StrategyId, std::vector<DecisionStrategy*> > d_reg_strategy;
+  /** Set of decision strategies in this user context */
+  DecisionStrategyList d_strategyCacheC;
+  /** Set of decision strategies that are context independent */
+  std::unordered_set<DecisionStrategy*> d_strategyCache;
 };
 
 }  // namespace theory
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 65f06c008..0f9a78516 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -570,8 +570,12 @@ void TheoryStrings::presolve() {
       inputVars.push_back(*itr);
     }
     d_sslds->initialize(inputVars);
+    // This strategy is local to a check-sat call, since we refresh the strategy
+    // on every call to presolve.
     getDecisionManager()->registerStrategy(
-        DecisionManager::STRAT_STRINGS_SUM_LENGTHS, d_sslds.get());
+        DecisionManager::STRAT_STRINGS_SUM_LENGTHS,
+        d_sslds.get(),
+        DecisionManager::STRAT_SCOPE_LOCAL_SOLVE);
   }
 }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8348c24d5..5d185ad9d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -274,7 +274,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
-      d_decManager(new DecisionManager(context)),
+      d_decManager(new DecisionManager(userContext)),
       d_curr_model(nullptr),
       d_aloc_curr_model(false),
       d_curr_model_builder(nullptr),
@@ -910,6 +910,10 @@ bool TheoryEngine::presolve() {
   // Reset the interrupt flag
   d_interrupted = false;
 
+  // Reset the decision manager. This clears its decision strategies that are
+  // no longer valid in this user context.
+  d_decManager->presolve();
+
   try {
     // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -933,9 +937,6 @@ bool TheoryEngine::presolve() {
 }/* TheoryEngine::presolve() */
 
 void TheoryEngine::postsolve() {
-  // Reset the decision manager. This clears its decision strategies, which are
-  // user-context-dependent.
-  d_decManager->reset();
   // no longer in SAT mode
   d_inSatMode = false;
   // Reset the interrupt flag
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 94e5f67c1..87696ef5f 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -504,6 +504,8 @@ void SortModel::initialize( OutputChannel* out ){
   if (d_c_dec_strat.get() != nullptr && !d_initialized)
   {
     d_initialized = true;
+    // Strategy is user-context-dependent, since it is in sync with
+    // user-context-dependent flag d_initialized.
     d_thss->getTheory()->getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get());
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c456ed2e8..a97670446 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1820,6 +1820,7 @@ set(regress_2_tests
   regress2/strings/norn-dis-0707-3.smt2
   regress2/strings/range-perf.smt2
   regress2/strings/repl-repl.smt2
+  regress2/strings/repl-repl-i-no-push.smt2
   regress2/strings/replaceall-diffrange.smt2
   regress2/strings/replaceall-len-c.smt2
   regress2/strings/small-1.smt2
diff --git a/test/regress/regress2/strings/repl-repl-i-no-push.smt2 b/test/regress/regress2/strings/repl-repl-i-no-push.smt2
new file mode 100644
index 000000000..0076af392
--- /dev/null
+++ b/test/regress/regress2/strings/repl-repl-i-no-push.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --strings-exp --strings-fmf --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic SLIA)
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+
+(assert (not (= (str.replace (str.replace x "B" x) x "AB") (str.replace (str.replace x "B" "AB") x "AB"))))
+(check-sat)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x "B" x) x "A") (str.replace (str.replace x "B" "A") x "A"))))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
+(check-sat)
+(pop 1)
+
+(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
+(assert (<= (str.len y) (str.len z)))
+(check-sat)