From 25e9c72dd689d3b621b901220794c652a3ba589a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 11 Jul 2011 03:33:14 +0000 Subject: merge from symmetry branch --- src/theory/uf/theory_uf.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/theory/uf/theory_uf.h') diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index eaab96f27..d78504dc8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -27,6 +27,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/symmetry_breaker.h" #include "context/cdo.h" #include "context/cdset.h" @@ -87,6 +88,9 @@ private: /** True node for predicates = false */ Node d_false; + /** Symmetry analyzer */ + SymmetryBreaker d_symb; + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -113,12 +117,13 @@ public: void preRegisterTerm(TNode term); void explain(TNode n); + void staticLearning(TNode in, NodeBuilder<>& learned); + void presolve(); + std::string identify() const { return "THEORY_UF"; } - void staticLearning(TNode in, NodeBuilder<>& learned); - };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ -- cgit v1.2.3