[klee-dev] how to add label to assert statements

[Sumit Kumar]

Hi Dan,

Thanks for introducing the z3 support. It has been great help. It has saved
me tons of work :).
Please find below my answers to some of your queries:

>Yes your previous e-mails were misleading because you said
"getConstraintLog method in Executor.cpp is called with
logFormat=STP".

Well, not exactly, because I am explicitly calling the
getConstraintLog(...) method with logFormat=STP option even when the
backend is z3. Now since my backend solver is z3, it in turn calls
getConstraintLog(....) method on the z3 core solver object using the
TimingSolver Object:

    char *log = solver->getConstraintLog(query); //in Executor.cpp inside
function getConstraintLog when logFormat=STP

>If your aim is to get to constraints in the SMT-LIBv2 format then why are
you using ``getConstraintLog()`` which will use the core solver's natural
constraint language (for Z3 this happens to be SMT-LIBv2 but you don't have
fine the grained control you need)? Instead you should do what Thuan is
suggesting and modify the ExprSMTLIBPrinter to add labels if that is your
goal.

I chose to use the getConstraintLog method instead of modifying
ExprSMTLIBPrinter for these reasons:
1. getConstraintLog(..) exposes Z3 C api to me. It allows me to modify/use
Z3 C api to get desired output.
2. getConstraintLog(..) method returns me a string instead of printing the
result.
Also, although I started with printing labels to assert statements, I later
realized that I didn't need to do that as I had access to z3 c/c++ api and
could pass the labels to z3 directly.

>If you are already using Z3 as the solver backend why don't you use
its C API to get the unsat core?

I also realized the same sometime back :) . I have already done exactly
what you have suggested. I am able to get the unsat core using the z3 c++
api.

P.S: While working on this I realized that it would be a lot better if
instead of using Z3 C api, C++ api was used as Z3 C++ api is much easier to
use than Z3 C api. I wonder if it would be good to rewrite the Z3 Core
Solver methods using Z3 C++ api.

--
Thanks and Regards,
Sumit


On 29 April 2016 at 02:19, Dan Liew <dan at su-root.co.uk> wrote:

> Hi,
>
> On 28 April 2016 at 20:57, Sumit Kumar <sumit686215 at gmail.com> wrote:
> > Hi,
> > I forgot to add this earlier and I think that this is important in this
> > context: I am running klee with following setting: -solver-backend=z3. I
> > apologize for missing this information.
>
> Yes your previous e-mails were misleading because you said
> "getConstraintLog method in Executor.cpp is called with
> logFormat=STP". It's cool that you're using the Z3 support I recently
> introduced but I am very bemused by how you are using it.
>
> * If your aim is to get to constraints in the SMT-LIBv2 format then
> why are you using ``getConstraintLog()`` which will use the core
> solver's natural constraint language (for Z3 this happens to be
> SMT-LIBv2 but you don't have fine the grained control you need)?
> Instead you should do what Thuan is suggesting and modify the
> ExprSMTLIBPrinter to add labels if that is your goal.
>
> * If you are already using Z3 as the solver backend why don't you use
> its C API to get the unsat core?
>
> Dan.
>
-------------- next part --------------
HTML attachment scrubbed and removed