From feefe1fcd35f63119e4944c434d8ed9e22a9cced Mon Sep 17 00:00:00 2001
From: Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
Date: Sun, 16 Jun 2024 03:09:05 +0200
Subject: [PATCH] Add command to convert smtml scripts to smt-lib scripts

---
 bin/main.ml                  | 45 +++++++++++++++++++++++++++++-------
 test/parser/test_core.t      |  2 +-
 test/parser/test_lia.t       |  2 +-
 test/parser/test_lra.t       |  2 +-
 test/parser/test_qf_fp.t     |  2 +-
 test/parser/test_qf_s.t      |  2 +-
 test/regression/test_pr_71.t |  2 +-
 7 files changed, 43 insertions(+), 14 deletions(-)

diff --git a/bin/main.ml b/bin/main.ml
index 2b65a6cc..dac1a72f 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -33,7 +33,7 @@ let prove_mode_conv =
     [ ("batch", Batch); ("cached", Cached); ("incremental", Incremental) ]
 
 let parse_cmdline =
-  let aux files solver prover_mode debug print_statistics =
+  let run debug files solver prover_mode print_statistics =
     let module Mappings =
       (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
     in
@@ -72,24 +72,53 @@ let parse_cmdline =
         Solver.pp_statistics state.solver
     end
   in
+
+  let to_smt2 debug solver file =
+    let module Mappings =
+      (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
+    in
+    Mappings.set_debug debug;
+    let ast = Parse.from_file ~filename:file in
+    let assertions =
+      List.filter_map (function Ast.Assert e -> Some e | _ -> None) ast
+    in
+    Format.printf "%a@." (Mappings.pp_smt ?status:None) assertions
+  in
+
   let open Cmdliner in
+  let file0 =
+    Arg.(
+      required
+      & pos 0 (some string) None
+      & info [] ~docv:"files" ~doc:"files to read" )
+  in
   let files =
     Arg.(value & pos_all string [] & info [] ~docv:"files" ~doc:"files to read")
-  and prover =
+  in
+  let solver =
     Arg.(
       value & opt solver_conv Z3_solver
       & info [ "s"; "solver" ] ~doc:"SMT solver to use" )
-  and prover_mode =
+  in
+  let solver_mode =
     Arg.(
       value & opt prove_mode_conv Batch & info [ "mode" ] ~doc:"SMT solver mode" )
-  and debug =
+  in
+  let debug =
     Arg.(value & flag & info [ "debug" ] ~doc:"Print debugging messages")
-  and print_statistics =
+  in
+  let print_statistics =
     Arg.(value & flag & info [ "st" ] ~doc:"Print statistics")
   in
-  Cmd.v
-    (Cmd.info "smtml" ~version:"%%VERSION%%")
-    Term.(const aux $ files $ prover $ prover_mode $ debug $ print_statistics)
+
+  let run_cmd =
+    Cmd.v (Cmd.info "run")
+      Term.(const run $ debug $ files $ solver $ solver_mode $ print_statistics)
+  in
+  let to_smt2 =
+    Cmd.v (Cmd.info "to-smt2") Term.(const to_smt2 $ debug $ solver $ file0)
+  in
+  Cmd.group (Cmd.info "smtml" ~version:"%%VERSION%%") [ run_cmd; to_smt2 ]
 
 let () =
   match Cmdliner.Cmd.eval_value parse_cmdline with
diff --git a/test/parser/test_core.t b/test/parser/test_core.t
index d2752686..44ceb565 100644
--- a/test/parser/test_core.t
+++ b/test/parser/test_core.t
@@ -1,5 +1,5 @@
 Test boolean parsing:
-  $ dune exec -- smtml test_core.smtml
+  $ smtml run test_core.smtml
   sat
   sat
   (model
diff --git a/test/parser/test_lia.t b/test/parser/test_lia.t
index 4860ec2b..9a359ab4 100644
--- a/test/parser/test_lia.t
+++ b/test/parser/test_lia.t
@@ -1,4 +1,4 @@
 Test int parsing:
-  $ dune exec -- smtml test_lia.smtml
+  $ smtml run test_lia.smtml
   sat
   sat
diff --git a/test/parser/test_lra.t b/test/parser/test_lra.t
index 1da1829e..4d64156d 100644
--- a/test/parser/test_lra.t
+++ b/test/parser/test_lra.t
@@ -1,5 +1,5 @@
 Test real parsing:
-  $ dune exec -- smtml test_lra.smtml
+  $ smtml run test_lra.smtml
   sat
   (model
     (x -2.)
diff --git a/test/parser/test_qf_fp.t b/test/parser/test_qf_fp.t
index 173cbd68..dcb8a296 100644
--- a/test/parser/test_qf_fp.t
+++ b/test/parser/test_qf_fp.t
@@ -1,5 +1,5 @@
 Test fp parsing:
-  $ dune exec -- smtml test_qf_fp.smtml
+  $ smtml run test_qf_fp.smtml
   unsat
   sat
   sat
diff --git a/test/parser/test_qf_s.t b/test/parser/test_qf_s.t
index 7d25b19a..98ddbd55 100644
--- a/test/parser/test_qf_s.t
+++ b/test/parser/test_qf_s.t
@@ -1,5 +1,5 @@
 Test parsing string:
-  $ dune exec -- smtml test_qf_s.smtml
+  $ smtml run test_qf_s.smtml
   sat
   (model
     (x "abcd"))
diff --git a/test/regression/test_pr_71.t b/test/regression/test_pr_71.t
index b7558ae2..561b1ae4 100644
--- a/test/regression/test_pr_71.t
+++ b/test/regression/test_pr_71.t
@@ -1,3 +1,3 @@
 Test float parsing:
-  $ smtml test_pr_71.smtml
+  $ smtml run test_pr_71.smtml
   sat