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);
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);
+ }
}
};
/** 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
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++)
#define CVC4__THEORY__DECISION_MANAGER__H
#include <map>
+#include "context/cdlist.h"
#include "theory/decision_strategy.h"
namespace CVC4 {
*/
class DecisionManager
{
+ typedef context::CDList<DecisionStrategy*> DecisionStrategyList;
+
public:
enum StrategyId
{
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
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
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);
}
}
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),
// 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
}/* 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
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());
}
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
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff