Commit 1f7a336a authored by Cristian Cadar's avatar Cristian Cadar Committed by Dan Liew
Browse files

Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to...

Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to negateQueryExpression() to make it clear what it does."

git-svn-id: 91177308-0d34-0410-b5e6-96231b3b80d8
parent 6505e9db
......@@ -198,7 +198,7 @@ namespace klee {
//Print SMTLIBv2 for all constraints in the query
virtual void printConstraints();
//Print SMTLIBv2 assert statement for the "mangled" query
//Print SMTLIBv2 assert statement for the negated query expression
virtual void printQuery();
///Print the SMTLIBv2 command to check satisfiability and also optionally request for values
......@@ -261,7 +261,7 @@ namespace klee {
PrintContext* p;
///This contains the query from the solver but negated for our purposes.
/// \sa mangleQuery()
/// \sa negateQueryExpression()
ref<Expr> queryAssert;
///Indicates if there were any constant arrays founds during a scan()
......@@ -277,7 +277,7 @@ namespace klee {
std::map<SMTLIBboolOptions,bool> smtlibBoolOptions;
///This sets queryAssert to be the boolean negation of the original Query
void mangleQuery();
void negateQueryExpression();
//Print a SMTLIBv2 option as a C-string
const char* getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option);
......@@ -69,7 +69,7 @@ namespace klee
query = &q;
reset(); // clear the data structures
void ExprSMTLIBPrinter::reset()
......@@ -831,7 +831,7 @@ namespace klee
*p << ")";
void ExprSMTLIBPrinter::mangleQuery()
void ExprSMTLIBPrinter::negateQueryExpression()
//Negating the query
queryAssert = Expr::createIsZero(query->expr);
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment