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/static_fact_manager.cpp170
-rw-r--r--src/theory/arrays/static_fact_manager.h116
-rw-r--r--src/theory/arrays/theory_arrays.cpp438
-rw-r--r--src/theory/arrays/theory_arrays.h47
6 files changed, 168 insertions, 861 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/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
deleted file mode 100644
index d2f4b75c9..000000000
--- a/src/theory/arrays/static_fact_manager.cpp
+++ /dev/null
@@ -1,170 +0,0 @@
-/********************* */
-/*! \file static_fact_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Clark Barrett, Mathias Preiner
- ** 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 Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include <iostream>
-
-#include "base/check.h"
-#include "expr/node.h"
-#include "theory/arrays/static_fact_manager.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-bool StaticFactManager::areEq(TNode a, TNode b) {
- return (find(a) == find(b));
-}
-
-bool StaticFactManager::areDiseq(TNode a, TNode b) {
- Node af = find(a);
- Node bf = find(b);
- Node left, right;
- unsigned i;
- for (i = 0; i < d_diseq.size(); ++i) {
- left = find(d_diseq[i][0]);
- right = find(d_diseq[i][1]);
- if ((left == af && right == bf) ||
- (left == bf && right == af)) {
- return true;
- }
- }
- return false;
-}
-
-void StaticFactManager::addDiseq(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL);
- d_diseq.push_back(eq);
-}
-
-void StaticFactManager::addEq(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL);
- Node a = find(eq[0]);
- Node b = find(eq[1]);
-
- if( a == b) {
- return;
- }
-
- /*
- * take care of the congruence closure part
- */
-
- // make "a" the one with shorter diseqList
- // CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
- // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
-
- // if(deq_ia != d_disequalities.end()) {
- // if(deq_ib == d_disequalities.end() ||
- // (*deq_ia).second->size() > (*deq_ib).second->size()) {
- // TNode tmp = a;
- // a = b;
- // b = tmp;
- // }
- // }
- // a = find(a);
- // b = find(b);
-
-
- // b becomes the canon of a
- setCanon(a, b);
-
- // deq_ia = d_disequalities.find(a);
- // map<TNode, TNode> alreadyDiseqs;
- // if(deq_ia != d_disequalities.end()) {
- // /*
- // * Collecting the disequalities of b, no need to check for conflicts
- // * since the representative of b does not change and we check all the things
- // * in a's class when we look at the diseq list of find(a)
- // */
-
- // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
- // if(deq_ib != d_disequalities.end()) {
- // CTNodeListAlloc* deq = (*deq_ib).second;
- // for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end();
- // j++) {
- // TNode deqn = *j;
- // TNode s = deqn[0];
- // TNode t = deqn[1];
- // TNode sp = find(s);
- // TNode tp = find(t);
- // Assert(sp == b || tp == b);
- // if(sp == b) {
- // alreadyDiseqs[tp] = deqn;
- // } else {
- // alreadyDiseqs[sp] = deqn;
- // }
- // }
- // }
-
- // /*
- // * Looking for conflicts in the a disequality list. Note
- // * that at this point a and b are already merged. Also has
- // * the side effect that it adds them to the list of b (which
- // * became the canonical representative)
- // */
-
- // CTNodeListAlloc* deqa = (*deq_ia).second;
- // for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end();
- // i++) {
- // TNode deqn = (*i);
- // Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() ==
- // kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; TNode sp = find(s);
- // TNode tp = find(t);
-
- // if(find(s) == find(t)) {
- // d_conflict = deqn;
- // return;
- // }
- // Assert( sp == b || tp == b);
-
- // // make sure not to add duplicates
-
- // if(sp == b) {
- // if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
- // appendToDiseqList(b, deqn);
- // alreadyDiseqs[tp] = deqn;
- // }
- // } else {
- // if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
- // appendToDiseqList(b, deqn);
- // alreadyDiseqs[sp] = deqn;
- // }
- // }
-
- // }
- // }
-
- // // TODO: check for equality propagations
- // // a and b are find(a) and find(b) here
- // checkPropagations(a,b);
-
- // if(a.getType().isArray()) {
- // checkRowLemmas(a,b);
- // checkRowLemmas(b,a);
- // // note the change in order, merge info adds the list of
- // // the 2nd argument to the first
- // d_infoMap.mergeInfo(b, a);
- // }
-}
-
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
deleted file mode 100644
index 2df4b0fda..000000000
--- a/src/theory/arrays/static_fact_manager.h
+++ /dev/null
@@ -1,116 +0,0 @@
-/********************* */
-/*! \file static_fact_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Clark Barrett, Mathias Preiner, Morgan Deters
- ** 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 Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-#define CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-
-#include <utility>
-#include <vector>
-#include <unordered_map>
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
- class StaticFactManager {
- /** Our underlying map type. */
- typedef std::unordered_map<Node, Node, NodeHashFunction> MapType;
-
- /**
- * Our map of Nodes to their canonical representatives.
- * If a Node is not present in the map, it is its own
- * representative.
- */
- MapType d_map;
- std::vector<Node> d_diseq;
-
-public:
- StaticFactManager() {}
-
- /**
- * Return a Node's union-find representative, doing path compression.
- */
- inline TNode find(TNode n);
-
- /**
- * Return a Node's union-find representative, NOT doing path compression.
- * This is useful for Assert() statements, debug checking, and similar
- * things that you do NOT want to mutate the structure.
- */
- inline TNode debugFind(TNode n) const;
-
- /**
- * Set the canonical representative of n to newParent. They should BOTH
- * be their own canonical representatives on entry to this funciton.
- */
- inline void setCanon(TNode n, TNode newParent);
-
- bool areEq(TNode a, TNode b);
- bool areDiseq(TNode a, TNode b);
- void addDiseq(TNode eq);
- void addEq(TNode eq);
-
-};/* class StaticFactManager<> */
-
-inline TNode StaticFactManager::debugFind(TNode n) const {
- MapType::const_iterator i = d_map.find(n);
- if(i == d_map.end()) {
- return n;
- } else {
- return debugFind((*i).second);
- }
-}
-
-inline TNode StaticFactManager::find(TNode n) {
- Trace("arraysuf") << "arraysUF find of " << n << std::endl;
- MapType::iterator i = d_map.find(n);
- if(i == d_map.end()) {
- Trace("arraysuf") << "arraysUF it is rep" << std::endl;
- return n;
- } else {
- Trace("arraysuf") << "arraysUF not rep: par is " << (*i).second << std::endl;
- std::pair<TNode, TNode> pr = *i;
- // our iterator is invalidated by the recursive call to find(),
- // since it mutates the map
- TNode p = find(pr.second);
- if(p == pr.second) {
- return p;
- }
- pr.second = p;
- d_map.insert(pr);
- return p;
- }
-}
-
-inline void StaticFactManager::setCanon(TNode n, TNode newParent) {
- Assert(d_map.find(n) == d_map.end());
- Assert(d_map.find(newParent) == d_map.end());
- if(n != newParent) {
- d_map[n] = newParent;
- }
-}
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /*CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b4a234748..408f4c682 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"
@@ -46,7 +43,6 @@ namespace arrays {
// Use static configuration of options for now
const bool d_ccStore = false;
-const bool d_useArrTable = false;
//const bool d_eagerLemmas = false;
const bool d_preprocess = true;
const bool d_solveWrite = true;
@@ -88,7 +84,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
d_isPreRegistered(c),
d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
d_notify(*this),
- d_conflict(c, false),
d_backtracker(c),
d_infoMap(c, &d_backtracker, name),
d_mergeQueue(c),
@@ -111,7 +106,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)
{
@@ -179,26 +173,6 @@ void TheoryArrays::finishInit()
{
d_equalityEngine->addFunctionKind(kind::STORE);
}
- if (d_useArrTable)
- {
- 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());
}
/////////////////////////////////////////////////////////////////////////////
@@ -421,7 +395,8 @@ bool TheoryArrays::propagateLit(TNode literal)
<< std::endl;
// If already in conflict, no more propagation
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
Debug("arrays") << spaces(getSatContext()->getLevel())
<< "TheoryArrays::propagateLit(" << literal
<< "): already in conflict" << std::endl;
@@ -434,43 +409,12 @@ bool TheoryArrays::propagateLit(TNode literal)
}
bool ok = d_out->propagate(literal);
if (!ok) {
- d_conflict = true;
+ d_state.notifyInConflict();
}
return ok;
}/* 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) {
@@ -695,7 +639,8 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
*/
void TheoryArrays::preRegisterTermInternal(TNode node)
{
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
return;
}
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
@@ -795,7 +740,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);
@@ -838,7 +784,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
// The may equal needs the node
d_mayEqualEqualityEngine.addTerm(node);
d_equalityEngine->addTerm(node);
- Assert(d_equalityEngine->getSize(node) == 1);
}
else {
d_equalityEngine->addTerm(node);
@@ -852,7 +797,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
// !d_equalityEngine->consistent());
}
-
void TheoryArrays::preRegisterTerm(TNode node)
{
preRegisterTermInternal(node);
@@ -864,19 +808,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);
}
/////////////////////////////////////////////////////////////////////////////
@@ -900,23 +857,6 @@ void TheoryArrays::notifySharedTerm(TNode t)
}
}
-
-EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
- Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
- if (d_equalityEngine->areEqual(a, b))
- {
- // The terms are implied to be equal
- return EQUALITY_TRUE;
- }
- else if (d_equalityEngine->areDisequal(a, b, false))
- {
- // The terms are implied to be dis-equal
- return EQUALITY_FALSE;
- }
- return EQUALITY_UNKNOWN;//FALSE_IN_MODEL;
-}
-
-
void TheoryArrays::checkPair(TNode r1, TNode r2)
{
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
@@ -1090,22 +1030,15 @@ void TheoryArrays::computeCareGraph()
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-bool TheoryArrays::collectModelInfo(TheoryModel* m)
+bool TheoryArrays::collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet)
{
- // Compute terms appearing in assertions and shared terms, and also
- // include additional reads due to the RIntro1 and RIntro2 rules.
- std::set<Node> termSet;
- computeRelevantTerms(termSet);
-
- // Send the equality engine information to the model
- if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
- {
- return false;
- }
-
+ // termSet contains terms appearing in assertions and shared terms, and also
+ // includes additional reads due to the RIntro1 and RIntro2 rules.
NodeManager* nm = NodeManager::currentNM();
// Compute arrays that we need to produce representatives for
std::vector<Node> arrays;
+
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
for (; !eqcs_i.isFinished(); ++eqcs_i) {
Node eqc = (*eqcs_i);
@@ -1158,12 +1091,14 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
//}
// Loop through all array equivalence classes that need a representative computed
- for (size_t i=0; i<arrays.size(); ++i) {
- TNode n = arrays[i];
- TNode nrep = d_equalityEngine->getRepresentative(n);
+ for (size_t i = 0; i < arrays.size(); ++i)
+ {
+ TNode n = arrays[i];
+ TNode nrep = d_equalityEngine->getRepresentative(n);
- //if (fullModel) {
- // Compute default value for this array - there is one default value for every mayEqual equivalence class
+ // if (fullModel) {
+ // Compute default value for this array - there is one default value for
+ // every mayEqual equivalence class
TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
it = d_defValues.find(mayRep);
// If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
@@ -1265,7 +1200,7 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
Node d = skolem.eqNode(ref);
Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
d_equalityEngine->assertEquality(d, true, d_true);
- Assert(!d_conflict);
+ Assert(!d_state.isInConflict());
d_skolemAssertions.push_back(d);
d_skolemIndex = d_skolemIndex + 1;
}
@@ -1274,145 +1209,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
return skolem;
}
-
-void TheoryArrays::check(Effort e) {
- if (done() && !fullEffort(e)) {
- return;
- }
-
- getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
-
- TimerStat::CodeTimer checkTimer(d_checkTime);
-
- while (!done() && !d_conflict)
+void TheoryArrays::postCheck(Effort level)
+{
+ if ((options::arraysEagerLemmas() || fullEffort(level))
+ && !d_state.isInConflict() && options::arraysWeakEquivalence())
{
- // Get all the assertions
- Assertion assertion = get();
- TNode fact = assertion.d_assertion;
-
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
-
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
-
- if (!assertion.d_isPreregistered)
- {
- if (atom.getKind() == kind::EQUAL) {
- if (!d_equalityEngine->hasTerm(atom[0]))
- {
- Assert(atom[0].isConst());
- d_equalityEngine->addTerm(atom[0]);
- }
- if (!d_equalityEngine->hasTerm(atom[1]))
- {
- Assert(atom[1].isConst());
- d_equalityEngine->addTerm(atom[1]);
- }
- }
- }
-
- // Do the work
- switch (fact.getKind()) {
- case kind::EQUAL:
- d_equalityEngine->assertEquality(fact, true, fact);
- break;
- case kind::SELECT:
- d_equalityEngine->assertPredicate(fact, true, fact);
- break;
- case kind::NOT:
- if (fact[0].getKind() == kind::SELECT) {
- d_equalityEngine->assertPredicate(fact[0], false, fact);
- }
- else if (!d_equalityEngine->areDisequal(fact[0][0], fact[0][1], false))
- {
- // Assert the dis-equality
- d_equalityEngine->assertEquality(fact[0], false, fact);
-
- // Apply ArrDiseq Rule if diseq is between arrays
- if(fact[0][0].getType().isArray() && !d_conflict) {
- if (d_conflict) { Debug("pf::array") << "Entering the skolemization branch" << std::endl; }
-
- NodeManager* nm = NodeManager::currentNM();
- TypeNode indexType = fact[0][0].getType()[0];
-
- 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;
- }
-
- 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))
- {
- // Propagate witness disequality - might produce a conflict
- d_permRef.push_back(lemma);
- Debug("pf::array") << "Asserting to the equality engine:" << std::endl
- << "\teq = " << eq << std::endl
- << "\treason = " << fact << std::endl;
-
- d_equalityEngine->assertEquality(eq, false, fact, d_reasonExt);
- ++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;
- }
- } else {
- Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
- d_modelConstraints.push_back(fact);
- }
- }
- break;
- default:
- Unreachable();
- break;
- }
- }
-
- if ((options::arraysEagerLemmas() || fullEffort(e)) && !d_conflict && options::arraysWeakEquivalence()) {
// Replay all array merges to update weak equivalence data structures
context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
TNode a, b, eq;
@@ -1488,7 +1289,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;
@@ -1499,10 +1300,13 @@ void TheoryArrays::check(Effort e) {
d_readTableContext->pop();
}
- if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) {
+ if (!options::arraysEagerLemmas() && fullEffort(level)
+ && !d_state.isInConflict() && !options::arraysWeakEquivalence())
+ {
// generate the lemmas on the worklist
Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
- while (d_RowQueue.size() > 0 && !d_conflict) {
+ while (d_RowQueue.size() > 0 && !d_state.isInConflict())
+ {
if (dischargeLemmas()) {
break;
}
@@ -1512,6 +1316,84 @@ void TheoryArrays::check(Effort e) {
Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
}
+bool TheoryArrays::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ if (!isPrereg)
+ {
+ if (atom.getKind() == kind::EQUAL)
+ {
+ if (!d_equalityEngine->hasTerm(atom[0]))
+ {
+ Assert(atom[0].isConst());
+ d_equalityEngine->addTerm(atom[0]);
+ }
+ if (!d_equalityEngine->hasTerm(atom[1]))
+ {
+ Assert(atom[1].isConst());
+ d_equalityEngine->addTerm(atom[1]);
+ }
+ }
+ }
+ return false;
+}
+
+void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
+{
+ // if a disequality
+ if (atom.getKind() == kind::EQUAL && !pol)
+ {
+ // Apply ArrDiseq Rule if diseq is between arrays
+ if (fact[0][0].getType().isArray() && !d_state.isInConflict())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode indexType = fact[0][0].getType()[0];
+
+ TNode k;
+ // k is the skolem for this disequality.
+ 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);
+
+ 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());
+
+ if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
+ && d_equalityEngine->hasTerm(bk))
+ {
+ // Propagate witness disequality - might produce a conflict
+ d_permRef.push_back(lemma);
+ Debug("pf::array") << "Asserting to the equality engine:" << std::endl
+ << "\teq = " << eq << std::endl
+ << "\treason = " << fact << std::endl;
+
+ d_equalityEngine->assertEquality(eq, false, fact);
+ ++d_numProp;
+ }
+
+ // 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);
+ }
+ }
+}
Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex)
{
@@ -1716,7 +1598,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
}
// If no more to do, break
- if (d_conflict || d_mergeQueue.empty()) {
+ if (d_state.isInConflict() || d_mergeQueue.empty())
+ {
break;
}
@@ -1916,7 +1799,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;
}
@@ -1927,7 +1811,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;
}
@@ -1938,7 +1823,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
{
Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
- if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
+ if (d_state.isInConflict() || d_RowAlreadyAdded.contains(lem))
+ {
return;
}
TNode a, b, i, j;
@@ -1965,33 +1851,23 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
propagate(lem);
}
- // If equivalent lemma already exists, don't enqueue this one
- if (d_useArrTable) {
- Node tableEntry = NodeManager::currentNM()->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
- if (d_equalityEngine->getSize(tableEntry) != 1)
- {
- return;
- }
- }
-
// Prefer equality between indexes so as not to introduce new read terms
if (options::arraysEagerIndexSplitting() && !bothExist
&& !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) {
@@ -2099,7 +1975,8 @@ bool TheoryArrays::dischargeLemmas()
int prop = options::arraysPropagate();
if (prop > 0) {
propagate(l);
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
return true;
}
}
@@ -2170,26 +2047,14 @@ 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;
+ d_state.notifyInConflict();
}
TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
@@ -2263,13 +2128,8 @@ TrustNode TheoryArrays::expandDefinition(Node node)
return TrustNode::null();
}
-void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet,
- bool includeShared)
+void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet)
{
- // include all standard terms
- std::set<Kind> irrKinds;
- computeRelevantTermsInternal(termSet, irrKinds, includeShared);
-
NodeManager* nm = NodeManager::currentNM();
// make sure RIntro1 reads are included in the relevant set of reads
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 8cbf826c1..dea3d4136 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;
/////////////////////////////////////////////////////////////////////////////
@@ -252,7 +240,6 @@ class TheoryArrays : public Theory {
public:
void notifySharedTerm(TNode t) override;
- EqualityStatus getEqualityStatus(TNode a, TNode b) override;
void computeCareGraph() override;
bool isShared(TNode t)
{
@@ -264,7 +251,9 @@ class TheoryArrays : public Theory {
/////////////////////////////////////////////////////////////////////////////
public:
- bool collectModelInfo(TheoryModel* m) override;
+ /** Collect model values in m based on the relevant terms given by termSet */
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
/////////////////////////////////////////////////////////////////////////////
// NOTIFICATIONS
@@ -278,8 +267,18 @@ class TheoryArrays : public Theory {
// MAIN SOLVER
/////////////////////////////////////////////////////////////////////////////
- public:
- void check(Effort e) override;
+ //--------------------------------- standard check
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Effort level) override;
+ /** Pre-notify fact, return true if processed. */
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+ /** Notify fact */
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+ //--------------------------------- end standard check
private:
TNode weakEquivGetRep(TNode node);
@@ -342,9 +341,6 @@ class TheoryArrays : public Theory {
/** The notify class for d_equalityEngine */
NotifyClass d_notify;
- /** Are we in conflict? */
- context::CDO<bool> d_conflict;
-
/** Conflict when merging constants */
void conflict(TNode a, TNode b);
@@ -445,9 +441,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.
@@ -478,13 +471,11 @@ class TheoryArrays : public Theory {
* for the comparison between the indexes that appears in the lemma.
*/
Node getNextDecisionRequest();
-
/**
- * Compute relevant terms. This includes additional select nodes for the
+ * Compute relevant terms. This includes select nodes for the
* RIntro1 and RIntro2 rules.
*/
- void computeRelevantTerms(std::set<Node>& termSet,
- bool includeShared = true) override;
+ void computeRelevantTerms(std::set<Node>& termSet) override;
};/* class TheoryArrays */
}/* CVC4::theory::arrays namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback