From 1f4b954a2cc7667a56a3007fa75c125fba93ed23 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Mar 2017 14:45:21 -0600
Subject: Eliminate Boolean term conversion. Generalizes removeITE pass to
 remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as
 theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

---
 src/expr/expr_template.cpp |  2 +-
 src/expr/node.h            | 10 ----------
 src/expr/node_manager.cpp  |  7 +++++++
 src/expr/node_manager.h    |  3 +++
 4 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'src/expr')

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 43e4a7b76..dad437bc6 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -528,7 +528,7 @@ Expr Expr::iffExpr(const Expr& e) const {
          "Don't have an expression manager for this expression!");
   PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
                       "Different expression managers!");
-  return d_exprManager->mkExpr(IFF, *this, e);
+  return d_exprManager->mkExpr(EQUAL, *this, e);
 }
 
 Expr Expr::impExpr(const Expr& e) const {
diff --git a/src/expr/node.h b/src/expr/node.h
index c9bfb75a4..6dbb5aa2b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -893,8 +893,6 @@ public:
   NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
                              const NodeTemplate<ref_count3>& elsepart) const;
   template <bool ref_count2>
-  NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
-  template <bool ref_count2>
   NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
   template <bool ref_count2>
   NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
@@ -1200,14 +1198,6 @@ NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
   return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
 }
 
-template <bool ref_count>
-template <bool ref_count2>
-NodeTemplate<true>
-NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
-  assertTNodeNotExpired();
-  return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
-}
-
 template <bool ref_count>
 template <bool ref_count2>
 NodeTemplate<true>
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a9be51418..ebf78f541 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -780,6 +780,13 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
   return n;
 }
 
+Node NodeManager::mkBooleanTermVariable() {
+  Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE);
+  n.setAttribute(TypeAttr(), booleanType());
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
 Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) {
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d85ff23d5..d2b45a636 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -528,6 +528,9 @@ public:
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
+  
+  /** Create a boolean term variable. */
+  Node mkBooleanTermVariable();
 
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);
-- 
cgit v1.2.3