// get the current output stream
// this output stream should coincide with wherever --dump-synth is output on
Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
- printSynthSolution(*nodeManagerOptions.getOut(), false);
+ printSynthSolution(*nodeManagerOptions.getOut());
// We will not refine the current candidate solution since it is a solution
// thus, we clear information regarding the current refinement
}
}
-void SynthConjecture::printSynthSolution(std::ostream& out,
- bool singleInvocation)
+void SynthConjecture::printSynthSolution(std::ostream& out)
{
Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
std::vector<Node> sols;
std::vector<int> statuses;
- if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
+ if (!getSynthSolutionsInternal(sols, statuses))
{
return;
}
}
}
-void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
- bool singleInvocation)
+void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> sols;
std::vector<int> statuses;
- if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
+ if (!getSynthSolutionsInternal(sols, statuses))
{
return;
}
}
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
- std::vector<int>& statuses,
- bool singleInvocation)
+ std::vector<int>& statuses)
{
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
// get the solution
Node sol;
int status = -1;
- if (singleInvocation)
+ if (isSingleInvocation())
{
Assert(d_ceg_si != NULL);
sol = d_ceg_si->getSolution(i, tn, status, true);
void doRefine(std::vector<Node>& lems);
//-------------------------------end for counterexample-guided check/refine
/**
- * prints the synthesis solution to output stream out.
- *
- * singleInvocation : set to true if we should consult the single invocation
- * module to get synthesis solutions.
+ * Prints the synthesis solution to output stream out. This invokes solution
+ * reconstruction if the conjecture is single invocation. Otherwise, it
+ * returns the enumer
*/
- void printSynthSolution(std::ostream& out, bool singleInvocation);
+ void printSynthSolution(std::ostream& out);
/** get synth solutions
*
* This returns a map from function-to-synthesize variables to their
* conjecture exists f. forall x. f( x )>x, this function may return the map
* containing the entry:
* f -> (lambda x. x+1)
- *
- * singleInvocation : set to true if we should consult the single invocation
- * module to get synthesis solutions.
*/
- void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation);
+ void 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.
* We store builtin versions under some conditions (such as when the sygus
* grammar is being ignored).
*
- * singleInvocation : set to true if we should consult the single invocation
- * module to get synthesis solutions.
+ * This consults the single invocation module to get synthesis solutions if
+ * isSingleInvocation() returns true.
*
* For example, for conjecture exists fg. forall x. f(x)>g(x), this function
* may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
* the sygus datatype constructor corresponding to variable x.
*/
bool getSynthSolutionsInternal(std::vector<Node>& sols,
- std::vector<int>& status,
- bool singleInvocation);
+ std::vector<int>& status);
//-------------------------------- sygus stream
/** current stream guard */
Node d_current_stream_guard;
SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
: QuantifiersModule(qe)
{
- d_conj = new SynthConjecture(qe);
- d_last_inst_si = false;
+ d_conjs.push_back(
+ std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
+ d_conj = d_conjs.back().get();
}
-SynthEngine::~SynthEngine() { delete d_conj; }
-
+SynthEngine::~SynthEngine() {}
bool SynthEngine::needsCheck(Theory::Effort e)
{
return e >= Theory::EFFORT_LAST_CALL;
QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
{
- return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
+ return QEFFORT_MODEL;
}
void SynthEngine::check(Theory::Effort e, QEffort quant_e)
{
// are we at the proper effort level?
- unsigned echeck =
- d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
- if (quant_e != echeck)
+ if (quant_e != QEFFORT_MODEL)
{
return;
}
// if we are waiting to assign the conjecture, do it now
- if (!d_waiting_conj.isNull())
+ bool assigned = !d_waiting_conj.empty();
+ while (!d_waiting_conj.empty())
{
- Node q = d_waiting_conj;
+ Node q = d_waiting_conj.back();
+ d_waiting_conj.pop_back();
Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q
<< std::endl;
- d_waiting_conj = Node::null();
- if (!d_conj->isAssigned())
- {
- assignConjecture(q);
- // assign conjecture always uses the output channel, we return and
- // re-check here.
- return;
- }
+ assignConjecture(q);
+ }
+ if (assigned)
+ {
+ // assign conjecture always uses the output channel, either by reducing a
+ // quantified formula to another, or adding initial lemmas during
+ // SynthConjecture::assign. Thus, we return here and re-check.
+ return;
}
Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---"
<< std::endl;
Trace("cegqi-engine-debug") << std::endl;
- bool active = false;
- bool value;
- if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value))
- {
- active = value;
- }
- else
+ Valuation& valuation = d_quantEngine->getValuation();
+ for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
+ SynthConjecture* sc = d_conjs[i].get();
+ bool active = false;
+ bool value;
+ if (valuation.hasSatValue(sc->getConjecture(), value))
+ {
+ active = value;
+ }
+ else
+ {
+ Trace("cegqi-engine-debug") << "...no value for quantified formula."
+ << std::endl;
+ }
Trace("cegqi-engine-debug")
- << "...no value for quantified formula." << std::endl;
- }
- Trace("cegqi-engine-debug")
- << "Current conjecture status : active : " << active << std::endl;
- if (active && d_conj->needsCheck())
- {
- checkConjecture(d_conj);
+ << "Current conjecture status : active : " << active << std::endl;
+ if (active && sc->needsCheck())
+ {
+ checkConjecture(sc);
+ }
}
Trace("cegqi-engine")
<< "Finished Counterexample Guided Instantiation engine." << std::endl;
}
-bool SynthEngine::assignConjecture(Node q)
+void SynthEngine::assignConjecture(Node q)
{
- if (d_conj->isAssigned())
- {
- return false;
- }
Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl;
if (options::sygusQePreproc())
{
<< std::endl;
d_quantEngine->getOutputChannel().lemma(lem);
// we've reduced the original to a preprocessed version, return
- return false;
+ return;
}
}
- d_conj->assign(q);
- return true;
+ // allocate a new synthesis conjecture if not assigned
+ if (d_conjs.back()->isAssigned())
+ {
+ d_conjs.push_back(
+ std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
+ }
+ d_conjs.back()->assign(q);
}
void SynthEngine::registerQuantifier(Node q)
{
if (d_quantEngine->getOwner(q) == this)
- { // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
- if (!d_conj->isAssigned())
+ {
+ Trace("cegqi") << "Register conjecture : " << q << std::endl;
+ if (options::sygusQePreproc())
{
- Trace("cegqi") << "Register conjecture : " << q << std::endl;
- if (options::sygusQePreproc())
- {
- d_waiting_conj = q;
- }
- else
- {
- // assign it now
- assignConjecture(q);
- }
+ d_waiting_conj.push_back(q);
}
else
{
- Assert(d_conj->getEmbeddedConjecture() == q);
+ // assign it now
+ assignConjecture(q);
}
}
else
conj->doSingleInvCheck(clems);
if (!clems.empty())
{
- d_last_inst_si = true;
for (const Node& lem : clems)
{
Trace("cegqi-lemma")
bool addedLemma = false;
for (const Node& lem : cclems)
{
- d_last_inst_si = false;
Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem
<< std::endl;
if (d_quantEngine->addLemma(lem))
void SynthEngine::printSynthSolution(std::ostream& out)
{
- if (d_conj->isAssigned())
- {
- d_conj->printSynthSolution(out, d_last_inst_si);
- }
- else
+ Assert(!d_conjs.empty());
+ for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
- Assert(false);
+ if (d_conjs[i]->isAssigned())
+ {
+ d_conjs[i]->printSynthSolution(out);
+ }
}
}
void SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
{
- if (d_conj->isAssigned())
+ for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
- d_conj->getSynthSolutions(sol_map, d_last_inst_si);
+ if (d_conjs[i]->isAssigned())
+ {
+ d_conjs[i]->getSynthSolutions(sol_map);
+ }
}
}
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
- /** the quantified formula stating the synthesis conjecture */
+ /** the conjecture formula(s) we are waiting to assign */
+ std::vector<Node> d_waiting_conj;
+ /** The synthesis conjectures that this class is managing. */
+ std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
+ /**
+ * The first conjecture in the above vector. We track this conjecture
+ * so that a synthesis conjecture can be preregistered during a call to
+ * preregisterAssertion.
+ */
SynthConjecture* d_conj;
- /** last instantiation by single invocation module? */
- bool d_last_inst_si;
- /** the conjecture we are waiting to assign */
- Node d_waiting_conj;
-
- private:
- /** assign quantified formula q as the conjecture
+ /** assign quantified formula q as a conjecture
*
- * This method returns true if q was successfully assigned as the synthesis
- * conjecture considered by this class. This method may return false, for
- * instance, if this class determines that it would rather rewrite q to
- * an equivalent form r (in which case this method returns the lemma
- * q <=> r). An example of this is the quantifier elimination step
- * option::sygusQePreproc().
+ * This method either assigns q to a synthesis conjecture object in d_conjs,
+ * or otherwise reduces q to an equivalent form. This method does the latter
+ * if this class determines that it would rather rewrite q to an equivalent
+ * form r (in which case this method returns the lemma q <=> r). An example of
+ * this is the quantifier elimination step option::sygusQePreproc().
*/
- bool assignConjecture(Node q);
+ void assignConjecture(Node q);
/** check conjecture */
void checkConjecture(SynthConjecture* conj);
SynthEngine(QuantifiersEngine* qe, context::Context* c);
~SynthEngine();
- public:
bool needsCheck(Theory::Effort e) override;
QEffort needsModel(Theory::Effort e) override;
/* Call during quantifier engine's check */
* SynthConjecture::getSynthSolutions.
*/
void getSynthSolutions(std::map<Node, Node>& sol_map);
- /** preregister assertion (before rewrite) */
+ /** preregister assertion (before rewrite)
+ *
+ * The purpose of this method is to inform the solution reconstruction
+ * techniques within the single invocation module that n is an original
+ * assertion, prior to rewriting. This is used as a heuristic to remember
+ * terms that are likely to help when trying to reconstruct a solution
+ * that fits a given input syntax.
+ */
void preregisterAssertion(Node n);
public:
projects / cvc5.git / commitdiff