summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r--src/theory/arrays/theory_arrays.h515
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback