From: Andrew Reynolds Date: Wed, 2 Sep 2020 15:56:53 +0000 (-0500) Subject: (new theory) Update TheoryArrays to the new standard (#5000) X-Git-Tag: cvc5-1.0.0~2919 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d10d1053a0616d8e791219f651b22c10f9039bf;p=cvc5.git (new theory) Update TheoryArrays to the new standard (#5000) This includes using the standard d_conflict flag in TheoryState and splitting its check into 3 callbacks. It also deletes some unused code and eliminates an assertion (line 791 of theory_arrays.cpp) which doesn't hold in a central architecture. Further work on standardization for arrays will add an InferenceManager to guard its uses of asserting facts to equality engine (both for proofs and configurable theory combination). FYI @barrettcw --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2da04ce66..0ad9526a5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -354,8 +354,6 @@ libcvc4_add_sources( theory/arith/type_enumerator.h theory/arrays/array_info.cpp theory/arrays/array_info.h - theory/arrays/static_fact_manager.cpp - theory/arrays/static_fact_manager.h theory/arrays/theory_arrays.cpp theory/arrays/theory_arrays.h theory/arrays/theory_arrays_rewriter.cpp 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 - -#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 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 -#include -#include - -#include "expr/node.h" - -namespace CVC4 { -namespace theory { -namespace arrays { - - class StaticFactManager { - /** Our underlying map type. */ - typedef std::unordered_map 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 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 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 603dc9639..408f4c682 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -43,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; @@ -85,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), @@ -175,10 +173,6 @@ void TheoryArrays::finishInit() { d_equalityEngine->addFunctionKind(kind::STORE); } - if (d_useArrTable) - { - d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN); - } } ///////////////////////////////////////////////////////////////////////////// @@ -401,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; @@ -414,7 +409,7 @@ bool TheoryArrays::propagateLit(TNode literal) } bool ok = d_out->propagate(literal); if (!ok) { - d_conflict = true; + d_state.notifyInConflict(); } return ok; }/* TheoryArrays::propagate(TNode) */ @@ -644,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; @@ -788,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); @@ -802,7 +797,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node) // !d_equalityEngine->consistent()); } - void TheoryArrays::preRegisterTerm(TNode node) { preRegisterTermInternal(node); @@ -863,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; @@ -1061,6 +1038,7 @@ bool TheoryArrays::collectModelValues(TheoryModel* m, NodeManager* nm = NodeManager::currentNM(); // Compute arrays that we need to produce representatives for std::vector arrays; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); for (; !eqcs_i.isFinished(); ++eqcs_i) { Node eqc = (*eqcs_i); @@ -1113,12 +1091,14 @@ bool TheoryArrays::collectModelValues(TheoryModel* m, //} // Loop through all array equivalence classes that need a representative computed - for (size_t i=0; igetRepresentative(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 @@ -1220,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; } @@ -1229,115 +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. - 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()); - - 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, theory::eq::MERGED_THROUGH_EXT); - ++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); - } - } - 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::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end(); TNode a, b, eq; @@ -1424,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; } @@ -1437,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& conjunctions, bool invert, unsigned startIndex) { @@ -1641,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; } @@ -1865,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; @@ -1892,15 +1851,6 @@ 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)) @@ -2025,7 +1975,8 @@ bool TheoryArrays::dischargeLemmas() int prop = options::arraysPropagate(); if (prop > 0) { propagate(l); - if (d_conflict) { + if (d_state.isInConflict()) + { return true; } } @@ -2103,7 +2054,7 @@ void TheoryArrays::conflict(TNode a, TNode b) { d_out->conflict(d_conflictNode); } - d_conflict = true; + d_state.notifyInConflict(); } TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy( diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 8fdbde0ab..dea3d4136 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -240,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) { @@ -252,6 +251,7 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// public: + /** Collect model values in m based on the relevant terms given by termSet */ bool collectModelValues(TheoryModel* m, const std::set& termSet) override; @@ -267,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); @@ -331,9 +341,6 @@ class TheoryArrays : public Theory { /** The notify class for d_equalityEngine */ NotifyClass d_notify; - /** Are we in conflict? */ - context::CDO d_conflict; - /** Conflict when merging constants */ void conflict(TNode a, TNode b); @@ -464,7 +471,6 @@ class TheoryArrays : public Theory { * for the comparison between the indexes that appears in the lemma. */ Node getNextDecisionRequest(); - /** * Compute relevant terms. This includes select nodes for the * RIntro1 and RIntro2 rules.