diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 3 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index b9e03987..1bce4ce5 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -251,7 +251,8 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown) let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown) let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown) -let nc_set kid ints = mk_nc (NC_set (kid, ints)) +let nc_set kid nums = mk_nc (NC_set (kid, nums)) +let nc_int_set kid ints = mk_nc (NC_set (kid, List.map big_int_of_int ints)) let nc_eq n1 n2 = mk_nc (NC_equal (n1, n2)) let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2)) let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown) diff --git a/src/ast_util.mli b/src/ast_util.mli index 66d87c71..8206637c 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -133,6 +133,7 @@ val nc_or : n_constraint -> n_constraint -> n_constraint val nc_true : n_constraint val nc_false : n_constraint val nc_set : kid -> big_int list -> n_constraint +val nc_int_set : kid -> int list -> n_constraint (* Negate a n_constraint. Note that there's no NC_not constructor, so this flips all the inequalites a the n_constraint leaves and uses |