diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 199 | ||||
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.h | 59 | ||||
-rw-r--r-- | src/theory/arrays/static_fact_manager.cpp | 170 | ||||
-rw-r--r-- | src/theory/arrays/static_fact_manager.h | 116 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 438 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 47 |
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 */ |