track deferrals across propositional reasoning

src/lib/CoAlgReasoner.ml

@@ -509,6 +509,7 @@ let getNextState core =
      minisat calls.
   *)
   let bs = coreGetBs core in
+  let deferralS = coreGetDeferral core in
   let fht = coreGetFht core in
   let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
   let solver = coreGetSolver core in
@@ -523,6 +524,7 @@ let getNextState core =
        satisfiable.
     *)
     let newbs = bsetMake () in
+    let newdefer = bsetMake () in
     (* if newbs = { l_1, .... l_n }, i.e.
 
             newbs = l_1 /\ ... /\ l_n
@@ -534,7 +536,7 @@ let getNextState core =
 
        By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
     *)
-    let rec mkExclClause f acc =
+    let rec mkExclClause deferral f acc =
       (* f is a formula that is true in the current satisfying assignment *)
       match lfGetType sort f with
       | OrF ->
@@ -543,50 +545,62 @@ let getNextState core =
           let lf1 = fhtMustFind fht f1 in
           (* if the first disjunct f1 is true, then we need to add subformulas
              of f1 to newbs&clause *)
-          if M.literal_status solver lf1 = M.LTRUE then mkExclClause f1 acc
+          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
           else
             (* otherwise f2 must be true *)
             let f2 = lfGetDest2 sort f in
             let lf2 = fhtMustFind fht f2 in
             assert (M.literal_status solver lf2 = M.LTRUE);
-            mkExclClause f2 acc
+            mkExclClause deferral f2 acc
       | AndF ->
           (* if the true f is a conjuction, then both conjunctions must be true *)
           let f1 = lfGetDest1 sort f in
           let lf1 = fhtMustFind fht f1 in
           assert (M.literal_status solver lf1 = M.LTRUE);
-          let acc1 = mkExclClause f1 acc in
+          let acc1 = mkExclClause deferral f1 acc in
           let f2 = lfGetDest2 sort f in
           let lf2 = fhtMustFind fht f2 in
           assert (M.literal_status solver lf2 = M.LTRUE);
-          mkExclClause f2 acc1
+          mkExclClause deferral f2 acc1
       | MuF
       | NuF ->
          let f1 = lfGetDest1 sort f in
-         mkExclClause f1 acc
+         mkExclClause deferral f1 acc
       | _ ->
-          (* if f is a trivial formula or modality, then add it ... *)
-          (* ... to newbs *)
-          bsetAdd newbs f;
-          (* ... and to the new clause *)
-          (M.neg_lit (fhtMustFind fht f))::acc
+         (* if f is a trivial formula or modality, then add it ... *)
+         (* ... to newbs *)
+         bsetAdd newbs f;
+         let defercandidate = lfGetDeferral sort f in
+         (if deferral = defercandidate then
+            bsetAdd newdefer f);
+         (* ... and to the new clause *)
+         (M.neg_lit (fhtMustFind fht f))::acc
     in
-    let clause = bsetFold mkExclClause bs [] in
+    let init_clause f acc =
+      let deferral =
+        if bsetMem deferralS f then
+          lfGetDeferral sort f
+        else
+          (Hashtbl.hash "ε")
+      in
+      mkExclClause deferral f acc
+    in
+    let clause = bsetFold init_clause bs [] in
     let okay = M.add_clause solver clause in
     assert (okay);
-    Some (sort, newbs)
+    Some (sort, newbs, newdefer)
 
-let newState sort bs =
+let newState sort bs defer =
   let (func, sl) = !sortTable.(sort) in
   let producer = CoAlgLogics.getExpandingFunctionProducer func in
   let exp = producer sort bs sl in
-  stateMake sort bs bs exp
+  stateMake sort bs defer exp
 
-let insertState parent sort bs =
+let insertState parent sort bs defer =
   let child =
     match graphFindState sort bs with
     | None ->
-        let s = newState sort bs in
+        let s = newState sort bs defer in
         graphInsertState sort bs s;
         queueInsertState s;
         s
@@ -597,8 +611,8 @@ let insertState parent sort bs =
 
 let expandCore core =
   match getNextState core with
-  | Some (sort, bs) ->
-      insertState core sort bs;
+  | Some (sort, bs, defer) ->
+      insertState core sort bs defer;
       queueInsertCore core
   | None ->
       let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in