Hi Dan, On 29 April 2016 at 14:30, Dan Liew <d...@su-root.co.uk> wrote:
> 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. > I was talking about 'Z3SolverImpl::getConstraintLog(const Query &query)' which is eventually called by Executor::getConstraintLog(...) when the backend is 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). > > Thanks for the suggestion. It has improved my understanding. 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(..)``? > > I used Z3 C++ API. I created a new solver object and used this method: "solver::add(z3::expr, z3::char*)" > >>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. > Let's hope it catches up fast. Z3 C++ api will make things really easy to understand and use. > 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. > I could not understand the 3rd point. Can you please explain it a little more. It would help me understand the working of KLEE better. -- Thanks and Regards, Sumit
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
