diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
commit | fef0f8190fc7e5f3b88b33e7574b7df1e629e80f (patch) | |
tree | dfdda739bf5008096860e19f6b9275fb2a257960 /src/expr | |
parent | 90d8205a86b698c2548108ca4db124fe9c3f738a (diff) |
Merge from nonclausal-simplification-v2 branch:
* Preprocessing-time, non-clausal, Boolean simplification round to
support "quasi-non-linear rewrites" as discussed at last few meetings.
* --simplification=none is the default for now, but we'll probably
change that to --simplification=incremental. --simplification=batch
is also a possibility. See --simplification=help for details.
* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 22 | ||||
-rw-r--r-- | src/expr/command.h | 13 | ||||
-rw-r--r-- | src/expr/node.h | 169 | ||||
-rw-r--r-- | src/expr/node_builder.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 16 | ||||
-rw-r--r-- | src/expr/type_node.h | 83 |
6 files changed, 272 insertions, 33 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index d300b27de..f416f84bb 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -279,6 +279,28 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out) const { out << " )"; } +/* class Simplify */ + +SimplifyCommand::SimplifyCommand(Expr term) : + d_term(term) { +} + +void SimplifyCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->simplify(d_term); +} + +Expr SimplifyCommand::getResult() const { + return d_result; +} + +void SimplifyCommand::printResult(std::ostream& out) const { + out << d_result << endl; +} + +void SimplifyCommand::toStream(std::ostream& out) const { + out << "Simplify( << " << d_term << " >> )"; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) : diff --git a/src/expr/command.h b/src/expr/command.h index 17736ed77..d0b72c3dd 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -164,6 +164,19 @@ public: void toStream(std::ostream& out) const; };/* class QueryCommand */ +// this is TRANSFORM in the CVC presentation language +class CVC4_PUBLIC SimplifyCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + SimplifyCommand(Expr term); + void invoke(SmtEngine* smtEngine); + Expr getResult() const; + void printResult(std::ostream& out) const; + void toStream(std::ostream& out) const; +};/* class SimplifyCommand */ + class CVC4_PUBLIC GetValueCommand : public Command { protected: Expr d_term; diff --git a/src/expr/node.h b/src/expr/node.h index a40b3fce5..9351293f8 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Reference-counted encapsulation of a pointer to node information. + ** \brief Reference-counted encapsulation of a pointer to node information ** ** Reference-counted encapsulation of a pointer to node information. **/ @@ -29,7 +29,7 @@ #include <iostream> #include <stdint.h> -#include "type.h" +#include "expr/type.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/expr.h" @@ -38,6 +38,8 @@ #include "util/output.h" #include "util/exception.h" #include "util/language.h" +#include "util/utility.h" +#include "util/hash.h" namespace CVC4 { @@ -156,6 +158,16 @@ namespace kind { template <bool ref_count> class NodeTemplate { + // for hash_maps, hash_sets.. + template <bool ref_count1> + struct HashFunction { + size_t operator()(CVC4::NodeTemplate<ref_count1> node) const { + return (size_t) node.getId(); + } + };/* struct HashFunction */ + + typedef HashFunction<false> TNodeHashFunction; + /** * The NodeValue has access to the private constructors, so that the * iterators can can create new nodes. @@ -209,6 +221,30 @@ class NodeTemplate { } } + /** + * Cache-aware, recursive version of substitute() used by the public + * member function with a similar signature. + */ + Node substitute(TNode node, TNode replacement, + std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + + /** + * Cache-aware, recursive version of substitute() used by the public + * member function with a similar signature. + */ + template <class Iterator1, class Iterator2> + Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, + Iterator2 replacementsBegin, Iterator2 replacementsEnd, + std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + + /** + * Cache-aware, recursive version of substitute() used by the public + * member function with a similar signature. + */ + template <class Iterator> + Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, + std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + public: /** Default constructor, makes a null expression. */ @@ -444,7 +480,7 @@ public: * type checking is not requested, getType() will do the minimum * amount of checking required to return a valid result. * - * @param check whether we should check the type as we compute it + * @param check whether we should check the type as we compute it * (default: false) */ TypeNode getType(bool check = false) const @@ -456,7 +492,9 @@ public: Node substitute(TNode node, TNode replacement) const; /** - * Simultaneous substitution of Nodes. + * Simultaneous substitution of Nodes. Elements in the Iterator1 + * range will be replaced by their corresponding element in the + * Iterator2 range. Both ranges should have the same size. */ template <class Iterator1, class Iterator2> Node substitute(Iterator1 nodesBegin, @@ -465,6 +503,14 @@ public: Iterator2 replacementsEnd) const; /** + * Simultaneous substitution of Nodes. Iterators should be over + * pairs (x,y) for the rewrites [x->y]. + */ + template <class Iterator> + Node substitute(Iterator substitutionsBegin, + Iterator substitutionsEnd) const; + + /** * Returns the kind of this node. * @return the kind */ @@ -1146,39 +1192,81 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const } template <bool ref_count> -Node NodeTemplate<ref_count>::substitute(TNode node, - TNode replacement) const { +inline Node +NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { + std::hash_map<TNode, TNode, TNodeHashFunction> cache; + return substitute(node, replacement, cache); +} + +template <bool ref_count> +Node +NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, + std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + // in cache? + typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + if(i != cache.end()) { + return (*i).second; + } + + // otherwise compute NodeBuilder<> nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator nb << getOperator(); } - for(TNode::const_iterator i = begin(), + for(const_iterator i = begin(), iend = end(); i != iend; ++i) { if(*i == node) { nb << replacement; } else { - (*i).substitute(node, replacement); + (*i).substitute(node, replacement, cache); } } + + // put in cache Node n = nb; + cache[*this] = n; return n; } template <bool ref_count> template <class Iterator1, class Iterator2> -Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, - Iterator1 nodesEnd, - Iterator2 replacementsBegin, - Iterator2 replacementsEnd) const { +inline Node +NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + std::hash_map<TNode, TNode, TNodeHashFunction> cache; + return substitute(nodesBegin, nodesEnd, + replacementsBegin, replacementsEnd, cache); +} + +template <bool ref_count> +template <class Iterator1, class Iterator2> +Node +NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd, + std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + // in cache? + typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + if(i != cache.end()) { + return (*i).second; + } + + // otherwise compute Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin, "Substitution iterator ranges must be equal size" ); Iterator1 j = find(nodesBegin, nodesEnd, *this); if(j != nodesEnd) { - return *(replacementsBegin + (j - nodesBegin)); + Node n = *(replacementsBegin + (j - nodesBegin)); + cache[*this] = n; + return n; } else if(getNumChildren() == 0) { + cache[*this] = *this; return *this; } else { NodeBuilder<> nb(getKind()); @@ -1186,14 +1274,65 @@ Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, // push the operator nb << getOperator(); } - for(TNode::const_iterator i = begin(), + for(const_iterator i = begin(), iend = end(); i != iend; ++i) { nb << (*i).substitute(nodesBegin, nodesEnd, - replacementsBegin, replacementsEnd); + replacementsBegin, replacementsEnd, + cache); + } + Node n = nb; + cache[*this] = n; + return n; + } +} + +template <bool ref_count> +template <class Iterator> +inline Node +NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, + Iterator substitutionsEnd) const { + std::hash_map<TNode, TNode, TNodeHashFunction> cache; + return substitute(substitutionsBegin, substitutionsEnd, cache); +} + +template <bool ref_count> +template <class Iterator> +Node +NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, + Iterator substitutionsEnd, + std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + // in cache? + typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + if(i != cache.end()) { + return (*i).second; + } + + // otherwise compute + Iterator j = find_if(substitutionsBegin, substitutionsEnd, + bind2nd(first_equal_to<typename Iterator::value_type::first_type, typename Iterator::value_type::second_type>(), *this)); + if(j != substitutionsEnd) { + Node n = (*j).second; + cache[*this] = n; + return n; + } else if(getNumChildren() == 0) { + cache[*this] = *this; + return *this; + } else { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + nb << (*i).substitute(substitutionsBegin, substitutionsEnd, cache); } Node n = nb; + cache[*this] = n; return n; } } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 68655aed9..cc7e89bc8 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1244,7 +1244,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const enabled and the current node isn't a variable or constant */ if( d_nm->getOptions()->earlyTypeChecking ) { kind::MetaKind mk = n.getMetaKind(); - if( mk != kind::metakind::VARIABLE + if( mk != kind::metakind::VARIABLE && mk != kind::metakind::CONSTANT ) { d_nm->getType(n, true); } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 7b0adaa95..a6ca39015 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -28,7 +28,15 @@ namespace CVC4 { TypeNode TypeNode::s_null( &expr::NodeValue::s_null ); TypeNode TypeNode::substitute(const TypeNode& type, - const TypeNode& replacement) const { + const TypeNode& replacement, + std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + // in cache? + std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + if(i != cache.end()) { + return (*i).second; + } + + // otherwise compute NodeBuilder<> nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator @@ -44,7 +52,11 @@ TypeNode TypeNode::substitute(const TypeNode& type, (*i).substitute(type, replacement); } } - return nb.constructTypeNode(); + + // put in cache + TypeNode tn = nb.constructTypeNode(); + cache[*this] = tn; + return tn; } Cardinality TypeNode::getCardinality() const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index b9fea939e..7f6ebd471 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -48,6 +48,17 @@ namespace expr { */ class TypeNode { +public: + + // for hash_maps, hash_sets.. + struct HashFunction { + size_t operator()(TypeNode node) const { + return (size_t) node.getId(); + } + };/* struct HashFunction */ + +private: + /** * The NodeValue has access to the private constructors, so that the * iterators can can create new types. @@ -79,6 +90,22 @@ class TypeNode { */ void assignNodeValue(expr::NodeValue* ev); + /** + * Cache-aware, recursive version of substitute() used by the public + * member function with a similar signature. + */ + TypeNode substitute(const TypeNode& type, const TypeNode& replacement, + std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + + /** + * Cache-aware, recursive version of substitute() used by the public + * member function with a similar signature. + */ + template <class Iterator1, class Iterator2> + TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd, + Iterator2 replacementsBegin, Iterator2 replacementsEnd, + std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + public: /** Default constructor, makes a null expression. */ @@ -114,16 +141,16 @@ public: /** * Substitution of TypeNodes. */ - TypeNode substitute(const TypeNode& type, const TypeNode& replacement) const; + inline TypeNode + substitute(const TypeNode& type, const TypeNode& replacement) const; /** * Simultaneous substitution of TypeNodes. */ template <class Iterator1, class Iterator2> - TypeNode substitute(Iterator1 typesBegin, - Iterator1 typesEnd, - Iterator2 replacementsBegin, - Iterator2 replacementsEnd) const; + inline TypeNode + substitute(Iterator1 typesBegin, Iterator1 typesEnd, + Iterator2 replacementsBegin, Iterator2 replacementsEnd) const; /** * Structural comparison operator for expressions. @@ -504,12 +531,7 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { return out; } -// for hash_maps, hash_sets.. -struct TypeNodeHashFunction { - size_t operator()(TypeNode node) const { - return (size_t) node.getId(); - } -};/* struct TypeNodeHashFunction */ +typedef TypeNode::HashFunction TypeNodeHashFunction; }/* CVC4 namespace */ @@ -527,17 +549,46 @@ inline TypeNode TypeNode::fromType(const Type& t) { return NodeManager::fromType(t); } +inline TypeNode +TypeNode::substitute(const TypeNode& type, + const TypeNode& replacement) const { + std::hash_map<TypeNode, TypeNode, HashFunction> cache; + return substitute(type, replacement, cache); +} + +template <class Iterator1, class Iterator2> +inline TypeNode +TypeNode::substitute(Iterator1 typesBegin, + Iterator1 typesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + std::hash_map<TypeNode, TypeNode, HashFunction> cache; + return substitute(typesBegin, typesEnd, + replacementsBegin, replacementsEnd, cache); +} + template <class Iterator1, class Iterator2> TypeNode TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, - Iterator2 replacementsEnd) const { + Iterator2 replacementsEnd, + std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + // in cache? + std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + if(i != cache.end()) { + return (*i).second; + } + + // otherwise compute Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin, "Substitution iterator ranges must be equal size" ); Iterator1 j = find(typesBegin, typesEnd, *this); if(j != typesEnd) { - return *(replacementsBegin + (j - typesBegin)); + TypeNode tn = *(replacementsBegin + (j - typesBegin)); + cache[*this] = tn; + return tn; } else if(getNumChildren() == 0) { + cache[*this] = *this; return *this; } else { NodeBuilder<> nb(getKind()); @@ -550,9 +601,11 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, i != iend; ++i) { nb << (*i).substitute(typesBegin, typesEnd, - replacementsBegin, replacementsEnd); + replacementsBegin, replacementsEnd, cache); } - return nb.constructTypeNode(); + TypeNode tn = nb.constructTypeNode(); + cache[*this] = tn; + return tn; } } |