checkUnsatCore();
}
}
- // Check that synthesis solutions satisfy the conjecture
- if (options::checkSynthSol()
- && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- checkSynthSolution();
- }
return r;
} catch (UnsafeInterruptException& e) {
throw ModalException(
"Cannot make check-synth commands when incremental solving is enabled");
}
-
- if (!d_private->d_sygusConjectureStale)
+ Expr query;
+ if (d_private->d_sygusConjectureStale)
{
- // do not need to reconstruct, we're done
- return checkSatisfiability(Expr(), true, false);
- }
-
- // build synthesis conjecture from asserted constraints and declared
- // variables/functions
- Node sygusVar =
- d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType());
- Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar);
- Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr);
- std::vector<Node> bodyv;
- Trace("smt") << "Sygus : Constructing sygus constraint...\n";
- unsigned n_constraints = d_private->d_sygusConstraints.size();
- Node body = n_constraints == 0
- ? d_nodeManager->mkConst(true)
- : (n_constraints == 1
- ? d_private->d_sygusConstraints[0]
- : d_nodeManager->mkNode(
+ // build synthesis conjecture from asserted constraints and declared
+ // variables/functions
+ Node sygusVar =
+ d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType());
+ Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar);
+ Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr);
+ std::vector<Node> bodyv;
+ Trace("smt") << "Sygus : Constructing sygus constraint...\n";
+ unsigned n_constraints = d_private->d_sygusConstraints.size();
+ Node body = n_constraints == 0
+ ? d_nodeManager->mkConst(true)
+ : (n_constraints == 1
+ ? d_private->d_sygusConstraints[0]
+ : d_nodeManager->mkNode(
kind::AND, d_private->d_sygusConstraints));
- body = body.notNode();
- Trace("smt") << "...constructed sygus constraint " << body << std::endl;
- if (!d_private->d_sygusVars.empty())
- {
- Node boundVars =
- d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars);
- body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body);
- Trace("smt") << "...constructed exists " << body << std::endl;
- }
- if (!d_private->d_sygusFunSymbols.empty())
- {
- Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
- d_private->d_sygusFunSymbols);
- body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr);
- }
- Trace("smt") << "...constructed forall " << body << std::endl;
+ body = body.notNode();
+ Trace("smt") << "...constructed sygus constraint " << body << std::endl;
+ if (!d_private->d_sygusVars.empty())
+ {
+ Node boundVars =
+ d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars);
+ body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body);
+ Trace("smt") << "...constructed exists " << body << std::endl;
+ }
+ if (!d_private->d_sygusFunSymbols.empty())
+ {
+ Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
+ d_private->d_sygusFunSymbols);
+ body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr);
+ }
+ Trace("smt") << "...constructed forall " << body << std::endl;
- // set attribute for synthesis conjecture
- setUserAttribute("sygus", sygusVar.toExpr(), {}, "");
+ // set attribute for synthesis conjecture
+ setUserAttribute("sygus", sygusVar.toExpr(), {}, "");
- Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
+ Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
- d_private->d_sygusConjectureStale = false;
+ d_private->d_sygusConjectureStale = false;
- if (options::incrementalSolving())
- {
- // we push a context so that this conjecture is removed if we modify it
- // later
- internalPush();
- assertFormula(body.toExpr(), true);
- return checkSatisfiability(body.toExpr(), true, false);
+ if (options::incrementalSolving())
+ {
+ // we push a context so that this conjecture is removed if we modify it
+ // later
+ internalPush();
+ assertFormula(body.toExpr(), true);
+ }
+ else
+ {
+ query = body.toExpr();
+ }
}
- return checkSatisfiability(body.toExpr(), true, false);
+ Result r = checkSatisfiability(query, true, false);
+
+ // Check that synthesis solutions satisfy the conjecture
+ if (options::checkSynthSol()
+ && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ checkSynthSolution();
+ }
+ return r;
}
/*
Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl;
map<Node, Node> sol_map;
/* Get solutions and build auxiliary vectors for substituting */
- d_theoryEngine->getSynthSolutions(sol_map);
+ if (!d_theoryEngine->getSynthSolutions(sol_map))
+ {
+ InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
+ return;
+ }
if (sol_map.empty())
{
- Trace("check-synth-sol") << "No solution to check!\n";
+ InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!";
return;
}
Trace("check-synth-sol") << "Got solution map:\n";
}
}
-void SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
+bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
{
SmtScope smts(this);
finalOptionsAreSet();
map<Node, Node> sol_mapn;
Assert(d_theoryEngine != nullptr);
- d_theoryEngine->getSynthSolutions(sol_mapn);
+ if (!d_theoryEngine->getSynthSolutions(sol_mapn))
+ {
+ return false;
+ }
for (std::pair<const Node, Node>& s : sol_mapn)
{
sol_map[s.first.toExpr()] = s.second.toExpr();
}
+ return true;
}
Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
/**
* Get synth solution.
*
- * This function adds entries to sol_map that map functions-to-synthesize with
+ * This method returns true if we are in a state immediately preceeded by
+ * a successful call to checkSynth.
+ *
+ * This method adds entries to sol_map that map functions-to-synthesize with
* their solutions, for all active conjectures. This should be called
* immediately after the solver answers unsat for sygus input.
*
* forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn )
* is a valid formula.
*/
- void getSynthSolutions(std::map<Expr, Expr>& sol_map);
+ bool getSynthSolutions(std::map<Expr, Expr>& sol_map);
/**
* Do quantifier elimination.
: d_qe(qe),
d_parent(p),
d_tds(qe->getTermDatabaseSygus()),
- d_hasSolution(false, qe->getUserContext()),
+ d_hasSolution(false),
d_ceg_si(new CegSingleInv(qe, this)),
d_ceg_proc(new SynthConjectureProcess(qe)),
d_ceg_gc(new CegGrammarConstructor(qe, this)),
return true;
}
Assert(d_master != nullptr);
+ Assert(!d_hasSolution);
// get the list of terms that the master strategy is interested in
std::vector<Node> terms;
lem = getStreamGuardedLemma(lem);
lems.push_back(lem);
recordInstantiation(candidate_values);
+ d_hasSolution = true;
return true;
}
Assert(!d_set_ce_sk_vars);
}
if (success)
{
+ d_hasSolution = true;
if (options::sygusStream())
{
// if we were successful, we immediately print the current solution.
// this saves us from introducing a verification lemma and a new guard.
printAndContinueStream(terms, candidate_values);
+ // streaming means now we immediately are looking for a new solution
+ d_hasSolution = false;
return false;
}
- d_hasSolution = true;
}
lem = getStreamGuardedLemma(lem);
lems.push_back(lem);
}
}
-void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> sols;
std::vector<int> statuses;
if (!getSynthSolutionsInternal(sols, statuses))
{
- return;
+ return false;
}
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
// store in map
sol_map[fvar] = bsol;
}
+ return true;
}
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
std::vector<int>& statuses)
{
+ if (!d_hasSolution)
+ {
+ return false;
+ }
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
Node prog = d_embed_quant[0][i];
void printSynthSolution(std::ostream& out);
/** get synth solutions
*
- * This returns a map from function-to-synthesize variables to their
- * builtin solution, which has the same type. For example, for synthesis
+ * This method returns true if this class has a solution available to the
+ * conjecture that it was assigned.
+ *
+ * This method adds entries to sol_map that map functions-to-synthesize to
+ * their builtin solution, which has the same type. For example, for synthesis
* conjecture exists f. forall x. f( x )>x, this function may return the map
* containing the entry:
* f -> (lambda x. x+1)
*/
- void getSynthSolutions(std::map<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, Node>& sol_map);
/**
* The feasible guard whose semantics are "this conjecture is feasiable".
* This is "G" in Figure 3 of Reynolds et al CAV 2015.
/** The feasible guard. */
Node d_feasible_guard;
/**
- * Do we have a solution in this user context? This is user-context dependent
- * to enable use cases of sygus in incremental mode.
+ * Do we have a solution in this solve context? This flag is reset to false
+ * on every call to presolve.
*/
- context::CDO<bool> d_hasSolution;
+ bool d_hasSolution;
/** the decision strategy for the feasible guard */
std::unique_ptr<DecisionStrategy> d_feasible_strategy;
/** single invocation utility */
}
SynthEngine::~SynthEngine() {}
+
+void SynthEngine::presolve()
+{
+ Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl;
+ for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
+ {
+ d_conjs[i]->presolve();
+ }
+ Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl;
+}
+
bool SynthEngine::needsCheck(Theory::Effort e)
{
return e >= Theory::EFFORT_LAST_CALL;
void SynthEngine::assignConjecture(Node q)
{
- Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl;
+ Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl;
if (options::sygusQePreproc())
{
// the following does quantifier elimination as a preprocess step
}
}
-void SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
{
+ bool ret = true;
for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
if (d_conjs[i]->isAssigned())
{
- d_conjs[i]->getSynthSolutions(sol_map);
+ if (!d_conjs[i]->getSynthSolutions(sol_map))
+ {
+ // if one conjecture fails, we fail overall
+ ret = false;
+ break;
+ }
}
}
+ return ret;
}
void SynthEngine::preregisterAssertion(Node n)
public:
SynthEngine(QuantifiersEngine* qe, context::Context* c);
~SynthEngine();
-
+ /** presolve
+ *
+ * Called at the beginning of each call to solve a synthesis problem, which
+ * may be e.g. a check-synth or get-abduct call.
+ */
+ void presolve() override;
+ /** needs check, return true if e is last call */
bool needsCheck(Theory::Effort e) override;
+ /** always needs model at effort QEFFORT_MODEL */
QEffort needsModel(Theory::Effort e) override;
/* Call during quantifier engine's check */
void check(Theory::Effort e, QEffort quant_e) override;
* For details on what is added to sol_map, see
* SynthConjecture::getSynthSolutions.
*/
- void getSynthSolutions(std::map<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, Node>& sol_map);
/** preregister assertion (before rewrite)
*
* The purpose of this method is to inform the solution reconstruction
return ret;
}
-void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
{
- d_private->d_synth_e->getSynthSolutions(sol_map);
+ return d_private->d_synth_e->getSynthSolutions(sol_map);
}
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
/** get synth solutions
*
- * This function adds entries to sol_map that map functions-to-synthesize with
+ * This method returns true if there is a synthesis solution available. This
+ * is the case if the last call to check satisfiability originated in a
+ * check-synth call, and the synthesis engine module of this class
+ * successfully found a solution for all active synthesis conjectures.
+ *
+ * This method adds entries to sol_map that map functions-to-synthesize with
* their solutions, for all active conjectures. This should be called
* immediately after the solver answers unsat for sygus input.
*
* For details on what is added to sol_map, see
- * CegConjecture::getSynthSolutions.
+ * SynthConjecture::getSynthSolutions.
*/
- void getSynthSolutions(std::map<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, Node>& sol_map);
//----------end user interface for instantiations
return d_curr_model;
}
-void TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
{
if (d_quantEngine)
{
- d_quantEngine->getSynthSolutions(sol_map);
- }
- else
- {
- Assert(false);
+ return d_quantEngine->getSynthSolutions(sol_map);
}
+ // we are not in a quantified logic, there is no synthesis solution
+ return false;
}
bool TheoryEngine::presolve() {
/** get synth solutions
*
- * This function adds entries to sol_map that map functions-to-synthesize with
+ * This method returns true if there is a synthesis solution available. This
+ * is the case if the last call to check satisfiability originated in a
+ * check-synth call, and the synthesis solver successfully found a solution
+ * for all active synthesis conjectures.
+ *
+ * This method adds entries to sol_map that map functions-to-synthesize with
* their solutions, for all active conjectures. This should be called
* immediately after the solver answers unsat for sygus input.
*
* For details on what is added to sol_map, see
- * CegConjecture::getSynthSolutions.
+ * SynthConjecture::getSynthSolutions.
*/
- void getSynthSolutions(std::map<Node, Node>& sol_map);
+ bool getSynthSolutions(std::map<Node, Node>& sol_map);
/**
* Get the model builder
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
-; COMMAND-LINE: --sygus-out=status --cegis-sample=trust
+; COMMAND-LINE: --sygus-out=status --cegis-sample=trust --no-check-synth-sol
(set-logic BV)
; we test --cegis-sample=trust since we can exhaustively sample BV4
projects / cvc5.git / commitdiff