summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am4
-rw-r--r--src/util/ite_removal.cpp94
-rw-r--r--src/util/ite_removal.h44
-rw-r--r--src/util/options.cpp16
-rw-r--r--src/util/options.h19
5 files changed, 155 insertions, 22 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index dc1da0659..83200a473 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -59,7 +59,9 @@ libutil_la_SOURCES = \
trans_closure.h \
trans_closure.cpp \
boolean_simplification.h \
- boolean_simplification.cpp
+ boolean_simplification.cpp \
+ ite_removal.h \
+ ite_removal.cpp
libutil_la_LIBADD = \
@builddir@/libutilcudd.la
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
new file mode 100644
index 000000000..e9c5122b3
--- /dev/null
+++ b/src/util/ite_removal.cpp
@@ -0,0 +1,94 @@
+/********************* */
+/*! \file ite_removal.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of cardinality
+ **
+ ** Simple class to represent a cardinality; used by the CVC4 type system
+ ** give the cardinality of sorts.
+ **/
+
+#include <vector>
+
+#include "util/ite_removal.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace std;
+
+struct IteRewriteAttrTag {};
+typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
+
+void RemoveITE::run(std::vector<Node>& output) {
+ for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
+ output[i] = run(output[i], output);
+ }
+}
+
+Node RemoveITE::run(TNode node, std::vector<Node>& output)
+{
+ // Current node
+ Debug("ite") << "removeITEs(" << node << ")" << endl;
+
+ // The result may be cached already
+ Node cachedRewrite;
+ NodeManager *nodeManager = NodeManager::currentNM();
+ if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) {
+ Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
+ return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
+ }
+
+ // If an ITE replace it
+ if(node.getKind() == kind::ITE) {
+ TypeNode nodeType = node.getType();
+ if(!nodeType.isBoolean()) {
+ // Make the skolem to represent the ITE
+ Node skolem = nodeManager->mkVar(nodeType);
+
+ // The new assertion
+ 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
+ nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
+
+ // Remove ITEs from the new assertion, rewrite it and push it to the output
+ output.push_back(run(newAssertion, output));
+
+ // The representation is now the skolem
+ return skolem;
+ }
+ }
+
+ // If not an ITE, go deep
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Remove the ITEs from the children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = run(*it, output);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
+ nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
+ return cachedRewrite;
+ } else {
+ nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+ return node;
+ }
+};
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
new file mode 100644
index 000000000..b286665cc
--- /dev/null
+++ b/src/util/ite_removal.h
@@ -0,0 +1,44 @@
+/********************* */
+/*! \file ite_removal.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, 2011 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 Representation of cardinality
+ **
+ ** Simple class to represent a cardinality; used by the CVC4 type system
+ ** give the cardinality of sorts.
+ **/
+
+#pragma once
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class RemoveITE {
+
+public:
+
+ /**
+ * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions.
+ */
+ static void run(std::vector<Node>& assertions);
+
+ /**
+ * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions.
+ */
+ static Node run(TNode node, std::vector<Node>& additionalAssertions);
+
+};
+
+
+}
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 314d85718..ff028b6c6 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -69,7 +69,7 @@ Options::Options() :
memoryMap(false),
strictParsing(false),
lazyDefinitionExpansion(false),
- simplificationMode(INCREMENTAL_MODE),
+ simplificationMode(SIMPLIFICATION_MODE_BATCH),
simplificationStyle(NO_SIMPLIFICATION_STYLE),
interactive(false),
interactiveSetByUser(false),
@@ -142,19 +142,15 @@ Languages currently supported as arguments to the -L / --lang option:\n\
static const string simplificationHelp = "\
Simplification modes currently supported by the --simplification option:\n\
\n\
-batch\n\
+batch (default) \n\
+ save up all ASSERTions; run nonclausal simplification and clausal\n\
(MiniSat) propagation for all of them only after reaching a querying command\n\
(CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
\n\
-incremental (default)\n\
+incremental\n\
+ run nonclausal simplification and clausal propagation at each ASSERT\n\
(and at CHECKSAT/QUERY/SUBTYPE)\n\
\n\
-incremental-lazy-sat\n\
-+ run nonclausal simplification at each ASSERT, but delay clausification of\n\
- ASSERT until reaching a CHECKSAT/QUERY/SUBTYPE, then clausify them all\n\
-\n\
You can also specify the level of aggressiveness for the simplification\n\
(by repeating the --simplification option):\n\
\n\
@@ -454,11 +450,9 @@ throw(OptionException) {
case SIMPLIFICATION_MODE:
if(!strcmp(optarg, "batch")) {
- simplificationMode = BATCH_MODE;
+ simplificationMode = SIMPLIFICATION_MODE_BATCH;
} else if(!strcmp(optarg, "incremental")) {
- simplificationMode = INCREMENTAL_MODE;
- } else if(!strcmp(optarg, "incremental-lazy-sat")) {
- simplificationMode = INCREMENTAL_LAZY_SAT_MODE;
+ simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
} else if(!strcmp(optarg, "aggressive")) {
simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE;
} else if(!strcmp(optarg, "toplevel")) {
diff --git a/src/util/options.h b/src/util/options.h
index a5e03d21b..06ca20073 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -106,10 +106,12 @@ struct CVC4_PUBLIC Options {
/** Enumeration of simplification modes (when to simplify). */
typedef enum {
- BATCH_MODE,
- INCREMENTAL_MODE,
- INCREMENTAL_LAZY_SAT_MODE
+ /** Simplify the assertions as they come in */
+ SIMPLIFICATION_MODE_INCREMENTAL,
+ /** Simplify the assertions all together once a check is requested */
+ SIMPLIFICATION_MODE_BATCH
} SimplificationMode;
+
/** When to perform nonclausal simplifications. */
SimplificationMode simplificationMode;
@@ -241,14 +243,11 @@ inline std::ostream& operator<<(std::ostream& out,
inline std::ostream& operator<<(std::ostream& out,
Options::SimplificationMode mode) {
switch(mode) {
- case Options::BATCH_MODE:
- out << "BATCH_MODE";
- break;
- case Options::INCREMENTAL_MODE:
- out << "INCREMENTAL_MODE";
+ case Options::SIMPLIFICATION_MODE_BATCH:
+ out << "SIMPLIFICATION_MODE_BATCH";
break;
- case Options::INCREMENTAL_LAZY_SAT_MODE:
- out << "INCREMENTAL_LAZY_SAT_MODE";
+ case Options::SIMPLIFICATION_MODE_INCREMENTAL:
+ out << "SIMPLIFICATION_MODE_INCREMENTAL";
break;
default:
out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback