[Array] new cmdline options

colibri2/tests/solve/smt_array/sat/dune

@@ -11,17 +11,17 @@
    (run
     %{exe:../../../generate_tests/generate_dune_tests.exe}
     --options
-    ""
+    "no-wegraph no-res-ext no-res-aup"
     --options
-    "array-res-ext"
+    "no-wegraph no-res-aup"
     --options
-    "array-res-ext array-res-aup"
+    "no-wegraph"
     --options
-    "array-wegraph"
+    "no-res-ext no-res-aup"
     --options
-    "array-wegraph array-res-ext"
+    "no-res-aup"
     --options
-    "array-wegraph array-res-ext array-res-aup"
+    ""
     .
     sat)))
  (mode promote))

colibri2/tests/solve/smt_array/sat/sat-res/dune

@@ -11,13 +11,13 @@
    (run
     %{exe:../../../../generate_tests/generate_dune_tests.exe}
     --options
-    "array-res-ext"
+    "no-wegraph no-res-aup"
     --options
-    "array-res-ext array-res-aup"
+    "no-wegraph"
     --options
-    "array-wegraph array-res-ext"
+    "no-res-aup"
     --options
-    "array-wegraph array-res-ext array-res-aup"
+    ""
     .
     sat)))
  (mode promote))

colibri2/tests/solve/smt_array/sat/sat-res/dune.inc

-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))

colibri2/tests/solve/smt_array/step_limit_reached/notes.txt

 - sat/test3.smt2:
   works with:
-  - "--array-res-ext"
-  - "--array-wegraph --array-res-ext"
+  - "--no-wegraph --no-res-aup"
+  - "--no-res-aup"
 
 - sat/test4.smt2:
   works with:
-  - ""
-  - "--array-wegraph"
+  - "--no-wegraph --no-res-ext --no-res-aup"
+  - "--no-res-ext --no-res-aup"
 
 - unsat/distinct2:
   fails with:
-  - ""
-  - "--array-wegraph"
+  - "--no-wegraph --no-res-ext --no-res-aup"
+  - "--no-res-ext --no-res-aup"
 
 - sat/test4.smt2

colibri2/tests/solve/smt_array/unsat/dune

@@ -11,17 +11,17 @@
    (run
     %{exe:../../../generate_tests/generate_dune_tests.exe}
     --options
-    ""
+    "no-wegraph no-res-ext no-res-aup"
     --options
-    "array-res-ext"
+    "no-wegraph no-res-aup"
     --options
-    "array-res-ext array-res-aup"
+    "no-wegraph"
     --options
-    "array-wegraph"
+    "no-res-ext no-res-aup"
     --options
-    "array-wegraph array-res-ext"
+    "no-res-aup"
     --options
-    "array-wegraph array-res-ext array-res-aup"
+    ""
     .
     unsat)))
  (mode promote))

colibri2/theories/array/RWRules.ml

@@ -318,7 +318,7 @@ let new_array =
   fun env ind_gty val_gty f ->
     (* Extensionality rule ext: a, b ⇒ (a = b) ⋁ (a[k] ≠ b[k]) *)
     let agty = Ground.Ty.array ind_gty val_gty in
-    (if not (Options.get env restrict_ext) then
+    (if Options.get env no_res_ext then
      match GHT.find_opt db_gty env agty with
      | Some s ->
          Ground.S.iter

colibri2/theories/array/array.ml

@@ -28,14 +28,14 @@ open RWRules
 (*
   Command line options:
   - "None": uses RW1(adown), RW2(aup), idx and extensionality
-  - "--array-res-ext": restricts the extrensionality rule using the foreign
+  - "--no-wegraph": don't use the weak equivalency graph
+  - "--no-res-ext": don't restrict the extrensionality rule using the foreign
     domain
-  - "--array-res-aup": restricts the RW2 rule using the linearity domain
+  - "--no-res-aup": don't restrict the RW2 rule using the linearity domain
   - "--array-ext-comb": to support additional combinators
     (const, map, def_ind, def_val)
   - "--array-blast-rule": uses the blast rule when it suits
   - "--array-def-values": suppots the rules on the default values
-  - "--array-wegraph": uses the weak equivalency graph
 *)
 
 let converter env (f : Ground.t) =
@@ -53,10 +53,10 @@ let converter env (f : Ground.t) =
   match s with
   | { app = { builtin = Expr.Base; id_ty; _ }; args; tyargs; _ } ->
       if IArray.is_empty args then (
-        if Options.get env restrict_aup && f_is_array then
+        if (not (Options.get env no_res_aup)) && f_is_array then
           (* update of the Linearity domain *)
           Linearity_dom.upd_dom env fn Empty)
-      else if Options.get env restrict_ext then (
+      else if not (Options.get env no_res_ext) then (
         (* update of the Foreign domain *)
         let subst, arg_tys =
           match id_ty.ty_descr with
@@ -94,9 +94,10 @@ let converter env (f : Ground.t) =
       Id.Array.set_id env a;
       Id.Index.set_id env i;
       Ground.add_ty env i ind_gty;
-      if Options.get env use_wegraph then WEGraph.new_select env fn a i;
+      if not (Options.get env no_wegraph) then WEGraph.new_select env fn a i;
       (* update of the Foreign domain *)
-      if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then
+      if (not (Options.get env no_res_ext)) && ind_gty.app.builtin == Expr.Array
+      then
         (* id and ground type are set during registration *)
         Foreign_dom.set_dom env (Ground.Ty.array ind_gty val_gty) i IsForeign;
       if Options.get env extended_comb then (
@@ -139,7 +140,7 @@ let converter env (f : Ground.t) =
       Id.Index.set_id env k;
       Id.Value.set_id env v;
       (* update of the Linearity domain *)
-      if Options.get env restrict_aup then
+      if not (Options.get env no_res_aup) then
         Linearity_dom.upd_dom env fn (Linear b);
       (* application of the `idx` rule *)
       let rn = Equality.equality env [ mk_select env a k ind_gty val_gty; v ] in
@@ -158,7 +159,7 @@ let converter env (f : Ground.t) =
         in
         Egraph.register env eq_node;
         Boolean.set_true env eq_node);
-      if Options.get env use_wegraph then WEGraph.new_store env a b k v
+      if not (Options.get env no_wegraph) then WEGraph.new_store env a b k v
   | {
    app = { builtin = Builtin.Array_diff; _ };
    args;
@@ -216,7 +217,7 @@ let init env =
   Array_value.init_ty env;
   Array_value.init_check env;
   Ground.register_converter env converter;
-  if Options.get env use_wegraph then (
+  if not (Options.get env no_wegraph) then (
     Id.Array.register_new_id_hook env WEGraph.new_id_hook;
     Id.Array.register_merge_hook env WEGraph.eq_arrays_norm;
     Id.Index.register_new_id_hook env WEGraph.new_index_id_hook;
@@ -227,7 +228,7 @@ let init env =
   (* extᵣ (restricted extensionality):
      - (a = b) ≡ false |> (a[k] ≠ b[k])
      - a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
-  if Options.get env restrict_ext then (
+  if not (Options.get env no_res_ext) then (
     (* if Options.get env use_wegraph then (
          (* (a = b) ≡ false |> (a[k] ≠ b[k]) (when a and b are neighbours) *)
          Equality.register_hook_new_disequality env apply_res_ext_1_2;
@@ -241,7 +242,7 @@ let init env =
     Foreign_dom.register_hook_new_foreign_array env apply_res_ext_2_1);
   let l = [ (adown_pattern, adown_run) ] in
   let l =
-    if Options.get env restrict_aup then (raup_pattern, raup_run) :: l
+    if not (Options.get env no_res_aup) then (raup_pattern, raup_run) :: l
     else (aup_pattern, aup_run) :: l
   in
   let l =

colibri2/theories/array/common.ml

@@ -24,16 +24,26 @@ open Colibri2_popop_lib
 open Popop_stdlib
 module HT = Datastructure.Hashtbl (DInt)
 
-let restrict_ext =
-  Options.register ~pp:Fmt.bool "Array.res-ext"
+let no_wegraph =
+  Options.register ~pp:Fmt.bool "Array.no-wegraph"
     Cmdliner.Arg.(
       value & flag
-      & info [ "array-res-ext" ] ~doc:"Restrict the extensionality rule")
+      & info [ "no-wegraph" ]
+          ~doc:"Don't use the array theory's weak equivalency graph")
 
-let restrict_aup =
+let no_res_ext =
+  Options.register ~pp:Fmt.bool "Array.no-res-ext"
+    Cmdliner.Arg.(
+      value & flag
+      & info [ "no-res-ext" ]
+          ~doc:"Don't restrict the array extensionality rule")
+
+let no_res_aup =
   Options.register ~pp:Fmt.bool "Array.res-aup"
     Cmdliner.Arg.(
-      value & flag & info [ "array-res-aup" ] ~doc:"Restrict the ⇑ rule")
+      value & flag
+      & info [ "no-res-aup" ]
+          ~doc:"Don't restrict the array's ⇑ (select over store) rule")
 
 let extended_comb =
   Options.register ~pp:Fmt.bool "Array.res-comb"
@@ -54,12 +64,6 @@ let default_values =
       & info [ "array-def-values" ]
           ~doc:"Use inference rules for default values")
 
-let use_wegraph =
-  Options.register ~pp:Fmt.bool "Array.wegraph"
-    Cmdliner.Arg.(
-      value & flag
-      & info [ "array-wegraph" ] ~doc:"Use the array's weak equivalency graph")
-
 let debug =
   Debug.register_info_flag ~desc:"Debugging messages of the array theory"
     "Array"
@@ -455,8 +459,8 @@ end) : IdDomSig = struct
       | Some id1, n1, Some id2, n2 ->
           Datastructure.Push.iter merge_hooks env ~f:(fun f ->
               f env (n1, id1) (n2, id2) b)
-          (* id1 always stays, b allows to determine which one will become the
-             representative *)
+      (* id1 always stays, b allows to determine which one will become the
+         representative *)
       | _ ->
           (* Ideally, should be unreachable, but it is with the test
              "./colibri2/tests/solve/smt_array/unsat/ite1.smt2"? *)

colibri2/theories/array/common.mli

@@ -19,12 +19,12 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-val restrict_ext : bool Options.t
-val restrict_aup : bool Options.t
+val no_wegraph : bool Options.t
+val no_res_ext : bool Options.t
+val no_res_aup : bool Options.t
 val extended_comb : bool Options.t
 val blast_rule : bool Options.t
 val default_values : bool Options.t
-val use_wegraph : bool Options.t
 val debug : Debug.flag
 val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t