CN: Check countermodels (#829)

* draft of minimal checking algo for string example * sync * bug fixes * fixed equality * removed completed TODOs * made LAT more modular * changed display to show resources that may be and are not invalid as well * code showing why mutual recursion is necessary * readability * cleanup * saving before merging * saving before merging * improved pp in explain * cleanup of comments * version fix * nits * nits * nits * nits * nits * fixed var bug in countermodels * reverted to 4.14 * Make SMT solver consider the full set of assumptions, including the ones leading to undecidability -- as an experiment. * fix for older OCaml * version errors and allows use of solver for comparison of candidate * changed display to only show predicates that failed the check, not ones that passed * style * style * fixes per PR comments * ask_solver fix * ask_solver fix * moved LAT logic into explain * removed old TODO * style * style * resolving comments * pr comment fixes * PR comment fixes; currently broken due to question of provable output type * temporary fix to Unknown ambiguity * resolving comments * style * style * no longer using try hard mode * removed try_hard * updated ask_solver to use add_assumption * added try-hard back * no longer shows output of checking preds if empty * style * style * style * style * style report * typo --------- Co-authored-by: Christopher Pulte <cp526@cam.ac.uk>
rems-project · Mar 5, 2025 · 5277e69 · 5277e69
1 parent 8813898
commit 5277e69
Show file tree

Hide file tree

Showing 14 changed files with 744 additions and 49 deletions.
diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
@@ -303,6 +303,7 @@ let verify
   no_inherit_loc
   magic_comment_char_dollar
   disable_resource_derived_constraints
+  try_hard
   =
   if json then (
     if debug_level > 0 then
@@ -323,6 +324,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;
@@ -872,6 +874,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)
@@ -1039,6 +1046,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 =