From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 30 Jun 2010 13:56:07 +0000 (+0000)
Subject: checking in CC module interface for reference.
X-Git-Tag: cvc5-1.0.0~8969
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a66af8d04cf854746f5e1b2902b1d29ba537429;p=cvc5.git

checking in CC module interface for reference.
---

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e92954340..644376f25 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -10,6 +10,7 @@ libutil_la_SOURCES = \
 	Assert.cpp \
 	Makefile.am \
 	Makefile.in \
+	congruence_closure.h \
 	debug.h \
 	decision_engine.cpp \
 	decision_engine.h \
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
new file mode 100644
index 000000000..c32bc28d3
--- /dev/null
+++ b/src/util/congruence_closure.h
@@ -0,0 +1,121 @@
+/*********************                                                        */
+/*! \file congruence_closure.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 The congruence closure module
+ **
+ ** The congruence closure module.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTIL__CONGRUENCE_CLOSURE_H
+#define __CVC4__UTIL__CONGRUENCE_CLOSURE_H
+
+#include <list>
+#include <algorithm>
+#include <utility>
+#include <ext/hash_map>
+
+#include "expr/node_manager.h"
+#include "expr/node.h"
+#include "context/cdmap.h"
+
+namespace CVC4 {
+
+/**
+ * Congruence closure module for CVC4.
+ *
+ * This is a service class for theories.  One uses a CongruenceClosure
+ * by adding a number of equalities with addEquality().
+ *
+ * OutputChannel is a template argument (it's probably a thin layer,
+ * and we want to avoid a virtual call hierarchy in this case, and
+ * enable aggressive inlining).  It need only implement one method,
+ * merge():
+ *
+ *   class MyOutputChannel {
+ *   public:
+ *     void merge(TNode a, TNode b) {
+ *       // CongruenceClosure is notifying us that a is now the EC
+ *       // representative for b in this context.  After a pop a will
+ *       // be its own representative again.
+ *     }
+ *   };
+ */
+template <class OutputChannel>
+class CongruenceClosure {
+  /** The output channel */
+  OutputChannel* d_out;
+
+public:
+  /** Construct a congruence closure module instance */
+  CongruenceClosure(context::Context* ctxt, OutputChannel* out);
+
+  /**
+   * Add an equality literal eq into CC consideration.  This is the
+   * only input to the congruence closure module.
+   */
+  void addEquality(TNode eq);
+
+  /**
+   * Inquire whether two expressions are congruent.
+   */
+  bool areCongruent(TNode a, TNode b) throw(AssertionException);
+
+  /**
+   * Find the EC representative for a term t
+   */
+  TNode find(TNode t) throw(AssertionException);
+
+  /**
+   * Request an explanation for why a and b are in the same EC.
+   * Throws a CongruenceClosureException if they aren't in the same
+   * EC.
+   */
+  Node explain(TNode a, TNode b)
+    throw(CongruenceClosureException, AssertionException);
+
+  /**
+   * Request an explanation for why the lhs and rhs of this equality
+   * are in the same EC.  Throws a CongruenceClosureException if they
+   * aren't in the same EC.
+   */
+  Node explain(TNode eq)
+    throw(CongruenceClosureException, AssertionException);
+
+private:
+
+  /**
+   * Internal propagation of information.
+   */
+  void propagate();
+
+  /**
+   * Internal lookup mapping.
+   */
+  TNode lookup(TNode a);
+
+  /**
+   * Internal lookup mapping.
+   */
+  void setLookup(TNode a, TNode b);
+
+  /**
+   * Internal normalization.
+   */
+  Node normalize(TNode t);
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UTIL__CONGRUENCE_CLOSURE_H */