diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 24 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.h | 15 |
2 files changed, 28 insertions, 11 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 8334f29d1..5d47cef4a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -20,6 +20,7 @@ #include <memory> #include "expr/node_algorithm.h" +#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -45,8 +46,9 @@ TheoryUF::TheoryUF(context::Context* c, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + ProofNodeManager* pnm, std::string instanceName) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName), + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ @@ -61,6 +63,12 @@ TheoryUF::TheoryUF(context::Context* c, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo()); + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + d_ufProofChecker.registerTo(pc); + } } TheoryUF::~TheoryUF() { @@ -159,7 +167,7 @@ void TheoryUF::check(Effort level) { }else{ // support for cardinality constraints is not enabled, set incomplete d_out->setIncomplete(); - } + } } //needed for models if( options::produceModels() ){ @@ -201,7 +209,7 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { return node.getKind()==kind::APPLY_UF ? 0 : 1; } -Node TheoryUF::expandDefinition(Node node) +TrustNode TheoryUF::expandDefinition(Node node) { Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : " << node << std::endl; @@ -216,10 +224,10 @@ Node TheoryUF::expandDefinition(Node node) { Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: " << node << " to " << ret << std::endl; - return ret; + return TrustNode::mkTrustRewrite(node, ret, nullptr); } } - return node; + return TrustNode::null(); } void TheoryUF::preRegisterTerm(TNode node) { @@ -304,8 +312,10 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro Debug("pf::uf") << std::endl; } -Node TheoryUF::explain(TNode literal) { - return explain(literal, NULL); +TrustNode TheoryUF::explain(TNode literal) +{ + Node exp = explain(literal, NULL); + return TrustNode::mkTrustPropExp(literal, exp, nullptr); } Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index a3e908b1f..58f4f18a5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -25,6 +25,7 @@ #include "expr/node_trie.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/proof_checker.h" #include "theory/uf/symmetry_breaker.h" #include "theory/uf/theory_uf_rewriter.h" @@ -183,8 +184,12 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, + TheoryUF(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr, std::string instanceName = ""); ~TheoryUF(); @@ -195,9 +200,9 @@ private: void finishInit() override; void check(Effort) override; - Node expandDefinition(Node node) override; + TrustNode expandDefinition(Node node) override; void preRegisterTerm(TNode term) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; bool collectModelInfo(TheoryModel* m) override; @@ -228,6 +233,8 @@ private: unsigned depth); TheoryUfRewriter d_rewriter; + /** Proof rule checker */ + UfProofRuleChecker d_ufProofChecker; };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |