From 3f7f9df5f0c419b7f7dd39e32852161f406a441f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 23 May 2011 21:58:12 +0000 Subject: [PATCH] Merge from arrays2 branch. --- src/expr/node.h | 10 + src/smt/smt_engine.cpp | 1 + src/theory/arrays/Makefile.am | 6 +- src/theory/arrays/array_info.cpp | 272 +++++++ src/theory/arrays/array_info.h | 239 ++++++ src/theory/arrays/kinds | 2 +- src/theory/arrays/theory_arrays.cpp | 835 ++++++++++++++++++++- src/theory/arrays/theory_arrays.h | 445 ++++++++++- src/theory/arrays/theory_arrays_rewriter.h | 51 +- src/theory/arrays/union_find.cpp | 59 ++ src/theory/arrays/union_find.h | 146 ++++ src/theory/theory_engine.cpp | 18 +- src/theory/theory_engine.h | 37 +- src/util/Makefile.am | 3 +- src/util/backtrackable.h | 214 ++++++ src/util/ntuple.h | 93 +++ src/util/stats.h | 18 + src/util/triple.h | 43 -- test/Makefile.am | 2 +- test/regress/regress0/Makefile.am | 2 +- test/regress/regress0/arrays/Makefile | 8 + test/regress/regress0/arrays/Makefile.am | 31 + test/regress/regress0/arrays/arrays0.smt2 | 22 + test/regress/regress0/arrays/arrays1.smt2 | 21 + test/regress/regress0/arrays/arrays2.smt2 | 21 + test/regress/regress0/arrays/arrays3.smt2 | 23 + test/regress/regress0/arrays/arrays4.smt2 | 23 + 27 files changed, 2563 insertions(+), 82 deletions(-) create mode 100644 src/theory/arrays/array_info.cpp create mode 100644 src/theory/arrays/array_info.h create mode 100644 src/theory/arrays/union_find.cpp create mode 100644 src/theory/arrays/union_find.h create mode 100644 src/util/backtrackable.h create mode 100644 src/util/ntuple.h delete mode 100644 src/util/triple.h create mode 100644 test/regress/regress0/arrays/Makefile create mode 100644 test/regress/regress0/arrays/Makefile.am create mode 100644 test/regress/regress0/arrays/arrays0.smt2 create mode 100644 test/regress/regress0/arrays/arrays1.smt2 create mode 100644 test/regress/regress0/arrays/arrays2.smt2 create mode 100644 test/regress/regress0/arrays/arrays3.smt2 create mode 100644 test/regress/regress0/arrays/arrays4.smt2 diff --git a/src/expr/node.h b/src/expr/node.h index 9351293f8..372eec8c0 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -27,6 +27,7 @@ #include #include #include +#include #include #include "expr/type.h" @@ -877,6 +878,15 @@ struct TNodeHashFunction { } };/* struct TNodeHashFunction */ +struct TNodePairHashFunction { + size_t operator()(const std::pair& pair ) const { + TNode n1 = pair.first; + TNode n2 = pair.second; + + return (size_t) (n1.getId() * 0x9e3779b9 + n2.getId()); + } +};/* struct TNodePairHashFunction */ + template inline size_t NodeTemplate::getNumChildren() const { assertTNodeNotExpired(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e99c20254..b8f8a522f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -253,6 +253,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { throw ModalException("logic already set"); } d_logic = s; + d_theoryEngine->d_logic = s; } void SmtEngine::setInfo(const std::string& key, const SExpr& value) diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 578915d69..1e070cdaf 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -9,6 +9,10 @@ libarrays_la_SOURCES = \ theory_arrays_type_rules.h \ theory_arrays_rewriter.h \ theory_arrays.h \ - theory_arrays.cpp + theory_arrays.cpp \ + union_find.h \ + union_find.cpp \ + array_info.h \ + array_info.cpp EXTRA_DIST = kinds diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp new file mode 100644 index 000000000..c795de0b9 --- /dev/null +++ b/src/theory/arrays/array_info.cpp @@ -0,0 +1,272 @@ +/********************* */ +/*! \file array_info.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains additional classes to store context dependent information + ** for each term of type array + ** + ** + **/ + +#include "array_info.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +bool inList(const CTNodeList* l, const TNode el) { + CTNodeList::const_iterator it = l->begin(); + for ( ; it!= l->end(); it ++) { + if(*it == el) + return true; + } + return false; +} + +void printList (CTNodeList* list) { + CTNodeList::const_iterator it = list->begin(); + Debug("arrays-info")<<" [ "; + for(; it != list->end(); it++ ) { + Debug("arrays-info")<<(*it)<<" "; + } + Debug("arrays-info")<<"] \n"; +} + +void printList (List* list) { + List::const_iterator it = list->begin(); + Debug("arrays-info")<<" [ "; + for(; it != list->end(); it++ ) { + Debug("arrays-info")<<(*it)<<" "; + } + Debug("arrays-info")<<"] \n"; +} + +void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ + std::set temp; + CTNodeList::const_iterator it; + for(it = la->begin() ; it != la->end(); it++ ) { + temp.insert((*it)); + } + + for(it = lb->begin() ; it!= lb->end(); it++ ) { + if(temp.count(*it) == 0) { + la->push_back(*it); + } + } +} + +void ArrayInfo::addIndex(const Node a, const TNode i) { + Assert(a.getType().isArray()); + Assert(!i.getType().isArray()); // temporary for flat arrays + Debug("arrays-ind")<<"Arrays::addIndex "<* temp_indices; + Info* temp_info; + + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_indices = new List(bck); + temp_indices->append(i); + + temp_info = new Info(ct, bck); + temp_info->indices = temp_indices; + + info_map[a] = temp_info; + } else { + temp_indices = (*it).second->indices; + temp_indices->append(i); + } + if(Debug.isOn("arrays-ind")) { + printList((*(info_map.find(a))).second->indices); + } + +} + +void ArrayInfo::addStore(const Node a, const TNode st){ + Assert(a.getType().isArray()); + Assert(st.getKind()== kind::STORE); // temporary for flat arrays + + CTNodeList* temp_store; + Info* temp_info; + + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_store = new(true) CTNodeList(ct); + temp_store->push_back(st); + + temp_info = new Info(ct, bck); + temp_info->stores = temp_store; + info_map[a]=temp_info; + } else { + temp_store = (*it).second->stores; + if(! inList(temp_store, st)) { + temp_store->push_back(st); + } + } +}; + + +void ArrayInfo::addInStore(const TNode a, const TNode b){ + Debug("arrays-addinstore")<<"Arrays::addInStore "<push_back(b); + + temp_info = new Info(ct, bck); + temp_info->in_stores = temp_inst; + info_map[a] = temp_info; + } else { + temp_inst = (*it).second->in_stores; + if(! inList(temp_inst, b)) { + temp_inst->push_back(b); + } + } +}; + + + +/** + * Returns the information associated with TNode a + */ + +const Info* ArrayInfo::getInfo(const TNode a) const{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) + return (*it).second; + return emptyInfo; +} + +List* ArrayInfo::getIndices(const TNode a) const{ + CNodeInfoMap::const_iterator it = info_map.find(a); + if(it!= info_map.end()) { + return (*it).second->indices; + } + return emptyListI; +} + +const CTNodeList* ArrayInfo::getStores(const TNode a) const{ + CNodeInfoMap::const_iterator it = info_map.find(a); + if(it!= info_map.end()) { + return (*it).second->stores; + } + return emptyList; +} + +const CTNodeList* ArrayInfo::getInStores(const TNode a) const{ + CNodeInfoMap::const_iterator it = info_map.find(a); + if(it!= info_map.end()) { + return (*it).second->in_stores; + } + return emptyList; +} + + +void ArrayInfo::mergeInfo(const TNode a, const TNode b){ + // can't have assertion that find(b) = a ! + TimerStat::CodeTimer codeTimer(d_mergeInfoTimer); + ++d_callsMergeInfo; + + Debug("arrays-mergei")<<"Arrays::mergeInfo merging "<print(); + + if(itb != info_map.end()) { + Debug("arrays-mergei")<<"Arrays::mergeInfo info "<print(); + + List* lista_i = (*ita).second->indices; + CTNodeList* lista_st = (*ita).second->stores; + CTNodeList* lista_inst = (*ita).second->in_stores; + + + List* listb_i = (*itb).second->indices; + CTNodeList* listb_st = (*itb).second->stores; + CTNodeList* listb_inst = (*itb).second->in_stores; + + lista_i->concat(listb_i); + mergeLists(lista_st, listb_st); + mergeLists(lista_inst, listb_inst); + + /* sketchy stats */ + + //FIXME + int s = 0;//lista_i->size(); + d_maxList.maxAssign(s); + + + if(s!= 0) { + d_avgIndexListLength.addEntry(s); + ++d_listsCount; + } + s = lista_st->size(); + d_maxList.maxAssign(s); + if(s!= 0) { + d_avgStoresListLength.addEntry(s); + ++d_listsCount; + } + + s = lista_inst->size(); + d_maxList.maxAssign(s); + if(s!=0) { + d_avgInStoresListLength.addEntry(s); + ++d_listsCount; + } + + /* end sketchy stats */ + + } + + } else { + Debug("arrays-mergei")<<" First element has no info \n"; + if(itb != info_map.end()) { + Debug("arrays-mergei")<<" adding second element's info \n"; + (*itb).second->print(); + + List* listb_i = (*itb).second->indices; + CTNodeList* listb_st = (*itb).second->stores; + CTNodeList* listb_inst = (*itb).second->in_stores; + + Info* temp_info = new Info(ct, bck); + + (temp_info->indices)->concat(listb_i); + mergeLists(temp_info->stores, listb_st); + mergeLists(temp_info->in_stores, listb_inst); + info_map[a] = temp_info; + + } else { + Debug("arrays-mergei")<<" Second element has no info \n"; + } + + } + Debug("arrays-mergei")<<"Arrays::mergeInfo done \n"; + +} + + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h new file mode 100644 index 000000000..6eb20e30a --- /dev/null +++ b/src/theory/arrays/array_info.h @@ -0,0 +1,239 @@ +/*! \file array_info.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains additional classes to store context dependent information + ** for each term of type array + ** + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H +#define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H +#include "util/backtrackable.h" +#include "context/cdlist.h" +#include "context/cdmap.h" +#include "expr/node.h" +#include "util/stats.h" +#include "util/ntuple.h" +#include +#include +#include +#include + +namespace CVC4 { +namespace theory { +namespace arrays { + +typedef context::CDList CTNodeList; + +struct TNodeQuadHashFunction { + size_t operator()(const quad& q ) const { + TNode n1 = q.first; + TNode n2 = q.second; + TNode n3 = q.third; + TNode n4 = q.fourth; + return (size_t) (n1.getId()*0x9e3779b9 + n2.getId()*0x30000059 + + n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF); + + } +};/* struct TNodeQuadHashFunction */ + +void printList (CTNodeList* list); +void printList( List* list); + +bool inList(const CTNodeList* l, const TNode el); + +/** + * Small class encapsulating the information + * in the map. It's a class and not a struct to + * call the destructor. + */ + +class Info { +public: + List* indices; + CTNodeList* stores; + CTNodeList* in_stores; + + Info(context::Context* c, Backtracker* bck) { + indices = new List(bck); + stores = new(true)CTNodeList(c); + in_stores = new(true)CTNodeList(c); + + } + + ~Info() { + //FIXME! + //indices->deleteSelf(); + stores->deleteSelf(); + in_stores->deleteSelf(); + } + + /** + * prints the information + */ + void print() const { + Assert(indices != NULL && stores!= NULL); // && equals != NULL); + Debug("arrays-info")<<" indices "; + printList(indices); + Debug("arrays-info")<<" stores "; + printList(stores); + Debug("arrays-info")<<" in_stores "; + printList(in_stores); + } +}; + + +typedef __gnu_cxx::hash_map CNodeInfoMap; + +/** + * Class keeping track of the following information for canonical + * representatives of type array [a] : + * indices at which it is being read (all i for which there is a + * term of the form SELECT a i) + * all store terms in the congruence class + * stores in which it appears (terms of the form STORE a _ _ ) + * + */ +class ArrayInfo { +private: + context::Context* ct; + Backtracker* bck; + CNodeInfoMap info_map; + + CTNodeList* emptyList; + List* emptyListI; + + + /* == STATISTICS == */ + + /** time spent in preregisterTerm() */ + TimerStat d_mergeInfoTimer; + AverageStat d_avgIndexListLength; + AverageStat d_avgStoresListLength; + AverageStat d_avgInStoresListLength; + IntStat d_listsCount; + IntStat d_callsMergeInfo; + IntStat d_maxList; + SizeStat d_tableSize; + + /** + * checks if a certain element is in the list l + * FIXME: better way to check for duplicates? + */ + + /** + * helper method that merges two lists into the first + * without adding duplicates + */ + void mergeLists(CTNodeList* la, const CTNodeList* lb) const; + +public: + const Info* emptyInfo; +/* + ArrayInfo(): ct(NULl), info + d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), + d_avgIndexListLength("theory::arrays::avgIndexListLength"), + d_avgStoresListLength("theory::arrays::avgStoresListLength"), + d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), + d_listsCount("theory::arrays::listsCount",0), + d_callsMergeInfo("theory::arrays::callsMergeInfo",0), + d_maxList("theory::arrays::maxList",0), + d_tableSize("theory::arrays::infoTableSize", info_map) { + StatisticsRegistry::registerStat(&d_mergeInfoTimer); + StatisticsRegistry::registerStat(&d_avgIndexListLength); + StatisticsRegistry::registerStat(&d_avgStoresListLength); + StatisticsRegistry::registerStat(&d_avgInStoresListLength); + StatisticsRegistry::registerStat(&d_listsCount); + StatisticsRegistry::registerStat(&d_callsMergeInfo); + StatisticsRegistry::registerStat(&d_maxList); + StatisticsRegistry::registerStat(&d_tableSize); + }*/ + ArrayInfo(context::Context* c, Backtracker* b): ct(c), bck(b), info_map(), + d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), + d_avgIndexListLength("theory::arrays::avgIndexListLength"), + d_avgStoresListLength("theory::arrays::avgStoresListLength"), + d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), + d_listsCount("theory::arrays::listsCount",0), + d_callsMergeInfo("theory::arrays::callsMergeInfo",0), + d_maxList("theory::arrays::maxList",0), + d_tableSize("theory::arrays::infoTableSize", info_map) { + emptyList = new(true) CTNodeList(ct); + emptyListI = new List(bck); + emptyInfo = new Info(ct, bck); + StatisticsRegistry::registerStat(&d_mergeInfoTimer); + StatisticsRegistry::registerStat(&d_avgIndexListLength); + StatisticsRegistry::registerStat(&d_avgStoresListLength); + StatisticsRegistry::registerStat(&d_avgInStoresListLength); + StatisticsRegistry::registerStat(&d_listsCount); + StatisticsRegistry::registerStat(&d_callsMergeInfo); + StatisticsRegistry::registerStat(&d_maxList); + StatisticsRegistry::registerStat(&d_tableSize); + } + + ~ArrayInfo(){ + CNodeInfoMap::iterator it = info_map.begin(); + for( ; it != info_map.end(); it++ ) { + if((*it).second!= emptyInfo) { + delete (*it).second; + } + } + emptyList->deleteSelf(); + delete emptyInfo; + StatisticsRegistry::unregisterStat(&d_mergeInfoTimer); + StatisticsRegistry::unregisterStat(&d_avgIndexListLength); + StatisticsRegistry::unregisterStat(&d_avgStoresListLength); + StatisticsRegistry::unregisterStat(&d_avgInStoresListLength); + StatisticsRegistry::unregisterStat(&d_listsCount); + StatisticsRegistry::unregisterStat(&d_callsMergeInfo); + StatisticsRegistry::unregisterStat(&d_maxList); + StatisticsRegistry::unregisterStat(&d_tableSize); + }; + + /** + * adds the node a to the map if it does not exist + * and it initializes the info. checks for duplicate i's + */ + void addIndex(const Node a, const TNode i); + void addStore(const Node a, const TNode st); + void addInStore(const TNode a, const TNode st); + + + /** + * Returns the information associated with TNode a + */ + + const Info* getInfo(const TNode a) const; + + List* getIndices(const TNode a) const; + + const CTNodeList* getStores(const TNode a) const; + + const CTNodeList* getInStores(const TNode a) const; + + /** + * merges the information of nodes a and b + * the nodes do not have to actually be in the map. + * pre-condition + * a should be the canonical representative of b + */ + void mergeInfo(const TNode a, const TNode b); +}; + + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARRAYS__ARRAY_INFO_H */ diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 4c68fb5cb..30242db30 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -7,7 +7,7 @@ theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" properties polite stable-infinite -properties check +properties check propagate presolve rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8b625613a..37c49b341 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -20,7 +20,7 @@ #include "theory/arrays/theory_arrays.h" #include "theory/valuation.h" #include "expr/kind.h" - +#include using namespace std; using namespace CVC4; @@ -31,33 +31,140 @@ using namespace CVC4::theory::arrays; TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_ARRAY, c, out, valuation) + Theory(THEORY_ARRAY, c, out, valuation), + d_ccChannel(this), + d_cc(c, &d_ccChannel), + d_unionFind(c), + d_backtracker(c), + d_infoMap(c,&d_backtracker), + d_disequalities(c), + d_equalities(c), + d_prop_queue(c), + d_atoms(), + d_explanations(c), + d_conflict(), + d_numRow("theory::arrays::number of Row lemmas", 0), + d_numExt("theory::arrays::number of Ext lemmas", 0), + d_numProp("theory::arrays::number of propagations", 0), + d_numExplain("theory::arrays::number of explanations", 0), + d_checkTimer("theory::arrays::checkTime"), + d_donePreregister(false) { + //d_backtracker = new Backtracker(c); + //d_infoMap = ArrayInfo(c, d_backtracker); + + StatisticsRegistry::registerStat(&d_numRow); + StatisticsRegistry::registerStat(&d_numExt); + StatisticsRegistry::registerStat(&d_numProp); + StatisticsRegistry::registerStat(&d_numExplain); + StatisticsRegistry::registerStat(&d_checkTimer); + + } TheoryArrays::~TheoryArrays() { + + StatisticsRegistry::unregisterStat(&d_numRow); + StatisticsRegistry::unregisterStat(&d_numExt); + StatisticsRegistry::unregisterStat(&d_numProp); + StatisticsRegistry::unregisterStat(&d_numExplain); + StatisticsRegistry::unregisterStat(&d_checkTimer); + } void TheoryArrays::addSharedTerm(TNode t) { - Debug("arrays") << "TheoryArrays::addSharedTerm(): " + Debug("arrays") << "Arrays::addSharedTerm(): " << t << endl; } void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { - Debug("arrays") << "TheoryArrays::notifyEq(): " - << lhs << " = " << rhs << endl; +} + +void TheoryArrays::notifyCongruent(TNode a, TNode b) { + Debug("arrays") << "Arrays::notifyCongruent(): " + << a << " = " << b << endl; + if(!d_conflict.isNull()) { + return; + } + merge(a,b); } void TheoryArrays::check(Effort e) { + TimerStat::CodeTimer codeTimer(d_checkTimer); + + if(!d_donePreregister ) { + // only start looking for lemmas after preregister on all input terms + // has been called + return; + } + + Debug("arrays") <<"Arrays::start check "; while(!done()) { Node assertion = get(); - Debug("arrays") << "TheoryArrays::check(): " << assertion << endl; + Debug("arrays") << "Arrays::check(): " << assertion << endl; + + switch(assertion.getKind()) { + case kind::EQUAL: + case kind::IFF: + d_cc.addEquality(assertion); + if(!d_conflict.isNull()) { + // addEquality can cause a notify congruent which calls merge + // which can lead to a conflict + Node conflict = constructConflict(d_conflict); + d_conflict = Node::null(); + d_out->conflict(conflict, false); + return; + } + merge(assertion[0], assertion[1]); + break; + case kind::NOT: + { + Assert(assertion[0].getKind() == kind::EQUAL || + assertion[0].getKind() == kind::IFF ); + Node a = assertion[0][0]; + Node b = assertion[0][1]; + addDiseq(assertion[0]); + + d_cc.addTerm(a); + d_cc.addTerm(b); + + if(!d_conflict.isNull()) { + // we got notified through notifyCongruent which called merge + // after addTerm since we weren't watching a or b before + Node conflict = constructConflict(d_conflict); + d_conflict = Node::null(); + d_out->conflict(conflict, false); + return; + } + else if(find(a) == find(b)) { + Node conflict = constructConflict(assertion[0]); + d_out->conflict(conflict, false); + return; + } + Assert(!d_cc.areCongruent(a,b)); + if(a.getType().isArray()) { + queueExtLemma(a, b); + } + break; + } + default: + Unhandled(assertion.getKind()); + } + + } + + if(fullEffort(e)) { + // generate the lemmas on the worklist + //while(!d_RowQueue.empty() || ! d_extQueue.empty()) { + dischargeLemmas(); + Debug("arrays-lem")<<"Arrays::discharged lemmas "<size() > (*deq_ib).second->size()) { + TNode tmp = a; + a = b; + b = tmp; + } + } + a = find(a); + b = find(b); + + if( a == b) { + return; + } + + + // 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); + } + + +} + + +void TheoryArrays::checkPropagations(TNode a, TNode b) { + EqLists::const_iterator ita = d_equalities.find(a); + EqLists::const_iterator itb = d_equalities.find(b); + + if(ita != d_equalities.end()) { + if(itb!= d_equalities.end()) { + // because b is the canonical representative + List* eqsa = (*ita).second; + List* eqsb = (*itb).second; + + for(List::const_iterator it = eqsa->begin(); it!= eqsa->end(); ++it) { + Node eq = *it; + Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); + if(find(eq[0])== find(eq[1])) { + d_prop_queue.push_back(eq); + } + } + eqsb->concat(eqsa); + } + else { + List* eqsb = new List(&d_backtracker); + List* eqsa = (*ita).second; + d_equalities.insert(b, eqsb); + eqsb->concat(eqsa); + } + } else { + List* eqsb = new List(&d_backtracker); + d_equalities.insert(b, eqsb); + List* eqsa = new List(&d_backtracker); + d_equalities.insert(a, eqsa); + eqsb->concat(eqsa); + } +} + + +bool TheoryArrays::isNonLinear(TNode a) { + Assert(a.getType().isArray()); + const CTNodeList* inst = d_infoMap.getInStores(find(a)); + if(inst->size()<=1) { + return false; + } + return true; +} + +bool TheoryArrays::isAxiom(TNode t1, TNode t2) { + Debug("arrays-axiom")<<"Arrays::isAxiom start "< nb(kind::AND); + + if(explanation.getKind() == kind::EQUAL || + explanation.getKind() == kind::IFF) { + // if the explanation is only one literal + if(!isAxiom(explanation[0], explanation[1]) && + !isAxiom(explanation[1], explanation[0])) { + nb<push_back(b); + } + else { + CTNodeList* list = new (true)CTNodeList(getContext()); + list->push_back(b); + d_atoms[a] = list; + } + +} +*/ + +void TheoryArrays::addEq(TNode eq) { + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + TNode a = eq[0]; + TNode b = eq[1]; + + // don't need to say find(a) because due to the structure of the lists it gets + // automatically added + appendToEqList(a, eq); + appendToEqList(b, eq); + +} + +void TheoryArrays::appendToEqList(TNode n, TNode eq) { + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + + EqLists::const_iterator it = d_equalities.find(n); + if(it == d_equalities.end()) { + List* eqs = new List(&d_backtracker); + eqs->append(eq); + d_equalities.insert(n, eqs); + } else { + List* eqs = (*it).second; + eqs->append(eq); + } +} + +void TheoryArrays::addDiseq(TNode diseq) { + Assert(diseq.getKind() == kind::EQUAL || + diseq.getKind() == kind::IFF); + TNode a = diseq[0]; + TNode b = diseq[1]; + + appendToDiseqList(find(a), diseq); + appendToDiseqList(find(b), diseq); + +} + +void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { + Debug("arrays") << "appending " << eq << endl + << " to diseq list of " << of << endl; + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + + CNodeTNodesMap::iterator deq_i = d_disequalities.find(of); + CTNodeListAlloc* deq; + if(deq_i == d_disequalities.end()) { + deq = new(getContext()->getCMM()) CTNodeListAlloc(true, getContext(), false, + ContextMemoryAllocator(getContext()->getCMM())); + d_disequalities.insertDataFromContextMemory(of, deq); + } else { + deq = (*deq_i).second; + } + + deq->push_back(eq); +} + + +/** + * Iterates through the indices of a and stores of b and checks if any new + * Row lemmas need to be instantiated. + */ + +bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) { + Assert(a.getType().isArray()); + Assert(b.getType().isArray()); + + if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 || + d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) { + return true; + } + + return false; +} + +bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) { + NodeManager* nm = NodeManager::currentNM(); + Node aj = nm->mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + + if(find(i) == find(j) || find(aj) == find(bj)) { + //Debug("arrays-lem")<<"isRedundantInContext valid "<begin(); + for( ; i!= (*it).second->end(); i++) { + Debug("arrays-prop")<<" "<<*i<<"\n"; + TNode s = (*i)[0]; + TNode t = (*i)[1]; + + Assert(find(s) == a || find(t) == a); + TNode sp, tp; + if(find(t) == a) { + sp = find(t); + tp = find(s); + } + else { + sp = find(s); + tp = find(t); + } + + if(tp == b) { + return *i; + } + + } + } + Debug("arrays-prop")<<" not disequal \n"; + return TNode::null(); +} + +bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { + Debug("arrays-prop")<<"Arrays::propagateFromRow "<mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + + Node eq_aj_bj = nm->mkNode(kind::EQUAL,aj, bj); + Node eq_ij = nm->mkNode(kind::EQUAL, i, j); + + // first check if the current context implies NOT (i = j) + // in which case we can propagate a[j] = b[j] + // FIXME: does i = j need to be a SAT literal or can we propagate anyway? + + // if it does not have an atom we must add the lemma (do we?!) + if(d_atoms.count(eq_aj_bj) != 0 || + d_atoms.count(nm->mkNode(kind::EQUAL, bj, aj))!=0) { + Node diseq = areDisequal(i, j); + // check if the current context implies that (NOT i = j) + if(diseq != TNode::null()) { + // if it's unassigned + Debug("arrays-prop")<<"satValue "<propagate(eq_aj_bj); + ++d_numProp; + // save explanation + d_explanations.insert(eq_aj_bj,std::make_pair(eq_ij, diseq)); + return true; + } + + } + } + + // now check if the current context implies NOT a[j] = b[j] + // in which case we propagate i = j + + // we can't propagate if it does not have an atom + if(d_atoms.count(eq_ij) != 0 || d_atoms.count(nm->mkNode(kind::EQUAL, j, i))!= 0) { + + Node diseq = areDisequal(aj, bj); + Assert(TNode::null() == Node::null()); + + if(diseq != TNode::null()) { + if(d_valuation.getSatValue(eq_ij) == Node::null()) { + d_out->propagate(eq_ij); + ++d_numProp; + // save explanation + d_explanations.insert(eq_ij, std::make_pair(eq_aj_bj,diseq)); + return true; + } + } + } + + Debug("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; + return false; +} + +void TheoryArrays::explain(TNode n) { + + + Debug("arrays")<<"Arrays::explain start for "< nb(kind::AND); + + if(explanation.getKind() == kind::EQUAL || + explanation.getKind() == kind::IFF) { + // if the explanation is only one literal + if(!isAxiom(explanation[0], explanation[1]) && + !isAxiom(explanation[1], explanation[0])) { + nb<explanation(reason); + + /* + context::CDMap, TNodeHashFunction>::const_iterator + it = d_explanations.find(n); + Assert(it!= d_explanations.end()); + TNode diseq = (*it).second.second; + TNode s = diseq[0]; + TNode t = diseq[1]; + + TNode eq = (*it).second.first; + TNode a = eq[0]; + TNode b = eq[1]; + + Assert ((find(a) == find(s) && find(b) == find(t)) || + (find(a) == find(t) && find(b) == find(s))); + + + if(find(a) == find(t)) { + TNode temp = t; + t = s; + s = temp; + } + + // construct the explanation + + NodeBuilder<> nb(kind::AND); + Node explanation1 = d_cc.explain(a, s); + Node explanation2 = d_cc.explain(b, t); + + if(explanation1.getKind() == kind::AND) { + for(TNode::iterator i= TNode(explanation1).begin(); + i!=TNode(explanation1).end(); ++i) { + nb << *i; + } + } else { + Assert(explanation1.getKind() == kind::EQUAL || + explanation1.getKind() == kind::IFF); + nb << explanation1; + } + + if(explanation2.getKind() == kind::AND) { + for(TNode::iterator i= TNode(explanation2).begin(); + i!=TNode(explanation2).end(); ++i) { + nb << *i; + } + } else { + Assert(explanation2.getKind() == kind::EQUAL || + explanation2.getKind() == kind::IFF); + nb << explanation2; + } + + nb << diseq; + Node reason = nb; + d_out->explanation(reason); + Debug("arrays")<<"explanation "<< reason<<" done \n"; + */ +} + +void TheoryArrays::checkRowLemmas(TNode a, TNode b) { + + Debug("arrays-crl")<<"Arrays::checkLemmas begin \n"<print(); + Debug("arrays-crl")<<" ------------ and "<print(); + + List* i_a = d_infoMap.getIndices(a); + const CTNodeList* st_b = d_infoMap.getStores(b); + const CTNodeList* inst_b = d_infoMap.getInStores(b); + + List::const_iterator it = i_a->begin(); + CTNodeList::const_iterator its; + + for( ; it != i_a->end(); it++ ) { + TNode i = *it; + its = st_b->begin(); + for ( ; its != st_b->end(); its++) { + TNode store = *its; + Assert(store.getKind() == kind::STORE); + TNode j = store[1]; + TNode c = store[0]; + + if( !isRedundandRowLemma(store, c, j, i)){ + //&&!propagateFromRow(store, c, j, i)) { + queueRowLemma(store, c, j, i); + } + } + + } + + it = i_a->begin(); + + for( ; it != i_a->end(); it++ ) { + TNode i = *it; + its = inst_b->begin(); + for ( ; its !=inst_b->end(); its++) { + TNode store = *its; + Assert(store.getKind() == kind::STORE); + TNode j = store[1]; + TNode c = store[0]; + + if ( isNonLinear(c) + &&!isRedundandRowLemma(store, c, j, i)){ + //&&!propagateFromRow(store, c, j, i)) { + queueRowLemma(store, c, j, i); + } + + } + } + + Debug("arrays-crl")<<"Arrays::checkLemmas done.\n"; +} + +/** + * Adds a new Row lemma of the form i = j OR a[j] = b[j] if i and j are not the + * same and a and b are also not identical. + * + */ + +inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { + Assert(a.getType().isArray()); + Assert(b.getType().isArray()); + + // construct lemma + NodeManager* nm = NodeManager::currentNM(); + Node aj = nm->mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); + Node eq2 = nm->mkNode(kind::EQUAL, i, j); + Node lem = nm->mkNode(kind::OR, eq2, eq1); + + + + Debug("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lem); + ++d_numRow; + +} + + +/** + * Because a is now being read at position i check if new lemmas can be + * instantiated for all store terms equal to a and all store terms of the form + * store(a _ _ ) + */ +void TheoryArrays::checkRowForIndex(TNode i, TNode a) { + Debug("arrays-cri")<<"Arrays::checkRowForIndex "<print(); + } + Assert(a.getType().isArray()); + + const CTNodeList* stores = d_infoMap.getStores(a); + const CTNodeList* instores = d_infoMap.getInStores(a); + CTNodeList::const_iterator it = stores->begin(); + + for(; it!= stores->end(); it++) { + TNode store = *it; + Assert(store.getKind()==kind::STORE); + TNode j = store[1]; + //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<begin(); + for(; it!= instores->end(); it++) { + TNode instore = *it; + Assert(instore.getKind()==kind::STORE); + TNode j = instore[1]; + //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<print(); + } + Assert(a.getType().isArray()); + Assert(a.getKind()==kind::STORE); + TNode b = a[0]; + TNode i = a[1]; + + List* js = d_infoMap.getIndices(b); + List::const_iterator it = js->begin(); + + for(; it!= js->end(); it++) { + TNode j = *it; + + if(!isRedundandRowLemma(a, b, i, j)) { + //Debug("arrays-lem")<<"Arrays::checkRowStore ("<mkVar(a.getType()[0]); + Node eq = nm->mkNode(kind::EQUAL, a, b); + Node ak = nm->mkNode(kind::SELECT, a, k); + Node bk = nm->mkNode(kind::SELECT, b, k); + Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk)); + Node lem = nm->mkNode(kind::OR, eq, neq); + + Debug("arrays-lem")<<"Arrays::addExtLemma "<lemma(lem); + ++d_numExt; + return; + } + Debug("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + +} + diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index fbbda9e44..bc1f670ba 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Theory of arrays. + ** \brief Theory of arrays ** ** Theory of arrays. **/ @@ -22,32 +22,465 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #include "theory/theory.h" +#include "theory/arrays/union_find.h" +#include "util/congruence_closure.h" +#include "array_info.h" +#include "util/hash.h" +#include "util/ntuple.h" +#include "util/stats.h" +#include "util/backtrackable.h" #include +#include namespace CVC4 { namespace theory { namespace arrays { +/** + * Decision procedure for arrays. + * + * Overview of decision procedure: + * + * Preliminary notation: + * Stores(a) = {t | a ~ t and t = store( _ _ _ )} + * InStores(a) = {t | t = store (b _ _) and a ~ b } + * Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)} + * ~ represents the equivalence relation based on the asserted equalities in the + * current context. + * + * The rules implemented are the following: + * store(b i v) + * Row1 ------------------- + * store(b i v)[i] = v + * + * store(b i v) a'[j] + * Row ---------------------- [ a' ~ store(b i v) or a' ~ b ] + * i = j OR a[j] = b[j] + * + * a b same kind arrays + * Ext ------------------------ [ a!= b in current context, k new var] + * a = b OR a[k] != b[k]p + * + * + * The Row1 one rule is implemented implicitly as follows: + * - for each store(b i v) term add the following equality to the congruence + * closure store(b i v)[i] = v + * - if one of the literals in a conflict is of the form store(b i v)[i] = v + * remove it from the conflict + * + * Because new store terms are not created, we need to check if we need to + * instantiate a new Row axiom in the following cases: + * 1. the congruence relation changes (i.e. two terms get merged) + * - when a new equality between array terms a = b is asserted we check if + * we can instantiate a Row lemma for all pairs of indices i where a is + * being read and stores + * - this is only done during full effort check + * 2. a new read term is created either as a consequences of an Ext lemma or a + * Row lemma + * - this is implemented in the checkRowForIndex method which is called + * when preregistering a term of the form a[i]. + * - as a consequence lemmas are instantiated even before full effort check + * + * The Ext axiom is instantiated when a disequality is asserted during full effort + * check. Ext lemmas are stored in a cache to prevent instantiating essentially + * the same lemma multiple times. + */ class TheoryArrays : public Theory { + +private: + + + class CongruenceChannel { + TheoryArrays* d_arrays; + + public: + CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {} + void notifyCongruent(TNode a, TNode b) { + d_arrays->notifyCongruent(a, b); + } + }; /* class CongruenceChannel*/ + friend class CongruenceChannel; + + /** + * Output channel connected to the congruence closure module. + */ + CongruenceChannel d_ccChannel; + + /** + * Instance of the congruence closure module. + */ + CongruenceClosure d_cc; + + /** + * Union find for storing the equalities. + */ + + UnionFind d_unionFind; + + Backtracker d_backtracker; + + + /** + * 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 + */ + + ArrayInfo d_infoMap; + + /** + * Received a notification from the congruence closure algorithm that the two + * nodes a and b have become congruent. + */ + + void notifyCongruent(TNode a, TNode b); + + + typedef context::CDList > CTNodeListAlloc; + typedef context::CDMap CNodeTNodesMap; + typedef context::CDMap*, TNodeHashFunction > EqLists; + + + typedef __gnu_cxx::hash_map 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 d_prop_queue; + + void checkPropagations(TNode a, TNode b); + + /** List of all atoms the SAT solver knows about and are candidates for + * propagation. */ + __gnu_cxx::hash_set d_atoms; + + /** List of disequalities needed to construct explanations for propagated + * row lemmas */ + + context::CDMap, TNodeHashFunction> d_explanations; + + /** + * stores the conflicting disequality (still need to call construct + * conflict to get the actual explanation) + */ + Node d_conflict; + + typedef context::CDList< quad > QuadCDList; + + + /** + * Ext lemma workslist that stores extensionality lemmas that still need to be added + */ + std::hash_set, TNodePairHashFunction> d_extQueue; + + /** + * Row Lemma worklist, stores lemmas that can still be added to the SAT solver + * to be emptied during full effort check + */ + std::hash_set, TNodeQuadHashFunction > d_RowQueue; + + /** + * 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, TNodePairHashFunction> d_extAlreadyAdded; + + /** + * 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, TNodeQuadHashFunction > d_RowAlreadyAdded; + + /* + * Congruence helper methods + */ + + void addDiseq(TNode diseq); + void addEq(TNode eq); + + void appendToDiseqList(TNode of, TNode eq); + void appendToEqList(TNode a, TNode b); + Node constructConflict(TNode diseq); + + /** + * Merges two congruence classes in the internal union-find and checks for a + * conflict. + */ + + void merge(TNode a, TNode b); + inline TNode find(TNode a); + inline TNode debugFind(TNode a) const; + + inline void setCanon(TNode a, TNode b); + + void queueRowLemma(TNode a, TNode b, TNode i, TNode j); + inline void queueExtLemma(TNode a, TNode b); + + /** + * Adds a Row lemma of the form: + * i = j OR a[j] = b[j] + */ + void addRowLemma(TNode a, TNode b, TNode i, TNode j); + + /** + * 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); + + /** + * 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); + + + bool isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j); + bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j); + + + + bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) { + //Debug("arrays-lem")<<"alreadyAddedRow check for "<, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin(); + a = find(a); + b = find(b); + i = find(i); + j = find(j); + + for( ; it!= d_RowAlreadyAdded.end(); it++) { + + 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_) { + //Debug("arrays-lem")<<"alreadyAddedRow found "< >& 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, TNodeQuadHashFunction > temp_Row; + temp_Row.swap(d_RowQueue); + + std::hash_set, 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); + } + } + + std::hash_set, TNodePairHashFunction> temp_ext; + temp_ext.swap(d_extQueue); + + std::hash_set, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin(); + for(; it2 != temp_ext.end(); it2++) { + addExtLemma((*it2).first, (*it2).second); + } + } + + /** 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); + + TNode areDisequal(TNode a, TNode b); + + + + /* + * === STATISTICS === + */ + + /** 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; + + public: TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation); ~TheoryArrays(); - void preRegisterTerm(TNode n) { } - //void registerTerm(TNode n) { } - //void presolve() { } + /** + * 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. + */ + void preRegisterTerm(TNode n) { + //TimerStat::CodeTimer codeTimer(d_preregisterTimer); + Debug("arrays-preregister")<<"Arrays::preRegisterTerm "<getLevel()<<"\n"; + d_infoMap.addIndex(n[0], n[1]); + checkRowForIndex(n[1], find(n[0])); + //Debug("arrays-preregister")<<"n[0] \n"; + //d_infoMap.getInfo(n[0])->print(); + //Debug("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: + Debug("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; + } + } + + //void registerTerm(TNode n) { + // Debug("arrays-register")<<"Arrays::registerTerm "<::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::const_iterator it = d_atoms.begin(); + + for(; it!= d_atoms.end(); it++) { + TNode eq = *it; + Assert(eq.getKind()==kind::EQUAL); + Debug("arrays-prop")<<"value of "<mkConst(true)); + } + // checks for RoW axiom: (select ( store a i v) i) = v and rewrites it + // to true + if(node[0].getKind()==kind::SELECT) { + TNode a = node[0][0]; + TNode j = node[0][1]; + if(a.getKind()==kind::STORE) { + TNode b = a[0]; + TNode i = a[1]; + TNode v = a[2]; + if(v == node[1] && i == j) { + Debug("arrays-postrewrite") << "Arrays::postRewrite true" << std::endl; + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + } + } + + if (node[0] > node[1]) { + Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); + // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change) + if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) { + return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + } else { + return RewriteResponse(REWRITE_DONE, newNode); + } + } + } + // FIXME: would it be better to move in preRewrite? + // if yes don't need the above case + if (node.getKind()==kind::SELECT) { + // we are rewriting (select (store a i v) i) to v + TNode a = node[0]; + TNode i = node[1]; + if(a.getKind() == kind::STORE) { + TNode b = a[0]; + TNode j = a[1]; + TNode v = a[2]; + if(i==j) { + Debug("arrays-postrewrite") << "Arrays::postrewrite to " << v << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, v); + } + } + } + return RewriteResponse(REWRITE_DONE, node); } static inline RewriteResponse preRewrite(TNode node) { + Debug("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp new file mode 100644 index 000000000..b0f06b78e --- /dev/null +++ b/src/theory/arrays/union_find.cpp @@ -0,0 +1,59 @@ +/********************* */ +/*! \file union_find.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "theory/arrays/union_find.h" +#include "util/Assert.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arrays { + +template +void UnionFind::notify() { + Trace("arraysuf") << "arraysUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; + while(d_offset < d_trace.size()) { + pair p = d_trace.back(); + if(p.second.isNull()) { + d_map.erase(p.first); + Trace("arraysuf") << "arraysUF " << d_trace.size() << " erasing " << p.first << endl; + } else { + d_map[p.first] = p.second; + Trace("arraysuf") << "arraysUF " << d_trace.size() << " replacing " << p << endl; + } + d_trace.pop_back(); + } + Trace("arraysuf") << "arraysUF cancelling finished." << endl; +} + +// The following declarations allow us to put functions in the .cpp file +// instead of the header, since we know which instantiations are needed. + +template void UnionFind::notify(); + +template void UnionFind::notify(); + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h new file mode 100644 index 000000000..4a882806c --- /dev/null +++ b/src/theory/arrays/union_find.h @@ -0,0 +1,146 @@ +/********************* */ +/*! \file union_find.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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__UNION_FIND_H +#define __CVC4__THEORY__ARRAYS__UNION_FIND_H + +#include +#include +#include + +#include "expr/node.h" +#include "context/cdo.h" + +namespace CVC4 { + +namespace context { + class Context; +}/* CVC4::context namespace */ + +namespace theory { +namespace arrays { + +// NodeType \in { Node, TNode } +template +class UnionFind : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef __gnu_cxx::hash_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; + + /** Our undo stack for changes made to d_map. */ + std::vector > d_trace; + + /** Our current offset in the d_trace stack (context-dependent). */ + context::CDO d_offset; + +public: + UnionFind(context::Context* ctxt) : + context::ContextNotifyObj(ctxt), + d_offset(ctxt, 0) { + } + + ~UnionFind() throw() { } + + /** + * 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); + + /** + * Called by the Context when a pop occurs. Cancels everything to the + * current context level. Overrides ContextNotifyObj::notify(). + */ + void notify(); + +};/* class UnionFind<> */ + +template +inline TNode UnionFind::debugFind(TNode n) const { + typename MapType::const_iterator i = d_map.find(n); + if(i == d_map.end()) { + return n; + } else { + return debugFind((*i).second); + } +} + +template +inline TNode UnionFind::find(TNode n) { + Trace("arraysuf") << "arraysUF find of " << n << std::endl; + typename 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; + } + d_trace.push_back(std::make_pair(n, pr.second)); + d_offset = d_trace.size(); + Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; + pr.second = p; + d_map.insert(pr); + return p; + } +} + +template +inline void UnionFind::setCanon(TNode n, TNode newParent) { + Assert(d_map.find(n) == d_map.end()); + Assert(d_map.find(newParent) == d_map.end()); + if(n != newParent) { + Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; + d_map[n] = newParent; + d_trace.push_back(std::make_pair(n, TNode::null())); + d_offset = d_trace.size(); + } +} + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /*__CVC4__THEORY__ARRAYS__UNION_FIND_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 69220ad62..cf105803c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -123,7 +123,11 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { // traversing a DAG as a tree and that can really blow up @CB if(! n.getAttribute(RegisteredAttr())) { n.setAttribute(RegisteredAttr(), true); - d_engine->theoryOf(n)->registerTerm(n); + if (n.getKind() == kind::EQUAL) { + d_engine->theoryOf(n[0])->registerTerm(n); + } else { + d_engine->theoryOf(n)->registerTerm(n); + } } } }/* Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) */ @@ -198,10 +202,13 @@ void TheoryEngine::preRegister(TNode preprocessed) { current.setAttribute(PreRegistered(), true); // Register this node if (current.getKind() == kind::EQUAL) { - TheoryId theoryLHS = Theory::theoryOf(current[0]); - Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; - markActive(theoryLHS); - d_theoryTable[theoryLHS]->preRegisterTerm(current); + if(d_logic == "QF_AX") { + d_theoryTable[theory::THEORY_ARRAY]->preRegisterTerm(current); + } else { + TheoryId theoryLHS = Theory::theoryOf(current[0]); + Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + markActive(theoryLHS); + d_theoryTable[theoryLHS]->preRegisterTerm(current); // TheoryId theoryRHS = Theory::theoryOf(current[1]); // if (theoryLHS != theoryRHS) { // markActive(theoryRHS); @@ -214,6 +221,7 @@ void TheoryEngine::preRegister(TNode preprocessed) { // d_theoryTable[typeTheory]->preRegisterTerm(current); // Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; // } + } } else { TheoryId theory = Theory::theoryOf(current); Debug("register") << "preregistering " << current << " with " << theory << std::endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e571c2bbd..2dd3db863 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -200,19 +200,17 @@ class TheoryEngine { } public: + /** The logic of the problem */ + std::string d_logic; - /** - * Construct a theory engine. - */ + /** Constructs a theory engine */ TheoryEngine(context::Context* ctxt); - /** - * Destroy a theory engine. - */ + /** Destroys a theory engine */ ~TheoryEngine(); /** - * Adds a theory. Only one theory per theoryId can be present, so if + * Adds a theory. Only one theory per TheoryId can be present, so if * there is another theory it will be deleted. */ template @@ -306,7 +304,7 @@ public: * @param node the assertion */ inline void assertFact(TNode node) { - Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl<assertFact(node); + if(d_logic == "QF_AX") { + //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n"; + d_theoryTable[theory::THEORY_ARRAY]->assertFact(node); + } else { + theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]); + Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl; + d_theoryTable[theoryLHS]->assertFact(node); // theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]); // if (theoryLHS != theoryRHS) { // Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl; @@ -332,6 +334,7 @@ public: // Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl; // d_theoryTable[typeTheory]->assertFact(node); // } + } } else { theory::Theory* theory = theoryOf(atom); Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; @@ -398,7 +401,12 @@ public: d_theoryOut.d_explanationNode = Node::null(); TNode atom = node.getKind() == kind::NOT ? node[0] : node; if (atom.getKind() == kind::EQUAL) { - theoryOf(atom[0])->explain(node); + if(d_logic == "QF_AX") { + //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n"; + d_theoryTable[theory::THEORY_ARRAY]->explain(node); + } else { + theoryOf(atom[0])->explain(node); + } } else { theoryOf(atom)->explain(node); } @@ -417,8 +425,7 @@ private: d_statPropagate("theory::propagate", 0), d_statLemma("theory::lemma", 0), d_statAugLemma("theory::aug_lemma", 0), - d_statExplanation("theory::explanation", 0) - { + d_statExplanation("theory::explanation", 0) { StatisticsRegistry::registerStat(&d_statConflicts); StatisticsRegistry::registerStat(&d_statPropagate); StatisticsRegistry::registerStat(&d_statLemma); @@ -433,7 +440,7 @@ private: StatisticsRegistry::unregisterStat(&d_statAugLemma); StatisticsRegistry::unregisterStat(&d_statExplanation); } - }; + };/* class TheoryEngine::Statistics */ Statistics d_statistics; };/* class TheoryEngine */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 5672d1eb2..b8f336f2d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -20,6 +20,7 @@ libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ libutil_la_SOURCES = \ Assert.h \ Assert.cpp \ + backtrackable.h \ Makefile.am \ Makefile.in \ congruence_closure.h \ @@ -47,7 +48,7 @@ libutil_la_SOURCES = \ dynamic_array.h \ language.h \ language.cpp \ - triple.h \ + ntuple.h \ recursion_breaker.h \ subrange_bound.h \ cardinality.h \ diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h new file mode 100644 index 000000000..b11ebf957 --- /dev/null +++ b/src/util/backtrackable.h @@ -0,0 +1,214 @@ +/*! \file backtrackable.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains a backtrackable list + ** + ** + **/ + +#include "cvc4_private.h" +#ifndef __CVC4__UTIL__BACKTRACKABLE_H +#define __CVC4__UTIL__BACKTRACKABLE_H + + +#include +#include +#include "context/cdo.h" + +namespace CVC4{ + +template class List; +template class List_iterator; +template class Backtracker; + +template +class ListNode{ +private: + T data; + ListNode* next; + + bool empty; + ListNode(const T& t, ListNode* n, bool e = false) : data(t), next(n), empty(e) {} + ~ListNode() { + // maybe set to NULL + delete next; + } + + friend class List; + friend class List_iterator; +}; /*class ListNode */ + +template +class List_iterator: public std::iterator { + friend class List; + +public: + const T& operator*(); + List_iterator& operator++(); + List_iterator operator++(int); + bool operator!=(const List_iterator & other) const; +private: + const ListNode* pointee; + List_iterator(const ListNode* p) : pointee(p) {} + +}; /* class List_iterator */ + +template const T& List_iterator::operator*() { + return pointee->data; +} + +template List_iterator& List_iterator::operator++() { + Assert(pointee != NULL); + pointee = pointee->next; + while(pointee != NULL && pointee->empty ) { + pointee = pointee->next; + } + return *this; +} + +template List_iterator List_iterator::operator++(int) { + List_iterator it = *this; + ++*this; + return it; +} + +template bool List_iterator::operator!=(const List_iterator& other) const { + return (this->pointee != other.pointee); +} + +// !! for the backtracking to work the lists must be allocated on the heap +// therefore the hashmap from TNode to List should store pointers! +template class List { + ListNode* head; + ListNode* tail; + ListNode* ptr_to_head; + bool uninitialized; + Backtracker* bck; + List (const List&) {} +public: + List(Backtracker* b) : ptr_to_head(NULL), uninitialized(true), bck(b) { + head = tail = (ListNode*)calloc(1,sizeof(ListNode*)); + head->next = NULL; + head->empty = true; + } + ~List() {delete head;} + bool empty() { + bck->checkConsistency(); + return head == NULL; + } + void append(const T& d); + //typedef List_iterator iterator; + typedef List_iterator const_iterator; + + const_iterator begin() { + bck->checkConsistency(); + if(head->empty) { + ListNode* temp = head; + // if the head is empty return the first non-empty element or NULL + while(temp != NULL && temp->empty ) { + temp = temp->next; + } + return List_iterator(temp); + } + return List_iterator(head); + } + + const_iterator end() { + bck->checkConsistency(); + return List_iterator(NULL); + } + void concat(List* other); + void unconcat(List* other); +}; /* class List */ + +template +void List::append (const T& d) { + bck->checkConsistency(); + + if(uninitialized) { + new(head)ListNode (d, head->next); + //head->data = d; + head->empty = false; + //Assert(tail == head); FIXME: do I need this because this list might be empty but appende to another one + uninitialized = false; + + } else { + ListNode* new_node = new ListNode(d, head); + head = new_node; + } + + if(ptr_to_head != NULL) { + ptr_to_head->next = head; + } +} + +template +void List::concat (List* other) { + bck->checkConsistency(); + bck->notifyConcat(this, other); + Assert(tail->next==NULL); + tail->next = other->head; + Assert(other->ptr_to_head == NULL); + other->ptr_to_head = tail; + tail = other->tail; +} + +template +void List::unconcat(List* other) { + // we do not need to check consistency since this is only called by the + //Backtracker when we are inconsistent + Assert(other->ptr_to_head != NULL); + other->ptr_to_head->next = NULL; + tail = other->ptr_to_head; + other->ptr_to_head = NULL; +} + +/* Backtrackable Table */ + +template class Backtracker { + friend class List; + std::vector*,List*> > undo_stack; + + int curr_level; + context::CDO pop_level; + + void checkConsistency(); + void notifyConcat(List* a, List* b); +public: + Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {} + ~Backtracker() {} + +}; /*class Backtrackable */ + +template void Backtracker::notifyConcat(List* a, List* b) { + curr_level++; + pop_level.set(pop_level.get()+1); + undo_stack.push_back( std::make_pair(a, b)); +} + +template void Backtracker::checkConsistency() { + if( curr_level == pop_level || pop_level == -1) { + return; + } + Assert(curr_level > pop_level); + + while (curr_level > pop_level) { + curr_level--; + List* l1 = undo_stack[curr_level].first; + List* l2 = undo_stack[curr_level].second; + l1->unconcat(l2); + undo_stack.pop_back(); + } + Assert(curr_level == pop_level); +} +} /* CVC4 namespace */ +#endif /* __CVC4__UTIL__BACKTRACKABLE_H */ diff --git a/src/util/ntuple.h b/src/util/ntuple.h new file mode 100644 index 000000000..a3b0dfdf4 --- /dev/null +++ b/src/util/ntuple.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file ntuple.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: lianah + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Similar to std::pair<>, for triples and quadruples + ** + ** Similar to std::pair<>, for triples and quadruples. Once we move to c++0x, this + ** can be removed in favor of (standard-provided) N-ary tuples. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__NTUPLE_H +#define __CVC4__NTUPLE_H + +namespace CVC4 { + +template +class triple { +public: + T1 first; + T2 second; + T3 third; +};/* class triple<> */ + +template +inline triple +make_triple(const T1& t1, const T2& t2, const T3& t3) { + return triple(t1, t2, t3); +}/* make_triple() */ + +template +class quad { +public: + T1 first; + T2 second; + T3 third; + T4 fourth; + quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) { + first = t1; + second = t2; + third = t3; + fourth = t4; + } +};/* class quad<> */ + +template +bool operator==(const quad& x, + const quad& y) { + return (x.first==y.first && x.second==y.second && + x.third == y.third && x.fourth==y.fourth); +} + +template +bool operator<(const quad& x, + const quad& y) { + if(x.first< y.first) { + return true; + } + else if (x.first == y.first) { + if(x.second < y.second) { + return true; + } + else if(y.second == y.second) { + if(x.third < y.third) { + return true; + } + else if (x.fourth < y.fourth) { + return true; + } + } + } + return false; +} + +template +inline quad +make_quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) { + return quad(t1, t2, t3, t4); +}/* make_quad() */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__NTUPLE_H */ diff --git a/src/util/stats.h b/src/util/stats.h index 882cc1f81..a94733595 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -446,6 +446,24 @@ public: };/* class IntStat */ +template +class SizeStat : public Stat { +private: + const T& d_sized; +public: + SizeStat(const std::string&name, const T& sized) : + Stat(name), d_sized(sized) {} + ~SizeStat() {} + + void flushInformation(std::ostream& out) const { + out<< d_sized.size(); + } + std::string getValue() const { + std::stringstream ss; + flushInformation(ss); + return ss.str(); + } +};/* class SizeStat */ /** * The value for an AverageStat is the running average of (e1, e_2, ..., e_n), diff --git a/src/util/triple.h b/src/util/triple.h deleted file mode 100644 index 9229a9eee..000000000 --- a/src/util/triple.h +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/*! \file triple.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Similar to std::pair<>, for triples - ** - ** Similar to std::pair<>, for triples. Once we move to c++0x, this - ** can be removed in favor of (standard-provided) N-ary tuples. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__TRIPLE_H -#define __CVC4__TRIPLE_H - -namespace CVC4 { - -template -class triple { -public: - T1 first; - T2 second; - T3 third; -}; - -template -inline triple -make_triple(const T1& t1, const T2& t2, const T3& t3) { - return triple(t1, t2, t3); -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__TRIPLE_H */ diff --git a/test/Makefile.am b/test/Makefile.am index aceef1b68..354b81470 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \ blu=''; \ std=''; \ } -subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3 +subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/arrays regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3 check-recursive: check-pre .PHONY: check-pre check-pre: diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 319601121..89df462e5 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra bv datatypes lemmas push-pop +SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 MAKEFLAGS = -k diff --git a/test/regress/regress0/arrays/Makefile b/test/regress/regress0/arrays/Makefile new file mode 100644 index 000000000..1f480a4ad --- /dev/null +++ b/test/regress/regress0/arrays/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/arrays + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am new file mode 100644 index 000000000..8fdeda04a --- /dev/null +++ b/test/regress/regress0/arrays/Makefile.am @@ -0,0 +1,31 @@ +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + arrays0.smt2 \ + arrays1.smt2 \ + arrays2.smt2 \ + arrays3.smt2 \ + arrays4.smt2 + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/arrays/arrays0.smt2 b/test/regress/regress0/arrays/arrays0.smt2 new file mode 100644 index 000000000..652ff0bcb --- /dev/null +++ b/test/regress/regress0/arrays/arrays0.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_AX) +(set-info :source | +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1)))) +(assert (not (= a1 a2))) +(check-sat) +(exit) diff --git a/test/regress/regress0/arrays/arrays1.smt2 b/test/regress/regress0/arrays/arrays1.smt2 new file mode 100644 index 000000000..f001cc33e --- /dev/null +++ b/test/regress/regress0/arrays/arrays1.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AX) +(set-info :source | +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun i0 () Index) +(declare-fun i1 () Index) +(assert (let ((?v_0 (select a1 i1))) (let ((?v_1 (store (store a1 i1 ?v_0) i1 ?v_0))) (let ((?v_2 (select ?v_1 i0))) (let ((?v_3 (store (store ?v_1 i0 ?v_2) i0 ?v_2))) (not (= ?v_3 ?v_3))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/arrays/arrays2.smt2 b/test/regress/regress0/arrays/arrays2.smt2 new file mode 100644 index 000000000..7c14477e2 --- /dev/null +++ b/test/regress/regress0/arrays/arrays2.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AX) +(set-info :source | +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun i0 () Index) +(declare-fun i1 () Index) +(assert (let ((?v_0 (select a1 i1))) (let ((?v_1 (store (store a1 i1 ?v_0) i1 ?v_0))) (let ((?v_2 (select ?v_1 i0))) (not (= (store (store ?v_1 i0 (select ?v_1 i1)) i1 ?v_2) (store (store ?v_1 i0 ?v_2) i0 ?v_2))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/arrays/arrays3.smt2 b/test/regress/regress0/arrays/arrays3.smt2 new file mode 100644 index 000000000..a21397b1d --- /dev/null +++ b/test/regress/regress0/arrays/arrays3.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_AX) +(set-info :source | +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(assert (let ((?v_0 (store a2 i1 (select a1 i1))) (?v_1 (store a1 i1 (select a2 i1)))) (= (store ?v_1 i1 (select ?v_0 i2)) (store ?v_0 i2 (select ?v_1 i2))))) +(assert (not (= a1 a2))) +(check-sat) +(exit) diff --git a/test/regress/regress0/arrays/arrays4.smt2 b/test/regress/regress0/arrays/arrays4.smt2 new file mode 100644 index 000000000..f4afded65 --- /dev/null +++ b/test/regress/regress0/arrays/arrays4.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_AX) +(set-info :source | +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(assert (let ((?v_0 (store a2 i1 (select a1 i1))) (?v_1 (store a1 i1 (select a2 i1)))) (= (store ?v_1 i2 (select ?v_0 i2)) (store ?v_0 i2 (select ?v_1 i2))))) +(assert (not (= a1 a2))) +(check-sat) +(exit) -- 2.30.2