Use multiple solvers

Useful to see what constraints we are generating that are particularly
hard, and which of our specs work with different solvers.

Refactor code to use smt in names rather than specifically z3

7 files changed, 154 insertions, 71 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index a1050972..2981660e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -110,7 +110,7 @@ type ctx =
     letbinds : int list;
     recursive_functions : IdSet.t;
     no_raw : bool;
-    optimize_z3 : bool;
+    optimize_smt : bool;
   }
 
 let initial_ctx env =
@@ -123,13 +123,13 @@ let initial_ctx env =
     letbinds = [];
     recursive_functions = IdSet.empty;
     no_raw = false;
-    optimize_z3 = true;
+    optimize_smt = true;
   }
 
 (** Convert a sail type into a C-type. This function can be quite
-   slow, because it uses ctx.local_env and Z3 to analyse the Sail
+   slow, because it uses ctx.local_env and SMT to analyse the Sail
    types and attempts to fit them into the smallest possible C
-   types, provided ctx.optimize_z3 is true (default) **)
+   types, provided ctx.optimize_smt is true (default) **)
 let rec ctyp_of_typ ctx typ =
   let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
   match typ_aux with
@@ -151,7 +151,7 @@ let rec ctyp_of_typ ctx typ =
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
              when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
            CT_int64
-        | n, m when ctx.optimize_z3 ->
+        | n, m when ctx.optimize_smt ->
            if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
              CT_int64
            else
@@ -173,7 +173,7 @@ let rec ctyp_of_typ ctx typ =
      let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
      begin match nexp_simp n with
      | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
-     | n when ctx.optimize_z3 && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
+     | n when ctx.optimize_smt && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
      | _ -> CT_lbits direction
      end
 
@@ -193,8 +193,8 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs)
 
-  | Typ_exist _ when ctx.optimize_z3 ->
-     (* Use Type_check.destruct_exist when optimising with z3, to
+  | Typ_exist _ when ctx.optimize_smt ->
+     (* Use Type_check.destruct_exist when optimising with SMT, to
         ensure that we don't cause any type variable clashes in
         local_env, and that we can optimize the existential based upon
         it's constraints. *)
diff --git a/src/constraint.ml b/src/constraint.ml
index b7fa50c3..09091655 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -55,6 +55,76 @@ open Util
 
 let opt_smt_verbose = ref false
 
+type solver = {
+    command : string;
+    header : string;
+    footer : string;
+    negative_literals : bool;
+    uninterpret_power : bool
+  }
+
+let cvc4_solver = {
+    command = "cvc4 -L smtlib2 --tlimit=2000";
+    header = "(set-logic QF_UFNIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let mathsat_solver = {
+    command = "mathsat";
+    header = "(set-logic QF_UFLIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let z3_solver = {
+    command = "z3 -t:1000 -T:10";
+    (* Using push and pop is much faster, I believe because
+       incremental mode uses a different solver. *)
+    header = "(push)\n";
+    footer = "(pop)\n";
+    negative_literals = true;
+    uninterpret_power = false;
+  }
+
+let yices_solver = {
+    command = "yices-smt2 --timeout=2";
+    header = "(set-logic QF_UFLIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let vampire_solver = {
+    (* vampire sometimes likes to ignore its time limit *)
+    command = "timeout -s SIGKILL 3s vampire --time_limit 2s --input_syntax smtlib2 --mode smtcomp";
+    header = "";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let alt_ergo_solver ={
+    command = "alt-ergo";
+    header = "";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let opt_solver = ref z3_solver
+
+let set_solver = function
+  | "z3" -> opt_solver := z3_solver
+  | "alt-ergo" -> opt_solver := alt_ergo_solver
+  | "cvc4" -> opt_solver := cvc4_solver
+  | "mathsat" -> opt_solver := mathsat_solver
+  | "vampire" -> opt_solver := vampire_solver
+  | "yices" -> opt_solver := yices_solver
+  | unknown -> prerr_endline ("Unrecognised SMT solver " ^ unknown)
+
 (* 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
@@ -101,6 +171,9 @@ let to_smt l vars constr =
     match aux with
     | Nexp_id id -> Atom (Util.zencode_string (string_of_id id))
     | Nexp_var v -> smt_var v
+    | Nexp_constant c
+         when Big_int.less_equal c (Big_int.of_int (-1)) && not !opt_solver.negative_literals ->
+       sfun "-" [Atom "0"; Atom (Big_int.to_string (Big_int.abs c))]
     | 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]
@@ -108,6 +181,7 @@ let to_smt l vars constr =
     | 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_neg nexp -> sfun "-" [smt_nexp nexp]
   in
@@ -137,12 +211,13 @@ let to_smt l vars constr =
 
 let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) =
   let variables, problem, var_map = to_smt l vars constr in
-  "(push)\n"
+  !opt_solver.header
   ^ variables ^ "\n"
+  ^ (if !opt_solver.uninterpret_power then "(declare-fun sailexp (Int) Int)\n" else "")
   ^ 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)",
+  ^ (if get_model then "\n(get-model)\n" else "\n")
+  ^ !opt_solver.footer,
   var_map
 
 type smt_result = Unknown | Sat | Unsat
@@ -184,12 +259,12 @@ let save_digests () =
   DigestMap.iter output !known_problems;
   close_out out_chan
 
-let call_z3' l vars constraints : smt_result =
+let call_smt' l vars constraints : smt_result =
   let problems = [constraints] in
-  let z3_file, _ = smtlib_of_constraints l vars constraints in
+  let smt_file, _ = smtlib_of_constraints l vars constraints in
 
   if !opt_smt_verbose then
-    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file)
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file)
   else ();
 
   let rec input_lines chan = function
