1 files changed, 67 insertions, 0 deletions
diff --git a/src/nexp_functions b/src/nexp_functions
new file mode 100644
index 00000000..e6ab14ba
--- /dev/null
+++ b/src/nexp_functions
@@ -0,0 +1,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*)
+