(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Normalize :> Normalize =
struct
open Useful;
(* ------------------------------------------------------------------------- *)
(* Constants. *)
(* ------------------------------------------------------------------------- *)
val prefix = "FOFtoCNF";
val skolemPrefix = "skolem" ^ prefix;
val definitionPrefix = "definition" ^ prefix;
(* ------------------------------------------------------------------------- *)
(* Storing huge real numbers as their log. *)
(* ------------------------------------------------------------------------- *)
datatype logReal = LogReal of real;
fun compareLogReal (LogReal logX, LogReal logY) =
Real.compare (logX,logY);
val zeroLogReal = LogReal ~1.0;
val oneLogReal = LogReal 0.0;
local
fun isZero logX = logX < 0.0;
(* Assume logX >= logY >= 0.0 *)
fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
in
fun isZeroLogReal (LogReal logX) = isZero logX;
fun multiplyLogReal (LogReal logX) (LogReal logY) =
if isZero logX orelse isZero logY then zeroLogReal
else LogReal (logX + logY);
fun addLogReal (lx as LogReal logX) (ly as LogReal logY) =
if isZero logX then ly
else if isZero logY then lx
else if logX < logY then LogReal (add logY logX)
else LogReal (add logX logY);
fun withinRelativeLogReal logDelta (LogReal logX) (LogReal logY) =
isZero logX orelse
(not (isZero logY) andalso logX < logY + logDelta);
end;
fun toStringLogReal (LogReal logX) = Real.toString logX;
(* ------------------------------------------------------------------------- *)
(* Counting the clauses that would be generated by conjunctive normal form. *)
(* ------------------------------------------------------------------------- *)
val countLogDelta = 0.01;
datatype count = Count of {positive : logReal, negative : logReal};
fun countCompare (count1,count2) =
let
val Count {positive = p1, negative = _} = count1
and Count {positive = p2, negative = _} = count2
in
compareLogReal (p1,p2)
end;
fun countNegate (Count {positive = p, negative = n}) =
Count {positive = n, negative = p};
fun countLeqish count1 count2 =
let
val Count {positive = p1, negative = _} = count1
and Count {positive = p2, negative = _} = count2
in
withinRelativeLogReal countLogDelta p1 p2
end;
(*MetisDebug
fun countEqualish count1 count2 =
countLeqish count1 count2 andalso
countLeqish count2 count1;
fun countEquivish count1 count2 =
countEqualish count1 count2 andalso
countEqualish (countNegate count1) (countNegate count2);
*)
val countTrue = Count {positive = zeroLogReal, negative = oneLogReal};
val countFalse = Count {positive = oneLogReal, negative = zeroLogReal};
val countLiteral = Count {positive = oneLogReal, negative = oneLogReal};
fun countAnd2 (count1,count2) =
let
val Count {positive = p1, negative = n1} = count1
and Count {positive = p2, negative = n2} = count2
val p = addLogReal p1 p2
and n = multiplyLogReal n1 n2
in
Count {positive = p, negative = n}
end;
fun countOr2 (count1,count2) =
let
val Count {positive = p1, negative = n1} = count1
and Count {positive = p2, negative = n2} = count2
val p = multiplyLogReal p1 p2
and n = addLogReal n1 n2
in
Count {positive = p, negative = n}
end;
(* Whether countXor2 is associative or not is an open question. *)
fun countXor2 (count1,count2) =
let
val Count {positive = p1, negative = n1} = count1
and Count {positive = p2, negative = n2} = count2
val p = addLogReal (multiplyLogReal p1 p2) (multiplyLogReal n1 n2)
and n = addLogReal (multiplyLogReal p1 n2) (multiplyLogReal n1 p2)
in
Count {positive = p, negative = n}
end;
fun countDefinition body_count = countXor2 (countLiteral,body_count);
val countToString =
let
val rToS = toStringLogReal
in
fn Count {positive = p, negative = n} =>
"(+" ^ rToS p ^ ",-" ^ rToS n ^ ")"
end;
val ppCount = Print.ppMap countToString Print.ppString;
(* ------------------------------------------------------------------------- *)
(* A type of normalized formula. *)
(* ------------------------------------------------------------------------- *)
datatype formula =
True
| False
| Literal of NameSet.set * Literal.literal
| And of NameSet.set * count * formula Set.set
| Or of NameSet.set * count * formula Set.set
| Xor of NameSet.set * count * bool * formula Set.set
| Exists of NameSet.set * count * NameSet.set * formula
| Forall of NameSet.set * count * NameSet.set * formula;
fun compare f1_f2 =
if Portable.pointerEqual f1_f2 then EQUAL
else
case f1_f2 of
(True,True) => EQUAL
| (True,_) => LESS
| (_,True) => GREATER
| (False,False) => EQUAL
| (False,_) => LESS
| (_,False) => GREATER
| (Literal (_,l1), Literal (_,l2)) => Literal.compare (l1,l2)
| (Literal _, _) => LESS
| (_, Literal _) => GREATER
| (And (_,_,s1), And (_,_,s2)) => Set.compare (s1,s2)
| (And _, _) => LESS
| (_, And _) => GREATER
| (Or (_,_,s1), Or (_,_,s2)) => Set.compare (s1,s2)
| (Or _, _) => LESS
| (_, Or _) => GREATER
| (Xor (_,_,p1,s1), Xor (_,_,p2,s2)) =>
(case boolCompare (p1,p2) of
LESS => LESS
| EQUAL => Set.compare (s1,s2)
| GREATER => GREATER)
| (Xor _, _) => LESS
| (_, Xor _) => GREATER
| (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) =>
(case NameSet.compare (n1,n2) of
LESS => LESS
| EQUAL => compare (f1,f2)
| GREATER => GREATER)
| (Exists _, _) => LESS
| (_, Exists _) => GREATER
| (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) =>
(case NameSet.compare (n1,n2) of
LESS => LESS
| EQUAL => compare (f1,f2)
| GREATER => GREATER);
val empty = Set.empty compare;
val singleton = Set.singleton compare;
local
fun neg True = False
| neg False = True
| neg (Literal (fv,lit)) = Literal (fv, Literal.negate lit)
| neg (And (fv,c,s)) = Or (fv, countNegate c, neg_set s)
| neg (Or (fv,c,s)) = And (fv, countNegate c, neg_set s)
| neg (Xor (fv,c,p,s)) = Xor (fv, c, not p, s)
| neg (Exists (fv,c,n,f)) = Forall (fv, countNegate c, n, neg f)
| neg (Forall (fv,c,n,f)) = Exists (fv, countNegate c, n, neg f)
and neg_set s = Set.foldl neg_elt empty s
and neg_elt (f,s) = Set.add s (neg f);
in
val negate = neg;
val negateSet = neg_set;
end;
fun negateMember x s = Set.member (negate x) s;
local
fun member s x = negateMember x s;
in
fun negateDisjoint s1 s2 =
if Set.size s1 < Set.size s2 then not (Set.exists (member s2) s1)
else not (Set.exists (member s1) s2);
end;
fun polarity True = true
| polarity False = false
| polarity (Literal (_,(pol,_))) = not pol
| polarity (And _) = true
| polarity (Or _) = false
| polarity (Xor (_,_,pol,_)) = pol
| polarity (Exists _) = true
| polarity (Forall _) = false;
(*MetisDebug
val polarity = fn f =>
let
val res1 = compare (f, negate f) = LESS
val res2 = polarity f
val _ = res1 = res2 orelse raise Bug "polarity"
in
res2
end;
*)
fun applyPolarity true fm = fm
| applyPolarity false fm = negate fm;
fun freeVars True = NameSet.empty
| freeVars False = NameSet.empty
| freeVars (Literal (fv,_)) = fv
| freeVars (And (fv,_,_)) = fv
| freeVars (Or (fv,_,_)) = fv
| freeVars (Xor (fv,_,_,_)) = fv
| freeVars (Exists (fv,_,_,_)) = fv
| freeVars (Forall (fv,_,_,_)) = fv;
fun freeIn v fm = NameSet.member v (freeVars fm);
val freeVarsSet =
let
fun free (fm,acc) = NameSet.union (freeVars fm) acc
in
Set.foldl free NameSet.empty
end;
fun count True = countTrue
| count False = countFalse
| count (Literal _) = countLiteral
| count (And (_,c,_)) = c
| count (Or (_,c,_)) = c
| count (Xor (_,c,p,_)) = if p then c else countNegate c
| count (Exists (_,c,_,_)) = c
| count (Forall (_,c,_,_)) = c;
val countAndSet =
let
fun countAnd (fm,c) = countAnd2 (count fm, c)
in
Set.foldl countAnd countTrue
end;
val countOrSet =
let
fun countOr (fm,c) = countOr2 (count fm, c)
in
Set.foldl countOr countFalse
end;
val countXorSet =
let
fun countXor (fm,c) = countXor2 (count fm, c)
in
Set.foldl countXor countFalse
end;
fun And2 (False,_) = False
| And2 (_,False) = False
| And2 (True,f2) = f2
| And2 (f1,True) = f1
| And2 (f1,f2) =
let
val (fv1,c1,s1) =
case f1 of
And fv_c_s => fv_c_s
| _ => (freeVars f1, count f1, singleton f1)
and (fv2,c2,s2) =
case f2 of
And fv_c_s => fv_c_s
| _ => (freeVars f2, count f2, singleton f2)
in
if not (negateDisjoint s1 s2) then False
else
let
val s = Set.union s1 s2
in
case Set.size s of
0 => True
| 1 => Set.pick s
| n =>
if n = Set.size s1 + Set.size s2 then
And (NameSet.union fv1 fv2, countAnd2 (c1,c2), s)
else
And (freeVarsSet s, countAndSet s, s)
end
end;
val AndList = List.foldl And2 True;
val AndSet = Set.foldl And2 True;
fun Or2 (True,_) = True
| Or2 (_,True) = True
| Or2 (False,f2) = f2
| Or2 (f1,False) = f1
| Or2 (f1,f2) =
let
val (fv1,c1,s1) =
case f1 of
Or fv_c_s => fv_c_s
| _ => (freeVars f1, count f1, singleton f1)
and (fv2,c2,s2) =
case f2 of
Or fv_c_s => fv_c_s
| _ => (freeVars f2, count f2, singleton f2)
in
if not (negateDisjoint s1 s2) then True
else
let
val s = Set.union s1 s2
in
case Set.size s of
0 => False
| 1 => Set.pick s
| n =>
if n = Set.size s1 + Set.size s2 then
Or (NameSet.union fv1 fv2, countOr2 (c1,c2), s)
else
Or (freeVarsSet s, countOrSet s, s)
end
end;
val OrList = List.foldl Or2 False;
val OrSet = Set.foldl Or2 False;
fun pushOr2 (f1,f2) =
let
val s1 = case f1 of And (_,_,s) => s | _ => singleton f1
and s2 = case f2 of And (_,_,s) => s | _ => singleton f2
fun g x1 (x2,acc) = And2 (Or2 (x1,x2), acc)
fun f (x1,acc) = Set.foldl (g x1) acc s2
in
Set.foldl f True s1
end;
val pushOrList = List.foldl pushOr2 False;
local
fun normalize fm =
let
val p = polarity fm
val fm = applyPolarity p fm
in
(freeVars fm, count fm, p, singleton fm)
end;
in
fun Xor2 (False,f2) = f2
| Xor2 (f1,False) = f1
| Xor2 (True,f2) = negate f2
| Xor2 (f1,True) = negate f1
| Xor2 (f1,f2) =
let
val (fv1,c1,p1,s1) = case f1 of Xor x => x | _ => normalize f1
and (fv2,c2,p2,s2) = case f2 of Xor x => x | _ => normalize f2
val s = Set.symmetricDifference s1 s2
val fm =
case Set.size s of
0 => False
| 1 => Set.pick s
| n =>
if n = Set.size s1 + Set.size s2 then
Xor (NameSet.union fv1 fv2, countXor2 (c1,c2), true, s)
else
Xor (freeVarsSet s, countXorSet s, true, s)
val p = p1 = p2
in
applyPolarity p fm
end;
end;
val XorList = List.foldl Xor2 False;
val XorSet = Set.foldl Xor2 False;
fun XorPolarityList (p,l) = applyPolarity p (XorList l);
fun XorPolaritySet (p,s) = applyPolarity p (XorSet s);
fun destXor (Xor (_,_,p,s)) =
let
val (fm1,s) = Set.deletePick s
val fm2 =
if Set.size s = 1 then applyPolarity p (Set.pick s)
else Xor (freeVarsSet s, countXorSet s, p, s)
in
(fm1,fm2)
end
| destXor _ = raise Error "destXor";
fun pushXor fm =
let
val (f1,f2) = destXor fm
val f1' = negate f1
and f2' = negate f2
in
And2 (Or2 (f1,f2), Or2 (f1',f2'))
end;
fun Exists1 (v,init_fm) =
let
fun exists_gen fm =
let
val fv = NameSet.delete (freeVars fm) v
val c = count fm
val n = NameSet.singleton v
in
Exists (fv,c,n,fm)
end
fun exists fm = if freeIn v fm then exists_free fm else fm
and exists_free (Or (_,_,s)) = OrList (Set.transform exists s)
| exists_free (fm as And (_,_,s)) =
let
val sv = Set.filter (freeIn v) s
in
if Set.size sv <> 1 then exists_gen fm
else
let
val fm = Set.pick sv
val s = Set.delete s fm
in
And2 (exists_free fm, AndSet s)
end
end
| exists_free (Exists (fv,c,n,f)) =
Exists (NameSet.delete fv v, c, NameSet.add n v, f)
| exists_free fm = exists_gen fm
in
exists init_fm
end;
fun ExistsList (vs,f) = List.foldl Exists1 f vs;
fun ExistsSet (n,f) = NameSet.foldl Exists1 f n;
fun Forall1 (v,init_fm) =
let
fun forall_gen fm =
let
val fv = NameSet.delete (freeVars fm) v
val c = count fm
val n = NameSet.singleton v
in
Forall (fv,c,n,fm)
end
fun forall fm = if freeIn v fm then forall_free fm else fm
and forall_free (And (_,_,s)) = AndList (Set.transform forall s)
| forall_free (fm as Or (_,_,s)) =
let
val sv = Set.filter (freeIn v) s
in
if Set.size sv <> 1 then forall_gen fm
else
let
val fm = Set.pick sv
val s = Set.delete s fm
in
Or2 (forall_free fm, OrSet s)
end
end
| forall_free (Forall (fv,c,n,f)) =
Forall (NameSet.delete fv v, c, NameSet.add n v, f)
| forall_free fm = forall_gen fm
in
forall init_fm
end;
fun ForallList (vs,f) = List.foldl Forall1 f vs;
fun ForallSet (n,f) = NameSet.foldl Forall1 f n;
fun generalize f = ForallSet (freeVars f, f);
local
fun subst_fv fvSub =
let
fun add_fv (v,s) = NameSet.union (NameMap.get fvSub v) s
in
NameSet.foldl add_fv NameSet.empty
end;
fun subst_rename (v,(avoid,bv,sub,domain,fvSub)) =
let
val v' = Term.variantPrime avoid v
val avoid = NameSet.add avoid v'
val bv = NameSet.add bv v'
val sub = Subst.insert sub (v, Term.Var v')
val domain = NameSet.add domain v
val fvSub = NameMap.insert fvSub (v, NameSet.singleton v')
in
(avoid,bv,sub,domain,fvSub)
end;
fun subst_check sub domain fvSub fm =
let
val domain = NameSet.intersect domain (freeVars fm)
in
if NameSet.null domain then fm
else subst_domain sub domain fvSub fm
end
and subst_domain sub domain fvSub fm =
case fm of
Literal (fv,lit) =>
let
val fv = NameSet.difference fv domain
val fv = NameSet.union fv (subst_fv fvSub domain)
val lit = Literal.subst sub lit
in
Literal (fv,lit)
end
| And (_,_,s) =>
AndList (Set.transform (subst_check sub domain fvSub) s)
| Or (_,_,s) =>
OrList (Set.transform (subst_check sub domain fvSub) s)
| Xor (_,_,p,s) =>
XorPolarityList (p, Set.transform (subst_check sub domain fvSub) s)
| Exists fv_c_n_f => subst_quant Exists sub domain fvSub fv_c_n_f
| Forall fv_c_n_f => subst_quant Forall sub domain fvSub fv_c_n_f
| _ => raise Bug "subst_domain"
and subst_quant quant sub domain fvSub (fv,c,bv,fm) =
let
val sub_fv = subst_fv fvSub domain
val fv = NameSet.union sub_fv (NameSet.difference fv domain)
val captured = NameSet.intersect bv sub_fv
val bv = NameSet.difference bv captured
val avoid = NameSet.union fv bv
val (_,bv,sub,domain,fvSub) =
NameSet.foldl subst_rename (avoid,bv,sub,domain,fvSub) captured
val fm = subst_domain sub domain fvSub fm
in
quant (fv,c,bv,fm)
end;
in
fun subst sub =
let
fun mk_dom (v,tm,(d,fv)) =
(NameSet.add d v, NameMap.insert fv (v, Term.freeVars tm))
val domain_fvSub = (NameSet.empty, NameMap.new ())
val (domain,fvSub) = Subst.foldl mk_dom domain_fvSub sub
in
subst_check sub domain fvSub
end;
end;
fun fromFormula fm =
case fm of
Formula.True => True
| Formula.False => False
| Formula.Atom atm => Literal (Atom.freeVars atm, (true,atm))
| Formula.Not p => negateFromFormula p
| Formula.And (p,q) => And2 (fromFormula p, fromFormula q)
| Formula.Or (p,q) => Or2 (fromFormula p, fromFormula q)
| Formula.Imp (p,q) => Or2 (negateFromFormula p, fromFormula q)
| Formula.Iff (p,q) => Xor2 (negateFromFormula p, fromFormula q)
| Formula.Forall (v,p) => Forall1 (v, fromFormula p)
| Formula.Exists (v,p) => Exists1 (v, fromFormula p)
and negateFromFormula fm =
case fm of
Formula.True => False
| Formula.False => True
| Formula.Atom atm => Literal (Atom.freeVars atm, (false,atm))
| Formula.Not p => fromFormula p
| Formula.And (p,q) => Or2 (negateFromFormula p, negateFromFormula q)
| Formula.Or (p,q) => And2 (negateFromFormula p, negateFromFormula q)
| Formula.Imp (p,q) => And2 (fromFormula p, negateFromFormula q)
| Formula.Iff (p,q) => Xor2 (fromFormula p, fromFormula q)
| Formula.Forall (v,p) => Exists1 (v, negateFromFormula p)
| Formula.Exists (v,p) => Forall1 (v, negateFromFormula p);
local
fun lastElt (s : formula Set.set) =
case Set.findr (K true) s of
NONE => raise Bug "lastElt: empty set"
| SOME fm => fm;
fun negateLastElt s =
let
val fm = lastElt s
in
Set.add (Set.delete s fm) (negate fm)
end;
fun form fm =
case fm of
True => Formula.True
| False => Formula.False
| Literal (_,lit) => Literal.toFormula lit
| And (_,_,s) => Formula.listMkConj (Set.transform form s)
| Or (_,_,s) => Formula.listMkDisj (Set.transform form s)
| Xor (_,_,p,s) =>
let
val s = if p then negateLastElt s else s
in
Formula.listMkEquiv (Set.transform form s)
end
| Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f)
| Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f);
in
val toFormula = form;
end;
fun toLiteral (Literal (_,lit)) = lit
| toLiteral _ = raise Error "Normalize.toLiteral";
local
fun addLiteral (l,s) = LiteralSet.add s (toLiteral l);
in
fun toClause False = LiteralSet.empty
| toClause (Or (_,_,s)) = Set.foldl addLiteral LiteralSet.empty s
| toClause l = LiteralSet.singleton (toLiteral l);
end;
val pp = Print.ppMap toFormula Formula.pp;
val toString = Print.toString pp;
(* ------------------------------------------------------------------------- *)
(* Negation normal form. *)
(* ------------------------------------------------------------------------- *)
fun nnf fm = toFormula (fromFormula fm);
(* ------------------------------------------------------------------------- *)
(* Basic conjunctive normal form. *)
(* ------------------------------------------------------------------------- *)
val newSkolemFunction =
let
val counter : int StringMap.map ref = ref (StringMap.new ())
in
fn n =>
let
val ref m = counter
val s = Name.toString n
val i = Option.getOpt (StringMap.peek m s, 0)
val () = counter := StringMap.insert m (s, i + 1)
val i = if i = 0 then "" else "_" ^ Int.toString i
val s = skolemPrefix ^ "_" ^ s ^ i
in
Name.fromString s
end
end;
fun skolemize fv bv fm =
let
val fv = NameSet.transform Term.Var fv
fun mk (v,s) = Subst.insert s (v, Term.Fn (newSkolemFunction v, fv))
in
subst (NameSet.foldl mk Subst.empty bv) fm
end;
local
fun rename avoid fv bv fm =
let
val captured = NameSet.intersect avoid bv
in
if NameSet.null captured then fm
else
let
fun ren (v,(a,s)) =
let
val v' = Term.variantPrime a v
in
(NameSet.add a v', Subst.insert s (v, Term.Var v'))
end
val avoid = NameSet.union (NameSet.union avoid fv) bv
val (_,sub) = NameSet.foldl ren (avoid,Subst.empty) captured
in
subst sub fm
end
end;
fun cnfFm avoid fm =
(*MetisTrace5
let
val fm' = cnfFm' avoid fm
val () = Print.trace pp "Normalize.cnfFm: fm" fm
val () = Print.trace pp "Normalize.cnfFm: fm'" fm'
in
fm'
end
and cnfFm' avoid fm =
*)
case fm of
True => True
| False => False
| Literal _ => fm
| And (_,_,s) => AndList (Set.transform (cnfFm avoid) s)
| Or (fv,_,s) =>
let
val avoid = NameSet.union avoid fv
val (fms,_) = Set.foldl cnfOr ([],avoid) s
in
pushOrList fms
end
| Xor _ => cnfFm avoid (pushXor fm)
| Exists (fv,_,n,f) => cnfFm avoid (skolemize fv n f)
| Forall (fv,_,n,f) => cnfFm avoid (rename avoid fv n f)
and cnfOr (fm,(fms,avoid)) =
let
val fm = cnfFm avoid fm
val fms = fm :: fms
val avoid = NameSet.union avoid (freeVars fm)
in
(fms,avoid)
end;
in
val basicCnf = cnfFm NameSet.empty;
end;
(* ------------------------------------------------------------------------- *)
(* Finding the formula definition that minimizes the number of clauses. *)
(* ------------------------------------------------------------------------- *)
local
type best = count * formula option;
fun minBreak countClauses fm best =
case fm of
True => best
| False => best
| Literal _ => best
| And (_,_,s) =>
minBreakSet countClauses countAnd2 countTrue AndSet s best
| Or (_,_,s) =>
minBreakSet countClauses countOr2 countFalse OrSet s best
| Xor (_,_,_,s) =>
minBreakSet countClauses countXor2 countFalse XorSet s best
| Exists (_,_,_,f) => minBreak countClauses f best
| Forall (_,_,_,f) => minBreak countClauses f best
and minBreakSet countClauses count2 count0 mkSet fmSet best =
let
fun cumulatives fms =
let
fun fwd (fm,(c1,s1,l)) =
let
val c1' = count2 (count fm, c1)
and s1' = Set.add s1 fm
in
(c1', s1', (c1,s1,fm) :: l)
end
fun bwd ((c1,s1,fm),(c2,s2,l)) =
let
val c2' = count2 (count fm, c2)
and s2' = Set.add s2 fm
in
(c2', s2', (c1,s1,fm,c2,s2) :: l)
end
val (c1,_,fms) = foldl fwd (count0,empty,[]) fms
val (c2,_,fms) = foldl bwd (count0,empty,[]) fms
(*MetisDebug
val _ = countEquivish c1 c2 orelse
raise Bug ("cumulativeCounts: c1 = " ^ countToString c1 ^
", c2 = " ^ countToString c2)
*)
in
fms
end
fun breakSing ((c1,_,fm,c2,_),best) =
let
val cFms = count2 (c1,c2)
fun countCls cFm = countClauses (count2 (cFms,cFm))
in
minBreak countCls fm best
end
val breakSet1 =
let
fun break c1 s1 fm c2 (best as (bcl,_)) =
if Set.null s1 then best
else
let
val cDef = countDefinition (countXor2 (c1, count fm))
val cFm = count2 (countLiteral,c2)
val cl = countAnd2 (cDef, countClauses cFm)
val noBetter = countLeqish bcl cl
in
if noBetter then best
else (cl, SOME (mkSet (Set.add s1 fm)))
end
in
fn ((c1,s1,fm,c2,s2),best) =>
break c1 s1 fm c2 (break c2 s2 fm c1 best)
end
val fms = Set.toList fmSet
fun breakSet measure best =
let
val fms = sortMap (measure o count) countCompare fms
in
foldl breakSet1 best (cumulatives fms)
end
val best = foldl breakSing best (cumulatives fms)
val best = breakSet I best
val best = breakSet countNegate best
val best = breakSet countClauses best
in
best
end
in
fun minimumDefinition fm =
let
val cl = count fm
in
if countLeqish cl countLiteral then NONE
else
let
val (cl',def) = minBreak I fm (cl,NONE)
(*MetisTrace1
val () =
case def of
NONE => ()
| SOME d =>
Print.trace pp ("defCNF: before = " ^ countToString cl ^
", after = " ^ countToString cl' ^
", definition") d
*)
in
def
end
end;
end;
(* ------------------------------------------------------------------------- *)
(* Conjunctive normal form derivations. *)
(* ------------------------------------------------------------------------- *)
datatype thm = Thm of formula * inference
and inference =
Axiom of Formula.formula
| Definition of string * Formula.formula
| Simplify of thm * thm list
| Conjunct of thm
| Specialize of thm
| Skolemize of thm
| Clausify of thm;
fun parentsInference inf =
case inf of
Axiom _ => []
| Definition _ => []
| Simplify (th,ths) => th :: ths
| Conjunct th => [th]
| Specialize th => [th]
| Skolemize th => [th]
| Clausify th => [th];
fun compareThm (Thm (fm1,_), Thm (fm2,_)) = compare (fm1,fm2);
fun parentsThm (Thm (_,inf)) = parentsInference inf;
fun mkAxiom fm = Thm (fromFormula fm, Axiom fm);
fun destThm (Thm (fm,inf)) = (toFormula fm, inf);
local
val emptyProved : (thm,Formula.formula) Map.map = Map.new compareThm;
fun isProved proved th = Map.inDomain th proved;
fun isUnproved proved th = not (isProved proved th);
fun lookupProved proved th =
case Map.peek proved th of
SOME fm => fm
| NONE => raise Bug "Normalize.lookupProved";
fun prove acc proved ths =
case ths of
[] => rev acc
| th :: ths' =>
if isProved proved th then prove acc proved ths'
else
let
val pars = parentsThm th
val deps = List.filter (isUnproved proved) pars
in
if null deps then
let
val (fm,inf) = destThm th
val fms = map (lookupProved proved) pars
val acc = (fm,inf,fms) :: acc
val proved = Map.insert proved (th,fm)
in
prove acc proved ths'
end
else
let
val ths = deps @ ths
in
prove acc proved ths
end
end;
in
val proveThms = prove [] emptyProved;
end;
fun toStringInference inf =
case inf of
Axiom _ => "Axiom"
| Definition _ => "Definition"
| Simplify _ => "Simplify"
| Conjunct _ => "Conjunct"
| Specialize _ => "Specialize"
| Skolemize _ => "Skolemize"
| Clausify _ => "Clausify";
val ppInference = Print.ppMap toStringInference Print.ppString;
(* ------------------------------------------------------------------------- *)
(* Simplifying with definitions. *)
(* ------------------------------------------------------------------------- *)
datatype simplify =
Simp of
{formula : (formula, formula * thm) Map.map,
andSet : (formula Set.set * formula * thm) list,
orSet : (formula Set.set * formula * thm) list,
xorSet : (formula Set.set * formula * thm) list};
val simplifyEmpty =
Simp
{formula = Map.new compare,
andSet = [],
orSet = [],
xorSet = []};
local
fun simpler fm s =
Set.size s <> 1 orelse
case Set.pick s of
True => false
| False => false
| Literal _ => false
| _ => true;
fun addSet set_defs body_def =
let
fun def_body_size (body,_,_) = Set.size body
val body_size = def_body_size body_def
val (body,_,_) = body_def
fun add acc [] = List.revAppend (acc,[body_def])
| add acc (l as (bd as (b,_,_)) :: bds) =
case Int.compare (def_body_size bd, body_size) of
LESS => List.revAppend (acc, body_def :: l)
| EQUAL =>
if Set.equal b body then List.revAppend (acc,l)
else add (bd :: acc) bds
| GREATER => add (bd :: acc) bds
in
add [] set_defs
end;
fun add simp (body,False,th) = add simp (negate body, True, th)
| add simp (True,_,_) = simp
| add (Simp {formula,andSet,orSet,xorSet}) (And (_,_,s), def, th) =
let
val andSet = addSet andSet (s,def,th)
and orSet = addSet orSet (negateSet s, negate def, th)
in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet}
end
| add (Simp {formula,andSet,orSet,xorSet}) (Or (_,_,s), def, th) =
let
val orSet = addSet orSet (s,def,th)
and andSet = addSet andSet (negateSet s, negate def, th)
in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet}
end
| add simp (Xor (_,_,p,s), def, th) =
let
val simp = addXorSet simp (s, applyPolarity p def, th)
in
case def of
True =>
let
fun addXorLiteral (fm as Literal _, simp) =
let
val s = Set.delete s fm
in
if not (simpler fm s) then simp
else addXorSet simp (s, applyPolarity (not p) fm, th)
end
| addXorLiteral (_,simp) = simp
in
Set.foldl addXorLiteral simp s
end
| _ => simp
end
| add (simp as Simp {formula,andSet,orSet,xorSet}) (body,def,th) =
if Map.inDomain body formula then simp
else
let
val formula = Map.insert formula (body,(def,th))
val formula = Map.insert formula (negate body, (negate def, th))
in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet}
end
and addXorSet (simp as Simp {formula,andSet,orSet,xorSet}) (s,def,th) =
if Set.size s = 1 then add simp (Set.pick s, def, th)
else
let
val xorSet = addSet xorSet (s,def,th)
in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet}
end;
in
fun simplifyAdd simp (th as Thm (fm,_)) = add simp (fm,True,th);
end;
local
fun simplifySet set_defs set =
let
fun pred (s,_,_) = Set.subset s set
in
case List.find pred set_defs of
NONE => NONE
| SOME (s,f,th) =>
let
val set = Set.add (Set.difference set s) f
in
SOME (set,th)
end
end;
in
fun simplify (Simp {formula,andSet,orSet,xorSet}) =
let
fun simp fm inf =
case simp_sub fm inf of
NONE => simp_top fm inf
| SOME (fm,inf) => try_simp_top fm inf
and try_simp_top fm inf =
case simp_top fm inf of
NONE => SOME (fm,inf)
| x => x
and simp_top fm inf =
case fm of
And (_,_,s) =>
(case simplifySet andSet s of
NONE => NONE
| SOME (s,th) =>
let
val fm = AndSet s
val inf = th :: inf
in
try_simp_top fm inf
end)
| Or (_,_,s) =>
(case simplifySet orSet s of
NONE => NONE
| SOME (s,th) =>
let
val fm = OrSet s
val inf = th :: inf
in
try_simp_top fm inf
end)
| Xor (_,_,p,s) =>
(case simplifySet xorSet s of
NONE => NONE
| SOME (s,th) =>
let
val fm = XorPolaritySet (p,s)
val inf = th :: inf
in
try_simp_top fm inf
end)
| _ =>
(case Map.peek formula fm of
NONE => NONE
| SOME (fm,th) =>
let
val inf = th :: inf
in
try_simp_top fm inf
end)
and simp_sub fm inf =
case fm of
And (_,_,s) =>
(case simp_set s inf of
NONE => NONE
| SOME (l,inf) => SOME (AndList l, inf))
| Or (_,_,s) =>
(case simp_set s inf of
NONE => NONE
| SOME (l,inf) => SOME (OrList l, inf))
| Xor (_,_,p,s) =>
(case simp_set s inf of
NONE => NONE
| SOME (l,inf) => SOME (XorPolarityList (p,l), inf))
| Exists (_,_,n,f) =>
(case simp f inf of
NONE => NONE
| SOME (f,inf) => SOME (ExistsSet (n,f), inf))
| Forall (_,_,n,f) =>
(case simp f inf of
NONE => NONE
| SOME (f,inf) => SOME (ForallSet (n,f), inf))
| _ => NONE
and simp_set s inf =
let
val (changed,l,inf) = Set.foldr simp_set_elt (false,[],inf) s
in
if changed then SOME (l,inf) else NONE
end
and simp_set_elt (fm,(changed,l,inf)) =
case simp fm inf of
NONE => (changed, fm :: l, inf)
| SOME (fm,inf) => (true, fm :: l, inf)
in
fn th as Thm (fm,_) =>
case simp fm [] of
SOME (fm,ths) =>
let
val inf = Simplify (th,ths)
in
Thm (fm,inf)
end
| NONE => th
end;
end;
(*MetisTrace2
val simplify = fn simp => fn th as Thm (fm,_) =>
let
val th' as Thm (fm',_) = simplify simp th
val () = if compare (fm,fm') = EQUAL then ()
else (Print.trace pp "Normalize.simplify: fm" fm;
Print.trace pp "Normalize.simplify: fm'" fm')
in
th'
end;
*)
(* ------------------------------------------------------------------------- *)
(* Definitions. *)
(* ------------------------------------------------------------------------- *)
val newDefinitionRelation =
let
val counter : int ref = ref 0
in
fn () =>
let
val ref i = counter
val () = counter := i + 1
in
definitionPrefix ^ "_" ^ Int.toString i
end
end;
fun newDefinition def =
let
val fv = freeVars def
val rel = newDefinitionRelation ()
val atm = (Name.fromString rel, NameSet.transform Term.Var fv)
val fm = Formula.Iff (Formula.Atom atm, toFormula def)
val fm = Formula.setMkForall (fv,fm)
val inf = Definition (rel,fm)
val lit = Literal (fv,(false,atm))
val fm = Xor2 (lit,def)
in
Thm (fm,inf)
end;
(* ------------------------------------------------------------------------- *)
(* Definitional conjunctive normal form. *)
(* ------------------------------------------------------------------------- *)
datatype cnf =
ConsistentCnf of simplify
| InconsistentCnf;
val initialCnf = ConsistentCnf simplifyEmpty;
local
fun def_cnf_inconsistent th =
let
val cls = [(LiteralSet.empty,th)]
in
(cls,InconsistentCnf)
end;
fun def_cnf_clause inf (fm,acc) =
let
val cl = toClause fm
val th = Thm (fm,inf)
in
(cl,th) :: acc
end
(*MetisDebug
handle Error err =>
(Print.trace pp "Normalize.addCnf.def_cnf_clause: fm" fm;
raise Bug ("Normalize.addCnf.def_cnf_clause: " ^ err));
*)
fun def_cnf cls simp ths =
case ths of
[] => (cls, ConsistentCnf simp)
| th :: ths => def_cnf_formula cls simp (simplify simp th) ths
and def_cnf_formula cls simp (th as Thm (fm,_)) ths =
case fm of
True => def_cnf cls simp ths
| False => def_cnf_inconsistent th
| And (_,_,s) =>
let
fun add (f,z) = Thm (f, Conjunct th) :: z
in
def_cnf cls simp (Set.foldr add ths s)
end
| Exists (fv,_,n,f) =>
let
val th = Thm (skolemize fv n f, Skolemize th)
in
def_cnf_formula cls simp th ths
end
| Forall (_,_,_,f) =>
let
val th = Thm (f, Specialize th)
in
def_cnf_formula cls simp th ths
end
| _ =>
case minimumDefinition fm of
SOME def =>
let
val ths = th :: ths
val th = newDefinition def
in
def_cnf_formula cls simp th ths
end
| NONE =>
let
val simp = simplifyAdd simp th
val fm = basicCnf fm
val inf = Clausify th
in
case fm of
True => def_cnf cls simp ths
| False => def_cnf_inconsistent (Thm (fm,inf))
| And (_,_,s) =>
let
val inf = Conjunct (Thm (fm,inf))
val cls = Set.foldl (def_cnf_clause inf) cls s
in
def_cnf cls simp ths
end
| fm => def_cnf (def_cnf_clause inf (fm,cls)) simp ths
end;
in
fun addCnf th cnf =
case cnf of
ConsistentCnf simp => def_cnf [] simp [th]
| InconsistentCnf => ([],cnf);
end;
local
fun add (th,(cls,cnf)) =
let
val (cls',cnf) = addCnf th cnf
in
(cls' @ cls, cnf)
end;
in
fun proveCnf ths =
let
val (cls,_) = List.foldl add ([],initialCnf) ths
in
rev cls
end;
end;
fun cnf fm =
let
val cls = proveCnf [mkAxiom fm]
in
map fst cls
end;
end