summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/array_proof_reconstruction.cpp199
-rw-r--r--src/theory/arrays/array_proof_reconstruction.h59
-rw-r--r--src/theory/arrays/theory_arrays.cpp182
-rw-r--r--src/theory/arrays/theory_arrays.h19
4 files changed, 54 insertions, 405 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
deleted file mode 100644
index abc4857e8..000000000
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ /dev/null
@@ -1,199 +0,0 @@
-/********************* */
-/*! \file array_proof_reconstruction.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Guy Katz, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
-
-#include "theory/arrays/array_proof_reconstruction.h"
-
-#include <memory>
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine)
- : d_equalityEngine(equalityEngine) {
-}
-
-void ArrayProofReconstruction::setRowMergeTag(unsigned tag) {
- d_reasonRow = tag;
-}
-
-void ArrayProofReconstruction::setRow1MergeTag(unsigned tag) {
- d_reasonRow1 = tag;
-}
-
-void ArrayProofReconstruction::setExtMergeTag(unsigned tag) {
- d_reasonExt = tag;
-}
-
-void ArrayProofReconstruction::notify(
- unsigned reasonType, Node reason, Node a, Node b,
- std::vector<TNode>& equalities, eq::EqProof* proof) const {
- Debug("pf::array") << "ArrayProofReconstruction::notify( "
- << reason << ", " << a << ", " << b << std::endl;
-
-
- if (reasonType == d_reasonExt) {
- if (proof) {
- // Todo: here we assume that a=b is an assertion. We should probably call
- // explain() recursively, to explain this.
- std::shared_ptr<eq::EqProof> childProof = std::make_shared<eq::EqProof>();
- childProof->d_node = reason;
- proof->d_children.push_back(childProof);
- }
- }
-
- else if (reasonType == d_reasonRow) {
- // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
- // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
- // or ((a[i]:=t)[k] == a[k]) because (i != k).
-
- if (proof) {
- if (a.getKind() == kind::SELECT) {
- // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
-
- // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
- // false in the first case and true in the second case.
- bool currentNodeIsUnchangedArray;
-
- Assert(a.getNumChildren() == 2);
- Assert(b.getNumChildren() == 2);
-
- if (a[0].getKind() == kind::VARIABLE || a[0].getKind() == kind::SKOLEM) {
- currentNodeIsUnchangedArray = true;
- } else if (b[0].getKind() == kind::VARIABLE || b[0].getKind() == kind::SKOLEM) {
- currentNodeIsUnchangedArray = false;
- } else {
- Assert(a[0].getKind() == kind::STORE);
- Assert(b[0].getKind() == kind::STORE);
-
- if (a[0][0] == b[0]) {
- currentNodeIsUnchangedArray = false;
- } else if (b[0][0] == a[0]) {
- currentNodeIsUnchangedArray = true;
- } else {
- Unreachable();
- }
- }
-
- Node indexOne = currentNodeIsUnchangedArray ? a[1] : a[0][1];
- Node indexTwo = currentNodeIsUnchangedArray ? b[0][1] : b[1];
-
- // Some assertions to ensure that the theory of arrays behaves as expected
- Assert(a[1] == b[1]);
- if (currentNodeIsUnchangedArray) {
- Assert(a[0] == b[0][0]);
- } else {
- Assert(a[0][0] == b[0]);
- }
-
- Debug("pf::ee") << "Getting explanation for ROW guard: "
- << indexOne << " != " << indexTwo << std::endl;
-
- std::shared_ptr<eq::EqProof> childProof =
- std::make_shared<eq::EqProof>();
- d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities,
- childProof.get());
-
- // It could be that the guard condition is a constant disequality. In
- // this case, we need to change it to a different format.
- bool haveNegChild = false;
- for (unsigned i = 0; i < childProof->d_children.size(); ++i) {
- if (childProof->d_children[i]->d_node.getKind() == kind::NOT)
- haveNegChild = true;
- }
-
- if ((childProof->d_children.size() != 0) &&
- (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS || !haveNegChild)) {
- // The proof has two children, explaining why each index is a (different) constant.
- Assert(childProof->d_children.size() == 2);
-
- Node constantOne, constantTwo;
- // Each subproof explains why one of the indices is constant.
-
- if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
- constantOne = childProof->d_children[0]->d_node;
- } else {
- Assert(childProof->d_children[0]->d_node.getKind() == kind::EQUAL);
- if ((childProof->d_children[0]->d_node[0] == indexOne) ||
- (childProof->d_children[0]->d_node[0] == indexTwo)) {
- constantOne = childProof->d_children[0]->d_node[1];
- } else {
- constantOne = childProof->d_children[0]->d_node[0];
- }
- }
-
- if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
- constantTwo = childProof->d_children[1]->d_node;
- } else {
- Assert(childProof->d_children[1]->d_node.getKind() == kind::EQUAL);
- if ((childProof->d_children[1]->d_node[0] == indexOne) ||
- (childProof->d_children[1]->d_node[0] == indexTwo)) {
- constantTwo = childProof->d_children[1]->d_node[1];
- } else {
- constantTwo = childProof->d_children[1]->d_node[0];
- }
- }
-
- std::shared_ptr<eq::EqProof> constantDisequalityProof =
- std::make_shared<eq::EqProof>();
- constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
- constantDisequalityProof->d_node =
- NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
-
- // Middle is where we need to insert the new disequality
- std::vector<std::shared_ptr<eq::EqProof>>::iterator middle =
- childProof->d_children.begin();
- ++middle;
-
- childProof->d_children.insert(middle, constantDisequalityProof);
-
- childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
- childProof->d_node =
- NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
- }
-
- proof->d_children.push_back(childProof);
- } else {
- // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]),
-
- Node indexOne = a;
- Node indexTwo = b;
-
- Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl
- << "The reason for the edge is: " << reason << std::endl;
-
- Assert(reason.getNumChildren() == 2);
- Debug("pf::ee") << "Getting explanation for ROW guard: " << reason[1] << std::endl;
-
- std::shared_ptr<eq::EqProof> childProof =
- std::make_shared<eq::EqProof>();
- d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false,
- equalities, childProof.get());
- proof->d_children.push_back(childProof);
- }
- }
-
- }
-
- else if (reasonType == d_reasonRow1) {
- // No special handling required at this time
- }
-}
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
deleted file mode 100644
index a73b5dd08..000000000
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/********************* */
-/*! \file array_proof_reconstruction.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Paul Meng, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Array-specific proof construction logic to be used during the
- ** equality engine's path reconstruction
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
-#define CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
-
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-/**
- * A callback class to be invoked whenever the equality engine traverses
- * an "array-owned" edge during path reconstruction.
- */
-
-class ArrayProofReconstruction : public eq::PathReconstructionNotify {
-public:
- ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
-
- void notify(unsigned reasonType, Node reason, Node a, Node b,
- std::vector<TNode>& equalities,
- eq::EqProof* proof) const override;
-
- void setRowMergeTag(unsigned tag);
- void setRow1MergeTag(unsigned tag);
- void setExtMergeTag(unsigned tag);
-
-private:
- /** Merge tag for ROW applications */
- unsigned d_reasonRow;
- /** Merge tag for ROW1 applications */
- unsigned d_reasonRow1;
- /** Merge tag for EXT applications */
- unsigned d_reasonExt;
-
- const eq::EqualityEngine* d_equalityEngine;
-}; /* class ArrayProofReconstruction */
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3adcd4f49..603dc9639 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,9 +23,6 @@
#include "expr/node_algorithm.h"
#include "options/arrays_options.h"
#include "options/smt_options.h"
-#include "proof/array_proof.h"
-#include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
#include "smt/command.h"
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.h"
@@ -111,7 +108,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
d_readTableContext(new context::Context()),
d_arrayMerges(c),
d_inCheckModel(false),
- d_proofReconstruction(nullptr),
d_dstrat(new TheoryArraysDecisionStrategy(this)),
d_dstratInit(false)
{
@@ -183,22 +179,6 @@ void TheoryArrays::finishInit()
{
d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
}
-
- d_proofReconstruction.reset(new ArrayProofReconstruction(d_equalityEngine));
- d_reasonRow = d_equalityEngine->getFreshMergeReasonType();
- d_reasonRow1 = d_equalityEngine->getFreshMergeReasonType();
- d_reasonExt = d_equalityEngine->getFreshMergeReasonType();
-
- d_proofReconstruction->setRowMergeTag(d_reasonRow);
- d_proofReconstruction->setRow1MergeTag(d_reasonRow1);
- d_proofReconstruction->setExtMergeTag(d_reasonExt);
-
- d_equalityEngine->addPathReconstructionTrigger(d_reasonRow,
- d_proofReconstruction.get());
- d_equalityEngine->addPathReconstructionTrigger(d_reasonRow1,
- d_proofReconstruction.get());
- d_equalityEngine->addPathReconstructionTrigger(d_reasonExt,
- d_proofReconstruction.get());
}
/////////////////////////////////////////////////////////////////////////////
@@ -440,37 +420,6 @@ bool TheoryArrays::propagateLit(TNode literal)
}/* TheoryArrays::propagate(TNode) */
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions,
- eq::EqProof* proof) {
- // Do the work
- bool polarity = literal.getKind() != kind::NOT;
- TNode atom = polarity ? literal : literal[0];
- //eq::EqProof * eqp = new eq::EqProof;
- // eq::EqProof * eqp = NULL;
- if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine->explainEquality(
- atom[0], atom[1], polarity, assumptions, proof);
- } else {
- d_equalityEngine->explainPredicate(atom, polarity, assumptions, proof);
- }
- if (Debug.isOn("pf::array"))
- {
- if (proof)
- {
- Debug("pf::array") << " Proof is : " << std::endl;
- proof->debug_print("pf::array");
- }
-
- Debug("pf::array") << "Array: explain( " << literal << " ):" << std::endl
- << "\t";
- for (unsigned i = 0; i < assumptions.size(); ++i)
- {
- Debug("pf::array") << assumptions[i] << " ";
- }
- Debug("pf::array") << std::endl;
- }
-}
-
TNode TheoryArrays::weakEquivGetRep(TNode node) {
TNode pointer;
while (true) {
@@ -795,7 +744,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
}
// Apply RIntro1 Rule
- d_equalityEngine->assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
+ d_equalityEngine->assertEquality(
+ ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1);
d_infoMap.addStore(node, node);
d_infoMap.addInStore(a, node);
@@ -864,19 +814,32 @@ void TheoryArrays::preRegisterTerm(TNode node)
}
}
-TrustNode TheoryArrays::explain(TNode literal)
+void TheoryArrays::explain(TNode literal, Node& explanation)
{
- Node explanation = explain(literal, NULL);
- return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
-}
-
-Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
++d_numExplain;
Debug("arrays") << spaces(getSatContext()->getLevel())
<< "TheoryArrays::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
- explain(literal, assumptions, proof);
- return mkAnd(assumptions);
+ // Do the work
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ if (atom.getKind() == kind::EQUAL)
+ {
+ d_equalityEngine->explainEquality(
+ atom[0], atom[1], polarity, assumptions, nullptr);
+ }
+ else
+ {
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
+ }
+ explanation = mkAnd(assumptions);
+}
+
+TrustNode TheoryArrays::explain(TNode literal)
+{
+ Node explanation;
+ explain(literal, explanation);
+ return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
}
/////////////////////////////////////////////////////////////////////////////
@@ -1329,49 +1292,20 @@ void TheoryArrays::check(Effort e) {
TNode k;
// k is the skolem for this disequality.
- if (!d_proofsEnabled) {
- Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl;
-
- // If not in replay mode, generate a fresh skolem variable
- k = getSkolem(fact,
- "array_ext_index",
- indexType,
- "an extensional lemma index variable from the theory of arrays",
- false);
-
- // Register this skolem for the proof replay phase
- PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k));
- } else {
- if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) {
- // In the solution pass we didn't need this skolem. Therefore, we don't need it
- // in this reply pass, either.
- break;
- }
-
- // Reuse the same skolem as in the solution pass
- k = ProofManager::getSkolemizationManager()->getSkolem(fact);
- Debug("pf::array") << "Skolem = " << k << std::endl;
- }
-
+ Debug("pf::array")
+ << "Check: kind::NOT: array theory making a skolem"
+ << std::endl;
+ k = getSkolem(
+ fact,
+ "array_ext_index",
+ indexType,
+ "an extensional lemma index variable from the theory of arrays",
+ false);
Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
Node eq = ak.eqNode(bk);
Node lemma = fact[0].orNode(eq.notNode());
- // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered
- // when we output the lemma. However, in replay need the lemma to be propagated, and so we
- // preregister manually.
- if (d_proofsEnabled) {
- if (!d_equalityEngine->hasTerm(ak))
- {
- preRegisterTermInternal(ak);
- }
- if (!d_equalityEngine->hasTerm(bk))
- {
- preRegisterTermInternal(bk);
- }
- }
-
if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
&& d_equalityEngine->hasTerm(bk))
{
@@ -1381,17 +1315,16 @@ void TheoryArrays::check(Effort e) {
<< "\teq = " << eq << std::endl
<< "\treason = " << fact << std::endl;
- d_equalityEngine->assertEquality(eq, false, fact, d_reasonExt);
+ d_equalityEngine->assertEquality(
+ eq, false, fact, theory::eq::MERGED_THROUGH_EXT);
++d_numProp;
}
- if (!d_proofsEnabled) {
- // If this is the solution pass, generate the lemma. Otherwise, don't generate it -
- // as this is the lemma that we're reproving...
- Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
- d_out->lemma(lemma);
- ++d_numExt;
- }
+ // If this is the solution pass, generate the lemma. Otherwise,
+ // don't generate it - as this is the lemma that we're reproving...
+ Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
+ d_out->lemma(lemma);
+ ++d_numExt;
} else {
Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
d_modelConstraints.push_back(fact);
@@ -1480,7 +1413,7 @@ void TheoryArrays::check(Effort e) {
lemma = mkAnd(conjunctions, true);
// LSH FIXME: which kind of arrays lemma is this
Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
- d_out->lemma(lemma, RULE_INVALID, LemmaProperty::SEND_ATOMS);
+ d_out->lemma(lemma, LemmaProperty::SEND_ATOMS);
d_readTableContext->pop();
Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
return;
@@ -1908,7 +1841,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
if (!bjExists) {
preRegisterTermInternal(bj);
}
- d_equalityEngine->assertEquality(aj_eq_bj, true, reason, d_reasonRow);
+ d_equalityEngine->assertEquality(
+ aj_eq_bj, true, reason, theory::eq::MERGED_THROUGH_ROW);
++d_numProp;
return;
}
@@ -1919,7 +1853,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
(aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
Node i_eq_j = i.eqNode(j);
d_permRef.push_back(reason);
- d_equalityEngine->assertEquality(i_eq_j, true, reason, d_reasonRow);
+ d_equalityEngine->assertEquality(
+ i_eq_j, true, reason, theory::eq::MERGED_THROUGH_ROW);
++d_numProp;
return;
}
@@ -1971,19 +1906,18 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
&& !d_equalityEngine->areDisequal(i, j, false))
{
Node i_eq_j;
- if (!d_proofsEnabled) {
- i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
- } else {
- i_eq_j = i.eqNode(j);
- }
-
+ i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
+#if 0
+ i_eq_j = i.eqNode(j);
+#endif
getOutputChannel().requirePhase(i_eq_j, true);
d_decisionRequests.push(i_eq_j);
}
// TODO: maybe add triggers here
- if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) {
+ if (options::arraysEagerLemmas() || bothExist)
+ {
// Make sure that any terms introduced by rewriting are appropriately stored in the equality database
Node aj2 = Rewriter::rewrite(aj);
if (aj != aj2) {
@@ -2162,23 +2096,11 @@ bool TheoryArrays::dischargeLemmas()
void TheoryArrays::conflict(TNode a, TNode b) {
Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
- std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ?
- std::make_shared<eq::EqProof>() : nullptr;
- d_conflictNode = explain(a.eqNode(b), proof.get());
+ explain(a.eqNode(b), d_conflictNode);
if (!d_inCheckModel) {
- std::unique_ptr<ProofArray> proof_array;
-
- if (d_proofsEnabled) {
- proof->debug_print("pf::array");
- proof_array.reset(new ProofArray(proof,
- /*row=*/d_reasonRow,
- /*row1=*/d_reasonRow1,
- /*ext=*/d_reasonExt));
- }
-
- d_out->conflict(d_conflictNode, std::move(proof_array));
+ d_out->conflict(d_conflictNode);
}
d_conflict = true;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 9044b9950..8fdbde0ab 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -26,7 +26,6 @@
#include "context/cdhashset.h"
#include "context/cdqueue.h"
#include "theory/arrays/array_info.h"
-#include "theory/arrays/array_proof_reconstruction.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
@@ -129,15 +128,6 @@ class TheoryArrays : public Theory {
/** conflicts in setModelVal */
IntStat d_numSetModelValConflicts;
- // Merge reason types
-
- /** Merge tag for ROW applications */
- unsigned d_reasonRow;
- /** Merge tag for ROW1 applications */
- unsigned d_reasonRow1;
- /** Merge tag for EXT applications */
- unsigned d_reasonExt;
-
public:
TheoryArrays(context::Context* c,
context::UserContext* u,
@@ -215,9 +205,8 @@ class TheoryArrays : public Theory {
/** Should be called to propagate the literal. */
bool propagateLit(TNode literal);
- /** Explain why this literal is true by adding assumptions */
- void explain(TNode literal, std::vector<TNode>& assumptions,
- eq::EqProof* proof);
+ /** Explain why this literal is true by building an explanation */
+ void explain(TNode literal, Node& exp);
/** For debugging only- checks invariants about when things are preregistered*/
context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
@@ -227,7 +216,6 @@ class TheoryArrays : public Theory {
public:
void preRegisterTerm(TNode n) override;
- Node explain(TNode n, eq::EqProof* proof);
TrustNode explain(TNode n) override;
/////////////////////////////////////////////////////////////////////////////
@@ -446,9 +434,6 @@ class TheoryArrays : public Theory {
bool d_inCheckModel;
int d_topLevel;
- /** An equality-engine callback for proof reconstruction */
- std::unique_ptr<ArrayProofReconstruction> d_proofReconstruction;
-
/**
* The decision strategy for the theory of arrays, which calls the
* getNextDecisionEngineRequest function below.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback