From 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 2 Sep 2011 20:41:08 +0000
Subject: Merge from my post-smtcomp branch.  Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.
---
 src/util/ite_removal.cpp | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

(limited to 'src/util/ite_removal.cpp')

diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index e9c5122b3..bd5048040 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -2,7 +2,7 @@
 /*! \file ite_removal.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -11,20 +11,22 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Representation of cardinality
+ ** \brief Removal of term ITEs
  **
- ** Simple class to represent a cardinality; used by the CVC4 type system
- ** give the cardinality of sorts.
+ ** Removal of term ITEs.
  **/
 
 #include <vector>
 
 #include "util/ite_removal.h"
 #include "theory/rewriter.h"
+#include "expr/command.h"
 
 using namespace CVC4;
 using namespace std;
 
+namespace CVC4 {
+
 struct IteRewriteAttrTag {};
 typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
 
@@ -34,8 +36,7 @@ void RemoveITE::run(std::vector<Node>& output) {
   }
 }
 
-Node RemoveITE::run(TNode node, std::vector<Node>& output)
-{
+Node RemoveITE::run(TNode node, std::vector<Node>& output) {
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
@@ -54,8 +55,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output)
       // Make the skolem to represent the ITE
       Node skolem = nodeManager->mkVar(nodeType);
 
+      if(Dump.isOn("declarations")) {
+        stringstream kss;
+        kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << skolem;
+        string ks = kss.str();
+        Dump("declarations") << CommentCommand(ks + " is a variable introduced due to term-level ITE removal") << endl
+                             << DeclareFunctionCommand(ks, nodeType.toType()) << endl;
+      }
+
       // The new assertion
-      Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
+      Node newAssertion =
+        nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
+                            skolem.eqNode(node[2]));
       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 
       // Attach the skolem
@@ -91,4 +102,6 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output)
     nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
     return node;
   }
-};
+}
+
+}/* CVC4 namespace */
-- 
cgit v1.2.3