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*)