Merge branch 'benchmarks' into 'master'

Integrated benchmarks and switch to incremental generated parser

See merge request !11

benchmarks/cardiGML.sh

+for DEPTH in {1..32}
+do
+    FILE=$(printf "%s%i" CARDI $DEPTH)
+    cool-gen_exec -series cardi -depth $DEPTH -output $FILE
+done
+
+hyperfine -i -w 1 -r 3 --style basic --export-csv "CARDI-cool-adaptive.csv" -P depth 1 316 "timeout 1m sh -c \"cat CARDI{depth}.cool | cool-coalg sat GML --propagationRate adaptive > CARDI{depth}-cool-adaptive.out\""
+#hyperfine -i -w 1 -r 3 --style basic --export-csv "CARDI-cool-once.csv" -P depth 1 512 "timeout 1m sh -c \"cat CARDI{depth}.cool | cool-coalg sat GML --propagationRate once > CARDI{depth}-cool-once.out\""
+
+./factSetup.sh
+hyperfine -i -w 1 -r 3 --style basic --export-csv "CARDI-fact.csv" -P depth 1 20 "timeout 1m sh -c \"cat CARDI{depth}.fact | ./factWrapper.sh > CARDI{depth}-fact.out\""

benchmarks/earlyGML.sh

+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "EARLY-adaptive.csv" 'cool-gen_exec -series early -depth {size} -functor GML | timeout 30m cool-coalg sat GML --propagationRate adaptive '
+
+#hyperfine -i -w 1 -r 3 --style basic -P size 1 10 --export-csv "EARLY-once.csv" 'cool-gen_exec -series early -depth {size} -functor GML | timeout 1m cool-coalg prov GML --propagationRate once'
+#crashed nach dem ersten schnell

benchmarks/factSetup.sh

+FaCT++ -get-default-options > /tmp/fact.conf 2> /dev/null
+printf '\n[Query]\nTBox = /tmp/fact.tbox\nTarget = formula\n' >> /tmp/fact.conf

benchmarks/factWrapper.sh

+
+while read -r fmla
+do
+    printf "(defconcept formula %s)\n" "$fmla" > /tmp/fact.tbox
+done
+
+FaCT++ /tmp/fact.conf 2> /dev/null

benchmarks/parityGML.sh

+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY1-adaptive.csv" 'cool-gen_exec -amount 1 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY2-adaptive.csv" 'cool-gen_exec -amount 2 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY4-adaptive.csv" 'cool-gen_exec -amount 4 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY8-adaptive.csv" 'cool-gen_exec -amount 8 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY16-adaptive.csv" 'cool-gen_exec -amount 16 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY32-adaptive.csv" 'cool-gen_exec -amount 32 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 20 --export-csv "PARITY64-adaptive.csv" 'cool-gen_exec -amount 64 -series parity -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+#hyperfine -i -w 1 -r 3 --style basic -P size 1 5 --export-csv "PARITY1-once.csv" 'cool-gen_exec -series parity -amount 1 -depth {size} -functor GML | timeout 1m cool-coalg prov GML --propagationRate once'
+#creasht ab 3 schnell

benchmarks/parityNegGML.sh

+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG1-adaptive.csv" 'cool-gen_exec -amount 1 -parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG2-adaptive.csv" 'cool-gen_exec -amount 2 -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG4-adaptive.csv" 'cool-gen_exec -amount 4 -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG8-adaptive.csv" 'cool-gen_exec -amount 8 -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG16-adaptive.csv" 'cool-gen_exec -amount 16 -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG32-adaptive.csv" 'cool-gen_exec -amount 32 -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "PARITYNEG64-adaptive.csv" 'cool-gen_exec -amount 64 -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+#hyperfine -i -w 1 -r 3 --style basic -P size 1 4 -P branching 1 10 --export-csv "PARITYNEG-once.csv" 'cool-gen_exec -amount {branching} -series parity-neg -depth {size} -functor GML | timeout 1m cool-coalg prov GML --propagationRate once'
+
+#crasht ab 3 schnell

benchmarks/rabin.sh

+hyperfine -i -w 1 -r 3 --style basic -P size 1 2 --export-csv "RABIN-REACTIVE-GML-adaptive.csv" 'cool-gen_exec -series rabin-reactive -depth {size} -amount 0 -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 3 --export-csv "RABIN-REACTIVE-K-adaptive.csv" 'cool-gen_exec -series rabin-reactive -depth {size} -functor K | timeout 1m cool-coalg sat K --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 3 --export-csv "RABIN-COBUECHI-GML-adaptive.csv" 'cool-gen_exec -series rabin-cobuechi -depth {size} -amount 0 -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "RABIN-COBUECHI-K-adaptive.csv" 'cool-gen_exec -series rabin-cobuechi -depth {size} -functor K | timeout 1m cool-coalg sat K --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 3 --export-csv "RABIN-GAME-COBUECHI-GML-adaptive.csv" 'cool-gen_exec -series rabin-game-cobuechi -depth {size} -amount 0 -functor GML | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "RABIN-GAME-COBUECHI-K-adaptive.csv" 'cool-gen_exec -series rabin-game-cobuechi -depth {size} -functor K | timeout 1m cool-coalg sat K --propagationRate adaptive '
+
+#hyperfine -i -w 1 -r 3 --style basic -P size 1 5 --export-csv "RABIN-once.csv" 'cool-gen_exec -functor GML -series rabin-reactive -depth {size} | timeout 1m cool-coalg sat GML --propagationRate once'

benchmarks/randomBenchmark.sh

+for FUNC in GML K
+do
+    for DEPTH in 16 32 64 128
+    do
+        COOL=()
+        FACT=()
+        for RUN in $(seq 1 100)
+        do
+            FILE=$(printf "%s%i_%i" $FUNC $DEPTH $RUN)
+            cool-gen_exec -functor $FUNC -depth $DEPTH -output $FILE
+            COOL+=("timeout 1m sh -c \"cat $FILE.cool | cool-coalg sat $FUNC > $FILE-cool.out\"")
+            FACT+=("timeout 1m sh -c \"cat $FILE.fact | ./factWrapper.sh > $FILE-fact.out\"")
+        done
+
+        hyperfine -i -w 1 -r 3 --style basic --export-csv "$FUNC-$DEPTH-cool.csv" "${COOL[@]}"
+
+        ./factSetup.sh
+        hyperfine -i -w 1 -r 3 --style basic --export-csv "$FUNC-$DEPTH-fact.csv" "${FACT[@]}"
+    done
+done

benchmarks/streettGML.sh

+hyperfine -i -w 1 -r 3 --style basic -P size 1 5 --export-csv "STREETT-adaptive.csv" 'cool-gen_exec -functor GML -series streett -depth {size} | timeout 1m cool-coalg prov GML --propagationRate adaptive '
+
+#hyperfine -i -w 1 -r 3 --style basic -P size 1 4 --export-csv "STREETT-once.csv" 'cool-gen_exec -functor GML -series streett -depth {size} | timeout 1m cool-coalg prov GML --propagationRate once'

benchmarks/streettK.sh

+hyperfine -w 1 -r 3 --style basic -P size 1 15 --export-csv "K-STREETT-once.csv" 'cool-gen_exec -functor K -series streett -depth {size} | cool-coalg prov K --propagationRate once'
+
+#hyperfine -w 1 -r 3 --style basic -P size 1 15 --export-csv "K-STREETT-adaptive.csv" 'cool-gen_exec -functor K -series streett -depth {size} | cool-coalg prov K --propagationRate adaptive'

benchmarks/treeGML.sh

