[models] Add tests for model generation

rsc/extra/pre-commit--git-hook

@@ -29,4 +29,4 @@ if [[ $errors -ne 0 ]]; then
 fi
 
 # If there are whitespace errors, print the offending file names and fail.
-exec git diff-index --check --cached $against --
+exec git diff-index --check --cached $against -- ':!*.t' ':!*.expected'

tests/models/arith/arith1.expected

@@ -0,0 +1,14 @@
+
+unknown
+(
+
+ ; Functions
+
+ ; Constants
+
+(define-fun x () Int 0)
+
+ ; Arrays not yet supported
+
+
+)

tests/models/arith/arith1.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Int)
+(assert (<= x 42))
+(check-sat)
+(get-model)

tests/models/arith/arith2.expected

@@ -0,0 +1,16 @@
+
+unknown
+(
+
+ ; Functions
+
+ ; Constants
+
+(define-fun x () Int 8)
+
+(define-fun y () Int 42)
+
+ ; Arrays not yet supported
+
+
+)

tests/models/arith/arith2.smt2

@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Int)
+(declare-const y Int)
+(assert (and (<= x 42) (>= x 0) (>= y 42) (= (+ x y) 50)))
+(check-sat)
+(get-model)

tests/models/bool/bool1.expected

@@ -0,0 +1,30 @@
+
+unknown
+(
+
+ ; Functions
+
+ ; Constants
+
+ ; Arrays not yet supported
+
+
+)
+
+unknown
+(
+
+ ; Functions
+
+ ; Constants
+
+(define-fun p () Bool true)
+
+(define-fun q () Bool true)
+
+(define-fun nq () Bool true)
+
+ ; Arrays not yet supported
+
+
+)

tests/models/bool/bool1.smt2

@@ -0,0 +1,15 @@
+(set-logic QF_UF)
+(set-option :produce-models true) ; enable model generation
+(declare-const p Bool)
+(declare-const q Bool)
+; (declare-const t Int)
+(define-fun nq () Bool q)
+(assert (=> (not p) (not nq)))
+(check-sat)
+(get-model)
+(get-assignment)
+(assert q)
+(check-sat)
+(get-model)
+(get-assignment)
+(exit)

tests/models/bool/bool2.expected

@@ -0,0 +1,12 @@
+
+unknown
+(
+
+ ; Functions
+
+ ; Constants
+
+ ; Arrays not yet supported
+
+
+)

tests/models/bool/bool2.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(set-option :produce-models true)
+(declare-const x Bool)
+(declare-const y Bool)
+(assert (or x (not x)))
+(check-sat)
+(get-model)
+(get-assignment)

tests/models/uf/uf1.expected

@@ -0,0 +1,18 @@
+
+unknown
+(
+
+ ; Functions
+
+(define-fun f ((arg_0 Int)) Int 0)
+
+ ; Constants
+
+(define-fun a () Int 0)
+
+(define-fun b () Int 0)
+
+ ; Arrays not yet supported
+
+
+)

tests/models/uf/uf1.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-fun f (Int) Int)
+(declare-const a Int)
+(declare-const b Int)
+(assert (= (f a) (f b)))
+(check-sat)
+(get-model)

tests/models/uf/uf2.expected

@@ -0,0 +1,18 @@
+
+unknown
+(
+
+ ; Functions
+
+(define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0))
+
+ ; Constants
+
+(define-fun a () Int 0)
+
+(define-fun b () Int (- 2))
+
+ ; Arrays not yet supported
+
+
+)

tests/models/uf/uf2.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-fun f (Int) Int)
+(declare-const a Int)
+(declare-const b Int)
+(assert (distinct (f a) (f b)))
+(check-sat)
+(get-model)

tools/gentest.ml

@@ -176,6 +176,7 @@ module Batch : sig
 
   val make:
     frontend:string option ->
+    filter:string list option ->
     path: string -> cmds: Cmd.t list
     -> pb_files: string list -> t
   (** Set up a batch of tests. *)
@@ -192,13 +193,23 @@ end = struct
     tests: Test.t list;
   }
 
-  let make ~frontend ~path ~cmds ~pb_files =
+  let make ~frontend ~filter ~path ~cmds ~pb_files =
+    let filter =
+      match filter with
+      | Some filter ->
+        fun cmd -> List.exists (String.equal (Cmd.name cmd)) filter
+      | None ->
+        fun _ -> true
+    in
     let arg = Option.map (Format.asprintf "--frontend %s") frontend in
     let tests = List.fold_left (fun acc1 pb_file ->
         List.fold_left (fun acc2 cmd ->
-            let cmd_opt = Option.map (fun arg -> Cmd.add_arg ~arg cmd) arg in
-            let cmd = Option.value ~default:cmd cmd_opt in
-            (Test.make ~cmd ~pb_file) :: acc2
+            if filter cmd then
+              let cmd_opt = Option.map (fun arg -> Cmd.add_arg ~arg cmd) arg in
+              let cmd = Option.value ~default:cmd cmd_opt in
+              (Test.make ~cmd ~pb_file) :: acc2
+            else
+              acc2
           ) acc1 cmds) [] pb_files
     in
     {path; cmds; tests}
@@ -247,12 +258,12 @@ let is_a_problem file =
   File.has_extension_in file [".ae"; ".smt2"; ".pstm2"; ".zip"]
 
 (* Generate a dune file for each subfolder of the path given as argument. *)
-let rec generate ?frontend path cmds =
+let rec generate ?frontend ?filter path cmds =
   let files, folders = File.scan_folder path in
   let () = match List.filter is_a_problem files with
     | [] -> ()
     | pb_files -> (
-        let batch = Batch.make ~frontend ~path ~cmds ~pb_files in
+        let batch = Batch.make ~frontend ~filter ~path ~cmds ~pb_files in
         Batch.generate_expected_file batch;
         Batch.generate_dune_file batch
       ) in
@@ -261,7 +272,12 @@ let rec generate ?frontend path cmds =
       let frontend =
         if folder = "dolmen" then Some "dolmen" else frontend
       in
-      generate ?frontend path cmds
+      let filter =
+        match folder with
+        | "models" -> Some ["models"; "models_ci"]
+        | _ -> filter
+      in
+      generate ?frontend ?filter path cmds
     ) folders
 
 let () =
@@ -293,6 +309,16 @@ let () =
       "--output=smtlib2"
     ; timelimit
     ; "--sat-solver CDCL-Tableaux" ])
+  ; ("runtest-quick", "models",
+     [ "--output=smtlib2"
+     ; "--frontend dolmen"
+     ; "--sat-solver=Tableaux"
+     ; timelimit ])
+  ; ("runtest-ci", "models_ci",
+     [ "--output=smtlib2"
+     ; "--frontend dolmen"
+     ; "--sat-solver=Tableaux"
+     ; timelimit ])
   ; ("runtest-ci", "dolmen_ci", [
       "--output=smtlib2"
     ; timelimit