[interpretation] Activate limited quantifications and unfolding of definitions.

src/interpretation.ml

@@ -36,29 +36,28 @@ type caisar_env = {
 
 type engine = caisar_env CRE.engine
 
-let ls_of_caisar_op (env : engine) op =
-  let caisar_env = CRE.user_env env in
-  if Hashtbl.mem caisar_env.ls_of_caisar_op op
-  then Hashtbl.find_exn caisar_env.ls_of_caisar_op op
-  else
+let ls_of_caisar_op engine op =
+  let caisar_env = CRE.user_env engine in
+  Hashtbl.find_or_add caisar_env.ls_of_caisar_op op ~default:(fun () ->
     let id = Ident.id_fresh "caisar_op" in
     let ty = match op with Dataset _ -> caisar_env.dataset_ty in
     let ls = Term.create_fsymbol id [] ty in
     Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:op ~data:ls;
     Term.Hls.add caisar_env.caisar_op_of_ls ls op;
-    ls
+    ls)
 
-let caisar_op_of_ls env ls =
-  let caisar_env = CRE.user_env env in
+let caisar_op_of_ls engine ls =
+  let caisar_env = CRE.user_env engine in
   Term.Hls.find caisar_env.caisar_op_of_ls ls
 
-let term_of_caisar_op env op = Term.t_app_infer (ls_of_caisar_op env op) []
+let term_of_caisar_op engine op =
+  Term.t_app_infer (ls_of_caisar_op engine op) []
 
-let read_caisar_env env cwd =
+let caisar_env env cwd =
   let th = Env.read_theory env [ "caisar" ] "Interpret" in
-  let dataset_ts = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
+  let ts_dataset = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
   {
-    dataset_ty = Ty.ty_app dataset_ts [];
+    dataset_ty = Ty.ty_app ts_dataset [];
     ls_of_caisar_op = Hashtbl.Poly.create ();
     caisar_op_of_ls = Term.Hls.create 10;
     cwd;
@@ -72,7 +71,7 @@ let compute_size_of_dataset ~cwd s =
   let d = Caml.Filename.concat cwd s in
   Array.length (Caml.Sys.readdir d)
 
-let built_in_caisar : caisar_env CRE.built_in_theories list =
+let builtin_caisar : caisar_env CRE.built_in_theories list =
   let open_dataset : _ CRE.builtin =
    fun engine _ l _ ->
     match l with
@@ -98,18 +97,18 @@ let built_in_caisar : caisar_env CRE.built_in_theories list =
   ]
 
 let interpret_task ~cwd env task =
-  let f = Task.task_goal_fmla task in
-  let caisar_env = read_caisar_env env cwd in
-  let engine =
-    CRE.create
-      {
-        compute_defs = false;
-        compute_builtin = true;
-        compute_def_set = Term.Sls.empty;
-        compute_max_quantifier_domain = 0;
-      }
-      env Ident.Mid.empty caisar_env built_in_caisar
+  let known_map = Task.task_known task in
+  let caisar_env = caisar_env env cwd in
+  let params =
+    {
+      CRE.compute_defs = true;
+      compute_builtin = true;
+      compute_def_set = Term.Sls.empty;
+      compute_max_quantifier_domain = Int.max_value;
+    }
   in
+  let engine = CRE.create params env known_map caisar_env builtin_caisar in
+  let f = Task.task_goal_fmla task in
   let f = CRE.normalize ~limit:1000 engine Term.Mvs.empty f in
   Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
     f print_caisar_op caisar_env

stdlib/caisar.mlw

@@ -83,6 +83,7 @@ end
 
 theory Interpret
   use bool.Bool
+  use int.Int
 
   type input
   type dataset
@@ -90,5 +91,7 @@ theory Interpret
   function open_dataset string: dataset
   function size dataset: int
 
-  predicate forall_ (d: dataset) (f: input -> bool)
+  function get (i:int) (d:dataset) : input
+
+  predicate forall_ (d: dataset) (f: input -> bool) = forall i:int. -1 < i < size d -> f (get i d)
 end

tests/interpretation.t

@@ -19,6 +19,10 @@ Test interpret
   >   goal G5:
   >       let dataset = open_dataset "datasets/a" in
   >       forall_ dataset (fun i -> robust i)
+  > 
+  >   goal G6:
+  >       let dataset = open_dataset "datasets/a" in
+  >       forall i:int. i=1+(size dataset) -> i < 4
   > end
   > EOF
   G1 : true
@@ -31,6 +35,9 @@ Test interpret
   G4 : true
   caisar_op1,
   (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
-  G5 : forall_ caisar_op2 (fun (i:input) -> robust i)
+  G5 : robust (get 0 caisar_op2) /\ robust (get 1 caisar_op2)
   caisar_op2,
   (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+  G6 : forall i:int. i = 3 -> i < 4
+  caisar_op3,
+  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })