On 7-4-2015 13:38, Tjark Weber wrote: > On Tue, 2015-04-07 at 12:27 +0200, Wishnu Prasetya wrote: >> Suppose I want to use a more recent version of Z3... will it be a lot of >> work to tweak the source code of HolSmt to achieve this? > There is only one way to find out: try it. As long as the input/output > syntax of Z3 hasn't changed, at least Z3_ORACLE_TAC should work. Proof > reconstruction (as performed by Z3_TAC) is probably somewhat more > fragile, as there never was a standardized proof format. I'd be > interested in the results of your experiments, and would be happy to > help fixing minor issues.
Ok, I tried it with few examples. This is what I did: * export HOL4_Z3_EXECUTABLE="/usr/local/z3-4.4.0/bin/z3" * load and open HolSmtLib from HOL * Z3_ORACLE_TAC is unavailable, because the self-configuration mechanism of HOLsmt does not recognize my new Z3. Saying: <<HOL message: HolSmtLib: solver Z3 (oracle) is available.>> ERROR: the parameter 'proof_mode' was renamed to 'proof', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:proof' for the full description of the parameter * BUT, I can invoke the worker function behind Z3_ORACLE as you pointed out: > Z3.Z3_SMT_Oracle ([],--`(x:int)>y ==> (x+1)>(y+1)`--) ; val it = UNSAT NONE: SolverSpec.result I can subsequently lift this to a tactic with some bits of programming. But anyway, it looks like it works! So, thanks again for the tips. --Wish. > > Fully supporting Z3 4.x would probably require a few days' worth of > changes to the HolSmt code base. If you don't have to use HOL4, you > might consider taking a look at Isabelle/HOL, which offers a similar > integration of (more recent versions of) Z3. > > Best, > Tjark > > ------------------------------------------------------------------------------ BPM Camp - Free Virtual Workshop May 6th at 10am PDT/1PM EDT Develop your own process in accordance with the BPMN 2 standard Learn Process modeling best practices with Bonita BPM through live exercises http://www.bonitasoft.com/be-part-of-it/events/bpm-camp-virtual- event?utm_ source=Sourceforge_BPM_Camp_5_6_15&utm_medium=email&utm_campaign=VA_SF _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
