diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 52 |
1 files changed, 32 insertions, 20 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e21b7ef7d..93a920f82 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -20,30 +20,34 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "proof/uf_proof.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/uf/theory_uf_strong_solver.h" using namespace std; -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; + +namespace CVC4 { +namespace theory { +namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo, SmtGlobals* globals, std::string name) + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ d_thss(NULL), - d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true), + d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_functionsTerms(c), - d_symb(u) + d_symb(u, name) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); @@ -204,27 +208,29 @@ Node TheoryUF::getNextDecisionRequest(){ } } -void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { +void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp); + d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); } - //for now, just print debug - //TODO : send the proof outwards : d_out->conflict( lem, eqp ); - if( eqp ){ - eqp->debug_print("uf-pf"); + if( pf ){ + Debug("uf-pf") << std::endl; + pf->debug_print("uf-pf"); } } Node TheoryUF::explain(TNode literal) { + return explain(literal, NULL); +} + +Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; - explain(literal, assumptions); + explain(literal, assumptions, pf); return mkAnd(assumptions); } @@ -508,13 +514,14 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { - //TODO: create EqProof at this level if d_proofEnabled = true + eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b)); + d_conflictNode = explain(a.iffNode(b),pf); } else { - d_conflictNode = explain(a.eqNode(b)); + d_conflictNode = explain(a.eqNode(b),pf); } - d_out->conflict(d_conflictNode); + ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; + d_out->conflict(d_conflictNode, puf); d_conflict = true; } @@ -541,3 +548,8 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_thss->assertDisequal(t1, t2, reason); } } + + +} /* namespace CVC4::theory::uf */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ |