summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/callbacks.cpp7
-rw-r--r--src/theory/arith/callbacks.h8
-rw-r--r--src/theory/arith/congruence_manager.cpp77
-rw-r--r--src/theory/arith/congruence_manager.h22
-rw-r--r--src/theory/arith/theory_arith_private.cpp13
-rw-r--r--src/theory/arith/theory_arith_private.h7
6 files changed, 92 insertions, 42 deletions
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 0c9cb6c9c..e1cb1c3ca 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -172,11 +172,12 @@ RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
{}
/* If you are not an equality engine, don't use this! */
-void RaiseEqualityEngineConflict::raiseEEConflict(Node n) const{
- d_ta.raiseBlackBoxConflict(n);
+void RaiseEqualityEngineConflict::raiseEEConflict(
+ Node n, std::shared_ptr<ProofNode> pf) const
+{
+ d_ta.raiseBlackBoxConflict(n, pf);
}
-
BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
: d_ta(ta)
{}
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 1ce61f46f..796a93ea4 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -19,6 +19,7 @@
#pragma once
#include "expr/node.h"
+#include "expr/proof_node.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
#include "theory/arith/constraint_forward.h"
@@ -177,8 +178,11 @@ private:
public:
RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
- /* If you are not an equality engine, don't use this! */
- void raiseEEConflict(Node n) const;
+ /* If you are not an equality engine, don't use this!
+ *
+ * The proof should prove that `n` is a conflict.
+ * */
+ void raiseEEConflict(Node n, std::shared_ptr<ProofNode> pf) const;
};
class BoundCountingLookup {
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 404b5bcd0..57214e0f8 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -148,11 +148,13 @@ void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1,
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
}
-void ArithCongruenceManager::raiseConflict(Node conflict){
+void ArithCongruenceManager::raiseConflict(Node conflict,
+ std::shared_ptr<ProofNode> pf)
+{
Assert(!inConflict());
Debug("arith::conflict") << "difference manager conflict " << conflict << std::endl;
d_inConflict.raise();
- d_raiseConflict.raiseEEConflict(conflict);
+ d_raiseConflict.raiseEEConflict(conflict, pf);
}
bool ArithCongruenceManager::inConflict() const{
return d_inConflict.isRaised();
@@ -345,11 +347,22 @@ bool ArithCongruenceManager::propagate(TNode x){
if(rewritten.getConst<bool>()){
return true;
}else{
+ // x rewrites to false.
++(d_statistics.d_conflicts);
-
- Node conf = flattenAnd(explainInternal(x));
- raiseConflict(conf);
+ TrustNode trn = explainInternal(x);
+ Node conf = flattenAnd(trn.getNode());
Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
+ if (isProofEnabled())
+ {
+ auto pf = trn.getGenerator()->getProofFor(trn.getProven());
+ auto confPf = d_pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {conf.negate()});
+ raiseConflict(conf, confPf);
+ }
+ else
+ {
+ raiseConflict(conf);
+ }
return false;
}
}
@@ -371,9 +384,10 @@ bool ArithCongruenceManager::propagate(TNode x){
<< c->negationHasProof() << std::endl;
if(c->negationHasProof()){
- Node expC = explainInternal(x);
+ TrustNode texpC = explainInternal(x);
+ Node expC = texpC.getNode();
ConstraintCP negC = c->getNegation();
- Node neg = negC->externalExplainByAssertions();
+ Node neg = Constraint::externalExplainByAssertions({negC});
Node conf = expC.andNode(neg);
Node final = flattenAnd(conf);
@@ -443,21 +457,15 @@ void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<
}
}
-Node ArithCongruenceManager::explainInternal(TNode internal){
- std::vector<TNode> assumptions;
- explain(internal, assumptions);
-
- std::set<TNode> assumptionSet;
- assumptionSet.insert(assumptions.begin(), assumptions.end());
-
- if (assumptionSet.size() == 1) {
- // All the same, or just one
- return assumptions[0];
- }else{
- NodeBuilder<> conjunction(kind::AND);
- enqueueIntoNB(assumptionSet, conjunction);
- return conjunction;
+TrustNode ArithCongruenceManager::explainInternal(TNode internal)
+{
+ if (isProofEnabled())
+ {
+ return d_pfee->explain(internal);
}
+ // otherwise, explain without proof generator
+ Node exp = d_ee->mkExplainLit(internal);
+ return TrustNode::mkTrustPropExp(internal, exp, nullptr);
}
TrustNode ArithCongruenceManager::explain(TNode external)
@@ -465,15 +473,28 @@ TrustNode ArithCongruenceManager::explain(TNode external)
Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
Node internal = externalToInternal(external);
Trace("arith-ee") << "...internal = " << internal << std::endl;
- Node exp = explainInternal(internal);
- if (isProofEnabled())
+ TrustNode trn = explainInternal(internal);
+ if (isProofEnabled() && trn.getProven()[1] != external)
{
- Node impl = NodeManager::currentNM()->mkNode(Kind::IMPLIES, exp, external);
- // For now, we just trust
- auto pfOfImpl = d_pnm->mkNode(PfRule::INT_TRUST, {}, {impl});
- return d_pfGenExplain->mkTrustNode(impl, pfOfImpl);
+ Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
+ Assert(trn.getProven().getKind() == Kind::IMPLIES);
+ Assert(trn.getGenerator() != nullptr);
+ Trace("arith-ee") << "tweaking proof to prove " << external << " not "
+ << trn.getProven()[1] << std::endl;
+ std::vector<std::shared_ptr<ProofNode>> assumptionPfs;
+ std::vector<Node> assumptions = andComponents(trn.getNode());
+ assumptionPfs.push_back(trn.toProofNode());
+ for (const auto& a : assumptions)
+ {
+ assumptionPfs.push_back(
+ d_pnm->mkNode(PfRule::TRUE_INTRO, {d_pnm->mkAssume(a)}, {}));
+ }
+ auto litPf = d_pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM, {assumptionPfs}, {external});
+ auto extPf = d_pnm->mkScope(litPf, assumptions);
+ return d_pfGenExplain->mkTrustedPropagation(external, trn.getNode(), extPf);
}
- return TrustNode::mkTrustPropExp(external, exp, nullptr);
+ return trn;
}
void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 8b9086eb0..3698f46d8 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -129,8 +129,12 @@ private:
/** Pointer to the proof equality engine of TheoryArith */
theory::eq::ProofEqEngine* d_pfee;
-
- void raiseConflict(Node conflict);
+ /** Raise a conflict node `conflict` to the theory of arithmetic.
+ *
+ * When proofs are enabled, a (closed) proof of the conflict should be
+ * provided.
+ */
+ void raiseConflict(Node conflict, std::shared_ptr<ProofNode> pf = nullptr);
/**
* Are proofs enabled? This is true if a non-null proof manager was provided
* to the constructor of this class.
@@ -195,8 +199,13 @@ private:
void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
- Node explainInternal(TNode internal);
-public:
+ /**
+ * Determine an explaination for `internal`. That is a conjunction of theory
+ * literals which imply `internal`.
+ *
+ * The TrustNode here is a trusted propagation.
+ */
+ TrustNode explainInternal(TNode internal);
public:
ArithCongruenceManager(context::Context* satContext,
@@ -221,7 +230,12 @@ public:
void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee);
//--------------------------------- end initialization
+ /**
+ * Return the trust node for the explanation of literal. The returned
+ * trust node is generated by the proof equality engine of this class.
+ */
TrustNode explain(TNode literal);
+
void explain(TNode lit, NodeBuilder<>& out);
void addWatchedPair(ArithVar s, TNode x, TNode y);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4e4259482..6652d3ee9 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -536,8 +536,17 @@ void TheoryArithPrivate::raiseConflict(ConstraintCP a){
d_conflicts.push_back(a);
}
-void TheoryArithPrivate::raiseBlackBoxConflict(Node bb){
- if(d_blackBoxConflict.get().isNull()){
+void TheoryArithPrivate::raiseBlackBoxConflict(Node bb,
+ std::shared_ptr<ProofNode> pf)
+{
+ Debug("arith::bb") << "raiseBlackBoxConflict: " << bb << std::endl;
+ if (d_blackBoxConflict.get().isNull())
+ {
+ if (options::proofNew())
+ {
+ Debug("arith::bb") << " with proof " << pf << std::endl;
+ d_blackBoxConflictPf.set(pf);
+ }
d_blackBoxConflict = bb;
}
}
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 5cb281b36..012e45b2f 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -17,9 +17,10 @@
#pragma once
+#include <stdint.h>
+
#include <map>
#include <queue>
-#include <stdint.h>
#include <vector>
#include "context/cdhashset.h"
@@ -57,6 +58,7 @@
#include "theory/eager_proof_generator.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
+#include "theory/trust_node.h"
#include "theory/valuation.h"
#include "util/dense_map.h"
#include "util/integer.h"
@@ -329,8 +331,7 @@ private:
// void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
/** This is a conflict that is magically known to hold. */
- void raiseBlackBoxConflict(Node bb);
-
+ void raiseBlackBoxConflict(Node bb, std::shared_ptr<ProofNode> pf = nullptr);
/**
* Returns true iff a conflict has been raised. This method is public since
* it is needed by the ArithState class to know whether we are in conflict.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback