HolSmt: parse indexed identifiers' indices as terms

Prior to SMT-LIB 2.5, the indices of indexed identifiers could only
be numerals.

In SMT-LIB 2.5 and later, identifiers can be indexed not just with
numerals but also with symbols. This was implemented in commit
8a2e9bc

However, the `quant-inst` inference rule in Z3 v4 proofs can contain
arbitrary terms as its indices, as seen in this example:

((_ quant-inst (v12 v17) (v11 v17 ?x304)) ...)

In order to add support for this rule in a follow-up commit, the
SMT-LIB parser was changed to support arbitrary terms as indices in
term identifiers (but not type identifiers).

This should be a superset of what SMT-LIB allows, which should be fine
because we don't need to implement a strict parser.

However, Z3 v2 proof certificates contain inference rules such as the
following:

(_ |th-lemma| arith farkas -41/42 -1)

In particular, `-41/42` and `-1` are not valid SMT-LIB terms. We used
to parse this successfully because we allowed arbitrary strings as
indices, but since we are trying to parse terms, this is now being
rejected by the parser.

Due to this regression, proof replay for some test cases was disabled
for Z3 v2 (but they are still enabled for Z3 v4).

src/HolSmt/Library.sml

@@ -132,6 +132,17 @@ struct
       end
   end
 
+  fun undo_look_ahead symbols get_token =
+  let
+    val buffer = ref symbols
+    fun get_token' () =
+      case !buffer of
+        [] => get_token ()
+      | x::xs => (buffer := xs; x)
+  in
+    get_token'
+  end
+
   fun parse_arbnum (s : string) =
     let
       fun handle_err () =
@@ -187,7 +198,7 @@ struct
 
   (* creates a dictionary that maps strings to lists of parsing functions *)
   fun dict_from_list xs
-      : (string, (string -> string list -> 'a list -> 'a) list)
+      : (string, (string -> Term.term list -> 'a list -> 'a) list)
         Redblackmap.dict =
     List.foldl extend_dict (Redblackmap.mkDict String.compare) xs
 

src/HolSmt/SmtLib_Logics.sml

@@ -35,12 +35,12 @@ local
 
   val BV_extension_tmdict = Library.dict_from_list [
     (* bit-vector constants *)
-    ("_", one_zero (fn token => fn n_str =>
+    ("_", one_zero (fn token => fn n_tm =>
       if String.isPrefix "bv" token then
         let
           val decimal = String.extract (token, 2, NONE)
           val value = Library.parse_arbnum decimal
-          val n = Library.parse_arbnum n_str
+          val n = Arbint.toNat (intSyntax.int_of_term n_tm)
         in
           Lib.curry wordsSyntax.mk_word value n
         end
@@ -63,21 +63,21 @@ local
     ("bvashr", K_zero_two wordsSyntax.mk_word_asr_bv),
     ("repeat", K_one_one
       (Lib.curry wordsSyntax.mk_word_replicate o numSyntax.mk_numeral o
-        Library.parse_arbnum)),
+      Arbint.toNat o intSyntax.int_of_term)),
     ("zero_extend", K_one_one (fn n => fn t => wordsSyntax.mk_w2w (t,
       fcpLib.index_type
         (Arbnum.+ (fcpLib.index_to_num (wordsSyntax.dim_of t),
-          Library.parse_arbnum n))))),
+          Arbint.toNat (intSyntax.int_of_term n)))))),
     ("sign_extend", K_one_one (fn n => fn t => wordsSyntax.mk_sw2sw (t,
       fcpLib.index_type
         (Arbnum.+ (fcpLib.index_to_num (wordsSyntax.dim_of t),
-          Library.parse_arbnum n))))),
+          Arbint.toNat (intSyntax.int_of_term n)))))),
     ("rotate_left", K_one_one
       (Lib.C (Lib.curry wordsSyntax.mk_word_rol) o numSyntax.mk_numeral o
-        Library.parse_arbnum)),
+        Arbint.toNat o intSyntax.int_of_term)),
     ("rotate_right", K_one_one
       (Lib.C (Lib.curry wordsSyntax.mk_word_ror) o numSyntax.mk_numeral o
-        Library.parse_arbnum)),
+        Arbint.toNat o intSyntax.int_of_term)),
     ("bvule", K_zero_two wordsSyntax.mk_word_ls),
     ("bvugt", K_zero_two wordsSyntax.mk_word_hi),
     ("bvuge", K_zero_two wordsSyntax.mk_word_hs),