+hyperfine -i -w 1 -r 3 --style basic -P size 1 13 --export-csv "TREE-adaptive.csv" 'cool-gen_exec -functor GML -series tree -depth $((2**{size})) | timeout 1m cool-coalg sat GML --propagationRate adaptive '
+
+hyperfine -i -w 1 -r 3 --style basic -P size 1 15 --export-csv "TREE-once.csv" 'cool-gen_exec -functor GML -series tree -depth $((2**{size})) | timeout 1m cool-coalg sat GML --propagationRate once'

benchmarks/uncardiGML.sh

+for DEPTH in {1..23}
+do
+    FILE=$(printf "%s%i" UNCARDI $DEPTH)
+    cool-gen_exec -series uncardi -depth $DEPTH -output $FILE
+done
+
+hyperfine -i -w 1 -r 3 --style basic --export-csv "UNCARDI-cool-adaptive.csv" -P depth 1 23 "timeout 1m sh -c \"cat UNCARDI{depth}.cool | cool-coalg sat GML --propagationRate adaptive > UNCARDI{depth}-cool-adaptive.out\""
+#hyperfine -i -w 1 -r 3 --style basic --export-csv "UNCARDI-cool-once.csv" -P depth 1 27 "timeout 1m sh -c \"cat UNCARDI{depth}.cool | cool-coalg sat GML --propagationRate once > UNCARDI{depth}-cool-once.out\""
+
+./factSetup.sh
+hyperfine -i -w 1 -r 3 --style basic --export-csv "UNCARDI-fact.csv" -P depth 1 12 "timeout 1m sh -c \"cat UNCARDI{depth}.fact | ./factWrapper.sh > UNCARDI{depth}-fact.out\""

default.nix

@@ -37,9 +37,9 @@ with nixpkgs; rec {
     });
   cool-docker = callPackage ./nix/cool-docker.nix { inherit versions cool; };
   cool-metrics = callPackage ./nix/cool-metrics.nix { inherit cool; };
-
+  cool-benchmark = callPackage ./nix/cool-benchmark.nix { inherit cool; factplusplus = callPackage ./nix/fact++.nix {}; };
   cool-devenv = mkShell {
-    inputsFrom = [ cool cool-lib cool-generators ];
+    inputsFrom = [ cool cool-lib cool-generators cool-benchmark ];
     packages = with ocamlPackages; [ ocaml-lsp dune_3 menhir ];
   };
 }

lib/src/ALCFormula.ml

@@ -1346,7 +1346,7 @@ let exportFormulaAlcTableau f =
 (** Creates a file representing a TBox in FaCT++ format.
     The satisfiability query is the definition
     of the special concept name "SAT".
-    @param The name of the output file.
+    @param filename The name of the output file.
     @param fl A list of formulae which are to be tested for joint satisfiability.
     @param tboxND A list of formulae representing
     the non-definitional part of a TBox.

lib/src/CoAlgFormula.ml

@@ -277,34 +277,6 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula *
 
 let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
 
-let convertToMu formula =
-  let name = Stream.next gensym in
-  let helper formula =
-    match formula with
-    | AF f1 ->
-       MU (name, (OR (f1, (AX (default_relation, (VAR name))))))
-    | EF f1 ->
-       MU (name, (OR (f1, (EX (default_relation, (VAR name))))))
-    | AG f1 ->
-       NU (name, (AND (f1, (AX (default_relation, (VAR name))))))
-    | EG f1 ->
-       NU (name, (AND (f1, (EX (default_relation, (VAR name))))))
-    | AU (f1, f2) ->
-       MU (name, (OR (f2, (AND (f1, (AX (default_relation, (VAR name))))))))
-    | EU (f1, f2) ->
-       MU (name, (OR (f2, (AND (f1, (EX (default_relation, (VAR name))))))))
-    | AR (f1, f2) ->
-       NU (name, (AND (f2, (OR (f1, (AX (default_relation, (VAR name))))))))
-    | ER (f1, f2) ->
-       NU (name, (AND (f2, (OR (f1, (EX (default_relation, (VAR name))))))))
-    | AB (f1, f2) ->
-       NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX (default_relation, (VAR name)))))))))
-    | EB (f1, f2) ->
-       NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX (default_relation, (VAR name)))))))))
-    | _ -> formula
-  in
-  convert_post helper formula
-
 let has_no_CTL_connectives formula =
   let accu = ref true in
   let helper formula =
@@ -314,49 +286,61 @@ let has_no_CTL_connectives formula =
   in
   iter helper formula; !accu
 
-let rec debug_buffer_of_formula sb f =
+let rec debug_buffer_of_formula sb (f : formula) =
   let p s = Buffer.add_string sb s in
   let psub f = Buffer.add_char sb '('; debug_buffer_of_formula sb f ; Buffer.add_char sb ')' in
-  match f with
+  let st s = "\"" ^ s ^ "\"" in
+  let int i = string_of_int i in
+  let rat r = string_of_rational r in
+  let bool b = string_of_bool b in
+  let lst f l =
+    match l with
+    | [] -> "[]"
+    | h :: t -> "[" ^ List.fold_left (fun accu a -> accu ^ "; " ^ f a) (f h) t ^ "]"
+  in
+  let bin' c a b = p (c ^ " (" ^ a); p ", "; psub b; p ")" in
+  let bin c a b = p (c ^ " ("); psub a; p ", "; psub b; p ")" in
+  let ter'' con a b c = p (con ^ " (" ^ a ^ ", " ^ b); p ", "; psub c; p ")" in
+  match (f : formula) with
   | TRUE -> p "TRUE"
   | FALSE -> p "FALSE"
-  | AP s -> p ("AP_" ^ s)
+  | AP s -> p ("AP " ^ st s)
   | NOT f -> p "NOT "; psub f
-  | AT (n, f) -> p ("AT_" ^ n); psub f
-  | OR (f1, f2) ->  p "OR "; psub f1; psub f2
-  | AND (f1, f2) ->  p "AND "; psub f1; psub f2
-  | EQU (f1, f2) ->  p "EQU "; psub f1; psub f2
-  | IMP (f1, f2) ->  p "IMP "; psub f1; psub f2
-  | EX (r, f) -> p ("EX_" ^ r); psub f
-  | AX (r, f) -> p ("AX_" ^ r); psub f
-  | ENFORCES (c, f) -> p "ENFORCES_{ "; List.iter (fun i -> p (string_of_int i ^ " ")) c; p "} "; psub f
-  | ALLOWS (c, f) -> p "ALLOWS_{ "; List.iter (fun i -> p (string_of_int i ^ " ")) c; p "} "; psub f
-  | MIN (i, r, f) -> p ("MIN_" ^ r ^ "^" ^ string_of_int i); psub f
-  | MAX (i, r, f) -> p ("MAX_" ^ r ^ "^" ^ string_of_int i); psub f
-  | MORETHAN (i, r, f) -> p ("MORETHAN_" ^ r ^ "^" ^ string_of_int i); psub f
-  | MAXEXCEPT (i, r, f) -> p ("MAXEXCEPT_" ^ r ^ "^" ^ string_of_int i); psub f
-  | ATLEASTPROB (i, f) -> p ("ATLEASTPROB^" ^ string_of_rational i); psub f
-  | LESSPROBFAIL (i, f) -> p ("LESSPROBFAIL^" ^ string_of_rational i); psub f
-  | CONST s -> p ("CONST_" ^ s)
-  | CONSTN s -> p ("CONSTN_" ^ s)
+  | AT (n, f) -> bin' "AT" (st n) f
+  | OR (f1, f2) ->  bin "OR" f1 f2
+  | AND (f1, f2) ->  bin "AND" f1 f2
+  | EQU (f1, f2) ->  bin "EQU" f1 f2
+  | IMP (f1, f2) ->  bin "IMP" f1 f2
+  | EX (r, f) -> bin' "EX" (st r) f
+  | AX (r, f) -> bin' "AX" (st r) f
+  | ENFORCES (c, f) -> bin' "ENFORCES" (lst int c) f
+  | ALLOWS (c, f) -> bin' "ALLOWS" (lst int c) f
+  | MIN (i, r, f) -> ter'' "MIN" (int i) (st r) f
+  | MAX (i, r, f) -> ter'' "MAX" (int i) (st r) f
+  | MORETHAN (i, r, f) -> ter'' "MORETHAN" (int i) (st r) f
+  | MAXEXCEPT (i, r, f) -> ter'' "MAXEXCEPT" (int i) (st r) f
+  | ATLEASTPROB (i, f) -> bin' "ATLEASTPROB" (rat i) f
+  | LESSPROBFAIL (i, f) -> bin' "LESSPROBFAIL" (rat i) f
+  | CONST s -> p ("CONST " ^ st s)
+  | CONSTN s -> p ("CONSTN" ^ st s)
   | ID f -> p "ID "; psub f
-  | NORM (f1, f2) ->  p "NORM "; psub f1; psub f2
-  | NORMN (f1, f2) ->  p "NORMN "; psub f1; psub f2
-  | CHC (f1, f2) ->  p "CHC "; psub f1; psub f2
-  | FUS (b, f) -> p ("FUS_" ^ string_of_bool b); psub f
-  | MU (v, f) -> p ("MU " ^ v); psub f
-  | NU  (v, f) -> p ("NU " ^ v); psub f
-  | VAR s -> p ("VAR " ^ s)
+  | NORM (f1, f2) -> bin "NORM" f1 f2
+  | NORMN (f1, f2) -> bin "NORMN" f1 f2
+  | CHC (f1, f2) ->  bin "CHC" f1 f2
+  | FUS (b, f) -> bin' "FUS" (bool b) f
+  | MU (v, f) -> bin' "MU" (st v) f
+  | NU  (v, f) -> bin' "NU " (st v) f
+  | VAR s -> p ("VAR " ^ st s)
   | AF f -> p "AF "; psub f
   | EF f -> p "EF "; psub f
   | AG f -> p "AG "; psub f
   | EG f -> p "EG "; psub f
-  | AU (f1, f2) ->  p "AU "; psub f1; psub f2
-  | EU (f1, f2) ->  p "EU "; psub f1; psub f2
-  | AR (f1, f2) ->  p "AR "; psub f1; psub f2
-  | ER (f1, f2) ->  p "ER "; psub f1; psub f2
-  | AB (f1, f2) ->  p "AB "; psub f1; psub f2
-  | EB (f1, f2) ->  p "EB "; psub f1; psub f2
+  | AU (f1, f2) -> bin "AU" f1 f2
+  | EU (f1, f2) -> bin "EU" f1 f2
+  | AR (f1, f2) -> bin "AR" f1 f2
+  | ER (f1, f2) -> bin "ER" f1 f2
+  | AB (f1, f2) -> bin "AB" f1 f2
+  | EB (f1, f2) -> bin "EB" f1 f2
 
 let debug_string_of_formula f =
   let sb = Buffer.create 128 in
@@ -808,7 +792,7 @@ let rec verifyMuAltFree formula =
      raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
 
 
-exception NotAconjunctive of unit
+exception NotAconjunctive of string
 
 let isMuAconjunctive (formula:formula) : bool =
   let module SS = Set.Make(String) in
@@ -834,7 +818,7 @@ let isMuAconjunctive (formula:formula) : bool =
 
        (* If both subformulas contain free mu variables, the formula is not aconjunctive *)
        if not (SS.is_empty a_vars) && not (SS.is_empty b_vars) then
-         raise (NotAconjunctive ())
+         raise (NotAconjunctive (string_of_int __LINE__))
        else
          SS.union a_vars b_vars (* one of them is empty anyways *)
 
@@ -856,7 +840,7 @@ let isMuAconjunctive (formula:formula) : bool =
        raise (CoAlgException ("verifyMuAconjunctiveInternal: CTL should have been removed at this point"))
   in
   try ignore (verifyMuAconjunctiveInternal formula SS.empty); true
-  with NotAconjunctive () -> false
+  with NotAconjunctive _ -> false
 
 (** Process from outside in. For every variable bound keep the tuple
     (name, negations). For every negation crossed map a +1 over snd on
@@ -1657,14 +1641,14 @@ let const_imp f1 f2 = IMP (f1, f2)
     @param f A formula.
     @return The formula EX (s, f).
  *)
-let const_ex s f = EX (s, f)
+let const_ex ?(rel = default_relation) f = EX (rel, f)
 
 (** Constructs an AX-formula from a formula.
     @param s A role name.
     @param f A formula.
     @return The formula AX (s, f).
  *)
-let const_ax s f = AX (s, f)
+let const_ax ?(rel = default_relation) f = AX (rel, f)
 
 (** Constructs a MIN-formula from a formula.
     @param n A non-negative integer.
@@ -1673,9 +1657,9 @@ let const_ax s f = AX (s, f)
     @return The formula MIN f.
     @raise CoAlgException Iff n is negative.
  *)
-let const_min n s f =
+let const_min n ?(rel = default_relation) f =
   if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
-  else MIN (n, s, f)
+  else MIN (n, rel, f)
 
 (** Constructs a MAX-formula from a formula.
     @param n A non-negative integer.
@@ -1684,9 +1668,9 @@ let const_min n s f =
     @return The formula MAX f.
     @raise CoAlgException Iff n is negative.
  *)
-let const_max n s f =
+let const_max n ?(rel = default_relation) f =
   if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
-  else MAX (n, s, f)
+  else MAX (n, rel, f)
 
 let const_enforces p f =
     ENFORCES (p,f)
@@ -1708,6 +1692,17 @@ let const_choice f1 f2 = CHC (f1, f2)
  *)
 let const_fusion first f1 = FUS (first, f1)
 
