<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<?fileVersion 4.0.0?>
-
-<cproject storage_type_id="org.eclipse.cdt.core.XmlProjectDescriptionStorage">
+<?fileVersion 4.0.0?><cproject storage_type_id="org.eclipse.cdt.core.XmlProjectDescriptionStorage">
<storageModule moduleId="org.eclipse.cdt.core.settings">
<cconfiguration id="cdt.managedbuild.toolchain.gnu.base.1461790692">
<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="cdt.managedbuild.toolchain.gnu.base.1461790692" moduleId="org.eclipse.cdt.core.settings" name="Default">
<useDefaultCommand>false</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
</target>
+ <target name="all" path="examples" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+ <buildCommand>make</buildCommand>
+ <buildArguments>-j10</buildArguments>
+ <buildTarget>all</buildTarget>
+ <stopOnError>true</stopOnError>
+ <useDefaultCommand>true</useDefaultCommand>
+ <runAllBuilders>true</runAllBuilders>
+ </target>
<target name="uf" path="src/theory/uf" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
<buildCommand>make</buildCommand>
<buildArguments>-j2</buildArguments>
</target>
</buildTargets>
</storageModule>
+ <storageModule moduleId="org.eclipse.cdt.core.LanguageSettingsProviders"/>
</cproject>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<project>
+ <configuration id="cdt.managedbuild.toolchain.gnu.base.1461790692" name="Default">
+ <extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
+ <provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
+ <provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
+ </extension>
+ </configuration>
+</project>
output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl;
// Ouput the solution also
- BoolExpr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i]));
+ Expr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i]));
output << "; " << AssertCommand(solution) << endl;
}
sha1encoder.get_digest(sha1digest);
// Create the assertion
- BoolExpr assertion;
+ Expr assertion;
for (unsigned i = 0; i < 5; ++ i) {
- BoolExpr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i]));
+ Expr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i]));
if (i > 0) {
assertion = assertion.andExpr(conjunct);
} else {
return s_manager;
}
-BoolExpr Word::operator == (const Word& b) const {
+Expr Word::operator == (const Word& b) const {
return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr());
}
}
/** Returns the comparison expression */
- CVC4::BoolExpr operator == (const Word& b) const;
+ CVC4::Expr operator == (const Word& b) const;
};
inline std::ostream& operator << (std::ostream& out, const Word& word) {
SmtEngine engine(&exprManager);
// Variables and assertions
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
vector<string> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
std::map<Expr, unsigned> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
const vector<string>& info_tags,
const vector<string>& info_data,
const map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions);
+ const vector<Expr>& assertions);
int main(int argc, char* argv[])
{
std::map<Expr, unsigned> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
}
}
-void translate_to_isat(const map<Expr, unsigned>& variables, const BoolExpr& assertion) {
+void translate_to_isat(const map<Expr, unsigned>& variables, const Expr& assertion) {
bool first;
unsigned n = assertion.getNumChildren();
const vector<string>& info_tags,
const vector<string>& info_data,
const std::map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions)
+ const vector<Expr>& assertions)
{
bool first;
const vector<string>& info_tags,
const vector<string>& info_data,
const map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions);
+ const vector<Expr>& assertions);
int main(int argc, char* argv[])
{
std::map<Expr, unsigned> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
}
}
-void translate_to_mathematica(const map<Expr, unsigned>& variables, const BoolExpr& assertion) {
+void translate_to_mathematica(const map<Expr, unsigned>& variables, const Expr& assertion) {
bool first;
unsigned n = assertion.getNumChildren();
const vector<string>& info_tags,
const vector<string>& info_data,
const std::map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions)
+ const vector<Expr>& assertions)
{
bool first;
const vector<string>& info_tags,
const vector<string>& info_data,
const map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions);
+ const vector<Expr>& assertions);
int main(int argc, char* argv[])
{
std::map<Expr, unsigned> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
}
}
-void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const BoolExpr& assertion) {
+void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const Expr& assertion) {
bool first;
unsigned n = assertion.getNumChildren();
const vector<string>& info_tags,
const vector<string>& info_data,
const std::map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions)
+ const vector<Expr>& assertions)
{
bool first;
const vector<string>& info_tags,
const vector<string>& info_data,
const map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions);
+ const vector<Expr>& assertions);
int main(int argc, char* argv[])
{
std::map<Expr, unsigned> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
}
}
-void translate_to_redlog(const map<Expr, unsigned>& variables, const BoolExpr& assertion) {
+void translate_to_redlog(const map<Expr, unsigned>& variables, const Expr& assertion) {
bool first;
unsigned n = assertion.getNumChildren();
const vector<string>& info_tags,
const vector<string>& info_data,
const std::map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions)
+ const vector<Expr>& assertions)
{
bool first;
Expr three = em.mkConst(Rational(3));
Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three);
- BoolExpr formula =
- BoolExpr(em.mkExpr(kind::AND, x_positive, y_positive)).
- impExpr(BoolExpr(twox_plus_y_geq_3));
+ Expr formula =
+ em.mkExpr(kind::AND, x_positive, y_positive).
+ impExpr(twox_plus_y_geq_3);
cout << "Checking validity of formula " << formula << " with CVC4." << endl;
cout << "CVC4 should report VALID." << endl;
}
void ValidityChecker::assertFormula(const Expr& e) {
- d_smt->assertFormula(CVC4::BoolExpr(e));
+ d_smt->assertFormula(e);
}
void ValidityChecker::registerAtom(const Expr& e) {
}
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() {
/* 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;
}
/* 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;
}
/* 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;
}
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;
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();
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();
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,
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,
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,
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,
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,
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,
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);
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;
return std::vector<Expr>(begin(), end());
}
+ /**
+ * 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 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 {
/**
${getConst_instantiations}
-#line 959 "${template}"
+#line 930 "${template}"
namespace expr {
}
static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
- BoolExpr e = c->getExpr();
+ Expr e = c->getExpr();
if(e.isNull()) {
out << "CheckSat()";
} else {
}
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 {
}
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 {
}
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
}
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
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);
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);
#include "expr/node.h"
#include "prop/theory_proxy.h"
#include "prop/registrar.h"
+#include "context/cdlist.h"
#include <ext/hash_map>
}
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);
}
}
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;
}
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();
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();
Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
+ context->pop();
+
// Notify the cnf
proxy->removeClausesAboveLevel(assertionLevel);
}
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
// 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());
}
}
}
}
-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) {
}
}
-Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
+Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) {
Assert(e.isNull() || e.getExprManager() == d_exprManager);
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);
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();
* 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();
* 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
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();
}
}
projects / cvc5.git / commitdiff