Hi Christine:

for my talk in Nantes on Tuesday, I would like to use
the perobject version of the CNF formula reduction

Please program the enclosed design using Ahmed's implementation
and send it to me this afternoon.

-- Karl

Formula = clauses: List(Clause) 
  perobject sats: int 
  perobject unsats: int
  perobject newClauses: List(Clause).
Clause = literals: List(Literal) 
  perobject newLiterals: List(Literal).
Literal : Pos | Neg common Variable.
Pos = . Neg = .
Variable = v: int.


void after (Literal l2) { reduce(l1,l2);}
  reduce(l1, l2)
  reduce(Pos(v), Pos(v)) = true: sats++
  reduce(Neg(v), Neg(v)) = true: sats++
  reduce(Neg(v), Pos(v)) = false: skip l2
  reduce(Pos(v), Neg(v)) = false: skip l2
  reduce(l1, l2) = l2 if l1 and l2 do not refer to the same variable: 
    add l2 to newLiterals

void after (Clause clause)
  if newLiterals is empty: unsats++ else add clause to newClauses;