diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/abduction_solver.cpp | 10 | ||||
-rw-r--r-- | src/smt/abstract_values.h | 6 | ||||
-rw-r--r-- | src/smt/check_models.cpp | 2 | ||||
-rw-r--r-- | src/smt/difficulty_post_processor.cpp | 2 | ||||
-rw-r--r-- | src/smt/interpolation_solver.cpp | 1 | ||||
-rw-r--r-- | src/smt/model.cpp | 3 | ||||
-rw-r--r-- | src/smt/preprocessor.cpp | 4 | ||||
-rw-r--r-- | src/smt/proof_final_callback.cpp | 30 | ||||
-rw-r--r-- | src/smt/proof_final_callback.h | 5 | ||||
-rw-r--r-- | src/smt/proof_manager.cpp | 23 | ||||
-rw-r--r-- | src/smt/proof_post_processor.cpp | 9 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 9 | ||||
-rw-r--r-- | src/smt/smt_solver.cpp | 8 | ||||
-rw-r--r-- | src/smt/solver_engine.cpp | 23 | ||||
-rw-r--r-- | src/smt/solver_engine.h | 16 | ||||
-rw-r--r-- | src/smt/sygus_solver.cpp | 315 | ||||
-rw-r--r-- | src/smt/sygus_solver.h | 98 |
17 files changed, 364 insertions, 200 deletions
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index ce11c5718..f17e768c9 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -50,6 +50,7 @@ bool AbductionSolver::getAbduct(const std::vector<Node>& axioms, std::vector<Node> asserts(axioms.begin(), axioms.end()); // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(goal); + conjn = rewrite(conjn); // now negate conjn = conjn.negate(); d_abdConj = conjn; @@ -93,11 +94,12 @@ bool AbductionSolver::getAbductInternal(const std::vector<Node>& axioms, Result r = d_subsolver->checkSat(); Trace("sygus-abduct") << " SolverEngine::getAbduct result: " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + // get the synthesis solution + std::map<Node, Node> sols; + // use the "getSubsolverSynthSolutions" interface, since we asserted the + // internal form of the SyGuS conjecture and used check-sat. + if (d_subsolver->getSubsolverSynthSolutions(sols)) { - // get the synthesis solution - std::map<Node, Node> sols; - d_subsolver->getSynthSolutions(sols); Assert(sols.size() == 1); std::map<Node, Node>::iterator its = sols.find(d_sssf); if (its != sols.end()) diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h index 32cff9378..354b8691f 100644 --- a/src/smt/abstract_values.h +++ b/src/smt/abstract_values.h @@ -48,7 +48,7 @@ class AbstractValues /** * Make a new (or return an existing) abstract value for a node. - * Can only use this if options::abstractValues() is on. + * Can only use this if abstractValues option is on. */ Node mkAbstractValue(TNode n); @@ -63,7 +63,7 @@ class AbstractValues /** * A map of AbsractValues to their actual constants. Only used if - * options::abstractValues() is on. + * abstractValues option is on. */ theory::SubstitutionMap d_abstractValueMap; @@ -71,7 +71,7 @@ class AbstractValues * A mapping of all abstract values (actual value |-> abstract) that * we've handed out. This is necessary to ensure that we give the * same AbstractValues for the same real constants. Only used if - * options::abstractValues() is on. + * abstractValues option is on. */ NodeToNodeHashMap d_abstractValues; }; diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 7d546eae7..f3393caae 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -71,7 +71,7 @@ void CheckModels::checkModel(TheoryModel* m, // evaluate e.g. divide-by-zero. This is intentional since the evaluation // is not trustworthy, since the UF introduced by expanding definitions may // not be properly constrained. - Node n = sm.apply(assertion, false); + Node n = sm.apply(assertion); verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n << std::endl; diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp index 31797ba5e..6d1882a4e 100644 --- a/src/smt/difficulty_post_processor.cpp +++ b/src/smt/difficulty_post_processor.cpp @@ -69,7 +69,7 @@ void DifficultyPostprocessCallback::getDifficultyMap( NodeManager* nm = NodeManager::currentNM(); for (const std::pair<const Node, uint64_t>& d : d_accMap) { - dmap[d.first] = nm->mkConst(CONST_RATIONAL, Rational(d.second)); + dmap[d.first] = nm->mkConstInt(Rational(d.second)); } } diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 36f8e2a8d..20be53e85 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -51,6 +51,7 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms, << std::endl; // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(conj); + conjn = rewrite(conjn); std::string name("__internal_interpol"); quantifiers::SygusInterpol interpolSolver(d_env); diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 5c427fa46..69dddded8 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -30,7 +30,8 @@ Model::Model(bool isKnownSat, const std::string& inputName) std::ostream& operator<<(std::ostream& out, const Model& m) { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); - Printer::getPrinter(options::outputLanguage())->toStream(out, m); + auto language = options::ioutils::getOutputLang(out); + Printer::getPrinter(language)->toStream(out, m); return out; } diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 41653b6ee..0fdb569c8 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -125,8 +125,8 @@ Node Preprocessor::expandDefinitions(const Node& node, // Ensure node is type-checked at this point. n.getType(true); } - // we apply substitutions here, before expanding definitions - n = d_env.getTopLevelSubstitutions().apply(n, false); + // apply substitutions here (without rewriting), before expanding definitions + n = d_env.getTopLevelSubstitutions().apply(n); // now call expand definitions n = d_exDefs.expandDefinitions(n, cache); return n; diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index 93b4cae19..484f0dd73 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -34,6 +34,9 @@ ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm) d_instRuleIds( smtStatisticsRegistry().registerHistogram<theory::InferenceId>( "finalProof::instRuleId")), + d_annotationRuleIds( + smtStatisticsRegistry().registerHistogram<theory::InferenceId>( + "finalProof::annotationRuleId")), d_totalRuleCount( smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")), d_minPedanticLevel( @@ -96,6 +99,33 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, } } } + else if (r == PfRule::ANNOTATION) + { + // we currently assume the annotation is a single inference id + const std::vector<Node>& args = pn->getArguments(); + if (args.size() > 0) + { + InferenceId id; + if (getInferenceId(args[0], id)) + { + d_annotationRuleIds << id; + } + } + } + // print for debugging + if (Trace.isOn("final-pf-hole")) + { + // currently only track theory rewrites + if (r == PfRule::THEORY_REWRITE) + { + const std::vector<Node>& args = pn->getArguments(); + Node eq = args[0]; + TheoryId tid = THEORY_BUILTIN; + builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid); + Trace("final-pf-hole") << "hole " << r << " " << tid << " : " << eq[0] + << " ---> " << eq[1] << std::endl; + } + } return false; } diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h index 88b8e20ef..a1e6b1f69 100644 --- a/src/smt/proof_final_callback.h +++ b/src/smt/proof_final_callback.h @@ -54,6 +54,11 @@ class ProofFinalCallback : public ProofNodeUpdaterCallback * marked with the given inference id. */ HistogramStat<theory::InferenceId> d_instRuleIds; + /** + * Counts number of postprocessed proof nodes of rule ANNOTATION that were + * marked with the given inference id. + */ + HistogramStat<theory::InferenceId> d_annotationRuleIds; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; /** The minimum pedantic level of any rule encountered */ diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 4cb9d5bf9..04f601680 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -41,7 +41,8 @@ PfManager::PfManager(Env& env) d_pchecker(new ProofChecker( options().proof.proofCheck == options::ProofCheckMode::EAGER, options().proof.proofPedantic)), - d_pnm(new ProofNodeManager(env.getRewriter(), d_pchecker.get())), + d_pnm(new ProofNodeManager( + env.getOptions(), env.getRewriter(), d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), d_pfpp(nullptr), @@ -150,8 +151,10 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as) Trace("smt-proof") << "SolverEngine::setFinalProof(): make scope...\n"; // Now make the final scope, which ensures that the only open leaves of the - // proof are the assertions. - d_finalProof = d_pnm->mkScope(pfn, assertions); + // proof are the assertions. If we are pruning the input, we will try to + // minimize the used assertions. + d_finalProof = + d_pnm->mkScope(pfn, assertions, true, options().proof.proofPruneInput); Trace("smt-proof") << "SolverEngine::setFinalProof(): finished.\n"; } @@ -227,20 +230,14 @@ void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap, std::map<Node, Node> dmapp = dmap; dmap.clear(); std::vector<Node> ppAsserts; - std::vector<Node> asserts; - getAssertions(as, asserts); for (const std::pair<const Node, Node>& ppa : dmapp) { Trace("difficulty") << " preprocess difficulty: " << ppa.second << " for " << ppa.first << std::endl; - // Ensure that only input assertions are marked as having a difficulty. - // In some cases, a lemma may be marked as having a difficulty - // internally, e.g. for lemmas that require justification, which we should - // skip or otherwise we end up with an open proof below. - if (std::find(asserts.begin(), asserts.end(), ppa.first) != asserts.end()) - { - ppAsserts.push_back(ppa.first); - } + // The difficulty manager should only report difficulty for preprocessed + // assertions, or we will get an open proof below. This is ensured + // internally by the difficuly manager. + ppAsserts.push_back(ppa.first); } // assume a SAT refutation from all input assertions that were marked // as having a difficulty diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a292fec8f..167a82e26 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -422,6 +422,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // not eliminated return Node::null(); } + Trace("smt-proof-pp-debug") << "Expand macro " << id << std::endl; // macro elimination if (id == PfRule::MACRO_SR_EQ_INTRO) { @@ -855,7 +856,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi; j++) { - Node nodej = nm->mkConst(CONST_RATIONAL, Rational(j)); + Node nodej = nm->mkConstInt(Rational(j)); cdp->addStep( children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej}); } @@ -1086,8 +1087,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, TNode child = children[i]; TNode scalar = args[i]; bool isPos = scalar.getConst<Rational>() > 0; - Node scalarCmp = nm->mkNode( - isPos ? GT : LT, scalar, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node scalarCmp = + nm->mkNode(isPos ? GT : LT, + scalar, + nm->mkConstRealOrInt(scalar.getType(), Rational(0))); // (= scalarCmp true) Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp}); Assert(!scalarCmpOrTrue.isNull()); diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index b2fe2b5d6..194290399 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -373,7 +373,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.produceInterpols != options::ProduceInterpols::NONE || opts.smt.modelCoresMode != options::ModelCoresMode::NONE || opts.smt.blockModelsMode != options::BlockModelsMode::NONE - || opts.smt.produceProofs) + || opts.smt.produceProofs || isSygus(opts)) && !opts.smt.produceAssertions) { verbose(1) << "SolverEngine: turning on produce-assertions to support " @@ -807,6 +807,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; + opts.arith.nlCadVarElim = true; if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; @@ -823,6 +824,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; + opts.arith.nlCadVarElim = true; if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; @@ -1161,9 +1163,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, bool SetDefaults::safeUnsatCores(const Options& opts) const { // whether we want to force safe unsat cores, i.e., if we are in the default - // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental - return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS - || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY; + // ASSUMPTIONS mode, since other ones are experimental + return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS; } bool SetDefaults::incompatibleWithQuantifiers(Options& opts, diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 4530df774..25c6f5f9f 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -71,7 +71,7 @@ void SmtSolver::finishInit() * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env)); + d_propEngine.reset(new prop::PropEngine(d_env, d_theoryEngine.get())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -89,7 +89,7 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env)); + d_propEngine.reset(new prop::PropEngine(d_env, d_theoryEngine.get())); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not @@ -158,13 +158,15 @@ Result SmtSolver::checkSatisfiability(Assertions& as, d_env.verbose(2) << "solving..." << std::endl; Trace("smt") << "SmtSolver::check(): running check" << endl; Result result = d_propEngine->checkSat(); + Trace("smt") << "SmtSolver::check(): result " << result << std::endl; rm->endCall(); Trace("limit") << "SmtSolver::check(): cumulative millis " << rm->getTimeUsage() << ", resources " << rm->getResourceUsage() << endl; - if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) + if ((d_env.getOptions().smt.solveRealAsInt + || d_env.getOptions().smt.solveIntAsBV > 0) && result.asSatisfiabilityResult().isSat() == Result::UNSAT) { result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 2cf4862a9..32838eccf 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1193,6 +1193,8 @@ std::vector<Node> SolverEngine::getAssertionsInternal() return res; } +const Options& SolverEngine::options() const { return d_env->getOptions(); } + std::vector<Node> SolverEngine::getExpandedAssertions() { std::vector<Node> easserts = getAssertions(); @@ -1270,7 +1272,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal() Assert(pe != nullptr); std::shared_ptr<ProofNode> pepf; - if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) + if (options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS) { pepf = pe->getRefutation(); } @@ -1282,7 +1284,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal() std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts); std::vector<Node> core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); - if (options::minimalUnsatCores()) + if (options().smt.minimalUnsatCores) { core = reduceUnsatCore(core); } @@ -1291,7 +1293,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal() std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core) { - Assert(options::unsatCores()) + Assert(options().smt.unsatCores) << "cannot reduce unsat core if unsat cores are turned off"; d_env->verbose(1) << "SolverEngine::reduceUnsatCore(): reducing unsat core" @@ -1386,7 +1388,7 @@ void SolverEngine::checkUnsatCore() theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { - Node assertionAfterExpansion = tls.apply(*i, false); + Node assertionAfterExpansion = tls.apply(*i); d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core member " << *i << ", expanded to " << assertionAfterExpansion << std::endl; @@ -1432,7 +1434,7 @@ void SolverEngine::checkModel(bool hardFailure) Assert(m != nullptr); // check the model with the theory engine for debugging - if (options::debugCheckModels()) + if (options().smt.debugCheckModels) { TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); @@ -1527,8 +1529,8 @@ void SolverEngine::printInstantiations(std::ostream& out) && getSmtMode() == SmtMode::UNSAT) { // minimize instantiations based on proof manager - getRelevantInstantiationTermVectors(rinsts, - options::dumpInstantiationsDebug()); + getRelevantInstantiationTermVectors( + rinsts, options().driver.dumpInstantiationsDebug); } else { @@ -1601,6 +1603,13 @@ bool SolverEngine::getSynthSolutions(std::map<Node, Node>& solMap) return d_sygusSolver->getSynthSolutions(solMap); } +bool SolverEngine::getSubsolverSynthSolutions(std::map<Node, Node>& solMap) +{ + SolverEngineScope smts(this); + finishInit(); + return d_sygusSolver->getSubsolverSynthSolutions(solMap); +} + Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { SolverEngineScope smts(this); diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index d7df78f08..95b31eab2 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -563,6 +563,16 @@ class CVC5_EXPORT SolverEngine * is a valid formula. */ bool getSynthSolutions(std::map<Node, Node>& solMap); + /** + * Same as above, but used for getting synthesis solutions from a "subsolver" + * that has been initialized to assert the synthesis conjecture as a + * normal assertion. + * + * This method returns true if we are in a state immediately preceded by + * a successful call to checkSat, where this SolverEngine has an asserted + * synthesis conjecture. + */ + bool getSubsolverSynthSolutions(std::map<Node, Node>& solMap); /** * Do quantifier elimination. @@ -1025,6 +1035,12 @@ class CVC5_EXPORT SolverEngine * changes. */ std::vector<Node> getAssertionsInternal(); + + /** + * Return a reference to options like for `EnvObj`. + */ + const Options& options() const; + /* Members -------------------------------------------------------------- */ /** Solver instance that owns this SolverEngine instance. */ diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 4c8d3e5bd..70ad65644 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -42,7 +42,14 @@ namespace cvc5 { namespace smt { SygusSolver::SygusSolver(Env& env, SmtSolver& sms) - : EnvObj(env), d_smtSolver(sms), d_sygusConjectureStale(userContext(), true) + : EnvObj(env), + d_smtSolver(sms), + d_sygusVars(userContext()), + d_sygusConstraints(userContext()), + d_sygusAssumps(userContext()), + d_sygusFunSymbols(userContext()), + d_sygusConjectureStale(userContext(), true), + d_subsolverCd(userContext(), nullptr) { } @@ -84,7 +91,7 @@ void SygusSolver::declareSynthFun(Node fn, } // sygus conjecture is now stale - setSygusConjectureStale(); + d_sygusConjectureStale = true; } void SygusSolver::assertSygusConstraint(Node n, bool isAssume) @@ -101,7 +108,7 @@ void SygusSolver::assertSygusConstraint(Node n, bool isAssume) } // sygus conjecture is now stale - setSygusConjectureStale(); + d_sygusConjectureStale = true; } void SygusSolver::assertSygusInvConstraint(Node inv, @@ -173,44 +180,50 @@ void SygusSolver::assertSygusInvConstraint(Node inv, d_sygusConstraints.push_back(constraint); // sygus conjecture is now stale - setSygusConjectureStale(); + d_sygusConjectureStale = true; } Result SygusSolver::checkSynth(Assertions& as) { - if (options().base.incrementalSolving) + Trace("smt") << "SygusSolver::checkSynth" << std::endl; + // if applicable, check if the subsolver is the correct one + if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get()) { - // TODO (project #7) - throw ModalException( - "Cannot make check-synth commands when incremental solving is enabled"); + // this can occur if we backtrack to a place where we were using a different + // subsolver than the current one. In this case, we should reconstruct + // the subsolver. + d_sygusConjectureStale = true; } - Trace("smt") << "SygusSolver::checkSynth" << std::endl; - std::vector<Node> query; + // TODO (project #7): we currently must always rebuild the synthesis + // conjecture + subsolver, since it answers unsat. When the subsolver is + // updated to treat "sat" as solution for synthesis conjecture, this line + // will be deleted. + d_sygusConjectureStale = true; if (d_sygusConjectureStale) { NodeManager* nm = NodeManager::currentNM(); // build synthesis conjecture from asserted constraints and declared // variables/functions Trace("smt") << "Sygus : Constructing sygus constraint...\n"; - Node body = nm->mkAnd(d_sygusConstraints); + Node body = nm->mkAnd(listToVector(d_sygusConstraints)); // note that if there are no constraints, then assumptions are irrelevant if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty()) { - Node bodyAssump = nm->mkAnd(d_sygusAssumps); + Node bodyAssump = nm->mkAnd(listToVector(d_sygusAssumps)); body = nm->mkNode(IMPLIES, bodyAssump, body); } body = body.notNode(); Trace("smt") << "...constructed sygus constraint " << body << std::endl; if (!d_sygusVars.empty()) { - Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusVars); + Node boundVars = nm->mkNode(BOUND_VAR_LIST, listToVector(d_sygusVars)); body = nm->mkNode(EXISTS, boundVars, body); Trace("smt") << "...constructed exists " << body << std::endl; } if (!d_sygusFunSymbols.empty()) { - body = - quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body); + body = quantifiers::SygusUtils::mkSygusConjecture( + listToVector(d_sygusFunSymbols), body); } Trace("smt") << "...constructed forall " << body << std::endl; @@ -218,59 +231,119 @@ Result SygusSolver::checkSynth(Assertions& as) d_sygusConjectureStale = false; - // TODO (project #7): if incremental, we should push a context and assert - query.push_back(body); - } + d_conj = body; + + // if we are using a subsolver, initialize it now + if (usingSygusSubsolver()) + { + // we generate a new solver engine to do the SyGuS query + initializeSygusSubsolver(d_subsolver, as); - Result r = d_smtSolver.checkSatisfiability(as, query, false); + // store the pointer (context-dependent) + d_subsolverCd = d_subsolver.get(); - // Check that synthesis solutions satisfy the conjecture - if (options().smt.checkSynthSol - && r.asSatisfiabilityResult().isSat() == Result::UNSAT) + // also assert the internal SyGuS conjecture + d_subsolver->assertFormula(d_conj); + } + } + else + { + Assert(d_subsolver != nullptr); + } + Result r; + if (usingSygusSubsolver()) + { + r = d_subsolver->checkSat(); + } + else + { + std::vector<Node> query; + query.push_back(d_conj); + r = d_smtSolver.checkSatisfiability(as, query, false); + } + // The result returned by the above call is typically "unknown", which may + // or may not correspond to a state in which we solved the conjecture + // successfully. Instead we call getSynthSolutions below. If this returns + // true, then we were successful. In this case, we set the result to "unsat", + // since the synthesis conjecture was negated when asserted to the subsolver. + // + // This behavior is done for 2 reasons: + // (1) if we do not negate the synthesis conjecture, the subsolver in some + // cases cannot answer "sat", e.g. in the presence of recursive function + // definitions. Instead the SyGuS language standard itself indicates that + // a correct solution for a conjecture is one where the synthesis conjecture + // is *T-valid* (in the presence of defined recursive functions). In other + // words, a SyGuS query asks to prove that the conjecture is valid when + // witnessed by the given solution. + // (2) we do not want the solver to explicitly answer "unsat" by giving an + // unsatisfiable set of formulas to the underlying PropEngine, or otherwise + // we will not be able to ask for further solutions. This is critical for + // incremental solving where multiple solutions are returned for the same + // set of constraints. Thus, the internal SyGuS solver will mark unknown + // with IncompleteId::QUANTIFIERS_SYGUS_SOLVED. Furthermore, this id may be + // overwritten by other means of incompleteness, so we cannot rely on this + // identifier being the final reason for unknown. + // + // Thus, we use getSynthSolutions as means of knowing the conjecture was + // solved. + std::map<Node, Node> sol_map; + if (getSynthSolutions(sol_map)) { - checkSynthSolution(as); + // if we have solutions, we return "unsat" by convention + r = Result(Result::UNSAT); + // Check that synthesis solutions satisfy the conjecture + if (options().smt.checkSynthSol) + { + checkSynthSolution(as, sol_map); + } + } + else + { + // otherwise, we return "unknown" + r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } return r; } -bool SygusSolver::getSynthSolutions(std::map<Node, Node>& sol_map) +bool SygusSolver::getSynthSolutions(std::map<Node, Node>& solMap) { Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl; - std::map<Node, std::map<Node, Node>> sol_mapn; + if (usingSygusSubsolver()) + { + // use the call to get the synth solutions from the subsolver + return d_subsolver->getSubsolverSynthSolutions(solMap); + } + return getSubsolverSynthSolutions(solMap); +} + +bool SygusSolver::getSubsolverSynthSolutions(std::map<Node, Node>& solMap) +{ + Trace("smt") << "SygusSolver::getSubsolverSynthSolutions" << std::endl; + std::map<Node, std::map<Node, Node>> solMapn; // fail if the theory engine does not have synthesis solutions QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); - if (qe == nullptr || !qe->getSynthSolutions(sol_mapn)) + if (qe == nullptr || !qe->getSynthSolutions(solMapn)) { return false; } - for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn) + for (std::pair<const Node, std::map<Node, Node>>& cs : solMapn) { for (std::pair<const Node, Node>& s : cs.second) { - sol_map[s.first] = s.second; + solMap[s.first] = s.second; } } return true; } -void SygusSolver::checkSynthSolution(Assertions& as) +void SygusSolver::checkSynthSolution(Assertions& as, + const std::map<Node, Node>& sol_map) { - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); if (isVerboseOn(1)) { verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution" << std::endl; } - std::map<Node, std::map<Node, Node>> sol_map; - // Get solutions and build auxiliary vectors for substituting - QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); - if (qe == nullptr || !qe->getSynthSolutions(sol_map)) - { - InternalError() - << "SygusSolver::checkSynthSolution(): No solution to check!"; - return; - } if (sol_map.empty()) { InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!"; @@ -279,100 +352,39 @@ void SygusSolver::checkSynthSolution(Assertions& as) Trace("check-synth-sol") << "Got solution map:\n"; // the set of synthesis conjectures in our assertions std::unordered_set<Node> conjs; + conjs.insert(d_conj); // For each of the above conjectures, the functions-to-synthesis and their // solutions. This is used as a substitution below. - std::map<Node, std::vector<Node>> fvarMap; - std::map<Node, std::vector<Node>> fsolMap; - for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map) + std::vector<Node> fvars; + std::vector<Node> fsols; + for (const std::pair<const Node, Node>& pair : sol_map) { - Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n"; - conjs.insert(cmap.first); - std::vector<Node>& fvars = fvarMap[cmap.first]; - std::vector<Node>& fsols = fsolMap[cmap.first]; - for (const std::pair<const Node, Node>& pair : cmap.second) - { - Trace("check-synth-sol") - << " " << pair.first << " --> " << pair.second << "\n"; - fvars.push_back(pair.first); - fsols.push_back(pair.second); - } + Trace("check-synth-sol") + << " " << pair.first << " --> " << pair.second << "\n"; + fvars.push_back(pair.first); + fsols.push_back(pair.second); } + Trace("check-synth-sol") << "Starting new SMT Engine\n"; Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions - const context::CDList<Node>& alist = as.getAssertionList(); - Assert(options().smt.produceAssertions) - << "Expected produce assertions to be true when checking synthesis " - "solution"; - // auxiliary assertions - std::vector<Node> auxAssertions; - // expand definitions cache - std::unordered_map<Node, Node> cache; - for (const Node& assertion : alist) - { - if (isVerboseOn(1)) - { - verbose(1) << "SyGuS::checkSynthSolution: checking assertion " - << assertion << std::endl; - } - Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n"; - // Apply any define-funs from the problem. - Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache); - if (isVerboseOn(1)) - { - verbose(1) << "SyGuS::checkSynthSolution: -- expands to " << n - << std::endl; - } - Trace("check-synth-sol") << "Expanded assertion " << n << "\n"; - if (conjs.find(n) == conjs.end()) - { - Trace("check-synth-sol") << "It is an auxiliary assertion\n"; - auxAssertions.push_back(n); - } - else - { - Trace("check-synth-sol") << "It is a synthesis conjecture\n"; - } - } // check all conjectures - for (Node conj : conjs) + for (const Node& conj : conjs) { // Start new SMT engine to check solutions std::unique_ptr<SolverEngine> solChecker; - initializeSubsolver(solChecker, d_env); + initializeSygusSubsolver(solChecker, as); solChecker->getOptions().smt.checkSynthSol = false; solChecker->getOptions().quantifiers.sygusRecFun = false; - // get the solution for this conjecture - std::vector<Node>& fvars = fvarMap[conj]; - std::vector<Node>& fsols = fsolMap[conj]; + Assert(conj.getKind() == FORALL); + Node conjBody = conj[1]; + // we must expand definitions here, since define-fun may contain the + // function-to-synthesize, which needs to be substituted. + conjBody = d_smtSolver.getPreprocessor()->expandDefinitions(conjBody); // Apply solution map to conjecture body - Node conjBody; - /* Whether property is quantifier free */ - if (conj[1].getKind() != EXISTS) - { - conjBody = conj[1].substitute( - fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); - } - else - { - conjBody = conj[1][1].substitute( - fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); - - /* Skolemize property */ - std::vector<Node> vars, skos; - for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j) - { - vars.push_back(conj[1][0][j]); - std::stringstream ss; - ss << "sk_" << j; - skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType())); - Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to " - << skos.back() << "\n"; - } - conjBody = conjBody.substitute( - vars.begin(), vars.end(), skos.begin(), skos.end()); - } + conjBody = conjBody.substitute( + fvars.begin(), fvars.end(), fsols.begin(), fsols.end()); if (isVerboseOn(1)) { @@ -382,17 +394,6 @@ void SygusSolver::checkSynthSolution(Assertions& as) Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody << "\n"; solChecker->assertFormula(conjBody); - // Assert all auxiliary assertions. This may include recursive function - // definitions that were added as assertions to the sygus problem. - for (Node a : auxAssertions) - { - // We require rewriting here, e.g. so that define-fun from the original - // problem are rewritten to true. If this is not the case, then the - // assertions module of the subsolver will complain about assertions - // with free variables. - Node ar = rewrite(a); - solChecker->assertFormula(ar); - } Result r = solChecker->checkSat(); if (isVerboseOn(1)) { @@ -414,15 +415,47 @@ void SygusSolver::checkSynthSolution(Assertions& as) } } -void SygusSolver::setSygusConjectureStale() +void SygusSolver::initializeSygusSubsolver(std::unique_ptr<SolverEngine>& se, + Assertions& as) { - if (d_sygusConjectureStale) + initializeSubsolver(se, d_env); + // carry the ordinary define-fun definitions + const context::CDList<Node>& alistDefs = as.getAssertionListDefinitions(); + std::unordered_set<Node> processed; + for (const Node& def : alistDefs) { - // already stale - return; + // only consider define-fun, represented as (= f (lambda ...)). + if (def.getKind() == EQUAL) + { + Assert(def[0].isVar()); + std::vector<Node> formals; + Node dbody = def[1]; + if (def[1].getKind() == LAMBDA) + { + formals.insert(formals.end(), def[1][0].begin(), def[1][0].end()); + dbody = dbody[1]; + } + se->defineFunction(def[0], formals, dbody); + processed.insert(def); + } } - d_sygusConjectureStale = true; - // TODO (project #7): if incremental, we should pop a context + // Also assert auxiliary assertions + const context::CDList<Node>& alist = as.getAssertionList(); + for (size_t i = 0, asize = alist.size(); i < asize; ++i) + { + Node a = alist[i]; + // ignore definitions here + if (processed.find(a) == processed.end()) + { + se->assertFormula(a); + } + } +} + +bool SygusSolver::usingSygusSubsolver() const +{ + // use SyGuS subsolver if in incremental mode + return options().base.incrementalSolving; } void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const @@ -467,5 +500,15 @@ void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const } } +std::vector<Node> SygusSolver::listToVector(const NodeList& list) +{ + std::vector<Node> vec; + for (const Node& n : list) + { + vec.push_back(n); + } + return vec; +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 0c742fbd4..4e7a04364 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -18,6 +18,7 @@ #ifndef CVC5__SMT__SYGUS_SOLVER_H #define CVC5__SMT__SYGUS_SOLVER_H +#include "context/cdlist.h" #include "context/cdo.h" #include "expr/node.h" #include "expr/type_node.h" @@ -27,7 +28,7 @@ namespace cvc5 { -class OutputManager; +class SolverEngine; namespace smt { @@ -37,13 +38,28 @@ class SmtSolver; * A solver for sygus queries. * * This class is responsible for responding to check-synth commands. It calls - * check satisfiability using an underlying SmtSolver object. + * check satisfiability using a separate SolverEngine "subsolver". * - * It also maintains a reference to a preprocessor for implementing - * checkSynthSolution. + * This solver operates in two modes. + * + * If in incremental mode, then the "main" SolverEngine for SyGuS inputs only + * maintains a (user-context) dependent state of SyGuS assertions, as well as + * assertions corresponding to (recursive) function definitions. The subsolver + * that solves SyGuS conjectures may be called to checkSat multiple times, + * however, push/pop (which impact SyGuS constraints) impacts only the main + * solver. This means that the conjecture being handled by the subsolver is + * reconstructed when the SyGuS conjecture is updated. The key property that + * this enables is that the subsolver does *not* get calls to push/pop, + * although it may receive multiple check-sat if the sygus functions and + * constraints are not updated between check-sat calls. + * + * If not in incremental mode, then the internal SyGuS conjecture is asserted + * to the "main" SolverEngine. */ class SygusSolver : protected EnvObj { + using NodeList = context::CDList<Node>; + public: SygusSolver(Env& env, SmtSolver& sms); ~SygusSolver(); @@ -134,6 +150,16 @@ class SygusSolver : protected EnvObj * is a valid formula. */ bool getSynthSolutions(std::map<Node, Node>& sol_map); + /** + * Same as above, but used for getting synthesis solutions from a "subsolver" + * that has been initialized to assert the synthesis conjecture as a + * normal assertion. + * + * This method returns true if we are in a state immediately preceded by + * a successful call to checkSat, where this SolverEngine has an asserted + * synthesis conjecture. + */ + bool getSubsolverSynthSolutions(std::map<Node, Node>& solMap); private: /** @@ -143,21 +169,13 @@ class SygusSolver : protected EnvObj * conjecture in which the functions-to-synthesize have been replaced by the * synthesized solutions, which is a quantifier-free formula, is * unsatisfiable. If not, then the found solutions are wrong. - */ - void checkSynthSolution(Assertions& as); - /** - * Set sygus conjecture is stale. The sygus conjecture is stale if either: - * (1) no sygus conjecture has been added as an assertion to this SMT engine, - * (2) there is a sygus conjecture that has been added as an assertion - * internally to this SMT engine, and there have been further calls such that - * the asserted conjecture is no longer up-to-date. * - * This method should be called when new sygus constraints are asserted and - * when functions-to-synthesize are declared. This function pops a user - * context if we are in incremental mode and the sygus conjecture was - * previously not stale. + * @param as The background assertions, which may include define-fun and + * define-fun-rec, + * @param sol_map Map from functions-to-synthesize to their solution (of the + * same type) for the asserted synthesis conjecture. */ - void setSygusConjectureStale(); + void checkSynthSolution(Assertions& as, const std::map<Node, Node>& solMap); /** * Expand definitions in sygus datatype tn, which ensures that all * sygus constructors that are used to build values of sygus datatype @@ -170,7 +188,19 @@ class SygusSolver : protected EnvObj * expansion. */ void expandDefinitionsSygusDt(TypeNode tn) const; - /** The SMT solver, which is used during checkSynth. */ + /** List to vector helper */ + static std::vector<Node> listToVector(const NodeList& list); + /** + * Initialize SyGuS subsolver based on the assertions from the "main" solver. + * This is used for check-synth using a subsolver, and for check-synth-sol. + * This constructs a subsolver se, and makes calls to add all define-fun + * and auxilary assertions. + */ + void initializeSygusSubsolver(std::unique_ptr<SolverEngine>& se, + Assertions& as); + /** Are we using a subsolver for the SyGuS query? */ + bool usingSygusSubsolver() const; + /** The SMT solver. */ SmtSolver& d_smtSolver; /** * sygus variables declared (from "declare-var" and "declare-fun" commands) @@ -178,17 +208,41 @@ class SygusSolver : protected EnvObj * The SyGuS semantics for declared variables is that they are implicitly * universally quantified in the constraints. */ - std::vector<Node> d_sygusVars; + NodeList d_sygusVars; /** sygus constraints */ - std::vector<Node> d_sygusConstraints; + NodeList d_sygusConstraints; /** sygus assumptions */ - std::vector<Node> d_sygusAssumps; + NodeList d_sygusAssumps; /** functions-to-synthesize */ - std::vector<Node> d_sygusFunSymbols; + NodeList d_sygusFunSymbols; + /** The current sygus conjecture */ + Node d_conj; /** * Whether we need to reconstruct the sygus conjecture. + * + * The sygus conjecture is stale if either: + * (1) no sygus conjecture has been added as an assertion to this SMT engine, + * (2) there is a sygus conjecture that has been added as an assertion + * internally to this SMT engine, and there have been further calls such that + * the asserted conjecture is no longer up-to-date. + * + * This flag should be set to true when new sygus constraints are asserted and + * when functions-to-synthesize are declared. */ context::CDO<bool> d_sygusConjectureStale; + /** + * The (context-dependent) pointer to the subsolver we have constructed. + * This is used to verify if the current subsolver is current, in case + * user-context dependent pop has a occurred. If this pointer does not match + * d_subsolver, then d_subsolver must be reconstructed in this context. + */ + context::CDO<SolverEngine*> d_subsolverCd; + /** + * The subsolver we are using. This is a separate copy of the SolverEngine + * which has the asserted synthesis conjecture, i.e. a formula returned by + * quantifiers::SygusUtils::mkSygusConjecture. + */ + std::unique_ptr<SolverEngine> d_subsolver; }; } // namespace smt |