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
+
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
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
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@
--- /dev/null
+/*
+ * 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
--- /dev/null
+/*
+ * 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 <string>
+#include <iostream>
+#include <stdint.h>
+
+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 */
--- /dev/null
+/*
+ * 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<Expr>& children) {
+ vector<Node> nodes;
+ vector<Expr>::const_iterator it = children.begin();
+ vector<Expr>::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
--- /dev/null
+/*
+ * 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 <vector>
+
+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<Expr>& 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 */
**/
#include "expr_value.h"
+#include <sstream>
+
+using namespace std;
namespace CVC4 {
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;
#include <stdint.h>
#include "kind.h"
+#include <string>
+
namespace CVC4 {
class Node;
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 */
#include "expr/node_builder.h"
#include "util/Assert.h"
+#include <sstream>
+
using namespace CVC4::expr;
+using namespace std;
namespace CVC4 {
Node Node::s_null(&ExprValue::s_null);
+Node Node::null() {
+ return s_null;
+}
+
+
bool Node::isNull() const {
return d_ev == &ExprValue::s_null;
}
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);
}
** 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 <vector>
+#include <string>
#include <iostream>
#include <stdint.h>
namespace CVC4 {
-inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Node&);
class NodeManager;
* Encapsulation of an ExprValue pointer. The reference count is
* maintained in the ExprValue.
*/
-class CVC4_PUBLIC Node {
+class Node {
friend class ExprValue;
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;
inline size_t numChildren() const;
- static Node null() { return s_null; }
+ static Node null();
typedef Node* iterator;
typedef Node const* const_iterator;
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;
}
inline std::ostream& operator<<(std::ostream& out, const Node& e) {
- e.toString(out);
+ e.toStream(out);
return out;
}
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() {
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_H */
+#endif /* __CVC4__NODE_H */
**
**/
-#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 <stdint.h>
#include "config.h"
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) {
**
**/
-#ifndef __CVC4__EXPR_BUILDER_H
-#define __CVC4__EXPR_BUILDER_H
+#ifndef __CVC4__NODE_BUILDER_H
+#define __CVC4__NODE_BUILDER_H
#include <vector>
#include <cstdlib>
// 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);
// variables are permitted to be duplicates (from POV of the expression manager)
if(d_kind == VARIABLE) {
ev = new ExprValue;
- hash = reinterpret_cast<uint64_t>(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<ev_iterator>(d_kind, ev_begin(), ev_end());
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 {
}
inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) {
- d_eb.append(e.negate());
+ d_eb.append(e.uMinusExpr());
return *this;
}
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_BUILDER_H */
+#endif /* __CVC4__NODE_BUILDER_H */
}
// N-ary version
-Node NodeManager::mkExpr(Kind kind, std::vector<Node> children) {
+Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
return NodeBuilder(this, kind).append(children);
}
**
**/
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
+#ifndef __CVC4__NODE_MANAGER_H
+#define __CVC4__NODE_MANAGER_H
#include <vector>
#include <map>
class ExprBuilder;
}/* CVC4::expr namespace */
-class CVC4_PUBLIC NodeManager {
+class NodeManager {
static __thread NodeManager* s_current;
friend class CVC4::NodeBuilder;
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<Node> children);
+ Node mkExpr(Kind kind, const std::vector<Node>& children);
// variables are special, because duplicates are permitted
Node mkVar();
#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"
throw new Exception("Too many input files specified.");
// Create the expression manager
- NodeManager exprMgr;
+ ExprManager exprMgr;
// Create the SmtEngine
SmtEngine smt(&exprMgr, &options);
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<Node>& children) {
+Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
return d_expr_manager->mkExpr(kind, children);
}
void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) {
}
-void AntlrParser::setExpressionManager(NodeManager* em) {
+void AntlrParser::setExpressionManager(ExprManager* em) {
d_expr_manager = em;
}
LT(0).get()->getColumn());
}
-Node AntlrParser::createPrecedenceExpr(const vector<Node>& exprs, const vector<
+Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
Kind>& kinds) {
return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
}
return pivot;
}
-Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs,
+Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
const std::vector<Kind>& kinds,
unsigned start_index, unsigned end_index) {
if(start_index == end_index)
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);
}
#include <antlr/LLkParser.hpp>
#include <antlr/SemanticException.hpp>
-#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"
* 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:
* @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.
* 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<Node>& children);
+ Expr newExpression(Kind kind, const std::vector<Expr>& 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<Node>& exprs, const std::vector<Kind>& kinds);
+ Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds);
/**
* Creates a new predicated over the given sorts.
* 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<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
+ Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& 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<Node> d_var_symbol_table;
+ SymbolTable<Expr> d_var_symbol_table;
};
std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
return cmd;
}
-Node CvcParser::parseNextExpression() throw(ParserException) {
- Node result;
+Expr CvcParser::parseNextExpression() throw(ParserException) {
+ Expr result;
if(!done()) {
try {
result = d_antlr_parser->formula();
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") +
*/
command returns [CVC4::Command* cmd = 0]
{
- Node f;
+ Expr f;
vector<string> ids;
}
: ASSERT f = formula { cmd = new AssertCommand(f); }
: 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<Node> formulas;
+ vector<Expr> formulas;
vector<Kind> kinds;
- Node f1, f2;
+ Expr f1, f2;
Kind k;
}
: f1 = primary_bool_formula { formulas.push_back(f1); }
}
;
-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
| IFF { kind = CVC4::IFF; }
;
-bool_atom returns [CVC4::Node atom]
+bool_atom returns [CVC4::Expr atom]
{
string p;
}
* @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.
* Parses the next complete expression of the stream.
* @return the expression parsed
*/
- Node parseNextExpression() throw(ParserException);
+ Expr parseNextExpression() throw(ParserException);
protected:
namespace CVC4 {
namespace parser {
-Parser::Parser(NodeManager* em) :
+Parser::Parser(ExprManager* em) :
d_expr_manager(em), d_done(false) {
}
namespace CVC4 {
// Forward declarations
-class Node;
+class Expr;
class Command;
-class NodeManager;
+class ExprManager;
namespace parser {
* Construct the parser that uses the given expression manager.
* @param em the expression manager.
*/
- Parser(NodeManager* em);
+ Parser(ExprManager* em);
/**
* Destructor.
/**
* 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.
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;
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();
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") +
/**
* Matches a propositional atom from the input.
*/
-prop_atom returns [CVC4::Node atom]
+prop_atom returns [CVC4::Expr atom]
{
std::string p;
}
* 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; }
/**
* Matches an annotated formula.
*/
-an_formula returns [CVC4::Node formula]
+an_formula returns [CVC4::Expr formula]
{
Kind kind;
- vector<Node> children;
+ vector<Expr> 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<Node>& formulas]
+an_formulas[std::vector<Expr>& formulas]
{
- Node f;
+ Expr f;
}
: ( f = an_formula { formulas.push_back(f); } )+
;
bench_attribute returns [ Command* smt_command = 0]
{
BenchmarkStatus b_status = SMT_UNKNOWN;
- Node formula;
+ Expr formula;
vector<string> sorts;
}
: C_LOGIC IDENTIFIER
* @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.
* Parses the next complete expression of the stream.
* @return the expression parsed
*/
- Node parseNextExpression() throw(ParserException);
+ Expr parseNextExpression() throw(ParserException);
protected:
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<Node>::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);
}
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();
}
#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"
//
// 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<Node> 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.
* 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.
* 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<Node> 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 */
* Author: dejan
*/
+#include <map>
#include "util/command.h"
#include "smt/smt_engine.h"
-#include "expr/node.h"
-#include "util/result.h"
using namespace std;
void EmptyCommand::invoke(SmtEngine* smt_engine) {
}
-AssertCommand::AssertCommand(const Node& e) :
+AssertCommand::AssertCommand(const BoolExpr& e) :
d_expr(e) {
}
CheckSatCommand::CheckSatCommand() {
}
-CheckSatCommand::CheckSatCommand(const Node& e) :
+CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
d_expr(e) {
}
smt_engine->checkSat(d_expr);
}
-QueryCommand::QueryCommand(const Node& e) :
+QueryCommand::QueryCommand(const BoolExpr& e) :
d_expr(e) {
}
d_command_sequence.push_back(cmd);
}
-// Printout methods
-
-using namespace std;
-
void EmptyCommand::toString(ostream& out) const {
out << "EmptyCommand(" << d_name << ")";
}
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 << "]";
}
#include <iostream>
#include "cvc4_config.h"
-#include "expr/node.h"
+#include "expr/expr.h"
namespace CVC4 {
class SmtEngine;
class Command;
- class Node;
}/* CVC4 namespace */
namespace CVC4 {
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 */
projects / cvc5.git / commitdiff