Hi all, I am working on klee and trying to integrate it with another solver (CVC4) to do some test. I found that klee communicates with STP by calling the c_interface.h. The good thing is that the solver I am using has the same interface (same name) and some of the inside functions have overlaps. I'm wondering if there is anythings other than the STPBuilder that I need to change in order to make this integration, because Daniel has mentioned that he did something so that klee can be separated from STP(http://www.mail-archive.com/[email protected]/msg00030.html).
Also, I know klee runs based on the .o file generated by llvm. So I want to ask in what language does klee represent the constraints and passing them to the solver? Is it in still in readable language such as SMT or CVC, or some lower level representation? Last question about the big picture of klee, in order to have a better understanding about how klee deals with constraints, what part of the code should I pay more attention to? Thanks in advance for helping me with these basic questions. Best Regards, Shiyu -- Shiyu Dong Graduate Student Electrical & Computer Engineering University of Texas at Austin Tel: (512) 927-7817 E-mail: [email protected]
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
