From cce6f83bbf8716f6793030aafbb250277ee5208d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Tue, 25 Jul 2023 12:17:50 +0200
Subject: [PATCH] Sane(r) error messages for produce-models error situations

This is a reloaded version of #738 with tests.

Fixes #737
---
 src/bin/common/solving_loop.ml | 12 ++++------
 tests/cram.t/run.t             | 42 ++++++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 7 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 940152825..dc9a54ff7 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -362,10 +362,10 @@ let main () =
          PR. See https://github.com/OCamlPro/alt-ergo/pull/553 *)
       if Stdlib.(Options.get_sat_solver () = Tableaux) then
         Options.set_interpretation ILast
-      else Printer.print_wrn "%a The generation of models is not supported \
-                              for the current SAT solver. Please choose the \
-                              SAT solver Tableaux."
-          Loc.report st_loc
+      else
+        Printer.print_smtlib_err
+          "Model generation requires the Tableaux solver \
+           (try --produce-models)";
     | ":produce-models", Symbol { name = Simple "false"; _ } ->
       Options.set_interpretation INone
     | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } ->
@@ -523,9 +523,7 @@ let main () =
           begin
             (* TODO: add the location of the statement. *)
             Printer.print_smtlib_err
-              "You have to set the flag :produce-models with \
-               (set-option :produce-models true) \
-               before using the statement (get-model).";
+              "Model generation disabled (try --produce-models)";
             st
           end
 
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 21ed6600d..b12111977 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -45,3 +45,45 @@ And some SMT2 action.
   unknown
   
   unsat
+
+Here are some tests to check that we have sane behavior given the insane
+combinations of produce-models et al.
+
+First, if model generation is not enabled, we should error out when a
+`(get-model)` statement is issued:
+
+  $ echo '(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
+  (error "Model generation disabled (try --produce-models)")
+
+This should be the case Tableaux solver as well:
+
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  (error "Model generation disabled (try --produce-models)")
+
+The messages above mention `--produce-models`, but we can also use
+`set-option`. This requires the Tableaux solver, however:
+
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2
+  (error "No model produced.")
+
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  (error "No model produced.")
+
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
+  (error "Model generation requires the Tableaux solver (try --produce-models)")
+  (error "Model generation disabled (try --produce-models)")
+
+And now some cases where it should work (using either `--produce-models` or
+`Tableaux` with `set-option`):
+
+  $ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null
+  
+  unknown
+  (
+  )
+
+  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null
+  
+  unknown
+  (
+  )