From b812decc8428d0873ac860b79c7ee5bf003bf09e Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Tue, 15 Dec 2015 13:36:08 -0800
Subject: [PATCH] Removing the build cycle for predicate.

---
 src/expr/predicate.cpp | 59 +++++++++++++++++++++++++++++++++++-------
 src/expr/predicate.h   | 24 +++++++++++------
 src/expr/type_node.cpp |  2 +-
 3 files changed, 66 insertions(+), 19 deletions(-)

diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
index b88951bf9..a4dd29592 100644
--- a/src/expr/predicate.cpp
+++ b/src/expr/predicate.cpp
@@ -25,32 +25,71 @@ using namespace std;
 
 namespace CVC4 {
 
-Predicate::Predicate(Expr e, Expr w) throw(IllegalArgumentException) : d_predicate(e), d_witness(w) {
+Predicate::Predicate(const Predicate& p)
+    : d_predicate(new Expr(p.getExpression()))
+    , d_witness(new Expr(p.getWitness()))
+{}
+
+Predicate::Predicate(const Expr& e) throw(IllegalArgumentException)
+    : d_predicate(new Expr(e))
+    , d_witness(new Expr())
+{
   CheckArgument(! e.isNull(), e, "Predicate cannot be null");
   CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
   CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
 }
 
-Predicate::operator Expr() const {
-  return d_predicate;
+Predicate::Predicate(const Expr& e, const Expr& w)
+    throw(IllegalArgumentException)
+    : d_predicate(new Expr(e))
+    , d_witness(new Expr(w))
+{
+  CheckArgument(! e.isNull(), e, "Predicate cannot be null");
+  CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
+  CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+}
+
+Predicate::~Predicate() {
+  delete d_predicate;
+  delete d_witness;
+}
+
+Predicate& Predicate::operator=(const Predicate& p){
+  (*d_predicate) = p.getExpression();
+  (*d_witness) = p.getWitness();
+  return *this;
+}
+
+
+// Predicate::operator Expr() const {
+//   return d_predicate;
+// }
+
+const Expr& Predicate::getExpression() const {
+  return *d_predicate;
+}
+
+const Expr& Predicate::getWitness() const {
+  return *d_witness;
 }
 
 bool Predicate::operator==(const Predicate& p) const {
-  return d_predicate == p.d_predicate && d_witness == p.d_witness;
+  return getExpression() == p.getExpression() &&
+      getWitness() == p.getWitness();
 }
 
-std::ostream&
-operator<<(std::ostream& out, const Predicate& p) {
-  out << p.d_predicate;
-  if(! p.d_witness.isNull()) {
-    out << " : " << p.d_witness;
+std::ostream& operator<<(std::ostream& out, const Predicate& p) {
+  out << p.getExpression();
+  const Expr& witness = p.getWitness();
+  if(! witness.isNull()) {
+    out << " : " << witness;
   }
   return out;
 }
 
 size_t PredicateHashFunction::operator()(const Predicate& p) const {
   ExprHashFunction h;
-  return h(p.d_witness) * 5039 + h(p.d_predicate);
+  return h(p.getWitness()) * 5039 + h(p.getExpression());
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/predicate.h b/src/expr/predicate.h
index cc3e8b576..669ecc29f 100644
--- a/src/expr/predicate.h
+++ b/src/expr/predicate.h
@@ -35,28 +35,36 @@ struct CVC4_PUBLIC PredicateHashFunction {
 
 }/* CVC4 namespace */
 
-// TIM: This needs to be here due to a circular dependency.
-#warning "TODO: Track down the circular dependence on expr.h."
-#include "expr/expr.h"
 
 namespace CVC4 {
+class CVC4_PUBLIC Expr;
+}/* CVC4 namespace */
+
 
+namespace CVC4 {
 class CVC4_PUBLIC Predicate {
+public:
 
-  Expr d_predicate;
-  Expr d_witness;
+  Predicate(const Expr& e) throw(IllegalArgumentException);
+  Predicate(const Expr& e, const Expr& w) throw(IllegalArgumentException);
 
-public:
+  Predicate(const Predicate& p);
+  ~Predicate();
+  Predicate& operator=(const Predicate& p);
 
-  Predicate(Expr e, Expr w = Expr()) throw(IllegalArgumentException);
+  //operator Expr() const;
 
-  operator Expr() const;
+  const Expr& getExpression() const;
+  const Expr& getWitness() const;
 
   bool operator==(const Predicate& p) const;
 
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p);
   friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
 
+private:
+  Expr* d_predicate;
+  Expr* d_witness;
 };/* class Predicate */
 
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 5319e1e98..869304c0a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -226,7 +226,7 @@ bool TypeNode::isComparableTo(TypeNode t) const {
 
 Node TypeNode::getSubtypePredicate() const {
   Assert(isPredicateSubtype());
-  return Node::fromExpr(getConst<Predicate>());
+  return Node::fromExpr(getConst<Predicate>().getExpression());
 }
 
 TypeNode TypeNode::getSubtypeParentType() const {
-- 
2.30.2