@@ -202,7 +277,7 @@ let call_z3' l vars constraints : smt_result =
        end
   in
 
-  let digest = Digest.string z3_file in
+  let digest = Digest.string smt_file in
   try
     let result = DigestMap.find digest !known_problems in
     result
@@ -210,45 +285,48 @@ let call_z3' l vars constraints : smt_result =
   | Not_found ->
     begin
       let (input_file, tmp_chan) =
-        try Filename.open_temp_file "constraint_" ".sat" with
-        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling Z3: " ^ msg))
+        try Filename.open_temp_file "constraint_" ".smt2" with
+        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling SMT: " ^ msg))
       in
-      output_string tmp_chan z3_file;
+      output_string tmp_chan smt_file;
       close_out tmp_chan;
-      let z3_output =
+      let smt_output =
         try
-          let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-          let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
-          let _ = Unix.close_process_in z3_chan in
-          z3_output
+          let smt_out, smt_in, smt_err = Unix.open_process_full (!opt_solver.command ^ " " ^ input_file) (Unix.environment ()) in
+          let smt_output =
+            try List.combine problems (input_lines smt_out (List.length problems)) with
+            | End_of_file -> List.combine problems ["unknown"]
+          in
+          let _ = Unix.close_process_full (smt_out, smt_in, smt_err) in
+          smt_output
         with
-        | exn -> raise (Reporting.err_general l ("Error when calling z3: " ^ Printexc.to_string exn))
+        | exn -> raise (Reporting.err_general l ("Error when calling smt: " ^ Printexc.to_string exn))
       in
       Sys.remove input_file;
       try
-        let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
+        let (problem, _) = List.find (fun (_, result) -> result = "unsat") smt_output in
         known_problems := DigestMap.add digest Unsat !known_problems;
         Unsat
       with
       | Not_found ->
-         let unsolved = List.filter (fun (_, result) -> result = "unknown") z3_output in
+         let unsolved = List.filter (fun (_, result) -> result = "unknown") smt_output in
          if unsolved == []
          then (known_problems := DigestMap.add digest Sat !known_problems; Sat)
          else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
     end
 
-let call_z3 l vars constraints =
-  let t = Profile.start_z3 () in
-  let result = call_z3' l vars constraints in
-  Profile.finish_z3 t;
+let call_smt l vars constraints =
+  let t = Profile.start_smt () in
+  let result = call_smt' l vars constraints in
+  Profile.finish_smt t;
   result
 
-let rec solve_z3 l vars constraints var =
-  let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
-  let z3_var = pp_sexpr (smt_var var) in
+let rec solve_smt l vars constraints var =
+  let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
+  let smt_var = pp_sexpr (smt_var var) in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file);
-     prerr_endline ("Solving for " ^ z3_var); *)
+  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file);
+     prerr_endline ("Solving for " ^ smt_var); *)
 
   let rec input_all chan =
     try
@@ -259,25 +337,25 @@ let rec solve_z3 l vars constraints var =
       End_of_file -> []
   in
 
-  let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
-  output_string tmp_chan z3_file;
+  let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".smt2" in
+  output_string tmp_chan smt_file;
   close_out tmp_chan;
-  let z3_output =
+  let smt_output =
     try
-      let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-      let z3_output = String.concat " " (input_all z3_chan) in
-      let _ = Unix.close_process_in z3_chan in
-      z3_output
+      let smt_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+      let smt_output = String.concat " " (input_all smt_chan) in
+      let _ = Unix.close_process_in smt_chan in
+      smt_output
     with
     | exn ->
-       raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn))
+       raise (Reporting.err_general l ("Got error when calling smt: " ^ Printexc.to_string exn))
   in
   Sys.remove input_file;
-  let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in
+  let regexp = {|(define-fun |} ^ smt_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 l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
+    let _ = Str.search_forward (Str.regexp regexp) smt_output 0 in
+    let result = Big_int.of_string (Str.matched_group 1 smt_output) in
+    begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
     | Unsat -> Some result
     | _ -> None
     end
diff --git a/src/constraint.mli b/src/constraint.mli
index fa318c35..e86c764a 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -54,11 +54,13 @@ open Ast_util
 
 val opt_smt_verbose : bool ref
 
+val set_solver : string -> unit
+
 type smt_result = Unknown | Sat | Unsat
 
 val load_digests : unit -> unit
 val save_digests : unit -> unit
 
-val call_z3 : l -> kind_aux KBindings.t -> n_constraint -> smt_result
+val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result
 
-val solve_z3 : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
+val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
diff --git a/src/profile.ml b/src/profile.ml
index 1a8bd30b..f64bdfe0 100644
--- a/src/profile.ml
+++ b/src/profile.ml
@@ -51,13 +51,13 @@
 let opt_profile = ref false
 
 type profile = {
-    z3_calls : int;
-    z3_time : float
+    smt_calls : int;
+    smt_time : float
   }
 
 let new_profile = {
-    z3_calls = 0;
-    z3_time = 0.0
+    smt_calls = 0;
+    smt_time = 0.0
   }
 
 let profile_stack = ref []
@@ -68,12 +68,12 @@ let update_profile f =
   | (p :: ps) ->
      profile_stack := f p :: ps
 
-let start_z3 () =
-  update_profile (fun p -> { p with z3_calls = p.z3_calls + 1 });
+let start_smt () =
+  update_profile (fun p -> { p with smt_calls = p.smt_calls + 1 });
   Sys.time ()
 
-let finish_z3 t =
-  update_profile (fun p -> { p with z3_time = p.z3_time +. (Sys.time () -. t) })
+let finish_smt t =
+  update_profile (fun p -> { p with smt_time = p.smt_time +. (Sys.time () -. t) })
 
 let start () =
   profile_stack := new_profile :: !profile_stack;
@@ -84,7 +84,7 @@ let finish msg t =
     begin match !profile_stack with
     | p :: ps ->
        prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profiled" |> magenta |> clear) msg (Sys.time () -. t));
-       prerr_endline (Printf.sprintf "  Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time);
+       prerr_endline (Printf.sprintf "  SMT calls: %d, SMT time: %fs" p.smt_calls p.smt_time);
        profile_stack := ps
     | [] -> ()
     end
diff --git a/src/sail.ml b/src/sail.ml
index 28c5db0a..9cf87af8 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -64,7 +64,7 @@ let opt_print_c = ref false
 let opt_print_latex = ref false
 let opt_print_coq = ref false
 let opt_print_cgen = ref false
-let opt_memo_z3 = ref true
+let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
 let opt_libs_lem = ref ([]:string list)
@@ -112,6 +112,9 @@ let options = Arg.align ([
   ( "-ocaml_generators",
     Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
     "<types> produce random generators for the given types");
+  ( "-smt_solver",
+    Arg.String (fun s -> Constraint.set_solver (String.trim s)),
+    "<solver> choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices.");
   ( "-latex",
     Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
     " pretty print the input to LaTeX");
@@ -208,7 +211,7 @@ let options = Arg.align ([
     " memoize calls to z3, improving performance when typechecking repeatedly (default)");
   ( "-no_memo_z3",
     Arg.Clear opt_memo_z3,
-    " do not memoize calls to z3");
+    " do not memoize calls to z3 (default)");
   ( "-memo",
     Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache],
     " memoize calls to z3, and intermediate compilation results");
@@ -268,7 +271,7 @@ let options = Arg.align ([
     "<verbosity> (debug) verbose typechecker output: 0 is silent");
   ( "-dsmt_verbose",
     Arg.Set Constraint.opt_smt_verbose,
-    " (debug) print SMTLIB constraints sent to Z3");
+    " (debug) print SMTLIB constraints sent to SMT solver");
   ( "-dno_cast",
     Arg.Set opt_dno_cast,
     " (debug) typecheck without any implicit casting");
diff --git a/src/type_check.ml b/src/type_check.ml
index 37f2cee7..65e13a19 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -401,7 +401,7 @@ module Env : sig
   val wf_nexp : ?exs:KidSet.t -> t -> nexp -> unit
   val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit
 
-  (* Some of the code in the environment needs to use the Z3 prover,
+  (* Some of the code in the environment needs to use the smt solver,
      which is defined below. To break the circularity this would cause
      (as the prove code depends on the environment), we add a
      reference to the prover to the initial environment. *)
@@ -1299,7 +1299,7 @@ and simp_typ_aux = function
      would become {('s:Bool) ('r: Bool), nc('r). bool('s & 'r)},
      wherein all the redundant boolean variables have been combined
      into a single one. Making this simplification allows us to avoid
-     having to pass large numbers of pointless variables to Z3 if we
+     having to pass large numbers of pointless variables to SMT if we
      ever bind this existential. *)
   | Typ_exist (vars, nc, Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool b, _)]), _)) ->
      let kids = KidSet.of_list (List.map kopt_kid vars) in
@@ -1385,11 +1385,11 @@ let rec nexp_variable_power (Nexp_aux (aux, _)) =
 let constraint_variable_power nc =
   List.exists nexp_variable_power (constraint_nexps nc)
 
-let prove_z3 env (NC_aux (_, l) as nc) =
+let prove_smt env (NC_aux (_, l) as nc) =
   let vars = Env.get_typ_vars env in
   let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
   let ncs = Env.get_constraints env in
-  match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs) with
+  match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs) with
   | Constraint.Unsat -> typ_debug (lazy "unsat"); true
   | Constraint.Sat -> typ_debug (lazy "sat"); false
   | Constraint.Unknown ->
