Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
if (d_theory->getId()==theory::THEORY_UF) {
- th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
+ th = new theory::uf::TheoryUF(&fakeContext,
+ &fakeContext,
+ oc,
+ v,
ProofManager::currentPM()->getLogicInfo(),
+ nullptr,
"replay::");
} else if (d_theory->getId()==theory::THEORY_ARRAYS) {
- th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
- ProofManager::currentPM()->getLogicInfo(),
- "replay::");
+ th = new theory::arrays::TheoryArrays(
+ &fakeContext,
+ &fakeContext,
+ oc,
+ v,
+ ProofManager::currentPM()->getLogicInfo(),
+ nullptr,
+ "replay::");
} else if (d_theory->getId() == theory::THEORY_ARITH) {
Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl;
os << " (clausify_false trust)";
theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
Assert(t != NULL);
- node = t->expandDefinition(n);
+ TrustNode trn = t->expandDefinition(n);
+ node = trn.isNull() ? Node(n) : trn.getNode();
}
// the partial functions can fall through, in which case we still
namespace theory {
namespace arith {
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
- , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
- , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
- , d_proofRecorder(nullptr)
+TheoryArith::TheoryArith(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
+ d_internal(
+ new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)),
+ d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
+ d_proofRecorder(nullptr)
{
smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
// if logic is non-linear
}
}
-Node TheoryArith::expandDefinition(Node node)
+TrustNode TheoryArith::expandDefinition(Node node)
{
- return d_internal->expandDefinition(node);
+ Node expNode = d_internal->expandDefinition(node);
+ return TrustNode::mkTrustRewrite(node, expNode, nullptr);
}
void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_internal->addSharedTerm(n);
}
-Node TheoryArith::ppRewrite(TNode atom) {
+TrustNode TheoryArith::ppRewrite(TNode atom)
+{
CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
- return d_internal->ppRewrite(atom);
+ Node ret = d_internal->ppRewrite(atom);
+ if (ret != atom)
+ {
+ return TrustNode::mkTrustRewrite(atom, ret, nullptr);
+ }
+ return TrustNode::null();
}
Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
return d_internal->needsCheckLastEffort();
}
-Node TheoryArith::explain(TNode n) {
- return d_internal->explain(n);
+TrustNode TheoryArith::explain(TNode n)
+{
+ Node exp = d_internal->explain(n);
+ return TrustNode::mkTrustPropExp(n, exp, nullptr);
}
bool TheoryArith::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
* http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
*/
class TheoryArith : public Theory {
-private:
+ private:
friend class TheoryArithPrivate;
TheoryArithPrivate* d_internal;
*/
proof::ArithProofRecorder * d_proofRecorder;
-public:
- TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo);
+ public:
+ TheoryArith(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
virtual ~TheoryArith();
TheoryRewriter* getTheoryRewriter() override;
void finishInit() override;
- Node expandDefinition(Node node) override;
+ TrustNode expandDefinition(Node node) override;
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
void check(Effort e) override;
bool needsCheckLastEffort() override;
void propagate(Effort e) override;
- Node explain(TNode n) override;
+ TrustNode explain(TNode n) override;
bool getCurrentSubstitution(int effort,
std::vector<Node>& vars,
std::vector<Node>& subs,
void presolve() override;
void notifyRestart() override;
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
- Node ppRewrite(TNode atom) override;
+ TrustNode ppRewrite(TNode atom) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
std::string identify() const override { return std::string("TheoryArith"); }
const EntailmentCheckParameters* params,
EntailmentCheckSideEffects* out) override;
- void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
+ void setProofRecorder(proof::ArithProofRecorder* proofRecorder)
{
d_proofRecorder = proofRecorder;
}
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
+ ProofNodeManager* pnm,
std::string name)
- : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name),
+ : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name),
d_numRow(name + "theory::arrays::number of Row lemmas", 0),
d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
d_numProp(name + "theory::arrays::number of propagations", 0),
return term;
}
-
-Node TheoryArrays::ppRewrite(TNode term) {
- if (!d_preprocess) return term;
+TrustNode TheoryArrays::ppRewrite(TNode term)
+{
+ if (!d_preprocess)
+ {
+ return TrustNode::null();
+ }
d_ppEqualityEngine.addTerm(term);
+ Node ret;
switch (term.getKind()) {
case kind::SELECT: {
// select(store(a,i,v),j) = select(a,j)
// IF i != j
if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) {
- return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
+ ret = NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
}
break;
}
if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) {
Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
- return outer;
+ ret = outer;
}
break;
}
case kind::EQUAL: {
- return solveWrite(term, d_solveWrite, d_solveWrite2, true);
+ ret = solveWrite(term, d_solveWrite, d_solveWrite2, true);
break;
}
default:
break;
}
- return term;
+ if (!ret.isNull() && ret != term)
+ {
+ return TrustNode::mkTrustRewrite(term, ret, nullptr);
+ }
+ return TrustNode::null();
}
// direct propagation now
}
-
-Node TheoryArrays::explain(TNode literal) {
+TrustNode TheoryArrays::explain(TNode literal)
+{
Node explanation = explain(literal, NULL);
- return explanation;
+ return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
}
Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
return std::string("th_arrays_dec");
}
-Node TheoryArrays::expandDefinition(Node node)
+TrustNode TheoryArrays::expandDefinition(Node node)
{
NodeManager* nm = NodeManager::currentNM();
Kind kind = node.getKind();
nm->mkNode(kind::SELECT, a, k),
nm->mkNode(kind::SELECT, b, k));
Node implies = nm->mkNode(kind::IMPLIES, range, eq);
- return nm->mkNode(kind::FORALL, bvl, implies);
+ Node ret = nm->mkNode(kind::FORALL, bvl, implies);
+ return TrustNode::mkTrustRewrite(node, ret, nullptr);
}
- return node;
+ return TrustNode::null();
}
}/* CVC4::theory::arrays namespace */
unsigned d_reasonExt;
public:
-
- TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo,
+ TheoryArrays(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr,
std::string name = "");
~TheoryArrays();
std::string identify() const override { return std::string("TheoryArrays"); }
- Node expandDefinition(Node node) override;
+ TrustNode expandDefinition(Node node) override;
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
public:
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
- Node ppRewrite(TNode atom) override;
+ TrustNode ppRewrite(TNode atom) override;
/////////////////////////////////////////////////////////////////////////////
// T-PROPAGATION / REGISTRATION
void preRegisterTerm(TNode n) override;
void propagate(Effort e) override;
Node explain(TNode n, eq::EqProof* proof);
- Node explain(TNode n) override;
+ TrustNode explain(TNode n) override;
/////////////////////////////////////////////////////////////////////////////
// SHARING
#include <stack>
#include <vector>
+#include "expr/proof_node_manager.h"
#include "smt_util/boolean_simplification.h"
#include "theory/booleans/circuit_propagator.h"
#include "theory/booleans/theory_bool_rewriter.h"
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm)
{
+ ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+ if (pc != nullptr)
+ {
+ // add checkers
+ d_bProofChecker.registerTo(pc);
+ }
}
Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
return Theory::ppAssert(in, outSubstitutions);
}
-/*
-void TheoryBool::check(Effort level) {
- if (done() && !fullEffort(level)) {
- return;
- }
- while (!done())
- {
- // Get all the assertions
- Assertion assertion = get();
- TNode fact = assertion.assertion;
- }
- if( Theory::fullEffort(level) ){
- }
-}
-*/
-
}/* CVC4::theory::booleans namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
#include "context/context.h"
+#include "theory/booleans/proof_checker.h"
#include "theory/booleans/theory_bool_rewriter.h"
#include "theory/theory.h"
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
- //void check(Effort);
-
std::string identify() const override { return std::string("TheoryBool"); }
private:
/** The theory rewriter for this theory. */
TheoryBoolRewriter d_rewriter;
+ /** Proof rule checker */
+ BoolProofRuleChecker d_bProofChecker;
};/* class TheoryBool */
}/* CVC4::theory::booleans namespace */
#include "theory/builtin/theory_builtin.h"
#include "expr/kind.h"
+#include "expr/proof_node_manager.h"
#include "theory/builtin/theory_builtin_rewriter.h"
#include "theory/theory_model.h"
#include "theory/valuation.h"
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo)
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm)
{
+ ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+ if (pc != nullptr)
+ {
+ // add checkers
+ d_bProofChecker.registerTo(pc);
+ }
}
std::string TheoryBuiltin::identify() const
#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#include "theory/builtin/proof_checker.h"
#include "theory/builtin/theory_builtin_rewriter.h"
#include "theory/theory.h"
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
private:
/** The theory rewriter for this theory. */
TheoryBuiltinRewriter d_rewriter;
+ /** Proof rule checker */
+ BuiltinProofRuleChecker d_bProofChecker;
}; /* class TheoryBuiltin */
} // namespace builtin
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
+ ProofNodeManager* pnm,
std::string name)
- : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
+ : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
d_context(c),
d_alreadyPropagatedSet(c),
d_sharedTermsSet(c),
tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
}
-Node TheoryBV::expandDefinition(Node node)
+TrustNode TheoryBV::expandDefinition(Node node)
{
Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
+ Node ret;
switch (node.getKind()) {
case kind::BITVECTOR_SDIV:
case kind::BITVECTOR_SREM:
case kind::BITVECTOR_SMOD:
- return TheoryBVRewriter::eliminateBVSDiv(node);
+ ret = TheoryBVRewriter::eliminateBVSDiv(node);
break;
case kind::BITVECTOR_UDIV:
if (options::bitvectorDivByZeroConst()) {
Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
- return nm->mkNode(kind, node[0], node[1]);
+ ret = nm->mkNode(kind, node[0], node[1]);
+ break;
}
TNode num = node[0], den = node[1];
kind::BITVECTOR_UREM_TOTAL, num, den);
Node divByZero = getBVDivByZero(node.getKind(), width);
Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
- node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
- return node;
+ ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
}
break;
default:
- return node;
break;
}
-
- Unreachable();
+ if (!ret.isNull() && node != ret)
+ {
+ return TrustNode::mkTrustRewrite(node, ret, nullptr);
+ }
+ return TrustNode::null();
}
void TheoryBV::preRegisterTerm(TNode node) {
return PP_ASSERT_STATUS_UNSOLVED;
}
-Node TheoryBV::ppRewrite(TNode t)
+TrustNode TheoryBV::ppRewrite(TNode t)
{
Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
Node res = t;
d_abstractionModule->addInputAtom(res);
}
Debug("bv-pp-rewrite") << "to " << res << "\n";
- return res;
+ if (res != t)
+ {
+ return TrustNode::mkTrustRewrite(t, res, nullptr);
+ }
+ return TrustNode::null();
}
void TheoryBV::presolve() {
d_subtheoryMap[sub]->explain(literal, assumptions);
}
-
-Node TheoryBV::explain(TNode node) {
+TrustNode TheoryBV::explain(TNode node)
+{
Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
std::vector<TNode> assumptions;
// Ask for the explanation
explain(node, assumptions);
// this means that it is something true at level 0
+ Node explanation;
if (assumptions.size() == 0) {
- return utils::mkTrue();
+ explanation = utils::mkTrue();
+ }
+ else
+ {
+ // return the explanation
+ explanation = utils::mkAnd(assumptions);
}
- // return the explanation
- Node explanation = utils::mkAnd(assumptions);
Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
Debug("bitvector::explain") << "TheoryBV::explain done. \n";
- return explanation;
+ return TrustNode::mkTrustPropExp(node, explanation, nullptr);
}
std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
-public:
-
- TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo,
+ public:
+ TheoryBV(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr,
std::string name = "");
~TheoryBV();
void finishInit() override;
- Node expandDefinition(Node node) override;
+ TrustNode expandDefinition(Node node) override;
void preRegisterTerm(TNode n) override;
void propagate(Effort e) override;
- Node explain(TNode n) override;
+ TrustNode explain(TNode n) override;
bool collectModelInfo(TheoryModel* m) override;
bool getCurrentSubstitution(int effort,
std::vector<Node>& vars,
std::vector<Node>& subs,
- std::map<Node, std::vector<Node> >& exp) override;
+ std::map<Node, std::vector<Node>>& exp) override;
int getReduction(int effort, Node n, Node& nr) override;
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void enableCoreTheorySlicer();
- Node ppRewrite(TNode t) override;
+ TrustNode ppRewrite(TNode t) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
void presolve() override;
- bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+ bool applyAbstraction(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions);
void setProofLog(proof::BitVectorProof* bvp);
private:
-
- class Statistics {
- public:
+ class Statistics
+ {
+ public:
AverageStat d_avgConflictSize;
IntStat d_solveSubstitutions;
TimerStat d_solveTimer;
UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm),
d_infer(c),
d_infer_exp(c),
d_term_sk(u),
}
}
-Node TheoryDatatypes::expandDefinition(Node n)
+TrustNode TheoryDatatypes::expandDefinition(Node n)
{
NodeManager* nm = NodeManager::currentNM();
// must ensure the type is well founded and has no nested recursion if
}
}
}
+ Node ret;
switch (n.getKind())
{
case kind::APPLY_SELECTOR:
Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
if (options::dtRewriteErrorSel())
{
- return sel;
+ ret = sel;
}
else
{
Node tester = c.getTester();
Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
tst = Rewriter::rewrite(tst);
- Node n_ret;
if (tst == d_true)
{
- n_ret = sel;
+ ret = sel;
}else{
mkExpDefSkolem(selector, ndt, n.getType());
Node sk =
nm->mkNode(kind::APPLY_UF, d_exp_def_skolem[ndt][selector], n[0]);
if (tst == nm->mkConst(false))
{
- n_ret = sk;
+ ret = sk;
}
else
{
- n_ret = nm->mkNode(kind::ITE, tst, sel, sk);
+ ret = nm->mkNode(kind::ITE, tst, sel, sk);
}
}
- // n_ret = Rewriter::rewrite( n_ret );
- Trace("dt-expand") << "Expand def : " << n << " to " << n_ret
+ Trace("dt-expand") << "Expand def : " << n << " to " << ret
<< std::endl;
- return n_ret;
}
}
break;
<< b[b.getNumChildren() - 1] << std::endl;
}
}
- Node n_ret = b;
- Debug("tuprec") << "return " << n_ret << std::endl;
- return n_ret;
+ ret = b;
+ Debug("tuprec") << "return " << ret << std::endl;
}
break;
- default: return n; break;
+ default: break;
}
- Unreachable();
+ if (!ret.isNull() && n != ret)
+ {
+ return TrustNode::mkTrustRewrite(n, ret, nullptr);
+ }
+ return TrustNode::null();
}
void TheoryDatatypes::presolve()
Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
}
-Node TheoryDatatypes::ppRewrite(TNode in)
+TrustNode TheoryDatatypes::ppRewrite(TNode in)
{
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
nn = rew.size()==0 ? d_true :
( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
}
- return nn;
+ if (in != nn)
+ {
+ return TrustNode::mkTrustRewrite(in, nn, nullptr);
+ }
}
// nothing to do
- return in;
-
+ return TrustNode::null();
}
void TheoryDatatypes::addSharedTerm(TNode t) {
}
}
-Node TheoryDatatypes::explain( TNode literal ){
+TrustNode TheoryDatatypes::explain(TNode literal)
+{
+ Node exp = explainLit(literal);
+ return TrustNode::mkTrustPropExp(literal, exp, nullptr);
+}
+
+Node TheoryDatatypes::explainLit(TNode literal)
+{
std::vector< TNode > assumptions;
explain( literal, assumptions );
return mkAnd( assumptions );
/** Conflict when merging two constants */
void TheoryDatatypes::conflict(TNode a, TNode b){
- d_conflictNode = explain( a.eqNode(b) );
+ Node eq = a.eqNode(b);
+ d_conflictNode = explainLit(eq);
Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
d_conflict = true;
std::vector< Node > rew;
if (utils::checkClash(cons1, cons2, rew))
{
- d_conflictNode = explain( unifEq );
+ d_conflictNode = explainLit(unifEq);
Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
d_conflict = true;
void computeCareGraph() override;
public:
- TheoryDatatypes(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo);
+ TheoryDatatypes(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
~TheoryDatatypes();
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
void explain( TNode literal, std::vector<TNode>& assumptions );
- Node explain(TNode literal) override;
+ TrustNode explain(TNode literal) override;
+ Node explainLit(TNode literal);
Node explain( std::vector< Node >& lits );
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
bool needsCheckLastEffort() override;
void preRegisterTerm(TNode n) override;
void finishInit() override;
- Node expandDefinition(Node n) override;
- Node ppRewrite(TNode n) override;
+ TrustNode expandDefinition(Node n) override;
+ TrustNode ppRewrite(TNode n) override;
void presolve() override;
void addSharedTerm(TNode t) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
} // namespace helper
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context *c,
- context::UserContext *u,
- OutputChannel &out,
+TheoryFp::TheoryFp(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
Valuation valuation,
- const LogicInfo &logicInfo)
- : Theory(THEORY_FP, c, u, out, valuation, logicInfo),
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
d_notification(*this),
d_equalityEngine(d_notification, c, "theory::fp::ee", true),
d_registeredTerms(u),
return uf;
}
-Node TheoryFp::expandDefinition(Node node)
+TrustNode TheoryFp::expandDefinition(Node node)
{
Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
<< std::endl;
if (res != node) {
Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
<< " rewritten to " << res << std::endl;
+ return TrustNode::mkTrustRewrite(node, res, nullptr);
}
-
- return res;
+ return TrustNode::null();
}
-Node TheoryFp::ppRewrite(TNode node)
+TrustNode TheoryFp::ppRewrite(TNode node)
{
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
{
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node
<< " rewritten to " << res << std::endl;
+ return TrustNode::mkTrustRewrite(node, res, nullptr);
}
- return res;
+ return TrustNode::null();
}
bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
d_equalityEngine.setMasterEqualityEngine(eq);
}
-Node TheoryFp::explain(TNode n) {
+TrustNode TheoryFp::explain(TNode n)
+{
Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl;
// All things we assert directly (and not via bit-vector) should
d_equalityEngine.explainPredicate(atom, polarity, assumptions);
}
- return helper::buildConjunct(assumptions);
+ Node exp = helper::buildConjunct(assumptions);
+ return TrustNode::mkTrustPropExp(n, exp, nullptr);
}
Node TheoryFp::getModelValue(TNode var) {
class TheoryFp : public Theory {
public:
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
- TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo);
+ TheoryFp(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
- Node expandDefinition(Node node) override;
+ TrustNode expandDefinition(Node node) override;
void preRegisterTerm(TNode node) override;
void addSharedTerm(TNode node) override;
- Node ppRewrite(TNode node) override;
+ TrustNode ppRewrite(TNode node) override;
void check(Effort) override;
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- Node explain(TNode n) override;
+ TrustNode explain(TNode n) override;
protected:
/** Equality engine */
#include "base/check.h"
#include "expr/kind.h"
+#include "expr/proof_node_manager.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/instantiation_engine.h"
#include "theory/quantifiers/fmf/model_engine.h"
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
+TheoryQuantifiers::TheoryQuantifiers(Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm)
{
out.handleUserAttribute( "fun-def", this );
out.handleUserAttribute( "sygus", this );
out.handleUserAttribute( "quant-inst-max-level", this );
out.handleUserAttribute( "quant-elim", this );
out.handleUserAttribute( "quant-elim-partial", this );
+
+ ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+ if (pc != nullptr)
+ {
+ // add the proof rules
+ d_qChecker.registerTo(pc);
+ }
}
TheoryQuantifiers::~TheoryQuantifiers() {
#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
-#include "context/cdhashmap.h"
#include "context/context.h"
#include "expr/node.h"
#include "theory/output_channel.h"
+#include "theory/quantifiers/proof_checker.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/theory.h"
-#include "theory/theory_engine.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
class TheoryQuantifiers : public Theory {
public:
- TheoryQuantifiers(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo);
+ TheoryQuantifiers(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
~TheoryQuantifiers();
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
private:
/** The theory rewriter for this theory. */
QuantifiersRewriter d_rewriter;
+ /** The proof rule checker */
+ QuantifiersProofRuleChecker d_qChecker;
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
namespace theory {
namespace sep {
-TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
- d_lemmas_produced_c(u),
- d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::sep::ee", true),
- d_conflict(c, false),
- d_reduce(u),
- d_infer(c),
- d_infer_exp(c),
- d_spatial_assertions(c)
+TheorySep::TheorySep(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm),
+ d_lemmas_produced_c(u),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::sep::ee", true),
+ d_conflict(c, false),
+ d_reduce(u),
+ d_infer(c),
+ d_infer_exp(c),
+ d_spatial_assertions(c)
{
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
/////////////////////////////////////////////////////////////////////////////
-
-Node TheorySep::ppRewrite(TNode term) {
- Trace("sep-pp") << "ppRewrite : " << term << std::endl;
- return term;
-}
-
Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
return PP_ASSERT_STATUS_UNSOLVED;
}
-
-Node TheorySep::explain(TNode literal)
+TrustNode TheorySep::explain(TNode literal)
{
Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
explain(literal, assumptions);
- return mkAnd(assumptions);
+ Node exp = mkAnd(assumptions);
+ return TrustNode::mkTrustPropExp(literal, exp, nullptr);
}
void TheorySep::conflict(TNode a, TNode b) {
Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
- Node conflictNode = explain(a.eqNode(b));
+ Node eq = a.eqNode(b);
+ std::vector<TNode> assumptions;
+ explain(eq, assumptions);
+ Node conflictNode = mkAnd(assumptions);
d_conflict = true;
d_out->conflict( conflictNode );
}
bool pol, bool hasPol, bool underSpatial );
public:
- TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheorySep(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm = nullptr);
~TheorySep();
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
public:
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
- Node ppRewrite(TNode atom) override;
void ppNotifyAssertions(const std::vector<Node>& assertions) override;
/////////////////////////////////////////////////////////////////////////////
public:
void propagate(Effort e) override;
- Node explain(TNode n) override;
+ TrustNode explain(TNode n) override;
public:
void addSharedTerm(TNode t) override;
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
d_internal(new TheorySetsPrivate(*this, c, u))
{
// Do not move me to the header.
d_internal->computeCareGraph();
}
-Node TheorySets::explain(TNode node) {
- return d_internal->explain(node);
+TrustNode TheorySets::explain(TNode node)
+{
+ Node exp = d_internal->explain(node);
+ return TrustNode::mkTrustPropExp(node, exp, nullptr);
}
EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
d_internal->preRegisterTerm(node);
}
-Node TheorySets::expandDefinition(Node n)
+TrustNode TheorySets::expandDefinition(Node n)
{
Kind nk = n.getKind();
if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm);
~TheorySets() override;
TheoryRewriter* getTheoryRewriter() override;
void check(Effort) override;
bool collectModelInfo(TheoryModel* m) override;
void computeCareGraph() override;
- Node explain(TNode) override;
+ TrustNode explain(TNode) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
Node getModelValue(TNode) override;
std::string identify() const override { return "THEORY_SETS"; }
void preRegisterTerm(TNode node) override;
- Node expandDefinition(Node n) override;
+ TrustNode expandDefinition(Node n) override;
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void presolve() override;
void propagate(Effort) override;
}
}
-Node TheorySetsPrivate::expandDefinition(Node node)
+TrustNode TheorySetsPrivate::expandDefinition(Node node)
{
Debug("sets-proc") << "expandDefinition : " << node << std::endl;
Node ite = nm->mkNode(kind::ITE, isEmpty, equal, memberAndEqual);
Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable);
Node witness = nm->mkNode(WITNESS, witnessVariables, ite);
- return witness;
+ return TrustNode::mkTrustRewrite(node, witness, nullptr);
}
- return node;
+ return TrustNode::null();
}
Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
* Another option to fix this is to make TheoryModel::getValue more general
* so that it makes theory-specific calls to evaluate interpreted symbols.
*/
- Node expandDefinition(Node n);
-
+ TrustNode expandDefinition(Node n);
+
void presolve();
void propagate(Theory::Effort);
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
d_notify(*this),
d_statistics(),
d_equalityEngine(d_notify, c, "theory::strings::ee", true),
return ok;
}
-
-Node TheoryStrings::explain( TNode literal ){
+TrustNode TheoryStrings::explain(TNode literal)
+{
Debug("strings-explain") << "explain called on " << literal << std::endl;
std::vector< TNode > assumptions;
d_im->explain(literal, assumptions);
+ Node ret;
if( assumptions.empty() ){
- return d_true;
+ ret = d_true;
}else if( assumptions.size()==1 ){
- return assumptions[0];
+ ret = assumptions[0];
}else{
- return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
+ ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
}
+ return TrustNode::mkTrustPropExp(literal, ret, nullptr);
}
bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars,
d_termReg.preRegisterTerm(n);
}
-Node TheoryStrings::expandDefinition(Node node)
+TrustNode TheoryStrings::expandDefinition(Node node)
{
Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
Node k = nm->mkBoundVar(nm->stringType());
Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
Node emp = Word::mkEmptyWord(node.getType());
- node = nm->mkNode(
+ Node ret = nm->mkNode(
WITNESS,
bvl,
nm->mkNode(
ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
+ return TrustNode::mkTrustRewrite(node, ret, nullptr);
}
- return node;
+ return TrustNode::null();
}
void TheoryStrings::check(Effort e) {
{
Debug("strings-conflict") << "Making conflict..." << std::endl;
d_state.setConflict();
- Node conflictNode;
- conflictNode = explain( a.eqNode(b) );
- Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
+ TrustNode conflictNode = explain(a.eqNode(b));
+ Trace("strings-conflict")
+ << "CONFLICT: Eq engine conflict : " << conflictNode.getNode()
+ << std::endl;
++(d_statistics.d_conflictsEqEngine);
- d_out->conflict( conflictNode );
+ d_out->conflict(conflictNode.getNode());
}
}
}
}
-Node TheoryStrings::ppRewrite(TNode atom) {
+TrustNode TheoryStrings::ppRewrite(TNode atom)
+{
Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
- Node atomElim;
+ Node atomRet = atom;
if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
{
// aggressive elimination of regular expression membership
- atomElim = d_regexp_elim.eliminate(atom);
+ Node atomElim = d_regexp_elim.eliminate(atomRet);
if (!atomElim.isNull())
{
Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim
<< " via regular expression elimination."
<< std::endl;
- atom = atomElim;
+ atomRet = atomElim;
}
}
if( !options::stringLazyPreproc() ){
//eager preprocess here
std::vector< Node > new_nodes;
StringsPreprocess* p = d_esolver->getPreprocess();
- Node ret = p->processAssertion(atom, new_nodes);
- if( ret!=atom ){
- Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl;
- for( unsigned i=0; i<new_nodes.size(); i++ ){
- Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl;
+ Node ret = p->processAssertion(atomRet, new_nodes);
+ if (ret != atomRet)
+ {
+ Trace("strings-ppr") << " rewrote " << atomRet << " -> " << ret
+ << ", with " << new_nodes.size() << " lemmas."
+ << std::endl;
+ for (const Node& lem : new_nodes)
+ {
+ Trace("strings-ppr") << " lemma : " << lem << std::endl;
++(d_statistics.d_lemmasEagerPreproc);
- d_out->lemma( new_nodes[i] );
+ d_out->lemma(lem);
}
- return ret;
+ atomRet = ret;
}else{
Assert(new_nodes.empty());
}
}
- return atom;
+ if (atomRet != atom)
+ {
+ return TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
+ }
+ return TrustNode::null();
}
/** run the given inference step */
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
public:
- TheoryStrings(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo);
+ TheoryStrings(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm);
~TheoryStrings();
/** finish initialization */
void finishInit() override;
/** Propagate */
void propagate(Effort e) override;
/** Explain */
- Node explain(TNode literal) override;
+ TrustNode explain(TNode literal) override;
/** Get the equality engine */
eq::EqualityEngine* getEqualityEngine() override;
/** Get current substitution */
/** preregister term */
void preRegisterTerm(TNode n) override;
/** Expand definition */
- Node expandDefinition(Node n) override;
+ TrustNode expandDefinition(Node n) override;
/** Check at effort e */
void check(Effort e) override;
/** needs check last effort */
/** called when a new equivalence class is created */
void eqNotifyNewClass(TNode t);
/** preprocess rewrite */
- Node ppRewrite(TNode atom) override;
+ TrustNode ppRewrite(TNode atom) override;
/**
* Get all relevant information in this theory regarding the current
* model. Return false if a contradiction is discovered.
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
+ ProofNodeManager* pnm,
std::string name)
: d_id(id),
d_instanceName(name),
d_satContext(satContext),
d_userContext(userContext),
d_logicInfo(logicInfo),
+ d_pnm(pnm),
d_facts(satContext),
d_factsHead(satContext, 0),
d_sharedTermsIndex(satContext, 0),
#include "theory/output_channel.h"
#include "theory/theory_id.h"
#include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
namespace CVC4 {
class TheoryEngine;
+class ProofNodeManager;
namespace theory {
/** Information about the logic we're operating within. */
const LogicInfo& d_logicInfo;
+ /** Pointer to proof node manager */
+ ProofNodeManager* d_pnm;
+
/**
* The assertFact() queue.
*
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
+ ProofNodeManager* pnm,
std::string instance = ""); // taking : No default.
/**
virtual void finishInit() { }
/**
+ * Expand definitions in the term node. This returns a term that is
+ * equivalent to node. It wraps this term in a TrustNode of kind
+ * TrustNodeKind::REWRITE. If node is unchanged by this method, the
+ * null TrustNode may be returned. This is an optimization to avoid
+ * constructing the trivial equality (= node node) internally within
+ * TrustNode.
+ *
+ * The purpose of this method is typically to eliminate the operators in node
+ * that are syntax sugar that cannot otherwise be eliminated during rewriting.
+ * For example, division relies on the introduction of an uninterpreted
+ * function for the divide-by-zero case, which we do not introduce with
+ * the rewriter, since this function may be cached in a non-global fashion.
+ *
* Some theories have kinds that are effectively definitions and should be
* expanded before they are handled. Definitions allow a much wider range of
* actions than the normal forms given by the rewriter. However no
* a theory wants to be notified about a term before preprocessing
* and simplification but doesn't necessarily want to rewrite it.
*/
- virtual Node expandDefinition(Node node)
+ virtual TrustNode expandDefinition(Node node)
{
// by default, do nothing
- return node;
+ return TrustNode::null();
}
/**
* Return an explanation for the literal represented by parameter n
* (which was previously propagated by this theory).
*/
- virtual Node explain(TNode n) {
+ virtual TrustNode explain(TNode n)
+ {
Unimplemented() << "Theory " << identify()
<< " propagated a node but doesn't implement the "
"Theory::explain() interface!";
* Given an atom of the theory coming from the input formula, this
* method can be overridden in a theory implementation to rewrite
* the atom into an equivalent form. This is only called just
- * before an input atom to the engine.
+ * before an input atom to the engine. This method returns a TrustNode of
+ * kind TrustNodeKind::REWRITE, which carries information about the proof
+ * generator for the rewrite. Similarly to expandDefinition, this method may
+ * return the null TrustNode if atom is unchanged.
*/
- virtual Node ppRewrite(TNode atom) { return atom; }
+ virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); }
/**
* Notify preprocessed assertions. Called on new assertions after
<< " Responsible theory is: "
<< theoryOf(atom)->getId() << std::endl;
- Node explanation = theoryOf(atom)->explain(node);
+ TrustNode texplanation = theoryOf(atom)->explain(node);
+ Node explanation = texplanation.getNode();
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
PROOF({
if(proofRecipe) {
}
else
{
- explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
+ TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
+ explanation = texp.getNode();
Debug("theory::explain") << "\tTerm was propagated by owner theory: "
<< theoryOf(toExplain.d_theory)->getId()
<< ". Explanation: " << explanation << std::endl;
d_userContext,
*d_theoryOut[theoryId],
theory::Valuation(this),
- d_logicInfo);
+ d_logicInfo,
+ nullptr);
theory::Rewriter::registerTheoryRewriter(
theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
}
unsigned nc = term.getNumChildren();
if (nc == 0)
{
- return d_engine.theoryOf(term)->ppRewrite(term);
+ TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
+ return trn.isNull() ? Node(term) : trn.getNode();
}
Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
}
newTerm = Rewriter::rewrite(Node(newNode));
}
- Node newTerm2 = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
+ TrustNode trn = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
+ Node newTerm2 = trn.isNull() ? newTerm : trn.getNode();
if (newTerm != newTerm2)
{
newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
#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"
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. */
// 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() {
}else{
// support for cardinality constraints is not enabled, set incomplete
d_out->setIncomplete();
- }
+ }
}
//needed for models
if( options::produceModels() ){
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;
{
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) {
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) {
#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"
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();
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;
unsigned depth);
TheoryUfRewriter d_rewriter;
+ /** Proof rule checker */
+ UfProofRuleChecker d_ufProofChecker;
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
context::UserContext* uctxt,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm)
{
}
void registerTerm(TNode) { Unimplemented(); }
void check(Theory::Effort) override { Unimplemented(); }
void propagate(Theory::Effort) override { Unimplemented(); }
- Node explain(TNode) override
+ TrustNode explain(TNode) override
{
Unimplemented();
- return Node::null();
+ return TrustNode::null();
}
Node getValue(TNode n) { return Node::null(); }
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo)
- : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
+ DummyTheory(Context* ctxt,
+ UserContext* uctxt,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(
+ theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, pnm)
{}
TheoryRewriter* getTheoryRewriter() { return nullptr; }
void presolve() override { Unimplemented(); }
void preRegisterTerm(TNode n) override {}
void propagate(Effort level) override {}
- Node explain(TNode n) override { return Node::null(); }
+ TrustNode explain(TNode n) override { return TrustNode::null(); }
Node getValue(TNode n) { return Node::null(); }
string identify() const override { return "DummyTheory"; }
};/* class DummyTheory */
d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
- d_dummy = new DummyTheory(
- d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
+ d_dummy = new DummyTheory(d_ctxt,
+ d_uctxt,
+ d_outputChannel,
+ Valuation(NULL),
+ *d_logicInfo,
+ nullptr);
d_outputChannel.clear();
atom0 = d_nm->mkConst(true);
atom1 = d_nm->mkConst(false);
projects / cvc5.git / commitdiff