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 new ML API.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-23 04:00:34 +00:00
parent f1ecf3ae0b
commit 49a4e77a6d
3 changed files with 807 additions and 858 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
examples/ml/ml_example.ml
View file

@ -4,7 +4,7 @@
*)
open Z3
open Z3.Context
open Z3.Arithmetic
exception ExampleException of string
@ -16,9 +16,9 @@ let _ =
Printf.printf "Running Z3 version %s\n" Version.to_string ;
let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (new context cfg) in
let is = (mk_symbol_int ctx 42) in
let ss = (mk_symbol_string ctx "mySymbol") in
let bs = (mk_bool_sort ctx) in
let is = (Symbol.mk_int ctx 42) in
let ss = (Symbol.mk_string ctx "mySymbol") in
let bs = (Sort.mk_bool ctx) in
let ints = (mk_int_sort ctx) in
let rs = (mk_real_sort ctx) in
Printf.printf "int symbol: %s\n" (Symbol.to_string (is :> symbol));

13
scripts/update_api.py
View file

@ -1154,8 +1154,11 @@ def mk_ml():
for k, v in Type2Str.iteritems():
if is_obj(k):
ml_native.write('and %s = ptr\n' % v.lower())
ml_native.write('\nexternal is_null : ptr -> bool\n')
ml_native.write('\n')
ml_native.write('external is_null : ptr -> bool\n')
ml_native.write(' = "n_is_null"\n\n')
ml_native.write('external mk_null : unit -> ptr\n')
ml_native.write(' = "n_mk_null"\n\n')
ml_native.write('exception Exception of string\n\n')
# ML declarations
@ -1295,6 +1298,14 @@ def mk_ml():
ml_wrapper.write('CAMLprim value n_is_null(value p) {\n')
ml_wrapper.write(' return Val_bool(Data_custom_val(p) == 0);\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('CAMLprim value n_mk_null( void ) {\n')
ml_wrapper.write(' CAMLparam0();\n')
ml_wrapper.write(' CAMLlocal1(result);\n')
ml_wrapper.write(' void * z3_result = 0;\n')
ml_wrapper.write(' result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1);\n')
ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n')
ml_wrapper.write(' CAMLreturn (result);\n')
ml_wrapper.write('}\n\n')
for name, result, params in _dotnet_decls:
ip = inparams(params)
op = outparams(params)

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

@ -593,6 +593,10 @@ object (self)
method cnstr_obj obj = (self#sno ctx obj) ; self
end
let patternaton (a : pattern array) =
let f (e : pattern) = e#gno in
Array.map f a
(** Parameter description objects *)
class param_descrs ctx =
object (self)
@ -1607,6 +1611,306 @@ struct
*)
let mk_or ( ctx : context ) ( args : bool_expr array ) =
(new bool_expr ctx)#cnstr_obj (Z3native.mk_or ctx#gno (Array.length args) (astaton args))
(**
Create a numeral of a given sort.
@param v A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form <c>[num]* / [num]*</c>.
@param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
@return A Term with value <paramref name="v"/> and sort <paramref name="ty"/>
*)
let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : sort ) =
create_expr ctx (Z3native.mk_numeral ctx#gno v ty#gno)
(**
Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
@param v Value of the numeral
@param ty Sort of the numeral
@return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
*)
let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) =
create_expr ctx (Z3native.mk_int ctx#gno v ty#gno)
end
(** Quantifier expressions *)
module Quantifiers =
struct
(**
The de-Burijn index of a bound variable.
<remarks>
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
the meaning of de-Bruijn indices by indicating the compilation process from
non-de-Bruijn formulas to de-Bruijn format.
<code>
abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
abs1(x, x, n) = b_n
abs1(y, x, n) = y
abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
</code>
The last line is significant: the index of a bound variable is different depending
on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its
index.
*)
let get_index ( x : expr ) =
if not (AST.is_var x) then
raise (Z3native.Exception "Term is not a bound variable.")
else
Z3native.get_index_value x#gnc x#gno
(** Quantifier patterns
Patterns comprise a list of terms. The list should be
non-empty. If the list comprises of more than one term, it is
also called a multi-pattern.
*)
module Pattern =
struct
(**
The number of terms in the pattern.
*)
let get_num_terms ( x : pattern ) =
Z3native.get_pattern_num_terms x#gnc x#gno
(**
The terms in the pattern.
*)
let get_terms ( x : pattern ) =
let n = (get_num_terms x) in
let f i = (create_expr x#gc (Z3native.get_pattern x#gnc x#gno i)) in
Array.init n f
(**
A string representation of the pattern.
*)
let to_string ( x : pattern ) = Z3native.pattern_to_string x#gnc x#gno
end
(**
Indicates whether the quantifier is universal.
*)
let is_universal ( x : quantifier ) =
lbool_of_int (Z3native.is_quantifier_forall x#gnc x#gno) == L_TRUE
(**
Indicates whether the quantifier is existential.
*)
let is_existential ( x : quantifier ) = not (is_universal x)
(**
The weight of the quantifier.
*)
let get_weight ( x : quantifier ) = Z3native.get_quantifier_weight x#gnc x#gno
(**
The number of patterns.
*)
let get_num_patterns ( x : quantifier ) = Z3native.get_quantifier_num_patterns x#gnc x#gno
(**
The patterns.
*)
let get_patterns ( x : quantifier ) =
let n = (get_num_patterns x) in
let f i = ((new pattern x#gc)#cnstr_obj (Z3native.get_quantifier_pattern_ast x#gnc x#gno i)) in
Array.init n f
(**
The number of no-patterns.
*)
let get_num_no_patterns ( x : quantifier ) = Z3native.get_quantifier_num_no_patterns x#gnc x#gno
(**
The no-patterns.
*)
let get_no_patterns ( x : quantifier ) =
let n = (get_num_patterns x) in
let f i = ((new pattern x#gc)#cnstr_obj (Z3native.get_quantifier_no_pattern_ast x#gnc x#gno i)) in
Array.init n f
(**
The number of bound variables.
*)
let get_num_bound ( x : quantifier ) = Z3native.get_quantifier_num_bound x#gnc x#gno
(**
The symbols for the bound variables.
*)
let get_bound_variable_names ( x : quantifier ) =
let n = (get_num_bound x) in
let f i = (create_symbol x#gc (Z3native.get_quantifier_bound_name x#gnc x#gno i)) in
Array.init n f
(**
The sorts of the bound variables.
*)
let get_bound_variable_sorts ( x : quantifier ) =
let n = (get_num_bound x) in
let f i = (create_sort x#gc (Z3native.get_quantifier_bound_sort x#gnc x#gno i)) in
Array.init n f
(**
The body of the quantifier.
*)
let get_body ( x : quantifier ) =
(new bool_expr x#gc)#cnstr_obj (Z3native.get_quantifier_body x#gnc x#gno)
(**
Creates a new bound variable.
@param index The de-Bruijn index of the variable
@param ty The sort of the variable
*)
let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) =
create_expr ctx (Z3native.mk_bound ctx#gno index ty#gno)
(**
Create a quantifier pattern.
*)
let mk_pattern ( ctx : context ) ( terms : expr array ) =
if (Array.length terms) == 0 then
raise (Z3native.Exception "Cannot create a pattern from zero terms")
else
(new pattern ctx)#cnstr_obj (Z3native.mk_pattern ctx#gno (Array.length terms) (astaton terms))
(**
Create a universal Quantifier.
<remarks>
Creates a forall formula, where <paramref name="weight"/> is the weight,
<paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
with the sorts of the bound variables, <paramref name="names"/> is an array with the
'names' of the bound variables, and <paramref name="body"/> is the body of the
quantifier. Quantifiers are associated with weights indicating
the importance of using the quantifier during instantiation.
@param sorts the sorts of the bound variables.
@param names names of the bound variables
@param body the body of the quantifier.
@param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
@param patterns array containing the patterns created using <c>MkPattern</c>.
@param noPatterns array containing the anti-patterns created using <c>MkPattern</c>.
@param quantifierID optional symbol to track quantifier.
@param skolemID optional symbol to track skolem constants.
*)
let mk_forall ( ctx : context ) ( sorts : sort array ) ( names : symbol array ) ( body : expr) ( weight : int option ) ( patterns : pattern array option ) ( nopatterns : pattern array option ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
if (Array.length sorts) != (Array.length names) then
raise (Z3native.Exception "Number of sorts does not match number of names")
else if (nopatterns == None && quantifier_id == None && skolem_id == None) then
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier ctx#gno (int_of_lbool L_TRUE)
(match weight with | None -> 1 | Some(x) -> x)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
(Array.length sorts) (astaton sorts)
(astaton names)
body#gno)
else
let null = Z3native.mk_null() in
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_ex ctx#gno (int_of_lbool L_TRUE)
(match weight with | None -> 1 | Some(x) -> x)
(match quantifier_id with | None -> null | Some(x) -> x#gno)
(match skolem_id with | None -> null | Some(x) -> x#gno)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
(match nopatterns with | None -> 0 | Some(x) -> (Array.length x))
(match nopatterns with | None -> [||] | Some(x) -> (patternaton x))
(Array.length sorts) (astaton sorts)
(astaton names)
body#gno)
(**
Create a universal Quantifier.
*)
let mk_forall_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr) ( weight : int option ) ( patterns : pattern array option ) ( nopatterns : pattern array option ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
if (nopatterns == None && quantifier_id == None && skolem_id == None) then
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const ctx#gno (int_of_lbool L_TRUE)
(match weight with | None -> 1 | Some(x) -> x)
(Array.length bound_constants) (expraton bound_constants)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
body#gno)
else
let null = Z3native.mk_null() in
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const_ex ctx#gno (int_of_lbool L_TRUE)
(match weight with | None -> 1 | Some(x) -> x)
(match quantifier_id with | None -> null | Some(x) -> x#gno)
(match skolem_id with | None -> null | Some(x) -> x#gno)
(Array.length bound_constants) (expraton bound_constants)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
(match nopatterns with | None -> 0 | Some(x) -> (Array.length x))
(match nopatterns with | None -> [||] | Some(x) -> (patternaton x))
body#gno)
(**
Create an existential Quantifier.
<seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
*)
let mk_exists ( ctx : context ) ( sorts : sort array ) ( names : symbol array ) ( body : expr) ( weight : int option ) ( patterns : pattern array option ) ( nopatterns : pattern array option ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
if (Array.length sorts) != (Array.length names) then
raise (Z3native.Exception "Number of sorts does not match number of names")
else if (nopatterns == None && quantifier_id == None && skolem_id == None) then
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier ctx#gno (int_of_lbool L_FALSE)
(match weight with | None -> 1 | Some(x) -> x)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
(Array.length sorts) (astaton sorts)
(astaton names)
body#gno)
else
let null = Z3native.mk_null() in
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_ex ctx#gno (int_of_lbool L_FALSE)
(match weight with | None -> 1 | Some(x) -> x)
(match quantifier_id with | None -> null | Some(x) -> x#gno)
(match skolem_id with | None -> null | Some(x) -> x#gno)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
(match nopatterns with | None -> 0 | Some(x) -> (Array.length x))
(match nopatterns with | None -> [||] | Some(x) -> (patternaton x))
(Array.length sorts) (astaton sorts)
(astaton names)
body#gno)
(**
Create an existential Quantifier.
*)
let mk_exists_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr) ( weight : int option ) ( patterns : pattern array option ) ( nopatterns : pattern array option ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
if (nopatterns == None && quantifier_id == None && skolem_id == None) then
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const ctx#gno (int_of_lbool L_FALSE)
(match weight with | None -> 1 | Some(x) -> x)
(Array.length bound_constants) (expraton bound_constants)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
body#gno)
else
let null = Z3native.mk_null() in
(new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const_ex ctx#gno (int_of_lbool L_FALSE)
(match weight with | None -> 1 | Some(x) -> x)
(match quantifier_id with | None -> null | Some(x) -> x#gno)
(match skolem_id with | None -> null | Some(x) -> x#gno)
(Array.length bound_constants) (expraton bound_constants)
(match patterns with | None -> 0 | Some(x) -> (Array.length x))
(match patterns with | None -> [||] | Some(x) -> (patternaton x))
(match nopatterns with | None -> 0 | Some(x) -> (Array.length x))
(match nopatterns with | None -> [||] | Some(x) -> (patternaton x))
body#gno)
(**
Create a Quantifier.
*)
let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort array ) ( names : symbol array ) ( body : expr) ( weight : int option ) ( patterns : pattern array option ) ( nopatterns : pattern array option ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
if (universal) then
(mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id)
else
(mk_exists ctx sorts names body weight patterns nopatterns quantifier_id skolem_id)
(**
Create a Quantifier.
*)
let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : expr array ) ( body : expr) ( weight : int option ) ( patterns : pattern array option ) ( nopatterns : pattern array option ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
if (universal) then
mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id
else
mk_exists_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id
end
(** Functions to manipulate Array expressions *)
@ -2002,148 +2306,6 @@ struct
end
(** Quantifier expressions *)
module Quantifiers =
struct
(**
The de-Burijn index of a bound variable.
<remarks>
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
the meaning of de-Bruijn indices by indicating the compilation process from
non-de-Bruijn formulas to de-Bruijn format.
<code>
abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
abs1(x, x, n) = b_n
abs1(y, x, n) = y
abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
</code>
The last line is significant: the index of a bound variable is different depending
on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its
index.
*)
let get_index ( x : expr ) =
if not (AST.is_var x) then
raise (Z3native.Exception "Term is not a bound variable.")
else
Z3native.get_index_value x#gnc x#gno
(** Quantifier patterns
Patterns comprise a list of terms. The list should be
non-empty. If the list comprises of more than one term, it is
also called a multi-pattern.
*)
module Pattern =
struct
(**
The number of terms in the pattern.
*)
let get_num_terms ( x : pattern ) =
Z3native.get_pattern_num_terms x#gnc x#gno
(**
The terms in the pattern.
*)
let get_terms ( x : pattern ) =
let n = (get_num_terms x) in
let f i = (create_expr x#gc (Z3native.get_pattern x#gnc x#gno i)) in
Array.init n f
(**
A string representation of the pattern.
*)
let to_string ( x : pattern ) = Z3native.pattern_to_string x#gnc x#gno
end
(**
Indicates whether the quantifier is universal.
*)
let is_universal ( x : quantifier ) =
lbool_of_int (Z3native.is_quantifier_forall x#gnc x#gno) == L_TRUE
(**
Indicates whether the quantifier is existential.
*)
let is_existential ( x : quantifier ) = not (is_universal x)
(**
The weight of the quantifier.
*)
let get_weight ( x : quantifier ) = Z3native.get_quantifier_weight x#gnc x#gno
(**
The number of patterns.
*)
let get_num_patterns ( x : quantifier ) = Z3native.get_quantifier_num_patterns x#gnc x#gno
(**
The patterns.
*)
let get_patterns ( x : quantifier ) =
let n = (get_num_patterns x) in
let f i = ((new pattern x#gc)#cnstr_obj (Z3native.get_quantifier_pattern_ast x#gnc x#gno i)) in
Array.init n f
(**
The number of no-patterns.
*)
let get_num_no_patterns ( x : quantifier ) = Z3native.get_quantifier_num_no_patterns x#gnc x#gno
(**
The no-patterns.
*)
let get_no_patterns ( x : quantifier ) =
let n = (get_num_patterns x) in
let f i = ((new pattern x#gc)#cnstr_obj (Z3native.get_quantifier_no_pattern_ast x#gnc x#gno i)) in
Array.init n f
(**
The number of bound variables.
*)
let get_num_bound ( x : quantifier ) = Z3native.get_quantifier_num_bound x#gnc x#gno
(**
The symbols for the bound variables.
*)
let get_bound_variable_names ( x : quantifier ) =
let n = (get_num_bound x) in
let f i = (create_symbol x#gc (Z3native.get_quantifier_bound_name x#gnc x#gno i)) in
Array.init n f
(**
The sorts of the bound variables.
*)
let get_bound_variable_sorts ( x : quantifier ) =
let n = (get_num_bound x) in
let f i = (create_sort x#gc (Z3native.get_quantifier_bound_sort x#gnc x#gno i)) in
Array.init n f
(**
The body of the quantifier.
*)
let get_body ( x : quantifier ) =
(new bool_expr x#gc)#cnstr_obj (Z3native.get_quantifier_body x#gnc x#gno)
(**
Creates a new bound variable.
@param index The de-Bruijn index of the variable
@param ty The sort of the variable
*)
let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) =
create_expr ctx (Z3native.mk_bound ctx#gno index ty#gno)
(**
Create a quantifier pattern.
*)
let mk_pattern ( ctx : context ) ( terms : expr array ) =
if (Array.length terms) == 0 then
raise (Z3native.Exception "Cannot create a pattern from zero terms")
else
(new pattern ctx)#cnstr_obj (Z3native.mk_pattern ctx#gno (Array.length terms) (astaton terms))
end
(** Functions to manipulate Datatype expressions *)
module Datatypes =
struct
@ -2639,6 +2801,53 @@ struct
let to_decimal_string ( x : algebraic_num ) ( precision : int ) =
Z3native.get_numeral_decimal_string x#gnc x#gno precision
(**
Create a real from a fraction.
@param num numerator of rational.
@param den denominator of rational.
@return A Term with value <paramref name="num"/>/<paramref name="den"/> and sort Real
<seealso cref="MkNumeral(string, Sort)"/>
*)
let mk_real_numeral_nd ( ctx : context ) ( num : int ) ( den : int) =
if (den == 0) then
raise (Z3native.Exception "Denominator is zero")
else
(new rat_num ctx)#cnstr_obj (Z3native.mk_real ctx#gno num den)
(**
Create a real numeral.
@param v A string representing the Term value in decimal notation.
@return A Term with value <paramref name="v"/> and sort Real
*)
let mk_real_numeral_s ( ctx : context ) ( v : string ) =
(new rat_num ctx)#cnstr_obj (Z3native.mk_numeral ctx#gno v (mk_real_sort ctx)#gno)
(**
Create a real numeral.
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Real
*)
let mk_real_numeral_i ( ctx : context ) ( v : int ) =
(new rat_num ctx)#cnstr_obj (Z3native.mk_int ctx#gno v (mk_real_sort ctx)#gno)
(**
Create an integer numeral.
@param v A string representing the Term value in decimal notation.
*)
let mk_int_numeral_s ( ctx : context ) ( v : string ) =
(new int_num ctx)#cnstr_obj (Z3native.mk_numeral ctx#gno v (mk_int_sort ctx)#gno)
(**
Create an integer numeral.
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Integer
*)
let mk_int_numeral_i ( ctx : context ) ( v : int ) =
(new int_num ctx)#cnstr_obj (Z3native.mk_int ctx#gno v (mk_int_sort ctx)#gno)
(** Returns a string representation of the numeral. *)
let to_string ( x : algebraic_num ) = Z3native.get_numeral_string x#gnc x#gno
end
@ -3387,9 +3596,17 @@ struct
let mk_mul_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
(new bool_expr ctx)#cnstr_obj (Z3native.mk_bvmul_no_underflow ctx#gno t1#gno t2#gno)
(**
Create a bit-vector numeral.
@param v A string representing the value in decimal notation.
@param size the size of the bit-vector
*)
let mk_numeral ( ctx : context ) ( ctx : context ) ( v : string ) ( size : int) =
(new bitvec_num ctx)#cnstr_obj (Z3native.mk_numeral ctx#gno v (mk_sort ctx size)#gno)
end
(** Functions to manipulate Proof objects *)
(** Functions to manipulate proof expressions *)
module Proofs =
struct
(**
@ -4567,284 +4784,6 @@ end
(* STUFF FROM THE CONTEXT *)
(**
(* NUMERALS *)
(* GENERAL NUMERALS *)
(**
Create a Term of a given sort.
*)
@param v A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form <c>[num]* / [num]*</c>.
@param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
@return A Term with value <paramref name="v"/> and sort <paramref name="ty"/>
public Expr MkNumeral(string v, Sort ty)
create_expr ctx (Z3native.mk_numeral ctx#gno v, ty#gno)
(**
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
*)
@param v Value of the numeral
@param ty Sort of the numeral
@return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
public Expr MkNumeral(int v, Sort ty)
create_expr ctx (Z3native.mk_int ctx#gno v, ty#gno)
(**
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
*)
@param v Value of the numeral
@param ty Sort of the numeral
@return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
public Expr MkNumeral(uint v, Sort ty)
create_expr ctx (Z3native.mk_unsigned_int ctx#gno v, ty#gno)
(**
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
*)
@param v Value of the numeral
@param ty Sort of the numeral
@return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
public Expr MkNumeral(long v, Sort ty)
create_expr ctx (Z3native.mk_int64 ctx#gno v, ty#gno)
(**
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
*)
@param v Value of the numeral
@param ty Sort of the numeral
@return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
public Expr MkNumeral(ulong v, Sort ty)
create_expr ctx (Z3native.mk_unsigned_int64 ctx#gno v, ty#gno)
(* REALS *)
(**
Create a real from a fraction.
*)
@param num numerator of rational.
@param den denominator of rational.
@return A Term with value <paramref name="num"/>/<paramref name="den"/> and sort Real
<seealso cref="MkNumeral(string, Sort)"/>
public RatNum MkReal(int num, int den)
if (den == 0)
throw new Z3Exception("Denominator is zero");
new RatNum(this, Z3native.mk_real ctx#gno num, den)
(**
Create a real numeral.
*)
@param v A string representing the Term value in decimal notation.
@return A Term with value <paramref name="v"/> and sort Real
public RatNum MkReal(string v)
new RatNum(this, Z3native.mk_numeral ctx#gno v, RealSort#gno)
(**
Create a real numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Real
public RatNum MkReal(int v)
new RatNum(this, Z3native.mk_int ctx#gno v, RealSort#gno)
(**
Create a real numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Real
public RatNum MkReal(uint v)
new RatNum(this, Z3native.mk_unsigned_int ctx#gno v, RealSort#gno)
(**
Create a real numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Real
public RatNum MkReal(long v)
new RatNum(this, Z3native.mk_int64 ctx#gno v, RealSort#gno)
(**
Create a real numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Real
public RatNum MkReal(ulong v)
new RatNum(this, Z3native.mk_unsigned_int64 ctx#gno v, RealSort#gno)
(* INTEGERS *)
(**
Create an integer numeral.
*)
@param v A string representing the Term value in decimal notation.
public IntNum MkInt(string v)
new IntNum(this, Z3native.mk_numeral ctx#gno v, IntSort#gno)
(**
Create an integer numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Integer
public IntNum MkInt(int v)
new IntNum(this, Z3native.mk_int ctx#gno v, IntSort#gno)
(**
Create an integer numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Integer
public IntNum MkInt(uint v)
new IntNum(this, Z3native.mk_unsigned_int ctx#gno v, IntSort#gno)
(**
Create an integer numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Integer
public IntNum MkInt(long v)
new IntNum(this, Z3native.mk_int64 ctx#gno v, IntSort#gno)
(**
Create an integer numeral.
*)
@param v value of the numeral.
@return A Term with value <paramref name="v"/> and sort Integer
public IntNum MkInt(ulong v)
new IntNum(this, Z3native.mk_unsigned_int64 ctx#gno v, IntSort#gno)
(* BIT-VECTORS *)
(**
Create a bit-vector numeral.
*)
@param v A string representing the value in decimal notation.
@param size the size of the bit-vector
let mk_bv_ ( ctx : context ) string v, uint size)
(BitVecNum)MkNumeral(v, MkBitVecSort(size)
(**
Create a bit-vector numeral.
*)
@param v value of the numeral.
@param size the size of the bit-vector
let mk_bv_ ( ctx : context ) int v, uint size)
(BitVecNum)MkNumeral(v, MkBitVecSort(size)
(**
Create a bit-vector numeral.
*)
@param v value of the numeral.
@param size the size of the bit-vector
let mk_bv_ ( ctx : context ) uint v, uint size)
(BitVecNum)MkNumeral(v, MkBitVecSort(size)
(**
Create a bit-vector numeral.
*)
@param v value of the numeral.
@param size the size of the bit-vector
let mk_bv_ ( ctx : context ) long v, uint size)
(BitVecNum)MkNumeral(v, MkBitVecSort(size)
(**
Create a bit-vector numeral.
*)
@param v value of the numeral.
@param size the size of the bit-vector
let mk_bv_ ( ctx : context ) ulong v, uint size)
(BitVecNum)MkNumeral(v, MkBitVecSort(size)
// Numerals
(* QUANTIFIERS *)
(**
Create a universal Quantifier.
<remarks>
Creates a forall formula, where <paramref name="weight"/> is the weight,
<paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
with the sorts of the bound variables, <paramref name="names"/> is an array with the
'names' of the bound variables, and <paramref name="body"/> is the body of the
quantifier. Quantifiers are associated with weights indicating
the importance of using the quantifier during instantiation.
*)
@param sorts the sorts of the bound variables.
@param names names of the bound variables
@param body the body of the quantifier.
@param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
@param patterns array containing the patterns created using <c>MkPattern</c>.
@param noPatterns array containing the anti-patterns created using <c>MkPattern</c>.
@param quantifierID optional symbol to track quantifier.
@param skolemID optional symbol to track skolem constants.
public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
(**
Create a universal Quantifier.
*)
public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
(**
Create an existential Quantifier.
*)
<seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
(**
Create an existential Quantifier.
*)
public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
(**
Create a Quantifier.
*)
public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
if (universal)
MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
else
MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
(**
Create a Quantifier.
*)
public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
if (universal)
MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
else
MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
// Expr
(* OPTIONS *)
(**
@ -5496,4 +5435,3 @@ end
GC.SuppressFinalize(this);
*)