diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 515 |
1 files changed, 165 insertions, 350 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index dcae47dc7..12dbd771d 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,7 +2,7 @@ /*! \file theory_arrays.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: lianah ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -22,17 +22,12 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #include "theory/theory.h" -#include "theory/arrays/union_find.h" -#include "util/congruence_closure.h" #include "theory/arrays/array_info.h" -#include "util/hash.h" -#include "util/ntuple.h" #include "util/stats.h" -#include "util/backtrackable.h" -#include "theory/arrays/static_fact_manager.h" - -#include <iostream> -#include <map> +#include "theory/uf/equality_engine.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdqueue.h" namespace CVC4 { namespace theory { @@ -87,417 +82,237 @@ namespace arrays { * check. Ext lemmas are stored in a cache to prevent instantiating essentially * the same lemma multiple times. */ -class TheoryArrays : public Theory { -private: +static inline std::string spaces(int level) +{ + std::string indentStr(level, ' '); + return indentStr; +} +class TheoryArrays : public Theory { - class CongruenceChannel { - TheoryArrays* d_arrays; + ///////////////////////////////////////////////////////////////////////////// + // MISC + ///////////////////////////////////////////////////////////////////////////// - public: - CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {} - void notifyCongruent(TNode a, TNode b) { - d_arrays->notifyCongruent(a, b); - } - }; /* class CongruenceChannel*/ - friend class CongruenceChannel; + private: - /** - * Output channel connected to the congruence closure module. - */ - CongruenceChannel d_ccChannel; + /** True node for predicates = true */ + Node d_true; - /** - * Instance of the congruence closure module. - */ - CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_1 - (kind::SELECT)> d_cc; + /** True node for predicates = false */ + Node d_false; - /** - * (Temporary) fact manager for preprocessing - eventually handle this with - * something more standard (like congruence closure module) - */ - StaticFactManager d_staticFactManager; + // Statistics - /** - * Cache for proprocessing of atoms. - */ - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - NodeMap d_ppCache; + /** number of Row lemmas */ + IntStat d_numRow; + /** number of Ext lemmas */ + IntStat d_numExt; + /** number of propagations */ + IntStat d_numProp; + /** number of explanations */ + IntStat d_numExplain; + /** calls to non-linear */ + IntStat d_numNonLinear; + /** splits on array variables */ + IntStat d_numSharedArrayVarSplits; + /** time spent in check() */ + TimerStat d_checkTimer; - /** - * Union find for storing the equalities. - */ + public: - UnionFind<Node, NodeHashFunction> d_unionFind; + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); + ~TheoryArrays(); - Backtracker<TNode> d_backtracker; + std::string identify() const { return std::string("TheoryArrays"); } + ///////////////////////////////////////////////////////////////////////////// + // PREPROCESSING + ///////////////////////////////////////////////////////////////////////////// - /** - * Context dependent map from a congruence class canonical representative of - * type array to an Info pointer that keeps track of information useful to axiom - * instantiation - */ + private: - ArrayInfo d_infoMap; + // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used + class PPNotifyClass { + public: + bool notify(TNode propagation) { return true; } + void notify(TNode t1, TNode t2) { } + }; - /** - * Received a notification from the congruence closure algorithm that the two - * nodes a and b have become congruent. - */ + /** The notify class for d_ppEqualityEngine */ + PPNotifyClass d_ppNotify; - void notifyCongruent(TNode a, TNode b); + /** Equaltity engine */ + uf::EqualityEngine<PPNotifyClass> d_ppEqualityEngine; + // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine + context::CDList<Node> d_ppFacts; - typedef context::CDChunkList<TNode> CTNodeListAlloc; - typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap; - typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists; + Node preprocessTerm(TNode term); + Node recursivePreprocessTerm(TNode term); + public: - typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap; - /** - * List of all disequalities this theory has seen. Maintains the invariant that - * if a is in the disequality list of b, then b is in that of a. FIXME? make non context dep map - * */ - CNodeTNodesMap d_disequalities; - EqLists d_equalities; - context::CDList<TNode> d_prop_queue; + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); - void checkPropagations(TNode a, TNode b); + ///////////////////////////////////////////////////////////////////////////// + // T-PROPAGATION / REGISTRATION + ///////////////////////////////////////////////////////////////////////////// - /** List of all atoms the SAT solver knows about and are candidates for - * propagation. */ - __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms; + private: - /** List of disequalities needed to construct explanations for propagated - * row lemmas */ + /** Literals to propagate */ + context::CDList<Node> d_literalsToPropagate; - context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations; + /** Index of the next literal to propagate */ + context::CDO<unsigned> d_literalsToPropagateIndex; - /** - * stores the conflicting disequality (still need to call construct - * conflict to get the actual explanation) - */ - Node d_conflict; + /** Should be called to propagate the literal. */ + bool propagate(TNode literal); - typedef context::CDList< quad<TNode, TNode, TNode, TNode > > QuadCDList; + /** Explain why this literal is true by adding assumptions */ + void explain(TNode literal, std::vector<TNode>& assumptions); + public: - /** - * Ext lemma workslist that stores extensionality lemmas that still need to be added - */ - std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extQueue; + void preRegisterTerm(TNode n); + void propagate(Effort e); + Node explain(TNode n); - /** - * Row Lemma worklist, stores lemmas that can still be added to the SAT solver - * to be emptied during full effort check - */ - std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowQueue; + ///////////////////////////////////////////////////////////////////////////// + // SHARING + ///////////////////////////////////////////////////////////////////////////// - /** - * Extensionality lemma cache which stores the array pair (a,b) for which - * a lemma of the form (a = b OR a[k]!= b[k]) has been added to the SAT solver. - */ - std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extAlreadyAdded; + private: - /** - * Read-over-write lemma cache storing a quadruple (a,b,i,j) for which a - * the lemma (i = j OR a[j] = b[j]) has been added to the SAT solver. Needed - * to prevent infinite recursion in addRowLemma. - */ - std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowAlreadyAdded; + class MayEqualNotifyClass { + public: + bool notify(TNode propagation) { return true; } + void notify(TNode t1, TNode t2) { } + }; - /* - * Congruence helper methods - */ + /** The notify class for d_mayEqualEqualityEngine */ + MayEqualNotifyClass d_mayEqualNotify; - void addDiseq(TNode diseq); - void addEq(TNode eq); + /** Equaltity engine for determining if two arrays might be equal */ + uf::EqualityEngine<MayEqualNotifyClass> d_mayEqualEqualityEngine; - void appendToDiseqList(TNode of, TNode eq); - void appendToEqList(TNode a, TNode b); - Node constructConflict(TNode diseq); + public: - /** - * Merges two congruence classes in the internal union-find and checks for a - * conflict. - */ + void addSharedTerm(TNode t); + EqualityStatus getEqualityStatus(TNode a, TNode b); + void computeCareGraph(); + bool isShared(TNode t) + { return (d_sharedArrays.find(t) != d_sharedArrays.end()); } - void merge(TNode a, TNode b); - inline TNode find(TNode a); - inline TNode debugFind(TNode a) const; - inline void setCanon(TNode a, TNode b); + ///////////////////////////////////////////////////////////////////////////// + // MODEL GENERATION + ///////////////////////////////////////////////////////////////////////////// - void queueRowLemma(TNode a, TNode b, TNode i, TNode j); - inline void queueExtLemma(TNode a, TNode b); + private: + public: - /** - * Adds a Row lemma of the form: - * i = j OR a[j] = b[j] - */ - void addRowLemma(TNode a, TNode b, TNode i, TNode j); + Node getValue(TNode n); - /** - * Adds a new Ext lemma of the form - * a = b OR a[k]!=b[k], for a new variable k - */ - void addExtLemma(TNode a, TNode b); + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// - /** - * Because Row1 axioms of the form (store a i v) [i] = v are not added as - * explicitly but are kept track of internally, is axiom recognizez an axiom - * of the above form given the two terms in the equality. - */ - bool isAxiom(TNode lhs, TNode rhs); + private: + public: + void presolve(); + void shutdown() { } - bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j); - bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j); + ///////////////////////////////////////////////////////////////////////////// + // MAIN SOLVER + ///////////////////////////////////////////////////////////////////////////// + public: + void check(Effort e); - bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) { - //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; - std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin(); - a = find(a); - b = find(b); - i = find(i); - j = find(j); + private: - for( ; it!= d_RowAlreadyAdded.end(); it++) { + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass { + TheoryArrays& d_arrays; + public: + NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {} - TNode a_ = find((*it).first); - TNode b_ = find((*it).second); - TNode i_ = find((*it).third); - TNode j_ = find((*it).fourth); - if( a == a_ && b == b_ && i==i_ && j==j_) { - //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n"; - return true; - } + bool notify(TNode propagation) { + Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to arrays + return d_arrays.propagate(propagation); } - return false; - } - - - bool isNonLinear(TNode n); - - /** - * Checks if any new Row lemmas need to be generated after merging arrays a - * and b; called after setCanon. - */ - void checkRowLemmas(TNode a, TNode b); - - /** - * Called after a new select term a[i] is created to check whether new Row - * lemmas need to be instantiated. - */ - void checkRowForIndex(TNode i, TNode a); - - void checkStore(TNode a); - /** - * Lemma helper functions to prevent changing the list we are iterating through. - */ - void insertInQuadQueue(std::set<quad<TNode, TNode, TNode, TNode> >& queue, TNode a, TNode b, TNode i, TNode j){ - if(i != j) { - queue.insert(make_quad(a,b,i,j)); - } - } - - void dischargeLemmas() { - // we need to swap the temporary lists because adding a lemma calls preregister - // which might modify the d_RowQueue we would be iterating through - std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > temp_Row; - temp_Row.swap(d_RowQueue); - - std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it1 = temp_Row.begin(); - for( ; it1!= temp_Row.end(); it1++) { - if(!isRedundantInContext((*it1).first, (*it1).second, (*it1).third, (*it1).fourth)) { - addRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth); - } - else { - // add it to queue may be needed later - queueRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth); + void notify(TNode t1, TNode t2) { + Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + if (t1.getType().isArray()) { + d_arrays.mergeArrays(t1, t2); + if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { + return; + } } + // Propagate equality between shared terms + Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); + d_arrays.propagate(equality); } + }; - std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> temp_ext; - temp_ext.swap(d_extQueue); - std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin(); - for(; it2 != temp_ext.end(); it2++) { - addExtLemma((*it2).first, (*it2).second); - } - } + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; - /** Checks if instead of adding a lemma of the form i = j OR a[j] = b[j] - * we can propagate either i = j or NOT a[j] = b[j] and does the propagation. - * Returns whether it did propagate. - */ - bool propagateFromRow(TNode a, TNode b, TNode i, TNode j); + /** Equaltity engine */ + uf::EqualityEngine<NotifyClass> d_equalityEngine; - TNode areDisequal(TNode a, TNode b); - - - - /* - * === STATISTICS === - */ + // Are we in conflict? + context::CDO<bool> d_conflict; - /** number of Row lemmas */ - IntStat d_numRow; - /** number of Ext lemmas */ - IntStat d_numExt; - - /** number of propagations */ - IntStat d_numProp; - IntStat d_numExplain; - /** time spent in check() */ - TimerStat d_checkTimer; - - bool d_donePreregister; - - Node preprocessTerm(TNode term); - Node recursivePreprocessTerm(TNode term); - -public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); - ~TheoryArrays(); + /** The conflict node */ + Node d_conflictNode; /** - * Stores in d_infoMap the following information for each term a of type array: - * - * - all i, such that there exists a term a[i] or a = store(b i v) - * (i.e. all indices it is being read atl; store(b i v) is implicitly read at - * position i due to the implicit axiom store(b i v)[i] = v ) - * - * - all the stores a is congruent to (this information is context dependent) - * - * - all store terms of the form store (a i v) (i.e. in which a appears - * directly; this is invariant because no new store terms are created) - * - * Note: completeness depends on having pre-register called on all the input - * terms before starting to instantiate lemmas. + * Context dependent map from a congruence class canonical representative of + * type array to an Info pointer that keeps track of information useful to axiom + * instantiation */ - void preRegisterTerm(TNode n) { - //TimerStat::CodeTimer codeTimer(d_preregisterTimer); - Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n"; - //TODO: check non-linear arrays with an AlwaysAssert!!! - //if(n.getType().isArray()) - - switch(n.getKind()) { - case kind::EQUAL: - // stores the seen atoms for propagation - Trace("arrays-preregister")<<"atom "<<n<<"\n"; - d_atoms.insert(n); - // add to proper equality lists - addEq(n); - break; - case kind::SELECT: - //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n"; - d_infoMap.addIndex(n[0], n[1]); - checkRowForIndex(n[1], find(n[0])); - //Trace("arrays-preregister")<<"n[0] \n"; - //d_infoMap.getInfo(n[0])->print(); - //Trace("arrays-preregister")<<"find(n[0]) \n"; - //d_infoMap.getInfo(find(n[0]))->print(); - break; - - case kind::STORE: - { - // this should always be called at level0 since we do not create new store terms - TNode a = n[0]; - TNode i = n[1]; - TNode v = n[2]; - - NodeManager* nm = NodeManager::currentNM(); - Node ni = nm->mkNode(kind::SELECT, n, i); - Node eq = nm->mkNode(kind::EQUAL, ni, v); - - d_cc.addEquality(eq); - - d_infoMap.addIndex(n, i); - d_infoMap.addStore(n, n); - d_infoMap.addInStore(a, n); - - checkStore(n); - - break; - } - default: - Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; - } - } - //void registerTerm(TNode n) { - // Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n"; - //} + Backtracker<TNode> d_backtracker; + ArrayInfo d_infoMap; - void presolve() { - Trace("arrays")<<"Presolving \n"; - d_donePreregister = true; - } + context::CDQueue<Node> d_mergeQueue; - void addSharedTerm(TNode t); - void notifyEq(TNode lhs, TNode rhs); - void check(Effort e); + bool d_mergeInProgress; - void propagate(Effort e) { + typedef quad<TNode, TNode, TNode, TNode> RowLemmaType; - // Trace("arrays-prop")<<"Propagating \n"; + context::CDQueue<RowLemmaType> d_RowQueue; + context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded; - // context::CDList<TNode>::const_iterator it = d_prop_queue.begin(); - /* - for(; it!= d_prop_queue.end(); it++) { - TNode eq = *it; - if(d_valuation.getSatValue(eq).isNull()) { - //FIXME remove already propagated literals? - d_out->propagate(eq); - ++d_numProp; - } - }*/ - //d_prop_queue.deleteSelf(); - /* - __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator it = d_atoms.begin(); - - for(; it!= d_atoms.end(); it++) { - TNode eq = *it; - Assert(eq.getKind()==kind::EQUAL); - Trace("arrays-prop")<<"value of "<<eq<<" "; - Trace("arrays-prop")<<d_valuation.getSatValue(eq); - if(find(eq[0]) == find(eq[1])) { - Trace("arrays-prop")<<" eq \n"; - ++d_numProp; - } - } - */ + context::CDHashMap<TNode, bool, TNodeHashFunction> d_sharedArrays; + context::CDO<bool> d_sharedTerms; + context::CDList<TNode> d_reads; + std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; - } - Node explain(TNode n); + // List of nodes that need permanent references in this context + context::CDList<Node> d_permRef; - Node getValue(TNode n); - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); - void shutdown() { } - std::string identify() const { return std::string("TheoryArrays"); } + Node mkAnd(std::vector<TNode>& conjunctions); + void setNonLinear(TNode a); + void mergeArrays(TNode a, TNode b); + void checkStore(TNode a); + void checkRowForIndex(TNode i, TNode a); + void checkRowLemmas(TNode a, TNode b); + void queueRowLemma(RowLemmaType lem); + void dischargeLemmas(); };/* class TheoryArrays */ -inline void TheoryArrays::setCanon(TNode a, TNode b) { - d_unionFind.setCanon(a, b); -} - -inline TNode TheoryArrays::find(TNode a) { - return d_unionFind.find(a); -} - -inline TNode TheoryArrays::debugFind(TNode a) const { - return d_unionFind.debugFind(a); -} - }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |