blob: e6ab14ba2413965060cd391fda3dd53aa26d430b (
plain)
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
|
val compare_nexps : nexp -> nexp -> int
(*usefull for sorting nexps*)
val contains_const : nexp -> bool
(*Does the given nexp recursively conain a constant*)
val get_var : nexp -> nexp option
(*extracts variable in a normalized nexp*)
val get_all_nvar : nexp -> string list
(*Gets a list (with duplicates) of all variables used in an nexp*)
val get_factor : nexp -> nexp
(*extracts a variables factor in a normalized nexp*)
val increment_factor : nexp -> nexp -> nexp
(*first nexp is multiplied by second, increased by one, expects normalized nexps*)
val negate : nexp -> nexp
(*negate normalized nexp into normalized form*)
val normalize_nexp : nexp -> nexp
(*convert nexp into a normal form*)
val nexp_eq_check : nexp -> nexp -> bool
(*structural equality*)
val nexp_gt : nexp -> nexp -> triple
(*greater than check, normalizes first, might not know*)
val nexp_ge : nexp -> nexp -> triple
(*greather than eq check, normalizes first, might not know*)
val nexp_eq : nexp -> nexp -> bool
(*wrapper on above that normalizes first*)
val nexp_one_more_then : nexp -> nexp -> bool
(*nexp_one_more_then n1 n2 checks if n1 is n2 + -1, n2 - 1*)
val contains_nuvar_nexp : nexp -> nexp -> bool
(*contains_nuvar n1 n2: n1 expected to be a nuvar (otherwise always false) otherwise says if n1 occurs in n2*)
val contains_nuvar : nexp -> constraints -> constraints
(*produces a list of all constraints that contain nexp, assumed to be a nuvar*)
val n_subst : s_env -> nexp -> nexp
(*replaces nvars*)
val contains_var : nexp -> nexp -> bool
(*expects nexp1 to be nvar or nuvar otherwise like contains_nuvar_nexp*)
val subst_nuvar : nexp -> nexp ->nexp
(*replace occurence of n1 (an nuvar) with n2 in n3*)
val subst_nuvars : (nexp * nexp) list -> nexp -> nexp
(*replace all occurences of the first nuvars in the list with the second nexp in the list in nexp*)
val get_nuvars : nexp -> nexp list
(*pull out all nuvars in an nexp*)
val get_all_nuvars_cs : constraints -> Set.Make(NexpM).t
(*pull out all the nuvars in a constraint set*)
val equate_nuvars : 'a -> constraints -> contraints
(*Set equal nuvars to each other in the constraint list... first parameter presently unused and has forgotten intent*)
|
