Commit e5426cbb authored by Thorsten Wißmann's avatar Thorsten Wißmann
Browse files

Make insertRule more disjunctive-aware

parent b856538d
...@@ -538,14 +538,17 @@ let insertRule state dep (chldrn: (sort * bset) list junction) : bool option = ...@@ -538,14 +538,17 @@ let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
in in
junctionEvalBoolOption (junc (List.map child2satState children)) junctionEvalBoolOption (junc (List.map child2satState children))
in in
let isUnsat = (satStateChildren = Some false) in
(* find out satisfiability *) (* find out satisfiability *)
let idx = stateAddRule state dep (List.rev children) in let idx = stateAddRule state dep (List.rev children) in
List.iter (fun c -> coreAddParent c state idx) children; List.iter (fun c -> coreAddParent c state idx) children;
if isUnsat then begin match satStateChildren with
propagateUnsat [UState (state, Some idx)]; | Some false -> (* definitely unsat *)
Some false propagateUnsat [UState (state, Some idx)];
end else None Some false
| Some true ->
(* TODO: propagateSat ? *)
Some true
| None -> None
(* tells whether it is satisfiable: (* tells whether it is satisfiable:
Some true -> surely satisfiable Some true -> surely satisfiable
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment