mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

more ML

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-26 16:54:45 +00:00
parent 25498345e5
commit c03d5277bc
2 changed files with 36 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

58
examples/ml/ml_example.ml
View file

@ -10,11 +10,12 @@ open Z3.Expr
open Z3.FuncDecl
open Z3.Goal
open Z3.Tactic
open Z3.Tactic.ApplyResult
open Z3.Probe
open Z3.Solver
open Z3.Arithmetic
exception ExampleException of string
exception TestFailedException of string
(**
@ -43,32 +44,37 @@ let basic_tests ( ctx : context ) =
let solver = (mk_solver ctx None) in
(Array.iter (fun a -> (Solver.assert_ solver [| a |])) (get_formulas g)) ;
if (check solver None) != SATISFIABLE then
raise (ExampleException "")
raise (TestFailedException "")
else
Printf.printf "Test passed.\n" ;
()
(*
ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g);
if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat))
throw new TestFailedException();
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g);
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
throw new TestFailedException();
g.Assert(ctx.MkEq(ctx.MkNumeral(1, ctx.MkBitVecSort(32)),
ctx.MkNumeral(2, ctx.MkBitVecSort(32))));
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g);
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat)
throw new TestFailedException();
Goal g2 = ctx.MkGoal(true, true);
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2);
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
throw new TestFailedException();
() ;
let ar = (Tactic.apply (mk_tactic ctx "simplify") g None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_sat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
(Goal.assert_ g [| (mk_eq ctx (mk_numeral_int ctx 1 (BitVectors.mk_sort ctx 32))
(mk_numeral_int ctx 2 (BitVectors.mk_sort ctx 32))) |] )
;
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
let g2 = (mk_goal ctx true true false) in
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_sat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
()
(*
g2 = ctx.MkGoal(true, true);
g2.Assert(ctx.MkFalse());
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2);
@ -131,7 +137,7 @@ let basic_tests ( ctx : context ) =
let _ =
if not (Log.open_ "z3.log") then
raise (ExampleException "Log couldn't be opened.")
raise (TestFailedException "Log couldn't be opened.")
else
(
Printf.printf "Running Z3 version %s\n" Version.to_string ;

4
src/api/ml/z3.ml
View file

@ -4391,6 +4391,10 @@ struct
let n = (get_num_subgoals x) in
let f i = (new goal x#gc)#cnstr_obj (Z3native.apply_result_get_subgoal x#gnc x#gno i) in
Array.init n f
(** Retrieves the subgoals from the apply_result. *)
let get_subgoal ( x : apply_result ) ( i : int ) =
(new goal x#gc)#cnstr_obj (Z3native.apply_result_get_subgoal x#gnc x#gno i)
(** Convert a model for the subgoal <paramref name="i"/> into a model for the original
goal <c>g</c>, that the ApplyResult was obtained from.