namespace quantifiers {
SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
- SynthEngine* p,
SygusStatistics& s)
: d_qe(qe),
- d_parent(p),
d_stats(s),
d_tds(qe->getTermDatabaseSygus()),
d_hasSolution(false),
d_qe->getOutputChannel().lemma(lem);
}
- if (options::sygusStream())
- {
- d_stream_strategy.reset(new SygusStreamDecisionStrategy(
- d_qe->getSatContext(), d_qe->getValuation()));
- d_qe->getDecisionManager()->registerStrategy(
- DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE,
- d_stream_strategy.get());
- d_current_stream_guard = d_stream_strategy->getLiteral(0);
- }
Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
<< std::endl;
}
{
d_hasSolution = true;
// the conjecture has a solution, so its negation holds
- Node lem = d_quant.negate();
- lem = getStreamGuardedLemma(lem);
- lems.push_back(lem);
+ lems.push_back(d_quant.negate());
}
return true;
}
std::vector<Node> terms;
d_master->getTermList(d_candidates, terms);
- // process the sygus streaming guard
- if (options::sygusStream())
- {
- Assert(!isSingleInvocation());
- // it may be the case that we have a new solution now
- Node currGuard = getCurrentStreamGuard();
- if (currGuard != d_current_stream_guard)
- {
- std::vector<Node> vals;
- std::vector<int> status;
- getSynthSolutionsInternal(vals, status);
- // we have a new guard, print and continue the stream
- printAndContinueStream(terms, vals);
- d_current_stream_guard = currGuard;
- return true;
- }
- }
-
Assert(!d_candidates.empty());
Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
// we have that the current candidate passed a sample test
// since we trust sampling in this mode, we assert there is no
// counterexample to the conjecture here.
- Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false));
- lem = getStreamGuardedLemma(lem);
- lems.push_back(lem);
- recordInstantiation(candidate_values);
- d_hasSolution = true;
+ lems.push_back(d_quant.negate());
+ recordSolution(candidate_values);
return true;
}
Assert(!d_set_ce_sk_vars);
// immediately skolemize inner existentials
- Node lem;
+ Node query;
// introduce the skolem variables
std::vector<Node> sks;
std::vector<Node> vars;
Trace("cegqi-check-debug")
<< " introduce skolem " << sk << " for " << v << "\n";
}
- lem = inst[0][1].substitute(
+ query = inst[0][1].substitute(
vars.begin(), vars.end(), sks.begin(), sks.end());
- lem = lem.negate();
+ query = query.negate();
}
else
{
// use the instance itself
- lem = inst;
+ query = inst;
}
}
d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
d_set_ce_sk_vars = true;
- if (lem.isNull())
+ if (query.isNull())
{
// no lemma to check
return false;
}
// simplify the lemma based on the term database sygus utility
- lem = d_tds->rewriteNode(lem);
+ query = d_tds->rewriteNode(query);
// eagerly unfold applications of evaluation function
- Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
- // record the instantiation
- // this is used for remembering the solution
- recordInstantiation(candidate_values);
-
- Node query = lem;
- bool success = false;
- if (query.isConst() && !query.getConst<bool>())
- {
- // short circuit the check
- lem = d_quant.negate();
- success = true;
- }
- else
+ Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl;
+ // Record the solution, which may be falsified below. We require recording
+ // here since the result of the satisfiability test may be unknown.
+ recordSolution(candidate_values);
+
+ if (!query.isConst() || query.getConst<bool>())
{
- // This is the "verification lemma", which states
- // either this conjecture does not have a solution, or candidate_values
- // is a solution for this conjecture.
- lem = nm->mkNode(OR, d_quant.negate(), query);
Trace("sygus-engine") << " *** Verify with subcall..." << std::endl;
-
Result r =
checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
Trace("sygus-engine") << " ...got " << r << std::endl;
}
return false;
}
- else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- // if the result in the subcall was unsatisfiable, we avoid
- // rechecking, hence we drop "query" from the verification lemma
- lem = d_quant.negate();
- // we can short circuit adding the lemma (for sygus stream)
- success = true;
- }
- else
+ else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
// In the rare case that the subcall is unknown, we simply exclude the
// solution, without adding a counterexample point. This should only
d_qe->getOutputChannel().setIncomplete();
return false;
}
+ // otherwise we are unsat, and we will process the solution below
}
- if (success)
+ // now mark that we have a solution
+ d_hasSolution = true;
+ if (options::sygusStream())
{
- 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;
- }
+ // immediately print the current solution
+ printAndContinueStream(terms, candidate_values);
+ // streaming means now we immediately are looking for a new solution
+ d_hasSolution = false;
+ return false;
}
- lem = getStreamGuardedLemma(lem);
- lems.push_back(lem);
+ // Use lemma to terminate with "unsat", this is justified by the verification
+ // check above, which confirms the synthesis conjecture is solved.
+ lems.push_back(d_quant.negate());
return true;
}
Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl;
}
-Node SynthConjecture::getCurrentStreamGuard() const
-{
- if (d_stream_strategy != nullptr)
- {
- // the stream guard is the current asserted literal of the stream strategy
- Node lit = d_stream_strategy->getAssertedLiteral();
- if (lit.isNull())
- {
- // if none exist, get the first
- lit = d_stream_strategy->getLiteral(0);
- }
- return lit;
- }
- return Node::null();
-}
-
-Node SynthConjecture::getStreamGuardedLemma(Node n) const
-{
- if (options::sygusStream())
- {
- // if we are in streaming mode, we guard with the current stream guard
- Node csg = getCurrentStreamGuard();
- Assert(!csg.isNull());
- return NodeManager::currentNM()->mkNode(kind::OR, csg.negate(), n);
- }
- return n;
-}
-
-SynthConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy(
- context::Context* satContext, Valuation valuation)
- : DecisionStrategyFmf(satContext, valuation)
-{
-}
-
-Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i)
-{
- NodeManager* nm = NodeManager::currentNM();
- Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType());
- return curr_stream_guard;
-}
-
void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
const std::vector<Node>& values)
{
return true;
}
+void SynthConjecture::recordSolution(std::vector<Node>& vs)
+{
+ Assert(vs.size() == d_candidates.size());
+ d_cinfo.clear();
+ for (unsigned i = 0; i < vs.size(); i++)
+ {
+ d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
+ }
+}
+
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
std::vector<int>& statuses)
{
}
else
{
- Node cprog = getCandidate(i);
+ Node cprog = d_candidates[i];
if (!d_cinfo[cprog].d_inst.empty())
{
// the solution is just the last instantiated term
namespace theory {
namespace quantifiers {
-class SynthEngine;
class SygusStatistics;
/**
class SynthConjecture
{
public:
- SynthConjecture(QuantifiersEngine* qe, SynthEngine* p, SygusStatistics& s);
+ SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s);
~SynthConjecture();
/** presolve */
void presolve();
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
- /** pointer to the synth engine that owns this */
- SynthEngine* d_parent;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
/** term database sygus of d_qe */
unsigned d_repair_index;
/** number of times we have called doRefine */
unsigned d_refine_count;
- /** get candidadate */
- Node getCandidate(unsigned int i) { return d_candidates[i]; }
- /** record instantiation (this is used to construct solutions later) */
- void recordInstantiation(std::vector<Node>& vs)
- {
- Assert(vs.size() == d_candidates.size());
- for (unsigned i = 0; i < vs.size(); i++)
- {
- d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
- }
- }
+ /** record solution (this is used to construct solutions later) */
+ void recordSolution(std::vector<Node>& vs);
/** get synth solutions internal
*
* This function constructs the body of solutions for all
bool getSynthSolutionsInternal(std::vector<Node>& sols,
std::vector<int>& status);
//-------------------------------- sygus stream
- /** current stream guard */
- Node d_current_stream_guard;
- /** the decision strategy for streaming solutions */
- class SygusStreamDecisionStrategy : public DecisionStrategyFmf
- {
- public:
- SygusStreamDecisionStrategy(context::Context* satContext,
- Valuation valuation);
- /** make literal */
- Node mkLiteral(unsigned i) override;
- /** identify */
- std::string identify() const override
- {
- return std::string("sygus_stream");
- }
- };
- std::unique_ptr<SygusStreamDecisionStrategy> d_stream_strategy;
- /** get current stream guard */
- Node getCurrentStreamGuard() const;
- /** get stream guarded lemma
- *
- * If sygusStream is enabled, this returns ( G V n ) where G is the guard
- * returned by getCurrentStreamGuard, otherwise this returns n.
- */
- Node getStreamGuardedLemma(Node n) const;
/**
* Prints the current synthesis solution to the output stream indicated by
* the Options object, send a lemma blocking the current solution to the
projects / cvc5.git / commitdiff