From: Dejan Jovanović Date: Fri, 11 Dec 2009 04:00:14 +0000 (+0000) Subject: Extracted the public Expr and ExprManager interface to encapsulate the optimized... X-Git-Tag: cvc5-1.0.0~9378 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d26cd7a159bb56f492e21b7536f68abf821ca02a;p=cvc5.git Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager. --- diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6ca68d35c..b8606e051 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -9,11 +9,16 @@ libexpr_la_SOURCES = \ attr_var_name.h \ node.h \ node_builder.h \ + expr.h \ expr_value.h \ node_manager.h \ + expr_manager.h \ node_attribute.h \ kind.h \ node.cpp \ node_builder.cpp \ node_manager.cpp \ - expr_value.cpp + expr_manager.cpp \ + expr_value.cpp \ + expr.cpp + diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index a668e8876..6b1555e6c 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -53,7 +53,7 @@ CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libexpr_la_LIBADD = am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \ - expr_value.lo + expr_manager.lo expr_value.lo expr.lo libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -225,14 +225,18 @@ libexpr_la_SOURCES = \ attr_var_name.h \ node.h \ node_builder.h \ + expr.h \ expr_value.h \ node_manager.h \ + expr_manager.h \ node_attribute.h \ kind.h \ node.cpp \ node_builder.cpp \ node_manager.cpp \ - expr_value.cpp + expr_manager.cpp \ + expr_value.cpp \ + expr.cpp all: all-am @@ -286,6 +290,8 @@ mostlyclean-compile: distclean-compile: -rm -f *.tab.c +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@ diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp new file mode 100644 index 000000000..af685aced --- /dev/null +++ b/src/expr/expr.cpp @@ -0,0 +1,154 @@ +/* + * expr.cpp + * + * Created on: Dec 10, 2009 + * Author: dejan + */ + +#include "expr/expr.h" +#include "expr/node.h" +#include "util/Assert.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const Expr& e) { + e.toStream(out); + return out; +} + +Expr::Expr() : + d_node(new Node()), d_em(NULL) { +} + +Expr::Expr(ExprManager* em, Node* node) : + d_node(node), d_em(em) { +} + +Expr::Expr(const Expr& e) : + d_node(new Node(*e.d_node)), d_em(e.d_em) { +} + +ExprManager* Expr::getExprManager() const { + return d_em; +} + +Expr::~Expr() { + delete d_node; +} + +Expr& Expr::operator=(const Expr& e) { + if(this != &e) { + delete d_node; + d_node = new Node(*e.d_node); + d_em = e.d_em; + } + return *this; +} + +bool Expr::operator==(const Expr& e) const { + if(d_em != e.d_em) + return false;Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + return *d_node == *e.d_node; +} + +bool Expr::operator!=(const Expr& e) const { + return !(*this == e); +} + +bool Expr::operator<(const Expr& e) const { + Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + if(d_em != e.d_em) + return false; + return *d_node < *e.d_node; +} + +uint64_t Expr::hash() const { + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return (d_node->isNull()); +} + +Kind Expr::getKind() const { + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->getKind(); +} + +size_t Expr::numChildren() const { + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->numChildren(); +} + +std::string Expr::toString() const { + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->toString(); +} + +bool Expr::isNull() const { + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->isNull(); +} + +void Expr::toStream(std::ostream& out) const { + d_node->toStream(out); +} + +Node Expr::getNode() const { + return *d_node; +} + +BoolExpr::BoolExpr() { +} + +BoolExpr::BoolExpr(const Expr& e) : + Expr(e) { +} + +BoolExpr BoolExpr::notExpr() const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + return d_em->mkExpr(NOT, *this); +} + +BoolExpr BoolExpr::andExpr(const BoolExpr& e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == e.d_em, "Different expression managers!"); + return d_em->mkExpr(AND, *this, e); +} + +BoolExpr BoolExpr::orExpr(const BoolExpr& e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == e.d_em, "Different expression managers!"); + return d_em->mkExpr(OR, *this, e); +} + +BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == e.d_em, "Different expression managers!"); + return d_em->mkExpr(XOR, *this, e); +} + +BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == e.d_em, "Different expression managers!"); + return d_em->mkExpr(IFF, *this, e); +} + +BoolExpr BoolExpr::impExpr(const BoolExpr& e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == e.d_em, "Different expression managers!"); + return d_em->mkExpr(IMPLIES, *this, e); +} + +BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == then_e.d_em, "Different expression managers!"); + Assert(d_em == else_e.d_em, "Different expression managers!"); + return d_em->mkExpr(ITE, *this, then_e, else_e); +} + +Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const { + Assert(d_em != NULL, "Don't have an expression manager for this expression!"); + Assert(d_em == then_e.getExprManager(), "Different expression managers!"); + Assert(d_em == else_e.getExprManager(), "Different expression managers!"); + return d_em->mkExpr(ITE, *this, then_e, else_e); +} + +} // End namespace CVC4 diff --git a/src/expr/expr.h b/src/expr/expr.h new file mode 100644 index 000000000..dc1926ce7 --- /dev/null +++ b/src/expr/expr.h @@ -0,0 +1,233 @@ +/* + * expr.h + * + * Created on: Dec 10, 2009 + * Author: dejan + */ + +#ifndef __CVC4__EXPR_H +#define __CVC4__EXPR_H + +#include "cvc4_config.h" +#include "expr/expr_manager.h" + +#include +#include +#include + +namespace CVC4 { + +// The internal expression representation +class Node; + +/** + * Class encapsulating CVC4 expressions and methods for constructing new + * expressions. + */ +class CVC4_PUBLIC Expr { + +public: + + /** Default constructor, makes a null expression. */ + Expr(); + + /** + * Copy constructor, makes a copy of a given expression + * @param the expression to copy + */ + Expr(const Expr& e); + + /** Destructor */ + ~Expr(); + + /** + * Assignment operator, makes a copy of the given expression. If the + * expression managers of the two expressions differ, the expression of + * the given expression will be used. + * @param e the expression to assign + * @return the reference to this expression after assignment + */ + Expr& operator=(const Expr& e); + + /** + * Syntactic comparison operator. Returns true if expressions belong to the + * same expression manager and are syntactically identical. + * @param e the expression to compare to + * @return true if expressions are syntactically the same, false otherwise + */ + bool operator==(const Expr& e) const; + + /** + * Syntactic dis-equality operator. + * @param e the expression to compare to + * @return true if expressions differ syntactically, false otherwise + */ + bool operator!=(const Expr& e) const; + + /** + * Order comparison operator. The only invariant on the order of expressions + * is that the expressions that were created sooner will be smaller in the + * ordering than all the expressions created later. Null expression is the + * smallest element of the ordering. The behavior of the operator is + * undefined if the expressions come from two different expression managers. + * @param e the expression to compare to + * @return true if this expression is smaller than the given one + */ + bool operator<(const Expr& e) const; + + /** + * Returns the hash value of the expression. Equal expression will have the + * same hash value. + */ + uint64_t hash() const; + + /** + * Returns the kind of the expression (AND, PLUS ...). + * @return the kind of the expression + */ + Kind getKind() const; + + /** + * Returns the number of children of this expression. + * @return the number of children + */ + size_t numChildren() const; + + /** + * Returns the string representation of the expression. + */ + std::string toString() const; + + /** + * Outputs the string representation of the expression to the stream. + * @param the output stream + */ + void toStream(std::ostream& out) const; + + /** + * Check if this is a null expression. + * @return true if a null expression + */ + bool isNull() const; + + /** + * Returns the expression reponsible for this expression. + */ + ExprManager* getExprManager() const; + +protected: + + /** + * Constructor for internal purposes. + * @param em the expression manager that handles this expression + * @param node the actuall expression node pointer + */ + Expr(ExprManager* em, Node* node); + + /** The internal expression representation */ + Node* d_node; + + /** The responsible expression manager */ + ExprManager* d_em; + + /** + * Returns the actual internal node. + * @return the internal node + */ + Node getNode() const; + + // Friend to access the actual internal node information and private methods*/ + friend class SmtEngine; + friend class ExprManager; +}; + +/** + * Output operator for expressions + * @param out the stream to output to + * @param e the expression to output + * @return the stream + */ +std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC; + +/** + * Extending the expression with the capability to construct Boolean + * expressions. + */ +class CVC4_PUBLIC BoolExpr : public Expr { + +public: + + /** Default constructor, makes a null expression */ + BoolExpr(); + + /** + * Convert an expression to a Boolean expression + */ + BoolExpr(const Expr& e); + + /** + * Negate this expression. + * @return the logical negation of this expression. + */ + BoolExpr notExpr() const; + + /** + * Conjunct the given expression to this expression. + * @param e the expression to conjunct + * @return the conjunction of this expression and e + */ + BoolExpr andExpr(const BoolExpr& e) const; + + /** + * Disjunct the given expression to this expression. + * @param e the expression to disjunct + * @return the disjunction of this expression and e + */ + BoolExpr orExpr(const BoolExpr& e) const; + + /** + * Make an exclusive or expression out of this expression and the given + * expression. + * @param e the right side of the xor + * @return the xor of this expression and e + */ + BoolExpr xorExpr(const BoolExpr& e) const; + + /** + * Make an equivalence expression out of this expression and the given + * expression. + * @param e the right side of the equivalence + * @return the equivalence expression + */ + BoolExpr iffExpr(const BoolExpr& e) const; + + /** + * Make an implication expression out of this expression and the given + * expression. + * @param e the right side of the equivalence + * @return the equivalence expression + */ + BoolExpr impExpr(const BoolExpr& e) const; + + /** + * Make a Boolean if-then-else expression using this expression as the + * condition, and given the then and else parts + * @param then_e the then branch expression + * @param else_e the else branch expression + * @return the if-then-else expression + */ + BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const; + + /** + * Make a term if-then-else expression using this expression as the + * condition, and given the then and else parts + * @param then_e the then branch expression + * @param else_e the else branch expression + * @return the if-then-else expression + */ + Expr iteExpr(const Expr& then_e, const Expr& else_e) const; +}; + +} + +#endif /* __CVC4__EXPR_H */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp new file mode 100644 index 000000000..877ba9d3c --- /dev/null +++ b/src/expr/expr_manager.cpp @@ -0,0 +1,78 @@ +/* + * expr_manager.cpp + * + * Created on: Dec 10, 2009 + * Author: dejan + */ + +#include "expr/node.h" +#include "expr/expr.h" +#include "expr/node_manager.h" +#include "expr/expr_manager.h" + +using namespace std; + +namespace CVC4 { + +ExprManager::ExprManager() +: d_nm(new NodeManager()) { +} + +ExprManager::~ExprManager() { + delete d_nm; +} + +Expr ExprManager::mkExpr(Kind kind) { + return Expr(this, new Node(d_nm->mkExpr(kind))); +} + +Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { + return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode()))); +} + +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { + return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(), + child2.getNode()))); +} + +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, + const Expr& child3) { + return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(), + child2.getNode(), child3.getNode()))); +} + +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, + const Expr& child3, const Expr& child4) { + return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(), + child2.getNode(), child3.getNode(), + child4.getNode()))); +} + +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, + const Expr& child3, const Expr& child4, + const Expr& child5) { + return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(), + child2.getNode(), child3.getNode(), + child5.getNode()))); +} + +Expr ExprManager::mkExpr(Kind kind, const vector& children) { + vector nodes; + vector::const_iterator it = children.begin(); + vector::const_iterator it_end = children.end(); + while(it != it_end) { + nodes.push_back(it->getNode()); + ++it; + } + return Expr(this, new Node(d_nm->mkExpr(kind, nodes))); +} + +Expr ExprManager::mkVar() { + return Expr(this, new Node(d_nm->mkVar())); +} + +NodeManager* ExprManager::getNodeManager() const { + return d_nm; +} + +} // End namespace CVC4 diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h new file mode 100644 index 000000000..4a7f359e9 --- /dev/null +++ b/src/expr/expr_manager.h @@ -0,0 +1,93 @@ +/* + * expr_manager.h + * + * Created on: Dec 10, 2009 + * Author: dejan + */ + +#ifndef __CVC4__EXPR_MANAGER_H +#define __CVC4__EXPR_MANAGER_H + +#include "cvc4_config.h" +#include "expr/kind.h" +#include + +namespace CVC4 { + +class Expr; +class NodeManager; +class SmtEngine; + +class CVC4_PUBLIC ExprManager { + +public: + + /** + * Creates an expressio manager. + */ + ExprManager(); + + /** + * Destroys the expression manager. No will be deallocated at this point, so + * any expression references that used to be managed by this expression + * manager and are left-over are bad. + */ + ~ExprManager(); + + /** + * Make a unary expression of a given kind (TRUE, FALSE,...). + * @param kind the kind of expression + * @return the expression + */ + Expr mkExpr(Kind kind); + + /** + * Make a unary expression of a given kind (NOT, BVNOT, ...). + * @param kind the kind of expression + * @return the expression + */ + Expr mkExpr(Kind kind, const Expr& child1); + + /** + * Make a ternary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @return the expression + */ + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2); + + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, + const Expr& child3); + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, + const Expr& child3, const Expr& child4); + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, + const Expr& child3, const Expr& child4, const Expr& child5); + + /** + * Make an n-ary expression of given kind given a vector of it's children + * @param kind the kind of expression to build + * @param children the subexpressions + * @return the n-ary expression + */ + Expr mkExpr(Kind kind, const std::vector& children); + + // variables are special, because duplicates are permitted + Expr mkVar(); + +private: + + /** The internal node manager */ + NodeManager* d_nm; + + /** + * Returns the internal node manager. This should only be used by internal + * users, i.e. the friend classes. + */ + NodeManager* getNodeManager() const; + + /** SmtEngine will use all the internals, so it will grab the node manager */ + friend class SmtEngine; +}; + +} + +#endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index 9ce7c3e12..af064f43d 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -15,6 +15,9 @@ **/ #include "expr_value.h" +#include + +using namespace std; namespace CVC4 { @@ -77,7 +80,13 @@ ExprValue::const_iterator ExprValue::rend() const { return d_children - 1; } -void ExprValue::toString(std::ostream& out) const { +string ExprValue::toString() const { + stringstream ss; + toStream(ss); + return ss.str(); +} + +void ExprValue::toStream(std::ostream& out) const { out << "(" << Kind(d_kind); if(d_kind == VARIABLE) { out << ":" << this; diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 10f09e565..25fada4af 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -25,6 +25,8 @@ #include #include "kind.h" +#include + namespace CVC4 { class Node; @@ -112,7 +114,8 @@ public: unsigned getId() const { return d_id; } unsigned getKind() const { return (Kind) d_kind; } - void CVC4_PUBLIC toString(std::ostream& out) const; + std::string toString() const; + void toStream(std::ostream& out) const; }; }/* CVC4::expr namespace */ diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 22a905470..be9ac995c 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -15,7 +15,10 @@ #include "expr/node_builder.h" #include "util/Assert.h" +#include + using namespace CVC4::expr; +using namespace std; namespace CVC4 { @@ -23,6 +26,11 @@ ExprValue ExprValue::s_null; Node Node::s_null(&ExprValue::s_null); +Node Node::null() { + return s_null; +} + + bool Node::isNull() const { return d_ev == &ExprValue::s_null; } @@ -82,12 +90,6 @@ Node Node::notExpr() const { return NodeManager::currentEM()->mkExpr(NOT, *this); } -// FIXME: What does this do and why? -Node Node::negate() const { // avoid double-negatives - return NodeBuilder(*this).negate(); -} - - Node Node::andExpr(const Node& right) const { return NodeManager::currentEM()->mkExpr(AND, *this, right); } diff --git a/src/expr/node.h b/src/expr/node.h index aec50000e..98847e428 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -10,10 +10,11 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#ifndef __CVC4__EXPR_H -#define __CVC4__EXPR_H +#ifndef __CVC4__NODE_H +#define __CVC4__NODE_H #include +#include #include #include @@ -26,7 +27,7 @@ namespace CVC4 { namespace CVC4 { -inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream&, const Node&); class NodeManager; @@ -40,7 +41,7 @@ using CVC4::expr::ExprValue; * Encapsulation of an ExprValue pointer. The reference count is * maintained in the ExprValue. */ -class CVC4_PUBLIC Node { +class Node { friend class ExprValue; @@ -99,7 +100,6 @@ public: Node eqExpr(const Node& right) const; Node notExpr() const; - Node negate() const; // avoid double-negatives Node andExpr(const Node& right) const; Node orExpr(const Node& right) const; Node iteExpr(const Node& thenpart, const Node& elsepart) const; @@ -115,7 +115,7 @@ public: inline size_t numChildren() const; - static Node null() { return s_null; } + static Node null(); typedef Node* iterator; typedef Node const* const_iterator; @@ -125,7 +125,8 @@ public: inline const_iterator begin() const; inline const_iterator end() const; - void toString(std::ostream&) const; + inline std::string toString() const; + inline void toStream(std::ostream&) const; bool isNull() const; @@ -142,7 +143,7 @@ inline bool Node::operator<(const Node& e) const { } inline std::ostream& operator<<(std::ostream& out, const Node& e) { - e.toString(out); + e.toStream(out); return out; } @@ -150,10 +151,12 @@ inline Kind Node::getKind() const { return Kind(d_ev->d_kind); } -inline void Node::toString(std::ostream& out) const { - if(d_ev) - d_ev->toString(out); - else out << "null"; +inline std::string Node::toString() const { + return d_ev->toString(); +} + +inline void Node::toStream(std::ostream& out) const { + d_ev->toStream(out); } inline Node::iterator Node::begin() { @@ -178,4 +181,4 @@ inline size_t Node::numChildren() const { }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_H */ +#endif /* __CVC4__NODE_H */ diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h index b978f097d..0b759efb4 100644 --- a/src/expr/node_attribute.h +++ b/src/expr/node_attribute.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H -#define __CVC4__EXPR__EXPR_ATTRIBUTE_H +#ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H +#define __CVC4__EXPR__NODE_ATTRIBUTE_H #include #include "config.h" diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 83d2ae41d..7d30ff4e3 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -104,15 +104,6 @@ NodeBuilder& NodeBuilder::notExpr() { return *this; } -// avoid double-negatives -NodeBuilder& NodeBuilder::negate() { - if(EXPECT_FALSE( d_kind == NOT )) - return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND ); - collapse(); - d_kind = NOT; - return *this; -} - NodeBuilder& NodeBuilder::andExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(d_kind != AND) { diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index be96c2e77..5be3c284d 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4__EXPR_BUILDER_H -#define __CVC4__EXPR_BUILDER_H +#ifndef __CVC4__NODE_BUILDER_H +#define __CVC4__NODE_BUILDER_H #include #include @@ -78,7 +78,6 @@ public: // Compound expression constructors NodeBuilder& eqExpr(const Node& right); NodeBuilder& notExpr(); - NodeBuilder& negate(); // avoid double-negatives NodeBuilder& andExpr(const Node& right); NodeBuilder& orExpr(const Node& right); NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart); @@ -209,7 +208,9 @@ inline NodeBuilder::operator Node() { // variables are permitted to be duplicates (from POV of the expression manager) if(d_kind == VARIABLE) { ev = new ExprValue; - hash = reinterpret_cast(ev); + ev->d_kind = d_kind; + ev->d_id = ExprValue::next_id++;// FIXME multithreading + return Node(ev); } else { if(d_nchildren <= nchild_thresh) { hash = ExprValue::computeHash(d_kind, ev_begin(), ev_end()); @@ -220,7 +221,7 @@ inline NodeBuilder::operator Node() { ev_iterator i_end = ev_end(); for(; i != i_end; ++i) { // The expressions in the allocated children are all 0, so we must - // construct it withouth using an assignment operator + // construct it without using an assignment operator ev->d_children[nc++].assignExprValue(*i); } } else { @@ -286,7 +287,7 @@ inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { } inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { - d_eb.append(e.negate()); + d_eb.append(e.uMinusExpr()); return *this; } @@ -310,4 +311,4 @@ inline MultExprBuilder& MultExprBuilder::operator*(Node e) { }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_BUILDER_H */ +#endif /* __CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 3c15aa9c4..8da87c9eb 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -82,7 +82,7 @@ Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, cons } // N-ary version -Node NodeManager::mkExpr(Kind kind, std::vector children) { +Node NodeManager::mkExpr(Kind kind, const std::vector& children) { return NodeBuilder(this, kind).append(children); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ca15d88b4..6c20b29e8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4__EXPR_MANAGER_H -#define __CVC4__EXPR_MANAGER_H +#ifndef __CVC4__NODE_MANAGER_H +#define __CVC4__NODE_MANAGER_H #include #include @@ -24,7 +24,7 @@ namespace expr { class ExprBuilder; }/* CVC4::expr namespace */ -class CVC4_PUBLIC NodeManager { +class NodeManager { static __thread NodeManager* s_current; friend class CVC4::NodeBuilder; @@ -45,7 +45,7 @@ public: Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4); Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5); // N-ary version - Node mkExpr(Kind kind, std::vector children); + Node mkExpr(Kind kind, const std::vector& children); // variables are special, because duplicates are permitted Node mkVar(); diff --git a/src/main/main.cpp b/src/main/main.cpp index c7e23aee2..d9d3988f1 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,7 +22,7 @@ #include "parser/parser.h" #include "parser/smt/smt_parser.h" #include "parser/cvc/cvc_parser.h" -#include "expr/node_manager.h" +#include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "util/command.h" #include "util/output.h" @@ -53,7 +53,7 @@ int main(int argc, char *argv[]) { throw new Exception("Too many input files specified."); // Create the expression manager - NodeManager exprMgr; + ExprManager exprMgr; // Create the SmtEngine SmtEngine smt(&exprMgr, &options); diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index d81336b53..a50b1f18f 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -65,29 +65,29 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : antlr::LLkParser(lexer, k) { } -Node AntlrParser::getVariable(std::string var_name) { - Node e = d_var_symbol_table.getObject(var_name); +Expr AntlrParser::getVariable(std::string var_name) { + Expr e = d_var_symbol_table.getObject(var_name); Debug("parser") << "getvar " << var_name << " gives " << e << endl; return e; } -Node AntlrParser::getTrueExpr() const { +Expr AntlrParser::getTrueExpr() const { return d_expr_manager->mkExpr(TRUE); } -Node AntlrParser::getFalseExpr() const { +Expr AntlrParser::getFalseExpr() const { return d_expr_manager->mkExpr(FALSE); } -Node AntlrParser::newExpression(Kind kind, const Node& child) { +Expr AntlrParser::newExpression(Kind kind, const Expr& child) { return d_expr_manager->mkExpr(kind, child); } -Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) { +Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) { return d_expr_manager->mkExpr(kind, child_1, child_2); } -Node AntlrParser::newExpression(Kind kind, const std::vector& children) { +Expr AntlrParser::newExpression(Kind kind, const std::vector& children) { return d_expr_manager->mkExpr(kind, children); } @@ -112,7 +112,7 @@ void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { void AntlrParser::addExtraSorts(const std::vector& extra_sorts) { } -void AntlrParser::setExpressionManager(NodeManager* em) { +void AntlrParser::setExpressionManager(ExprManager* em) { d_expr_manager = em; } @@ -132,7 +132,7 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Node AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< +Expr AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< Kind>& kinds) { return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } @@ -154,7 +154,7 @@ unsigned AntlrParser::findPivot(const std::vector& kinds, return pivot; } -Node AntlrParser::createPrecedenceExpr(const std::vector& exprs, +Expr AntlrParser::createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index) { if(start_index == end_index) @@ -162,8 +162,8 @@ Node AntlrParser::createPrecedenceExpr(const std::vector& exprs, unsigned pivot = findPivot(kinds, start_index, end_index - 1); - Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); - Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); + Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); + Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 26f206e43..ad23d45f8 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -15,8 +15,8 @@ #include #include -#include "expr/node.h" -#include "expr/node_manager.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" #include "util/command.h" #include "util/Assert.h" #include "parser/symbol_table.h" @@ -48,7 +48,7 @@ public: * Set's the expression manager to use when creating/managing expression. * @param expr_manager the expression manager */ - void setExpressionManager(NodeManager* expr_manager); + void setExpressionManager(ExprManager* expr_manager); protected: @@ -89,7 +89,7 @@ protected: * @param var_name the name of the variable * @return the variable expression */ - Node getVariable(std::string var_name); + Expr getVariable(std::string var_name); /** * Types of symbols. @@ -113,40 +113,40 @@ protected: * Returns the true expression. * @return the true expression */ - Node getTrueExpr() const; + Expr getTrueExpr() const; /** * Returns the false expression. * @return the false expression */ - Node getFalseExpr() const; + Expr getFalseExpr() const; /** * Creates a new unary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param child the child */ - Node newExpression(Kind kind, const Node& child); + Expr newExpression(Kind kind, const Expr& child); /** * Creates a new binary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Node newExpression(Kind kind, const Node& child_1, const Node& child_2); + Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2); /** * Creates a new CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Node newExpression(Kind kind, const std::vector& children); + Expr newExpression(Kind kind, const std::vector& children); /** * Creates a new expression based on the given string of expressions and kinds. * The expression is created so that it respects the kinds precedence table. */ - Node createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds); + Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds); /** * Creates a new predicated over the given sorts. @@ -193,16 +193,16 @@ private: * Creates a new expression based on the given string of expressions and kinds. * The expression is created so that it respects the kinds precedence table. */ - Node createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); + Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); /** The status of the benchmark */ BenchmarkStatus d_benchmark_status; /** The expression manager */ - NodeManager* d_expr_manager; + ExprManager* d_expr_manager; /** The symbol table lookup */ - SymbolTable d_var_symbol_table; + SymbolTable d_var_symbol_table; }; std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status); diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp index 2bb01007a..adeb5761d 100644 --- a/src/parser/cvc/cvc_parser.cpp +++ b/src/parser/cvc/cvc_parser.cpp @@ -44,8 +44,8 @@ Command* CvcParser::parseNextCommand() throw(ParserException) { return cmd; } -Node CvcParser::parseNextExpression() throw(ParserException) { - Node result; +Expr CvcParser::parseNextExpression() throw(ParserException) { + Expr result; if(!done()) { try { result = d_antlr_parser->formula(); @@ -62,7 +62,7 @@ CvcParser::~CvcParser() { delete d_antlr_lexer; } -CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) : +CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) : Parser(em), d_input(input) { if(!d_input) { throw ParserException(string("Read error") + diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 812925b0b..625f2c381 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -34,7 +34,7 @@ options { */ command returns [CVC4::Command* cmd = 0] { - Node f; + Expr f; vector ids; } : ASSERT f = formula { cmd = new AssertCommand(f); } @@ -60,15 +60,15 @@ type : BOOLEAN ; -formula returns [CVC4::Node formula] +formula returns [CVC4::Expr formula] : formula = bool_formula ; -bool_formula returns [CVC4::Node formula] +bool_formula returns [CVC4::Expr formula] { - vector formulas; + vector formulas; vector kinds; - Node f1, f2; + Expr f1, f2; Kind k; } : f1 = primary_bool_formula { formulas.push_back(f1); } @@ -79,7 +79,7 @@ bool_formula returns [CVC4::Node formula] } ; -primary_bool_formula returns [CVC4::Node formula] +primary_bool_formula returns [CVC4::Expr formula] : formula = bool_atom | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } | LPAREN formula = bool_formula RPAREN @@ -93,7 +93,7 @@ bool_operator returns [CVC4::Kind kind] | IFF { kind = CVC4::IFF; } ; -bool_atom returns [CVC4::Node atom] +bool_atom returns [CVC4::Expr atom] { string p; } diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h index 07699916f..9cb6b7594 100644 --- a/src/parser/cvc/cvc_parser.h +++ b/src/parser/cvc/cvc_parser.h @@ -37,7 +37,7 @@ public: * @param input the input stream to parse * @param file_name the name of the file (for diagnostic output) */ - CvcParser(NodeManager* em, std::istream& input, const char* file_name = ""); + CvcParser(ExprManager* em, std::istream& input, const char* file_name = ""); /** * Destructor. @@ -57,7 +57,7 @@ public: * Parses the next complete expression of the stream. * @return the expression parsed */ - Node parseNextExpression() throw(ParserException); + Expr parseNextExpression() throw(ParserException); protected: diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c6d5bcb5c..8d4af5ba1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { namespace parser { -Parser::Parser(NodeManager* em) : +Parser::Parser(ExprManager* em) : d_expr_manager(em), d_done(false) { } diff --git a/src/parser/parser.h b/src/parser/parser.h index 7f63261c7..7755d65f0 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -22,9 +22,9 @@ namespace CVC4 { // Forward declarations -class Node; +class Expr; class Command; -class NodeManager; +class ExprManager; namespace parser { @@ -44,7 +44,7 @@ public: * Construct the parser that uses the given expression manager. * @param em the expression manager. */ - Parser(NodeManager* em); + Parser(ExprManager* em); /** * Destructor. @@ -60,7 +60,7 @@ public: /** * Parse the next expression of the stream */ - virtual Node parseNextExpression() throw (ParserException) = 0; + virtual Expr parseNextExpression() throw (ParserException) = 0; /** * Check if we are done -- either the end of input has been reached. @@ -73,7 +73,7 @@ protected: void setDone(bool done = true); /** Expression manager the parser will be using */ - NodeManager* d_expr_manager; + ExprManager* d_expr_manager; /** Are we done */ bool d_done; diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp index 411866540..65d36690c 100644 --- a/src/parser/smt/smt_parser.cpp +++ b/src/parser/smt/smt_parser.cpp @@ -41,8 +41,8 @@ Command* SmtParser::parseNextCommand() throw(ParserException) { return cmd; } -Node SmtParser::parseNextExpression() throw(ParserException) { - Node result; +Expr SmtParser::parseNextExpression() throw(ParserException) { + Expr result; if(!done()) { try { result = d_antlr_parser->an_formula(); @@ -59,7 +59,7 @@ SmtParser::~SmtParser() { delete d_antlr_lexer; } -SmtParser::SmtParser(NodeManager* em, istream& input, const char* file_name) : +SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) : Parser(em), d_input(input) { if(!d_input) { throw ParserException(string("Read error") + diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index c2f5c145b..b1bb35e6f 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -60,7 +60,7 @@ pred_symb returns [std::string p] /** * Matches a propositional atom from the input. */ -prop_atom returns [CVC4::Node atom] +prop_atom returns [CVC4::Expr atom] { std::string p; } @@ -78,14 +78,14 @@ prop_atom returns [CVC4::Node atom] * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined * here in order to get rid of the ugly antlr non-determinism warrnings. */ -an_atom returns [CVC4::Node atom] +an_atom returns [CVC4::Expr atom] : atom = prop_atom ; /** * Matches on of the unary Boolean conectives. */ -connective returns [CVC4::Kind kind] +bool_connective returns [CVC4::Kind kind] : NOT { kind = CVC4::NOT; } | IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } @@ -97,18 +97,18 @@ connective returns [CVC4::Kind kind] /** * Matches an annotated formula. */ -an_formula returns [CVC4::Node formula] +an_formula returns [CVC4::Expr formula] { Kind kind; - vector children; + vector children; } : formula = an_atom - | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } + | LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } ; -an_formulas[std::vector& formulas] +an_formulas[std::vector& formulas] { - Node f; + Expr f; } : ( f = an_formula { formulas.push_back(f); } )+ ; @@ -149,7 +149,7 @@ status returns [ AntlrParser::BenchmarkStatus status ] bench_attribute returns [ Command* smt_command = 0] { BenchmarkStatus b_status = SMT_UNKNOWN; - Node formula; + Expr formula; vector sorts; } : C_LOGIC IDENTIFIER diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index 7dedcd5b4..a68f0e783 100644 --- a/src/parser/smt/smt_parser.h +++ b/src/parser/smt/smt_parser.h @@ -37,7 +37,7 @@ public: * @param input the input stream to parse * @param file_name the name of the file (for diagnostic output) */ - SmtParser(NodeManager* em, std::istream& input, const char* file_name = ""); + SmtParser(ExprManager* em, std::istream& input, const char* file_name = ""); /** * Destructor. @@ -57,7 +57,7 @@ public: * Parses the next complete expression of the stream. * @return the expression parsed */ - Node parseNextExpression() throw(ParserException); + Expr parseNextExpression() throw(ParserException); protected: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4ccdd07d0..723263177 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -15,24 +15,39 @@ namespace CVC4 { +SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : + d_public_em(em), + d_em(em->getNodeManager()), + d_opts(opts), + d_de(), + d_te(), + d_prop(d_de, d_te) { + } + +SmtEngine::~SmtEngine() { + +} + void SmtEngine::doCommand(Command* c) { c->invoke(this); } -Node SmtEngine::preprocess(Node e) { +Node SmtEngine::preprocess(const Node& e) { return e; } -void SmtEngine::processAssertionList() { +Node SmtEngine::processAssertionList() { + Node asserts; for(std::vector::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) - d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i); + asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i); + return asserts; } Result SmtEngine::check() { - processAssertionList(); - d_prop.solve(d_expr); + Node asserts = processAssertionList(); + d_prop.solve(asserts); return Result(Result::VALIDITY_UNKNOWN); } @@ -41,25 +56,25 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEngine::addFormula(Node e) { +void SmtEngine::addFormula(const Node& e) { d_assertions.push_back(e); } -Result SmtEngine::checkSat(Node e) { - e = preprocess(e); - addFormula(e); +Result SmtEngine::checkSat(const BoolExpr& e) { + Node node_e = preprocess(e.getNode()); + addFormula(node_e); return check(); } -Result SmtEngine::query(Node e) { - e = preprocess(e); - addFormula(e); +Result SmtEngine::query(const BoolExpr& e) { + Node node_e = preprocess(e.getNode()); + addFormula(node_e); return check(); } -Result SmtEngine::assertFormula(Node e) { - e = preprocess(e); - addFormula(e); +Result SmtEngine::assertFormula(const BoolExpr& e) { + Node node_e = preprocess(e.getNode()); + addFormula(node_e); return quickCheck(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c4addc7dd..edcbdcca3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -16,7 +16,9 @@ #include "cvc4_config.h" #include "expr/node.h" +#include "expr/expr.h" #include "expr/node_manager.h" +#include "expr/expr_manager.h" #include "util/result.h" #include "util/model.h" #include "util/options.h" @@ -42,73 +44,19 @@ class Command; // // The CNF conversion can go on in PropEngine. -class SmtEngine { - /** Current set of assertions. */ - // TODO: make context-aware to handle user-level push/pop. - std::vector d_assertions; - - /** Our expression manager */ - NodeManager *d_em; - - /** User-level options */ - Options *d_opts; - - /** Expression built-up for handing off to the propagation engine */ - Node d_expr; - - /** The decision engine */ - DecisionEngine d_de; - - /** The decision engine */ - TheoryEngine d_te; - - /** The propositional engine */ - PropEngine d_prop; - - /** - * Pre-process an Node. This is expected to be highly-variable, - * with a lot of "source-level configurability" to add multiple - * passes over the Node. TODO: may need to specify a LEVEL of - * preprocessing (certain contexts need more/less ?). - */ - Node preprocess(Node); +class CVC4_PUBLIC SmtEngine { - /** - * Adds a formula to the current context. - */ - void addFormula(Node); - - /** - * Full check of consistency in current context. Returns true iff - * consistent. - */ - Result check(); +public: /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). + * Construct an SmtEngine with the given expression manager and user options. */ - Result quickCheck(); + SmtEngine(ExprManager* em, Options* opts) throw(); /** - * Process the assertion list: for literals and conjunctions of - * literals, assert to T-solver. - */ - void processAssertionList(); - -public: - /* - * Construct an SmtEngine with the given expression manager and user options. + * Destruct the smt engine. */ - SmtEngine(NodeManager* em, Options* opts) throw() : - d_em(em), - d_opts(opts), - d_expr(Node::null()), - d_de(), - d_te(), - d_prop(d_de, d_te) { - } + ~SmtEngine(); /** * Execute a command. @@ -121,25 +69,25 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(Node); + Result assertFormula(const BoolExpr& e); /** * Add a formula to the current context and call check(). Returns * true iff consistent. */ - Result query(Node); + Result query(const BoolExpr& e); /** * Add a formula to the current context and call check(). Returns * true iff consistent. */ - Result checkSat(Node); + Result checkSat(const BoolExpr& e); /** * Simplify a formula without doing "much" work. Requires assist * from the SAT Engine. */ - Node simplify(Node); + Expr simplify(const Expr& e); /** * Get a (counter)model (only if preceded by a SAT or INVALID query. @@ -155,6 +103,64 @@ public: * Pop a user-level context. Throws an exception if nothing to pop. */ void pop(); + +private: + + /** Current set of assertions. */ + // TODO: make context-aware to handle user-level push/pop. + std::vector d_assertions; + + /** Our expression manager */ + ExprManager *d_public_em; + + /** Out internal expression/node manager */ + NodeManager *d_em; + + /** User-level options */ + Options *d_opts; + + /** The decision engine */ + DecisionEngine d_de; + + /** The decision engine */ + TheoryEngine d_te; + + /** The propositional engine */ + PropEngine d_prop; + + /** + * Pre-process an Node. This is expected to be highly-variable, + * with a lot of "source-level configurability" to add multiple + * passes over the Node. TODO: may need to specify a LEVEL of + * preprocessing (certain contexts need more/less ?). + */ + Node preprocess(const Node& e); + + /** + * Adds a formula to the current context. + */ + void addFormula(const Node& e); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + /** + * Process the assertion list: for literals and conjunctions of + * literals, assert to T-solver. + */ + Node processAssertionList(); + + };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/util/command.cpp b/src/util/command.cpp index 0953a2ba2..3911897f5 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -5,10 +5,9 @@ * Author: dejan */ +#include #include "util/command.h" #include "smt/smt_engine.h" -#include "expr/node.h" -#include "util/result.h" using namespace std; @@ -26,7 +25,7 @@ EmptyCommand::EmptyCommand(string name) : void EmptyCommand::invoke(SmtEngine* smt_engine) { } -AssertCommand::AssertCommand(const Node& e) : +AssertCommand::AssertCommand(const BoolExpr& e) : d_expr(e) { } @@ -37,7 +36,7 @@ void AssertCommand::invoke(SmtEngine* smt_engine) { CheckSatCommand::CheckSatCommand() { } -CheckSatCommand::CheckSatCommand(const Node& e) : +CheckSatCommand::CheckSatCommand(const BoolExpr& e) : d_expr(e) { } @@ -45,7 +44,7 @@ void CheckSatCommand::invoke(SmtEngine* smt_engine) { smt_engine->checkSat(d_expr); } -QueryCommand::QueryCommand(const Node& e) : +QueryCommand::QueryCommand(const BoolExpr& e) : d_expr(e) { } @@ -73,10 +72,6 @@ void CommandSequence::addCommand(Command* cmd) { d_command_sequence.push_back(cmd); } -// Printout methods - -using namespace std; - void EmptyCommand::toString(ostream& out) const { out << "EmptyCommand(" << d_name << ")"; } @@ -98,8 +93,9 @@ void QueryCommand::toString(ostream& out) const { void CommandSequence::toString(ostream& out) const { out << "CommandSequence[" << endl; - for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) + for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) { out << *d_command_sequence[i] << endl; + } out << "]"; } diff --git a/src/util/command.h b/src/util/command.h index 189872220..221c513f0 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -15,12 +15,11 @@ #include #include "cvc4_config.h" -#include "expr/node.h" +#include "expr/expr.h" namespace CVC4 { class SmtEngine; class Command; - class Node; }/* CVC4 namespace */ namespace CVC4 { @@ -45,33 +44,33 @@ private: class CVC4_PUBLIC AssertCommand : public Command { -protected: - Node d_expr; public: - AssertCommand(const Node& e); + AssertCommand(const BoolExpr& e); void invoke(CVC4::SmtEngine* smt_engine); void toString(std::ostream& out) const; +protected: + BoolExpr d_expr; };/* class AssertCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); - CheckSatCommand(const Node& e); + CheckSatCommand(const BoolExpr& e); void invoke(SmtEngine* smt); void toString(std::ostream& out) const; protected: - Node d_expr; + BoolExpr d_expr; };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { public: - QueryCommand(const Node& e); + QueryCommand(const BoolExpr& e); void invoke(SmtEngine* smt); void toString(std::ostream& out) const; protected: - Node d_expr; + BoolExpr d_expr; };/* class QueryCommand */