#include <vector>
#include <string>
#include <iostream>
+#include <utility>
#include <stdint.h>
#include "expr/type.h"
}
};/* struct TNodeHashFunction */
+struct TNodePairHashFunction {
+ size_t operator()(const std::pair<CVC4::TNode, CVC4::TNode>& pair ) const {
+ TNode n1 = pair.first;
+ TNode n2 = pair.second;
+
+ return (size_t) (n1.getId() * 0x9e3779b9 + n2.getId());
+ }
+};/* struct TNodePairHashFunction */
+
template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
assertTNodeNotExpired();
throw ModalException("logic already set");
}
d_logic = s;
+ d_theoryEngine->d_logic = s;
}
void SmtEngine::setInfo(const std::string& key, const SExpr& value)
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
--- /dev/null
+/********************* */
+/*! \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<TNode>* list) {
+ List<TNode>::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<TNode> 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 "<<a<<"["<<i<<"]\n";
+ List<TNode>* temp_indices;
+ Info* temp_info;
+
+ CNodeInfoMap::iterator it = info_map.find(a);
+ if(it == info_map.end()) {
+ temp_indices = new List<TNode>(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 "<<a<<" ~ "<<b<<"\n";
+ Assert(a.getType().isArray());
+ Assert(b.getType().isArray());
+
+ CTNodeList* temp_inst;
+ Info* temp_info;
+
+ CNodeInfoMap::iterator it = info_map.find(a);
+ if(it == info_map.end()) {
+ temp_inst = new(true) CTNodeList(ct);
+ temp_inst->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<TNode>* 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 "<<a<<"\n";
+ Debug("arrays-mergei")<<" and "<<b<<"\n";
+
+ CNodeInfoMap::iterator ita = info_map.find(a);
+ CNodeInfoMap::iterator itb = info_map.find(b);
+
+ if(ita != info_map.end()) {
+ Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
+ if(Debug.isOn("arrays-mergei"))
+ (*ita).second->print();
+
+ if(itb != info_map.end()) {
+ Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
+ if(Debug.isOn("arrays-mergei"))
+ (*itb).second->print();
+
+ List<TNode>* lista_i = (*ita).second->indices;
+ CTNodeList* lista_st = (*ita).second->stores;
+ CTNodeList* lista_inst = (*ita).second->in_stores;
+
+
+ List<TNode>* 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<TNode>* 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 */
--- /dev/null
+/*! \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 <ext/hash_set>
+#include <ext/hash_map>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+typedef context::CDList<TNode> CTNodeList;
+
+struct TNodeQuadHashFunction {
+ size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& 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<TNode>* 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<TNode>* indices;
+ CTNodeList* stores;
+ CTNodeList* in_stores;
+
+ Info(context::Context* c, Backtracker<TNode>* bck) {
+ indices = new List<TNode>(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<Node, Info*, NodeHashFunction> 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<TNode>* bck;
+ CNodeInfoMap info_map;
+
+ CTNodeList* emptyList;
+ List<TNode>* 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<CNodeInfoMap > 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<TNode>* 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<TNode>(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<TNode>* 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 */
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"
#include "theory/arrays/theory_arrays.h"
#include "theory/valuation.h"
#include "expr/kind.h"
-
+#include <map>
using namespace std;
using namespace CVC4;
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<TNode>(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 "<<d_RowQueue.size()<<"\n";
+ //}
}
- Debug("arrays") << "TheoryArrays::check(): done" << endl;
+ Debug("arrays") << "Arrays::check(): done" << endl;
}
Node TheoryArrays::getValue(TNode n) {
Unhandled(n.getKind());
}
}
+
+void TheoryArrays::merge(TNode a, TNode b) {
+ Assert(d_conflict.isNull());
+
+ Debug("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
+
+ /*
+ * take care of the congruence closure part
+ */
+
+ // make "a" the one with shorter diseqList
+ CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
+ CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+
+ if(deq_ia != d_disequalities.end()) {
+ if(deq_ib == d_disequalities.end() ||
+ (*deq_ia).second->size() > (*deq_ib).second->size()) {
+ TNode tmp = a;
+ a = b;
+ b = tmp;
+ }
+ }
+ a = find(a);
+ b = find(b);
+
+ if( a == b) {
+ return;
+ }
+
+
+ // b becomes the canon of a
+ setCanon(a, b);
+
+ deq_ia = d_disequalities.find(a);
+ map<TNode, TNode> alreadyDiseqs;
+ if(deq_ia != d_disequalities.end()) {
+ /*
+ * Collecting the disequalities of b, no need to check for conflicts
+ * since the representative of b does not change and we check all the things
+ * in a's class when we look at the diseq list of find(a)
+ */
+
+ CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+ if(deq_ib != d_disequalities.end()) {
+ CTNodeListAlloc* deq = (*deq_ib).second;
+ for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) {
+ TNode deqn = *j;
+ TNode s = deqn[0];
+ TNode t = deqn[1];
+ TNode sp = find(s);
+ TNode tp = find(t);
+ Assert(sp == b || tp == b);
+ if(sp == b) {
+ alreadyDiseqs[tp] = deqn;
+ } else {
+ alreadyDiseqs[sp] = deqn;
+ }
+ }
+ }
+
+ /*
+ * Looking for conflicts in the a disequality list. Note
+ * that at this point a and b are already merged. Also has
+ * the side effect that it adds them to the list of b (which
+ * became the canonical representative)
+ */
+
+ CTNodeListAlloc* deqa = (*deq_ia).second;
+ for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) {
+ TNode deqn = (*i);
+ Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF);
+ TNode s = deqn[0];
+ TNode t = deqn[1];
+ TNode sp = find(s);
+ TNode tp = find(t);
+
+ if(find(s) == find(t)) {
+ d_conflict = deqn;
+ return;
+ }
+ Assert( sp == b || tp == b);
+
+ // make sure not to add duplicates
+
+ if(sp == b) {
+ if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
+ appendToDiseqList(b, deqn);
+ alreadyDiseqs[tp] = deqn;
+ }
+ } else {
+ if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
+ appendToDiseqList(b, deqn);
+ alreadyDiseqs[sp] = deqn;
+ }
+ }
+
+ }
+ }
+
+ // TODO: check for equality propagations
+ // a and b are find(a) and find(b) here
+ checkPropagations(a,b);
+
+ if(a.getType().isArray()) {
+ checkRowLemmas(a,b);
+ checkRowLemmas(b,a);
+ // note the change in order, merge info adds the list of
+ // the 2nd argument to the first
+ d_infoMap.mergeInfo(b, a);
+ }
+
+
+}
+
+
+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<TNode>* eqsa = (*ita).second;
+ List<TNode>* eqsb = (*itb).second;
+
+ for(List<TNode>::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<TNode>* eqsb = new List<TNode>(&d_backtracker);
+ List<TNode>* eqsa = (*ita).second;
+ d_equalities.insert(b, eqsb);
+ eqsb->concat(eqsa);
+ }
+ } else {
+ List<TNode>* eqsb = new List<TNode>(&d_backtracker);
+ d_equalities.insert(b, eqsb);
+ List<TNode>* eqsa = new List<TNode>(&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 "<<t1<<" = "<<t2<<"\n";
+ if(t1.getKind() == kind::SELECT) {
+ TNode a = t1[0];
+ TNode i = t1[1];
+
+ if(a.getKind() == kind::STORE) {
+ TNode b = a[0];
+ TNode j = a[1];
+ TNode v = a[2];
+ if(i == j && v == t2) {
+ Debug("arrays-axiom")<<"Arrays::isAxiom true\n";
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+
+Node TheoryArrays::constructConflict(TNode diseq) {
+ Debug("arrays") << "arrays: begin constructConflict()" << endl;
+ Debug("arrays") << "arrays: using diseq == " << diseq << endl;
+
+ // returns the reason the two terms are equal
+ Node explanation = d_cc.explain(diseq[0], diseq[1]);
+
+ NodeBuilder<> 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;
+ }
+ }
+ else {
+ Assert(explanation.getKind() == kind::AND);
+ for(TNode::iterator i = TNode(explanation).begin();
+ i != TNode(explanation).end(); i++) {
+ if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
+ nb<<*i;
+ }
+ }
+ }
+
+ nb<<diseq.notNode();
+ Node conflict = nb;
+ Debug("arrays") << "conflict constructed : " << conflict << endl;
+ return conflict;
+}
+
+/*
+void TheoryArrays::addAtom(TNode eq) {
+ Assert(eq.getKind() == kind::EQUAL);
+
+ TNode lhs = eq[0];
+ TNode rhs = eq[1];
+
+ appendToAtomList(find(lhs), rhs);
+ appendToAtomList(find(rhs), lhs);
+}
+
+void TheoryArrays::appendToAtomList(TNode a, TNode b) {
+ Assert(find(a) == a);
+
+ NodeTNodesMap::const_iterator it = d_atoms.find(a);
+ if(it != d_atoms.end()) {
+ (*it).second->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<TNode>* eqs = new List<TNode>(&d_backtracker);
+ eqs->append(eq);
+ d_equalities.insert(n, eqs);
+ } else {
+ List<TNode>* 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<TNode>(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 "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+ checkRowForIndex(j,b); // why am i doing this?
+ checkRowForIndex(i,a);
+ return true;
+ }
+ if(alreadyAddedRow(a,b,i,j)) {
+ // Debug("arrays-lem")<<"isRedundantInContext already added "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+ return true;
+ }
+ return false;
+}
+
+TNode TheoryArrays::areDisequal(TNode a, TNode b) {
+ Debug("arrays-prop")<<"Arrays::areDisequal "<<a<<" "<<b<<"\n";
+
+ a = find(a);
+ b = find(b);
+
+ CNodeTNodesMap::const_iterator it = d_disequalities.find(a);
+ if(it!= d_disequalities.end()) {
+ CTNodeListAlloc::const_iterator i = (*it).second->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 "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node aj = nm->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 "<<d_valuation.getSatValue(eq_aj_bj).isNull();
+ if(d_valuation.getSatValue(eq_aj_bj).isNull()) {
+ d_out->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 "<<n<<"\n";
+ ++d_numExplain;
+
+ Assert(n.getKind()==kind::EQUAL);
+
+ Node explanation = d_cc.explain(n[0], n[1]);
+
+ NodeBuilder<> 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;
+ }
+ }
+ else {
+ Assert(explanation.getKind() == kind::AND);
+ for(TNode::iterator i = TNode(explanation).begin();
+ i != TNode(explanation).end(); i++) {
+ if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
+ nb<<*i;
+ }
+ }
+ }
+ Node reason = nb;
+
+ d_out->explanation(reason);
+
+ /*
+ context::CDMap<TNode, std::pair<TNode, TNode>, 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"<<a<<"\n";
+ if(Debug.isOn("arrays-crl"))
+ d_infoMap.getInfo(a)->print();
+ Debug("arrays-crl")<<" ------------ and "<<b<<"\n";
+ if(Debug.isOn("arrays-crl"))
+ d_infoMap.getInfo(b)->print();
+
+ List<TNode>* i_a = d_infoMap.getIndices(a);
+ const CTNodeList* st_b = d_infoMap.getStores(b);
+ const CTNodeList* inst_b = d_infoMap.getInStores(b);
+
+ List<TNode>::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 "<<lem<<"\n";
+ d_RowAlreadyAdded.insert(make_quad(a,b,i,j));
+ d_out->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 "<<a<<"\n";
+ Debug("arrays-cri")<<" index "<<i<<"\n";
+
+ if(Debug.isOn("arrays-cri")) {
+ d_infoMap.getInfo(a)->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 ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+ if(!isRedundandRowLemma(store, store[0], j, i)) {
+ //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(store, store[0], j, i);
+ }
+ }
+
+ it = instores->begin();
+ for(; it!= instores->end(); it++) {
+ TNode instore = *it;
+ Assert(instore.getKind()==kind::STORE);
+ TNode j = instore[1];
+ //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+ if(!isRedundandRowLemma(instore, instore[0], j, i)) {
+ //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(instore, instore[0], j, i);
+ }
+ }
+
+}
+
+
+void TheoryArrays::checkStore(TNode a) {
+ Debug("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
+
+ if(Debug.isOn("arrays-cri")) {
+ d_infoMap.getInfo(a)->print();
+ }
+ Assert(a.getType().isArray());
+ Assert(a.getKind()==kind::STORE);
+ TNode b = a[0];
+ TNode i = a[1];
+
+ List<TNode>* js = d_infoMap.getIndices(b);
+ List<TNode>::const_iterator it = js->begin();
+
+ for(; it!= js->end(); it++) {
+ TNode j = *it;
+
+ if(!isRedundandRowLemma(a, b, i, j)) {
+ //Debug("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+ queueRowLemma(a,b,i,j);
+ }
+ }
+
+}
+
+inline void TheoryArrays::queueExtLemma(TNode a, TNode b) {
+ Assert(a.getType().isArray() && b.getType().isArray());
+
+ d_extQueue.insert(make_pair(a,b));
+}
+
+void TheoryArrays::queueRowLemma(TNode a, TNode b, TNode i, TNode j) {
+ Assert(a.getType().isArray() && b.getType().isArray());
+//if(!isRedundantInContext(a,b,i,j)) {
+ d_RowQueue.insert(make_quad(a, b, i, j));
+}
+
+/**
+* Adds a new Ext lemma of the form
+* a = b OR a[k]!=b[k], for a new variable k
+*/
+
+inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
+ Assert(a.getType().isArray());
+ Assert(b.getType().isArray());
+
+ Debug("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
+ Debug("arrays-cle")<<" and "<<b<<" \n";
+
+
+ if( d_extAlreadyAdded.count(make_pair(a, b)) == 0
+ && d_extAlreadyAdded.count(make_pair(b, a)) == 0) {
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node k = nm->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 "<<lem<<"\n";
+ d_extAlreadyAdded.insert(make_pair(a,b));
+ d_out->lemma(lem);
+ ++d_numExt;
+ return;
+ }
+ Debug("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
+
+}
+
** 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.
**/
#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 <iostream>
+#include <map>
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<CongruenceChannel, CONGRUENCE_OPERATORS_1
+ (kind::SELECT)> d_cc;
+
+ /**
+ * Union find for storing the equalities.
+ */
+
+ UnionFind<Node, NodeHashFunction> d_unionFind;
+
+ Backtracker<TNode> 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<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc;
+ typedef context::CDMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
+ typedef context::CDMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
+
+
+ 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;
+
+ void checkPropagations(TNode a, TNode b);
+
+ /** List of all atoms the SAT solver knows about and are candidates for
+ * propagation. */
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms;
+
+ /** List of disequalities needed to construct explanations for propagated
+ * row lemmas */
+
+ context::CDMap<TNode, std::pair<TNode, TNode>, 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<TNode, TNode, TNode, TNode > > QuadCDList;
+
+
+ /**
+ * Ext lemma workslist that stores extensionality lemmas that still need to be added
+ */
+ std::hash_set<std::pair<TNode, TNode>, 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<quad<TNode, TNode, TNode, TNode>, 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<std::pair<TNode, TNode>, 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<quad<TNode, TNode, TNode, TNode>, 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 "<<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);
+
+ 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 "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
+ return true;
+ }
+ }
+ 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);
+ }
+ }
+
+ 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);
+ }
+ }
+
+ /** 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 "<<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
+ Debug("arrays-preregister")<<"atom "<<n<<"\n";
+ d_atoms.insert(n);
+ // add to proper equality lists
+ addEq(n);
+ break;
+ case kind::SELECT:
+ //Debug("arrays-preregister")<<"at level "<<getContext()->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 "<<n<<"\n";
+ //}
+
+ void presolve() {
+ Debug("arrays")<<"Presolving \n";
+ d_donePreregister = true;
+ }
void addSharedTerm(TNode t);
void notifyEq(TNode lhs, TNode rhs);
void check(Effort e);
- //void propagate(Effort e) { }
- void explain(TNode n) { }
+
+ void propagate(Effort e) {
+
+ Debug("arrays-prop")<<"Propagating \n";
+
+ 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);
+ Debug("arrays-prop")<<"value of "<<eq<<" ";
+ Debug("arrays-prop")<<d_valuation.getSatValue(eq);
+ if(find(eq[0]) == find(eq[1])) {
+ Debug("arrays-prop")<<" eq \n";
+ ++d_numProp;
+ }
+ }
+ */
+
+ }
+ void explain(TNode n);
+
Node getValue(TNode n);
void shutdown() { }
std::string identify() const { return std::string("TheoryArrays"); }
+
};/* 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 */
public:
- static inline RewriteResponse postRewrite(TNode node) {
+ static RewriteResponse postRewrite(TNode node) {
+ Debug("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
+ if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+ if(node[0] == node[1]) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->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);
}
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#include "theory/arrays/union_find.h"
+#include "util/Assert.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+template <class NodeType, class NodeHash>
+void UnionFind<NodeType, NodeHash>::notify() {
+ Trace("arraysuf") << "arraysUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl;
+ while(d_offset < d_trace.size()) {
+ pair<TNode, TNode> 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<Node, NodeHashFunction>::notify();
+
+template void UnionFind<TNode, TNodeHashFunction>::notify();
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 <utility>
+#include <vector>
+#include <ext/hash_map>
+
+#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 NodeType, class NodeHash>
+class UnionFind : context::ContextNotifyObj {
+ /** Our underlying map type. */
+ typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> 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<std::pair<TNode, TNode> > d_trace;
+
+ /** Our current offset in the d_trace stack (context-dependent). */
+ context::CDO<size_t> 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 <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::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 <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::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<TNode, TNode> pr = *i;
+ // our iterator is invalidated by the recursive call to find(),
+ // since it mutates the map
+ TNode p = find(pr.second);
+ if(p == pr.second) {
+ return p;
+ }
+ 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 <class NodeType, class NodeHash>
+inline void UnionFind<NodeType, NodeHash>::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 */
// 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()) */
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);
// 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;
}
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 <class TheoryClass>
* @param node the assertion
*/
inline void assertFact(TNode node) {
- Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+ Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl<<d_logic<<std::endl;
// Mark it as asserted in this context
//
// Again, equality is a special case
if (atom.getKind() == kind::EQUAL) {
- theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]);
- Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl;
- d_theoryTable[theoryLHS]->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;
// 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;
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);
}
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);
StatisticsRegistry::unregisterStat(&d_statAugLemma);
StatisticsRegistry::unregisterStat(&d_statExplanation);
}
- };
+ };/* class TheoryEngine::Statistics */
Statistics d_statistics;
};/* class TheoryEngine */
libutil_la_SOURCES = \
Assert.h \
Assert.cpp \
+ backtrackable.h \
Makefile.am \
Makefile.in \
congruence_closure.h \
dynamic_array.h \
language.h \
language.cpp \
- triple.h \
+ ntuple.h \
recursion_breaker.h \
subrange_bound.h \
cardinality.h \
--- /dev/null
+/*! \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 <cstdlib>
+#include <vector>
+#include "context/cdo.h"
+
+namespace CVC4{
+
+template <class T> class List;
+template <class T> class List_iterator;
+template <class T> class Backtracker;
+
+template <class T>
+class ListNode{
+private:
+ T data;
+ ListNode<T>* next;
+
+ bool empty;
+ ListNode(const T& t, ListNode<T>* n, bool e = false) : data(t), next(n), empty(e) {}
+ ~ListNode() {
+ // maybe set to NULL
+ delete next;
+ }
+
+ friend class List<T>;
+ friend class List_iterator<T>;
+}; /*class ListNode */
+
+template <class T>
+class List_iterator: public std::iterator <std::forward_iterator_tag, T> {
+ friend class List<T>;
+
+public:
+ const T& operator*();
+ List_iterator<T>& operator++();
+ List_iterator<T> operator++(int);
+ bool operator!=(const List_iterator<T> & other) const;
+private:
+ const ListNode<T>* pointee;
+ List_iterator(const ListNode<T>* p) : pointee(p) {}
+
+}; /* class List_iterator */
+
+template <class T> const T& List_iterator<T>::operator*() {
+ return pointee->data;
+}
+
+template <class T> List_iterator<T>& List_iterator<T>::operator++() {
+ Assert(pointee != NULL);
+ pointee = pointee->next;
+ while(pointee != NULL && pointee->empty ) {
+ pointee = pointee->next;
+ }
+ return *this;
+}
+
+template <class T> List_iterator<T> List_iterator<T>::operator++(int) {
+ List_iterator<T> it = *this;
+ ++*this;
+ return it;
+}
+
+template <class T> bool List_iterator<T>::operator!=(const List_iterator<T>& 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<TNode> should store pointers!
+template <class T> class List {
+ ListNode<T>* head;
+ ListNode<T>* tail;
+ ListNode<T>* ptr_to_head;
+ bool uninitialized;
+ Backtracker<T>* bck;
+ List (const List&) {}
+public:
+ List(Backtracker<T>* b) : ptr_to_head(NULL), uninitialized(true), bck(b) {
+ head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>*));
+ head->next = NULL;
+ head->empty = true;
+ }
+ ~List() {delete head;}
+ bool empty() {
+ bck->checkConsistency();
+ return head == NULL;
+ }
+ void append(const T& d);
+ //typedef List_iterator<T> iterator;
+ typedef List_iterator<T> const_iterator;
+
+ const_iterator begin() {
+ bck->checkConsistency();
+ if(head->empty) {
+ ListNode<T>* 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<T>(temp);
+ }
+ return List_iterator<T>(head);
+ }
+
+ const_iterator end() {
+ bck->checkConsistency();
+ return List_iterator<T>(NULL);
+ }
+ void concat(List<T>* other);
+ void unconcat(List<T>* other);
+}; /* class List */
+
+template <class T>
+void List<T>::append (const T& d) {
+ bck->checkConsistency();
+
+ if(uninitialized) {
+ new(head)ListNode<T> (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<T>* new_node = new ListNode<T>(d, head);
+ head = new_node;
+ }
+
+ if(ptr_to_head != NULL) {
+ ptr_to_head->next = head;
+ }
+}
+
+template <class T>
+void List<T>::concat (List<T>* 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 <class T>
+void List<T>::unconcat(List<T>* 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 T> class Backtracker {
+ friend class List<T>;
+ std::vector<std::pair<List<T>*,List<T>*> > undo_stack;
+
+ int curr_level;
+ context::CDO<int> pop_level;
+
+ void checkConsistency();
+ void notifyConcat(List<T>* a, List<T>* b);
+public:
+ Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {}
+ ~Backtracker() {}
+
+}; /*class Backtrackable */
+
+template <class T> void Backtracker<T>::notifyConcat(List<T>* a, List<T>* b) {
+ curr_level++;
+ pop_level.set(pop_level.get()+1);
+ undo_stack.push_back( std::make_pair(a, b));
+}
+
+template <class T> void Backtracker<T>::checkConsistency() {
+ if( curr_level == pop_level || pop_level == -1) {
+ return;
+ }
+ Assert(curr_level > pop_level);
+
+ while (curr_level > pop_level) {
+ curr_level--;
+ List<T>* l1 = undo_stack[curr_level].first;
+ List<T>* 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 */
--- /dev/null
+/********************* */
+/*! \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 T1, class T2, class T3>
+class triple {
+public:
+ T1 first;
+ T2 second;
+ T3 third;
+};/* class triple<> */
+
+template <class T1, class T2, class T3>
+inline triple<T1, T2, T3>
+make_triple(const T1& t1, const T2& t2, const T3& t3) {
+ return triple<T1, T2, T3>(t1, t2, t3);
+}/* make_triple() */
+
+template <class T1, class T2, class T3, class T4>
+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 <class T1, class T2, class T3, class T4>
+bool operator==(const quad<T1,T2,T3,T4>& x,
+ const quad<T1,T2,T3,T4>& y) {
+ return (x.first==y.first && x.second==y.second &&
+ x.third == y.third && x.fourth==y.fourth);
+}
+
+template <class T1, class T2, class T3, class T4>
+bool operator<(const quad<T1,T2,T3,T4>& x,
+ const quad<T1,T2,T3,T4>& 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 <class T1, class T2, class T3, class T4>
+inline quad<T1, T2, T3, T4>
+make_quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) {
+ return quad<T1, T2, T3, T4>(t1, t2, t3, t4);
+}/* make_quad() */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__NTUPLE_H */
};/* class IntStat */
+template <class T>
+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),
+++ /dev/null
-/********************* */
-/*! \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 T1, class T2, class T3>
-class triple {
-public:
- T1 first;
- T2 second;
- T3 third;
-};
-
-template <class T1, class T2, class T3>
-inline triple<T1, T2, T3>
-make_triple(const T1& t1, const T2& t2, const T3& t3) {
- return triple<T1, T2, T3>(t1, t2, t3);
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__TRIPLE_H */
blu='\e[1;34m'; \
std='\e[m'; \
}
-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:
-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
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/arrays
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
--- /dev/null
+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:
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
projects / cvc5.git / commitdiff