summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/compat/cvc3_compat.cpp6
-rw-r--r--src/expr/command.cpp12
-rw-r--r--src/expr/command.h18
-rw-r--r--src/expr/expr_template.cpp33
-rw-r--r--src/expr/expr_template.h128
-rw-r--r--src/printer/ast/ast_printer.cpp2
-rw-r--r--src/printer/cvc/cvc_printer.cpp4
-rw-r--r--src/printer/smt2/smt2_printer.cpp4
-rw-r--r--src/prop/cnf_stream.cpp4
-rw-r--r--src/prop/cnf_stream.h1
-rw-r--r--src/prop/minisat/core/Solver.cc24
-rw-r--r--src/prop/prop_engine.cpp4
-rw-r--r--src/smt/smt_engine.cpp10
-rw-r--r--src/smt/smt_engine.h8
-rw-r--r--src/theory/theory_engine.cpp40
15 files changed, 105 insertions, 193 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 8ba91b419..2ed3c0a7f 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2071,7 +2071,7 @@ void ValidityChecker::setTimeLimit(unsigned limit) {
}
void ValidityChecker::assertFormula(const Expr& e) {
- d_smt->assertFormula(CVC4::BoolExpr(e));
+ d_smt->assertFormula(e);
}
void ValidityChecker::registerAtom(const Expr& e) {
@@ -2107,11 +2107,11 @@ static QueryResult cvc4resultToCvc3result(CVC4::Result r) {
}
QueryResult ValidityChecker::query(const Expr& e) {
- return cvc4resultToCvc3result(d_smt->query(CVC4::BoolExpr(e)));
+ return cvc4resultToCvc3result(d_smt->query(e));
}
QueryResult ValidityChecker::checkUnsat(const Expr& e) {
- return cvc4resultToCvc3result(d_smt->checkSat(CVC4::BoolExpr(e)));
+ return cvc4resultToCvc3result(d_smt->checkSat(e));
}
QueryResult ValidityChecker::checkContinue() {
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index a62a9421f..220629cfd 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -177,11 +177,11 @@ Command* EchoCommand::clone() const {
/* class AssertCommand */
-AssertCommand::AssertCommand(const BoolExpr& e) throw() :
+AssertCommand::AssertCommand(const Expr& e) throw() :
d_expr(e) {
}
-BoolExpr AssertCommand::getExpr() const throw() {
+Expr AssertCommand::getExpr() const throw() {
return d_expr;
}
@@ -248,11 +248,11 @@ Command* PopCommand::clone() const {
/* class CheckSatCommand */
-CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
+CheckSatCommand::CheckSatCommand(const Expr& expr) throw() :
d_expr(expr) {
}
-BoolExpr CheckSatCommand::getExpr() const throw() {
+Expr CheckSatCommand::getExpr() const throw() {
return d_expr;
}
@@ -291,11 +291,11 @@ Command* CheckSatCommand::clone() const {
/* class QueryCommand */
-QueryCommand::QueryCommand(const BoolExpr& e) throw() :
+QueryCommand::QueryCommand(const Expr& e) throw() :
d_expr(e) {
}
-BoolExpr QueryCommand::getExpr() const throw() {
+Expr QueryCommand::getExpr() const throw() {
return d_expr;
}
diff --git a/src/expr/command.h b/src/expr/command.h
index 6f5b0bd4c..9fabf129e 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -290,11 +290,11 @@ public:
class CVC4_PUBLIC AssertCommand : public Command {
protected:
- BoolExpr d_expr;
+ Expr d_expr;
public:
- AssertCommand(const BoolExpr& e) throw();
+ AssertCommand(const Expr& e) throw();
~AssertCommand() throw() {}
- BoolExpr getExpr() const throw();
+ Expr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
@@ -423,13 +423,13 @@ public:
class CVC4_PUBLIC CheckSatCommand : public Command {
protected:
- BoolExpr d_expr;
+ Expr d_expr;
Result d_result;
public:
CheckSatCommand() throw();
- CheckSatCommand(const BoolExpr& expr) throw();
+ CheckSatCommand(const Expr& expr) throw();
~CheckSatCommand() throw() {}
- BoolExpr getExpr() const throw();
+ Expr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
Result getResult() const throw();
void printResult(std::ostream& out) const throw();
@@ -439,12 +439,12 @@ public:
class CVC4_PUBLIC QueryCommand : public Command {
protected:
- BoolExpr d_expr;
+ Expr d_expr;
Result d_result;
public:
- QueryCommand(const BoolExpr& e) throw();
+ QueryCommand(const Expr& e) throw();
~QueryCommand() throw() {}
- BoolExpr getExpr() const throw();
+ Expr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
Result getResult() const throw();
void printResult(std::ostream& out) const throw();
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 2f9e27c0c..d535beec2 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -467,20 +467,13 @@ TNode Expr::getTNode() const throw() {
return *d_node;
}
-BoolExpr::BoolExpr() {
-}
-
-BoolExpr::BoolExpr(const Expr& e) :
- Expr(e) {
-}
-
-BoolExpr BoolExpr::notExpr() const {
+Expr Expr::notExpr() const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
return d_exprManager->mkExpr(NOT, *this);
}
-BoolExpr BoolExpr::andExpr(const BoolExpr& e) const {
+Expr Expr::andExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
CheckArgument(d_exprManager == e.d_exprManager, e,
@@ -488,7 +481,7 @@ BoolExpr BoolExpr::andExpr(const BoolExpr& e) const {
return d_exprManager->mkExpr(AND, *this, e);
}
-BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
+Expr Expr::orExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
CheckArgument(d_exprManager == e.d_exprManager, e,
@@ -496,7 +489,7 @@ BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
return d_exprManager->mkExpr(OR, *this, e);
}
-BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
+Expr Expr::xorExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
CheckArgument(d_exprManager == e.d_exprManager, e,
@@ -504,7 +497,7 @@ BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
return d_exprManager->mkExpr(XOR, *this, e);
}
-BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
+Expr Expr::iffExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
CheckArgument(d_exprManager == e.d_exprManager, e,
@@ -512,7 +505,7 @@ BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
return d_exprManager->mkExpr(IFF, *this, e);
}
-BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
+Expr Expr::impExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
CheckArgument(d_exprManager == e.d_exprManager, e,
@@ -520,8 +513,8 @@ BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
return d_exprManager->mkExpr(IMPLIES, *this, e);
}
-BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e,
- const BoolExpr& else_e) const {
+Expr Expr::iteExpr(const Expr& then_e,
+ const Expr& else_e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
CheckArgument(d_exprManager == then_e.d_exprManager, then_e,
@@ -531,16 +524,6 @@ BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e,
return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
}
-Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
- Assert(d_exprManager != NULL,
- "Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == then_e.getExprManager(), then_e,
- "Different expression managers!");
- CheckArgument(d_exprManager == else_e.getExprManager(), else_e,
- "Different expression managers!");
- return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
-}
-
void Expr::printAst(std::ostream & o, int indent) const {
ExprManagerScope ems(*this);
getNode().printAst(o, indent);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 4255e3454..b530d13b2 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -161,16 +161,12 @@ struct ExprHashFunction {
size_t operator()(CVC4::Expr e) const;
};/* struct ExprHashFunction */
-class BoolExpr;
-
/**
* Class encapsulating CVC4 expressions and methods for constructing new
* expressions.
*/
class CVC4_PUBLIC Expr {
- friend class BoolExpr;
-
/** The internal expression representation */
NodeTemplate<true>* d_node;
@@ -313,6 +309,48 @@ public:
}
/**
+ * Returns the Boolean negation of this Expr.
+ */
+ Expr notExpr() const;
+
+ /**
+ * Returns the conjunction of this expression and
+ * the given expression.
+ */
+ Expr andExpr(const Expr& e) const;
+
+ /**
+ * Returns the disjunction of this expression and
+ * the given expression.
+ */
+ Expr orExpr(const Expr& e) const;
+
+ /**
+ * Returns the exclusive disjunction of this expression and
+ * the given expression.
+ */
+ Expr xorExpr(const Expr& e) const;
+
+ /**
+ * Returns the Boolean equivalence of this expression and
+ * the given expression.
+ */
+ Expr iffExpr(const Expr& e) const;
+
+ /**
+ * Returns the implication of this expression and
+ * the given expression.
+ */
+ Expr impExpr(const Expr& e) const;
+
+ /**
+ * Returns the if-then-else expression with this expression
+ * as the Boolean condition and the given expressions as
+ * the "then" and "else" expressions.
+ */
+ Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
+
+ /**
* Iterator type for the children of an Expr.
*/
class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
@@ -562,86 +600,6 @@ private:
};/* class Expr */
-/**
- * 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;
-
-};/* class BoolExpr */
-
namespace expr {
/**
@@ -968,7 +926,7 @@ public:
${getConst_instantiations}
-#line 959 "${template}"
+#line 930 "${template}"
namespace expr {
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 4ae66f510..34bf0bb6d 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -208,7 +208,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() {
}
static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
- BoolExpr e = c->getExpr();
+ Expr e = c->getExpr();
if(e.isNull()) {
out << "CheckSat()";
} else {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 56d9a20b0..5d2ffb9db 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -821,7 +821,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() {
}
static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
- BoolExpr e = c->getExpr();
+ Expr e = c->getExpr();
if(!e.isNull()) {
out << "CHECKSAT " << e << ";";
} else {
@@ -830,7 +830,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
}
static void toStream(std::ostream& out, const QueryCommand* c) throw() {
- BoolExpr e = c->getExpr();
+ Expr e = c->getExpr();
if(!e.isNull()) {
out << "QUERY " << e << ";";
} else {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5d9a13786..31754cb3a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -615,7 +615,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() {
}
static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
- BoolExpr e = c->getExpr();
+ Expr e = c->getExpr();
if(!e.isNull()) {
out << PushCommand() << endl
<< AssertCommand(e) << endl
@@ -627,7 +627,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
}
static void toStream(std::ostream& out, const QueryCommand* c) throw() {
- BoolExpr e = c->getExpr();
+ Expr e = c->getExpr();
if(!e.isNull()) {
out << PushCommand() << endl
<< AssertCommand(BooleanSimplification::negate(e)) << endl
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index f47637b72..e7c74525d 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -75,7 +75,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << endl;
if(Dump.isOn("clauses")) {
if(c.size() == 1) {
- Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr()));
+ Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
} else {
Assert(c.size() > 1);
NodeBuilder<> b(kind::OR);
@@ -83,7 +83,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
b << getNode(c[i]);
}
Node n = b;
- Dump("clauses") << AssertCommand(BoolExpr(n.toExpr()));
+ Dump("clauses") << AssertCommand(Expr(n.toExpr()));
}
}
d_satSolver->addClause(c, d_removable);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 5efedd4ca..a6e2b2e02 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -30,6 +30,7 @@
#include "expr/node.h"
#include "prop/theory_proxy.h"
#include "prop/registrar.h"
+#include "context/cdlist.h"
#include <ext/hash_map>
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5e19eb776..7fc7a1d9c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -349,11 +349,11 @@ void Solver::cancelUntil(int level) {
}
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
+ assigns [x] = l_Undef;
+ vardata[x].trail_index = -1;
+ if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
+ polarity[x] = sign(trail[c]);
if(intro_level(x) != -1) {// might be unregistered
- assigns [x] = l_Undef;
- vardata[x].trail_index = -1;
- if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
- polarity[x] = sign(trail[c]);
insertVarOrder(x);
}
}
@@ -1409,6 +1409,9 @@ void Solver::push()
trail_ok.push(ok);
trail_user_lim.push(trail.size());
assert(trail_user_lim.size() == assertionLevel);
+
+ context->push();
+
Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
}
@@ -1438,10 +1441,10 @@ void Solver::pop()
while(downto < trail.size()) {
Debug("minisat") << "== unassigning " << trail.last() << std::endl;
Var x = var(trail.last());
+ assigns [x] = l_Undef;
+ vardata[x].trail_index = -1;
+ polarity[x] = sign(trail.last());
if(intro_level(x) != -1) {// might be unregistered
- assigns [x] = l_Undef;
- vardata[x].trail_index = -1;
- polarity[x] = sign(trail.last());
insertVarOrder(x);
}
trail.pop();
@@ -1458,9 +1461,12 @@ void Solver::pop()
Debug("minisat") << "== unassigning " << l << std::endl;
Var x = var(l);
assigns [x] = l_Undef;
+ vardata[x].trail_index = -1;
if (phase_saving >= 1 && (polarity[x] & 0x2) == 0)
polarity[x] = sign(l);
- insertVarOrder(x);
+ if(intro_level(x) != -1) {// might be unregistered
+ insertVarOrder(x);
+ }
trail_user.pop();
}
trail_user.pop();
@@ -1470,6 +1476,8 @@ void Solver::pop()
Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
+ context->pop();
+
// Notify the cnf
proxy->removeClausesAboveLevel(assertionLevel);
}
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 973adc67f..12e85de13 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -111,9 +111,9 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
if(!d_inCheckSat && Dump.isOn("learned")) {
- Dump("learned") << AssertCommand(BoolExpr(node.toExpr()));
+ Dump("learned") << AssertCommand(node.toExpr());
} else if(Dump.isOn("lemmas")) {
- Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
+ Dump("lemmas") << AssertCommand(node.toExpr());
}
// Assert as removable
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 878588d15..2d83b7960 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1770,7 +1770,7 @@ void SmtEnginePrivate::processAssertions() {
// Push the simplified assertions to the dump output stream
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
Dump("assertions")
- << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
+ << AssertCommand(d_assertionsToCheck[i].toExpr());
}
}
@@ -1812,7 +1812,7 @@ void SmtEnginePrivate::addFormula(TNode n)
}
}
-void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) {
+void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
Type type = e.getType(options::typeChecking());
Type boolType = d_exprManager->booleanType();
if(type != boolType) {
@@ -1824,7 +1824,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) {
}
}
-Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) {
Assert(e.isNull() || e.getExprManager() == d_exprManager);
@@ -1891,7 +1891,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
return r;
}/* SmtEngine::checkSat() */
-Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::query(const Expr& e) throw(TypeCheckingException) {
Assert(!e.isNull());
Assert(e.getExprManager() == d_exprManager);
@@ -1955,7 +1955,7 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
return r;
}/* SmtEngine::query() */
-Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::assertFormula(const Expr& e) throw(TypeCheckingException) {
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f30a98935..df2e47b5b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -263,7 +263,7 @@ class CVC4_PUBLIC SmtEngine {
* Fully type-check the argument, and also type-check that it's
* actually Boolean.
*/
- void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException);
+ void ensureBoolean(const Expr& e) throw(TypeCheckingException);
void internalPush();
@@ -362,20 +362,20 @@ public:
* literals and conjunction of literals. Returns false iff
* inconsistent.
*/
- Result assertFormula(const BoolExpr& e) throw(TypeCheckingException);
+ Result assertFormula(const Expr& e) throw(TypeCheckingException);
/**
* Check validity of an expression with respect to the current set
* of assertions by asserting the query expression's negation and
* calling check(). Returns valid, invalid, or unknown result.
*/
- Result query(const BoolExpr& e) throw(TypeCheckingException);
+ Result query(const Expr& e) throw(TypeCheckingException);
/**
* Assert a formula (if provided) to the current context and call
* check(). Returns sat, unsat, or unknown result.
*/
- Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException);
+ Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException);
/**
* Simplify a formula without doing "much" work. Does not involve
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 61b66ba3e..de32409c5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -211,53 +211,15 @@ void TheoryEngine::dumpAssertions(const char* tag) {
Node assertionNode = (*it).assertion;
// Purify all the terms
- BoolExpr assertionExpr(assertionNode.toExpr());
if ((*it).isPreregistered) {
Dump(tag) << CommentCommand("Preregistered");
} else {
Dump(tag) << CommentCommand("Shared assertion");
}
- Dump(tag) << AssertCommand(assertionExpr);
+ Dump(tag) << AssertCommand(assertionNode.toExpr());
}
Dump(tag) << CheckSatCommand();
- // Check for any missed propagations of shared terms
- if (d_logicInfo.isSharingEnabled()) {
- Dump(tag) << CommentCommand("Shared term equalities");
- context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
- for (; it != it_end; ++ it) {
- TNode t1 = (*it);
- context::CDList<TNode>::const_iterator it2 = it;
- for (++ it2; it2 != it_end; ++ it2) {
- TNode t2 = (*it2);
- if (t1.getType() == t2.getType()) {
- Node equality = t1.eqNode(t2);
- if (d_sharedTerms.isKnown(equality)) {
- continue;
- }
- Node disequality = equality.notNode();
- if (d_sharedTerms.isKnown(disequality)) {
- continue;
- }
-
- // Check equality
- Dump(tag) << PushCommand();
- BoolExpr eqExpr(equality.toExpr());
- Dump(tag) << AssertCommand(eqExpr);
- Dump(tag) << CheckSatCommand();
- Dump(tag) << PopCommand();
-
- // Check disequality
- Dump(tag) << PushCommand();
- BoolExpr diseqExpr(disequality.toExpr());
- Dump(tag) << AssertCommand(diseqExpr);
- Dump(tag) << CheckSatCommand();
- Dump(tag) << PopCommand();
- }
- }
- }
- }
-
Dump(tag) << PopCommand();
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback