diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 2 | ||||
-rw-r--r-- | src/expr/attr_type.h | 10 | ||||
-rw-r--r-- | src/expr/expr.cpp | 18 | ||||
-rw-r--r-- | src/expr/expr_attribute.h | 10 | ||||
-rw-r--r-- | src/expr/expr_builder.cpp | 21 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 12 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 8 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_value.h | 24 | ||||
-rw-r--r-- | src/expr/kind.h | 30 |
11 files changed, 79 insertions, 60 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6833f9f97..17b7d8dcd 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libexpr.a diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index d24385f8e..1d5e8eb0c 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -9,12 +9,13 @@ ** **/ -#ifndef __CVC4_ATTR_TYPE_H -#define __CVC4_ATTR_TYPE_H +#ifndef __CVC4__EXPR__ATTR_TYPE_H +#define __CVC4__EXPR__ATTR_TYPE_H #include "expr_attribute.h" namespace CVC4 { +namespace expr { class Type; @@ -29,6 +30,7 @@ public: extern AttrTable<Type_attr> type_table; -} /* CVC4 namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_ATTR_TYPE_H */ +#endif /* __CVC4__EXPR__ATTR_TYPE_H */ diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index b6484ef25..f1b334ff8 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -14,33 +14,31 @@ #include "expr_value.h" #include "expr_builder.h" +using namespace CVC4::expr; + namespace CVC4 { Expr Expr::s_null(0); Expr::Expr(ExprValue* ev) : d_ev(ev) { - // FIXME: thread-safety - ++d_ev->d_rc; + d_ev->inc(); } Expr::Expr(const Expr& e) { - // FIXME: thread-safety if((d_ev = e.d_ev)) - ++d_ev->d_rc; + d_ev->inc(); } Expr::~Expr() { - // FIXME: thread-safety - --d_ev->d_rc; + d_ev->dec(); } Expr& Expr::operator=(const Expr& e) { - // FIXME: thread-safety if(d_ev) - --d_ev->d_rc; + d_ev->dec(); if((d_ev = e.d_ev)) - ++d_ev->d_rc; + d_ev->inc(); return *this; } @@ -97,4 +95,4 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms, return ExprBuilder(*this).substExpr(oldTerms, newTerms); } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h index 3525a8370..b44c9af6f 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_EXPR_ATTRIBUTE_H -#define __CVC4_EXPR_ATTRIBUTE_H +#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H +#define __CVC4__EXPR__EXPR_ATTRIBUTE_H // TODO WARNING this file needs work ! @@ -20,6 +20,7 @@ #include "cvc4_expr.h" namespace CVC4 { +namespace expr { template <class value_type> class AttrTables; @@ -93,6 +94,7 @@ class AttributeTable { }; -} /* CVC4 namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_ATTRIBUTE_H */ +#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */ diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index 2f7114a9b..3b0cf4041 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -139,43 +139,41 @@ void ExprBuilder::addChild(const Expr& e) { v->reserve(nchild_thresh + 5); for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { v->push_back(Expr(*i)); - i->dec(); + (*i)->dec(); } - v.push_back(e); + v->push_back(e); d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { - d_children.u_vec.push_back(e); + d_children.u_vec->push_back(e); ++d_nchildren; } else { - ExprValue *ev = e->d_ev; + ExprValue *ev = e.d_ev; d_children.u_arr[d_nchildren] = ev; ev->inc(); ++d_nchildren; } - return *this; } -void ExprBuilder::addChild(const ExprValue* ev) { +void ExprBuilder::addChild(ExprValue* ev) { if(d_nchildren == nchild_thresh) { vector<Expr>* v = new vector<Expr>(); v->reserve(nchild_thresh + 5); for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { v->push_back(Expr(*i)); - i->dec(); + (*i)->dec(); } - v.push_back(Expr(ev)); + v->push_back(Expr(ev)); d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { - d_children.u_vec.push_back(Expr(ev)); + d_children.u_vec->push_back(Expr(ev)); ++d_nchildren; } else { d_children.u_arr[d_nchildren] = ev; ev->inc(); ++d_nchildren; } - return *this; } void ExprBuilder::collapse() { @@ -184,7 +182,6 @@ void ExprBuilder::collapse() { v->reserve(nchild_thresh + 5); } - return *this; } // not const @@ -206,4 +203,4 @@ PlusExprBuilder ExprBuilder::operator- (Expr) { MultExprBuilder ExprBuilder::operator* (Expr) { } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 1104c17f5..fc303572d 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_EXPR_BUILDER_H -#define __CVC4_EXPR_BUILDER_H +#ifndef __CVC4__EXPR_BUILDER_H +#define __CVC4__EXPR_BUILDER_H #include <vector> #include "expr_manager.h" @@ -42,13 +42,13 @@ class ExprBuilder { } d_children; void addChild(const Expr&); - void addChild(const ExprValue*); + void addChild(ExprValue*); void collapse(); typedef ExprValue** ev_iterator; typedef ExprValue const** const_ev_iterator; - void reset(const ExprValue*); + ExprBuilder& reset(const ExprValue*); public: @@ -154,6 +154,6 @@ public: };/* class MultExprBuilder */ -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_BUILDER_H */ +#endif /* __CVC4__EXPR_BUILDER_H */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 80091bef6..a65a2f3cd 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -49,4 +49,4 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) { return ExprBuilder(this, kind).append(children); } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 7e0da01c6..802cfe9c0 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_EXPR_MANAGER_H -#define __CVC4_EXPR_MANAGER_H +#ifndef __CVC4__EXPR_MANAGER_H +#define __CVC4__EXPR_MANAGER_H #include <vector> #include "cvc4_expr.h" @@ -53,6 +53,6 @@ public: // do we want a varargs one? perhaps not.. }; -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_MANAGER_H */ +#endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index 451538f3f..fa5628e26 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -76,4 +76,4 @@ ExprValue::const_iterator ExprValue::rend() const { return d_children - 1; } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 4b4b4f612..88984d286 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -14,14 +14,19 @@ ** reference count on ExprValue instances and **/ -#ifndef __CVC4_EXPR_VALUE_H -#define __CVC4_EXPR_VALUE_H +#ifndef __CVC4__EXPR__EXPR_VALUE_H +#define __CVC4__EXPR__EXPR_VALUE_H #include <stdint.h> #include "cvc4_expr.h" namespace CVC4 { +class Expr; +class ExprBuilder; + +namespace expr { + /** * This is an ExprValue. */ @@ -47,11 +52,13 @@ class ExprValue { /** Variable number of child nodes */ Expr d_children[0]; - friend class Expr; - friend class ExprBuilder; + // todo add exprMgr ref in debug case + + friend class CVC4::Expr; + friend class CVC4::ExprBuilder; - ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; } - ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; } + ExprValue* inc(); + ExprValue* dec(); public: /** Hash this expression. @@ -74,6 +81,7 @@ public: const_iterator rend() const; }; -} /* CVC4 namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_VALUE_H */ +#endif /* __CVC4__EXPR__EXPR_VALUE_H */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 9c4e4d5ab..98cc7e2e3 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_KIND_H -#define __CVC4_KIND_H +#ifndef __CVC4__KIND_H +#define __CVC4__KIND_H namespace CVC4 { @@ -19,20 +19,32 @@ namespace CVC4 { // placeholder for design & development work. enum Kind { + /* undefined */ UNDEFINED_KIND = -1, + + /* built-ins */ EQUAL, + ITE, + SKOLEM, + VARIABLE, + + /* propositional connectives */ + FALSE, + TRUE, + + NOT, + AND, + IFF, OR, XOR, - NOT, + + /* from arith */ PLUS, - MINUS, - ITE, - IFF, - SKOLEM, - SUBST + MINUS + };/* enum Kind */ }/* CVC4 namespace */ -#endif /* __CVC4_KIND_H */ +#endif /* __CVC4__KIND_H */ |