On Tue, Jan 24, 2012 at 8:20 AM, Daniel Wainwright <[email protected]> wrote: > Hi, > > I would like to try integrating other constraint solvers into KLEE and > Kleaver, probably Yices and maybe some others, to help make an evaluation of > how the solvers perform on the type of path constraints we're looking at. > > I can see how STP is integrated in, but the problem I've hit is that KLEE > uses the array type in STP, which I don't believe Yices has an equivalent of. > So my question is, what is the simplest way of converting the constraints > KLEE generates into a form Yices can understand? I am guessing this may have > been considered before as it is listed as a proposed project on the KLEE > website. > > If anyone is aware of other constraint solvers that may be more closely > matched to the form of constraints KLEE expects, or knows of work that has > been done comparing constraint solvers this way, that would also be helpful. > > Thanks for you help, > Daniel
Hi, I would be interested in experimenting with constraint solvers, especially SMT [1] solvers, which should be more efficient in many cases. You've pointed out that not all features of one constraint solvers are present in others. What do you think about making first, new layer of abstraction between Klee.Kleavier and Constraint Solvers ? Such layer (which can be API, wrapper, loadable shared library wrapping constraint solver) IMHO could be a good starting point in making next steps of experimenting with constraint solvers. What came to my mind are: * hybrid solutions: I imagine wrapper which uses many constraint solvers depending on type of equations to solve ** choose constraint solver depending on features needed to solve equation ** maybe with some Knowledge Discovery/Data Mining algorithm , to make it learn for when to apply which solver * parrallel/distributed model of constraints solving ** When Klee meets constraint to solve which size is above given threshold, than creates job of solving constraint, leaves current state on waiting queue. When results of solving constraint comes back, than related state/states come back to processing queue. Just a few ideas, where abstracting STP into "constraint_solver" wrapper plus "wrapped STP" would help. Best regards, Grzegorz Wierzowiecki [1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
