summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/abduction_solver.cpp10
-rw-r--r--src/smt/abstract_values.h6
-rw-r--r--src/smt/check_models.cpp2
-rw-r--r--src/smt/difficulty_post_processor.cpp2
-rw-r--r--src/smt/interpolation_solver.cpp1
-rw-r--r--src/smt/model.cpp3
-rw-r--r--src/smt/preprocessor.cpp4
-rw-r--r--src/smt/proof_final_callback.cpp30
-rw-r--r--src/smt/proof_final_callback.h5
-rw-r--r--src/smt/proof_manager.cpp23
-rw-r--r--src/smt/proof_post_processor.cpp9
-rw-r--r--src/smt/set_defaults.cpp9
-rw-r--r--src/smt/smt_solver.cpp8
-rw-r--r--src/smt/solver_engine.cpp23
-rw-r--r--src/smt/solver_engine.h16
-rw-r--r--src/smt/sygus_solver.cpp315
-rw-r--r--src/smt/sygus_solver.h98
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback