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

ML API: renamed assert_ to add

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-02-26 19:45:45 +00:00
parent 050629536a
commit c1e29dabe7
3 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
examples/ml/ml_example.ml
View file

@ -29,11 +29,11 @@ let model_converter_test ( ctx : context ) =
let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
let g4 = (mk_goal ctx true false false ) in let g4 = (mk_goal ctx true false false ) in
(Goal.assert_ g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ; (Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
(Goal.assert_ g4 [ (mk_eq ctx (Goal.add g4 [ (mk_eq ctx
yr yr
(Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ; (Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ;
(Goal.assert_ g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ; (Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
( (
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
if ((get_num_subgoals ar) == 1 && if ((get_num_subgoals ar) == 1 &&
@ -53,7 +53,7 @@ let model_converter_test ( ctx : context ) =
Printf.printf "Test passed.\n" Printf.printf "Test passed.\n"
; ;
let solver = (mk_solver ctx None) in let solver = (mk_solver ctx None) in
let f e = (Solver.assert_ solver [ e ]) in let f e = (Solver.add solver [ e ]) in
ignore (List.map f (get_formulas (get_subgoal ar 0))) ; ignore (List.map f (get_formulas (get_subgoal ar 0))) ;
let q = (check solver []) in let q = (check solver []) in
if q != SATISFIABLE then if q != SATISFIABLE then
@ -88,12 +88,12 @@ let basic_tests ( ctx : context ) =
let trivial_eq = (mk_eq ctx fapp fapp) in let trivial_eq = (mk_eq ctx fapp fapp) in
let nontrivial_eq = (mk_eq ctx fapp fapp2) in let nontrivial_eq = (mk_eq ctx fapp fapp2) in
let g = (mk_goal ctx true false false) in let g = (mk_goal ctx true false false) in
(Goal.assert_ g [ trivial_eq ]) ; (Goal.add g [ trivial_eq ]) ;
(Goal.assert_ g [ nontrivial_eq ]) ; (Goal.add g [ nontrivial_eq ]) ;
Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ; Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ;
( (
let solver = (mk_solver ctx None) in let solver = (mk_solver ctx None) in
(List.iter (fun a -> (Solver.assert_ solver [ a ])) (get_formulas g)) ; (List.iter (fun a -> (Solver.add solver [ a ])) (get_formulas g)) ;
if (check solver []) != SATISFIABLE then if (check solver []) != SATISFIABLE then
raise (TestFailedException "") raise (TestFailedException "")
else else
@ -116,7 +116,7 @@ let basic_tests ( ctx : context ) =
else else
Printf.printf "Test passed.\n" Printf.printf "Test passed.\n"
); );
(Goal.assert_ g [ (mk_eq ctx (Goal.add g [ (mk_eq ctx
(mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32)) (mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32))
(mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] ) (mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] )
; ;
@ -139,7 +139,7 @@ let basic_tests ( ctx : context ) =
); );
( (
let g2 = (mk_goal ctx true true false) in let g2 = (mk_goal ctx true true false) in
(Goal.assert_ g2 [ (Boolean.mk_false ctx) ]) ; (Goal.add g2 [ (Boolean.mk_false ctx) ]) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 && if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then (not (is_decided_unsat (get_subgoal ar 0)))) then
@ -151,10 +151,10 @@ let basic_tests ( ctx : context ) =
let g3 = (mk_goal ctx true true false) in let g3 = (mk_goal ctx true true false) in
let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in
let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in
(Goal.assert_ g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ; (Goal.add g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ;
(Goal.assert_ g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ; (Goal.add g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ;
let constr = (mk_eq ctx xc yc) in let constr = (mk_eq ctx xc yc) in
(Goal.assert_ g3 [ constr ] ) ; (Goal.add g3 [ constr ] ) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in
if ((get_num_subgoals ar) == 1 && if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then (not (is_decided_unsat (get_subgoal ar 0)))) then

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

@ -1850,7 +1850,7 @@ struct
let is_garbage ( x : goal ) = let is_garbage ( x : goal ) =
(get_precision x) == GOAL_UNDER_OVER (get_precision x) == GOAL_UNDER_OVER
let assert_ ( x : goal ) ( constraints : expr list ) = let add ( x : goal ) ( constraints : expr list ) =
let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e) in let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e) in
ignore (List.map f constraints) ; ignore (List.map f constraints) ;
() ()
@ -2370,11 +2370,11 @@ struct
let reset ( x : solver ) = Z3native.solver_reset (z3obj_gnc x) (z3obj_gno x) let reset ( x : solver ) = Z3native.solver_reset (z3obj_gnc x) (z3obj_gno x)
let assert_ ( x : solver ) ( constraints : expr list ) = let add ( x : solver ) ( constraints : expr list ) =
let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in
ignore (List.map f constraints) ignore (List.map f constraints)
let assert_and_track_a ( x : solver ) ( cs : expr list ) ( ps : expr list ) = let assert_and_track_l ( x : solver ) ( cs : expr list ) ( ps : expr list ) =
if ((List.length cs) != (List.length ps)) then if ((List.length cs) != (List.length ps)) then
raise (Z3native.Exception "Argument size mismatch") raise (Z3native.Exception "Argument size mismatch")
else else
@ -2473,7 +2473,7 @@ struct
let get_param_descrs ( x : fixedpoint ) = let get_param_descrs ( x : fixedpoint ) =
Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
let assert_ ( x : fixedpoint ) ( constraints : expr list ) = let add ( x : fixedpoint ) ( constraints : expr list ) =
let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in
ignore (List.map f constraints) ; ignore (List.map f constraints) ;
() ()

8
src/api/ml/z3.mli
View file

@ -2221,7 +2221,7 @@ sig
val is_garbage : goal -> bool val is_garbage : goal -> bool
(** Adds the constraints to the given goal. *) (** Adds the constraints to the given goal. *)
val assert_ : goal -> Expr.expr list -> unit val add : goal -> Expr.expr list -> unit
(** Indicates whether the goal contains `false'. *) (** Indicates whether the goal contains `false'. *)
val is_inconsistent : goal -> bool val is_inconsistent : goal -> bool
@ -2648,7 +2648,7 @@ sig
val reset : solver -> unit val reset : solver -> unit
(** Assert a constraint (or multiple) into the solver. *) (** Assert a constraint (or multiple) into the solver. *)
val assert_ : solver -> Expr.expr list -> unit val add : solver -> Expr.expr list -> unit
(** * Assert multiple constraints (cs) into the solver, and track them (in the (** * Assert multiple constraints (cs) into the solver, and track them (in the
* unsat) core * unsat) core
@ -2661,7 +2661,7 @@ sig
* of the Boolean variables provided using {!assert_and_track} * of the Boolean variables provided using {!assert_and_track}
* and the Boolean literals * and the Boolean literals
* provided using {!check} with assumptions. *) * provided using {!check} with assumptions. *)
val assert_and_track_a : solver -> Expr.expr list -> Expr.expr list -> unit val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit
(** * Assert a constraint (c) into the solver, and track it (in the unsat) core (** * Assert a constraint (c) into the solver, and track it (in the unsat) core
* using the Boolean constant p. * using the Boolean constant p.
@ -2752,7 +2752,7 @@ sig
val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs
(** Assert a constraints into the fixedpoint solver. *) (** Assert a constraints into the fixedpoint solver. *)
val assert_ : fixedpoint -> Expr.expr list -> unit val add : fixedpoint -> Expr.expr list -> unit
(** Register predicate as recursive relation. *) (** Register predicate as recursive relation. *)
val register_relation : fixedpoint -> FuncDecl.func_decl -> unit val register_relation : fixedpoint -> FuncDecl.func_decl -> unit