Hi,
You can update methods in ExprSMTLIBPrinter class like printConstraints and
printQuery to modify "assert" statements and add "named" at the end of the
assert. Following is the example code for printConstraints
void ExprSMTLIBPrinter::printConstraints()
{
if(humanReadable)
*o << "; Constraints" << endl;
//Generate assert statements for each constraint
for(ConstraintManager::const_iterator i= query->constraints.begin(); i !=
query->constraints.end(); i++)
{
// modified by rubinovk
*p << "(assert (!";
//*p << "(assert ";
p->pushIndent();
printSeperator();
//recurse into Expression
printExpression(*i,SORT_BOOL);
p->popIndent();
printSeperator();
//added by rubinovk
*p << ":named a" << getAssertNum() << ")";
*p << " )";
//*p << ")";
p->breakLineI();
}
}
The function getAssertNum() gets the next identifier for the label. So
using this function, you can generate query in which assert statements have
labels like a0, a1, a2 and so on. By feeding such query into Z3, you will
get your expected unsat core if the formula is unsatisfiable.
Hope it helps,
Thuan
On Mon, Apr 25, 2016 at 9:44 PM, Sumit Kumar <sumit686...@gmail.com> wrote:
> Hi,
>
> Can anyone please tell me how to add label to each of the assert
> statements in the smt2lib formula emitted by KLEE when getConstraintLog
> method in Executor.cpp is called with logFormat=STP ? Even if anyone has a
> faint idea of how it can be done please tell.
>
> P.S:This will help me to get an unsat core when I feed the constraint log
> to z3 solver.
>
> --
> Thanks and Regards,
> Sumit
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
