HolSmt: implement div and mod, fix proof replay, fix translation

Manual/Description/HolSmt.tex

@@ -164,12 +164,12 @@ \subsection{Interface}
 formulas) can be found in \ml{SmtLib\_Parser.sml}, with auxiliary
 functions in \ml{SmtLib\_\{Logics,Theories\}.sml}.
 
-The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{int}
-and \holtxt{real}, fixed-width word types, and the following terms:
-equality, Boolean connectives, quantifiers, numeric literals,
-arithmetic operators, comparison operators, function application, and
-various word operations.  Notably, the SMT-LIB interface does
-\emph{not} support type \holtxt{num}, data types or records, and
+The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{num},
+\holtxt{int} and \holtxt{real}, fixed-width word types, and the
+following terms: equality, Boolean connectives, quantifiers, numeric
+literals, arithmetic operators, comparison operators, function
+application, and various word operations.  Notably, the SMT-LIB
+interface does \emph{not} support data types or records, and
 higher-order formulas.  See the files mentioned above and the examples
 in \ml{selftest.sml} for further details.
 
@@ -194,7 +194,7 @@ \subsection{Interface}
 \subsection{Installing SMT solvers}
 
 \ml{HolSmtLib} has been tested with cvc5~1.1.0, Yices~1.0.40, and
-Z3~4.12.4. Later versions may or may not work.  (Yices~2 is not
+Z3~4.12.6. Later versions may or may not work.  (Yices~2 is not
 supported.)  To use \ml{HolSmtLib}, you need to install at least one
 of these SMT solvers on your machine.  As mentioned before, Yices
 supports a larger fragment of higher-order logic than Z3, but proof

Manual/Translations/IT/Description/HolSmt.tex

@@ -164,12 +164,12 @@ \subsection{Interface}
 formulas) can be found in \ml{SmtLib\_Parser.sml}, with auxiliary
 functions in \ml{SmtLib\_\{Logics,Theories\}.sml}.
 
-The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{int}
-and \holtxt{real}, fixed-width word types, and the following terms:
-equality, Boolean connectives, quantifiers, numeric literals,
-arithmetic operators, comparison operators, function application, and
-various word operations.  Notably, the SMT-LIB interface does
-\emph{not} support type \holtxt{num}, data types or records, and
+The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{num},
+\holtxt{int} and \holtxt{real}, fixed-width word types, and the
+following terms: equality, Boolean connectives, quantifiers, numeric
+literals, arithmetic operators, comparison operators, function
+application, and various word operations.  Notably, the SMT-LIB
+interface does \emph{not} support data types or records, and
 higher-order formulas.  See the files mentioned above and the examples
 in \ml{selftest.sml} for further details.
 
@@ -194,7 +194,7 @@ \subsection{Interface}
 \subsection{Installing SMT solvers}
 
 \ml{HolSmtLib} has been tested with cvc5~1.1.0, Yices~1.0.40, and
-Z3~4.12.4. Later versions may or may not work.  (Yices~2 is not
+Z3~4.12.6. Later versions may or may not work.  (Yices~2 is not
 supported.)  To use \ml{HolSmtLib}, you need to install at least one
 of these SMT solvers on your machine.  As mentioned before, Yices
 supports a larger fragment of higher-order logic than Z3, but proof

src/HolSmt/HolSmtScript.sml

@@ -2,6 +2,8 @@
 
 (* Various theorems for HolSmtLib *)
 
+  val op >> = Tactical.>>
+
   val T = tautLib.TAUT_PROVE
   val P = bossLib.PROVE []
   val S = simpLib.SIMP_PROVE (simpLib.++ (simpLib.++ (simpLib.++
@@ -12,6 +14,9 @@
   val W = wordsLib.WORD_DECIDE
   val B = blastLib.BBLAST_PROVE
 
+  val I = simpLib.SIMP_PROVE (simpLib.++ (simpLib.++
+    (bossLib.arith_ss, intSimps.INT_RWTS_ss), intSimps.INT_ARITH_ss))
+
   (* simplify 't' using 'thms', then prove the simplified term using
      'TAUT_PROVE' *)
   fun U thms t =
@@ -29,7 +34,6 @@
   val _ = Theory.new_theory "HolSmt"
   val _ = ParseExtras.temp_loose_equality()
 
-
   (* constants used by Z3 *)
 
   (* exclusive or *)
@@ -478,10 +482,10 @@
     ``(x = y) \/ ((x =+ z) f y = f y)``)
   val _ = s ("t005", Tactical.prove
     (``(f = g) \/ (f (array_ext f g) <> g (array_ext f g))``,
-    Tactical.THEN (Tactic.DISJ_CASES_TAC
-        (Thm.SPEC ``?x. f x <> g x`` boolTheory.EXCLUDED_MIDDLE),
-      Tactical.THEN (Rewrite.REWRITE_TAC [array_ext_def],
-        bossLib.METIS_TAC []))))
+      Tactic.DISJ_CASES_TAC
+        (Thm.SPEC ``?x. f x <> g x`` boolTheory.EXCLUDED_MIDDLE)
+      >> Rewrite.REWRITE_TAC [array_ext_def]
+      >> bossLib.METIS_TAC []))
 
   val _ = s ("t006", A ``((x :int) <> y) \/ (x <= y)``)
   val _ = s ("t007", A ``((x :int) <> y) \/ (x >= y)``)
@@ -500,11 +504,10 @@
     let
       val RW = bossLib.RW_TAC (bossLib.++ (bossLib.bool_ss, fcpLib.FCP_ss))
     in
-      Tactical.THEN (RW [],
-        Tactical.THEN (Tactic.EXISTS_TAC ``0 :num``,
-          Tactical.THEN (RW [wordsTheory.DIMINDEX_GT_0,
-              wordsTheory.word_1comp_def],
-            tautLib.TAUT_TAC)))
+      RW []
+      >> Tactic.EXISTS_TAC ``0 :num``
+      >> RW [wordsTheory.DIMINDEX_GT_0, wordsTheory.word_1comp_def]
+      >> tautLib.TAUT_TAC
     end))
   val _ = s ("t018", W ``(x = y) ==> x ' i ==> y ' i``)
   val _ = s ("t019", S ``(1w = ~(x :word1)) \/ x ' 0``)

src/HolSmt/SmtLib.sml

@@ -90,8 +90,8 @@ local
     (intSyntax.minus_tm, apfst_K "-"),
     (intSyntax.plus_tm, apfst_K "+"),
     (intSyntax.mult_tm, apfst_K "*"),
-    (* (..., "div"), *)
-    (* (..., "mod"), *)
+    (Term.prim_mk_const {Thy="integer", Name="ediv"}, apfst_K "div"),
+    (Term.prim_mk_const {Thy="integer", Name="emod"}, apfst_K "mod"),
     (intSyntax.absval_tm, apfst_K "abs"),
     (intSyntax.leq_tm, apfst_K "<="),
     (intSyntax.less_tm, apfst_K "<"),
@@ -421,18 +421,24 @@ local
     end
     handle Feedback.HOL_ERR _ =>
 
-    (* let binder - somewhat similar to quantifiers, but we only
-       translate one let at a time (so we don't have to worry about
-       semantic differences caused by parallel vs. sequential let) *)
+    (* let binder - somewhat similar to quantifiers *)
     let
-      val (M, N) = boolSyntax.dest_let tm
-      val (var, body) = Term.dest_abs M
-      val (acc, (Ndecls, N)) = translate_term (acc, (bounds, N))
-      val (bounds, name) = create_bound_name (bounds, var)
+      val (bindings, body) = pairSyntax.dest_anylet tm
+      val (vars, bodies) = ListPair.unzip bindings
+      (* we should translate the bodies without first creating the bound names *)
+      val bounds_bodies = List.map (fn body => (bounds, body)) bodies
+      val (acc, decls_bodies) = Lib.foldl_map translate_term (acc, bounds_bodies)
+      (* now we can create the bound names *)
+      val (bounds, smtvars) = Lib.foldl_map create_bound_name (bounds, vars)
+      val decls_bodies_smtvars = ListPair.zipEq (decls_bodies, smtvars)
+      val (decls, smtbinds) = List.foldl (fn (((d, b), v), (decls, smtbinds)) =>
+        (d @ decls, "(" ^ v ^ " " ^ b ^ ")" :: smtbinds)) ([], [])
+          decls_bodies_smtvars
+      val bindings_str = String.concatWith " " (List.rev smtbinds)
       val (acc, (bodydecls, body)) = translate_term (acc, (bounds, body))
     in
-      (acc, (Ndecls @ bodydecls,
-        "(let ((" ^ name ^ " " ^ N ^ ")) " ^ body ^ ")"))
+      (acc, (decls @ bodydecls,
+        "(let (" ^ bindings_str ^ ") " ^ body ^ ")"))
     end
     handle Feedback.HOL_ERR _ =>
 
@@ -628,8 +634,9 @@ in
         (* arithmeticTheory *)
         GREATER_DEF, GREATER_EQ, MIN_DEF, MAX_DEF,
         (* integerTheory *)
-        INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN, INT_MUL,
-        INT_OF_NUM, INT_POS,
+        INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN, INT_OF_NUM,
+        INT_POS, NUM_OF_INT, NUM_INT_MUL, NUM_INT_EDIV, NUM_INT_EMOD,
+        INT_DIV_EDIV, INT_MOD_EMOD, INT_QUOT_EDIV, INT_REM_EMOD,
         (* others *)
         int_arithTheory.INT_NUM_SUB,
         realaxTheory.real_min, realaxTheory.real_max, realTheory.abs

src/HolSmt/SmtLib_Parser.sml

@@ -451,10 +451,14 @@ local
   end
 
   (* returns an extended 'tmdict' *)
-  fun parse_declare_fun get_token (tydict, tmdict) =
+  fun parse_declare_const_fun parse_types get_token (tydict, tmdict) =
   let
     val name = get_token ()
-    val domain_types = parse_type_list get_token tydict
+    val domain_types =
+      if parse_types then
+        parse_type_list get_token tydict
+      else
+        []
     val range_type = parse_type get_token tydict
     val _ = Library.expect_token ")" (get_token ())
     val tm = Term.mk_var (name,
@@ -469,6 +473,9 @@ local
     (tm, Library.extend_dict ((name, parsefn), tmdict))
   end
 
+  val parse_declare_const = parse_declare_const_fun false
+  val parse_declare_fun = parse_declare_const_fun true
+
   (* returns an extended 'tmdict', and the definition (as a formula) *)
   fun parse_define_fun get_token (tydict, tmdict) =
   let
@@ -506,17 +513,20 @@ local
     (tmdict, definition)
   end
 
-  (* returns the logic's name, its 'tydict', its 'tmdict' extended with
-     declared function symbols, and a list of asserted formulas *)
-  fun parse_commands get_token state =
+  fun dest_state cmd (SOME x) = x
+    | dest_state cmd NONE     =
+        raise ERR "dest_state" ("received " ^ cmd ^ " before set-logic")
+
+  and finalize_state cmd state =
   let
-    fun dest_state cmd =
-      case state of
-        SOME x => x
-      | NONE   => raise ERR "parse_commands" (cmd ^ " issued before set-logic")
-    val _ = Library.expect_token "(" (get_token ())
-    val command = get_token ()
+    val (logic, tydict, tmdict, asserted) = dest_state cmd state
   in
+    (logic, tydict, tmdict, List.rev asserted)
+  end
+
+  (* returns the logic's name, its 'tydict', its 'tmdict' extended with
+     declared function symbols, and a list of asserted formulas *)
+  and parse_command command get_token state =
     case command of "set-info" =>
       let
         val _ = parse_set_info get_token
@@ -533,57 +543,75 @@ local
       end
     | "declare-sort" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "declare-sort"
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-sort" state
         val tydict = parse_declare_sort get_token tydict
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
+    | "declare-const" =>
+      let
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-const" state
+        val (_, tmdict) = parse_declare_const get_token (tydict, tmdict)
+      in
+        parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
+      end
     | "declare-fun" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "declare-fun"
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-fun" state
         val (_, tmdict) = parse_declare_fun get_token (tydict, tmdict)
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
     | "define-fun" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "define-fun"
+        val (logic, tydict, tmdict, asserted) = dest_state "define-fun" state
         val (tmdict, def) = parse_define_fun get_token (tydict, tmdict)
         val asserted = def :: asserted
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
     | "assert" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "assert"
+        val (logic, tydict, tmdict, asserted) = dest_state "assert" state
         val asserted = parse_term get_token (tydict, tmdict) :: asserted
         val _ = Library.expect_token ")" (get_token ())
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
     | "check-sat" =>
       let
-        val _ = dest_state "check-sat"
+        val _ = dest_state "check-sat" state
         val _ = Library.expect_token ")" (get_token ())
       in
         parse_commands get_token state
       end
     | "get-proof" =>
       let
-        val _ = dest_state "get-proof"
+        val _ = dest_state "get-proof" state
         val _ = Library.expect_token ")" (get_token ())
       in
         parse_commands get_token state
       end
     | "exit" =>
-      let
-        val (logic, tydict, tmdict, asserted) = dest_state "exit"
-        val _ = Library.expect_token ")" (get_token ())
-      in
-        (logic, tydict, tmdict, List.rev asserted)
-      end
+      finalize_state "exit" state
+        before Library.expect_token ")" (get_token ())
     | _ =>
       raise ERR "parse_commands" ("unknown command '" ^ command ^ "'")
+
+  (* returns the logic's name, its 'tydict', its 'tmdict' extended with
+     declared function symbols, and a list of asserted formulas *)
+  and parse_commands get_token state =
+  let
+    val tok = SOME (get_token ())
+      (* assume an error to be end-of-stream *)
+      handle _ => NONE
+  in
+    case tok of
+      NONE => finalize_state "(end-of-stream)" state
+    | SOME t => (
+        Library.expect_token "(" t;
+        parse_command (get_token ()) get_token state
+      )
   end
 
   (* entry point into the parser (i.e., the grammar's start symbol) *)

src/HolSmt/SmtLib_Theories.sml

@@ -270,7 +270,10 @@ in
       ("-", leftassoc intSyntax.mk_minus),
       ("+", leftassoc intSyntax.mk_plus),
       ("*", leftassoc intSyntax.mk_mult),
-      (* FIXME: add parsing of div and mod *)
+      ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="integer", Name="ediv"}, t1), t2))),
+      ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="integer", Name="emod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),
@@ -332,7 +335,14 @@ in
       ("-", leftassoc intSyntax.mk_minus),
       ("+", leftassoc intSyntax.mk_plus),
       ("*", leftassoc intSyntax.mk_mult),
-      (* FIXME: add parsing of div and mod *)
+      ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="integer", Name="ediv"}, t1), t2))),
+      ("div0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="integer", Name="ediv"}, t1), t2))),
+      ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="integer", Name="emod"}, t1), t2))),
+      ("mod0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="integer", Name="emod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),

src/HolSmt/Z3_Proof.sml

@@ -37,6 +37,7 @@ struct
                      | DEF_AXIOM of Term.term
                      | ELIM_UNUSED of Term.term
                      | HYPOTHESIS of Term.term
+                     | IFF_FALSE of proofterm * Term.term
                      | IFF_TRUE of proofterm * Term.term
                      | INTRO_DEF of Term.term
                      | LEMMA of proofterm * Term.term

src/HolSmt/Z3_ProofParser.sml

@@ -111,6 +111,8 @@ local
     ("and-elim",        one_prem "and-elim"),
     (* the following is used in `(_ th-lemma arith ...)` inference rules *)
     ("arith",           builtin_name "arith"),
+    (* the following is used in `(_ th-lemma arith ...)` inference rules *)
+    ("assign-bounds",   builtin_name "assign-bounds"),
     (* the following is used in `(_ th-lemma bv ...)` inference rules *)
     ("bv",              builtin_name "bv"),
     ("asserted",        zero_prems "asserted"),
