summaryrefslogtreecommitdiff
path: root/src/ast_util.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/ast_util.mli')
-rw-r--r--src/ast_util.mli6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 1cd621b4..f55cdf16 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -138,6 +138,12 @@ val no_effect : effect
val mk_effect : base_effect_aux list -> effect
val nexp_simp : nexp -> nexp
+val constraint_simp : n_constraint -> n_constraint
+
+(* If a constraint is a conjunction, return a list of all the top-level conjuncts *)
+val constraint_conj : n_constraint -> n_constraint list
+(* Same as constraint_conj but for disjunctions *)
+val constraint_disj : n_constraint -> n_constraint list
(* Utilities for building n-expressions *)
val nconstant : Big_int.num -> nexp