Make SMT solver consider the full set of assumptions, including the o…

…nes leading to undecidability -- as an experiment.

backend/cn/bin/main.ml

@@ -287,6 +287,7 @@ let verify
   no_inherit_loc
   magic_comment_char_dollar
   disable_resource_derived_constraints
+  try_hard
   =
   if json then (
     if debug_level > 0 then
@@ -307,6 +308,7 @@ let verify
   Solver.solver_path := solver_path;
   Solver.solver_type := solver_type;
   Solver.solver_flags := solver_flags;
+  Solver.try_hard := try_hard;
   Check.skip_and_only := (opt_comma_split skip, opt_comma_split only);
   IndexTerms.use_vip := not dont_use_vip;
   Check.fail_fast := fail_fast;
@@ -743,6 +745,11 @@ module Verify_flags = struct
       & info [ "solver-type" ] ~docv:"z3|cvc5" ~doc)
 
 
+  let try_hard =
+    let doc = "Try undecidable SMT solving using full set of assumptions" in
+    Arg.(value & flag & info [ "try_hard" ] ~doc)
+
+
   let only =
     let doc = "only type-check this function (or comma-separated names)" in
     Arg.(value & opt (some string) None & info [ "only" ] ~doc)
@@ -886,6 +893,7 @@ let verify_t : unit Term.t =
   $ Common_flags.no_inherit_loc
   $ Common_flags.magic_comment_char_dollar
   $ Verify_flags.disable_resource_derived_constraints
+  $ Verify_flags.try_hard
 
 
 let verify_cmd =

backend/cn/lib/simple_smt.ml

@@ -381,6 +381,13 @@ let set_subset ext xs ys =
   app_ nm [ xs; ys ]
 
 
+(** {1 Quantifiers} *)
+
+(** A command to construct a universal quantification. *)
+let forall (qs : (sexp * sexp) list) (p : sexp) = 
+  let pair (x, y) = list [x;y] in
+  app_ "forall" [list (List.map pair qs); p]
+
 (** {1 Commands}
     The S-Expressions in this section define commands to the SMT solver.
     These can be sent to solver using {!ack_command}. *)

backend/cn/lib/solver.ml

@@ -1394,51 +1394,121 @@ let model_evaluator, reset_model_evaluator_state =
 
 (* ---------------------------------------------------------------------------*)
 
+module TryHard = struct
+
+  let translate_forall solver qs body = 
+    let rec alpha_rename qs body = 
+      match qs with
+      | [] -> ([],body)
+      | (s, bt) :: qs' ->
+        let qs',body = alpha_rename qs' body in
+        let s, body = IT.alpha_rename s body in
+        (((s, bt) :: qs'), body)
+    in
+    let qs, body = alpha_rename qs body in
+    let body_ = translate_term solver body in
+    let qs_ = 
+      List.map (fun (s, bt) ->
+        let name = CN_Names.var_name s in
+        let sort = translate_base_type bt in
+        (SMT.atom name, sort)
+        ) qs
+    in
+    SMT.forall qs_ body_
+
+  let translate_lc solver = function
+    | LC.T it -> translate_term solver it
+    | LC.Forall ((s, bt), body) -> translate_forall solver [(s, bt)] body
+
+
+  let translate_function solver f args rbt body =
+    let loc = Locations.other __LOC__ in
+    let arg_exprs = List.map (fun (s,bt) -> IT.sym_ (s, bt, loc)) args in
+    translate_forall solver args (eq_ (apply_ f arg_exprs rbt loc, body) loc)
+
+  let translate_functions solver =
+    let open Definition.Function in
+    List.filter_map (fun (f, def) ->
+      match def.body with
+      | Rec_Def body -> 
+          (* Normally this would require the relevant functions,
+             including `f`, to already have been declared. Here this
+             happens lazily (in the `Apply` case), including for `f`. *)
+          Some (translate_function solver f def.args def.return_bt body)
+      | Def _ -> None
+      | Uninterp -> None
+      ) (Sym.Map.bindings solver.globals.logical_functions)
+
+
+  let translate_foralls solver assumptions =
+    List.map (translate_lc solver) (List.filter LC.is_forall assumptions)
+
+end
+
+let try_hard = ref false
+
+
 (** The main way to query the solver. *)
 let provable ~loc ~solver ~global ~assumptions ~simp_ctxt lc =
   let _ = loc in
-  (* ISD: should we use this somehow? *)
-  let s1 = { solver with globals = global } in
-  let rtrue () =
-    model_state := No_model;
-    `True
+  let _ = global in
+  let set_model smt_solver qs =
+    let defs = SMT.get_model smt_solver in
+    let model = model_evaluator solver defs in
+    model_state := Model (model, qs)
   in
   match shortcut simp_ctxt lc with
-  | `True -> rtrue ()
+  | `True -> 
+    model_state := No_model;
+    `True
   | `No_shortcut lc ->
-    let { expr; qs; extra } = translate_goal s1 assumptions lc in
-    let model_from sol =
-      let defs = SMT.get_model sol in
-      let mo = model_evaluator s1 defs in
-      model_state := Model (mo, qs)
-    in
-    let nlc = SMT.bool_not expr in
-    let inc = s1.smt_solver in
-    debug_ack_command s1 (SMT.push 1);
-    debug_ack_command s1 (SMT.assume (SMT.bool_ands (nlc :: extra)));
-    let res = SMT.check inc in
-    (match res with
+    let { expr; qs; extra } = translate_goal solver assumptions lc in
+    let nexpr = SMT.bool_not expr in
+    let inc = solver.smt_solver in
+    debug_ack_command solver (SMT.push 1);
+    debug_ack_command solver (SMT.assume (SMT.bool_ands (nexpr :: extra)));
+    (match SMT.check inc with
      | SMT.Unsat ->
-       debug_ack_command s1 (SMT.pop 1);
-       rtrue ()
+       debug_ack_command solver (SMT.pop 1);
+       model_state := No_model;
+       `True
+     | SMT.Sat when !try_hard ->
+       debug_ack_command solver (SMT.pop 1);
+       let assumptions = LC.Set.to_list assumptions in
+       let foralls = TryHard.translate_foralls solver assumptions in
+       let functions = TryHard.translate_functions solver in
+       debug_ack_command solver (SMT.push 1);
+       debug_ack_command solver (SMT.assume (SMT.bool_ands (nexpr :: foralls @ functions)));
+       Pp.(debug 3 (lazy !^"***** try-hard *****"));
+       (match SMT.check inc with
+        | SMT.Unsat ->
+            debug_ack_command solver (SMT.pop 1);
+            model_state := No_model;
+            Pp.(debug 3 (lazy !^"***** try-hard: provable *****"));
+            `True
+        | SMT.Sat ->
+            set_model inc qs;
+            debug_ack_command solver (SMT.pop 1);
+            Pp.(debug 3 (lazy !^"***** try-hard: unprovable *****"));
+            `False
+        | SMT.Unknown ->
+            set_model inc qs;
+            debug_ack_command solver (SMT.pop 1);
+            Pp.(debug 3 (lazy !^"***** try-hard: unknown *****"));
+            `False)
      | SMT.Sat ->
-       model_from inc;
-       debug_ack_command s1 (SMT.pop 1);
+       set_model inc qs;
+       debug_ack_command solver (SMT.pop 1);
        `False
      | SMT.Unknown ->
-       debug_ack_command s1 (SMT.pop 1);
+       debug_ack_command solver (SMT.pop 1);
        failwith "Unknown")
 
 
-(* let () = Z3.Solver.reset solver.non_incremental in let () = List.iter (fun lc ->
-   Z3.Solver.add solver.non_incremental [lc] ) (nlc :: extra @ existing_scs) in let
-   (elapsed2, res2) = time_f_elapsed (time_f_logs loc 5 "Z3(non-inc)" (Z3.Solver.check
-   solver.non_incremental)) [] in maybe_save_slow_problem (res_short_string res2) loc lc
-   expr smt2_doc elapsed2 solver.non_incremental; match res2 with |
-   Z3.Solver.UNSATISFIABLE -> rtrue () | Z3.Solver.SATISFIABLE -> rfalse qs
-   solver.non_incremental | Z3.Solver.UNKNOWN -> let reason = Z3.Solver.get_reason_unknown
-   solver.non_incremental in failwith ("SMT solver returned 'unknown'; reason: " ^
-   reason) *)
+
+
+
+
 
 (* ISD: Could these globs be different from the saved ones? *)
 let eval mo t =

backend/cn/lib/solver.mli

@@ -56,3 +56,6 @@ val model : unit -> model_with_q
     counter-example model (e.g. for evaluating sub-terms). Might return None in
     case we ask for the value of a "don't care" value in the (minimal) model. *)
 val eval : model -> IndexTerms.t -> IndexTerms.t option
+
+(** Try undecidable SMT solving using full set of assumptions. *)
+val try_hard : bool ref