This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
for (size_t i = 0; i < size; ++i)
{
Node prev = (*assertionsToPreprocess)[i];
- Node next = quantifiers::QuantifiersRewriter::preprocess(prev);
- if (next != prev)
+ TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev);
+ if (!trn.isNull())
{
+ Node next = trn.getNode();
assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
Trace("quantifiers-preprocess")
using namespace std;
using namespace CVC4::kind;
+using namespace CVC4::theory;
namespace CVC4 {
namespace preprocessing {
if (pas.getKind() == FORALL)
{
// preprocess the quantified formula
- pas = theory::quantifiers::QuantifiersRewriter::preprocess(pas);
+ TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas);
+ if (!trn.isNull())
+ {
+ pas = trn.getNode();
+ }
Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl;
}
if (pas.getKind() == FORALL)
{
}
-Node InstRewriterCegqi::rewriteInstantiation(Node q,
- std::vector<Node>& terms,
- Node inst,
- bool doVts)
+TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts)
{
return d_parent->rewriteInstantiation(q, terms, inst, doVts);
}
}
}
}
-Node InstStrategyCegqi::rewriteInstantiation(Node q,
- std::vector<Node>& terms,
- Node inst,
- bool doVts)
+TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts)
{
+ Node prevInst = inst;
if (doVts)
{
// do virtual term substitution
{
inst = doNestedQE(q, terms, inst, doVts);
}
- return inst;
+ if (prevInst != inst)
+ {
+ // not proof producing yet
+ return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
+ }
+ return TrustNode::null();
}
InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
~InstRewriterCegqi() {}
/**
* Rewrite the instantiation via d_parent, based on virtual term substitution
- * and nested quantifier elimination.
+ * and nested quantifier elimination. Returns a TrustNode of kind REWRITE,
+ * corresponding to the rewrite and its proof generator.
*/
- Node rewriteInstantiation(Node q,
- std::vector<Node>& terms,
- Node inst,
- bool doVts) override;
+ TrustNode rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts) override;
private:
/** pointer to the parent of this class */
* We rewrite inst based on virtual term substitution and nested quantifier
* elimination. For details, see "Solving Quantified Linear Arithmetic via
* Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al.
+ *
+ * Returns a TrustNode of kind REWRITE, corresponding to the rewrite and its
+ * proof generator.
*/
- Node rewriteInstantiation(Node q,
- std::vector<Node>& terms,
- Node inst,
- bool doVts);
+ TrustNode rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts);
/** get the instantiation rewriter object */
InstantiationRewriter* getInstRewriter() const;
namespace theory {
namespace quantifiers {
-Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u)
+Instantiate::Instantiate(QuantifiersEngine* qe,
+ context::UserContext* u,
+ ProofNodeManager* pnm)
: d_qe(qe),
+ d_pnm(pnm),
d_term_db(nullptr),
d_term_util(nullptr),
d_total_inst_debug(u),
- d_c_inst_match_trie_dom(u)
+ d_c_inst_match_trie_dom(u),
+ d_pfInst(pnm ? new CDProof(pnm) : nullptr)
{
}
return false;
}
+ // Set up a proof if proofs are enabled. This proof stores a proof of
+ // the instantiation body with q as a free assumption.
+ std::shared_ptr<LazyCDProof> pfTmp;
+ if (isProofEnabled())
+ {
+ pfTmp.reset(new LazyCDProof(
+ d_pnm, nullptr, nullptr, "Instantiate::LazyCDProof::tmp"));
+ }
+
// construct the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
Assert(d_term_util->d_vars[q].size() == terms.size());
// get the instantiation
- Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+ Node body =
+ getInstantiation(q, d_term_util->d_vars[q], terms, doVts, pfTmp.get());
Node orig_body = body;
- // now preprocess
- body = quantifiers::QuantifiersRewriter::preprocess(body, true);
+ // now preprocess, storing the trust node for the rewrite
+ TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true);
+ if (!tpBody.isNull())
+ {
+ Assert(tpBody.getKind() == TrustNodeKind::REWRITE);
+ body = tpBody.getNode();
+ // do a tranformation step
+ if (pfTmp != nullptr)
+ {
+ // ----------------- from preprocess
+ // orig_body orig_body = body
+ // ------------------------------ EQ_RESOLVE
+ // body
+ Node proven = tpBody.getProven();
+ // add the transformation proof, or THEORY_PREPROCESS if none provided
+ pfTmp->addLazyStep(proven,
+ tpBody.getGenerator(),
+ true,
+ "Instantiate::getInstantiation:qpreprocess",
+ false,
+ PfRule::THEORY_PREPROCESS);
+ pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {body});
+ }
+ }
Trace("inst-debug") << "...preprocess to " << body << std::endl;
// construct the lemma
Trace("inst-assert") << "(assert " << body << ")" << std::endl;
- Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
- lem = Rewriter::rewrite(lem);
+ // construct the instantiation, and rewrite the lemma
+ Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, q, body);
+
+ // If proofs are enabled, construct the proof, which is of the form:
+ // ... free assumption q ...
+ // ------------------------- from pfTmp
+ // body
+ // ------------------------- SCOPE
+ // (=> q body)
+ // -------------------------- MACRO_SR_PRED_ELIM
+ // lem
+ bool hasProof = false;
+ if (isProofEnabled())
+ {
+ // make the proof of body
+ std::shared_ptr<ProofNode> pfn = pfTmp->getProofFor(body);
+ // make the scope proof to get (=> q body)
+ std::vector<Node> assumps;
+ assumps.push_back(q);
+ std::shared_ptr<ProofNode> pfns = d_pnm->mkScope({pfn}, assumps);
+ Assert(assumps.size() == 1 && assumps[0] == q);
+ // store in the main proof
+ d_pfInst->addProof(pfns);
+ Node prevLem = lem;
+ lem = Rewriter::rewrite(lem);
+ if (prevLem != lem)
+ {
+ d_pfInst->addStep(lem, PfRule::MACRO_SR_PRED_ELIM, {prevLem}, {});
+ }
+ hasProof = true;
+ }
+ else
+ {
+ lem = Rewriter::rewrite(lem);
+ }
- // check for lemma duplication
- if (!d_qe->addLemma(lem, true, false))
+ // added lemma, which checks for lemma duplication
+ bool addedLem = false;
+ if (hasProof)
+ {
+ // use trust interface
+ TrustNode tlem = TrustNode::mkTrustLemma(lem, d_pfInst.get());
+ addedLem = d_qe->addTrustedLemma(tlem, true, false);
+ }
+ else
+ {
+ addedLem = d_qe->addLemma(lem, true, false);
+ }
+
+ if (!addedLem)
{
Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
++(d_statistics.d_inst_duplicate);
Node Instantiate::getInstantiation(Node q,
std::vector<Node>& vars,
std::vector<Node>& terms,
- bool doVts)
+ bool doVts,
+ LazyCDProof* pf)
{
Node body;
Assert(vars.size() == terms.size());
// Notice that this could be optimized, but no significant performance
// improvements were observed with alternative implementations (see #1386).
body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
+
+ // store the proof of the instantiated body, with (open) assumption q
+ if (pf != nullptr)
+ {
+ pf->addStep(body, PfRule::INSTANTIATE, {q}, terms);
+ }
+
// run rewriters to rewrite the instantiation in sequence.
for (InstantiationRewriter*& ir : d_instRewrite)
{
- body = ir->rewriteInstantiation(q, terms, body, doVts);
+ TrustNode trn = ir->rewriteInstantiation(q, terms, body, doVts);
+ if (!trn.isNull())
+ {
+ Node newBody = trn.getNode();
+ // if using proofs, we store a preprocess + transformation step.
+ if (pf != nullptr)
+ {
+ Node proven = trn.getProven();
+ pf->addLazyStep(proven,
+ trn.getGenerator(),
+ true,
+ "Instantiate::getInstantiation:rewrite_inst",
+ false,
+ PfRule::THEORY_PREPROCESS);
+ pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {});
+ }
+ body = newBody;
+ }
}
return body;
}
#endif
}
+bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
+
void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
{
if (!options::trackInstLemmas())
#include <map>
#include "expr/node.h"
+#include "expr/proof.h"
#include "theory/quantifiers/inst_match_trie.h"
#include "theory/quantifiers/quant_util.h"
#include "util/statistics_registry.h"
*
* The flag doVts is whether we must apply virtual term substitution to the
* instantiation.
+ *
+ * Returns a TrustNode of kind REWRITE, corresponding to the rewrite of inst
+ * and its proof generator.
*/
- virtual Node rewriteInstantiation(Node q,
- std::vector<Node>& terms,
- Node inst,
- bool doVts) = 0;
+ virtual TrustNode rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts) = 0;
};
/** Instantiate
typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
public:
- Instantiate(QuantifiersEngine* qe, context::UserContext* u);
+ Instantiate(QuantifiersEngine* qe,
+ context::UserContext* u,
+ ProofNodeManager* pnm = nullptr);
~Instantiate();
/** reset */
*
* Returns the instantiation lemma for q under substitution { vars -> terms }.
* doVts is whether to apply virtual term substitution to its body.
+ *
+ * If provided, pf is a lazy proof for which we store a proof of the
+ * returned formula with free assumption q. This typically stores a
+ * single INSTANTIATE step concluding the instantiated body of q from q.
*/
Node getInstantiation(Node q,
std::vector<Node>& vars,
std::vector<Node>& terms,
- bool doVts = false);
+ bool doVts = false,
+ LazyCDProof* pf = nullptr);
/** get instantiation
*
* Same as above, but with vars/terms specified by InstMatch m.
std::map<Node, std::vector<Node> >& tvec);
//--------------------------------------end user-level interface utilities
+ /** Are proofs enabled for this object? */
+ bool isProofEnabled() const;
+
/** statistics class
*
* This tracks statistics on the number of instantiations successfully
/** pointer to the quantifiers engine */
QuantifiersEngine* d_qe;
+ /** pointer to the proof node manager */
+ ProofNodeManager* d_pnm;
/** cache of term database for quantifiers engine */
TermDb* d_term_db;
/** cache of term util for quantifiers engine */
* of these instantiations, for each quantified formula.
*/
std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
+ /**
+ * A CDProof storing instantiation steps.
+ */
+ std::unique_ptr<CDProof> d_pfInst;
};
} /* CVC4::theory::quantifiers namespace */
return n;
}
-
-Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst)
+{
Node prev = n;
if( options::preSkolemQuant() ){
if( n!=prev ){
Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
+ return TrustNode::mkTrustRewrite(prev, n, nullptr);
}
- return n;
+ return TrustNode::null();
}
}/* CVC4::theory::quantifiers namespace */
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
namespace CVC4 {
namespace theory {
* registered quantified formula. If this flag is true, we do not apply
* certain steps like pre-skolemization since we know they will have no
* effect.
+ *
+ * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
*/
- static Node preprocess( Node n, bool isInst = false );
+ static TrustNode preprocess(Node n, bool isInst = false);
static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false );
QuantifiersEngine::QuantifiersEngine(context::Context* c,
context::UserContext* u,
- TheoryEngine* te)
+ TheoryEngine* te,
+ ProofNodeManager* pnm)
: d_te(te),
d_masterEqualityEngine(nullptr),
d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
d_term_db(new quantifiers::TermDb(c, u, this)),
d_sygus_tdb(nullptr),
d_quant_attr(new quantifiers::QuantAttributes(this)),
- d_instantiate(new quantifiers::Instantiate(this, u)),
+ d_instantiate(new quantifiers::Instantiate(this, u, pnm)),
d_skolemize(new quantifiers::Skolemize(this, u)),
d_term_enum(new quantifiers::TermEnumeration),
d_conflict_c(c, false),
}
}
+bool QuantifiersEngine::addTrustedLemma(TrustNode tlem,
+ bool doCache,
+ bool doRewrite)
+{
+ Node lem = tlem.getProven();
+ if (!addLemma(lem, doCache, doRewrite))
+ {
+ return false;
+ }
+ d_lemmasWaitingPg[lem] = tlem.getGenerator();
+ return true;
+}
+
bool QuantifiersEngine::removeLemma( Node lem ) {
std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
if( it!=d_lemmas_waiting.end() ){
}
void QuantifiersEngine::flushLemmas(){
+ OutputChannel& out = getOutputChannel();
if( !d_lemmas_waiting.empty() ){
//take default output channel if none is provided
d_hasAddedLemma = true;
- for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
- Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
- getOutputChannel().lemma(d_lemmas_waiting[i], LemmaProperty::PREPROCESS);
+ std::map<Node, ProofGenerator*>::iterator itp;
+ for (const Node& lemw : d_lemmas_waiting)
+ {
+ Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
+ itp = d_lemmasWaitingPg.find(lemw);
+ if (itp != d_lemmasWaitingPg.end())
+ {
+ TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);
+ out.trustedLemma(tlemw, LemmaProperty::PREPROCESS);
+ }
+ else
+ {
+ out.lemma(lemw, LemmaProperty::PREPROCESS);
+ }
}
d_lemmas_waiting.clear();
}
if( !d_phase_req_waiting.empty() ){
for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
- getOutputChannel().requirePhase( it->first, it->second );
+ out.requirePhase(it->first, it->second);
}
d_phase_req_waiting.clear();
}
typedef context::CDList<bool> BoolList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-public:
- QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
+ public:
+ QuantifiersEngine(context::Context* c,
+ context::UserContext* u,
+ TheoryEngine* te,
+ ProofNodeManager* pnm);
~QuantifiersEngine();
//---------------------- external interface
/** get theory engine */
void flushLemmas();
public:
- /** add lemma lem */
- bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
- /** remove pending lemma */
- bool removeLemma( Node lem );
- /** add require phase */
- void addRequirePhase( Node lit, bool req );
- /** mark relevant quantified formula, this will indicate it should be checked before the others */
- void markRelevant( Node q );
- /** has added lemma */
- bool hasAddedLemma() const;
- /** theory engine needs check
- *
- * This is true if the theory engine has more constraints to process. When
- * it is false, we are tentatively going to terminate solving with
- * sat/unknown. For details, see TheoryEngine::needCheck.
- */
- bool theoryEngineNeedsCheck() const;
- /** is in conflict */
- bool inConflict() { return d_conflict; }
- /** set conflict */
- void setConflict();
- /** get current q effort */
- QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
- /** get number of waiting lemmas */
- unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
- /** get needs check */
- bool getInstWhenNeedsCheck( Theory::Effort e );
- /** get user pat mode */
- options::UserPatMode getInstUserPatMode();
+ /**
+ * Add lemma to the lemma buffer of this quantifiers engine.
+ * @param lem The lemma to send
+ * @param doCache Whether to cache the lemma (to check for duplicate lemmas)
+ * @param doRewrite Whether to rewrite the lemma
+ * @return true if the lemma was successfully added to the buffer
+ */
+ bool addLemma(Node lem, bool doCache = true, bool doRewrite = true);
+ /**
+ * Add trusted lemma lem, same as above, but where a proof generator may be
+ * provided along with the lemma.
+ */
+ bool addTrustedLemma(TrustNode tlem,
+ bool doCache = true,
+ bool doRewrite = true);
+ /** remove pending lemma */
+ bool removeLemma(Node lem);
+ /** add require phase */
+ void addRequirePhase(Node lit, bool req);
+ /** mark relevant quantified formula, this will indicate it should be checked
+ * before the others */
+ void markRelevant(Node q);
+ /** has added lemma */
+ bool hasAddedLemma() const;
+ /** theory engine needs check
+ *
+ * This is true if the theory engine has more constraints to process. When
+ * it is false, we are tentatively going to terminate solving with
+ * sat/unknown. For details, see TheoryEngine::needCheck.
+ */
+ bool theoryEngineNeedsCheck() const;
+ /** is in conflict */
+ bool inConflict() { return d_conflict; }
+ /** set conflict */
+ void setConflict();
+ /** get current q effort */
+ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
+ /** get number of waiting lemmas */
+ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
+ /** get needs check */
+ bool getInstWhenNeedsCheck(Theory::Effort e);
+ /** get user pat mode */
+ options::UserPatMode getInstUserPatMode();
- public:
- /** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
- /** notification when master equality engine is updated */
- void eqNotifyNewClass(TNode t);
- /** debug print equality engine */
- void debugPrintEqualityEngine( const char * c );
- /** get internal representative
- *
- * Choose a term that is equivalent to a in the current context that is the
- * best term for instantiating the index^th variable of quantified formula q.
- * If no legal term can be found, we return null. This can occur if:
- * - a's type is not a subtype of the type of the index^th variable of q,
- * - a is in an equivalent class with all terms that are restricted not to
- * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
- * guided instantiation.
- */
- Node getInternalRepresentative( Node a, Node q, int index );
+public:
+ /** add term to database */
+ void addTermToDatabase(Node n,
+ bool withinQuant = false,
+ bool withinInstClosure = false);
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
+ /** debug print equality engine */
+ void debugPrintEqualityEngine(const char* c);
+ /** get internal representative
+ *
+ * Choose a term that is equivalent to a in the current context that is the
+ * best term for instantiating the index^th variable of quantified formula q.
+ * If no legal term can be found, we return null. This can occur if:
+ * - a's type is not a subtype of the type of the index^th variable of q,
+ * - a is in an equivalent class with all terms that are restricted not to
+ * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
+ * guided instantiation.
+ */
+ Node getInternalRepresentative(Node a, Node q, int index);
- public:
- //----------user interface for instantiations (see quantifiers/instantiate.h)
- /** print instantiations */
- void printInstantiations(std::ostream& out);
- /** print solution for synthesis conjectures */
- void printSynthSolution(std::ostream& out);
- /** get list of quantified formulas that were instantiated */
- void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
- /** get instantiations */
- void getInstantiations(Node q, std::vector<Node>& insts);
- void getInstantiations(std::map<Node, std::vector<Node> >& insts);
- /** get instantiation term vectors */
- void getInstantiationTermVectors(Node q,
- std::vector<std::vector<Node> >& tvecs);
- void getInstantiationTermVectors(
- std::map<Node, std::vector<std::vector<Node> > >& insts);
- /** get instantiated conjunction */
- Node getInstantiatedConjunction(Node q);
- /** get unsat core lemmas */
- bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
- /** get explanation for instantiation lemmas */
- void getExplanationForInstLemmas(const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec);
+public:
+ //----------user interface for instantiations (see quantifiers/instantiate.h)
+ /** print instantiations */
+ void printInstantiations(std::ostream& out);
+ /** print solution for synthesis conjectures */
+ void printSynthSolution(std::ostream& out);
+ /** get list of quantified formulas that were instantiated */
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+ /** get instantiations */
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ void getInstantiations(std::map<Node, std::vector<Node> >& insts);
+ /** get instantiation term vectors */
+ void getInstantiationTermVectors(Node q,
+ std::vector<std::vector<Node> >& tvecs);
+ void getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /** get instantiated conjunction */
+ Node getInstantiatedConjunction(Node q);
+ /** get unsat core lemmas */
+ bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+ /** get explanation for instantiation lemmas */
+ void getExplanationForInstLemmas(const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec);
- /** get synth solutions
- *
- * 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
- * SynthConjecture::getSynthSolutions.
- */
- bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
+ /** get synth solutions
+ *
+ * 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
+ * SynthConjecture::getSynthSolutions.
+ */
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
- //----------end user interface for instantiations
+ //----------end user interface for instantiations
- /** statistics class */
- class Statistics {
+ /** statistics class */
+ class Statistics
+ {
public:
TimerStat d_time;
TimerStat d_qcf_time;
BoolMap d_lemmas_produced_c;
/** lemmas waiting */
std::vector<Node> d_lemmas_waiting;
+ /** map from waiting lemmas to their proof generators */
+ std::map<Node, ProofGenerator*> d_lemmasWaitingPg;
/** phase requirements waiting */
std::map<Node, bool> d_phase_req_waiting;
/** inst round counters TODO: make context-dependent? */
if (d_logicInfo.isQuantified())
{
// initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+ d_quantEngine =
+ new QuantifiersEngine(d_context, d_userContext, this, d_pnm);
}
// initialize the theory combination manager, which decides and allocates the
// equality engines to use for all theories.
projects / cvc5.git / commitdiff