@@ -122,6 +124,7 @@ local
     (* the following is used in `(_ th-lemma arith ...)` inference rules *)
     ("farkas",          builtin_name "farkas"),
     ("hypothesis",      zero_prems "hypothesis"),
+    ("iff-false",       one_prem "iff-false"),
     ("iff-true",        one_prem "iff-true"),
     ("intro-def",       zero_prems "intro-def"),
     ("lemma",           one_prem "lemma"),
@@ -138,7 +141,9 @@ local
     ("quant-inst",      list_args_zero_prems "quant-inst"),
     ("quant-intro",     one_prem "quant-intro"),
     ("refl",            zero_prems "refl"),
-    ("rewrite",         zero_prems "rewrite"),
+    (* in `rewrite` proof rules, we currently ignore the indices (if they exist) *)
+    ("rewrite",         (fn token => fn indices => fn prems =>
+      zero_prems "rewrite" token [] prems)),
     ("sk",              zero_prems "sk"),
     ("symm",            one_prem "symm"),
     ("th-lemma",        SmtLib_Theories.list_list (fn token => fn indices =>
@@ -342,6 +347,7 @@ local
       ("def-axiom",       zero_prems_pt DEF_AXIOM),
       ("elim-unused",     zero_prems_pt ELIM_UNUSED),
       ("hypothesis",      zero_prems_pt HYPOTHESIS),
+      ("iff-false",       one_prem_pt IFF_FALSE),
       ("iff-true",        one_prem_pt IFF_TRUE),
       ("intro-def",       zero_prems_pt INTRO_DEF),
       ("lemma",           one_prem_pt LEMMA),