From d5a9c8b28a0bda8ca340848aaa9fa95d17ef0df2 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 11 Jul 2011 20:00:29 +0000 Subject: [PATCH] Adding static_fact_manager --- src/theory/arrays/static_fact_manager.cpp | 172 ++++++++++++++++++++++ src/theory/arrays/static_fact_manager.h | 119 +++++++++++++++ 2 files changed, 291 insertions(+) create mode 100644 src/theory/arrays/static_fact_manager.cpp create mode 100644 src/theory/arrays/static_fact_manager.h diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp new file mode 100644 index 000000000..1e135514a --- /dev/null +++ b/src/theory/arrays/static_fact_manager.cpp @@ -0,0 +1,172 @@ +/********************* */ +/*! \file static_fact_manager.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/static_fact_manager.h" +#include "util/Assert.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arrays { + +bool StaticFactManager::areEq(TNode a, TNode b) { + return (find(a) == find(b)); +} + +bool StaticFactManager::areDiseq(TNode a, TNode b) { + Node af = find(a); + Node bf = find(b); + Node left, right; + unsigned i; + for (i = 0; i < d_diseq.size(); ++i) { + left = find(d_diseq[i][0]); + right = find(d_diseq[i][1]); + if ((left == af && right == bf) || + (left == bf && right == af)) { + return true; + } + } + return false; +} + +void StaticFactManager::addDiseq(TNode eq) { + Assert(eq.getKind() == kind::EQUAL); + d_diseq.push_back(eq); +} + +void StaticFactManager::addEq(TNode eq) { + Assert(eq.getKind() == kind::EQUAL); + Node a = find(eq[0]); + Node b = find(eq[1]); + + if( a == b) { + return; + } + + /* + * take care of the congruence closure part + */ + + // make "a" the one with shorter diseqList + // CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a); + // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); + + // if(deq_ia != d_disequalities.end()) { + // if(deq_ib == d_disequalities.end() || + // (*deq_ia).second->size() > (*deq_ib).second->size()) { + // TNode tmp = a; + // a = b; + // b = tmp; + // } + // } + // a = find(a); + // b = find(b); + + + // b becomes the canon of a + setCanon(a, b); + + // deq_ia = d_disequalities.find(a); + // map alreadyDiseqs; + // if(deq_ia != d_disequalities.end()) { + // /* + // * Collecting the disequalities of b, no need to check for conflicts + // * since the representative of b does not change and we check all the things + // * in a's class when we look at the diseq list of find(a) + // */ + + // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); + // if(deq_ib != d_disequalities.end()) { + // CTNodeListAlloc* deq = (*deq_ib).second; + // for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) { + // TNode deqn = *j; + // TNode s = deqn[0]; + // TNode t = deqn[1]; + // TNode sp = find(s); + // TNode tp = find(t); + // Assert(sp == b || tp == b); + // if(sp == b) { + // alreadyDiseqs[tp] = deqn; + // } else { + // alreadyDiseqs[sp] = deqn; + // } + // } + // } + + // /* + // * Looking for conflicts in the a disequality list. Note + // * that at this point a and b are already merged. Also has + // * the side effect that it adds them to the list of b (which + // * became the canonical representative) + // */ + + // CTNodeListAlloc* deqa = (*deq_ia).second; + // for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) { + // TNode deqn = (*i); + // Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF); + // TNode s = deqn[0]; + // TNode t = deqn[1]; + // TNode sp = find(s); + // TNode tp = find(t); + + // if(find(s) == find(t)) { + // d_conflict = deqn; + // return; + // } + // Assert( sp == b || tp == b); + + // // make sure not to add duplicates + + // if(sp == b) { + // if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { + // appendToDiseqList(b, deqn); + // alreadyDiseqs[tp] = deqn; + // } + // } else { + // if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { + // appendToDiseqList(b, deqn); + // alreadyDiseqs[sp] = deqn; + // } + // } + + // } + // } + + // // TODO: check for equality propagations + // // a and b are find(a) and find(b) here + // checkPropagations(a,b); + + // if(a.getType().isArray()) { + // checkRowLemmas(a,b); + // checkRowLemmas(b,a); + // // note the change in order, merge info adds the list of + // // the 2nd argument to the first + // d_infoMap.mergeInfo(b, a); + // } +} + + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h new file mode 100644 index 000000000..d2dfc5f2d --- /dev/null +++ b/src/theory/arrays/static_fact_manager.h @@ -0,0 +1,119 @@ +/********************* */ +/*! \file static_fact_manager.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__STATIC_FACT_MANAGER_H +#define __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H + +#include +#include +#include + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + + class StaticFactManager { + /** Our underlying map type. */ + typedef __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; + std::vector d_diseq; + +public: + StaticFactManager() {} + ~StaticFactManager() 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); + + bool areEq(TNode a, TNode b); + bool areDiseq(TNode a, TNode b); + void addDiseq(TNode eq); + void addEq(TNode eq); + +};/* class StaticFactManager<> */ + +inline TNode StaticFactManager::debugFind(TNode n) const { + typename MapType::const_iterator i = d_map.find(n); + if(i == d_map.end()) { + return n; + } else { + return debugFind((*i).second); + } +} + +inline TNode StaticFactManager::find(TNode n) { + Trace("arraysuf") << "arraysUF find of " << n << std::endl; + 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; + } + pr.second = p; + d_map.insert(pr); + return p; + } +} + +inline void StaticFactManager::setCanon(TNode n, TNode newParent) { + Assert(d_map.find(n) == d_map.end()); + Assert(d_map.find(newParent) == d_map.end()); + if(n != newParent) { + d_map[n] = newParent; + } +} + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /*__CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */ -- 2.30.2