diff options
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/congruence_closure.h | 121 |
2 files changed, 122 insertions, 0 deletions
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 */ |