diff options
Diffstat (limited to 'src/constraint.ml')
| -rw-r--r-- | src/constraint.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index 1bd6a437..6c34bc9b 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -179,17 +179,22 @@ let to_smt l vars constr = | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2] | Nexp_sum (nexp1, nexp2) -> sfun "+" [smt_nexp nexp1; smt_nexp nexp2] | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2] - | Nexp_exp (Nexp_aux (Nexp_constant c, _)) when Big_int.greater c Big_int.zero -> - Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c))) - | Nexp_exp nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp] - | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp] + | Nexp_exp nexp -> + begin match nexp_simp nexp with + | Nexp_aux (Nexp_constant c, _) when Big_int.greater_equal c Big_int.zero -> + Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c))) + | nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp] + | nexp -> sfun "^" [Atom "2"; smt_nexp nexp] + end | Nexp_neg nexp -> sfun "-" [smt_nexp nexp] in let rec smt_constraint (NC_aux (aux, l) : n_constraint) : sexpr = match aux with | NC_equal (nexp1, nexp2) -> sfun "=" [smt_nexp nexp1; smt_nexp nexp2] | NC_bounded_le (nexp1, nexp2) -> sfun "<=" [smt_nexp nexp1; smt_nexp nexp2] + | NC_bounded_lt (nexp1, nexp2) -> sfun "<" [smt_nexp nexp1; smt_nexp nexp2] | NC_bounded_ge (nexp1, nexp2) -> sfun ">=" [smt_nexp nexp1; smt_nexp nexp2] + | NC_bounded_gt (nexp1, nexp2) -> sfun ">" [smt_nexp nexp1; smt_nexp nexp2] | NC_not_equal (nexp1, nexp2) -> sfun "not" [sfun "=" [smt_nexp nexp1; smt_nexp nexp2]] | NC_set (v, ints) -> sfun "or" (List.map (fun i -> sfun "=" [smt_var v; Atom (Big_int.to_string i)]) ints) |