mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +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 74ab6dbd22
commit c37eb794c2
2 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1850,7 +1850,7 @@ struct
let is_garbage ( x : goal ) =
(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
ignore (List.map f constraints) ;
()
@ -2370,11 +2370,11 @@ struct
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
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
raise (Z3native.Exception "Argument size mismatch")
else
@ -2473,7 +2473,7 @@ struct
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))
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
ignore (List.map f constraints) ;
()