Merge branch 'flatmu'

_oasis

@@ -100,7 +100,7 @@ Executable coalg
   ByteOpt:        -cc g++
   CCOpt: -std=c++98 -x c++
   if flag(static)
-    CCLib:            -static
+    CCLib:            -static -ltinfo -lgpm -lz -ldl -lltdl
 
 Executable "cool-owl"
   CompiledObject:   native
@@ -160,7 +160,7 @@ Executable debugger
   ByteOpt:        -cc g++
   CCOpt: -std=c++98 -x c++
   if flag(static)
-    CCLib:            -static
+    CCLib:            -static -lz -ldl -lltdl
 
 
 

randmu.py

+#!/usr/bin/python3
+#
+# Ideal:
+
+#   Start with a single variable. While formula is still below the
+#   target size, replace a random variable by a random
+#   connective. once the target size has been reached, replace all
+#   unguarded variables by propositional atoms. Replace all remaining
+#   variables by either an allowed fixpoint variable or a
+#   propositional atom
+
+import random
+import string
+import argparse
+import os
+
+
+variables = []
+syntax = 'cool'
+
+
+def _gensym():
+    i = 0
+    while True:
+        i = i + 1
+        yield "G%d" % i
+
+
+gensym = iter(_gensym())
+
+
+
+class Connective:
+    pass
+
+
+
+class Propositional(Connective):
+    pass
+
+
+
+class And(Propositional):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        if syntax == 'tatl':
+            return "((%s) /\ (%s))" % (left, right)
+        else:
+            return "((%s) & (%s))" % (left, right)
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class Or(Propositional):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        if syntax == 'tatl':
+            return "((%s) \/ (%s))" % (left, right)
+        else:
+            return "((%s) | (%s))" % (left, right)
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class Modal(Connective):
+    pass
+
+
+class Box(Modal):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'ctl':
+            return "AX (%s)" % (subformula,)
+        else:
+            return "[] (%s)" % (subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Diamond(Modal):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'ctl':
+            return "EX (%s)" % (subformula,)
+        else:
+            return "<> (%s)" % (subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Fixpoint(Connective):
+    pass
+
+class Mu(Fixpoint):
+    def __init__(self):
+        self._subformula = Variable(self)
+        self._var = next(gensym)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'cool':
+            return "(μ %s . (%s))" % (self._var, subformula)
+        else:
+            return "(mu %s . (%s))" % (self._var, subformula)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        if fixpoint == 'nu':
+            guarded = []
+            unguarded = []
+
+        self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
+
+
+
+class Nu(Fixpoint):
+    def __init__(self):
+        self._subformula = Variable(self)
+        self._var = next(gensym)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'cool':
+            return "(ν %s . (%s))" % (self._var, subformula)
+        else:
+            return "(nu %s . (%s))" % (self._var, subformula)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        if fixpoint == 'mu':
+            guarded = []
+            unguarded = []
+
+        self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
+
+
+
+class CTL(Connective):
+    pass
+
+
+
+class AG(CTL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        return "AG (%s)" % (subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class AF(CTL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        return "AF (%s)" % (subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class EG(CTL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        return "EG (%s)" % (subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class EF(CTL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        return "EF (%s)" % (subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class AU(CTL):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        return "A((%s) U (%s))" % (left, right)
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class AR(CTL):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        return "A((%s) R (%s))" % (left, right)
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class EU(CTL):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        return "E((%s) U (%s))" % (left, right)
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class ER(CTL):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        return "E((%s) R (%s))" % (left, right)
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class ATL:
+    def coalition(self):
+        if not hasattr(self, '_coalition'):
+            self._coalition = []
+            while len(self._coalition) == 0:
+                self._coalition = []
+                for i in range(1, 6):
+                    if random.getrandbits(1) == 1:
+                        self._coalition.append(str(i))
+
+        if syntax == 'tatl':
+            return ",".join(self._coalition)
+        else:
+            return " ".join(self._coalition)
+
+
+
+class Next(ATL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'tatl':
+            return "<<%s>>X(%s)" % (self.coalition(), subformula,)
+        else:
+            return "[{%s}](%s)" % (self.coalition(), subformula,)
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Always(ATL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'tatl':
+            return "<<%s>>G(%s)" % (self.coalition(), subformula,)
+        else:
+            return "(ν X . ((%s) & [{%s}]X))" % (subformula,self.coalition())
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Eventually(ATL):
+    def __init__(self):
+        self._subformula = Variable(self)
+
+
+    def __str__(self):
+        subformula = str(self._subformula)
+        if syntax == 'tatl':
+            return "<<%s>>F(%s)" % (self.coalition(), subformula,)
+        else:
+            return "(μ X . ((%s) | [{%s}]X))" % (subformula, self.coalition())
+
+
+    def replace(self, what, withw):
+        assert self._subformula == what
+        self._subformula = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Until(ATL):
+    def __init__(self):
+        self._left = Variable(self)
+        self._right = Variable(self)
+
+
+    def __str__(self):
+        left = str(self._left)
+        right = str(self._right)
+        if syntax == 'tatl':
+            return "<<%s>>((%s) U (%s))" % (self.coalition(),left, right)
+        else:
+            return "(μ X . ((%s) | ((%s) & [{%s}]X)))" % (right,left,self.coalition())
+
+
+    def replace(self, what, withw):
+        if what == self._left:
+            self._left = withw
+        else:
+            assert self._right == what
+            self._right = withw
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+connectives = []
+
+
+class Variable:
+    def __init__(self, parent):
+        self._parent = parent
+        variables.append(self)
+
+
+    def __str__(self):
+        return "(undecided)"
+
+
+    def replace(self):
+        assert self._parent != None
+        replacement = random.choice(connectives)()
+        variables.remove(self)
+        self._parent.replace(self, replacement)
+
+
+    def finalize(self, atoms, guarded, unguarded, fixpoint):
+        choice = random.choice(guarded + atoms)
+        if choice in atoms:
+            choice = random.choice([choice, "~%s" % choice])
+
+        variables.remove(self)
+        self._parent.replace(self, choice)
+
+
+
+def main(args):
+    global connectives
+    if args.logic == 'afmu':
+        connectives = [And, And, Or, Or, Box, Diamond, Mu, Nu]
+        os.makedirs(os.path.join(args.destdir, 'cool'))
+        os.makedirs(os.path.join(args.destdir, 'mlsolver'))
+
+    elif args.logic == 'CTL':
+        connectives = [And, And, Or, Or, Box, Diamond, AF, AG, EF, EG, AU, EU]
+        os.makedirs(os.path.join(args.destdir, 'ctl'))
+
+    elif args.logic == 'ATL':
+        connectives = [And, And, Or, Or, Next, Always, Eventually, Until]
+        os.makedirs(os.path.join(args.destdir, 'cool'))
+        os.makedirs(os.path.join(args.destdir, 'tatl'))
+
+    for i in range(0, args.count):
+        global variables
+        global syntax
+        variables = []
+        formula = random.choice(connectives)()
+
+        for _ in range(0, args.constructors):
+            random.choice(variables).replace()
+
+        formula.finalize(list(string.ascii_lowercase[:args.atoms]), [], [], 'none')
+
+        if args.logic == 'afmu':
+            with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
+                syntax = 'cool'
+                f.write(str(formula))
+
+            with open(os.path.join(args.destdir, 'mlsolver', 'random.%04d.mlsolver' % i), 'w') as f:
+                syntax = 'mlsolver'
+                f.write(str(formula))
+
+        elif args.logic == 'CTL':
+            with open(os.path.join(args.destdir, 'ctl', 'random.%04d.ctl' % i), 'w') as f:
+                syntax = 'ctl'
+                f.write(str(formula))
+
+        elif args.logic == 'ATL':
+            with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
+                syntax = 'cool'
+                f.write(str(formula))
+
+            with open(os.path.join(args.destdir, 'tatl', 'random.%04d.tatl' % i), 'w') as f:
+                syntax = 'tatl'
+                f.write(str(formula))
+
+    print(args.destdir)
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description="Generator for random μ-Calculus-Formulas")
+    parser.add_argument('--atoms', type=int, required=True,
+                        help="Number of propositional arguments to use")
+    parser.add_argument('--constructors', type=int, required=True,
+                        help="Number of connectives to build")
+    parser.add_argument('--count', type=int, required=True,
+                        help="Number of formulas to generate")
+    parser.add_argument('--destdir', type=str, required=True,
+                        help="Directory to place created formulas in")
+    parser.add_argument('--logic', choices=['CTL', 'ATL', 'afmu'], required=True)
+
+    args = parser.parse_args()
+
+    main(args)

src/.dir-locals.el

+((nil
+  (indent-tabs-mode . nil)))

src/coalg/coalg.ml

@@ -46,9 +46,10 @@ let _ =
 
 let printUsage () =
   print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
-  print_endline "       <task> in { sat print nnf prov (is »not.(sat ¬f)«) }";
+  print_endline "       <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) }";
   print_endline "       <functor> in { MultiModalK (or equivalently K)";
   print_endline "                      MultiModalKD (or equivalently KD)";
+  print_endline "                      Monotone";
   print_endline "                      CoalitionLogic (or equivalently CL)";
   print_endline "                      Const id1 ... idn (or equivalently Constant id1 ... idn)";
   print_endline "                      Id (or equivalently Identity)";
@@ -167,6 +168,28 @@ let choiceNNF () =
       done
     with End_of_file -> ()
 
+let choiceGraph () =
+  choiceSat ();
+  print_endline "digraph reasonerstate {";
+  CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
+  CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
+  print_endline "}"
+
+let choiceVerify () =
+    try
+      while true do
+        let input = read_line () in
+        if not (GenAndComp.isEmptyString input) then
+          let f = CoAlgFormula.importFormula input in
+          let str = CoAlgFormula.exportFormula f in
+          incr counter;
+          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
+          flush stdout;
+          CoAlgFormula.verifyFormula f;
+        else ()
+      done
+    with End_of_file -> ()
+
 let rec parseFlags arr offs : unit =
     let offs = ref (offs) in
     let getParam () =
@@ -198,6 +221,6 @@ let _ =
     | "prov" -> choiceProvable ()
     | "print" -> choicePrint ()
     | "nnf" -> choiceNNF ()
+    | "verify" -> choiceVerify ()
+    | "graph" -> choiceGraph ()
     | _ -> printUsage ()
-
-

src/debugger/debugger.ml

@@ -69,6 +69,12 @@ let listCores args =
 let listStates args =
     CM.graphIterStates (fun state -> print_endline (CM.stateToString state))
 
+let exportGraph args =
+  print_endline "digraph reasonerstate {";
+  CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
+  CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
+  print_endline "}"
+
 let showNode = function
     | (n::_) ->
         let n = int_of_string n in
@@ -101,11 +107,10 @@ let _ =
         Repl.bind "status" (fun _ -> printStatus ()) "Prints reasoning status" "";
         Repl.bind "lscores" listCores "Lists all cores" "";
         Repl.bind "lsstates" listStates "Lists all states" "";
+        Repl.bind "graphviz" exportGraph "Graphviz source of reasoner state" "";
         Repl.bind "node" showNode "shows details of a node" "usage: node n";
         Repl.exitBinding
       ];
     }
     in
     Repl.start session
-
-

src/lib/CoAlgFormula.mli

@@ -41,6 +41,19 @@ type formula =
   | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
   | CHC of formula * formula
   | FUS of bool * formula
+  | MU of string * formula
+  | NU of string * formula
+  | VAR of string
+  | AF of formula
+  | EF of formula
+  | AG of formula
+  | EG of formula
+  | AU of formula * formula
+  | EU of formula * formula
+  | AR of formula * formula
+  | ER of formula * formula
+  | AB of formula * formula
+  | EB of formula * formula
 
 exception ConversionException of formula
 
@@ -66,6 +79,8 @@ val importFormula : string -> formula
 val importSortedFormula : string -> sortedFormula
 val importQuery : string -> sortedFormula list * sortedFormula
 
+val verifyFormula : formula -> unit
+
 val nnfNeg : formula -> formula
 val nnf : formula -> formula
 
@@ -146,9 +161,14 @@ and hcFormula_node =
   | HCNORMN of hcFormula * hcFormula
   | HCCHC of hcFormula * hcFormula
   | HCFUS of bool * hcFormula
+  | HCMU of string * hcFormula
+  | HCNU of string * hcFormula
+  | HCVAR of string
 
 module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
 
 val hc_formula : HcFormula.t -> formula -> hcFormula
+val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
+val hc_freeIn : string -> hcFormula -> bool
 
 module HcFHt : (Hashtbl.S with type key = hcFormula)

src/lib/CoAlgLogics.mli

@@ -6,4 +6,4 @@
 open CoAlgMisc
 
 
-val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander
+val getExpandingFunctionProducer : functors -> sort -> bset -> bset -> sort list -> stateExpander

src/lib/CoAlgMisc.mli

@@ -12,6 +12,7 @@
 type functors =
   | MultiModalK
   | MultiModalKD
+  | Monotone
   | CoalitionLogic
   | GML
   | PML
@@ -52,6 +53,8 @@ type formulaType =
   | NormnF (* negation normal form of default implication *)
   | ChcF
   | FusF
+  | MuF
+  | NuF
 
 type localFormula
 type bset
@@ -93,7 +96,7 @@ and nodeStatus =
 
 and dependencies = bset list -> bset
 
-and rule = (dependencies * (sort * bset) lazylist)
+and rule = (dependencies * (sort * bset * bset) lazylist)
 
 and 'a lazyliststep =
   | MultipleElements of 'a list
@@ -165,6 +168,7 @@ val queueInsertCnstr : cset -> unit
 val queueGetElement : unit -> queueElement
 val queuePrettyStatus : unit -> string
 
+val setPropagationCounter : int -> unit
 val doNominalPropagation : unit -> bool
 val doSatPropagation : unit -> bool
 
@@ -178,11 +182,11 @@ val graphIterStates : (state -> unit) -> unit
 val graphIterCores : (core -> unit) -> unit
 val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
 val graphClearCnstr : unit -> unit
-val graphFindState : sort -> bset -> state option
-val graphFindCore : sort -> bset -> core option
+val graphFindState : sort -> (bset * bset) -> state option
+val graphFindCore : sort -> (bset * bset) -> core option
 val graphFindCnstr : cset -> constrnt option
-val graphInsertState : sort -> bset -> state -> unit
-val graphInsertCore : sort -> bset -> core -> unit
+val graphInsertState : sort -> (bset * bset) -> state -> unit
+val graphInsertCore : sort -> (bset * bset) -> core -> unit
 val graphInsertCnstr : cset -> constrnt -> unit
 val graphReplaceCnstr : cset -> constrnt -> unit
 val graphSizeState : unit -> int
@@ -210,10 +214,12 @@ val cssIter : (cset -> unit) -> csetSet -> unit
 (*      "Module type" and a specific implementation of state nodes           *)
 (*****************************************************************************)
 
-val stateMake : sort -> bset -> stateExpander -> state
+val stateMake : sort -> bset -> bset -> stateExpander -> state
 val stateGetSort : state -> sort
 val stateGetBs : state -> bset
 val stateSetBs : state -> bset -> unit
+val stateGetDeferral : state -> bset
+val stateSetDeferral : state -> bset -> unit
 val stateGetStatus : state -> nodeStatus
 val stateSetStatus : state -> nodeStatus -> unit
 val stateGetParents : state -> core list
@@ -225,6 +231,7 @@ val stateGetConstraints : state -> csetSet
 val stateSetConstraints : state -> csetSet -> unit
 val stateNextRule : state -> ruleEnumeration
 val stateToString : state -> string
+val stateToDot : state -> string
 val stateGetIdx : state -> int
 
 
@@ -232,24 +239,28 @@ val stateGetIdx : state -> int
 (*      "Module type" and a specific implementation of core nodes            *)
 (*****************************************************************************)
 
-val coreMake : sort -> bset -> Minisat.solver -> fht -> core
+val coreMake : sort -> bset -> bset -> Minisat.solver option -> fht -> core
 val coreGetSort : core -> sort
 val coreGetBs : core -> bset
-val coreSetBs :core -> bset -> unit
+val coreSetBs : core -> bset -> unit
+val coreGetDeferral : core -> bset
+val coreSetDeferral : core -> bset -> unit
 val coreGetStatus : core -> nodeStatus
 val coreSetStatus : core -> nodeStatus -> unit
-val coreGetParents :core -> (state * int) list
+val coreGetParents : core -> (state * int) list
 val coreAddParent : core -> state -> int -> unit
 val coreGetChildren : core -> state list
 val coreAddChild : core -> state -> unit
 val coreGetConstraints : core -> csetSet
 val coreSetConstraints : core -> csetSet -> unit
-val coreGetSolver : core -> Minisat.solver
+val coreGetSolver : core -> Minisat.solver option
+val coreDeallocateSolver : core -> unit
 val coreGetFht : core -> fht
 val coreGetIdx : core -> int
 val coreGetConstraintParents : core -> cset list
 val coreAddConstraintParent : core -> cset -> unit
 val coreToString : core -> string
+val coreToDot : core -> string
 
 
 (*****************************************************************************)
@@ -259,6 +270,8 @@ val coreToString : core -> string
 
 val setEmptyState : unit -> setState
 val setEmptyCore : unit -> setCore
+val setCopyState : setState -> setState
+val setCopyCore : setCore -> setCore
 val setEmptyCnstr : unit -> setCnstr
 val setAddState : setState -> state -> unit
 val setAddCore : setCore -> core -> unit
@@ -272,6 +285,8 @@ val setRemoveCnstr : setCnstr -> cset -> unit
 val setIterState : (state -> unit) -> setState -> unit
 val setIterCore : (core -> unit) -> setCore -> unit
 val setIterCnstr : (cset -> unit) -> setCnstr -> unit
+val setLengthState : setState -> int
+val setLengthCore : setCore -> int
 
 
 (*****************************************************************************)
@@ -303,6 +318,8 @@ val bsetMake : unit -> bset (* a new bset which only contains True *)
 val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
 val bsetAdd : bset -> localFormula -> unit
 val bsetMem : bset -> localFormula -> bool
+val bsetRem : bset -> int -> unit
+val bsetCompare : bset -> bset -> int
 val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
 val bsetIter : (localFormula -> unit) -> bset -> unit
 val bsetFilter : bset -> (localFormula -> bool) -> bset
@@ -331,6 +348,7 @@ val lfGetType : sort -> localFormula -> formulaType
 val lfGetDest1 : sort -> localFormula -> localFormula
 val lfGetDest2 : sort -> localFormula -> localFormula
 val lfGetDest3 : sort -> localFormula -> int
+val lfGetDeferral : sort -> localFormula -> int
 val lfGetDestNum : sort -> localFormula -> int
 val lfGetDestNum2 : sort -> localFormula -> int
 val lfGetDestAg : sort -> localFormula -> int array

src/lib/HashConsing.ml

@@ -208,11 +208,18 @@ module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
           let ndeN = H.negNde nde in
           let hkeyN = realhash ndeN in
           let fmlN = H.toFml ndeN in
-          let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
-          nd.neg <- ndN;
           let idxN = hkeyN mod ds in
-          data.(idxN) <- ndN :: data.(idxN);
-          hc.size <- osize + 2;
+          let bucketN = data.(idxN) in
+          try begin
+            find ndeN bucketN;
+            hc.size <- succ osize;
+          end
+          with Not_found ->
+            let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
+            nd.neg <- ndN;
+            let idxN = hkeyN mod ds in
+            data.(idxN) <- ndN :: data.(idxN);
+            hc.size <- osize + 2
         else hc.size <- succ osize;
         if hc.size > ds lsl 1 then resize hc else ();
         nd

src/testsuite/cool-testsuite.ml

@@ -37,15 +37,15 @@ let k_testcases: satCheck list =
     ; c Unsat "<R> ((<R> C) & (<S> False))"
     ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
     ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
-    ; c Sat   "<R> A & <R> B |- [R] C"
-    ; c Unsat "<R> A & <R> B |- [R] (~A & ~B)"
-    ; c Unsat "<R> A & <R> B |- [R] ~B"
-    ; c Sat   "<R> A & <R> ~A |- [R] B"
-    ; c Unsat "<R> A & <R> ~A & (B => [R] ~A) |- [R] B"
-    ; c Sat   "<R> A & <R> ~A & (B => [R] ~A) & (C => ~D) & (D => ~E) & <R> C & <R> D & <R> E |- True"
-    ; c Unsat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
-    ; c Sat   "(<R> D | <R> E) & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
-    ; c Sat   "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & (D & E => <R> ~(D&E)) |- True"
+    ; c Sat   "<R> a & <R> B |- [R] C"
+    ; c Unsat "<R> a & <R> B |- [R] (~a & ~B)"
+    ; c Unsat "<R> a & <R> B |- [R] ~B"
+    ; c Sat   "<R> a & <R> ~a |- [R] B"
+    ; c Unsat "<R> a & <R> ~a & (B => [R] ~a) |- [R] B"
+    ; c Sat   "<R> a & <R> ~a & (B => [R] ~a) & (C => ~D) & (D => ~e) & <R> C & <R> D & <R> e |- True"
+    ; c Unsat "<R> D & <R> e & ((<R> D & <R> e) => [R] e) & ~(D & e) |- True"
+    ; c Sat   "(<R> D | <R> e) & ((<R> D & <R> e) => [R] e) & ~(D & e) |- True"
+    ; c Sat   "<R> D & <R> e & ((<R> D & <R> e) => [R] e) & (D & e => <R> ~(D&e)) |- True"
     ]