diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 94 | ||||
-rw-r--r-- | src/util/ite_removal.h | 44 | ||||
-rw-r--r-- | src/util/options.cpp | 16 | ||||
-rw-r--r-- | src/util/options.h | 19 |
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) << "]"; |