Support SMT-LIB v2.7 bit-vector operators in psmt2

The new bit-vector operators from v2.7 are not available in SMT-LIB 2.6
scripts, which makes sense since Dolmen is intended to be able to check
adherence to the specification.

On the other hand, there is no standard specification for the psmt2
format, and while it implements polymorphism differently from SMT-LIB
2.7, there is no reason for psmt2 operators to be restricted to those
available in version 2.6 of the standard.

Allow the new bit-vector operators from version 2.7 of the standard when
parsing files with psmt2 syntax.

Author: bclement-ocp

src/languages/smtlib2/print/print.ml

@@ -753,20 +753,20 @@ module Make(Config : Config)(Lexer : Lexer with type token := Config.token) = st
 
           | To_int { n = _; signed = true; } ->
             begin match Config.version with
-              | V2_7 -> simple "sbv_to_int"
-              | V2_6 | Poly -> _cannot_print "sbv_to_int"
+              | V2_7 | Poly -> simple "sbv_to_int"
+              | V2_6 -> _cannot_print "sbv_to_int"
             end
           | To_int { n = _; signed = false; } ->
             begin match Config.version with
-              | V2_7 -> simple "ubv_to_int"
+              | V2_7 | Poly -> simple "ubv_to_int"
               (* bvconv extension
                  TODO: use a flag to enable extensions such as this one ? *)
-              | V2_6 | Poly -> simple "bv2nat" (* 2.7: "sbv_to_int" *)
+              | V2_6 -> simple "bv2nat" (* 2.7: "sbv_to_int" *)
             end
           | Of_int { n } ->
             begin match Config.version with
-              | V2_6 | Poly -> p Term (N.indexed "int2bv" [int n])
-              | V2_7 -> p Term (N.indexed "int_to_bv" [int n])
+              | V2_6 -> p Term (N.indexed "int2bv" [int n])
+              | V2_7 | Poly -> p Term (N.indexed "int_to_bv" [int n])
             end
         end
 

src/typecheck/bitv.ml

@@ -232,11 +232,12 @@ module Smtlib2 = struct
       | _ -> T.extract i j bitv
 
     let parse version env s =
-      let atleast2_7 () =
+      (* Whether to include bit-vector operators from smt-lib 2.7 *)
+      let bitv2_7 () =
         match (version : Dolmen.Smtlib2.version) with
-        | `Script (`Latest | `V2_7)
+        | `Script (`Latest | `V2_7 | `Poly)
         | `Response (`Latest | `V2_7) -> true
-        | `Script (`V2_6 | `Poly)
+        | `Script (`V2_6)
         | `Response (`V2_6) -> false
       in
       match s with
@@ -325,34 +326,34 @@ module Smtlib2 = struct
       | Type.Id { ns = Term; name = Simple "concat"; } ->
         Type.builtin_term (Base.term_app2 (module Type) env s T.concat)
 
-      | Type.Id { ns = Term; name = Simple "bvnego"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvnego"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app1 (module Type) env s T.nego)
-      | Type.Id { ns = Term; name = Simple "bvsaddo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvsaddo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s (T.addo ~signed:true))
-      | Type.Id { ns = Term; name = Simple "bvuaddo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvuaddo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s (T.addo ~signed:false))
-      | Type.Id { ns = Term; name = Simple "bvssubo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvssubo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s (T.subo ~signed:true))
-      | Type.Id { ns = Term; name = Simple "bvusubo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvusubo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s (T.subo ~signed:false))
-      | Type.Id { ns = Term; name = Simple "bvsmulo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvsmulo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s (T.mulo ~signed:true))
-      | Type.Id { ns = Term; name = Simple "bvumulo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvumulo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s (T.mulo ~signed:false))
-      | Type.Id { ns = Term; name = Simple "bvsdivo"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "bvsdivo"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app2 (module Type) env s T.divo)
 
-      | Type.Id { ns = Term; name = Simple "ubv_to_int"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "ubv_to_int"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app1 (module Type) env s (T.to_int ~signed:false))
-      | Type.Id { ns = Term; name = Simple "sbv_to_int"; } when atleast2_7 () ->
+      | Type.Id { ns = Term; name = Simple "sbv_to_int"; } when bitv2_7 () ->
         Type.builtin_term (Base.term_app1 (module Type) env s (T.to_int ~signed:true))
 
       (* indexed terms *)
       | Type.Id { ns = Term; name = Indexed { basename; indexes; } } as symbol ->
         Base.parse_indexed basename indexes (function
             | s when (String.length s >= 2 && s.[0] = 'b' && s.[1] = 'v') ->
               `Unary (fun n -> Type.builtin_term (parse_extended_lit env symbol s n))
-            | "int_to_bv" when atleast2_7 () -> `Unary (function i_s ->
+            | "int_to_bv" when bitv2_7 () -> `Unary (function i_s ->
                 Type.builtin_term (Base.term_app1_ast (module Type) env symbol
                           (indexed_positive env T.of_int i_s)))
             | "repeat" -> `Unary (function i_s ->