summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am2
-rw-r--r--src/expr/attr_type.h10
-rw-r--r--src/expr/expr.cpp18
-rw-r--r--src/expr/expr_attribute.h10
-rw-r--r--src/expr/expr_builder.cpp21
-rw-r--r--src/expr/expr_builder.h12
-rw-r--r--src/expr/expr_manager.cpp2
-rw-r--r--src/expr/expr_manager.h8
-rw-r--r--src/expr/expr_value.cpp2
-rw-r--r--src/expr/expr_value.h24
-rw-r--r--src/expr/kind.h30
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback