print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
print $OUT $standard_template;
print $OUT " **\n";
- print $OUT " ** \brief [[ Add one-line brief description here ]]\n";
+ print $OUT " ** \\brief [[ Add one-line brief description here ]]\n";
print $OUT " **\n";
print $OUT " ** [[ Add lengthier description here ]]\n";
print $OUT " ** \\todo document this file\n";
namespace expr {
const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
+const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
}/* CVC4::expr namespace */
return d_node->isConst();
}
-void Expr::toStream(std::ostream& out) const {
+void Expr::toStream(std::ostream& out, int depth, bool types) const {
ExprManagerScope ems(*this);
- d_node->toStream(out);
+ d_node->toStream(out, depth, types);
}
Node Expr::getNode() const {
namespace expr {
class CVC4_PUBLIC ExprSetDepth;
+ class CVC4_PUBLIC ExprPrintTypes;
}/* CVC4::expr namespace */
/**
~TypeCheckingException() throw ();
/**
- * Get the Node that caused the type-checking to fail.
- * @return the node
+ * Get the Expr that caused the type-checking to fail.
+ * @return the expr
*/
Expr getExpression() const;
* Outputs the string representation of the expression to the stream.
* @param out the output stream
*/
- void toStream(std::ostream& out) const;
+ void toStream(std::ostream& out, int depth = -1, bool types = false) const;
/**
* Check if this is a null expression.
ExprManager* getExprManager() const;
/**
- * IOStream manipulator to set the maximum depth of Nodes when
+ * IOStream manipulator to set the maximum depth of Exprs when
* pretty-printing. -1 means print to any depth. E.g.:
*
* // let a, b, c, and d be VARIABLEs
- * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
- * out << setdepth(3) << n;
+ * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ * out << setdepth(3) << e;
*
* gives "(OR a b (AND c (NOT d)))", but
*
- * out << setdepth(1) << [same node as above]
+ * out << setdepth(1) << [same expr as above]
*
* gives "(OR a b (...))"
*/
typedef expr::ExprSetDepth setdepth;
+ /**
+ * IOStream manipulator to print type ascriptions or not.
+ *
+ * // let a, b, c, and d be variables of sort U
+ * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ * out << e;
+ *
+ * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+ */
+ typedef expr::ExprPrintTypes printtypes;
+
/**
* Very basic pretty printer for Expr.
* This is equivalent to calling e.getNode().printAst(...)
*/
NodeTemplate<true> getNode() const;
- // Friend to access the actual internal node information and private methods
+ // Friend to access the actual internal expr information and private methods
friend class SmtEngine;
friend class ExprManager;
};
namespace expr {
/**
- * IOStream manipulator to set the maximum depth of Nodes when
+ * IOStream manipulator to set the maximum depth of Exprs when
* pretty-printing. -1 means print to any depth. E.g.:
*
* // let a, b, c, and d be VARIABLEs
- * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
- * out << setdepth(3) << n;
+ * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ * out << setdepth(3) << e;
*
* gives "(OR a b (AND c (NOT d)))", but
*
- * out << setdepth(1) << [same node as above]
+ * out << setdepth(1) << [same expr as above]
*
* gives "(OR a b (...))".
*
static const int s_defaultPrintDepth = 3;
/**
- * When this manipulator is
+ * When this manipulator is used, the depth is stored here.
*/
long d_depth;
}
};
+/**
+ * IOStream manipulator to print type ascriptions or not.
+ *
+ * // let a, b, c, and d be variables of sort U
+ * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ * out << e;
+ *
+ * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+ */
+class CVC4_PUBLIC ExprPrintTypes {
+ /**
+ * The allocated index in ios_base for our depth setting.
+ */
+ static const int s_iosIndex;
+
+ /**
+ * The default depth to print, for ostreams that haven't yet had a
+ * setdepth() applied to them.
+ */
+ static const int s_defaultPrintTypes = false;
+
+ /**
+ * When this manipulator is used, the setting is stored here.
+ */
+ bool d_printTypes;
+
+public:
+ /**
+ * Construct a ExprPrintTypes with the given setting.
+ */
+ ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
+
+ inline void applyPrintTypes(std::ostream& out) {
+ out.iword(s_iosIndex) = d_printTypes;
+ }
+
+ static inline bool getPrintTypes(std::ostream& out) {
+ return out.iword(s_iosIndex);
+ }
+
+ static inline void setPrintTypes(std::ostream& out, bool printTypes) {
+ out.iword(s_iosIndex) = printTypes;
+ }
+};
+
}/* CVC4::expr namespace */
${getConst_instantiations}
namespace expr {
/**
- * Sets the default depth when pretty-printing a Node to an ostream.
- * Use like this:
+ * Sets the default print-types setting when pretty-printing an Expr
+ * to an ostream. Use like this:
*
- * // let out be an ostream, n a Node
- * out << Node::setdepth(n) << n << endl;
+ * // let out be an ostream, e an Expr
+ * out << Expr::setdepth(n) << e << endl;
*
* The depth stays permanently (until set again) with the stream.
*/
return out;
}
+/**
+ * Sets the default depth when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ * // let out be an ostream, e an Expr
+ * out << Expr::setprinttypes(true) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
+ pt.applyPrintTypes(out);
+ return out;
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
* given stream
* @param out the sream to serialise this node to
*/
- inline void toStream(std::ostream& out, int toDepth = -1) const {
+ inline void toStream(std::ostream& out, int toDepth = -1,
+ bool types = false) const {
if(!ref_count) {
Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
}
- d_nv->toStream(out, toDepth);
+ d_nv->toStream(out, toDepth, types);
}
/**
*/
typedef expr::ExprSetDepth setdepth;
+ /**
+ * IOStream manipulator to print type ascriptions or not.
+ *
+ * // let a, b, c, and d be variables of sort U
+ * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
+ * out << n;
+ *
+ * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+ */
+ typedef expr::ExprPrintTypes printtypes;
+
/**
* Very basic pretty printer for Node.
* @param o output stream to print to.
* @param indent number of spaces to indent the formula by.
*/
- void printAst(std::ostream & o, int indent = 0) const;
+ inline void printAst(std::ostream& out, int indent = 0) const;
NodeTemplate<true> eqNode(const NodeTemplate& right) const;
NodeTemplate<true> impNode(const NodeTemplate& right) const;
NodeTemplate<true> xorNode(const NodeTemplate& right) const;
-private:
-
- /**
- * Indents the given stream a given amount of spaces.
- * @param out the stream to indent
- * @param indent the numer of spaces
- */
- static void indent(std::ostream& out, int indent) {
- for(int i = 0; i < indent; i++) {
- out << ' ';
- }
- }
-
};/* class NodeTemplate<ref_count> */
/**
* @return the changed stream.
*/
inline std::ostream& operator<<(std::ostream& out, TNode n) {
- n.toStream(out, Node::setdepth::getDepth(out));
+ n.toStream(out,
+ Node::setdepth::getDepth(out),
+ Node::printtypes::getPrintTypes(out));
return out;
}
}
template <bool ref_count>
-void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
- indent(out, ind);
- out << '(';
- out << getKind();
- if(getMetaKind() == kind::metakind::VARIABLE) {
- out << ' ' << getId();
- } else if(getMetaKind() == kind::metakind::CONSTANT) {
- out << ' ';
- kind::metakind::NodeValueConstPrinter::toStream(out, d_nv);
- } else {
- if(hasOperator()) {
- out << std::endl;
- getOperator().printAst(out, ind + 1);
- }
- if(getNumChildren() >= 1) {
- for(const_iterator child = begin(); child != end(); ++child) {
- out << std::endl;
- (*child).printAst(out, ind + 1);
- }
- out << std::endl;
- indent(out, ind);
- }
- }
- out << ')';
+inline void
+NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
+ d_nv->printAst(out, indent);
}
/**
* to meet. A cleaner solution is welcomed.
*/
static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
+ Warning() << Node::setdepth(-1) << n << std::endl;
+ Warning().flush();
+}
+static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) {
n.printAst(Warning(), 0);
Warning().flush();
}
static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
+ Warning() << Node::setdepth(-1) << n << std::endl;
+ Warning().flush();
+}
+static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) {
n.printAst(Warning(), 0);
Warning().flush();
}
operator Node();
operator Node() const;
- inline void toStream(std::ostream& out, int depth = -1) const {
+ inline void toStream(std::ostream& out, int depth = -1,
+ bool types = false) const {
Assert(!isUsed(), "NodeBuilder is one-shot only; "
"attempt to access it after conversion");
- d_nv->toStream(out, depth);
+ d_nv->toStream(out, depth, types);
}
NodeBuilder<nchild_thresh>& operator&=(TNode);
template <unsigned nchild_thresh>
inline std::ostream& operator<<(std::ostream& out,
const NodeBuilder<nchild_thresh>& b) {
- b.toStream(out, Node::setdepth::getDepth(out));
+ b.toStream(out,
+ Node::setdepth::getDepth(out),
+ Node::printtypes::getPrintTypes(out));
return out;
}
if(!hasType) {
// Infer the type
switch(n.getKind()) {
+ case kind::SORT_TYPE:
+ typeNode = kindType();
+ break;
case kind::EQUAL:
typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n);
break;
}
inline TypeNode NodeManager::mkSort() {
- TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
- return type;
+ return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode();
}
inline TypeNode NodeManager::mkSort(const std::string& name) {
return ss.str();
}
-void NodeValue::toStream(std::ostream& out, int toDepth) const {
+void NodeValue::toStream(std::ostream& out, int toDepth, bool types) const {
using namespace CVC4::kind;
using namespace CVC4;
if(getKind() == kind::NULL_EXPR) {
out << "null";
} else if(getMetaKind() == kind::metakind::VARIABLE) {
- if(getKind() != kind::VARIABLE) {
+ if(getKind() != kind::VARIABLE &&
+ getKind() != kind::SORT_TYPE) {
out << getKind() << ':';
}
string s;
+ NodeManager* nm = NodeManager::currentNM();
// conceptually "this" is const, and hasAttribute() doesn't change
// its argument, but it requires a non-const key arg (for now)
- if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this),
- VarNameAttr(), s)) {
+ if(nm->getAttribute(const_cast<NodeValue*>(this),
+ VarNameAttr(), s)) {
out << s;
} else {
out << "var_" << d_id;
}
+ if(types) {
+ // print the whole type, but not *its* type
+ out << ":";
+ nm->getType(TNode(this)).toStream(out, -1, false);
+ }
} else {
out << '(' << Kind(d_kind);
if(getMetaKind() == kind::metakind::CONSTANT) {
out << ' ';
}
if(toDepth != 0) {
- (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1);
+ (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types);
} else {
out << "(...)";
}
}
}
+void NodeValue::printAst(std::ostream& out, int ind) const {
+ indent(out, ind);
+ out << '(';
+ out << getKind();
+ if(getMetaKind() == kind::metakind::VARIABLE) {
+ out << ' ' << getId();
+ } else if(getMetaKind() == kind::metakind::CONSTANT) {
+ out << ' ';
+ kind::metakind::NodeValueConstPrinter::toStream(out, this);
+ } else {
+ if(nv_begin() != nv_end()) {
+ for(const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
+ out << std::endl;
+ (*child)->printAst(out, ind + 1);
+ }
+ out << std::endl;
+ indent(out, ind);
+ }
+ }
+ out << ')';
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
}
std::string toString() const;
- void toStream(std::ostream& out, int toDepth = -1) const;
+ void toStream(std::ostream& out, int toDepth = -1, bool types = false) const;
static inline unsigned kindToDKind(Kind k) {
return ((unsigned) k) & kindMask;
NodeValue* getChild(int i) const;
+ void printAst(std::ostream& out, int indent = 0) const;
+
+private:
+
+ /**
+ * Indents the given stream a given amount of spaces.
+ * @param out the stream to indent
+ * @param indent the numer of spaces
+ */
+ static inline void indent(std::ostream& out, int indent) {
+ for(int i = 0; i < indent; i++) {
+ out << ' ';
+ }
+ }
+
};/* class NodeValue */
/**
}/* CVC4 namespace */
#include "expr/node_manager.h"
+#include "expr/type_node.h"
namespace CVC4 {
namespace expr {
}
inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
- nv.toStream(out, Node::setdepth::getDepth(out));
+ nv.toStream(out,
+ Node::setdepth::getDepth(out),
+ Node::printtypes::getPrintTypes(out));
return out;
}
}/* CVC4::expr namespace */
+
+#ifdef CVC4_DEBUG
+/**
+ * Pretty printer for use within gdb. This is not intended to be used
+ * outside of gdb. This writes to the Warning() stream and immediately
+ * flushes the stream.
+ */
+static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
+ Warning() << Node::setdepth(-1) << *nv << std::endl;
+ Warning().flush();
+}
+
+static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) {
+ nv->printAst(Warning(), 0);
+ Warning().flush();
+}
+#endif /* CVC4_DEBUG */
+
}/* CVC4 namespace */
#endif /* __CVC4__EXPR__NODE_VALUE_H */
/** Is this a sort kind */
bool TypeNode::isSort() const {
- return getKind() == kind::VARIABLE;
+ return getKind() == kind::SORT_TYPE;
}
/** Is this a kind type (i.e., the type of a type)? */
* given stream
* @param out the sream to serialise this node to
*/
- inline void toStream(std::ostream& out, int toDepth = -1) const {
- d_nv->toStream(out, toDepth);
+ inline void toStream(std::ostream& out, int toDepth = -1,
+ bool types = false) const {
+ d_nv->toStream(out, toDepth, types);
}
/**
* @param o output stream to print to.
* @param indent number of spaces to indent the formula by.
*/
- void printAst(std::ostream & o, int indent = 0) const;
+ void printAst(std::ostream& out, int indent = 0) const;
/**
* Returns true if this type is a null type.
* @return the changed stream.
*/
inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
- n.toStream(out, Node::setdepth::getDepth(out));
+ n.toStream(out,
+ Node::setdepth::getDepth(out),
+ Node::printtypes::getPrintTypes(out));
return out;
}
NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
}
+inline void TypeNode::printAst(std::ostream& out, int indent) const {
+ d_nv->printAst(out, indent);
+}
+
+#ifdef CVC4_DEBUG
+/**
+ * Pretty printer for use within gdb. This is not intended to be used
+ * outside of gdb. This writes to the Warning() stream and immediately
+ * flushes the stream.
+ *
+ * Note that this function cannot be a template, since the compiler
+ * won't instantiate it. Even if we explicitly instantiate. (Odd?)
+ * So we implement twice. We mark as __attribute__((used)) so that
+ * GCC emits code for it even though static analysis indicates it's
+ * never called.
+ *
+ * Tim's Note: I moved this into the node.h file because this allows gdb
+ * to find the symbol, and use it, which is the first standard this code needs
+ * to meet. A cleaner solution is welcomed.
+ */
+static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
+ Warning() << Node::setdepth(-1) << n << std::endl;
+ Warning().flush();
+}
+static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {
+ n.printAst(Warning(), 0);
+ Warning().flush();
+}
+#endif /* CVC4_DEBUG */
+
}/* CVC4 namespace */
#endif /* __CVC4__NODE_H */
USE_MMAP,
SHOW_CONFIG,
STRICT_PARSING,
- DEFAULT_EXPR_DEPTH
+ DEFAULT_EXPR_DEPTH,
+ PRINT_EXPR_TYPES
};/* enum OptionValue */
/**
{ "mmap", no_argument , NULL, USE_MMAP },
{ "strict-parsing", no_argument , NULL, STRICT_PARSING },
{ "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
+ { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
};/* if you add things to the above, please remember to update usage.h! */
/** Full argv[0] */
}
break;
+ case PRINT_EXPR_TYPES:
+ {
+ Debug.getStream() << Expr::printtypes(true);
+ Trace.getStream() << Expr::printtypes(true);
+ Notice.getStream() << Expr::printtypes(true);
+ Chat.getStream() << Expr::printtypes(true);
+ Message.getStream() << Expr::printtypes(true);
+ Warning.getStream() << Expr::printtypes(true);
+ }
+ break;
+
case SHOW_CONFIG:
fputs(Configuration::about().c_str(), stdout);
printf("\n");
Without an input file, or with `-', CVC4 reads from standard input.\n\
\n\
CVC4 options:\n\
- --lang | -L force input language (default is `auto'; see --lang help)\n\
- --version | -V identify this CVC4 binary\n\
- --help | -h this command line reference\n\
- --parse-only exit after parsing input\n\
- --mmap memory map file input\n\
- --show-config show CVC4 static configuration\n"
-#ifdef CVC4_DEBUG
-"\
- --segv-nospin don't spin on segfault waiting for gdb\n"
-#endif
-#ifndef CVC4_MUZZLE
-"\
- --no-checking disable semantic checks in the parser\n\
- --strict-parsing fail on inputs that are not strictly conformant (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\
- --stats give statistics on exit\n\
- --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n"
-#endif
+ --lang | -L force input language (default is `auto'; see --lang help)\n\
+ --version | -V identify this CVC4 binary\n\
+ --help | -h this command line reference\n\
+ --parse-only exit after parsing input\n\
+ --mmap memory map file input\n\
+ --show-config show CVC4 static configuration\n\
+ --segv-nospin don't spin on segfault waiting for gdb\n\
+ --no-checking disable semantic checks in the parser\n\
+ --strict-parsing fail on inputs that are not strictly conformant (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\
+ --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"
;
}/* CVC4::main namespace */
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
"expr/type_constant.h" \
"basic types"
operator FUNCTION_TYPE 2: "function type"
-variable SORT_TYPE "sort type"
namespace theory {
+// rewrite cache support
+template <bool topLevel> struct PreRewriteCacheTag {};
+typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop;
+typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache;
+template <bool topLevel> struct PostRewriteCacheTag {};
+typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop;
+typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache;
+
/**
* Instances of this class serve as response codes from
* Theory::preRewrite() and Theory::postRewrite(). Instances of
return true;
}
+ /**
+ * Check whether a node is in the pre-rewrite cache or not.
+ */
+ static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
+ if(topLevel) {
+ return n.hasAttribute(PreRewriteCacheTop());
+ } else {
+ return n.hasAttribute(PreRewriteCache());
+ }
+ }
+
+ /**
+ * Get the value of the pre-rewrite cache (or Node::null()) if there is
+ * none).
+ */
+ static Node getPreRewriteCache(TNode n, bool topLevel) throw() {
+ if(topLevel) {
+ Node out;
+ if(n.getAttribute(PreRewriteCacheTop(), out)) {
+ return out.isNull() ? Node(n) : out;
+ }
+ } else {
+ Node out;
+ if(n.getAttribute(PreRewriteCache(), out)) {
+ return out.isNull() ? Node(n) : out;
+ }
+ }
+ return Node::null();
+ }
+
+ /**
+ * Set the value of the pre-rewrite cache. v cannot be a null Node.
+ */
+ static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() {
+ AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
+ AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()");
+ // mappings from n -> n are actually stored as n -> null as a
+ // special case, to avoid cycles in the reference-counting of Nodes
+ if(topLevel) {
+ n.setAttribute(PreRewriteCacheTop(), n == v ? TNode::null() : v);
+ } else {
+ n.setAttribute(PreRewriteCache(), n == v ? TNode::null() : v);
+ }
+ }
+
+ /**
+ * Check whether a node is in the post-rewrite cache or not.
+ */
+ static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
+ if(topLevel) {
+ return n.hasAttribute(PostRewriteCacheTop());
+ } else {
+ return n.hasAttribute(PostRewriteCache());
+ }
+ }
+
+ /**
+ * Get the value of the post-rewrite cache (or Node::null()) if there is
+ * none).
+ */
+ static Node getPostRewriteCache(TNode n, bool topLevel) throw() {
+ if(topLevel) {
+ Node out;
+ if(n.getAttribute(PostRewriteCacheTop(), out)) {
+ return out.isNull() ? Node(n) : out;
+ }
+ } else {
+ Node out;
+ if(n.getAttribute(PostRewriteCache(), out)) {
+ return out.isNull() ? Node(n) : out;
+ }
+ }
+ return Node::null();
+ }
+
+ /**
+ * Set the value of the post-rewrite cache. v cannot be a null Node.
+ */
+ static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() {
+ AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
+ AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()");
+ // mappings from n -> n are actually stored as n -> null as a
+ // special case, to avoid cycles in the reference-counting of Nodes
+ if(topLevel) {
+ n.setAttribute(PostRewriteCacheTop(), n == v ? TNode::null() : v);
+ } else {
+ n.setAttribute(PostRewriteCache(), n == v ? TNode::null() : v);
+ }
+ }
+
};/* class Theory */
std::ostream& operator<<(std::ostream& os, Theory::Effort level);
Assert(k >= 0 && k < kind::LAST_KIND);
if(n.getMetaKind() == kind::metakind::VARIABLE) {
+ // FIXME: we don't yet have a Type-to-Theory map. When we do,
+ // look up the type of the var and return that Theory (?)
+
+ //The following JUST hacks around this lack of a table
TypeNode t = n.getType();
- if(t.isBoolean()) {
- return &d_bool;
- } else if(t.isReal()) {
- return &d_arith;
- } else if(t.isArray()) {
- return &d_arrays;
- } else {
- return &d_uf;
- }
- //Unimplemented();
- } else if(k == kind::EQUAL) {
- // if LHS is a variable, use theoryOf(LHS.getType())
- // otherwise, use theoryOf(LHS)
- TNode lhs = n[0];
- if(lhs.getMetaKind() == kind::metakind::VARIABLE) {
- // FIXME: we don't yet have a Type-to-Theory map. When we do,
- // look up the type of the LHS and return that Theory (?)
-
- //The following JUST hacks around this lack of a table
- TypeNode type_of_n = lhs.getType();
- if(type_of_n.isReal()) {
- return &d_arith;
- } else if(type_of_n.isArray()) {
- return &d_arrays;
- } else {
- return &d_uf;
- //Unimplemented();
+ Kind k = t.getKind();
+ if(k == kind::TYPE_CONSTANT) {
+ switch(TypeConstant tc = t.getConst<TypeConstant>()) {
+ case BOOLEAN_TYPE:
+ return d_theoryOfTable[kind::CONST_BOOLEAN];
+ case INTEGER_TYPE:
+ return d_theoryOfTable[kind::CONST_INTEGER];
+ case REAL_TYPE:
+ return d_theoryOfTable[kind::CONST_RATIONAL];
+ case KIND_TYPE:
+ default:
+ Unhandled(tc);
}
- } else {
- return theoryOf(lhs);
}
+
+ return d_theoryOfTable[k];
+ } else if(k == kind::EQUAL) {
+ // equality is special: use LHS
+ return theoryOf(n[0]);
} else {
// use our Kind-to-Theory mapping
return d_theoryOfTable[k];
/* Our goal is to tease out any ITE's sitting under a theory operator. */
Node TheoryEngine::removeITEs(TNode node) {
- Debug("ite") << "handleNonAtomicNode(" << node << ")" << endl;
+ Debug("ite") << "removeITEs(" << node << ")" << endl;
/* The result may be cached already */
Node cachedRewrite;
TypeNode nodeType = node[1].getType();
if(!nodeType.isBoolean()){
- Node skolem = nodeManager->mkVar(node.getType());
+ Node skolem = nodeManager->mkSkolem(node.getType());
Node newAssertion =
nodeManager->mkNode(
kind::ITE,
namespace CVC4 {
-namespace theory {
-
-// rewrite cache support
-template <bool topLevel> struct PreRewriteCacheTag {};
-typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop;
-typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache;
-template <bool topLevel> struct PostRewriteCacheTag {};
-typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop;
-typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache;
-
-}/* CVC4::theory namespace */
-
// In terms of abstraction, this is below (and provides services to)
// PropEngine.
theory::arrays::TheoryArrays d_arrays;
theory::bv::TheoryBV d_bv;
-
/**
* Check whether a node is in the pre-rewrite cache or not.
*/
static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
- if(topLevel) {
- return n.hasAttribute(theory::PreRewriteCacheTop());
- } else {
- return n.hasAttribute(theory::PreRewriteCache());
- }
+ return theory::Theory::inPreRewriteCache(n, topLevel);
}
/**
* Get the value of the pre-rewrite cache (or Node::null()) if there is
* none).
*/
- static Node getPreRewriteCache(TNode in, bool topLevel) throw() {
- if(topLevel) {
- Node out;
- if(in.getAttribute(theory::PreRewriteCacheTop(), out)) {
- return out.isNull() ? Node(in) : out;
- }
- } else {
- Node out;
- if(in.getAttribute(theory::PreRewriteCache(), out)) {
- return out.isNull() ? Node(in) : out;
- }
- }
- return Node::null();
+ static Node getPreRewriteCache(TNode n, bool topLevel) throw() {
+ return theory::Theory::getPreRewriteCache(n, topLevel);
}
/**
* Set the value of the pre-rewrite cache. v cannot be a null Node.
*/
static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() {
- AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
- AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()");
- // mappings from n -> n are actually stored as n -> null as a
- // special case, to avoid cycles in the reference-counting of Nodes
- if(topLevel) {
- n.setAttribute(theory::PreRewriteCacheTop(), n == v ? TNode::null() : v);
- } else {
- n.setAttribute(theory::PreRewriteCache(), n == v ? TNode::null() : v);
- }
+ return theory::Theory::setPreRewriteCache(n, topLevel, v);
}
/**
* Check whether a node is in the post-rewrite cache or not.
*/
static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
- if(topLevel) {
- return n.hasAttribute(theory::PostRewriteCacheTop());
- } else {
- return n.hasAttribute(theory::PostRewriteCache());
- }
+ return theory::Theory::inPostRewriteCache(n, topLevel);
}
/**
* Get the value of the post-rewrite cache (or Node::null()) if there is
* none).
*/
- static Node getPostRewriteCache(TNode in, bool topLevel) throw() {
- if(topLevel) {
- Node out;
- if(in.getAttribute(theory::PostRewriteCacheTop(), out)) {
- return out.isNull() ? Node(in) : out;
- }
- } else {
- Node out;
- if(in.getAttribute(theory::PostRewriteCache(), out)) {
- return out.isNull() ? Node(in) : out;
- }
- }
- return Node::null();
+ static Node getPostRewriteCache(TNode n, bool topLevel) throw() {
+ return theory::Theory::getPostRewriteCache(n, topLevel);
}
/**
* Set the value of the post-rewrite cache. v cannot be a null Node.
*/
static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() {
- AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
- AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()");
- // mappings from n -> n are actually stored as n -> null as a
- // special case, to avoid cycles in the reference-counting of Nodes
- if(topLevel) {
- n.setAttribute(theory::PostRewriteCacheTop(), n == v ? TNode::null() : v);
- } else {
- n.setAttribute(theory::PostRewriteCache(), n == v ? TNode::null() : v);
- }
+ return theory::Theory::setPostRewriteCache(n, topLevel, v);
}
/**
*/
Node rewrite(TNode in);
+ /**
+ * Replace ITE forms in a node.
+ */
Node removeITEs(TNode t);
public:
StatisticsRegistry::registerStat(&d_statAugLemma);
StatisticsRegistry::registerStat(&d_statExplanatation);
}
+
+ ~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_statConflicts);
+ StatisticsRegistry::unregisterStat(&d_statPropagate);
+ StatisticsRegistry::unregisterStat(&d_statLemma);
+ StatisticsRegistry::unregisterStat(&d_statAugLemma);
+ StatisticsRegistry::unregisterStat(&d_statExplanatation);
+ }
};
Statistics d_statistics;
theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
+variable SORT_TYPE "sort type"
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
#ifdef CVC4_STATISTICS_ON
-#define USE_STATISTICS true
+# define USE_STATISTICS true
#else
-#define USE_STATISTICS false
+# define USE_STATISTICS false
#endif
class CVC4_PUBLIC Stat;
static inline void registerStat(Stat* s) throw (AssertionException);
static inline void unregisterStat(Stat* s) throw (AssertionException);
-}; /* class StatisticsRegistry */
+};/* class StatisticsRegistry */
class CVC4_PUBLIC Stat {
/**
- * class T must have stream insertion operation defined.
+ * class T must have stream insertion operation defined.
* std::ostream& operator<<(std::ostream&, const T&);
*/
template<class T>
--- /dev/null
+Regressions
+===========
+
+To insert a new regression, add the file to Subversion, for example:
+
+ svn add regress/regress0/testMyFunctionality.cvc
+
+Also add it to the relevant Makefile.am, here, in regress/regress0/Makefile.am.
+
+A number of regressions exist under test/regress that aren't listed in any
+Makefile.am. These are regressions that may someday be included in the standard
+suite of tests, but aren't yet included (perhaps they test functionality not
+yet supported).
+
+If you want to add a new directory of regressions, add the directory name to
+SUBDIRS (with . running first, by convention), and set up the new directory
+with a new Makefile.am, adding all to the Subversion repository.
+
+=== EXPECTED OUTPUT, ERROR, AND EXIT CODES ===
+
+In the case of CVC input, you can specify expected stdout, stderr, and exit
+codes with the following lines directly in the CVC regression file:
+
+% EXPECT: stdout
+% EXPECT-ERROR: stderr
+% EXIT: 0
+
+expects an exit status of 0 from cvc4, the single line "stderr" on stderr,
+and the single line "stdout" on stdout. You can repeat EXPECT and EXPECT-ERROR
+lines as many times as you like, and at different points of the file. This is
+useful for multiple queries:
+
+% EXPECT: INVALID
+QUERY FALSE;
+% EXPECT: VALID
+QUERY TRUE;
+% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: Parse Error: regress.cvc:7.13: Unexpected token: 'error'.
+syntax error;
+% EXIT: 1
+
+Use of % gestures in CVC format is natural, as these are comments and ignored
+by the CVC presentation language lexer. In SMT and SMT2 formats, you can do the
+same, putting % gestures in the file. However, the run_regression script
+separates these from the benchmark before running cvc4, so the cvc4 SMT and SMT2
+lexers never see (and get tripped up on) the % gestures. But there's then the
+annoyance that you can't run SMT and SMT2 regressions from the command line
+without the aid of the run_regression script. So, if you prefer, you can separate
+the benchmark from the output expectations yourself, putting the benchmark in
+(e.g.) regress/regress0/benchmark.smt, and the % EXPECT: lines in
+regress/regress0/benchmark.smt.expect, which is specifically looked for by
+the run_regression script. If such an .expect file exists, the benchmark
+is left verbatim (and never processed to remove the % EXPECT: lines) by the
+run_regression script.
+
+ -- Morgan Deters <mdeters@cs.nyu.edu> Thu, 01 Jul 2010 13:36:53 -0400
context/cdlist_black \
context/cdmap_black \
context/cdmap_white \
+ theory/theory_engine_white \
theory/theory_black \
theory/theory_uf_white \
theory/theory_arith_white \
--- /dev/null
+/********************* */
+/*! \file theory_engine_white.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 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 White box testing of CVC4::theory::Theory.
+ **
+ ** White box testing of CVC4::theory::Theory.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <deque>
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/theoryof_table.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/kind.h"
+#include "context/context.h"
+#include "util/rational.h"
+#include "util/integer.h"
+#include "util/Assert.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+using namespace std;
+
+class FakeOutputChannel : public OutputChannel {
+ void conflict(TNode n, bool safe) throw(AssertionException) {
+ Unimplemented();
+ }
+ void propagate(TNode n, bool safe) throw(AssertionException) {
+ Unimplemented();
+ }
+ void lemma(TNode n, bool safe) throw(AssertionException) {
+ Unimplemented();
+ }
+ void augmentingLemma(TNode n, bool safe) throw(AssertionException) {
+ Unimplemented();
+ }
+ void explanation(TNode n, bool safe) throw(AssertionException) {
+ Unimplemented();
+ }
+};/* class FakeOutputChannel */
+
+class FakeTheory;
+
+enum RewriteType {
+ PRE,
+ POST
+};/* enum RewriteType */
+
+struct RewriteItem {
+ RewriteType d_type;
+ FakeTheory* d_theory;
+ Node d_node;
+ bool d_topLevel;
+};/* struct RewriteItem */
+
+class FakeTheory : public Theory {
+ std::string d_id;
+
+ static std::deque<RewriteItem> s_expected;
+
+public:
+ FakeTheory(context::Context* ctxt, OutputChannel& out, std::string id) :
+ Theory(ctxt, out),
+ d_id(id) {
+ }
+
+ static void expect(RewriteType type, FakeTheory* thy,
+ TNode n, bool topLevel) throw() {
+ RewriteItem item = { type, thy, n, topLevel };
+ s_expected.push_back(item);
+ }
+
+ static bool nothingMoreExpected() throw() {
+ return s_expected.empty();
+ }
+
+ RewriteResponse preRewrite(TNode n, bool topLevel) {
+ if(s_expected.empty()) {
+ cout << std::endl
+ << "didn't expect anything more, but got" << std::endl
+ << " PRE " << topLevel << " " << identify() << " " << n << std::endl;
+ }
+ TS_ASSERT(!s_expected.empty());
+
+ RewriteItem expected = s_expected.front();
+ s_expected.pop_front();
+
+ if(expected.d_type != PRE ||
+ expected.d_theory != this ||
+ expected.d_node != n ||
+ expected.d_topLevel != topLevel) {
+ cout << std::endl
+ << "HAVE PRE " << topLevel << " " << identify() << " " << n << std::endl
+ << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
+ }
+
+ TS_ASSERT_EQUALS(expected.d_type, PRE);
+ TS_ASSERT_EQUALS(expected.d_theory, this);
+ TS_ASSERT_EQUALS(expected.d_node, n);
+ TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
+
+ return RewritingComplete(n);
+ }
+
+ RewriteResponse postRewrite(TNode n, bool topLevel) {
+ if(s_expected.empty()) {
+ cout << std::endl
+ << "didn't expect anything more, but got" << std::endl
+ << " POST " << topLevel << " " << identify() << " " << n << std::endl;
+ }
+ TS_ASSERT(!s_expected.empty());
+
+ RewriteItem expected = s_expected.front();
+ s_expected.pop_front();
+
+ if(expected.d_type != POST ||
+ expected.d_theory != this ||
+ expected.d_node != n ||
+ expected.d_topLevel != topLevel) {
+ cout << std::endl
+ << "HAVE POST " << topLevel << " " << identify() << " " << n << std::endl
+ << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
+ }
+
+ TS_ASSERT_EQUALS(expected.d_type, POST);
+ TS_ASSERT_EQUALS(expected.d_theory, this);
+ TS_ASSERT_EQUALS(expected.d_node, n);
+ TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
+
+ return RewritingComplete(n);
+ }
+
+ std::string identify() const throw() {
+ return "Fake" + d_id;
+ }
+
+ void preRegisterTerm(TNode) { Unimplemented(); }
+ void registerTerm(TNode) { Unimplemented(); }
+ void check(Theory::Effort) { Unimplemented(); }
+ void propagate(Theory::Effort) { Unimplemented(); }
+ void explain(TNode, Theory::Effort) { Unimplemented(); }
+};/* class FakeTheory */
+
+std::deque<RewriteItem> FakeTheory::s_expected;
+
+/**
+ * Test the TheoryEngine.
+ */
+class TheoryEngineWhite : public CxxTest::TestSuite {
+ Context* d_ctxt;
+
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+ FakeOutputChannel *d_nullChannel;
+ FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv;
+ TheoryEngine* d_theoryEngine;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+
+ d_nm = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nm);
+
+ d_nullChannel = new FakeOutputChannel;
+
+ d_builtin = new FakeTheory(d_ctxt, *d_nullChannel, "Builtin");
+ d_bool = new FakeTheory(d_ctxt, *d_nullChannel, "Bool");
+ d_uf = new FakeTheory(d_ctxt, *d_nullChannel, "UF");
+ d_arith = new FakeTheory(d_ctxt, *d_nullChannel, "Arith");
+ d_arrays = new FakeTheory(d_ctxt, *d_nullChannel, "Arrays");
+ d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
+
+ d_theoryEngine = new TheoryEngine(d_ctxt);
+
+ // insert our fake versions into the theoryOf table
+ d_theoryEngine->d_theoryOfTable.
+ registerTheory(reinterpret_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
+ d_theoryEngine->d_theoryOfTable.
+ registerTheory(reinterpret_cast<theory::booleans::TheoryBool*>(d_bool));
+ d_theoryEngine->d_theoryOfTable.
+ registerTheory(reinterpret_cast<theory::uf::TheoryUF*>(d_uf));
+ d_theoryEngine->d_theoryOfTable.
+ registerTheory(reinterpret_cast<theory::arith::TheoryArith*>(d_arith));
+ d_theoryEngine->d_theoryOfTable.
+ registerTheory(reinterpret_cast<theory::arrays::TheoryArrays*>(d_arrays));
+ d_theoryEngine->d_theoryOfTable.
+ registerTheory(reinterpret_cast<theory::bv::TheoryBV*>(d_bv));
+
+ Debug.on("theory-rewrite");
+ }
+
+ void tearDown() {
+ delete d_theoryEngine;
+
+ delete d_bv;
+ delete d_arrays;
+ delete d_arith;
+ delete d_uf;
+ delete d_bool;
+ delete d_builtin;
+
+ delete d_nullChannel;
+
+ delete d_scope;
+ delete d_nm;
+
+ delete d_ctxt;
+ }
+
+ void testRewriterSimple() {
+ Node x = d_nm->mkVar("x", d_nm->integerType());
+ Node y = d_nm->mkVar("y", d_nm->integerType());
+ Node z = d_nm->mkVar("z", d_nm->integerType());
+
+ // make the expression (PLUS x y (MULT z 0))
+ Node zero = d_nm->mkConst(Rational("0"));
+ Node zTimesZero = d_nm->mkNode(MULT, z, zero);
+ Node n = d_nm->mkNode(PLUS, x, y, zTimesZero);
+
+ Node nExpected = n;
+ Node nOut;
+
+ FakeTheory::expect(PRE, d_arith, n, true);
+ FakeTheory::expect(PRE, d_arith, x, false);
+ FakeTheory::expect(POST, d_arith, x, false);
+ FakeTheory::expect(PRE, d_arith, y, false);
+ FakeTheory::expect(POST, d_arith, y, false);
+ FakeTheory::expect(PRE, d_arith, zTimesZero, false);
+ FakeTheory::expect(PRE, d_arith, z, false);
+ FakeTheory::expect(POST, d_arith, z, false);
+ FakeTheory::expect(PRE, d_arith, zero, false);
+ FakeTheory::expect(POST, d_arith, zero, false);
+ FakeTheory::expect(POST, d_arith, zTimesZero, false);
+ FakeTheory::expect(POST, d_arith, n, true);
+ nOut = d_theoryEngine->rewrite(n);
+ TS_ASSERT(FakeTheory::nothingMoreExpected());
+
+ TS_ASSERT_EQUALS(nOut, nExpected);
+ }
+
+ void testRewriterComplicated() {
+ Node x = d_nm->mkVar("x", d_nm->integerType());
+ Node y = d_nm->mkVar("y", d_nm->realType());
+ Node z1 = d_nm->mkVar("z1", d_nm->mkSort("U"));
+ Node z2 = d_nm->mkVar("z2", d_nm->mkSort("U"));
+ Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(),
+ d_nm->integerType()));
+ Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(),
+ d_nm->integerType()));
+ Node one = d_nm->mkConst(Rational("1"));
+ Node two = d_nm->mkConst(Rational("2"));
+
+ Node f1 = d_nm->mkNode(APPLY_UF, f, one);
+ Node f2 = d_nm->mkNode(APPLY_UF, f, two);
+ Node fx = d_nm->mkNode(APPLY_UF, f, x);
+ Node ffx = d_nm->mkNode(APPLY_UF, f, fx);
+ Node gy = d_nm->mkNode(APPLY_UF, g, y);
+ Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2);
+ Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2);
+ Node ffxeqgy = d_nm->mkNode(EQUAL,
+ ffx,
+ gy);
+ Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2, ffx);
+ Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1);
+ Node or1 = d_nm->mkNode(OR, and1, ffxeqf1);
+ // make the expression:
+ // (IMPLIES (EQUAL (f 1) (f 2)) (OR (AND (EQUAL (f (f x)) (g y)) (EQUAL z1 z2) (f (f x)))) (EQUAL (f (f x)) (f 1)))
+ Node n = d_nm->mkNode(IMPLIES, f1eqf2, or1);
+ Node nExpected = n;
+ Node nOut;
+
+ // We WOULD expect that the commented-out calls were made, except
+ // for the cache
+ FakeTheory::expect(PRE, d_bool, n, true);
+ FakeTheory::expect(PRE, d_uf, f1eqf2, true);
+ FakeTheory::expect(PRE, d_uf, f1, false);
+ FakeTheory::expect(PRE, d_builtin, f, true);
+ FakeTheory::expect(POST, d_builtin, f, true);
+ FakeTheory::expect(PRE, d_arith, one, true);
+ FakeTheory::expect(POST, d_arith, one, true);
+ FakeTheory::expect(POST, d_uf, f1, false);
+ FakeTheory::expect(PRE, d_uf, f2, false);
+ //FakeTheory::expect(PRE, d_builtin, f, true);
+ //FakeTheory::expect(POST, d_builtin, f, true);
+ FakeTheory::expect(PRE, d_arith, two, true);
+ FakeTheory::expect(POST, d_arith, two, true);
+ FakeTheory::expect(POST, d_uf, f2, false);
+ FakeTheory::expect(POST, d_uf, f1eqf2, true);
+ FakeTheory::expect(PRE, d_bool, or1, false);
+ FakeTheory::expect(PRE, d_bool, and1, false);
+ FakeTheory::expect(PRE, d_uf, ffxeqgy, true);
+ FakeTheory::expect(PRE, d_uf, ffx, false);
+ FakeTheory::expect(PRE, d_uf, fx, false);
+ //FakeTheory::expect(PRE, d_builtin, f, true);
+ //FakeTheory::expect(POST, d_builtin, f, true);
+ FakeTheory::expect(PRE, d_arith, x, true);
+ FakeTheory::expect(POST, d_arith, x, true);
+ FakeTheory::expect(POST, d_uf, fx, false);
+ FakeTheory::expect(POST, d_uf, ffx, false);
+ FakeTheory::expect(PRE, d_uf, gy, false);
+ FakeTheory::expect(PRE, d_builtin, g, true);
+ FakeTheory::expect(POST, d_builtin, g, true);
+ FakeTheory::expect(PRE, d_arith, y, true);
+ FakeTheory::expect(POST, d_arith, y, true);
+ FakeTheory::expect(POST, d_uf, gy, false);
+ FakeTheory::expect(POST, d_uf, ffxeqgy, true);
+ FakeTheory::expect(PRE, d_uf, z1eqz2, true);
+ FakeTheory::expect(PRE, d_uf, z1, false);
+ FakeTheory::expect(POST, d_uf, z1, false);
+ FakeTheory::expect(PRE, d_uf, z2, false);
+ FakeTheory::expect(POST, d_uf, z2, false);
+ FakeTheory::expect(POST, d_uf, z1eqz2, true);
+ // tricky one: ffx is in cache but for a non-topLevel !
+ FakeTheory::expect(PRE, d_uf, ffx, true);
+ //FakeTheory::expect(PRE, d_uf, fx, false);
+ //FakeTheory::expect(POST, d_uf, fx, false);
+ FakeTheory::expect(POST, d_uf, ffx, true);
+ FakeTheory::expect(POST, d_bool, and1, false);
+ FakeTheory::expect(PRE, d_uf, ffxeqf1, true);
+ //FakeTheory::expect(PRE, d_uf, ffx, false);
+ //FakeTheory::expect(POST, d_uf, ffx, false);
+ //FakeTheory::expect(PRE, d_uf, f1, false);
+ //FakeTheory::expect(POST, d_uf, f1, false);
+ FakeTheory::expect(POST, d_uf, ffxeqf1, true);
+ FakeTheory::expect(POST, d_bool, or1, false);
+ FakeTheory::expect(POST, d_bool, n, true);
+ nOut = d_theoryEngine->rewrite(n);
+ TS_ASSERT(FakeTheory::nothingMoreExpected());
+
+ TS_ASSERT_EQUALS(nOut, nExpected);
+ }
+};
projects / cvc5.git / commitdiff