+let const_maxexcept n ?(rel = default_relation) f = MAXEXCEPT (n, rel, f)
+let const_morethan n ?(rel = default_relation) f = MORETHAN (n, rel, f)
+
+let const_big_or formulas = match formulas with
+  | [] -> FALSE
+  | h :: tl -> List.fold_left const_or h tl
+
+let const_big_and formulas = match formulas with
+  | [] -> TRUE
+  | h :: tl -> List.fold_left const_and h tl
+
 
 (** Hash-consed formulae, which are in negation normal form,
     such that structural and physical equality coincide.
@@ -2248,6 +2243,43 @@ let rec parseFormulaToTree formula =
     | EB (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
         Node ([child1; child2], (fun fList -> EB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
 
+let uniqueVars f =
+  let rec h form mapping =
+    match form with
+    | VAR s -> begin
+        match List.assoc_opt s mapping with
+        | Some v -> VAR v
+        | None -> VAR s  (* leave free variables untouched *)
+      end
+    | MU (s, sub) -> let name = Stream.next gensym in
+                     MU (name, h sub ((s, name) :: mapping))
+    | NU (s, sub) -> let name = Stream.next gensym in
+                     NU (name, h sub ((s, name) :: mapping))
+    | NOT sub -> NOT (h sub mapping)
+    | AT (s, sub) -> AT (s, h sub mapping)
+    | OR (sub1, sub2) -> OR ((h sub1 mapping), (h sub2 mapping))
+    | AND (sub1, sub2) -> AND ((h sub1 mapping), (h sub2 mapping))
+    | EQU (sub1, sub2) -> EQU ((h sub1 mapping), (h sub2 mapping))
+    | IMP (sub1, sub2) -> IMP ((h sub1 mapping), (h sub2 mapping))
+    | EX (s, sub) -> EX (s, h sub mapping)
+    | AX (s, sub) -> AX (s, h sub mapping)
+    | ENFORCES (s, sub) -> ENFORCES (s, h sub mapping)
+    | ALLOWS   (s, sub) -> ALLOWS (s, h sub mapping)
+    | MIN (r, s, sub) -> MIN (r, s, h sub mapping)
+    | MAX (r, s, sub) -> MAX (r, s, h sub mapping)
+    | MORETHAN (r, s, sub) -> MORETHAN (r, s, h sub mapping)
+    | MAXEXCEPT (r, s, sub) -> MAXEXCEPT (r, s, h sub mapping)
+    | ATLEASTPROB  (r, sub) -> ATLEASTPROB (r, h sub mapping)
+    | LESSPROBFAIL (r, sub) -> LESSPROBFAIL (r, h sub mapping)
+    | ID sub -> ID (h sub mapping)
+    | NORM (sub1, sub2) -> NORM ((h sub1 mapping), (h sub2 mapping))
+    | NORMN (sub1, sub2) -> NORMN ((h sub1 mapping), (h sub2 mapping))
+    | CHC (sub1, sub2) -> CHC ((h sub1 mapping), (h sub2 mapping))
+    | FUS (b, sub) -> FUS (b, h sub mapping)
+    | other -> other            (* no formula arguments *)
+  in
+  h f []
+
 
 (** Computes the free fixpoint variables occurring in a formula *)
 let rec freeVariables f =
@@ -2264,4 +2296,33 @@ let checkClosed f = match freeVariables f with
   | [] -> ()
   | frees -> raise (CoAlgException (Printf.sprintf "%s is not closed because the variables '%s' occur freely" (string_of_formula f) (List.fold_right (fun el accu -> el ^ " " ^ accu) (List.tl frees) (List.hd frees))))
 
+let convertToMu formula =
+  let name = Stream.next gensym in
+  let helper formula =
+    match formula with
+    | AF f1 ->
+       MU (name, (OR (f1, (const_ax (VAR name)))))
+    | EF f1 ->
+       MU (name, (OR (f1, (const_ex (VAR name)))))
+    | AG f1 ->
+       NU (name, (AND (f1, (const_ax (VAR name)))))
+    | EG f1 ->
+       NU (name, (AND (f1, (const_ex (VAR name)))))
+    | AU (f1, f2) ->
+       MU (name, (OR (f2, (AND (f1, (const_ax (VAR name)))))))
+    | EU (f1, f2) ->
+       MU (name, (OR (f2, (AND (f1, (const_ex (VAR name)))))))
+    | AR (f1, f2) ->
+       NU (name, (AND (f2, (OR (f1, (const_ex (VAR name)))))))
+    | ER (f1, f2) ->
+       NU (name, (AND (f2, (OR (f1, (const_ex (VAR name)))))))
+    | AB (f1, f2) ->
+       NOT (MU (name, (OR (f2, (AND ((NOT f1), (const_ex (VAR name))))))))
+    | EB (f1, f2) ->
+       NOT (MU (name, (OR (f2, (AND ((NOT f1), (const_ax (VAR name))))))))
+    | _ -> formula
+  in
+  convert_post helper formula
+
+
 (* vim: set et sw=2 sts=2 ts=8 : *)

lib/src/CoAlgFormula.mli

@@ -97,6 +97,8 @@ val equals: formula -> formula -> bool
 val nnfNeg : formula -> formula
 val nnf : formula -> formula
 
+val uniqueVars : formula -> formula
+
 val simplify : formula -> formula
 
 val dest_ap : formula -> string
@@ -141,14 +143,19 @@ val const_or : formula -> formula -> formula
 val const_and : formula -> formula -> formula
 val const_equ : formula -> formula -> formula
 val const_imp : formula -> formula -> formula
-val const_ex : string -> formula -> formula
-val const_ax : string -> formula -> formula
-val const_min : int -> string -> formula -> formula
-val const_max : int -> string -> formula -> formula
+val const_ex : ?rel:string -> formula -> formula
+val const_ax : ?rel:string -> formula -> formula
+val const_min : int -> ?rel:string -> formula -> formula
+val const_max : int -> ?rel:string -> formula -> formula
 val const_enforces : int list -> formula -> formula
 val const_allows : int list -> formula -> formula
 val const_choice : formula -> formula -> formula
 val const_fusion : bool -> formula -> formula
+val const_morethan : int -> ?rel:string -> formula -> formula
+val const_maxexcept : int -> ?rel:string -> formula -> formula
+
+val const_big_or : formula list -> formula
+val const_big_and : formula list -> formula
 
 type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
 and hcFormula_node =

lib/src/CoAlgReasonerOneStepFun.ml

@@ -259,18 +259,7 @@ let rec propagateUnsat = function
                 coreSetStatus core Unsat;
                 coreDeallocateSolver core;
                 if core == graphGetRoot () then raise (CoAlg_finished false) else ();
-                let prop acc (state, idx) =
-                  let turnsUnsat =
-                    match stateGetStatus state with
-                    | Open
-                    | Expandable ->
-                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
-                    | Unsat
-                    | Sat -> false
-                  in
-                  if turnsUnsat then (UState (state, Some idx))::acc else acc
-                in
-                let tl2 = List.fold_left prop tl (coreGetParents core) in
+                let tl2 = tl in
                 List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
           end
         | UCnstr cset ->

lib/src/CoolParser.ml

@@ -54,7 +54,7 @@ let parse_formula target expr =
      end
 
 
-let postprocess = F.convertToMu
+let postprocess = F.convertToMu >> F.uniqueVars 
 
 let raw_formula_of_string = parse_formula FormulaParser.Incremental.formula
 

lib/src/CoolUtils.ml

@@ -44,6 +44,16 @@ module TList = struct
       | (l::ls) ->
          let tail = combinations ls in
          List.fold_left (fun acc x -> acc @ List.map (fun lst -> x::lst) tail) [] l
+      
+    let range start stop =
+      List.init ((stop - start) + 1) (fun x -> start + x)
+    let rec take i l =
+      match i with
+      | 0 -> []
+      | i -> match l with
+             | [] -> []
+             | h :: t -> h :: take (i - 1) t
+
 end
 
 module TString = struct
@@ -142,11 +152,14 @@ let eval a f = f a
 let id a = a
 let foreach_l a f = List.iter f a
 let (<<) f g x = f(g(x))
+let (>>) f g x = g(f(x))
 let tee f a = f a; a
 let repeat n fct = for _i = 1 to n do fct () done
 let map_fst f (a,b) = (f a, b)
 let map_snd f (a,b) = (a, f b)
 
+let unless cond f arg = if cond then () else ignore (f arg)
+
 exception No_value
 let fromSome optionalvalue =
     match optionalvalue with

lib/src/CoolUtils.mli

@@ -22,12 +22,14 @@ module TList : sig
     val powerset : ('a list) -> ('a list list)
     val prod : ('a list) -> ('b list) -> (('a * 'b) list)
     val empty : ('a list) -> bool
+    val take : int -> 'a list -> 'a list
 
     (** Compute possible combinations of the sublists.
 
         [combinations [[1;2];[3;4]] = [[1;3];[1;4];[2;3];[2;4]]]
      *)
     val combinations : 'a list list -> 'a list list
+    val range: int -> int -> int list
 end
 
 (** Additional utility functions for the String module  *)
@@ -88,10 +90,13 @@ val id : 'a -> 'a
 val foreach_l : ('a list) -> ('a -> unit) -> unit
 val repeat : int -> (unit -> unit) -> unit
 val (<<) : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
+val (>>) : ('a -> 'b) -> ('b ->'c) -> ('a -> 'c)
 val tee : ('a -> unit) -> 'a -> 'a
 val map_fst : ('a -> 'c) -> 'a * 'b -> 'c * 'b
 val map_snd : ('b -> 'c) -> 'a * 'b -> 'a * 'c
 
+val unless : bool -> ('a -> 'b) -> 'a -> unit
+
 exception No_value