- match SFormula.expr f with
- Formula.True | Formula.False -> if b then f else SFormula.not_ f
- | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
- | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
- | Formula.Atom(a) -> begin
- let l, b', q = Atom.node a in
- if q == State.dummy then if b then f else SFormula.not_ f
- else
- if b == b' then begin
- (* a appears positively, either no negation or double negation *)
- if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
- SFormula.atom_ (Atom.make (l, true, q))
- end else begin
+ match Formula.expr f with
+ Boolean.True | Boolean.False -> if b then f else Formula.not_ f
+ | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
+ | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
+ | Boolean.Atom(a, b') -> begin
+ match a.Atom.node with
+ | Move (m, q) ->
+ if b == b' then begin
+ (* a appears positively, either no negation or double negation *)
+ if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
+ Formula.mk_atom (Move(m, q))
+ end else begin