summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp24
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.h22
-rw-r--r--src/theory/quantifiers/instantiate.cpp130
-rw-r--r--src/theory/quantifiers/instantiate.h32
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp7
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h5
-rw-r--r--src/theory/quantifiers_engine.cpp38
-rw-r--r--src/theory/quantifiers_engine.h204
-rw-r--r--src/theory/theory_engine.cpp3
9 files changed, 328 insertions, 137 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index c156cbdf8..a771309f0 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -42,10 +42,10 @@ InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
{
}
-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);
}
@@ -453,11 +453,12 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q)
}
}
}
-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
@@ -470,7 +471,12 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q,
{
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
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index dac5a198c..c767b8a4e 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -43,12 +43,13 @@ class InstRewriterCegqi : public InstantiationRewriter
~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 */
@@ -106,11 +107,14 @@ class InstStrategyCegqi : public QuantifiersModule
* 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;
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 04b6e0dda..abf2ecdbe 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -35,12 +35,16 @@ namespace CVC4 {
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)
{
}
@@ -231,24 +235,101 @@ bool Instantiate::addInstantiation(
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);
@@ -367,7 +448,8 @@ bool Instantiate::existsInstantiation(Node q,
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());
@@ -375,10 +457,34 @@ Node Instantiate::getInstantiation(Node q,
// 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;
}
@@ -675,6 +781,8 @@ void Instantiate::getExplanationForInstLemmas(
#endif
}
+bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
+
void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
{
if (!options::trackInstLemmas())
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 8b1e0f7fc..7e984b116 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -20,6 +20,7 @@
#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"
@@ -53,11 +54,14 @@ class InstantiationRewriter
*
* 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
@@ -84,7 +88,9 @@ class Instantiate : public QuantifiersUtil
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 */
@@ -174,11 +180,16 @@ class Instantiate : public QuantifiersUtil
*
* 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.
@@ -277,6 +288,9 @@ class Instantiate : public QuantifiersUtil
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
@@ -327,6 +341,8 @@ class Instantiate : public QuantifiersUtil
/** 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 */
@@ -359,6 +375,10 @@ class Instantiate : public QuantifiersUtil
* 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 */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0848032f8..e34c1c823 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -2052,8 +2052,8 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
return n;
}
-
-Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst)
+{
Node prev = n;
if( options::preSkolemQuant() ){
@@ -2078,8 +2078,9 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
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 */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index da3bd2212..196e4b108 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -20,6 +20,7 @@
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
namespace CVC4 {
namespace theory {
@@ -284,8 +285,10 @@ public:
* 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 );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2e69080e7..da60561ad 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -174,7 +174,8 @@ class QuantifiersEnginePrivate
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)),
@@ -187,7 +188,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
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),
@@ -1021,6 +1022,19 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
}
}
+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() ){
@@ -1102,19 +1116,31 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode()
}
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();
}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 6afc4f925..bd88034cb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -55,8 +55,11 @@ class QuantifiersEngine {
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 */
@@ -196,100 +199,117 @@ private:
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;
@@ -379,6 +399,8 @@ public:
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? */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6837d4be5..6a548e5b6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -165,7 +165,8 @@ void TheoryEngine::finishInit() {
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback