Hi, On 29 April 2016 at 06:55, Sumit Kumar <sumit686...@gmail.com> wrote: > 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
Okay so our naming is really bad here. I've opened an issue so we don't forget to fix this https://github.com/klee/klee/issues/382 >>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. ``Executor::getConstraintLog()`` doesn't really expose the Z3 C API to you. The method just gets the solver to emit the constraint log which if you're using Z3 eventually calls Z3. > 2. getConstraintLog(..) method returns me a string instead of printing the > result. The ExprSMTLIBPrinter doesn't have to "print the result". It just writes to an ``llvm::raw_ostream``. That can be a file but you can also use ``llvm::raw_string_ostream`` instead to write to a std::string. You use the following method to set the output. ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output). Any if you have used ``logFormat=SMTLIB2`` with ``Executor::getConstraintLog()`` you would have got a string in SMT-LIBv2 format. > 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. I'm curious what Z3 C API function did you use to label the Z3_asts? Was it ``Z3_solver_assert_and_track(..)``? >>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. I don't want to use Z3's C++ API for several reasons 1. The C++ API is built on top of the C API so everything the C++ API can do the C API can also do. 2. The C++ API doesn't expose everything the C API does. This is improving but the C API is where all newly exposed features will be added first. 3. We need to control Z3's memory management for Z3_ast and Z3_sort nodes manually. IIRC the C++ API doesn't let you do this. Dan. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
