diff options
48 files changed, 2089 insertions, 209 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; } } diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index c9aba5952..1e26699ec 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -71,11 +71,13 @@ # define CVC4_NORETURN __attribute__ ((__noreturn__)) # define CVC4_CONST_FUNCTION __attribute__ ((__const__)) # define CVC4_PURE_FUNCTION __attribute__ ((__pure__)) +# define CVC4_WARN_UNUSED_RESULT __attribute__ ((__warn_unused_result__)) #else /* ! __GNUC__ */ # define CVC4_UNUSED # define CVC4_NORETURN # define CVC4_CONST_FUNCTION # define CVC4_PURE_FUNCTION +# define CVC4_WARN_UNUSED_RESULT #endif /* __GNUC__ */ #define EXPECT_TRUE(x) __builtin_expect( (x), true ) diff --git a/src/main/main.cpp b/src/main/main.cpp index 23e6cd2ea..9cb963d5c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Main driver for CVC4 executable. + ** \brief Main driver for CVC4 executable ** ** Main driver for CVC4 executable. **/ diff --git a/src/main/main.h b/src/main/main.h index b2e6e401b..e472b43f1 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -5,13 +5,13 @@ ** Major contributors: none ** Minor contributors (to current version): dejan, barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 Header for main CVC4 driver. + ** \brief Header for main CVC4 driver ** ** Header for main CVC4 driver. **/ @@ -28,7 +28,6 @@ #define __CVC4__MAIN__MAIN_H namespace CVC4 { - namespace main { /** Full argv[0] */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index fce785cc7..b3c253dab 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -676,7 +676,7 @@ mainCommand[CVC4::Command*& cmd] ) | TRANSFORM_TOK formula[f] - { UNSUPPORTED("TRANSFORM command"); } + { cmd = new SimplifyCommand(f); } | PRINT_TOK formula[f] { UNSUPPORTED("PRINT command"); } @@ -1428,6 +1428,9 @@ postfixTerm[CVC4::Expr& f] } /* record / tuple select */ + // FIXME - clash in lexer between tuple-select and real; can + // resolve with syntactic predicate in ANTLR 3.3, but broken in + // 3.2 ? /*| DOT ( identifier[id,CHECK_NONE,SYM_VARIABLE] { UNSUPPORTED("record select not implemented yet"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 3f7eb58c0..0d5f367ad 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -101,7 +101,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::NOT: out << "not "; break; case kind::AND: out << "and "; break; case kind::IFF: out << "iff "; break; - case kind::IMPLIES: out << "implies "; break; + case kind::IMPLIES: out << "=> "; break; case kind::OR: out << "or "; break; case kind::XOR: out << "xor "; break; case kind::ITE: out << "ite "; break; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b01260815..e99c20254 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -11,13 +11,14 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief The main entry point into the CVC4 library's SMT interface. + ** \brief The main entry point into the CVC4 library's SMT interface ** ** The main entry point into the CVC4 library's SMT interface. **/ #include <vector> #include <string> +#include <utility> #include <sstream> #include <ext/hash_map> @@ -33,11 +34,13 @@ #include "smt/no_such_function_exception.h" #include "smt/smt_engine.h" #include "theory/theory_engine.h" +#include "util/boolean_simplification.h" #include "util/configuration.h" #include "util/exception.h" #include "util/options.h" #include "util/output.h" #include "util/hash.h" +#include "theory/substitutions.h" #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" @@ -48,7 +51,6 @@ #include "theory/bv/theory_bv.h" #include "theory/datatypes/theory_datatypes.h" - using namespace std; using namespace CVC4; using namespace CVC4::smt; @@ -96,27 +98,66 @@ public: * of method calls. */ class SmtEnginePrivate { + SmtEngine& d_smt; + + vector<Node> d_assertionsToSimplify; + vector<Node> d_assertionsToPushToSat; + + theory::Substitutions d_topLevelSubstitutions; + + /** + * Adjust the currently "withheld" assertions for the current + * Options scope's SimplificationMode if purge is false, or push + * them all out to the prop layer if purge is true. + */ + void adjustAssertions(bool purge = false); + public: + SmtEnginePrivate(SmtEngine& smt) : d_smt(smt) { } + + /** + * Push withheld assertions out to the propositional layer, if any. + */ + void pushAssertions() { + Trace("smt") << "SMT pushing all withheld assertions" << endl; + + adjustAssertions(true); + Assert(d_assertionsToSimplify.empty()); + Assert(d_assertionsToPushToSat.empty()); + + Trace("smt") << "SMT done pushing all withheld assertions" << endl; + } + /** - * Pre-process a Node. This is expected to be highly-variable, - * with a lot of "source-level configurability" to add multiple - * passes over the Node. + * Perform non-clausal simplification of a Node. This involves + * Theory implementations, but does NOT involve the SAT solver in + * any way. */ - static Node preprocess(SmtEngine& smt, TNode n) + Node simplify(TNode n, bool noPersist = false) throw(NoSuchFunctionException, AssertionException); /** - * Adds a formula to the current context. + * Perform preprocessing of a Node. This involves ITE removal and + * Theory-specific rewriting, but NO action by the SAT solver. */ - static void addFormula(SmtEngine& smt, TNode n) + Node preprocess(TNode n) + throw(AssertionException); + + /** + * Adds a formula to the current context. Action here depends on + * the SimplificationMode (in the current Options scope); the + * formula might be pushed out to the propositional layer + * immediately, or it might be simplified and kept, or it might not + * even be simplified. + */ + void addFormula(TNode n) throw(NoSuchFunctionException, AssertionException); /** * Expand definitions in n. */ - static Node expandDefinitions(SmtEngine& smt, TNode n, - hash_map<TNode, Node, TNodeHashFunction>& cache) + Node expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache) throw(NoSuchFunctionException, AssertionException); };/* class SmtEnginePrivate */ @@ -129,6 +170,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_userContext(new Context()), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), + d_private(new smt::SmtEnginePrivate(*this)), d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_staticLearningTime("smt::SmtEngine::staticLearningTime") { @@ -215,7 +257,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { - Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; + Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(key == ":name" || key == ":source" || key == ":category" || @@ -241,7 +283,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) SExpr SmtEngine::getInfo(const std::string& key) const throw(BadOptionException) { - Debug("smt") << "SMT getInfo(" << key << ")" << endl; + Trace("smt") << "SMT getInfo(" << key << ")" << endl; if(key == ":all-statistics") { vector<SExpr> stats; for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin(); @@ -279,7 +321,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { - Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; + Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(key == ":print-success") { throw BadOptionException(); @@ -318,7 +360,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) SExpr SmtEngine::getOption(const std::string& key) const throw(BadOptionException) { - Debug("smt") << "SMT getOption(" << key << ")" << endl; + Trace("smt") << "SMT getOption(" << key << ")" << endl; if(key == ":print-success") { return SExpr("true"); } else if(key == ":expand-definitions") { @@ -349,7 +391,7 @@ SExpr SmtEngine::getOption(const std::string& key) const void SmtEngine::defineFunction(Expr func, const std::vector<Expr>& formals, Expr formula) { - Debug("smt") << "SMT defineFunction(" << func << ")" << endl; + Trace("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); Type formulaType = formula.getType(Options::current()->typeChecking);// type check body Type funcType = func.getType(); @@ -381,7 +423,7 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } -Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n, +Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache) throw(NoSuchFunctionException, AssertionException) { @@ -393,14 +435,15 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n, // maybe it's in the cache hash_map<TNode, Node, TNodeHashFunction>::iterator cacheHit = cache.find(n); if(cacheHit != cache.end()) { - return (*cacheHit).second; + TNode ret = (*cacheHit).second; + return ret.isNull() ? n : ret; } // otherwise expand it if(n.getKind() == kind::APPLY) { TNode func = n.getOperator(); SmtEngine::DefinedFunctionMap::const_iterator i = - smt.d_definedFunctions->find(func); + d_smt.d_definedFunctions->find(func); DefinedFunction def = (*i).second; vector<Node> formals = def.getFormals(); @@ -409,9 +452,11 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n, Debug("expand") << " func: " << func << endl; string name = func.getAttribute(expr::VarNameAttr()); Debug("expand") << " : \"" << name << "\"" << endl; - if(i == smt.d_definedFunctions->end()) { - throw NoSuchFunctionException(Expr(smt.d_exprManager, new Node(func))); - } + } + if(i == d_smt.d_definedFunctions->end()) { + throw NoSuchFunctionException(Expr(d_smt.d_exprManager, new Node(func))); + } + if(Debug.isOn("expand")) { Debug("expand") << " defn: " << def.getFunction() << endl << " ["; if(formals.size() > 0) { @@ -429,8 +474,8 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n, n.begin(), n.end()); Debug("expand") << "made : " << instance << endl; - Node expanded = expandDefinitions(smt, instance, cache); - cache[n] = expanded; + Node expanded = this->expandDefinitions(instance, cache); + cache[n] = (n == expanded ? Node::null() : expanded); return expanded; } else { Debug("expand") << "cons : " << n << endl; @@ -443,47 +488,108 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n, iend = n.end(); i != iend; ++i) { - Node expanded = expandDefinitions(smt, *i, cache); + Node expanded = this->expandDefinitions(*i, cache); Debug("expand") << "exchld: " << expanded << endl; nb << expanded; } Node node = nb; - cache[n] = node; + cache[n] = n == node ? Node::null() : node; return node; } } -Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) +Node SmtEnginePrivate::simplify(TNode in, bool noPersist) throw(NoSuchFunctionException, AssertionException) { - try { Node n; + if(!Options::current()->lazyDefinitionExpansion) { - TimerStat::CodeTimer codeTimer(smt.d_definitionExpansionTime); - //Chat() << "Expanding definitions: " << in << endl; + TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); + Chat() << "Expanding definitions: " << in << endl; Debug("expand") << "have: " << n << endl; hash_map<TNode, Node, TNodeHashFunction> cache; - n = expandDefinitions(smt, in, cache); + n = this->expandDefinitions(in, cache); Debug("expand") << "made: " << n << endl; } else { n = in; } + if(Options::current()->simplificationStyle == Options::NO_SIMPLIFICATION_STYLE) { + Chat() << "Not doing nonclausal simplification (by user request)" << endl; + } else { + if(Options::current()->simplificationStyle == Options::AGGRESSIVE_SIMPLIFICATION_STYLE) { + Unimplemented("can't do aggressive nonclausal simplification yet"); + } + Chat() << "Simplifying (non-clausally): " << n << endl; + TimerStat::CodeTimer codeTimer(d_smt.d_nonclausalSimplificationTime); + Trace("smt-simplify") << "simplifying: " << n << endl; + n = n.substitute(d_topLevelSubstitutions.begin(), d_topLevelSubstitutions.end()); + size_t oldSize = d_topLevelSubstitutions.size(); + n = d_smt.d_theoryEngine->simplify(n, d_topLevelSubstitutions); + if(n.getKind() != kind::AND && d_topLevelSubstitutions.size() > oldSize) { + Debug("smt-simplify") << "new top level substitutions not incorporated " + << "into assertion (" + << (d_topLevelSubstitutions.size() - oldSize) + << "):" << endl; + NodeBuilder<> b(kind::AND); + b << n; + for(size_t i = oldSize; i < d_topLevelSubstitutions.size(); ++i) { + Debug("smt-simplify") << " " << d_topLevelSubstitutions[i] << endl; + TNode x = d_topLevelSubstitutions[i].first; + TNode y = d_topLevelSubstitutions[i].second; + if(x.getType().isBoolean()) { + if(x.getMetaKind() == kind::metakind::CONSTANT) { + if(y.getMetaKind() == kind::metakind::CONSTANT) { + if(x == y) { + b << d_smt.d_nodeManager->mkConst(true); + } else { + b << d_smt.d_nodeManager->mkConst(false); + } + } else { + if(x.getConst<bool>()) { + b << y; + } else { + b << BooleanSimplification::negate(y); + } + } + } else if(y.getMetaKind() == kind::metakind::CONSTANT) { + if(y.getConst<bool>()) { + b << x; + } else { + b << BooleanSimplification::negate(x); + } + } else { + b << x.iffNode(y); + } + } else { + b << x.eqNode(y); + } + } + n = b; + n = BooleanSimplification::simplifyConflict(n); + } + Trace("smt-simplify") << "+++++++ got: " << n << endl; + if(noPersist) { + d_topLevelSubstitutions.resize(oldSize); + } + } + // For now, don't re-statically-learn from learned facts; this could // be useful though (e.g., theory T1 could learn something further // from something learned previously by T2). - //Chat() << "Performing static learning: " << n << endl; - TimerStat::CodeTimer codeTimer(smt.d_staticLearningTime); + Chat() << "Performing static learning: " << n << endl; + TimerStat::CodeTimer codeTimer(d_smt.d_staticLearningTime); NodeBuilder<> learned(kind::AND); learned << n; - smt.d_theoryEngine->staticLearning(n, learned); + d_smt.d_theoryEngine->staticLearning(n, learned); if(learned.getNumChildren() == 1) { learned.clear(); } else { n = learned; } - return smt.d_theoryEngine->preprocess(n); + return n; + } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any // typechecking exceptions via (e.g.) ensureBoolean(). But a @@ -498,23 +604,10 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) } } -Result SmtEngine::check() { - Debug("smt") << "SMT check()" << endl; - return d_propEngine->checkSat(); -} - -Result SmtEngine::quickCheck() { - Debug("smt") << "SMT quickCheck()" << endl; - return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK); -} - -void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) - throw(NoSuchFunctionException, AssertionException) { +Node SmtEnginePrivate::preprocess(TNode in) throw(AssertionException) { try { - Debug("smt") << "push_back assertion " << n << endl; - smt.d_haveAdditions = true; - Node node = SmtEnginePrivate::preprocess(smt, n); - smt.d_propEngine->assertFormula(node); + Chat() << "Preprocessing / rewriting: " << in << endl; + return d_smt.d_theoryEngine->preprocess(in); } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any // typechecking exceptions via (e.g.) ensureBoolean(). But a @@ -523,12 +616,84 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) // process without any error notice. stringstream ss; ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "A bad expression was produced internally. Original exception follows:\n" + << "A bad expression was produced. Original exception follows:\n" << tcep; InternalError(ss.str().c_str()); } } +Result SmtEngine::check() { + Trace("smt") << "SMT check()" << endl; + + // make sure the prop layer has all assertions + d_private->pushAssertions(); + + return d_propEngine->checkSat(); +} + +Result SmtEngine::quickCheck() { + Trace("smt") << "SMT quickCheck()" << endl; + return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK); +} + +void SmtEnginePrivate::adjustAssertions(bool purge) { + + // If the "purge" argument is true, we ignore the mode and push all + // assertions out to the propositional layer (by pretending we're in + // INCREMENTAL mode). + + Options::SimplificationMode mode = + purge ? Options::INCREMENTAL_MODE : Options::current()->simplificationMode; + + Trace("smt") << "SMT processing assertion lists in " << mode << " mode" << endl; + + if(mode == Options::BATCH_MODE) { + // nothing to do in batch mode until pushAssertions() is called + } else if(mode == Options::INCREMENTAL_LAZY_SAT_MODE || + mode == Options::INCREMENTAL_MODE) { + // make sure d_assertionsToSimplify is cleared out, and everything + // is on d_assertionsToPushToSat + + for(vector<Node>::iterator i = d_assertionsToSimplify.begin(), + i_end = d_assertionsToSimplify.end(); + i != i_end; + ++i) { + Trace("smt") << "SMT simplifying " << *i << endl; + d_assertionsToPushToSat.push_back(this->simplify(*i)); + } + d_assertionsToSimplify.clear(); + + if(mode == Options::INCREMENTAL_MODE) { + // make sure the d_assertionsToPushToSat queue is also cleared out + + for(vector<Node>::iterator i = d_assertionsToPushToSat.begin(), + i_end = d_assertionsToPushToSat.end(); + i != i_end; + ++i) { + Trace("smt") << "SMT preprocessing " << *i << endl; + Node n = this->preprocess(*i); + Trace("smt") << "SMT pushing to MiniSat " << n << endl; + + Chat() << "Pushing to MiniSat: " << n << endl; + d_smt.d_propEngine->assertFormula(n); + } + d_assertionsToPushToSat.clear(); + } + } else { + Unhandled(mode); + } +} + +void SmtEnginePrivate::addFormula(TNode n) + throw(NoSuchFunctionException, AssertionException) { + + Trace("smt") << "push_back assertion " << n << endl; + d_smt.d_haveAdditions = true; + + d_assertionsToSimplify.push_back(n); + adjustAssertions(); +} + void SmtEngine::ensureBoolean(const BoolExpr& e) { Type type = e.getType(Options::current()->typeChecking); Type boolType = d_exprManager->booleanType(); @@ -545,7 +710,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) { Result SmtEngine::checkSat(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT checkSat(" << e << ")" << endl; + Trace("smt") << "SMT checkSat(" << e << ")" << endl; if(d_queryMade && !Options::current()->incrementalSolving) { throw ModalException("Cannot make multiple queries unless " "incremental solving is enabled " @@ -554,19 +719,19 @@ Result SmtEngine::checkSat(const BoolExpr& e) { d_queryMade = true; ensureBoolean(e);// ensure expr is type-checked at this point internalPush(); - SmtEnginePrivate::addFormula(*this, e.getNode()); + d_private->addFormula(e.getNode()); Result r = check().asSatisfiabilityResult(); internalPop(); d_status = r; d_haveAdditions = false; - Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; + Trace("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::query(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT query(" << e << ")" << endl; + Trace("smt") << "SMT query(" << e << ")" << endl; if(d_queryMade && !Options::current()->incrementalSolving) { throw ModalException("Cannot make multiple queries unless " "incremental solving is enabled " @@ -575,24 +740,24 @@ Result SmtEngine::query(const BoolExpr& e) { d_queryMade = true; ensureBoolean(e);// ensure expr is type-checked at this point internalPush(); - smt::SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); + d_private->addFormula(e.getNode().notNode()); Result r = check().asValidityResult(); internalPop(); d_status = r; d_haveAdditions = false; - Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; + Trace("smt") << "SMT query(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::assertFormula(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT assertFormula(" << e << ")" << endl; + Trace("smt") << "SMT assertFormula(" << e << ")" << endl; ensureBoolean(e);// type check node if(d_assertionList != NULL) { d_assertionList->push_back(e); } - smt::SmtEnginePrivate::addFormula(*this, e.getNode()); + d_private->addFormula(e.getNode()); return quickCheck().asValidityResult(); } @@ -602,10 +767,8 @@ Expr SmtEngine::simplify(const Expr& e) { if( Options::current()->typeChecking ) { e.getType(true);// ensure expr is type-checked at this point } - Debug("smt") << "SMT simplify(" << e << ")" << endl; - // probably want to do an addFormula(), to get preprocessing, static - // learning, definition expansion... - Unimplemented(); + Trace("smt") << "SMT simplify(" << e << ")" << endl; + return BooleanSimplification::simplify(d_private->simplify(e, true)).toExpr(); } Expr SmtEngine::getValue(const Expr& e) @@ -613,7 +776,7 @@ Expr SmtEngine::getValue(const Expr& e) Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Type type = e.getType(Options::current()->typeChecking);// ensure expr is type-checked at this point - Debug("smt") << "SMT getValue(" << e << ")" << endl; + Trace("smt") << "SMT getValue(" << e << ")" << endl; if(!Options::current()->produceModels) { const char* msg = "Cannot get value when produce-models options is off."; @@ -634,9 +797,9 @@ Expr SmtEngine::getValue(const Expr& e) } Node eNode = e.getNode(); - Node n = smt::SmtEnginePrivate::preprocess(*this, eNode); + Node n = d_private->preprocess(eNode);// theory rewriting - Debug("smt") << "--- getting value of " << n << endl; + Trace("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); // type-check the result we got @@ -672,7 +835,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { } SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { - Debug("smt") << "SMT getAssignment()" << endl; + Trace("smt") << "SMT getAssignment()" << endl; if(!Options::current()->produceAssignments) { const char* msg = "Cannot get the current assignment when " @@ -700,9 +863,9 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { ++i) { Assert((*i).getType() == boolType); - Node n = smt::SmtEnginePrivate::preprocess(*this, *i); + Node n = d_private->preprocess(*i);// theory rewriting - Debug("smt") << "--- getting value of " << n << endl; + Trace("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); // type-check the result we got @@ -725,7 +888,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT getAssertions()" << endl; + Trace("smt") << "SMT getAssertions()" << endl; if(!Options::current()->interactive) { const char* msg = "Cannot query the current assertion list when not in interactive mode."; @@ -737,7 +900,7 @@ vector<Expr> SmtEngine::getAssertions() void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT push()" << endl; + Trace("smt") << "SMT push()" << endl; if(!Options::current()->incrementalSolving) { throw ModalException("Cannot push when not solving incrementally (use --incremental)"); } @@ -749,7 +912,7 @@ void SmtEngine::push() { void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT pop()" << endl; + Trace("smt") << "SMT pop()" << endl; if(!Options::current()->incrementalSolving) { throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); } @@ -766,13 +929,13 @@ void SmtEngine::pop() { } void SmtEngine::internalPop() { - Debug("smt") << "internalPop()" << endl; + Trace("smt") << "internalPop()" << endl; d_propEngine->pop(); d_userContext->pop(); } void SmtEngine::internalPush() { - Debug("smt") << "internalPush()" << endl; + Trace("smt") << "internalPush()" << endl; d_userContext->push(); d_propEngine->push(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 408db1a2f..38c064492 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -148,6 +148,11 @@ class CVC4_PUBLIC SmtEngine { Result d_status; /** + * A private utility class to SmtEngine. + */ + smt::SmtEnginePrivate* d_private; + + /** * This is called by the destructor, just before destroying the * PropEngine, TheoryEngine, and DecisionEngine (in that order). It * is important because there are destruction ordering issues @@ -260,8 +265,10 @@ public: Result checkSat(const BoolExpr& e); /** - * Simplify a formula without doing "much" work. Requires assist - * from the SAT Engine. + * Simplify a formula without doing "much" work. Does not involve + * the SAT Engine in the simplification, but uses the current + * assertions and the current partial model, if one has been + * constructed. * * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index eecf95875..d720d5136 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -23,6 +23,7 @@ libtheory_la_SOURCES = \ rewriter.h \ rewriter_attributes.h \ rewriter.cpp \ + substitutions.h \ valuation.h \ valuation.cpp diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e724312fa..7c72b5a28 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -83,6 +83,7 @@ TheoryArith::Statistics::Statistics(): d_statSlackVariables("theory::arith::SlackVariables", 0), d_statDisequalitySplits("theory::arith::DisequalitySplits", 0), d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0), + d_simplifyTimer("theory::arith::simplifyTimer"), d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), @@ -96,6 +97,7 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_statSlackVariables); StatisticsRegistry::registerStat(&d_statDisequalitySplits); StatisticsRegistry::registerStat(&d_statDisequalityConflicts); + StatisticsRegistry::registerStat(&d_simplifyTimer); StatisticsRegistry::registerStat(&d_staticLearningTimer); StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); @@ -114,6 +116,7 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statSlackVariables); StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts); + StatisticsRegistry::unregisterStat(&d_simplifyTimer); StatisticsRegistry::unregisterStat(&d_staticLearningTimer); StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); @@ -127,6 +130,12 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_restartTimer); } +Node TheoryArith::simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions) { + TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer); + Trace("simplify:arith") << "arith-simplifying: " << in << endl; + return d_valuation.rewrite(in); +} + void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 9580a6c71..1c8955d35 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -149,6 +149,7 @@ public: void presolve(); void notifyRestart(); + Node simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions); void staticLearning(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } @@ -234,6 +235,7 @@ private: IntStat d_statUserVariables, d_statSlackVariables; IntStat d_statDisequalitySplits; IntStat d_statDisequalityConflicts; + TimerStat d_simplifyTimer; TimerStat d_staticLearningTimer; IntStat d_permanentlyRemovedVariables; diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 0263ae017..524a39b69 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -10,6 +10,8 @@ libbooleans_la_SOURCES = \ theory_bool.cpp \ theory_bool_type_rules.h \ theory_bool_rewriter.h \ - theory_bool_rewriter.cpp + theory_bool_rewriter.cpp \ + circuit_propagator.h \ + circuit_propagator.cpp EXTRA_DIST = kinds diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp new file mode 100644 index 000000000..e5055c164 --- /dev/null +++ b/src/theory/booleans/circuit_propagator.cpp @@ -0,0 +1,382 @@ +/********************* */ +/*! \file circuit_propagator.cpp + ** \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 A non-clausal circuit propagator for Boolean simplification + ** + ** A non-clausal circuit propagator for Boolean simplification. + **/ + +#include "theory/booleans/circuit_propagator.h" +#include "util/utility.h" + +#include <vector> +#include <algorithm> + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace booleans { + +void CircuitPropagator::propagateBackward(TNode in, bool polarity, vector<TNode>& changed) { + if(!isPropagatedBackward(in)) { + Debug("circuit-prop") << push << "propagateBackward(" << polarity << "): " << in << endl; + setPropagatedBackward(in); + // backward rules + switch(Kind k = in.getKind()) { + case kind::AND: + if(polarity) { + // AND = TRUE: forall children c, assign(c = TRUE) + for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) { + Debug("circuit-prop") << "bAND1" << endl; + assign(*i, true, changed); + } + } else { + // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) + TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, true))); + if(holdout != in.end()) { + Debug("circuit-prop") << "bAND2" << endl; + assign(*holdout, false, changed); + } + } + break; + case kind::OR: + if(polarity) { + // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) + TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, false))); + if(holdout != in.end()) { + Debug("circuit-prop") << "bOR1" << endl; + assign(*holdout, true, changed); + } + } else { + // OR = FALSE: forall children c, assign(c = FALSE) + for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) { + Debug("circuit-prop") << "bOR2" << endl; + assign(*i, false, changed); + } + } + break; + case kind::NOT: + // NOT = b: assign(c = !b) + Debug("circuit-prop") << "bNOT" << endl; + assign(in[0], !polarity, changed); + break; + case kind::ITE: + if(isAssignedTo(in[0], true)) { + // ITE c x y = v: if c is assigned and TRUE, assign(x = v) + Debug("circuit-prop") << "bITE1" << endl; + assign(in[1], polarity, changed); + } else if(isAssignedTo(in[0], false)) { + // ITE c x y = v: if c is assigned and FALSE, assign(y = v) + Debug("circuit-prop") << "bITE2" << endl; + assign(in[2], polarity, changed); + } else if(isAssigned(in[1]) && isAssigned(in[2])) { + if(assignment(in[1]) == polarity && assignment(in[2]) != polarity) { + // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE) + Debug("circuit-prop") << "bITE3" << endl; + assign(in[0], true, changed); + } else if(assignment(in[1]) == !polarity && assignment(in[2]) == polarity) { + // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE) + Debug("circuit-prop") << "bITE4" << endl; + assign(in[0], true, changed); + } + } + break; + case kind::IFF: + if(polarity) { + // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) + if(isAssigned(in[0])) { + assign(in[1], assignment(in[0]), changed); + Debug("circuit-prop") << "bIFF1" << endl; + } else if(isAssigned(in[1])) { + Debug("circuit-prop") << "bIFF2" << endl; + assign(in[0], assignment(in[1]), changed); + } + } else { + // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment]) + if(isAssigned(in[0])) { + Debug("circuit-prop") << "bIFF3" << endl; + assign(in[1], !assignment(in[0]), changed); + } else if(isAssigned(in[1])) { + Debug("circuit-prop") << "bIFF4" << endl; + assign(in[0], !assignment(in[1]), changed); + } + } + break; + case kind::IMPLIES: + if(polarity) { + if(isAssignedTo(in[0], true)) { + // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) + Debug("circuit-prop") << "bIMPLIES1" << endl; + assign(in[1], true, changed); + } + if(isAssignedTo(in[1], false)) { + // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) + Debug("circuit-prop") << "bIMPLIES2" << endl; + assign(in[0], false, changed); + } + } else { + // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) + Debug("circuit-prop") << "bIMPLIES3" << endl; + assign(in[0], true, changed); + assign(in[1], false, changed); + } + break; + case kind::XOR: + if(polarity) { + if(isAssigned(in[0])) { + // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) + Debug("circuit-prop") << "bXOR1" << endl; + assign(in[1], !assignment(in[0]), changed); + } else if(isAssigned(in[1])) { + // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) + Debug("circuit-prop") << "bXOR2" << endl; + assign(in[0], !assignment(in[1]), changed); + } + } else { + if(isAssigned(in[0])) { + // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) + Debug("circuit-prop") << "bXOR3" << endl; + assign(in[1], assignment(in[0]), changed); + } else if(isAssigned(in[1])) { + // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) + Debug("circuit-prop") << "bXOR4" << endl; + assign(in[0], assignment(in[1]), changed); + } + } + break; + case kind::CONST_BOOLEAN: + // nothing to do + break; + default: + Unhandled(k); + } + Debug("circuit-prop") << pop; + } +} + + +void CircuitPropagator::propagateForward(TNode child, bool polarity, vector<TNode>& changed) { + if(!isPropagatedForward(child)) { + IndentedScope(Debug("circuit-prop")); + Debug("circuit-prop") << "propagateForward (" << polarity << "): " << child << endl; + std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>::const_iterator iter = d_backEdges.find(child); + if(d_backEdges.find(child) == d_backEdges.end()) { + Debug("circuit-prop") << "no backedges, must be ROOT?: " << child << endl; + return; + } + const vector<TNode>& uses = (*iter).second; + setPropagatedForward(child); + for(vector<TNode>::const_iterator useIter = uses.begin(), useIter_end = uses.end(); useIter != useIter_end; ++useIter) { + TNode in = *useIter; // this is the outer node + Debug("circuit-prop") << "considering use: " << in << endl; + IndentedScope(Debug("circuit-prop")); + // forward rules + switch(Kind k = in.getKind()) { + case kind::AND: + if(polarity) { + TNode::iterator holdout; + holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, true))); + if(holdout == in.end()) { // all children are assigned TRUE + // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE) + Debug("circuit-prop") << "fAND1" << endl; + assign(in, true, changed); + } else if(isAssignedTo(in, false)) {// the AND is FALSE + // is the holdout unique ? + TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, true))); + if(other == in.end()) { // the holdout is unique + // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE) + Debug("circuit-prop") << "fAND2" << endl; + assign(*holdout, false, changed); + } + } + } else { + // AND ...(x=FALSE)...: assign(AND = FALSE) + Debug("circuit-prop") << "fAND3" << endl; + assign(in, false, changed); + } + break; + case kind::OR: + if(polarity) { + // OR ...(x=TRUE)...: assign(OR = TRUE) + Debug("circuit-prop") << "fOR1" << endl; + assign(in, true, changed); + } else { + TNode::iterator holdout; + holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, false))); + if(holdout == in.end()) { // all children are assigned FALSE + // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE) + Debug("circuit-prop") << "fOR2" << endl; + assign(in, false, changed); + } else if(isAssignedTo(in, true)) {// the OR is TRUE + // is the holdout unique ? + TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, false))); + if(other == in.end()) { // the holdout is unique + // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE) + Debug("circuit-prop") << "fOR3" << endl; + assign(*holdout, true, changed); + } + } + } + break; + + case kind::NOT: + // NOT (x=b): assign(NOT = !b) + Debug("circuit-prop") << "fNOT" << endl; + assign(in, !polarity, changed); + break; + case kind::ITE: + if(child == in[0]) { + if(polarity) { + if(isAssigned(in[1])) { + // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) + Debug("circuit-prop") << "fITE1" << endl; + assign(in, assignment(in[1]), changed); + } + } else { + if(isAssigned(in[2])) { + // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) + Debug("circuit-prop") << "fITE2" << endl; + assign(in, assignment(in[2]), changed); + } + } + } else if(child == in[1]) { + if(isAssignedTo(in[0], true)) { + // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) + Debug("circuit-prop") << "fITE3" << endl; + assign(in, assignment(in[1]), changed); + } + } else { + Assert(child == in[2]); + if(isAssignedTo(in[0], false)) { + // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) + Debug("circuit-prop") << "fITE4" << endl; + assign(in, assignment(in[2]), changed); + } + } + break; + case kind::IFF: + if(child == in[0]) { + if(isAssigned(in[1])) { + // IFF (x=b) y: if y is assigned, assign(IFF = (x.assignment <=> y.assignment)) + Debug("circuit-prop") << "fIFF1" << endl; + assign(in, assignment(in[0]) == assignment(in[1]), changed); + } else if(isAssigned(in)) { + // IFF (x=b) y: if IFF is assigned, assign(y = (b <=> IFF.assignment)) + Debug("circuit-prop") << "fIFF2" << endl; + assign(in[1], polarity == assignment(in), changed); + } + } else { + Assert(child == in[1]); + if(isAssigned(in[0])) { + // IFF x (y=b): if x is assigned, assign(IFF = (x.assignment <=> y.assignment)) + Debug("circuit-prop") << "fIFF3" << endl; + assign(in, assignment(in[0]) == assignment(in[1]), changed); + } else if(isAssigned(in)) { + // IFF x (y=b): if IFF is assigned, assign(x = (b <=> IFF.assignment)) + Debug("circuit-prop") << "fIFF4" << endl; + assign(in[0], polarity == assignment(in), changed); + } + } + break; + case kind::IMPLIES: + if(isAssigned(in[0]) && isAssigned(in[1])) { + // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) + assign(in, !assignment(in[0]) || assignment(in[1]), changed); + Debug("circuit-prop") << "fIMPLIES1" << endl; + } else { + if(child == in[0] && assignment(in[0]) && isAssignedTo(in, true)) { + // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) + Debug("circuit-prop") << "fIMPLIES2" << endl; + assign(in[1], true, changed); + } + if(child == in[1] && !assignment(in[1]) && isAssignedTo(in, true)) { + // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) + Debug("circuit-prop") << "fIMPLIES3" << endl; + assign(in[0], false, changed); + } + // Note that IMPLIES == FALSE doesn't need any cases here + // because if that assignment has been done, we've already + // propagated all the children (in back-propagation). + } + break; + case kind::XOR: + if(isAssigned(in)) { + if(child == in[0]) { + // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) + Debug("circuit-prop") << "fXOR1" << endl; + assign(in[1], polarity ^ assignment(in), changed); + } else { + Assert(child == in[1]); + // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) + Debug("circuit-prop") << "fXOR2" << endl; + assign(in[0], polarity ^ assignment(in), changed); + } + } + if( (child == in[0] && isAssigned(in[1])) || + (child == in[1] && isAssigned(in[0])) ) { + // XOR (x=v) y [with y assigned], assign(XOR = (v ^ assignment(y)) + // XOR x (y=v) [with x assigned], assign(XOR = (assignment(x) ^ v) + Debug("circuit-prop") << "fXOR3" << endl; + assign(in, assignment(in[0]) ^ assignment(in[1]), changed); + } + break; + case kind::CONST_BOOLEAN: + InternalError("Forward-propagating a constant Boolean value makes no sense"); + default: + Unhandled(k); + } + } + } +} + + +bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) { + try { + vector<TNode> changed; + + Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL); + + Debug("circuit-prop") << "B: " << (polarity ? "" : "~") << in << endl; + propagateBackward(in, polarity, changed); + Debug("circuit-prop") << "F: " << (polarity ? "" : "~") << in << endl; + propagateForward(in, polarity, changed); + + while(!changed.empty()) { + vector<TNode> worklist; + worklist.swap(changed); + + for(vector<TNode>::iterator i = worklist.begin(), i_end = worklist.end(); i != i_end; ++i) { + if(kindToTheoryId((*i).getKind()) != THEORY_BOOL) { + if(assignment(*i)) { + newFacts.push_back(*i); + } else { + newFacts.push_back((*i).notNode()); + } + } else { + Debug("circuit-prop") << "B: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl; + propagateBackward(*i, assignment(*i), changed); + Debug("circuit-prop") << "F: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl; + propagateForward(*i, assignment(*i), changed); + } + } + } + } catch(ConflictException& ce) { + return true; + } + return false; +} + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h new file mode 100644 index 000000000..f9efc20af --- /dev/null +++ b/src/theory/booleans/circuit_propagator.h @@ -0,0 +1,206 @@ +/********************* */ +/*! \file circuit_propagator.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 A non-clausal circuit propagator for Boolean simplification + ** + ** A non-clausal circuit propagator for Boolean simplification. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H +#define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H + +#include <vector> +#include <functional> + +#include "theory/theory.h" +#include "context/context.h" +#include "util/hash.h" +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +/** + * The main purpose of the CircuitPropagator class is to maintain the + * state of the circuit for subsequent calls to propagate(), so that + * the same fact is not output twice, so that the same edge in the + * circuit isn't propagated twice, etc. + */ +class CircuitPropagator { + const std::vector<TNode>& d_atoms; + const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& d_backEdges; + + class ConflictException : Exception { + public: + ConflictException() : Exception("A conflict was found in the CircuitPropagator") { + } + };/* class ConflictException */ + + enum { + ASSIGNMENT_MASK = 1, + IS_ASSIGNED_MASK = 2, + IS_PROPAGATED_FORWARD_MASK = 4, + IS_PROPAGATED_BACKWARD_MASK = 8 + };/* enum */ + + /** + * For each Node we care about, we have a 4-bit state: + * Bit 0 (ASSIGNMENT_MASK) is set to indicate the current assignment + * Bit 1 (IS_ASSIGNED_MASK) is set if a value is assigned + * Bit 2 (IS_PROPAGATED_FORWARD) is set to indicate it's been propagated forward + * Bit 2 (IS_PROPAGATED_BACKWARD) is set to indicate it's been propagated backward + */ + std::hash_map<TNode, unsigned, TNodeHashFunction> d_state; + + /** Assign Node in circuit with the value and add it to the changed vector; note conflicts. */ + void assign(TNode n, bool b, std::vector<TNode>& changed) { + if(n.getMetaKind() == kind::metakind::CONSTANT) { + bool c = n.getConst<bool>(); + if(c != b) { + Debug("circuit-prop") << "while assigning(" << b << "): " << n + << ", constant conflict" << std::endl; + throw ConflictException(); + } else { + Debug("circuit-prop") << "assigning(" << b << "): " << n + << ", nothing to do" << std::endl; + } + return; + } + unsigned& state = d_state[n]; + if((state & IS_ASSIGNED_MASK) != 0) {// if assigned already + if(((state & ASSIGNMENT_MASK) != 0) != b) {// conflict + Debug("circuit-prop") << "while assigning(" << b << "): " << n + << ", got conflicting assignment(" << assignment(n) << "): " + << n << std::endl; + throw ConflictException(); + } else { + Debug("circuit-prop") << "already assigned(" << b << "): " << n << std::endl; + } + } else {// if unassigned + Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl; + state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0); + changed.push_back(n); + } + } + /** True iff Node is assigned in circuit (either true or false). */ + bool isAssigned(TNode n) { + return (d_state[n] & IS_ASSIGNED_MASK) != 0; + } + /** True iff Node is assigned in circuit (either true or false). */ + bool isAssigned(TNode n) const { + std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); + return i != d_state.end() && ((*i).second & IS_ASSIGNED_MASK) != 0; + } + /** True iff Node is assigned in circuit with the value given. */ + bool isAssignedTo(TNode n, bool b) { + unsigned state = d_state[n]; + return (state & IS_ASSIGNED_MASK) && + (state & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + } + /** True iff Node is assigned in circuit (either true or false). */ + bool isAssignedTo(TNode n, bool b) const { + std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); + return i != d_state.end() && + ((*i).second & IS_ASSIGNED_MASK) && + ((*i).second & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + } + /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ + bool assignment(TNode n) { + unsigned state = d_state[n]; + Assert((state & IS_ASSIGNED_MASK) != 0); + return (state & ASSIGNMENT_MASK) != 0; + } + /** Has this node already been propagated forward? */ + bool isPropagatedForward(TNode n) { + return (d_state[n] & IS_PROPAGATED_FORWARD_MASK) != 0; + } + /** Has this node already been propagated backward? */ + bool isPropagatedBackward(TNode n) { + return (d_state[n] & IS_PROPAGATED_BACKWARD_MASK) != 0; + } + /** Mark this node as already having been propagated forward. */ + void setPropagatedForward(TNode n) { + d_state[n] |= IS_PROPAGATED_FORWARD_MASK; + } + /** Mark this node as already having been propagated backward. */ + void setPropagatedBackward(TNode n) { + d_state[n] |= IS_PROPAGATED_BACKWARD_MASK; + } + + /** Predicate for use in STL functions. */ + class IsAssigned : public std::unary_function<TNode, bool> { + CircuitPropagator& d_circuit; + public: + IsAssigned(CircuitPropagator& circuit) : + d_circuit(circuit) { + } + + bool operator()(TNode in) const { + return d_circuit.isAssigned(in); + } + };/* class IsAssigned */ + + /** Predicate for use in STL functions. */ + class IsAssignedTo : public std::unary_function<TNode, bool> { + CircuitPropagator& d_circuit; + bool d_value; + public: + IsAssignedTo(CircuitPropagator& circuit, bool value) : + d_circuit(circuit), + d_value(value) { + } + + bool operator()(TNode in) const { + return d_circuit.isAssignedTo(in, d_value); + } + };/* class IsAssignedTo */ + + /** + * Propagate new information (in = polarity) forward in circuit to + * the parents of "in". + */ + void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts); + /** + * Propagate new information (in = polarity) backward in circuit to + * the children of "in". + */ + void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts); + +public: + /** + * Construct a new CircuitPropagator with the given atoms and backEdges. + */ + CircuitPropagator(const std::vector<TNode>& atoms, const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& backEdges) + : d_atoms(atoms), + d_backEdges(backEdges) { + } + + /** + * Propagate new information (in == polarity) through the circuit + * propagator. New information discovered by the propagator are put + * in the (output-only) newFacts vector. + * + * @return true iff conflict found + */ + bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT; + +};/* class CircuitPropagator */ + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 878b18478..b06972a2e 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -18,7 +18,15 @@ #include "theory/theory.h" #include "theory/booleans/theory_bool.h" +#include "theory/booleans/circuit_propagator.h" #include "theory/valuation.h" +#include "util/boolean_simplification.h" + +#include <vector> +#include <stack> +#include "util/hash.h" + +using namespace std; namespace CVC4 { namespace theory { @@ -89,6 +97,137 @@ Node TheoryBool::getValue(TNode n) { } } +static void +findAtoms(TNode in, vector<TNode>& atoms, + hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) { + Kind k = in.getKind(); + Assert(kindToTheoryId(k) == THEORY_BOOL); + + stack< pair<TNode, TNode::iterator> > trail; + hash_set<TNode, TNodeHashFunction> seen; + trail.push(make_pair(in, in.begin())); + + while(!trail.empty()) { + pair<TNode, TNode::iterator>& pr = trail.top(); + Debug("simplify") << "looking at: " << pr.first << endl; + if(pr.second == pr.first.end()) { + trail.pop(); + } else { + if(pr.second == pr.first.begin()) { + Debug("simplify") << "first visit: " << pr.first << endl; + // first time we've visited this node? + if(seen.find(pr.first) == seen.end()) { + Debug("simplify") << "+ haven't seen it yet." << endl; + seen.insert(pr.first); + } else { + Debug("simplify") << "+ saw it before." << endl; + trail.pop(); + continue; + } + } + TNode n = *pr.second++; + if(seen.find(n) == seen.end()) { + Debug("simplify") << "back edge " << n << " to " << pr.first << endl; + backEdges[n].push_back(pr.first); + Kind nk = n.getKind(); + if(kindToTheoryId(nk) == THEORY_BOOL) { + trail.push(make_pair(n, n.begin())); + } else { + Debug("simplify") << "atom: " << n << endl; + atoms.push_back(n); + } + } + } + } +} + +Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) { + const unsigned prev = outSubstitutions.size(); + + if(kindToTheoryId(in.getKind()) != THEORY_BOOL) { + Assert(in.getMetaKind() == kind::metakind::VARIABLE && + in.getType().isBoolean()); + return in; + } + + // form back edges and atoms + vector<TNode> atoms; + hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges; + Debug("simplify") << "finding atoms..." << endl << push; + findAtoms(in, atoms, backEdges); + Debug("simplify") << pop << "done finding atoms..." << endl; + + hash_map<TNode, Node, TNodeHashFunction> simplified; + + vector<Node> newFacts; + CircuitPropagator circuit(atoms, backEdges); + Debug("simplify") << "propagate..." << endl; + if(circuit.propagate(in, true, newFacts)) { + Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl; + return NodeManager::currentNM()->mkConst(false); + } + Debug("simplify") << "done w/ propagate..." << endl; + + for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) { + TNode a = *i; + if(a.getKind() == kind::NOT) { + if(a[0].getMetaKind() == kind::metakind::VARIABLE ) { + Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl; + outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false))); + } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) { + Debug("simplify") << "simplifying: " << a << endl; + simplified[a] = d_valuation.simplify(a, outSubstitutions); + Debug("simplify") << "done simplifying, got: " << simplified[a] << endl; + } + } else { + if(a.getMetaKind() == kind::metakind::VARIABLE) { + Debug("simplify") << "found bool unit " << a << "..." << endl; + outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true))); + } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) { + Debug("simplify") << "simplifying: " << a << endl; + simplified[a] = d_valuation.simplify(a, outSubstitutions); + Debug("simplify") << "done simplifying, got: " << simplified[a] << endl; + } + } + } + + Debug("simplify") << "substituting in root..." << endl; + Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end()); + Debug("simplify") << "got: " << n << endl; + if(Debug.isOn("simplify")) { + Debug("simplify") << "new substitutions:" << endl; + copy(outSubstitutions.begin() + prev, outSubstitutions.end(), + ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n")); + Debug("simplify") << "done." << endl; + } + if(outSubstitutions.size() > prev) { + NodeBuilder<> b(kind::AND); + b << n; + for(Substitutions::iterator i = outSubstitutions.begin() + prev, + i_end = outSubstitutions.end(); + i != i_end; + ++i) { + if((*i).first.getType().isBoolean()) { + if((*i).second.getMetaKind() == kind::metakind::CONSTANT) { + if((*i).second.getConst<bool>()) { + b << (*i).first; + } else { + b << BooleanSimplification::negate((*i).first); + } + } else { + b << (*i).first.iffNode((*i).second); + } + } else { + b << (*i).first.eqNode((*i).second); + } + } + n = b; + } + Debug("simplify") << "final boolean simplification returned: " << n << endl; + return n; +} + + }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index fd6d20e03..40bbd3308 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -5,13 +5,13 @@ ** Major contributors: taking ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 The theory of booleans. + ** \brief The theory of booleans ** ** The theory of booleans. **/ @@ -36,8 +36,10 @@ public: Node getValue(TNode n); + Node simplify(TNode in, Substitutions& outSubstitutions); + std::string identify() const { return std::string("TheoryBool"); } -}; +};/* class TheoryBool */ }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1c779bd79..ddfd2ab59 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,6 +26,47 @@ namespace CVC4 { namespace theory { namespace builtin { +Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) { + if(in.getKind() == kind::EQUAL) { + Node lhs = d_valuation.simplify(in[0], outSubstitutions); + Node rhs = d_valuation.simplify(in[1], outSubstitutions); + Node n = lhs.eqNode(rhs); + if( n[0].getMetaKind() == kind::metakind::VARIABLE && + n[1].getMetaKind() == kind::metakind::CONSTANT ) { + Debug("simplify:builtin") << "found new substitution! " + << n[0] << " => " << n[1] << endl; + outSubstitutions.push_back(make_pair(n[0], n[1])); + // with our substitutions we've subsumed the equality + return NodeManager::currentNM()->mkConst(true); + } else if( n[1].getMetaKind() == kind::metakind::VARIABLE && + n[0].getMetaKind() == kind::metakind::CONSTANT ) { + Debug("simplify:builtin") << "found new substitution! " + << n[1] << " => " << n[0] << endl; + outSubstitutions.push_back(make_pair(n[1], n[0])); + // with our substitutions we've subsumed the equality + return NodeManager::currentNM()->mkConst(true); + } + } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) { + TNode::iterator found = in[0].end(); + for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) { + if((*i).getMetaKind() == kind::metakind::CONSTANT) { + found = i; + break; + } + } + if(found != in[0].end()) { + for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) { + if(i != found) { + outSubstitutions.push_back(make_pair(*i, *found)); + } + } + // with our substitutions we've subsumed the (NOT (DISTINCT...)) + return NodeManager::currentNM()->mkConst(true); + } + } + return in; +} + Node TheoryBuiltin::getValue(TNode n) { switch(n.getKind()) { diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 4e62401ff..a97773dce 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,6 +31,7 @@ class TheoryBuiltin : public Theory { public: TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) : Theory(THEORY_BUILTIN, c, out, valuation) {} + Node simplify(TNode in, Substitutions& outSubstitutions); Node getValue(TNode n); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 2056c6306..45c108b72 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -131,7 +131,7 @@ struct TheoryTraits<${theory_id}> { static const bool hasPropagate = ${theory_has_propagate}; static const bool hasStaticLearning = ${theory_has_staticLearning}; static const bool hasRegisterTerm = ${theory_has_registerTerm}; - static const bool hasNotifyRestart = ${theory_has_staticLearning}; + static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; }; " diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 403ccf755..884d0af72 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -1,9 +1,20 @@ -/* - * rewriter.h - * - * Created on: Dec 13, 2010 - * Author: dejan - */ +/********************* */ +/*! \file rewriter.h + ** \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 The Rewriter class + ** + ** The Rewriter class. + **/ #pragma once @@ -13,11 +24,15 @@ namespace CVC4 { namespace theory { +/** + * Theory rewriters signal whether more rewriting is needed (or not) + * by using a member of this enumeration. See RewriteResponse, below. + */ enum RewriteStatus { REWRITE_DONE, REWRITE_AGAIN, REWRITE_AGAIN_FULL -}; +};/* enum RewriteStatus */ /** * Instances of this class serve as response codes from @@ -29,9 +44,13 @@ enum RewriteStatus { struct RewriteResponse { const RewriteStatus status; const Node node; - RewriteResponse(RewriteStatus status, Node node) : status(status), node(node) {} -}; + RewriteResponse(RewriteStatus status, Node node) : + status(status), node(node) {} +};/* struct RewriteResponse */ +/** + * The main rewriter class. All functionality is static. + */ class Rewriter { /** Returns the appropriate cache for a node */ @@ -41,21 +60,28 @@ class Rewriter { static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node); /** Sets the appropriate cache for a node */ - static void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); + static void setPreRewriteCache(theory::TheoryId theoryId, + TNode node, TNode cache); /** Sets the appropriate cache for a node */ - static void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); + static void setPostRewriteCache(theory::TheoryId theoryId, + TNode node, TNode cache); + + // disable construction of rewriters; all functionality is static + Rewriter() CVC4_UNUSED; + Rewriter(const Rewriter&) CVC4_UNUSED; public: - /** Calls the pre rewrite for the given theory */ + /** Calls the pre-rewriter for the given theory */ static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); - /** Calls the post rewrite for the given theory */ + /** Calls the post-rewriter for the given theory */ static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); /** - * Rewrites the node using theoryOf to determine which rewriter to use on the node. + * Rewrites the node using theoryOf() to determine which rewriter to + * use on the node. */ static Node rewrite(Node node); @@ -65,7 +91,7 @@ public: static Node rewriteTo(theory::TheoryId theoryId, Node node); /** - * Should be called before the rewriter get's used for the first time. + * Should be called before the rewriter gets used for the first time. */ static void init(); @@ -73,7 +99,7 @@ public: * Should be called to clean up any state. */ static void shutdown(); -}; +};/* class Rewriter */ -} // Namesapce theory -} // Namespace CVC4 +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index d33d7314e..86c2585b1 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -1,9 +1,20 @@ -/* - * rewriter_attributes.h - * - * Created on: Dec 27, 2010 - * Author: dejan - */ +/********************* */ +/*! \file rewriter_attributes.h + ** \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 Rewriter attributes + ** + ** Rewriter attributes. + **/ #pragma once @@ -79,8 +90,7 @@ struct RewriteAttibute { node.setAttribute(post_rewrite(), cache); } } -}; - -} // Namespace CVC4 -} // Namespace theory +};/* struct RewriteAttribute */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h new file mode 100644 index 000000000..32e1599ea --- /dev/null +++ b/src/theory/substitutions.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file substitutions.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 A substitution mapping for theory simplification + ** + ** A substitution mapping for theory simplification. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SUBSTITUTIONS_H +#define __CVC4__THEORY__SUBSTITUTIONS_H + +#include <utility> +#include <vector> +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +/** + * The type for the Substitutions mapping output by + * Theory::simplify(), TheoryEngine::simplify(), and + * Valuation::simplify(). This is in its own header to avoid circular + * dependences between those three. + */ +typedef std::vector< std::pair<Node, Node> > Substitutions; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */ diff --git a/src/theory/theory.h b/src/theory/theory.h index ac40c55d1..bba4c623a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/attribute.h" #include "theory/valuation.h" +#include "theory/substitutions.h" #include "theory/output_channel.h" #include "context/context.h" #include "context/cdlist.h" @@ -159,6 +160,9 @@ protected: public: + /** + * Return the ID of the theory responsible for the given type. + */ static inline TheoryId theoryOf(TypeNode typeNode) { if (typeNode.getKind() == kind::TYPE_CONSTANT) { return typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); @@ -168,10 +172,11 @@ public: } /** - * Returns the theory responsible for the node. + * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { - if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { + if (node.getMetaKind() == kind::metakind::VARIABLE || + node.getMetaKind() == kind::metakind::CONSTANT) { // Constants, variables, 0-ary constructors return theoryOf(node.getType()); } else { @@ -374,13 +379,29 @@ public: } /** - * The theory should only add (via .operator<< or .append()) to the - * "learned" builder. It is a conjunction to add to the formula at + * Statically learn from assertion "in," which has been asserted + * true at the top level. The theory should only add (via + * ::operator<< or ::append()) to the "learned" builder---it should + * *never* clear it. It is a conjunction to add to the formula at * the top-level and may contain other theories' contributions. */ virtual void staticLearning(TNode in, NodeBuilder<>& learned) { } /** + * Simplify a node in a theory-specific way. The node is a theory + * operation or its negation, or an equality between theory-typed + * terms or its negation. Add to "outSubstitutions" any + * replacements you want to make for the entire subterm; if you add + * [x,y] to the vector, the enclosing Boolean formula (call it + * "phi") will be replaced with (AND phi[x->y] (x = y)). Use + * Valuation::simplify() to simplify subterms (it maintains a cache + * and dispatches to the appropriate theory). + */ + virtual Node simplify(TNode in, Substitutions& outSubstitutions) { + return in; + } + + /** * A Theory is called with presolve exactly one time per user * check-sat. presolve() is called after preregistration, * rewriting, and Boolean propagation, (other theories' diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b4d6654b1..69220ad62 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -420,9 +420,40 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ } - // notify each theory using the statement above + // static learning for each theory using the statement above CVC4_FOR_EACH_THEORY } +Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) { + SimplifyCache::Scope cache(d_simplifyCache, in); + if(cache) { + outSubstitutions.insert(outSubstitutions.end(), + cache.get().second.begin(), + cache.get().second.end()); + return cache.get().first; + } + + size_t prevSize = outSubstitutions.size(); + + TNode atom = in.getKind() == kind::NOT ? in[0] : in; + + theory::Theory* theory = theoryOf(atom); + + Debug("simplify") << push << "simplifying " << in << " to " << theory->identify() << std::endl; + Node n = theory->simplify(in, outSubstitutions); + Debug("simplify") << "got from " << theory->identify() << " : " << n << std::endl << pop; + + atom = n.getKind() == kind::NOT ? n[0] : n; + + if(atom.getKind() == kind::EQUAL) { + theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType()); + Debug("simplify") << push << "simplifying " << n << " to " << typeTheory << std::endl; + n = d_theoryTable[typeTheory]->simplify(n, outSubstitutions); + Debug("simplify") << "got from " << d_theoryTable[typeTheory]->identify() << " : " << n << std::endl << pop; + } + + cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end()))); + return n; +} }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 19374d6db..e571c2bbd 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -22,15 +22,20 @@ #define __CVC4__THEORY_ENGINE_H #include <deque> +#include <vector> +#include <utility> #include "expr/node.h" #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/rewriter.h" +#include "theory/substitutions.h" #include "theory/valuation.h" #include "util/options.h" #include "util/stats.h" +#include "util/hash.h" +#include "util/cache.h" namespace CVC4 { @@ -69,6 +74,16 @@ class TheoryEngine { size_t d_activeTheories; /** + * The type of the simplification cache. + */ + typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache; + + /** + * A cache for simplification. + */ + SimplifyCache d_simplifyCache; + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -273,11 +288,17 @@ public: } /** - * Preprocess a node. This involves theory-specific rewriting, then - * calling preRegister() on what's left over. + * Preprocess a node. This involves ITE removal and theory-specific + * rewriting. + * * @param n the node to preprocess */ Node preprocess(TNode n); + + /** + * Preregister a Theory atom with the responsible theory (or + * theories). + */ void preRegister(TNode preprocessed); /** @@ -325,12 +346,18 @@ public: bool check(theory::Theory::Effort effort); /** - * Calls staticLearning() on all active theories, accumulating their + * Calls staticLearning() on all theories, accumulating their * combined contributions in the "learned" builder. */ void staticLearning(TNode in, NodeBuilder<>& learned); /** + * Calls simplify() on all theories, accumulating their combined + * contributions in the "outSubstitutions" vector. + */ + Node simplify(TNode in, theory::Substitutions& outSubstitutions); + + /** * Calls presolve() on all active theories and returns true * if one of the theories discovers a conflict. */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 536255c2d..604ae21e1 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -41,5 +41,13 @@ Node Valuation::getSatValue(TNode n) const{ } } +Node Valuation::simplify(TNode in, Substitutions& outSubstitutions) { + return d_engine->simplify(in, outSubstitutions); +} + +Node Valuation::rewrite(TNode in) { + return d_engine->preprocess(in); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 0c60ec5ea..d46b9aab1 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -24,6 +24,7 @@ #define __CVC4__THEORY__VALUATION_H #include "expr/node.h" +#include "theory/substitutions.h" namespace CVC4 { @@ -50,6 +51,20 @@ public: */ Node getSatValue(TNode n) const; + /** + * Simplify a node. Intended to be used by a theory's simplify() + * function to simplify subterms (TheoryEngine will cache the + * results and make sure that the request is directed to the correct + * theory). + */ + Node simplify(TNode in, Substitutions& outSubstitutions); + + /** + * Rewrite a node. Intended to be used by a theory to have the + * TheoryEngine fully rewrite a node. + */ + Node rewrite(TNode in); + };/* class Valuation */ }/* CVC4::theory namespace */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 27b9e42d2..20806464d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -51,6 +51,8 @@ libutil_la_SOURCES = \ subrange_bound.h \ cardinality.h \ cardinality.cpp \ + cache.h \ + utility.h \ trans_closure.h \ trans_closure.cpp \ boolean_simplification.h \ diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp index a154f342f..92534bfd4 100644 --- a/src/util/boolean_simplification.cpp +++ b/src/util/boolean_simplification.cpp @@ -20,7 +20,7 @@ namespace CVC4 { -void +bool BooleanSimplification::push_back_associative_commute_recursive (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) throw(AssertionException) { @@ -28,17 +28,40 @@ BooleanSimplification::push_back_associative_commute_recursive for(; i != end; ++i){ Node child = *i; if(child.getKind() == k){ - push_back_associative_commute_recursive(child, buffer, k, notK, negateNode); + if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) { + return false; + } }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ - push_back_associative_commute_recursive(child, buffer, notK, k, !negateNode); + if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) { + return false; + } }else{ if(negateNode){ - buffer.push_back(negate(child)); + if(child.getMetaKind() == kind::metakind::CONSTANT) { + if((k == kind::AND && child.getConst<bool>()) || + (k == kind::OR && !child.getConst<bool>())) { + buffer.clear(); + buffer.push_back(negate(child)); + return false; + } + } else { + buffer.push_back(negate(child)); + } }else{ - buffer.push_back(child); + if(child.getMetaKind() == kind::metakind::CONSTANT) { + if((k == kind::OR && child.getConst<bool>()) || + (k == kind::AND && !child.getConst<bool>())) { + buffer.clear(); + buffer.push_back(child); + return false; + } + } else { + buffer.push_back(child); + } } } } + return true; }/* BooleanSimplification::push_back_associative_commute_recursive() */ }/* CVC4 namespace */ diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index e938a2b38..c2da8af5b 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -39,9 +39,9 @@ class BooleanSimplification { BooleanSimplification() CVC4_UNUSED; BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED; - static void push_back_associative_commute_recursive + static bool push_back_associative_commute_recursive (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) - throw(AssertionException); + throw(AssertionException) CVC4_WARN_UNUSED_RESULT; public: @@ -80,6 +80,10 @@ public: removeDuplicates(buffer); + if(buffer.size() == 1) { + return buffer[0]; + } + NodeBuilder<> nb(kind::AND); nb.append(buffer); return nb; @@ -100,6 +104,11 @@ public: removeDuplicates(buffer); + Assert(buffer.size() > 0); + if(buffer.size() == 1) { + return buffer[0]; + } + NodeBuilder<> nb(kind::OR); nb.append(buffer); return nb; @@ -138,10 +147,14 @@ public: * @param k the kind to collapse (should equal the kind of node n) * @param notK the "negation" of kind k (e.g. OR's negation is AND), * or kind::UNDEFINED_KIND if none. + * @param negateChildren true if the children of the resulting node + * (that is, the elements in buffer) should all be negated; you want + * this if e.g. you're simplifying the (OR...) in (NOT (OR...)), + * intending to make the result an AND. */ static inline void push_back_associative_commute(Node n, std::vector<Node>& buffer, - Kind k, Kind notK) + Kind k, Kind notK, bool negateChildren = false) throw(AssertionException) { AssertArgument(buffer.empty(), buffer); AssertArgument(!n.isNull(), n); @@ -150,7 +163,13 @@ public: AssertArgument(n.getKind() == k, n, "expected node to have kind %s", kindToString(k).c_str()); - push_back_associative_commute_recursive(n, buffer, k, notK, false); + bool b CVC4_UNUSED = + push_back_associative_commute_recursive(n, buffer, k, notK, false); + + if(buffer.size() == 0) { + // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away + buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false)); + } }/* push_back_associative_commute() */ /** @@ -168,6 +187,9 @@ public: base = base[0]; polarity = !polarity; } + if(n.getMetaKind() == kind::metakind::CONSTANT) { + return NodeManager::currentNM()->mkConst(!n.getConst<bool>()); + } if(polarity){ return base.notNode(); }else{ @@ -175,6 +197,26 @@ public: } } + /** + * Simplify an OR, AND, or IMPLIES. This function is the identity + * for all other kinds. + */ + inline static Node simplify(TNode n) throw(AssertionException) { + switch(n.getKind()) { + case kind::AND: + return simplifyConflict(n); + + case kind::OR: + return simplifyClause(n); + + case kind::IMPLIES: + return simplifyHornClause(n); + + default: + return n; + } + } + };/* class BooleanSimplification */ }/* CVC4 namespace */ diff --git a/src/util/cache.h b/src/util/cache.h new file mode 100644 index 000000000..08c624d99 --- /dev/null +++ b/src/util/cache.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file cache.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 A generic Cache<> template class for use by functions that + ** walk the Node DAG and want to cache results for sub-DAGs + ** + ** A generic Cache<> template class for use by functions that walk + ** the Node DAG and want to cache results for sub-DAGs. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CACHE_H +#define __CVC4__CACHE_H + +#include <utility> +#include <functional> + +namespace CVC4 { + +/** + * A generic implementation of a cache for functions that walk the + * Node DAG performing a computation and want to cache some or all + * computations. + */ +template <class T, class U, class Hasher = std::hash<T> > +class Cache { + typedef std::hash_map<T, U, Hasher> Map; + Map d_map; + std::vector<T> d_current; + typename Map::iterator d_result; + + // disallow copy/assignment + Cache(const Cache&) CVC4_UNUSED; + Cache& operator=(const Cache&) CVC4_UNUSED; + +public: + + typedef T key_type; + typedef U value_type; + typedef Hasher hash_function; + + /** + * Makes it easy and error-free to use a Cache<> in a function. + */ + class Scope { + Cache& d_cache; + bool d_fired; + + public: + Scope(Cache<T, U, Hasher>& cache, const T& elt) throw(AssertionException) : + d_cache(cache), + d_fired(d_cache.computing(elt)) { + } + + ~Scope() { + if(!d_fired) { + d_cache();// pop stack + } + } + + operator bool() throw() { + return d_fired; + } + + const U& get() throw(AssertionException) { + Assert(d_fired, "nothing in cache"); + return d_cache.get(); + } + + U& operator()(U& computed) throw(AssertionException) { + Assert(!d_fired, "can only cache a computation once"); + d_fired = true; + return d_cache(computed); + } + const U& operator()(const U& computed) throw(AssertionException) { + Assert(!d_fired, "can only cache a computation once"); + d_fired = true; + return d_cache(computed); + } + };/* class Cache::Scope */ + + Cache() {} + + bool computing(const T& elt) { + d_result = d_map.find(elt); + bool found = (d_result != d_map.end()); + if(!found) { + d_current.push_back(elt); + } + return found; + } + + const U& get() { + Assert(d_result != d_map.end()); + return (*d_result).second; + } + + // cache nothing (just pop) + void operator()() { + d_current.pop_back(); + } + + U& operator()(U& result) { + d_map.insert(d_current.back(), result); + d_current.pop_back(); + return result; + } + const U& operator()(const U& result) { + d_map.insert(std::make_pair(d_current.back(), result)); + d_current.pop_back(); + return result; + } +};/* class Cache<> */ + + +}/* CVC4 namespace */ + +#endif /* __CVC4__CACHE_H */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 2a3f69fd6..ab52e7f93 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -109,7 +109,7 @@ void Datatype::addConstructor(const Constructor& c) { Cardinality Datatype::getCardinality() const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); - RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { return Cardinality::INTEGERS; } @@ -159,7 +159,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) { return self.getAttribute(DatatypeWellFoundedAttr()); } - RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // This *path* is cyclic, so may not be well-founded. The // datatype itself might still be well-founded, though (we'll find @@ -518,7 +518,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { return self.getAttribute(DatatypeWellFoundedAttr()); } - RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // This *path* is cyclic, sso may not be well-founded. The // constructor itself might still be well-founded, though (we'll @@ -563,7 +563,7 @@ Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) { return groundTerm; } - RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // Recursive path, we should skip and go to the next constructor; // see lengthy comments in Datatype::mkGroundTerm(). diff --git a/src/util/datatype.h b/src/util/datatype.h index 75da1405f..7d9ae6f39 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -427,6 +427,24 @@ struct CVC4_PUBLIC DatatypeHashStrategy { } };/* struct DatatypeHashStrategy */ +/** + * A hash function for Datatypes. Needed to store them in hash sets + * and hash maps. + */ +struct CVC4_PUBLIC DatatypeHashFunction { + inline size_t operator()(const Datatype& dt) const { + return StringHashFunction()(dt.getName()); + } + inline size_t operator()(const Datatype* dt) const { + return StringHashFunction()(dt->getName()); + } + inline size_t operator()(const Datatype::Constructor& dtc) const { + return StringHashFunction()(dtc.getName()); + } + inline size_t operator()(const Datatype::Constructor* dtc) const { + return StringHashFunction()(dtc->getName()); + } +};/* struct DatatypeHashFunction */ // FUNCTION DECLARATIONS FOR OUTPUT STREAMS diff --git a/src/util/options.cpp b/src/util/options.cpp index 1329a443a..dbe0f6804 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -69,6 +69,8 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), + simplificationMode(INCREMENTAL_MODE), + simplificationStyle(NO_SIMPLIFICATION_STYLE), interactive(false), interactiveSetByUser(false), segvNoSpin(false), @@ -83,7 +85,7 @@ Options::Options() : rewriteArithEqualities(false), arithPropagation(false), satRandomFreq(0.0), - satRandomSeed(91648253), //Minisat's default value + satRandomSeed(91648253),// Minisat's default value pivotRule(MINIMUM) { } @@ -102,10 +104,10 @@ static const string optionsDescription = "\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ - --verbose | -v increase verbosity (repeatable)\n\ - --quiet | -q decrease verbosity (repeatable)\n\ - --trace | -t tracing for something (e.g. --trace pushpop)\n\ - --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ + --verbose | -v increase verbosity (may be repeated)\n\ + --quiet | -q decrease verbosity (may be repeated)\n\ + --trace | -t trace something (e.g. -t pushpop), can repeat\n\ + --debug | -d debug something (e.g. -d arith), can repeat\n\ --stats give statistics on exit\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ @@ -115,8 +117,9 @@ static const string optionsDescription = "\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ - --replay file replay decisions from file\n\ - --replay-log file log decisions and propagations to file\n\ + --simplification=MODE choose simplification mode, see --simplification=help\n\ + --replay=file replay decisions from file\n\ + --replay-log=file log decisions and propagations to file\n\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ @@ -132,14 +135,42 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2 | smtlib2 SMT-LIB format 2.0\n\ "; +static const string simplificationHelp = "\ +Simplification modes currently supported by the --simplification option:\n\ +\n\ +batch\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\ ++ 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\ +toplevel (default)\n\ ++ apply toplevel simplifications (things known true/false at outer level\n\ + only)\n\ +\n\ +aggressive\n\ ++ do aggressive, local simplification across the entire formula\n\ +\n\ +none\n\ ++ do not perform nonclausal simplification\n\ +"; + string Options::getDescription() const { return optionsDescription; } void Options::printUsage(const std::string msg, std::ostream& out) { out << msg << optionsDescription << endl << flush; - // printf(usage + options.getDescription(), options.binary_name.c_str()); - // printf(usage, binary_name.c_str()); } void Options::printLanguageHelp(std::ostream& out) { @@ -155,7 +186,7 @@ void Options::printLanguageHelp(std::ostream& out) { * any collision. */ enum OptionValue { - SMTCOMP = 256, /* no clash with char options */ + SMTCOMP = 256, /* avoid clashing with char options */ STATS, SEGV_NOSPIN, PARSE_ONLY, @@ -168,6 +199,7 @@ enum OptionValue { PRINT_EXPR_TYPES, UF_THEORY, LAZY_DEFINITION_EXPANSION, + SIMPLIFICATION_MODE, INTERACTIVE, NO_INTERACTIVE, PRODUCE_MODELS, @@ -231,6 +263,7 @@ static struct option cmdlineOptions[] = { { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, { "uf" , required_argument, NULL, UF_THEORY }, { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, + { "simplification", required_argument, NULL, SIMPLIFICATION_MODE }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, PRODUCE_MODELS }, @@ -397,8 +430,8 @@ throw(OptionException) { uf_implementation = Options::MORGAN; } else if(!strcmp(optarg, "help")) { printf("UF implementations available:\n"); - printf("tim\n"); - printf("morgan\n"); + printf(" tim\n"); + printf(" morgan\n"); exit(1); } else { throw OptionException(string("unknown option for --uf: `") + @@ -411,6 +444,28 @@ throw(OptionException) { lazyDefinitionExpansion = true; break; + case SIMPLIFICATION_MODE: + if(!strcmp(optarg, "batch")) { + simplificationMode = BATCH_MODE; + } else if(!strcmp(optarg, "incremental")) { + simplificationMode = INCREMENTAL_MODE; + } else if(!strcmp(optarg, "incremental-lazy-sat")) { + simplificationMode = INCREMENTAL_LAZY_SAT_MODE; + } else if(!strcmp(optarg, "aggressive")) { + simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE; + } else if(!strcmp(optarg, "toplevel")) { + simplificationStyle = TOPLEVEL_SIMPLIFICATION_STYLE; + } else if(!strcmp(optarg, "none")) { + simplificationStyle = NO_SIMPLIFICATION_STYLE; + } else if(!strcmp(optarg, "help")) { + puts(simplificationHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --simplification: `") + + optarg + "'. Try --simplification help."); + } + break; + case INTERACTIVE: interactive = true; interactiveSetByUser = true; @@ -545,14 +600,12 @@ throw(OptionException) { printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); - case '?': - throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); - case ':': throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); + case '?': default: - throw OptionException(string("can't understand option:") + argv[optind - 1] + "'"); + throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); } } diff --git a/src/util/options.h b/src/util/options.h index be432e5a7..d9d9c8567 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -34,7 +34,7 @@ namespace CVC4 { class ExprStream; /** Class representing an option-parsing exception. */ -class OptionException : public CVC4::Exception { +class CVC4_PUBLIC OptionException : public CVC4::Exception { public: OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) { @@ -104,6 +104,25 @@ struct CVC4_PUBLIC Options { /** Should we expand function definitions lazily? */ bool lazyDefinitionExpansion; + /** Enumeration of simplification modes (when to simplify). */ + typedef enum { + BATCH_MODE, + INCREMENTAL_MODE, + INCREMENTAL_LAZY_SAT_MODE + } SimplificationMode; + /** When to perform nonclausal simplifications. */ + SimplificationMode simplificationMode; + + /** Enumeration of simplification styles (how much to simplify). */ + typedef enum { + AGGRESSIVE_SIMPLIFICATION_STYLE, + TOPLEVEL_SIMPLIFICATION_STYLE, + NO_SIMPLIFICATION_STYLE + } SimplificationStyle; + + /** Style of nonclausal simplifications to perform. */ + SimplificationStyle simplificationStyle; + /** Whether we're in interactive mode or not */ bool interactive; @@ -188,6 +207,9 @@ struct CVC4_PUBLIC Options { };/* struct Options */ inline std::ostream& operator<<(std::ostream& out, + Options::UfImplementation uf) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) { switch(uf) { case Options::TIM: @@ -203,7 +225,28 @@ inline std::ostream& operator<<(std::ostream& out, return out; } -std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule); +inline std::ostream& operator<<(std::ostream& out, + Options::SimplificationMode mode) CVC4_PUBLIC; +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"; + break; + case Options::INCREMENTAL_LAZY_SAT_MODE: + out << "INCREMENTAL_LAZY_SAT_MODE"; + break; + default: + out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/output.cpp b/src/util/output.cpp index 88628481f..29de4c360 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -31,6 +31,9 @@ ostream null_os(&null_sb); NullC nullCvc4Stream CVC4_PUBLIC; +const std::string CVC4ostream::s_tab = " "; +const int CVC4ostream::s_indentIosIndex = ios_base::xalloc(); + DebugC DebugChannel CVC4_PUBLIC (&cout); WarningC WarningChannel CVC4_PUBLIC (&cerr); MessageC MessageChannel CVC4_PUBLIC (&cout); diff --git a/src/util/output.h b/src/util/output.h index b0e210c17..6d0f27f2a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -21,6 +21,7 @@ #ifndef __CVC4__OUTPUT_H #define __CVC4__OUTPUT_H +#include <ios> #include <iostream> #include <string> #include <cstdio> @@ -59,20 +60,42 @@ extern null_streambuf null_sb; extern std::ostream null_os CVC4_PUBLIC; class CVC4_PUBLIC CVC4ostream { + static const std::string s_tab; + static const int s_indentIosIndex; + + /** The underlying ostream */ std::ostream* d_os; - // Current indentation - unsigned d_indent; + /** Are we in the first column? */ + bool d_firstColumn; - std::ostream& (*d_endl)(std::ostream&); + /** The endl manipulator (why do we need to keep this?) */ + std::ostream& (*const d_endl)(std::ostream&); public: - CVC4ostream() : d_os(NULL) {} - explicit CVC4ostream(std::ostream* os) : d_os(os), d_indent(0) { - d_endl = &std::endl; + CVC4ostream() : + d_os(NULL), + d_firstColumn(false), + d_endl(&std::endl) { + } + explicit CVC4ostream(std::ostream* os) : + d_os(os), + d_firstColumn(true), + d_endl(&std::endl) { } - void pushIndent() { d_indent ++; } - void popIndent() { if (d_indent > 0) -- d_indent; } + void pushIndent() { + if(d_os != NULL) { + ++d_os->iword(s_indentIosIndex); + } + } + void popIndent() { + if(d_os != NULL) { + long& indent = d_os->iword(s_indentIosIndex); + if(indent > 0) { + --indent; + } + } + } CVC4ostream& flush() { if(d_os != NULL) { @@ -87,6 +110,13 @@ public: template <class T> CVC4ostream& operator<<(T const& t) { if(d_os != NULL) { + if(d_firstColumn) { + d_firstColumn = false; + long indent = d_os->iword(s_indentIosIndex); + for(long i = 0; i < indent; ++ i) { + d_os = &(*d_os << s_tab); + } + } d_os = &(*d_os << t); } return *this; @@ -97,10 +127,8 @@ public: if(d_os != NULL) { d_os = &(*d_os << pf); - if (pf == d_endl) { - for (unsigned i = 0; i < d_indent; ++ i) { - d_os = &(*d_os << '\t'); - } + if(pf == d_endl) { + d_firstColumn = true; } } return *this; @@ -452,6 +480,27 @@ public: extern NullC nullCvc4Stream CVC4_PUBLIC; +/** + * Pushes an indentation level on construction, pop on destruction. + * Useful for tracing recursive functions especially, but also can be + * used for clearly separating different phases of an algorithm, + * or iterations of a loop, or... etc. + */ +class IndentedScope { + CVC4ostream d_out; +public: + inline IndentedScope(CVC4ostream out); + inline ~IndentedScope(); +};/* class IndentedScope */ + +#ifdef CVC4_DEBUG +inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } +inline IndentedScope::~IndentedScope() { d_out << pop; } +#else /* CVC4_DEBUG */ +inline IndentedScope::IndentedScope(CVC4ostream out) {} +inline IndentedScope::~IndentedScope() {} +#endif /* CVC4_DEBUG */ + }/* CVC4 namespace */ #endif /* __CVC4__OUTPUT_H */ diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h index 6f82eec5c..6573e9b64 100644 --- a/src/util/recursion_breaker.h +++ b/src/util/recursion_breaker.h @@ -79,10 +79,9 @@ namespace CVC4 { -template <class T> +template <class T, class Hasher = std::hash<T> > class RecursionBreaker { - //typedef std::hash_set<T> Set; - typedef std::set<T> Set; + typedef std::hash_set<T, Hasher> Set; typedef std::map<std::string, Set> Map; static CVC4_THREADLOCAL(Map*) s_maps; @@ -92,6 +91,7 @@ class RecursionBreaker { bool d_recursion; public: + /** Mark that item has been seen for tag. */ RecursionBreaker(std::string tag, const T& item) : d_tag(tag), d_item(item) { @@ -107,6 +107,7 @@ public: } } + /** Clean up the seen trail. */ ~RecursionBreaker() { Assert(s_maps->find(d_tag) != s_maps->end()); if(!d_recursion) { @@ -119,14 +120,15 @@ public: } } + /** Return true iff recursion has been detected. */ bool isRecursion() const throw() { return d_recursion; } };/* class RecursionBreaker<T> */ -template <class T> -CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps; +template <class T, class Hasher> +CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps; }/* CVC4 namespace */ diff --git a/src/util/tls.h.in b/src/util/tls.h.in index c2892d11c..fc0b6932b 100644 --- a/src/util/tls.h.in +++ b/src/util/tls.h.in @@ -26,13 +26,17 @@ #line 28 "@srcdir@/tls.h.in" +// A bit obnoxious: we have to take varargs to support multi-argument +// template types in the threadlocals. +// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise, +// due to the embedded comma. #if @CVC4_TLS_SUPPORTED@ -# define CVC4_THREADLOCAL(__type) @CVC4_TLS@ __type -# define CVC4_THREADLOCAL_PUBLIC(__type) @CVC4_TLS@ CVC4_PUBLIC __type +# define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type +# define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type #else # include <pthread.h> -# define CVC4_THREADLOCAL(__type) ::CVC4::ThreadLocal< __type > -# define CVC4_THREADLOCAL_PUBLIC(__type) CVC4_PUBLIC ::CVC4::ThreadLocal< __type > +# define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type > +# define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type > namespace CVC4 { @@ -76,6 +80,49 @@ public: };/* class ThreadLocalImpl<T, true> */ template <class T> +class ThreadLocalImpl<T*, true> { + pthread_key_t d_key; + + static void cleanup(void*) { + } + +public: + ThreadLocalImpl() { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + } + + ThreadLocalImpl(const T* t) { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t))); + } + + ThreadLocalImpl(const ThreadLocalImpl& tl) { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl)))); + } + + ThreadLocalImpl& operator=(const T* t) { + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t))); + return *this; + } + ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) { + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl)))); + return *this; + } + + operator T*() const { + return static_cast<T*>(pthread_getspecific(d_key)); + } + + T operator*() { + return *static_cast<T*>(pthread_getspecific(d_key)); + } + T* operator->() { + return static_cast<T*>(pthread_getspecific(d_key)); + } +};/* class ThreadLocalImpl<T*, true> */ + +template <class T> class ThreadLocalImpl<T, false> { };/* class ThreadLocalImpl<T, false> */ diff --git a/src/util/utility.h b/src/util/utility.h new file mode 100644 index 000000000..9aa4c1158 --- /dev/null +++ b/src/util/utility.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file utility.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 Some standard STL-related utility functions for CVC4 + ** + ** Some standard STL-related utility functions for CVC4. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__UTILITY_H +#define __CVC4__UTILITY_H + +#include <utility> +#include <functional> + +namespace CVC4 { + + +/** + * Like std::equal_to<>, but tests equality between the first element + * of a pair and an element. + */ +template <class T, class U> +struct first_equal_to : std::binary_function<std::pair<T, U>, T, bool> { + bool operator()(const std::pair<T, U>& pr, const T& x) const { + return pr.first == x; + } +};/* struct first_equal_to<T> */ + + +/** + * Like std::equal_to<>, but tests equality between the second element + * of a pair and an element. + */ +template <class T, class U> +struct second_equal_to : std::binary_function<std::pair<T, U>, U, bool> { + bool operator()(const std::pair<T, U>& pr, const U& x) const { + return pr.second == x; + } +};/* struct first_equal_to<T> */ + + +/** + * Using std::find_if(), finds the first iterator in [first,last) + * range that satisfies predicate. If none, return last; otherwise, + * search for a second one. If there IS a second one, return last, + * otherwise return the first (and unique) iterator satisfying pred(). + */ +template <class InputIterator, class Predicate> +inline InputIterator find_if_unique(InputIterator first, InputIterator last, Predicate pred) { + InputIterator match = std::find_if(first, last, pred); + if(match == last) { + return last; + } + + InputIterator match2 = match; + match2 = std::find_if(++match2, last, pred); + return (match2 == last) ? match : last; +} + + +}/* CVC4 namespace */ + +#endif /* __CVC4__UTILITY_H */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index b898c4cc2..319601121 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -20,6 +20,8 @@ SMT_TESTS = \ ite_real_valid.smt \ let.smt \ let2.smt \ + simplification_bug.smt \ + simplification_bug2.smt \ simple.smt \ simple2.smt \ simple-lra.smt \ diff --git a/test/regress/regress0/simplification_bug.smt b/test/regress/regress0/simplification_bug.smt new file mode 100644 index 000000000..8f45badeb --- /dev/null +++ b/test/regress/regress0/simplification_bug.smt @@ -0,0 +1,7 @@ +(benchmark simplification_bug +:logic QF_SAT +:extrapreds ((b)) +:status unsat +:formula +(and false b) +) diff --git a/test/regress/regress0/simplification_bug2.smt b/test/regress/regress0/simplification_bug2.smt new file mode 100644 index 000000000..f251d6dfa --- /dev/null +++ b/test/regress/regress0/simplification_bug2.smt @@ -0,0 +1,7 @@ +(benchmark flet_test +:logic QF_UF +:extrapreds ((b)) +:status unsat +:formula +(and b (or false false)) +) |