-
Notifications
You must be signed in to change notification settings - Fork 6
/
arith.mli
124 lines (91 loc) · 3.34 KB
/
arith.mli
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
(* Copyright 2014 INRIA *)
(* Module for arithemtic functions *)
exception NotaFormula
exception EndReached
(* Type manipulation *)
val type_int : Expr.expr
val type_rat : Expr.expr
val type_real : Expr.expr
val mix_type : Expr.expr -> Expr.expr -> Expr.expr
(* Q manipulation *)
val is_z : Q.t -> bool
val is_q : Q.t -> bool
val floor : Q.t -> Q.t
val ceil : Q.t -> Q.t
(* Expression manipulation *)
val comp_neg : string -> string
val mk_int : string -> Expr.t
val mk_rat : string -> Expr.t
val mk_real : string -> Expr.t
val is_num_string : string -> bool
val is_int : Expr.expr -> bool
val is_rat : Expr.expr -> bool
val is_real : Expr.expr -> bool
val is_num : Expr.expr -> bool
(* Expression construction *)
val mk_op : string -> Expr.expr -> Expr.expr -> Expr.expr
val mk_ubop : string -> Expr.expr -> Expr.expr
val mk_bop : string -> Expr.expr -> Expr.expr -> Expr.expr
val const : string -> Expr.expr
val sum : Expr.expr -> Expr.expr -> Expr.expr
val diff : Expr.expr -> Expr.expr -> Expr.expr
val uminus : Expr.expr -> Expr.expr
val mul : Expr.expr -> Expr.expr -> Expr.expr
val minus_one : Expr.expr -> Expr.expr
val plus_one : Expr.expr -> Expr.expr
val less : Expr.expr -> Expr.expr -> Expr.expr
val lesseq : Expr.expr -> Expr.expr -> Expr.expr
val greater : Expr.expr -> Expr.expr -> Expr.expr
val greatereq : Expr.expr -> Expr.expr -> Expr.expr
val arith_eq : Expr.expr -> Expr.expr -> Expr.expr
val coerce : Expr.expr -> Expr.expr -> Expr.expr
(* Formula manipulation *)
val find_coef : Expr.t -> ('a * Expr.t) list -> 'a
val fadd : (Q.t * Expr.t) list -> (Q.t * Expr.t) list -> (Q.t * Expr.t) list
val fdiff : (Q.t * Expr.t) list -> (Q.t * Expr.t) list -> (Q.t * Expr.t) list
val fmul : Q.t -> (Q.t * 'a) list -> (Q.t * 'a) list
val fsep : (Q.t * Expr.t) list -> Expr.t -> Q.t * (Q.t * Expr.t) list
val fis_tau : (Q.t * Expr.t) list -> bool
val fis_meta : (Q.t * Expr.t) list -> bool
val sanitize : (Q.t * 'a) list -> (Q.t * 'a) list
val normalize :
(Q.t * Expr.t) list -> (Q.t * Expr.t) list -> Q.t * (Q.t * Expr.t) list
(* Conversion functions *)
val of_cexpr : Expr.expr -> Q.t
val of_nexpr : Expr.t -> (Q.t * Expr.t) list
val of_bexpr : Expr.expr -> (Q.t * Expr.t) list * string * Q.t
val is_bexpr : Expr.expr -> bool
val is_rexpr : Expr.expr -> bool
val to_nexpr : (Q.t * Expr.expr) list -> Expr.expr
val to_bexpr : (Q.t * Expr.expr) list * string * Q.t -> Expr.expr
val expr_norm : Expr.expr -> Expr.expr
val norm_coef : Expr.expr -> Expr.expr
val coqify : Expr.expr -> Expr.expr
val coqify_term : Expr.expr -> Expr.expr
val coqify_to_q : Expr.expr -> Expr.expr
val coqify_to_r : Expr.expr -> Expr.expr
(* Choice trees *)
type 'a clist
val cl_from_list : 'a list -> 'a clist
val cl_to_list : 'a clist -> 'a list
val cl_current : 'a clist -> 'a
val cl_next : 'a clist -> unit
val cl_reset : 'a clist -> unit
type 'a ctree = {
node : 'a clist;
children : 'a ctree array;
}
val collapse : 'a ctree -> 'a ctree
val reset : 'a ctree -> unit
val next : 'a ctree -> unit
val current : 'a ctree -> 'a list
val ct_all : 'a ctree -> 'a list list
val ct_from_ml : Mlproof.proof -> Expr.t ctree option
val next_inst : Mlproof.proof -> Mlproof.proof
val sctree : Expr.t ctree -> string
(* Simplex solver helper *)
type solution =
| Unsat
| Abstract of (Expr.t * Expr.t) list
val try_solve : Expr.t list -> solution
val solve_tree : Expr.t ctree -> solution