mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge pull request #2206 from Bronsa/master

Browse source 
fix name clash in ocaml api
This commit is contained in:
Nikolaj Bjorner 2019-03-26 08:06:47 -07:00 committed by GitHub
parent 8da1b024b7 9008beeb01
commit 3a7bf2cf61
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -717,7 +717,7 @@ struct
else
mk_exists ctx sorts names body weight patterns nopatterns quantifier_id skolem_id
let mk_quantifier (ctx:context) (universal:bool) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =
let mk_quantifier_const (ctx:context) (universal:bool) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =
if universal then
mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id
else

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

@ -743,10 +743,10 @@ sig
val mk_lambda : context -> (Symbol.symbol * Sort.sort) list -> Expr.expr -> quantifier
(** Create a Quantifier. *)
val mk_quantifier : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier
val mk_quantifier : context -> bool -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier
(** Create a Quantifier. *)
val mk_quantifier : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier
val mk_quantifier_const : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier
(** A string representation of the quantifier. *)
val to_string : quantifier -> string