summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile.in2
-rw-r--r--src/context/Makefile.in2
-rw-r--r--src/expr/Makefile.in2
-rw-r--r--src/expr/node.h6
-rw-r--r--src/expr/node_builder.h72
-rw-r--r--src/expr/node_manager.cpp2
-rw-r--r--src/expr/node_value.h2
-rw-r--r--src/main/Makefile.in2
-rw-r--r--src/main/getopt.cpp9
-rw-r--r--src/parser/Makefile.in2
-rw-r--r--src/parser/cvc/Makefile.in2
-rw-r--r--src/parser/smt/Makefile.in2
-rw-r--r--src/prop/Makefile.in2
-rw-r--r--src/prop/minisat/Makefile.in2
-rw-r--r--src/prop/prop_engine.cpp24
-rw-r--r--src/smt/Makefile.in2
-rw-r--r--src/smt/smt_engine.cpp47
-rw-r--r--src/smt/smt_engine.h2
-rw-r--r--src/theory/Makefile.in2
-rw-r--r--src/theory/uf/Makefile.in2
-rw-r--r--src/util/Assert.h24
-rw-r--r--src/util/Makefile.in2
-rw-r--r--src/util/output.h2
23 files changed, 175 insertions, 41 deletions
diff --git a/src/Makefile.in b/src/Makefile.in
index 9099b92be..08f7c6421 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -159,6 +159,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/context/Makefile.in b/src/context/Makefile.in
index c4f82d42a..5428ba8b9 100644
--- a/src/context/Makefile.in
+++ b/src/context/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index 4892220d8..848d8d72b 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -93,6 +93,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/expr/node.h b/src/expr/node.h
index fd2603ffa..b40443923 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -25,6 +25,7 @@
#include "cvc4_config.h"
#include "expr/kind.h"
+#include "util/Assert.h"
namespace CVC4 {
class Node;
@@ -105,6 +106,11 @@ public:
bool operator==(const Node& e) const { return d_ev == e.d_ev; }
bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
+ Node operator[](int i) const {
+ Assert(i >= 0 && i < d_ev->d_nchildren);
+ return Node(d_ev->d_children[i]);
+ }
+
/**
* We compare by expression ids so, keeping things deterministic and having
* that subexpressions have to be smaller than the enclosing expressions.
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 1dee91735..747854d23 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -168,6 +168,7 @@ public:
NodeBuilder& append(const Node& n) {
Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+ Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl;
allocateEvIfNecessaryForAppend();
NodeValue* ev = n.d_ev;
d_hash = NodeValue::computeHash(d_hash, ev);
@@ -364,7 +365,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder() :
d_used(false),
d_ev(&d_inlineEv),
d_inlineEv(0),
- d_childrenStorage(0) {}
+ d_childrenStorage() {}
template <unsigned nchild_thresh>
inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
@@ -373,9 +374,9 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
d_used(false),
d_ev(&d_inlineEv),
d_inlineEv(0),
- d_childrenStorage(0) {
+ d_childrenStorage() {
- Message() << "kind " << k << std::endl;
+ //Message() << "kind " << k << std::endl;
d_inlineEv.d_kind = k;
}
@@ -386,13 +387,13 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
d_used(nb.d_used),
d_ev(&d_inlineEv),
d_inlineEv(0),
- d_childrenStorage(0) {
+ d_childrenStorage() {
if(evIsAllocated(nb)) {
realloc(nb->d_size, false);
- std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+ std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
} else {
- std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+ std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
}
}
@@ -404,13 +405,13 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
d_used(nb.d_used),
d_ev(&d_inlineEv),
d_inlineEv(0),
- d_childrenStorage(0) {
+ d_childrenStorage() {
if(nb.d_ev->d_nchildren > nchild_thresh) {
realloc(nb.d_size, false);
- std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+ std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
} else {
- std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+ std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
}
}
@@ -421,7 +422,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
d_used(false),
d_ev(&d_inlineEv),
d_inlineEv(0),
- d_childrenStorage(0) {}
+ d_childrenStorage() {}
template <unsigned nchild_thresh>
inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
@@ -432,7 +433,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
d_inlineEv(0),
d_childrenStorage() {
- Message() << "kind " << k << std::endl;
+ //Message() << "kind " << k << std::endl;
d_inlineEv.d_kind = k;
}
@@ -466,9 +467,9 @@ void NodeBuilder<nchild_thresh>::realloc() {
d_ev->d_rc = 0;
d_ev->d_kind = d_inlineEv.d_kind;
d_ev->d_nchildren = nchild_thresh;
- std::copy(d_ev->d_children,
- d_inlineEv.d_children,
- d_inlineEv.d_children + nchild_thresh);
+ std::copy(d_inlineEv.d_children,
+ d_inlineEv.d_children + nchild_thresh,
+ d_ev->d_children);
}
}
@@ -489,9 +490,9 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
d_ev->d_kind = d_inlineEv.d_kind;
d_ev->d_nchildren = nchild_thresh;
if(copy) {
- std::copy(d_ev->d_children,
- d_inlineEv.d_children,
- d_inlineEv.d_children + nchild_thresh);
+ std::copy(d_inlineEv.d_children,
+ d_inlineEv.d_children + nchild_thresh,
+ d_ev->d_children);
}
}
}
@@ -502,6 +503,21 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
Assert(d_ev->d_kind != UNDEFINED_KIND,
"Can't make an expression of an undefined kind!");
+ if(d_ev->d_kind == VARIABLE) {
+ Assert(d_ev->d_nchildren == 0);
+ NodeValue *ev = (NodeValue*)
+ std::malloc(sizeof(NodeValue) +
+ ( sizeof(NodeValue*) * d_inlineEv.d_nchildren ));
+ ev->d_nchildren = 0;
+ ev->d_kind = VARIABLE;
+ ev->d_id = NodeValue::next_id++;// FIXME multithreading
+ ev->d_rc = 0;
+ d_used = true;
+ d_ev = NULL;
+ Debug("prop") << "result: " << Node(ev) << std::endl;
+ return Node(ev);
+ }
+
// implementation differs depending on whether the expression value
// was malloc'ed or not
@@ -510,6 +526,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
if(ev != NULL) {
// expression already exists in node manager
d_used = true;
+ Debug("prop") << "result: " << Node(ev) << std::endl;
return Node(ev);
}
@@ -520,30 +537,41 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
// this inserts into the NodeManager;
// return the result of lookup() in case another thread beat us to it
d_used = true;
- return d_nm->lookup(d_hash, ev);
+ Node n = d_nm->lookup(d_hash, ev);
+ Debug("prop") << "result: " << n << std::endl;
+ return n;
}
NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv);
if(ev != NULL) {
// expression already exists in node manager
d_used = true;
+ Debug("prop") << "result: " << Node(ev) << std::endl;
return Node(ev);
}
// otherwise create the canonical expression value for this node
ev = (NodeValue*)
std::malloc(sizeof(NodeValue) +
- ( sizeof(NodeValue*) * d_inlineEv.d_nchildren) );
- ev->d_nchildren = d_ev->d_nchildren;
- ev->d_kind = d_ev->d_kind;
+ ( sizeof(NodeValue*) * d_inlineEv.d_nchildren ));
+ ev->d_nchildren = d_inlineEv.d_nchildren;
+ ev->d_kind = d_inlineEv.d_kind;
ev->d_id = NodeValue::next_id++;// FIXME multithreading
ev->d_rc = 0;
+ std::copy(d_inlineEv.d_children,
+ d_inlineEv.d_children + d_inlineEv.d_nchildren,
+ ev->d_children);
d_used = true;
d_ev = NULL;
// this inserts into the NodeManager;
// return the result of lookup() in case another thread beat us to it
- return d_nm->lookup(d_hash, ev);
+ if(ev->numChildren()) {
+ Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl;
+ }
+ Node n = d_nm->lookup(d_hash, ev);
+ Debug("prop") << "result: " << n << std::endl;
+ return n;
}
}/* CVC4 namespace */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index eba8c4d18..a307eb11f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -58,6 +58,7 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
return *j;
}
+
// didn't find it, insert
std::vector<Node> v;
Node e(ev);
@@ -99,6 +100,7 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
return j->d_ev;
}
+
// didn't find it, don't insert
return 0;
}
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 954fe0aaa..985ad15a7 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -177,7 +177,7 @@ namespace CVC4 {
namespace expr {
inline Node NodeValue::node_iterator::operator*() {
- return Node((NodeValue*) d_i);
+ return Node(*d_i);
}
}/* CVC4::expr namespace */
diff --git a/src/main/Makefile.in b/src/main/Makefile.in
index 8e2c49989..6a2677109 100644
--- a/src/main/Makefile.in
+++ b/src/main/Makefile.in
@@ -94,6 +94,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 81cbc2df8..123bc3204 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -110,7 +110,8 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
}
if(strcmp(optarg, "help")) {
- throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help.");
+ throw OptionException(string("unknown language for --lang: `") +
+ optarg + "'. Try --lang help.");
}
fputs(lang_help, stdout);
@@ -132,13 +133,13 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
break;
case '?':
- throw OptionException(string("can't understand option: `") + argv[optind] + "'");
+ throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'");
case ':':
- throw OptionException(string("option `") + argv[optind] + "' missing its required argument");
+ throw OptionException(string("option missing its required argument"));// + argv[optind - 1] + "' missing its required argument");
default:
- throw OptionException(string("can't understand option: `") + argv[optind] + "'");
+ throw OptionException(string("can't understand option"));//: `") + argv[optind - 1] + "'");
}
}
diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in
index 31ae05da5..b6c6ae102 100644
--- a/src/parser/Makefile.in
+++ b/src/parser/Makefile.in
@@ -163,6 +163,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index 28b80800e..e63b15e26 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -96,6 +96,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 6145b4c4e..a65d62c88 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -96,6 +96,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index c6538df38..e5ac92c61 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index 1dbc8da9f..278d68790 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ffd335453..afc84a5b4 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -64,7 +64,13 @@ static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>*
c->push(Lit(v->second, true));
return;
}
- Unhandled();
+ if(e.getKind() == OR) {
+ for(Node::iterator i = e.begin(); i != e.end(); ++i) {
+ doAtom(minisat, vars, *i, c);
+ }
+ return;
+ }
+ Unhandled(e.getKind());
}
static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
@@ -72,6 +78,20 @@ static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>*
Debug("prop") << " " << e << endl;
if(e.getKind() == VARIABLE || e.getKind() == NOT) {
doAtom(minisat, vars, e, &c);
+ } else if(e.getKind() == FALSE) {
+ // inconsistency
+ Notice() << "adding FALSE clause" << endl;
+ Var v = minisat->newVar();
+ c.push(Lit(v, true));
+ minisat->addClause(c);
+ Notice() << "added unit clause " << v << " [[ " << (*varsReverse)[v] << " ]]" << endl;
+ c.clear();
+ c.push(Lit(v, false));
+ minisat->addClause(c);
+ Notice() << "added unit clause -" << v << " [[ -" << (*varsReverse)[v] << " ]]" << endl;
+ } else if(e.getKind() == TRUE) {
+ Notice() << "adding TRUE clause (do nothing)" << endl;
+ // do nothing
} else {
Assert(e.getKind() == OR);
for(Node::iterator i = e.begin(); i != e.end(); ++i) {
@@ -101,7 +121,7 @@ void PropEngine::solve(Node e) {
d_sat.verbosity = 1;
bool result = d_sat.solve();
- Notice() << "result is " << (result ? "sat" : "unsat") << endl;
+ Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
if(result) {
Notice() << "model:" << endl;
for(int i = 0; i < d_sat.model.size(); ++i)
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in
index 35126e382..aa00d5e25 100644
--- a/src/smt/Makefile.in
+++ b/src/smt/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4c7f6a156..018936f7c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -15,37 +15,55 @@
#include "smt/smt_engine.h"
#include "util/exception.h"
#include "util/command.h"
+#include "util/output.h"
+#include "expr/node_builder.h"
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) {
- }
+ d_assertions(),
+ d_public_em(em),
+ d_nm(em->getNodeManager()),
+ d_opts(opts),
+ d_de(),
+ d_te(),
+ d_prop(d_de, d_te) {
+}
SmtEngine::~SmtEngine() {
}
void SmtEngine::doCommand(Command* c) {
+ NodeManagerScope nms(d_nm);
c->invoke(this);
}
Node SmtEngine::preprocess(const Node& e) {
+ if(e.getKind() == NOT) {
+ if(e[0].getKind() == TRUE) {
+ return d_nm->mkNode(FALSE);
+ } else if(e[0].getKind() == FALSE) {
+ return d_nm->mkNode(TRUE);
+ } else if(e[0].getKind() == NOT) {
+ return preprocess(e[0][0]);
+ }
+ }
return e;
}
Node SmtEngine::processAssertionList() {
- Node asserts;
+ if(d_assertions.size() == 1) {
+ return d_assertions[0];
+ }
+
+ NodeBuilder<> asserts(AND);
for(std::vector<Node>::iterator i = d_assertions.begin();
i != d_assertions.end();
++i) {
- asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i);
+ asserts << *i;
}
+
return asserts;
}
@@ -61,25 +79,34 @@ Result SmtEngine::quickCheck() {
}
void SmtEngine::addFormula(const Node& e) {
+ Debug("smt") << "push_back assertion " << e << std::endl;
d_assertions.push_back(e);
}
Result SmtEngine::checkSat(const BoolExpr& e) {
+ NodeManagerScope nms(d_nm);
Node node_e = preprocess(e.getNode());
addFormula(node_e);
return check();
}
Result SmtEngine::query(const BoolExpr& e) {
- Node node_e = preprocess(e.getNode());
+ NodeManagerScope nms(d_nm);
+ Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
addFormula(node_e);
return check();
}
Result SmtEngine::assertFormula(const BoolExpr& e) {
+ NodeManagerScope nms(d_nm);
Node node_e = preprocess(e.getNode());
addFormula(node_e);
return quickCheck();
}
+Expr SmtEngine::simplify(const Expr& e) {
+ Expr simplify(const Expr& e);
+ Unimplemented();
+}
+
}/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 98cffb6de..027d3d603 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -118,7 +118,7 @@ private:
ExprManager *d_public_em;
/** Out internal expression/node manager */
- NodeManager *d_em;
+ NodeManager *d_nm;
/** User-level options */
Options *d_opts;
diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in
index dafd68b6c..379d1171b 100644
--- a/src/theory/Makefile.in
+++ b/src/theory/Makefile.in
@@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in
index 3b3cd6bbb..b1a6081d2 100644
--- a/src/theory/uf/Makefile.in
+++ b/src/theory/uf/Makefile.in
@@ -78,6 +78,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 49c97e9b6..d8e881613 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -113,6 +113,28 @@ public:
}
};/* class UnhandledCaseException */
+class CVC4_PUBLIC UnimplementedOperationException : public AssertionException {
+protected:
+ UnimplementedOperationException() : AssertionException() {}
+
+public:
+ UnimplementedOperationException(const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Unimplemented code encountered",
+ NULL, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ UnimplementedOperationException(const char* function, const char* file,
+ unsigned line) :
+ AssertionException() {
+ construct("Unimplemented code encountered", NULL, function, file, line);
+ }
+};/* class UnimplementedOperationException */
+
class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
protected:
IllegalArgumentException() : AssertionException() {}
@@ -172,6 +194,8 @@ public:
throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define Unhandled(msg...) \
throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unimplemented(msg...) \
+ throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define IllegalArgument(arg, msg...) \
throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define CheckArgument(cond, arg, msg...) \
diff --git a/src/util/Makefile.in b/src/util/Makefile.in
index 3ac892aba..686f4cc33 100644
--- a/src/util/Makefile.in
+++ b/src/util/Makefile.in
@@ -93,6 +93,8 @@ AUTOCONF = @AUTOCONF@
AUTOHEADER = @AUTOHEADER@
AUTOMAKE = @AUTOMAKE@
AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
CC = @CC@
CCDEPMODE = @CCDEPMODE@
CFLAGS = @CFLAGS@
diff --git a/src/util/output.h b/src/util/output.h
index 57ce5f3ca..c1e513703 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -55,7 +55,7 @@ public:
// Yeting option not possible here
std::ostream& operator()(const char* tag) {
- if(d_tags.find(tag) != d_tags.end())
+ if(d_tags.find(std::string(tag)) != d_tags.end())
return *d_os;
else return null_os;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback