From b3ea287bcf8be43714595b6921a0c47d25a67eee Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 16 Nov 2018 16:26:35 +0000 Subject: Various bugfixes and a simple profiling feature for rewrites --- src/constraint.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/constraint.ml') diff --git a/src/constraint.ml b/src/constraint.ml index d66705b6..cf861423 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -219,7 +219,7 @@ let save_digests () = DigestMap.iter output !known_problems; close_out out_chan -let rec call_z3 constraints : smt_result = +let call_z3' constraints : smt_result = let problems = [constraints] in let z3_file = smtlib_of_constraints constraints in @@ -261,6 +261,12 @@ let rec call_z3 constraints : smt_result = else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown) end +let call_z3 constraints = + let t = Profile.start_z3 () in + let result = call_z3' constraints in + Profile.finish_z3 t; + result + let rec solve_z3 constraints var = let problems = [constraints] in let z3_file = smtlib_of_constraints ~get_model:true constraints in -- cgit v1.2.3 From 2c25110ad2f5e636239ba65a2154aae79ffa253c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 7 Dec 2018 21:53:29 +0000 Subject: Working on better flow typing for ASL On a new branch because it's completely broken everything for now --- src/constraint.ml | 229 +++++++++++++++--------------------------------------- 1 file changed, 62 insertions(+), 167 deletions(-) (limited to 'src/constraint.ml') diff --git a/src/constraint.ml b/src/constraint.ml index cf861423..460e8c76 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -49,86 +49,10 @@ (**************************************************************************) module Big_int = Nat_big_num +open Ast +open Ast_util open Util -(* ===== Integer Constraints ===== *) - -type nexp_op = string - -type nexp = - | NFun of (nexp_op * nexp list) - | N2n of nexp - | NConstant of Big_int.num - | NVar of int - -let big_int_op : nexp_op -> (Big_int.num -> Big_int.num -> Big_int.num) option = function - | "+" -> Some Big_int.add - | "-" -> Some Big_int.sub - | "*" -> Some Big_int.mul - | _ -> None - -let rec arith constr = - let constr' = match constr with - | NFun (op, [x; y]) -> NFun (op, [arith x; arith y]) - | N2n c -> N2n (arith c) - | c -> c - in - match constr' with - | NFun (op, [NConstant x; NConstant y]) as c -> - begin - match big_int_op op with - | Some op -> NConstant (op x y) - | None -> c - end - | N2n (NConstant x) -> NConstant (Big_int.pow_int_positive 2 (Big_int.to_int x)) - | c -> c - -(* ===== Boolean Constraints ===== *) - -type constraint_bool_op = And | Or - -type constraint_compare_op = Gt | Lt | GtEq | LtEq | Eq | NEq - -let negate_comparison = function - | Gt -> LtEq - | Lt -> GtEq - | GtEq -> Lt - | LtEq -> Gt - | Eq -> NEq - | NEq -> Eq - -type 'a constraint_bool = - | BFun of (constraint_bool_op * 'a constraint_bool * 'a constraint_bool) - | Not of 'a constraint_bool - | CFun of (constraint_compare_op * 'a * 'a) - | Forall of (int list * 'a constraint_bool) - | Boolean of bool - -let rec pairs (xs : 'a list) (ys : 'a list) : ('a * 'b) list = - match xs with - | [] -> [] - | (x :: xs) -> List.map (fun y -> (x, y)) ys @ pairs xs ys - -(* Get a set of variables from a constraint *) -module IntSet = Set.Make( - struct - let compare = Pervasives.compare - type t = int - end) - -let rec nexp_vars : nexp -> IntSet.t = function - | NConstant _ -> IntSet.empty - | NVar v -> IntSet.singleton v - | NFun (_, xs) -> List.fold_left IntSet.union IntSet.empty (List.map nexp_vars xs) - | N2n x -> nexp_vars x - -let rec constraint_vars : nexp constraint_bool -> IntSet.t = function - | BFun (_, x, y) -> IntSet.union (constraint_vars x) (constraint_vars y) - | Not x -> constraint_vars x - | CFun (_, x, y) -> IntSet.union (nexp_vars x) (nexp_vars y) - | Forall (vars, x) -> IntSet.diff (constraint_vars x) (IntSet.of_list vars) - | Boolean _ -> IntSet.empty - (* SMTLIB v2.0 format is based on S-expressions so we have a lightweight representation of those here. *) type sexpr = List of (sexpr list) | Atom of string @@ -139,47 +63,67 @@ let rec pp_sexpr : sexpr -> string = function | List xs -> "(" ^ string_of_list " " pp_sexpr xs ^ ")" | Atom x -> x -let var_decs constr = - constraint_vars constr - |> IntSet.elements - |> List.map (fun var -> sfun "declare-const" [Atom ("v" ^ string_of_int var); Atom "Int"]) - |> string_of_list "\n" pp_sexpr +let zencode_kid kid = Util.zencode_string (string_of_kid kid) -let cop_sexpr op x y = - match op with - | Gt -> sfun ">" [x; y] - | Lt -> sfun "<" [x; y] - | GtEq -> sfun ">=" [x; y] - | LtEq -> sfun "<=" [x; y] - | Eq -> sfun "=" [x; y] - | NEq -> sfun "not" [sfun "=" [x; y]] +(** Each non-Type/Order kind in Sail mapes to a type in the SMT solver *) +let smt_type l = function + | K_int -> Atom "Int" + | K_bool -> Atom "Bool" + | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kinded variable to SMT solver") -let rec sexpr_of_nexp = function - | NFun (op, xs) -> sfun op (List.map sexpr_of_nexp xs) - | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x] - | NConstant c -> Atom (Big_int.to_string c) (* CHECK: do we do negative constants right? *) - | NVar var -> Atom ("v" ^ string_of_int var) +let smt_var v = Atom ("v" ^ zencode_kid v) -let rec sexpr_of_constraint = function - | BFun (And, x, y) -> sfun "and" [sexpr_of_constraint x; sexpr_of_constraint y] - | BFun (Or, x, y) -> sfun "or" [sexpr_of_constraint x; sexpr_of_constraint y] - | Not x -> sfun "not" [sexpr_of_constraint x] - | CFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp (arith x)) (sexpr_of_nexp (arith y)) - | Forall (vars, x) -> - sfun "forall" [List (List.map (fun v -> List [Atom ("v" ^ string_of_int v); Atom "Int"]) vars); sexpr_of_constraint x] - | Boolean true -> Atom "true" - | Boolean false -> Atom "false" +(** var_decs outputs the list of variables to be used by the SMT + solver in SMTLIB v2.0 format. It takes a kind_aux KBindings, as + returned by Type_check.get_typ_vars *) +let var_decs l (vars : kind_aux KBindings.t) : string = vars + |> KBindings.bindings + |> List.map (fun (v, k) -> sfun "declare-const" [smt_var v; smt_type l k]) + |> string_of_list "\n" pp_sexpr -let smtlib_of_constraints ?get_model:(get_model=false) constr : string = +let rec smt_nexp (Nexp_aux (aux, l) : nexp) : sexpr = + match aux with + | Nexp_id id -> Atom (Util.zencode_string (string_of_id id)) + | Nexp_var v -> smt_var v + | Nexp_constant c -> Atom (Big_int.to_string c) + | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps) + | 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 -> sfun "^" [Atom "2"; smt_nexp nexp] + | Nexp_neg nexp -> sfun "-" [smt_nexp nexp] + +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_ge (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) + | NC_or (nc1, nc2) -> sfun "or" [smt_constraint nc1; smt_constraint nc2] + | NC_and (nc1, nc2) -> sfun "and" [smt_constraint nc1; smt_constraint nc2] + | NC_app (id, args) -> + sfun (string_of_id id) (List.map smt_typ_arg args) + | NC_true -> Atom "true" + | NC_false -> Atom "false" + | NC_var v -> smt_var v + +and smt_typ_arg (Typ_arg_aux (aux, l) : typ_arg) : sexpr = + match aux with + | Typ_arg_nexp nexp -> smt_nexp nexp + | Typ_arg_bool nc -> smt_constraint nc + | _ -> + raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") + +let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string = "(push)\n" - ^ var_decs constr ^ "\n" - ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; sexpr_of_constraint constr]) + ^ var_decs l vars ^ "\n" + ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; smt_constraint constr]) ^ "\n(assert constraint)\n(check-sat)" ^ (if get_model then "\n(get-model)" else "") ^ "\n(pop)" -type t = nexp constraint_bool - type smt_result = Unknown | Sat | Unsat module DigestMap = Map.Make(Digest) @@ -219,9 +163,9 @@ let save_digests () = DigestMap.iter output !known_problems; close_out out_chan -let call_z3' constraints : smt_result = +let call_z3' l vars constraints : smt_result = let problems = [constraints] in - let z3_file = smtlib_of_constraints constraints in + let z3_file = smtlib_of_constraints l vars constraints in (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) @@ -261,15 +205,15 @@ let call_z3' constraints : smt_result = else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown) end -let call_z3 constraints = +let call_z3 l vars constraints = let t = Profile.start_z3 () in - let result = call_z3' constraints in + let result = call_z3' l vars constraints in Profile.finish_z3 t; result -let rec solve_z3 constraints var = +let rec solve_z3 l vars constraints var = let problems = [constraints] in - let z3_file = smtlib_of_constraints ~get_model:true constraints in + let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) @@ -289,62 +233,13 @@ let rec solve_z3 constraints var = let z3_output = String.concat " " (input_all z3_chan) in let _ = Unix.close_process_in z3_chan in Sys.remove input_file; - let regexp = {|(define-fun v|} ^ string_of_int var ^ {| () Int[ ]+\([0-9]+\))|} in + let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in try let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in let result = Big_int.of_string (Str.matched_group 1 z3_output) in - begin match call_z3 (BFun (And, constraints, CFun (NEq, NConstant result, NVar var))) with + begin match call_z3 l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with | Unsat -> Some result | _ -> None end with Not_found -> None - -let string_of constr = smtlib_of_constraints constr - -(* ===== Abstract API for building constraints ===== *) - -(* These functions are exported from constraint.mli, and ensure that - the internal representation of constraints remains opaque. *) - -let implies (x : t) (y : t) : t = - BFun (Or, Not x, y) - -let conj (x : t) (y : t) : t = - BFun (And, x, y) - -let disj (x : t) (y : t) : t = - BFun (Or, x, y) - -let forall (vars : int list) (x : t) : t = - if vars = [] then x else Forall (vars, x) - -let negate (x : t) : t = Not x - -let literal (b : bool) : t = Boolean b - -let lt x y : t = CFun (Lt, x, y) - -let lteq x y : t = CFun (LtEq, x, y) - -let gt x y : t = CFun (Gt, x, y) - -let gteq x y : t = CFun (GtEq, x, y) - -let eq x y : t = CFun (Eq, x, y) - -let neq x y : t = CFun (NEq, x, y) - -let pow2 x : nexp = N2n x - -let add x y : nexp = NFun ("+", [x; y]) - -let sub x y : nexp = NFun ("-", [x; y]) - -let mult x y : nexp = NFun ("*", [x; y]) - -let app f xs : nexp = NFun (f, xs) - -let constant (x : Big_int.num) : nexp = NConstant x - -let variable (v : int) : nexp = NVar v -- cgit v1.2.3 From d8f0854ca9d80d3af8d6a4aaec778643eda9421c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 8 Dec 2018 01:06:28 +0000 Subject: Compiling again Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of uvar as the result of unify. Plus A_ could either stand for argument, or Any/A type which is quite appropriate in most use cases. Restore instantiation info in infer_funapp'. Ideally we would save this instead of recomputing it ever time we need it. However I checked and there are over 300 places in the code that would need to be changed to add an extra argument to E_app. Still some issues causing specialisation to fail however. Improve the error message when we swap how we infer/check an l-expression, as this could previously cause the actual cause of a type-checking failure to be effectively hidden. --- src/constraint.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/constraint.ml') diff --git a/src/constraint.ml b/src/constraint.ml index 460e8c76..f512eb8a 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -109,10 +109,10 @@ let rec smt_constraint (NC_aux (aux, l) : n_constraint) : sexpr = | NC_false -> Atom "false" | NC_var v -> smt_var v -and smt_typ_arg (Typ_arg_aux (aux, l) : typ_arg) : sexpr = +and smt_typ_arg (A_aux (aux, l) : typ_arg) : sexpr = match aux with - | Typ_arg_nexp nexp -> smt_nexp nexp - | Typ_arg_bool nc -> smt_constraint nc + | A_nexp nexp -> smt_nexp nexp + | A_bool nc -> smt_constraint nc | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") -- cgit v1.2.3 From ab4b9ca4f7cab45b6a2a13d0ef125dcf9c276a06 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 11 Dec 2018 19:54:14 +0000 Subject: Fix all tests with type checking changes --- src/constraint.ml | 112 +++++++++++++++++++++++++++++++----------------------- 1 file changed, 64 insertions(+), 48 deletions(-) (limited to 'src/constraint.ml') diff --git a/src/constraint.ml b/src/constraint.ml index f512eb8a..a16b8c73 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -63,63 +63,79 @@ let rec pp_sexpr : sexpr -> string = function | List xs -> "(" ^ string_of_list " " pp_sexpr xs ^ ")" | Atom x -> x -let zencode_kid kid = Util.zencode_string (string_of_kid kid) - (** Each non-Type/Order kind in Sail mapes to a type in the SMT solver *) let smt_type l = function | K_int -> Atom "Int" | K_bool -> Atom "Bool" | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kinded variable to SMT solver") -let smt_var v = Atom ("v" ^ zencode_kid v) - -(** var_decs outputs the list of variables to be used by the SMT - solver in SMTLIB v2.0 format. It takes a kind_aux KBindings, as - returned by Type_check.get_typ_vars *) -let var_decs l (vars : kind_aux KBindings.t) : string = vars - |> KBindings.bindings - |> List.map (fun (v, k) -> sfun "declare-const" [smt_var v; smt_type l k]) - |> string_of_list "\n" pp_sexpr - -let rec smt_nexp (Nexp_aux (aux, l) : nexp) : sexpr = - match aux with - | Nexp_id id -> Atom (Util.zencode_string (string_of_id id)) - | Nexp_var v -> smt_var v - | Nexp_constant c -> Atom (Big_int.to_string c) - | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps) - | 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 -> sfun "^" [Atom "2"; smt_nexp nexp] - | Nexp_neg nexp -> sfun "-" [smt_nexp nexp] - -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_ge (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) - | NC_or (nc1, nc2) -> sfun "or" [smt_constraint nc1; smt_constraint nc2] - | NC_and (nc1, nc2) -> sfun "and" [smt_constraint nc1; smt_constraint nc2] - | NC_app (id, args) -> - sfun (string_of_id id) (List.map smt_typ_arg args) - | NC_true -> Atom "true" - | NC_false -> Atom "false" - | NC_var v -> smt_var v - -and smt_typ_arg (A_aux (aux, l) : typ_arg) : sexpr = - match aux with - | A_nexp nexp -> smt_nexp nexp - | A_bool nc -> smt_constraint nc - | _ -> - raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") +let to_smt l vars constr = + (* Numbering all SMT variables v0, ... vn, rather than generating + names based on their Sail names (e.g. using zencode) ensures that + alpha-equivalent constraints generate the same SMT problem, which + is important for the SMT memoisation to work properly. *) + let var_map = ref KBindings.empty in + let vnum = ref (-1) in + let smt_var v = + match KBindings.find_opt v !var_map with + | Some n -> Atom ("v" ^ string_of_int n) + | None -> + let n = !vnum + 1 in + var_map := KBindings.add v n !var_map; + vnum := n; + Atom ("v" ^ string_of_int n) + in + + (* var_decs outputs the list of variables to be used by the SMT + solver in SMTLIB v2.0 format. It takes a kind_aux KBindings, as + returned by Type_check.get_typ_vars *) + let var_decs l (vars : kind_aux KBindings.t) : string = + vars + |> KBindings.bindings + |> List.map (fun (v, k) -> sfun "declare-const" [smt_var v; smt_type l k]) + |> string_of_list "\n" pp_sexpr + in + let rec smt_nexp (Nexp_aux (aux, l) : nexp) : sexpr = + match aux with + | Nexp_id id -> Atom (Util.zencode_string (string_of_id id)) + | Nexp_var v -> smt_var v + | Nexp_constant c -> Atom (Big_int.to_string c) + | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps) + | 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 -> sfun "^" [Atom "2"; smt_nexp nexp] + | 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_ge (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) + | NC_or (nc1, nc2) -> sfun "or" [smt_constraint nc1; smt_constraint nc2] + | NC_and (nc1, nc2) -> sfun "and" [smt_constraint nc1; smt_constraint nc2] + | NC_app (id, args) -> + sfun (string_of_id id) (List.map smt_typ_arg args) + | NC_true -> Atom "true" + | NC_false -> Atom "false" + | NC_var v -> smt_var v + and smt_typ_arg (A_aux (aux, l) : typ_arg) : sexpr = + match aux with + | A_nexp nexp -> smt_nexp nexp + | A_bool nc -> smt_constraint nc + | _ -> + raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") + in + var_decs l vars, smt_constraint constr let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string = + let variables, problem = to_smt l vars constr in "(push)\n" - ^ var_decs l vars ^ "\n" - ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; smt_constraint constr]) + ^ variables ^ "\n" + ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem]) ^ "\n(assert constraint)\n(check-sat)" ^ (if get_model then "\n(get-model)" else "") ^ "\n(pop)" -- cgit v1.2.3 From b9a051d186593fdd3bbf295e20f7ace78e668580 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Dec 2018 22:37:04 +0000 Subject: Fix some small bugs Now all ARM, RISC-V, and CHERI-MIPS all build successfully with type-checking changes. All typechecker/c/ocaml/lem/builtin/riscv/arm tests are now working as well. Now the python test scripts can run sequentially with TEST_PAR=1 there's no reason to keep the old shell versions around anymore. --- src/constraint.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/constraint.ml') diff --git a/src/constraint.ml b/src/constraint.ml index a16b8c73..7ead0cc8 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -104,6 +104,8 @@ 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 -> sfun "^" [Atom "2"; smt_nexp nexp] | Nexp_neg nexp -> sfun "-" [smt_nexp nexp] in @@ -228,7 +230,6 @@ let call_z3 l vars constraints = result let rec solve_z3 l vars constraints var = - let problems = [constraints] in let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) -- cgit v1.2.3