From b8d319d520d877e9062ea771f8efe8eed1c81876 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Apr 2022 15:03:33 -0500 Subject: [PATCH] Add `deep-restart` option (#8644) 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. --- src/options/base_options.toml | 6 +- src/options/smt_options.toml | 34 ++++++++ src/prop/theory_proxy.cpp | 12 ++- src/prop/zero_level_learner.cpp | 58 ++++++++++++- src/prop/zero_level_learner.h | 2 + src/smt/set_defaults.cpp | 35 +++++++- src/smt/smt_solver.cpp | 85 +++++++++++++++++++ src/smt/smt_solver.h | 22 +++++ src/smt/solver_engine.cpp | 47 +++++++++- src/smt/solver_engine.h | 8 ++ test/regress/cli/CMakeLists.txt | 5 ++ .../cli/regress0/deep-restart/dd.266.smt2 | 7 ++ .../deep-restart/dd.fuzz21.smtv1.smt2 | 12 +++ .../regress0/deep-restart/dd.issue4735.smt2 | 10 +++ .../deep-restart/dd.wrong-sat-020322.smt2 | 10 +++ .../regress0/printer/deep-restart-output.smt2 | 11 +++ 16 files changed, 356 insertions(+), 8 deletions(-) create mode 100644 test/regress/cli/regress0/deep-restart/dd.266.smt2 create mode 100644 test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 create mode 100644 test/regress/cli/regress0/deep-restart/dd.issue4735.smt2 create mode 100644 test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 create mode 100644 test/regress/cli/regress0/printer/deep-restart-output.smt2 diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 13aa1020b..96b2a9655 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -215,7 +215,11 @@ name = "Base" 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]] diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 645d06296..7aaf05f93 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -461,3 +461,37 @@ name = "SMT Layer" 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" diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d6c6f6a56..ba47061b0 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -53,8 +53,10 @@ TheoryProxy::TheoryProxy(Env& env, 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(env, theoryEngine); @@ -143,7 +145,11 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { 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); diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index 32eb90059..9f2d79b63 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -39,7 +39,26 @@ ZeroLevelLearner::ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine) 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() {} @@ -143,6 +162,15 @@ void ZeroLevelLearner::notifyInputFormulas(const std::vector& assertions) << 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( + static_cast(d_ppnAtoms.size()) * options().smt.deepRestartFactor); + Trace("level-zero") << "Restart threshold is " << d_deepRestartThreshold + << std::endl; } bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel) @@ -168,6 +196,32 @@ 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; } @@ -188,7 +242,7 @@ modes::LearnedLitType ZeroLevelLearner::computeLearnedLiteralType( // 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; diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h index 16b5e7e3c..b5dbd7a88 100644 --- a/src/prop/zero_level_learner.h +++ b/src/prop/zero_level_learner.h @@ -105,6 +105,8 @@ class ZeroLevelLearner : protected EnvObj 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 d_learnedTypes; }; /* class ZeroLevelLearner */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index fca7abee9..50404dccb 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -186,6 +186,8 @@ void SetDefaults::setDefaultsPre(Options& opts) // 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; } } @@ -956,6 +958,11 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, << std::endl; opts.arith.nlCovVarElim = false; } + if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) + { + reason << "deep restarts"; + return true; + } return false; } @@ -1047,6 +1054,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "solveIntAsBV"; return true; } + if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) + { + reason << "deep restarts"; + return true; + } if (opts.parallel.computePartitions > 1) { reason << "compute partitions"; @@ -1062,7 +1074,6 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, notifyModifyOption("cegqiNestedQE", "false", "incremental solving"); opts.quantifiers.cegqiNestedQE = false; opts.arith.arithMLTrick = false; - return false; } @@ -1078,6 +1089,13 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, } 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) @@ -1194,6 +1212,11 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, notifyModifyOption("unconstrainedSimp", "false", "unsat cores"); opts.smt.unconstrainedSimp = false; } + if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) + { + reason << "deep restarts"; + return true; + } return false; } @@ -1213,6 +1236,11 @@ bool SetDefaults::incompatibleWithSygus(Options& opts, { return true; } + if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) + { + reason << "deep restarts"; + return true; + } return false; } @@ -1566,6 +1594,11 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { 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 diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index bd23ff353..b75049235 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -238,6 +238,37 @@ void SmtSolver::processAssertions(Assertions& as) // 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 elimSkolems; + for (const std::pair& 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); } @@ -245,6 +276,60 @@ void SmtSolver::processAssertions(Assertions& as) as.clearCurrent(); } +void SmtSolver::deepRestart(Assertions& asr, const std::vector& 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& 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(); } diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 78d11ef2a..634cf276b 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -102,6 +102,19 @@ class SmtSolver : protected EnvObj * 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& zll); //------------------------------------------ access methods /** Get a pointer to the TheoryEngine owned by this solver. */ TheoryEngine* getTheoryEngine(); @@ -114,6 +127,8 @@ class SmtSolver : protected EnvObj //------------------------------------------ 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 */ @@ -122,6 +137,13 @@ class SmtSolver : protected EnvObj std::unique_ptr d_theoryEngine; /** The propositional engine */ std::unique_ptr d_propEngine; + //------------------------------------------ Bookkeeping for deep restarts + /** The exact list of preprocessed assertions we sent to the PropEngine */ + std::vector d_ppAssertions; + /** The skolem map associated with d_ppAssertions */ + std::unordered_map d_ppSkolemMap; + /** All learned literals, used for debugging */ + std::unordered_set d_allLearnedLits; }; } // namespace smt diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index b763adc54..44014d174 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -762,7 +762,19 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions) 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; @@ -1804,6 +1816,39 @@ void SolverEngine::resetAssertions() 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 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()) diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 4d4fceaef..f5eff833a 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -952,6 +952,14 @@ class CVC5_EXPORT SolverEngine */ 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 diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 8dcc979d4..212bcabca 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -592,6 +592,10 @@ set(regress_0_tests 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 @@ -945,6 +949,7 @@ set(regress_0_tests 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 diff --git a/test/regress/cli/regress0/deep-restart/dd.266.smt2 b/test/regress/cli/regress0/deep-restart/dd.266.smt2 new file mode 100644 index 000000000..9e6317d39 --- /dev/null +++ b/test/regress/cli/regress0/deep-restart/dd.266.smt2 @@ -0,0 +1,7 @@ +; 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) diff --git a/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 b/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 new file mode 100644 index 000000000..d5f2e21d8 --- /dev/null +++ b/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 @@ -0,0 +1,12 @@ +; 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))))))) diff --git a/test/regress/cli/regress0/deep-restart/dd.issue4735.smt2 b/test/regress/cli/regress0/deep-restart/dd.issue4735.smt2 new file mode 100644 index 000000000..5aa01ce7d --- /dev/null +++ b/test/regress/cli/regress0/deep-restart/dd.issue4735.smt2 @@ -0,0 +1,10 @@ +; 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) diff --git a/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 b/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 new file mode 100644 index 000000000..d39dc8dca --- /dev/null +++ b/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 @@ -0,0 +1,10 @@ +; 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) diff --git a/test/regress/cli/regress0/printer/deep-restart-output.smt2 b/test/regress/cli/regress0/printer/deep-restart-output.smt2 new file mode 100644 index 000000000..8bfc663f4 --- /dev/null +++ b/test/regress/cli/regress0/printer/deep-restart-output.smt2 @@ -0,0 +1,11 @@ +; 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) -- 2.30.2