diff options
| author | Alasdair Armstrong | 2019-07-16 18:57:46 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-07-16 18:57:46 +0100 |
| commit | cd909e15b97739b10214023af04b2fbbb4d20cf7 (patch) | |
| tree | 9a418c7cafa915c29e93242848a1411cbd8b8f7c /src/constraint.ml | |
| parent | 6d3a6edcd616621eb40420cfb16a34762a32c5c1 (diff) | |
| parent | 170543faa031d90186e6b45612ed8374f1c25f7b (diff) | |
Merge remote-tracking branch 'origin/sail2' into separate_bv
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) |