Adds the ability to have the SmtSolver automatically deep restart after a criteria is met (we have learned new top-level literals, and a threshold of time since the last learned literal has passed). This can be used for non-incremental satisfiability queries only.
By default, --deep-restart=input kicks in on 155 of our regressions, this adds 4 delta-debugged regressions that exercise the feature.
name = "pre-asserts"
help = "print a benchmark corresponding to the assertions of the input problem before preprocessing"
description = "With ``-o pre-asserts``, cvc5 prints a benchmark corresponding to the assertions of the input problem before preprocessing."
- example-file = "regress0/printer/pre-asserts-output.smt2"
+[[option.mode.DEEP_RESTART]]
+ name = "deep-restart"
+ help = "print when cvc5 performs a deep restart along with the literals it has learned"
+ description = "With ``-o deep-restart``, cvc5 prints when it performs a deep restart along with the literals it has learned."
+ example-file = "regress0/printer/deep-restart-output.smt2"
# Stores then enabled output tags.
[[option]]
type = "bool"
default = "false"
help = "checks whether produced solutions to get-abduct are correct"
+
+[[option]]
+ name = "deepRestartMode"
+ category = "expert"
+ long = "deep-restart=MODE"
+ type = "DeepRestartMode"
+ default = "NONE"
+ help = "mode for deep restarts"
+ help_mode = "Mode for deep restarts"
+[[option.mode.NONE]]
+ name = "none"
+ help = "do not use deep restart"
+[[option.mode.INPUT]]
+ name = "input"
+ help = "learn literals that appear in the input"
+[[option.mode.INPUT_AND_SOLVABLE]]
+ name = "input-and-solvable"
+ help = "learn literals that appear in the input and those that can be solved for variables that appear in the input"
+[[option.mode.INPUT_AND_PROP]]
+ name = "input-and-prop"
+ help = "learn literals that appear in the input and those that can be solved for variables, or correspond to constant propagations for terms that appear in the input"
+[[option.mode.ALL]]
+ name = "all"
+ help = "learn all literals"
+
+[[option]]
+ name = "deepRestartFactor"
+ category = "expert"
+ long = "deep-restart-factor=F"
+ type = "double"
+ default = "3.0"
+ minimum = "0.0"
+ maximum = "1000.0"
+ help = "sets the threshold for average assertions per literal before a deep restart"
d_zll(nullptr),
d_stopSearch(false, userContext())
{
- bool trackZeroLevel = isOutputOn(OutputTag::LEARNED_LITS)
- || options().smt.produceLearnedLiterals;
+ bool trackZeroLevel =
+ options().smt.deepRestartMode != options::DeepRestartMode::NONE
+ || isOutputOn(OutputTag::LEARNED_LITS)
+ || options().smt.produceLearnedLiterals;
if (trackZeroLevel)
{
d_zll = std::make_unique<ZeroLevelLearner>(env, theoryEngine);
break;
}
int32_t alevel = d_propEngine->getDecisionLevel(assertion);
- d_zll->notifyAsserted(assertion, alevel);
+ if (!d_zll->notifyAsserted(assertion, alevel))
+ {
+ d_stopSearch = true;
+ break;
+ }
}
// now, assert to theory engine
d_theoryEngine->assertFact(assertion);
d_assertNoLearnCount(0)
{
// get the learned types
- d_learnedTypes.insert(modes::LearnedLitType::INPUT);
+ options::DeepRestartMode lmode = options().smt.deepRestartMode;
+ if (lmode != options::DeepRestartMode::NONE)
+ {
+ d_learnedTypes.insert(modes::LearnedLitType::INPUT);
+ if (lmode == options::DeepRestartMode::ALL)
+ {
+ d_learnedTypes.insert(modes::LearnedLitType::INTERNAL);
+ d_learnedTypes.insert(modes::LearnedLitType::SOLVABLE);
+ d_learnedTypes.insert(modes::LearnedLitType::CONSTANT_PROP);
+ }
+ else if (lmode == options::DeepRestartMode::INPUT_AND_SOLVABLE)
+ {
+ d_learnedTypes.insert(modes::LearnedLitType::SOLVABLE);
+ }
+ else if (lmode == options::DeepRestartMode::INPUT_AND_PROP)
+ {
+ d_learnedTypes.insert(modes::LearnedLitType::SOLVABLE);
+ d_learnedTypes.insert(modes::LearnedLitType::CONSTANT_PROP);
+ }
+ }
}
ZeroLevelLearner::~ZeroLevelLearner() {}
<< d_env.getTopLevelSubstitutions().get().size()
<< std::endl;
Trace("level-zero") << d_ldb.toStringDebug();
+ // the threshold is by default d_ppnAtoms.size()*3.0, which means we restart
+ // if we have learned any literals, and the number of assertions since the
+ // last learned literal is equal to the total number of literals in the
+ // input problem times 3, i.e. each literal has been asserted on average 3
+ // times.
+ d_deepRestartThreshold = static_cast<size_t>(
+ static_cast<double>(d_ppnAtoms.size()) * options().smt.deepRestartFactor);
+ Trace("level-zero") << "Restart threshold is " << d_deepRestartThreshold
+ << std::endl;
}
bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel)
processLearnedLiteral(assertion, ltype);
return true;
}
+ // request a deep restart?
+ if (options().smt.deepRestartMode != options::DeepRestartMode::NONE)
+ {
+ if (hasLearnedLiteralForRestart() > 0)
+ {
+ // if non-empty and non-learned atoms have been asserted beyond the
+ // threshold
+ if (d_assertNoLearnCount > d_deepRestartThreshold)
+ {
+ Trace("level-zero") << "DEEP RESTART after " << d_assertNoLearnCount
+ << " asserts." << std::endl;
+ return false;
+ }
+ }
+ }
+ if (TraceIsOn("level-zero-debug"))
+ {
+ if (d_assertNoLearnCount > 0
+ && d_assertNoLearnCount % d_deepRestartThreshold == 0)
+ {
+ Trace("level-zero-debug")
+ << "#asserts without learning = " << d_assertNoLearnCount << " ("
+ << (d_assertNoLearnCount / d_deepRestartThreshold) << "x)"
+ << std::endl;
+ }
+ }
return true;
}
// if we solved for any variable from input, we are SOLVABLE.
for (const Node& v : ss.d_vars)
{
- if (d_ppnSyms.find(v) == d_ppnSyms.end())
+ if (d_ppnSyms.find(v) != d_ppnSyms.end())
{
Trace("level-zero-assert") << "...solvable due to " << v << std::endl;
ltype = modes::LearnedLitType::SOLVABLE;
NodeSet d_ppnSyms;
/** Current counter of assertions */
size_t d_assertNoLearnCount;
+ /** The threshold */
+ size_t d_deepRestartThreshold;
/** learnable learned literal types (for deep restart), based on option */
std::unordered_set<modes::LearnedLitType> d_learnedTypes;
}; /* class ZeroLevelLearner */
// used by the user to rephrase the input.
opts.quantifiers.sygusInference = false;
opts.quantifiers.sygusRewSynthInput = false;
+ // deep restart does not work with internal subsolvers?
+ opts.smt.deepRestartMode = options::DeepRestartMode::NONE;
}
}
<< std::endl;
opts.arith.nlCovVarElim = false;
}
+ if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
+ {
+ reason << "deep restarts";
+ return true;
+ }
return false;
}
reason << "solveIntAsBV";
return true;
}
+ if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
+ {
+ reason << "deep restarts";
+ return true;
+ }
if (opts.parallel.computePartitions > 1)
{
reason << "compute partitions";
notifyModifyOption("cegqiNestedQE", "false", "incremental solving");
opts.quantifiers.cegqiNestedQE = false;
opts.arith.arithMLTrick = false;
-
return false;
}
}
notifyModifyOption("simplificationMode", "none", "unsat cores");
opts.smt.simplificationMode = options::SimplificationMode::NONE;
+ if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
+ {
+ verbose(1) << "SolverEngine: turning off deep restart to support unsat "
+ "cores"
+ << std::endl;
+ opts.smt.deepRestartMode = options::DeepRestartMode::NONE;
+ }
}
if (opts.smt.learnedRewrite)
notifyModifyOption("unconstrainedSimp", "false", "unsat cores");
opts.smt.unconstrainedSimp = false;
}
+ if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
+ {
+ reason << "deep restarts";
+ return true;
+ }
return false;
}
{
return true;
}
+ if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
+ {
+ reason << "deep restarts";
+ return true;
+ }
return false;
}
{
opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE;
}
+ if (opts.quantifiers.globalNegate)
+ {
+ notifyModifyOption("deep-restart", "false", "global-negate");
+ opts.smt.deepRestartMode = options::DeepRestartMode::NONE;
+ }
}
void SetDefaults::setDefaultsSygus(Options& opts) const
// to the actual preprocessed learned literals, as the input may have
// undergone further preprocessing.
preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
+ // if we can deep restart, we always remember the preprocessed formulas,
+ // which are the basis for the next check-sat.
+ if (canDeepRestart())
+ {
+ // incompatible with global negation
+ Assert(!as.isGlobalNegated());
+ theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
+ // note that if a skolem is eliminated in preprocessing, we remove it
+ // from the preprocessed skolem map
+ std::vector<size_t> elimSkolems;
+ for (const std::pair<const size_t, Node>& k : d_ppSkolemMap)
+ {
+ if (sm.hasSubstitution(k.second))
+ {
+ Trace("deep-restart-ism")
+ << "SKOLEM:" << k.second << " was eliminated during preprocessing"
+ << std::endl;
+ elimSkolems.push_back(k.first);
+ continue;
+ }
+ Trace("deep-restart-ism") << "SKOLEM:" << k.second << " is skolem for "
+ << assertions[k.first] << std::endl;
+ }
+ for (size_t i : elimSkolems)
+ {
+ ism.erase(i);
+ }
+ // remember the assertions and Skolem mapping
+ d_ppAssertions = assertions;
+ d_ppSkolemMap = ism;
+ }
d_propEngine->assertInputFormulas(assertions, ism);
}
as.clearCurrent();
}
+void SmtSolver::deepRestart(Assertions& asr, const std::vector<Node>& zll)
+{
+ Assert(canDeepRestart());
+ Assert(!zll.empty());
+ Trace("deep-restart") << "Have " << zll.size()
+ << " zero level learned literals" << std::endl;
+
+ preprocessing::AssertionPipeline& apr = asr.getAssertionPipeline();
+ // Copy the preprocessed assertions and skolem map information directly
+ for (const Node& a : d_ppAssertions)
+ {
+ apr.push_back(a);
+ }
+ preprocessing::IteSkolemMap& ismr = apr.getIteSkolemMap();
+ for (const std::pair<const size_t, Node>& k : d_ppSkolemMap)
+ {
+ // carry the entire skolem map, which should align with the order of
+ // assertions passed into the new assertions pipeline
+ ismr[k.first] = k.second;
+ }
+
+ if (isOutputOn(OutputTag::DEEP_RESTART))
+ {
+ output(OutputTag::DEEP_RESTART) << "(deep-restart (";
+ bool firstTime = true;
+ for (TNode lit : zll)
+ {
+ output(OutputTag::DEEP_RESTART) << (firstTime ? "" : " ") << lit;
+ firstTime = false;
+ }
+ output(OutputTag::DEEP_RESTART) << "))" << std::endl;
+ }
+ for (TNode lit : zll)
+ {
+ Trace("deep-restart-lit") << "Restart learned lit: " << lit << std::endl;
+ apr.push_back(lit);
+ if (Configuration::isAssertionBuild())
+ {
+ Assert(d_allLearnedLits.find(lit) == d_allLearnedLits.end())
+ << "Relearned: " << lit << std::endl;
+ d_allLearnedLits.insert(lit);
+ }
+ }
+ Trace("deep-restart") << "Finished compute deep restart" << std::endl;
+
+ // we now finish init to reconstruct prop engine and theory engine
+ finishInit();
+}
+
+bool SmtSolver::canDeepRestart() const
+{
+ return options().smt.deepRestartMode != options::DeepRestartMode::NONE;
+}
+
TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
* into the SMT solver, and clears the buffer.
*/
void processAssertions(Assertions& as);
+ /**
+ * Perform a deep restart.
+ *
+ * This constructs a fresh copy of the theory engine and prop engine, and
+ * populates the given assertions for the next call to checkSatisfiability.
+ * In particular, we add the preprocessed assertions from the previous
+ * call to checkSatisfiability, as well as those in zll.
+ *
+ * @param as The assertions to populate
+ * @param zll The zero-level literals we learned on the previous call to
+ * checkSatisfiability.
+ */
+ void deepRestart(Assertions& as, const std::vector<Node>& zll);
//------------------------------------------ access methods
/** Get a pointer to the TheoryEngine owned by this solver. */
TheoryEngine* getTheoryEngine();
//------------------------------------------ end access methods
private:
+ /** Whether we track information necessary for deep restarts */
+ bool canDeepRestart() const;
/** The preprocessor of this SMT solver */
Preprocessor d_pp;
/** Reference to the statistics of SolverEngine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
/** The propositional engine */
std::unique_ptr<prop::PropEngine> d_propEngine;
+ //------------------------------------------ Bookkeeping for deep restarts
+ /** The exact list of preprocessed assertions we sent to the PropEngine */
+ std::vector<Node> d_ppAssertions;
+ /** The skolem map associated with d_ppAssertions */
+ std::unordered_map<size_t, Node> d_ppSkolemMap;
+ /** All learned literals, used for debugging */
+ std::unordered_set<Node> d_allLearnedLits;
};
} // namespace smt
Assert(d_state->isFullyReady());
// check the satisfiability with the solver object
- Result r = d_smtSolver->checkSatisfiability(*d_asserts.get(), assumptions);
+ Assertions& as = *d_asserts.get();
+ Result r = d_smtSolver->checkSatisfiability(as, assumptions);
+
+ // If the result is unknown, we may optionally do a "deep restart" where
+ // the members of the SMT solver are reconstructed and given the
+ // preprocessed input formulas (plus additional learned formulas). Notice
+ // that assumptions are pushed to the preprocessed input in the above call, so
+ // any additional satisfiability checks use an empty set of assumptions.
+ while (r.getStatus() == Result::UNKNOWN && deepRestart())
+ {
+ Trace("smt") << "SolverEngine::checkSat after deep restart" << std::endl;
+ r = d_smtSolver->checkSatisfiability(as, {});
+ }
Trace("smt") << "SolverEngine::checkSat(" << assumptions << ") => " << r
<< endl;
d_smtSolver->resetAssertions();
}
+bool SolverEngine::deepRestart()
+{
+ SolverEngineScope smts(this);
+ if (options().smt.deepRestartMode == options::DeepRestartMode::NONE)
+ {
+ // deep restarts not enabled
+ return false;
+ }
+ Trace("smt") << "SMT deepRestart()" << endl;
+
+ Assert(d_state->isFullyInited());
+
+ // get the zero-level learned literals now, before resetting the context
+ std::vector<Node> zll =
+ getPropEngine()->getLearnedZeroLevelLiteralsForRestart();
+
+ if (zll.empty())
+ {
+ // not worthwhile to restart if we didn't learn anything
+ Trace("deep-restart") << "No learned literals" << std::endl;
+ return false;
+ }
+
+ d_asserts->clearCurrent();
+ d_state->notifyResetAssertions();
+ // deep restart the SMT solver, which reconstructs the theory engine and
+ // prop engine.
+ d_smtSolver->deepRestart(*d_asserts.get(), zll);
+ // push the state to maintain global context around everything
+ d_state->setup();
+ return true;
+}
+
void SolverEngine::interrupt()
{
if (!d_state->isFullyInited())
*/
theory::QuantifiersEngine* getAvailableQuantifiersEngine(const char* c) const;
+ /**
+ * Deep restart, assumes that we just ran a satisfiability check.
+ * Returns true if we wish to reconstruct the SMT solver and try again. If
+ * so, the SMT solver is deep restarted, and we are prepared to make another
+ * satisfiability check.
+ */
+ bool deepRestart();
+
// --------------------------------------- callbacks from the state
/**
* Notify push pre, which is called just before the user context of the state
regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smtv1.smt2
regress0/decision/wchains010ue.delta02.smtv1.smt2
regress0/declare-fun-is-match.smt2
+ regress0/deep-restart/dd.266.smt2
+ regress0/deep-restart/dd.fuzz21.smtv1.smt2
+ regress0/deep-restart/dd.issue4735.smt2
+ regress0/deep-restart/dd.wrong-sat-020322.smt2
regress0/define-fun-model.smt2
regress0/difficulty-simple.smt2
regress0/difficulty-model-ex.smt2
regress0/print_model.cvc.smt2
regress0/printer/bv_consts_bin.smt2
regress0/printer/bv_consts_dec.smt2
+ regress0/printer/deep-restart-output.smt2
regress0/printer/empty_sort.smt2
regress0/printer/empty_symbol_name.smt2
regress0/printer/learned-lit-output.smt2
--- /dev/null
+; COMMAND-LINE: --deep-restart=input
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-const x Bool)
+(declare-fun s () String)
+(assert (not (<= 0 (ite x 0 (str.to_int (str.substr s 0 1))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --deep-restart=input
+; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
+; DISABLE-TESTER: lfsc
+(set-logic ALL)
+(declare-const v (_ BitVec 2))
+(declare-const x7 Bool)
+(declare-const x Bool)
+(declare-const x79 Bool)
+(declare-const x799 (_ BitVec 1))
+(check-sat-assuming ((and (distinct (_ bv0 1) (ite x (_ bv1 1) (_ bv0 1))) (or (bvsge (_ bv0 1) (ite x7 (_ bv1 1) (_ bv0 1))) x7) (not (= (_ bv0 4) ((_ zero_extend 3) (ite x79 (_ bv1 1) (_ bv0 1))))) (or x79 (distinct (_ bv0 4) (bvxor (_ bv2 4) ((_ zero_extend 3) (ite x79 (_ bv1 1) (_ bv0 1)))))) (bvuge (_ bv1 4) ((_ sign_extend 1) ((_ repeat 3) (ite (= (_ bv0 4) ((_ sign_extend 3) (ite (distinct (_ bv0 4) (bvor (_ bv1 4) ((_ zero_extend 2) v))) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))) (bvsgt (_ bv0 4) ((_ repeat 4) (ite (bvslt (ite (distinct (_ bv0 4) ((_ sign_extend 3) (ite (bvslt (_ bv0 1) x799) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) (_ bv0 1)) (_ bv1 1) (_ bv0 1)))))))
--- /dev/null
+; COMMAND-LINE: --deep-restart=input
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x Bool)
+(declare-fun b () Int)
+(declare-fun f () String)
+(declare-fun k () String)
+(assert (ite (distinct b 0) (= (str.++ k f) (str.++ k k)) x))
+(assert (distinct true (= b 0)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --deep-restart=input-and-prop --strings-exp
+; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
+; DISABLE-TESTER: lfsc
+(set-logic ALL)
+(declare-sort E 0)
+(declare-fun s () (Seq E))
+(assert (distinct s (str.update s 0 (seq.unit (seq.nth s 0)))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --deep-restart=input -o deep-restart
+; EXPECT: (deep-restart ((= f k)))
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x Bool)
+(declare-fun b () Int)
+(declare-fun f () String)
+(declare-fun k () String)
+(assert (ite (distinct b 0) (= (str.++ k f) (str.++ k k)) x))
+(assert (distinct true (= b 0)))
+(check-sat)
projects / cvc5.git / commitdiff