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) :
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;
** 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.
**/
#include <iostream>
#include <stdint.h>
-#include "type.h"
+#include "expr/type.h"
#include "expr/kind.h"
#include "expr/metakind.h"
#include "expr/expr.h"
#include "util/output.h"
#include "util/exception.h"
#include "util/language.h"
+#include "util/utility.h"
+#include "util/hash.h"
namespace CVC4 {
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.
}
}
+ /**
+ * 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. */
* 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
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,
Iterator2 replacementsBegin,
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
}
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());
// 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;
}
}
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);
}
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
(*i).substitute(type, replacement);
}
}
- return nb.constructTypeNode();
+
+ // put in cache
+ TypeNode tn = nb.constructTypeNode();
+ cache[*this] = tn;
+ return tn;
}
Cardinality TypeNode::getCardinality() const {
*/
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.
*/
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. */
/**
* 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.
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 */
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());
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;
}
}
# 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 )
** 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.
**/
** 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.
**/
#define __CVC4__MAIN__MAIN_H
namespace CVC4 {
-
namespace main {
/** Full argv[0] */
)
| TRANSFORM_TOK formula[f]
- { UNSUPPORTED("TRANSFORM command"); }
+ { cmd = new SimplifyCommand(f); }
| PRINT_TOK formula[f]
{ UNSUPPORTED("PRINT command"); }
}
/* 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");
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;
** 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>
#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"
#include "theory/bv/theory_bv.h"
#include "theory/datatypes/theory_datatypes.h"
-
using namespace std;
using namespace CVC4;
using namespace CVC4::smt;
* 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 */
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") {
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" ||
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();
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();
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") {
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();
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) {
// 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();
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) {
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;
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
}
}
-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
// 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();
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 "
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 "
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();
}
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)
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.";
}
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
}
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 "
++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
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.";
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)");
}
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)");
}
}
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();
}
*/
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
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?
rewriter.h \
rewriter_attributes.h \
rewriter.cpp \
+ substitutions.h \
valuation.h \
valuation.cpp
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"),
StatisticsRegistry::registerStat(&d_statSlackVariables);
StatisticsRegistry::registerStat(&d_statDisequalitySplits);
StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
+ StatisticsRegistry::registerStat(&d_simplifyTimer);
StatisticsRegistry::registerStat(&d_staticLearningTimer);
StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
StatisticsRegistry::unregisterStat(&d_statSlackVariables);
StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
+ StatisticsRegistry::unregisterStat(&d_simplifyTimer);
StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
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);
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"); }
IntStat d_statUserVariables, d_statSlackVariables;
IntStat d_statDisequalitySplits;
IntStat d_statDisequalityConflicts;
+ TimerStat d_simplifyTimer;
TimerStat d_staticLearningTimer;
IntStat d_permanentlyRemovedVariables;
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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
** 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
#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 {
}
}
+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 */
** 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.
**/
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 */
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()) {
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 */
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};
};
"
-/*
- * 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
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
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 */
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);
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();
* Should be called to clean up any state.
*/
static void shutdown();
-};
+};/* class Rewriter */
-} // Namesapce theory
-} // Namespace CVC4
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
-/*
- * 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
node.setAttribute(post_rewrite(), cache);
}
}
-};
-
-} // Namespace CVC4
-} // Namespace theory
+};/* struct RewriteAttribute */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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>());
}
/**
- * 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 {
}
/**
- * 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,
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 */
#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 {
*/
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.
}
/**
- * 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);
/**
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.
}
}
+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 */
#define __CVC4__THEORY__VALUATION_H
#include "expr/node.h"
+#include "theory/substitutions.h"
namespace CVC4 {
*/
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 */
subrange_bound.h \
cardinality.h \
cardinality.cpp \
+ cache.h \
+ utility.h \
trans_closure.h \
trans_closure.cpp \
boolean_simplification.h \
namespace CVC4 {
-void
+bool
BooleanSimplification::push_back_associative_commute_recursive
(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
throw(AssertionException) {
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 */
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:
removeDuplicates(buffer);
+ if(buffer.size() == 1) {
+ return buffer[0];
+ }
+
NodeBuilder<> nb(kind::AND);
nb.append(buffer);
return nb;
removeDuplicates(buffer);
+ Assert(buffer.size() > 0);
+ if(buffer.size() == 1) {
+ return buffer[0];
+ }
+
NodeBuilder<> nb(kind::OR);
nb.append(buffer);
return nb;
* @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);
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() */
/**
base = base[0];
polarity = !polarity;
}
+ if(n.getMetaKind() == kind::metakind::CONSTANT) {
+ return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
+ }
if(polarity){
return base.notNode();
}else{
}
}
+ /**
+ * 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 */
--- /dev/null
+/********************* */
+/*! \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 */
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;
}
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
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
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().
}
};/* 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
memoryMap(false),
strictParsing(false),
lazyDefinitionExpansion(false),
+ simplificationMode(INCREMENTAL_MODE),
+ simplificationStyle(NO_SIMPLIFICATION_STYLE),
interactive(false),
interactiveSetByUser(false),
segvNoSpin(false),
rewriteArithEqualities(false),
arithPropagation(false),
satRandomFreq(0.0),
- satRandomSeed(91648253), //Minisat's default value
+ satRandomSeed(91648253),// Minisat's default value
pivotRule(MINIMUM)
{
}
--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\
--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\
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) {
* any collision.
*/
enum OptionValue {
- SMTCOMP = 256, /* no clash with char options */
+ SMTCOMP = 256, /* avoid clashing with char options */
STATS,
SEGV_NOSPIN,
PARSE_ONLY,
PRINT_EXPR_TYPES,
UF_THEORY,
LAZY_DEFINITION_EXPANSION,
+ SIMPLIFICATION_MODE,
INTERACTIVE,
NO_INTERACTIVE,
PRODUCE_MODELS,
{ "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 },
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: `") +
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;
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] + "'");
}
}
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) {
/** 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;
throw(OptionException);
};/* 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) {
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 */
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);
#ifndef __CVC4__OUTPUT_H
#define __CVC4__OUTPUT_H
+#include <ios>
#include <iostream>
#include <string>
#include <cstdio>
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) {
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;
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;
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 */
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;
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) {
}
}
+ /** Clean up the seen trail. */
~RecursionBreaker() {
Assert(s_maps->find(d_tag) != s_maps->end());
if(!d_recursion) {
}
}
+ /** 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 */
#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 {
}
};/* 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> */
--- /dev/null
+/********************* */
+/*! \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 */
ite_real_valid.smt \
let.smt \
let2.smt \
+ simplification_bug.smt \
+ simplification_bug2.smt \
simple.smt \
simple2.smt \
simple-lra.smt \
--- /dev/null
+(benchmark simplification_bug
+:logic QF_SAT
+:extrapreds ((b))
+:status unsat
+:formula
+(and false b)
+)
--- /dev/null
+(benchmark flet_test
+:logic QF_UF
+:extrapreds ((b))
+:status unsat
+:formula
+(and b (or false false))
+)
projects / cvc5.git / commitdiff