@@ -1397,7 +1397,7 @@ let prove_z3 env (NC_aux (_, l) as nc) =
         constraints, even when such constraints are irrelevant *)
      let ncs' = List.concat (List.map constraint_conj ncs) in
      let ncs' = List.filter (fun nc -> not (constraint_variable_power nc)) ncs' in
-     match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs') with
+     match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs') with
      | Constraint.Unsat -> typ_debug (lazy "unsat"); true
      | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false
 
@@ -1411,7 +1411,7 @@ let solve env (Nexp_aux (_, l) as nexp) =
     let vars = Env.get_typ_vars env in
     let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
     let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
-    Constraint.solve_z3 l vars constr (mk_kid "solve#")
+    Constraint.solve_smt l vars constr (mk_kid "solve#")
 
 let debug_pos (file, line, _, _) =
   "(" ^ file ^ "/" ^ string_of_int line ^ ") "
@@ -1424,7 +1424,7 @@ let prove pos env nc =
   else ();
   match nc_aux with
   | NC_true -> true
-  | _ -> prove_z3 env nc
+  | _ -> prove_smt env nc
 
 (**************************************************************************)
 (* 3. Unification                                                         *)
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index ad2592df..e5650646 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -50,9 +50,9 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 
 for i in `ls $DIR/pass/ | grep sail`;
 do
-    if $SAILDIR/sail -just_check -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
+    if $SAILDIR/sail -no_memo_z3 -just_check -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
     then
-	if $SAILDIR/sail -just_check -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i;
+	if $SAILDIR/sail -no_memo_z3 -just_check -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i;
 	then
 	    if diff $DIR/rtpass/$i $DIR/rtpass2/$i;
 	    then
@@ -71,7 +71,7 @@ do
     for file in $DIR/pass/${i%.sail}/*.sail;
     do
 	pushd $DIR/pass > /dev/null;
-	if $SAILDIR/sail ${i%.sail}/$(basename $file) 2> result;
+	if $SAILDIR/sail -no_memo_z3 ${i%.sail}/$(basename $file) 2> result;
 	then
 	    red "failing variant of $i $(basename $file) passed" "fail"
 	else