src/HolSmt/SmtLib_Parser.sml

@@ -5,7 +5,7 @@
 structure SmtLib_Parser =
 struct
 
-  type 'a parse_fn = string -> string list -> 'a list -> 'a
+  type 'a parse_fn = string -> Term.term list -> 'a list -> 'a
 
 local
 
@@ -43,7 +43,7 @@ local
      to these arguments. It raises 'HOL_ERR' if the arguments are not
      valid. 'parse_term' uses the result of the first parsing function
      that does not raise 'HOL_ERR'. 5. Each parsing function
-     additionally takes a list of indices, each one a string. This
+     additionally takes a list of indices, each one a `Term.term`. This
      list will be empty for non-indexed identifiers, and non-empty for
      indexed identifiers. Non-indexed identifiers are therefore
      parsed as a special case of indexed identifiers. This allows
@@ -73,7 +73,7 @@ local
      for declared types, one for declared terms), while parsing types
      only requires one dictionary (for declared types). *)
 
-  fun t_with_args dict (token : string) (indices : string list)
+  fun t_with_args dict (token : string) (indices : Term.term list)
       (args : 'a list) : 'a =
     Lib.tryfind (fn f => f token indices args) (Redblackmap.find (dict, token)
       handle Redblackmap.NotFound => [])
@@ -83,10 +83,15 @@ local
       handle Redblackmap.NotFound => [])
     handle Feedback.HOL_ERR _ =>
       raise ERR "t_with_args" ("failed to parse '" ^ token ^
-        "' (with indices [" ^ String.concatWith ", " indices ^
-        "] and " ^ Int.toString (List.length args) ^ " argument(s))")
+        "' (with indices [" ^ String.concatWith ", "
+        (List.map Hol_pp.term_to_string indices) ^ "] and " ^
+        Int.toString (List.length args) ^ " argument(s))")
 
-  fun parse_indexed_t get_token dict : 'a list -> 'a =
+  (***************************************************************************)
+  (* type-specific parsing functions                                         *)
+  (***************************************************************************)
+
+  fun parse_indexed_type get_token dict : Type.hol_type list -> Type.hol_type =
   let
     (* returns all tokens before the next ")" *)
     fun get_tokens acc =
@@ -100,14 +105,12 @@ local
     end
   in
     case get_tokens [] of
-      [] => raise ERR "parse_indexed_t" "'_' immediately followed by ')'"
-    | hd::tl => t_with_args dict hd tl
+      [] => raise ERR "parse_indexed_type" "'_' immediately followed by ')'"
+    | hd::tl =>
+        t_with_args dict hd (List.map (numSyntax.mk_numeral o
+          Library.parse_arbnum) tl)
   end
 
-  (***************************************************************************)
-  (* type-specific parsing functions                                         *)
-  (***************************************************************************)
-
   fun parse_type_operands get_token tydict acc : Type.hol_type list =
   let
     val token = get_token ()
@@ -137,7 +140,7 @@ local
     val token = get_token ()
   in
     if token = "_" then
-      parse_indexed_t get_token tydict
+      parse_indexed_type get_token tydict
     else
       let
         val t = parse_compound_type get_token tydict token
@@ -169,7 +172,26 @@ local
   (* term-specific parsing functions                                         *)
   (***************************************************************************)
 
-  fun parse_var_bindings get_token (tydict, tmdict)
+  fun parse_indexed_term get_token (tydict, tmdict) : Term.term list -> Term.term =
+  let
+    val head = get_token ()
+
+    (* returns all terms corresponding to the indices *)
+    fun get_indices acc =
+    let
+      val token = get_token ()
+      val get_token' = Library.undo_look_ahead [token] get_token
+    in
+      if token = ")" then
+        List.rev acc
+      else
+        get_indices (parse_term get_token' (tydict, tmdict) :: acc)
+    end
+  in
+    t_with_args tmdict head (get_indices [])
+  end
+
+  and parse_var_bindings get_token (tydict, tmdict)
     : (string * Term.term) list =
   let
     val _ = Library.expect_token "(" (get_token ())
@@ -306,7 +328,7 @@ local
     val token = get_token ()
   in
     if token = "_" then
-      parse_indexed_t get_token tmdict
+      parse_indexed_term get_token (tydict, tmdict)
     else
       let
         val t = if token = "let" then

src/HolSmt/SmtLib_Theories.sml

@@ -156,7 +156,7 @@ in
 
     val tydict = Library.dict_from_list [
       ("BitVec", K_one_zero (wordsSyntax.mk_word_type o fcpLib.index_type o
-        Library.parse_arbnum))
+        numSyntax.dest_numeral))
     ]
 
     val tmdict = Library.dict_from_list [
@@ -183,9 +183,10 @@ in
           raise ERR "<Fixed_Size_BitVectors.tmdict._>"
             "not a bit-vector constant")),
       ("concat", K_zero_two wordsSyntax.mk_word_concat),
-      ("extract", K_two_one (fn (m_str, n_str) =>
+      ("extract", K_two_one (fn (m_tm, n_tm) =>
         let
-          val (m, n) = Lib.pair_map Library.parse_arbnum (m_str, n_str)
+          val (m, n) = Lib.pair_map (Arbint.toNat o intSyntax.int_of_term)
+            (m_tm, n_tm)
           val index_type = fcpLib.index_type (Arbnum.plus1 (Arbnum.- (m, n)))
           val (m, n) = Lib.pair_map numSyntax.mk_numeral (m, n)
         in

src/HolSmt/Z3_ProofParser.sml

@@ -90,12 +90,26 @@ local
       ([listSyntax.mk_list_type pt_ty, Type.bool], pt_ty))))) o
       Lib.apfst (Lib.C (Lib.curry listSyntax.mk_list) pt_ty) o Lib.front_last)
 
+  (* This function is used only to allow some symbols used as indices in indexed
+     identifiers to be parsed (as terms) without the parser erroring out due to
+     not having the symbols in the term dictionary. *)
+  fun builtin_name name =
+    SmtLib_Theories.K_zero_zero (Term.mk_var (name, Type.alpha))
+
   val z3_builtin_dict = Library.dict_from_list [
     ("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 bv ...)` inference rules *)
+    ("bv",              builtin_name "bv"),
     ("asserted",        zero_prems "asserted"),
     ("commutativity",   zero_prems "commutativity"),
     ("def-axiom",       zero_prems "def-axiom"),
     ("elim-unused",     zero_prems "elim-unused"),
+    (* the following is used in `(_ th-lemma arith ...)` inference rules *)
+    ("eq-propagate",    builtin_name "eq-propagate"),
+    (* the following is used in `(_ th-lemma arith ...)` inference rules *)
+    ("farkas",          builtin_name "farkas"),
     ("hypothesis",      zero_prems "hypothesis"),
     ("iff-true",        one_prem "iff-true"),
     ("intro-def",       zero_prems "intro-def"),
@@ -112,23 +126,26 @@ local
     ("th-lemma",        SmtLib_Theories.list_list (fn token => fn indices =>
       fn prems =>
         let
-          (* Parsing this rule: (_ |th-lemma| arith farkas -1 -1 1)
+          (* Parsing this rule: (_ |th-lemma| arith farkas 1 1 1)
              The vertical bars have already been eliminated in the tokenizer, so
              we're already matching "th-lemma".
 
-             The indices will be passed as ["arith", "farkas", "-1", "-1", "1"]
-             but currently we only care about the first one (the theory name), so
-             we'll discard the rest.
+             The indices will be passed as [``arith``, ``farkas``, ``1``, ``1``,
+             ``1``] but currently we only care about the first one (the theory
+             name), so we'll discard the rest.
 
              We'll change the name of the rule to "th-lemma-<theory>" which will
              later hook into the theory-specific rule processing. *)
-          val theory = List.hd indices
-          val name = "th-lemma-" ^ theory
+          val theory_tm = List.hd indices
+          val theory_str = Lib.fst (Term.dest_var theory_tm)
+          val name = "th-lemma-" ^ theory_str
         in
           list_prems name token [] prems
         end)),
     ("trans",           two_prems "trans"),
     ("trans*",          list_prems "trans*"),
+    (* the following is used in `(_ th-lemma arith ...)` inference rules *)
+    ("triangle-eq",     builtin_name "triangle-eq"),
     ("true-axiom",      zero_prems "true-axiom"),
     ("unit-resolution", list_prems "unit-resolution"),
 
@@ -178,11 +195,12 @@ local
       else
         raise ERR "<z3_builtin_dict._>" "not extract[m:n]")),
     (* (_ extractm n) t *)
-    ("_", SmtLib_Theories.one_one (fn token => fn n_str =>
+    ("_", SmtLib_Theories.one_one (fn token => fn n_tm =>
       if String.isPrefix "extract" token then
         let
           val m_str = String.extract (token, 7, NONE)
-          val (m, n) = Lib.pair_map Library.parse_arbnum (m_str, n_str)
+          val m = Library.parse_arbnum m_str
+          val n = Arbint.toNat (intSyntax.int_of_term n_tm)
           val index_type = fcpLib.index_type (Arbnum.plus1 (Arbnum.- (m, n)))
           val (m, n) = Lib.pair_map numSyntax.mk_numeral (m, n)
         in
@@ -339,17 +357,6 @@ local
     (Redblackmap.insert (steps, id, proofterm_of_term t), vars)
   end
 
-  fun undo_look_ahead symbols get_token =
-  let
-    val buffer = ref symbols
-    fun get_token' () =
-      case !buffer of
-        [] => get_token ()
-      | x::xs => (buffer := xs; x)
-  in
-    get_token'
-  end
-
   (* distinguishes between a term definition and a proofterm
      definition; returns a (possibly extended) dictionary and proof *)
   fun parse_definition get_token (tydict, tmdict, proof) =
@@ -391,7 +398,7 @@ local
     else
       let
         (* undo look-ahead of 2 tokens *)
-        val get_token' = undo_look_ahead ["(", head] get_token
+        val get_token' = Library.undo_look_ahead ["(", head] get_token
         val t = SmtLib_Parser.parse_term get_token' (tydict, tmdict)
       in
         (* Z3 assigns no ID to the final proof step; we use ID 0 *)
@@ -424,7 +431,7 @@ local
     ) else
       let
         (* undo look-ahead of 2 tokens *)
-        val get_token' = undo_look_ahead ["(", head] get_token
+        val get_token' = Library.undo_look_ahead ["(", head] get_token
       in
         parse_proof_expression get_token' (tydict, tmdict, proof) rpars
       end
@@ -457,7 +464,7 @@ local
       (* Z3 v2.19 proof *)
       let
         (* undo look-ahead of the 2 tokens *)
-        val get_token' = undo_look_ahead ["(", token] get_token
+        val get_token' = Library.undo_look_ahead ["(", token] get_token
       in
         parse_proof_decl get_token' state 0
       end
@@ -466,7 +473,7 @@ local
       let
         val () = Library.expect_token "(" token
         (* leave the 1st parenthesis consumed and undo the 2nd *)
-        val get_token' = undo_look_ahead ["("] get_token
+        val get_token' = Library.undo_look_ahead ["("] get_token
       in
         parse_proof_decl get_token' state 1
       end

src/HolSmt/selftest.sml

@@ -467,8 +467,10 @@ in
     (``(x:real) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``x > 0 ==> (x:real) / 42 < x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``x < 0 ==> (x:real) / 42 > x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``x > 0 ==> (x:real) / 42 < x``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``x < 0 ==> (x:real) / 42 > x``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``abs (x:real) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(abs (x:real) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
@@ -554,10 +556,14 @@ in
 
     (``((x:int) < y) = (y > x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``((x:int) <= y) = (y >= x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:int) < y /\ y <= z ==> x < z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:int) <= y /\ y <= z ==> x <= z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:int) > y /\ y >= z ==> x > z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:int) >= y /\ y >= z ==> x >= z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:int) < y /\ y <= z ==> x < z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:int) <= y /\ y <= z ==> x <= z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:int) > y /\ y >= z ==> x > z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:int) >= y /\ y >= z ==> x >= z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``(x:int) >= 0``, [sat_YO, sat_Z3, sat_Z3p]),
     (``0 < (x:int) /\ x <= 1 ==> (x = 1)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
@@ -572,7 +578,8 @@ in
     (``0r <= 1r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``1r <= 0r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:real) <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:real) <= y ==> 42 * x <= 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:real) <= y ==> 42 * x <= 42 * y``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``1r > 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``0r > 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -582,14 +589,19 @@ in
     (``1r >= 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``0r >= 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:real) >= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:real) >= y ==> 42 * x >= 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:real) >= y ==> 42 * x >= 42 * y``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``((x:real) < y) = (y > x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``((x:real) <= y) = (y >= x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:real) < y /\ y <= z ==> x < z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:real) <= y /\ y <= z ==> x <= z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:real) > y /\ y >= z ==> x > z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
-    (``(x:real) >= y /\ y >= z ==> x >= z``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:real) < y /\ y <= z ==> x < z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) <= y /\ y <= z ==> x <= z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) > y /\ y >= z ==> x > z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) >= y /\ y >= z ==> x >= z``,
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``(x:real) >= 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``0 < (x:real) /\ x <= 1 ==> (x = 1)``,