--- /dev/null
+/********************* */
+/*! \file trans_closure.cpp
+ ** \verbatim
+ ** Original author: barrett
+ ** 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 The transitive closure module implementation
+ **
+ ** Implementation file for TransitiveClosure class.
+ **/
+
+
+#include "util/trans_closure.h"
+
+
+using namespace std;
+
+
+namespace CVC4 {
+
+
+TransitiveClosure::~TransitiveClosure() {
+ unsigned i;
+ for (i = 0; i < adjMatrix.size(); ++i) {
+ adjMatrix[i]->deleteSelf();
+ }
+}
+
+
+bool TransitiveClosure::addEdge(unsigned i, unsigned j)
+{
+ if (adjMatrix.size() > j && adjMatrix[j]->read(i)) {
+ return false;
+ }
+ while (i >= adjMatrix.size()) {
+ adjMatrix.push_back(new (true) CDBV(d_context));
+ }
+ adjMatrix[i]->write(j);
+ unsigned k;
+ for (k = 0; k < adjMatrix.size(); ++k) {
+ if (adjMatrix[k]->read(i)) {
+ adjMatrix[k]->write(j);
+ adjMatrix[k]->merge(adjMatrix[j]);
+ }
+ }
+ return true;
+}
+
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file transitive_closure.h
+ ** \verbatim
+ ** Original author: barrett
+ ** 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 The transitive closure module
+ **
+ ** The transitive closure module.
+ **/
+
+#ifndef __CVC4__UTIL__TRANSITIVE_CLOSURE_H
+#define __CVC4__UTIL__TRANSITIVE_CLOSURE_H
+
+#include "context/context.h"
+
+namespace CVC4 {
+
+/*
+ * Implements context-dependent variable-sized boolean vector
+ */
+class CDBV :public context::ContextObj {
+ uint64_t d_data;
+ CDBV* d_next;
+
+ CDBV(const CDBV& cdbv) : ContextObj(cdbv), d_data(cdbv.d_data), d_next(cdbv.d_next) {}
+
+ /**
+ * operator= for CDBV is private to ensure CDBV object is not copied.
+ */
+ CDBV& operator=(const CDBV& cdbv);
+
+protected:
+ context::ContextObj* save(context::ContextMemoryManager* pCMM) {
+ return new(pCMM) CDBV(*this);
+ }
+
+ void restore(context::ContextObj* pContextObj) {
+ d_data = ((CDBV*) pContextObj)->d_data;
+ }
+
+ uint64_t data() { return d_data; }
+
+ CDBV* next() { return d_next; }
+
+public:
+ CDBV(context::Context* context) :
+ ContextObj(context), d_data(0), d_next(NULL)
+ {}
+
+ ~CDBV() {
+ if (d_next != NULL) {
+ d_next->deleteSelf();
+ }
+ destroy();
+ }
+
+ bool read(unsigned index) {
+ if (index < 64) return (d_data & (unsigned(1) << index)) != 0;
+ else if (d_next == NULL) return false;
+ else return d_next->read(index - 64);
+ }
+
+ void write(unsigned index) {
+ if (index < 64) {
+ unsigned mask = unsigned(1) << index;
+ if ((d_data & mask) != 0) return;
+ makeCurrent();
+ d_data = d_data | mask;
+ }
+ else if (d_next != NULL) {
+ d_next->write(index - 64);
+ }
+ else {
+ makeCurrent();
+ d_next = new(true) CDBV(getContext());
+ d_next->write(index - 64);
+ }
+ }
+
+ void merge(CDBV* pcdbv) {
+ d_data = d_data | pcdbv->data();
+ if (d_next != NULL && pcdbv->next() != NULL) {
+ d_next->merge(pcdbv->next());
+ }
+ }
+
+};
+
+
+/**
+ * Transitive closure module for CVC4.
+ *
+ */
+class TransitiveClosure {
+ context::Context* d_context;
+ std::vector<CDBV* > adjMatrix;
+
+public:
+ TransitiveClosure(context::Context* context) : d_context(context) {}
+ ~TransitiveClosure();
+
+ /* Add an edge from node i to node j. Return true if successful, false if this edge would create a cycle */
+ bool addEdge(unsigned i, unsigned j);
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */
--- /dev/null
+/********************* */
+/*! \file trans_closure_black.h
+ ** \verbatim
+ ** Original author: barrett
+ ** 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 Black box testing of CVC4::TransitiveClosure.
+ **
+ ** Black box testing of CVC4::TransitiveClosure.
+ **/
+
+
+#include "util/trans_closure.h"
+
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
+
+
+class TransitiveClosureBlack : public CxxTest::TestSuite {
+ Context* d_context;
+ TransitiveClosure* d_tc;
+
+public:
+
+ void setUp() {
+ d_context = new Context;
+ d_tc = new TransitiveClosure(d_context);
+ }
+
+ void tearDown() {
+ try {
+ delete d_tc;
+ delete d_context;
+ } catch(Exception& e) {
+ Warning() << std::endl << e << std::endl;
+ throw;
+ }
+ }
+
+ void testSimple() {
+ //Debug.on("cc");
+ // add terms, then add equalities
+
+ bool b;
+ b = d_tc->addEdge(1,2);
+ TS_ASSERT(!b);
+
+ b = d_tc->addEdge(2,3);
+ TS_ASSERT(!b);
+
+ b = d_tc->addEdge(3,1);
+ TS_ASSERT(b);
+ }
+
+
+};/* class TransitiveClosureBlack */
projects / cvc5.git / commitdiff