summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.cpp
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2020-09-01 19:08:23 -0300
committerGitHub <noreply@github.com>2020-09-01 19:08:23 -0300
commit8ad308b23c705e73507a42d2425289e999d47f86 (patch)
tree29e3ac78844bc57171e0d122d758a8371a292a93 /src/theory/uf/theory_uf.cpp
parent62ec0666dd4d409ee85603ae94d7ab1a2b4c9dcc (diff)
Removes old proof code (#4964)
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r--src/theory/uf/theory_uf.cpp51
1 files changed, 19 insertions, 32 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f94cc36af..3d90637e2 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -25,9 +25,6 @@
#include "options/smt_options.h"
#include "options/theory_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/cardinality_extension.h"
@@ -288,39 +285,30 @@ bool TheoryUF::propagateLit(TNode literal)
return ok;
}/* TheoryUF::propagate(TNode) */
-void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
+void TheoryUF::explain(TNode literal, Node& exp)
+{
+ Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
+ std::vector<TNode> assumptions;
// Do the work
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
- if (atom.getKind() == kind::EQUAL) {
+ if (atom.getKind() == kind::EQUAL)
+ {
d_equalityEngine->explainEquality(
- atom[0], atom[1], polarity, assumptions, pf);
- } else {
- d_equalityEngine->explainPredicate(atom, polarity, assumptions, pf);
- }
- if( pf ){
- Debug("pf::uf") << std::endl;
- pf->debug_print("pf::uf");
+ atom[0], atom[1], polarity, assumptions, nullptr);
}
-
- Debug("pf::uf") << "UF: explain( " << literal << " ):" << std::endl << "\t";
- for (unsigned i = 0; i < assumptions.size(); ++i) {
- Debug("pf::uf") << assumptions[i] << " ";
+ else
+ {
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
}
- Debug("pf::uf") << std::endl;
+ exp = mkAnd(assumptions);
}
TrustNode TheoryUF::explain(TNode literal)
{
- Node exp = explain(literal, NULL);
- return TrustNode::mkTrustPropExp(literal, exp, nullptr);
-}
-
-Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
- Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
- std::vector<TNode> assumptions;
- explain(literal, assumptions, pf);
- return mkAnd(assumptions);
+ Node explanation;
+ explain(literal, explanation);
+ return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
}
bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
@@ -662,12 +650,11 @@ void TheoryUF::computeCareGraph() {
<< std::endl;
}/* TheoryUF::computeCareGraph() */
-void TheoryUF::conflict(TNode a, TNode b) {
- std::shared_ptr<eq::EqProof> pf =
- d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
- Node conf = explain(a.eqNode(b), pf.get());
- std::unique_ptr<ProofUF> puf(d_proofsEnabled ? new ProofUF(pf) : nullptr);
- d_out->conflict(conf, std::move(puf));
+void TheoryUF::conflict(TNode a, TNode b)
+{
+ Node conf;
+ explain(a.eqNode(b), conf);
+ d_out->conflict(conf);
d_state.notifyInConflict();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback