using Nemerle using Nemerle.Utility using Nemerle.Logging using Nemerle.Collections using Nemerle.Imperative using Nemerle.Profiling set namespace Fx7 public class ProvingGrinder type E = ProofGen.E pool : Term.Pool cache_neg : Hashtable [Term, Term * E] = Hashtable () cache_pos : Hashtable [Term, Term * E] = Hashtable () static CNFSize (f : Term, neg : bool) : int match (f.Name) | "and" when !neg \ | "or" when neg => mutable res = 0 f.IterChildren (c => res += CNFSize (c, neg)) res | "and" | "or" => mutable res = 1 f.IterChildren (c => res *= CNFSize (c, neg)) res | "not" => CNFSize (f.OnlyChild, !neg) | _ => 1 static LinSize (f : Term) : int match (f.Name) | "and" | "or" => mutable res = 0 f.IterChildren (c => res += LinSize (c)) res | "not" => LinSize (f.OnlyChild) | _ => 1 ContainsVar (var : Term, form : Term) : bool assert (var.Arity == 0) if (var === form) true else when (form.Name == "forall") match (form.Children) | [vars, _] | [vars, _, _] => when (vars.Children.Exists (_ == var : object)) return false | _ => assert (false) form.Children.Exists (ContainsVar (var, _)) BuildForall (vars : list [Term], pats : Term, body : Term) : Term def vars = pool.Get ("$@vars", vars) if (pats == null) pool.Get ("forall", [vars, body]) else pool.Get ("forall", [vars, pats, body]) GrindForall (vars : Term, pats : Term, body : Term, proof : E) : Term * E assert (vars.Name == "$@vars") def (used, not_used) = vars.Children.Partition (ContainsVar (_, body)) if (pats != null && not_used.Exists (ContainsVar (_, pats))) log (GRIND, $"the formula FORALL $vars. $body uses variables unused in body in the pattern: $pats") (pool.Get ("forall", [vars, pats, body]), proof) else if (used is []) log (GRIND, $ "got rid of vars in FORALL $vars. $body") (body, E.Comp (vars.Children.FoldLeft (E.Id (), (_, acc) => E.App ("remove_unused", [acc])), proof)) else unless (not_used is []) log (GRIND, $ "droped $not_used from FORALL $vars. $body") def orig_vars = vars def grind_neq (pats, vars, clause) def is_var (v) v.Arity == 0 && vars.Contains (v) def is_ground (t) ! vars.Exists (ContainsVar (_, t)) def is_neq (_ : Term) | Term.E ("not", [Term.E ("=", [t1, t2])]) => if (t1 !== t2 && is_var (t1) && (is_var (t2) || is_ground (t2))) Some (t1, t2) else if (is_var (t2) && is_ground (t1)) Some (t2, t1) else None () | _ => None () def find_neq (_) | (acc, t :: ts) => match (is_neq (t)) | Some as r => (r, acc.RevAppend (ts)) | None => find_neq (t :: acc, ts) | (acc, []) => (None (), acc.Rev ()) match (find_neq ([], clause)) | (Some ((t1, t2)), rest) => def subst = IntTree.Empty ().Add (t1.Id, t2) def rest = rest.Map (_.Apply (subst)) def pats = if (pats == null) null else pats.Apply (subst) def vars = vars.Filter (_ != t1 : object) grind_neq (pats, vars, rest) | _ => def body' = match (clause) | [] => log (WARN, $"formula FORALL $orig_vars. $body reduced to false") pool.Get ("false", []) | [one] => one | several => pool.Get ("or", several) when (body !== body') log (GRIND, $"FORALL $orig_vars. $body ==> FORALL $vars. $(body')") if (vars is []) body' else BuildForall (vars, pats, body') if (Driver.GrindForall && body.Name == "or") assert (! Driver.ProofLogging) (grind_neq (pats, used, body.Children), null) else def proof = if (used.Length == vars.Arity) proof else def skips = vars.Children.FoldRight (E.Id (), (v, acc) => E.App (if (used.Contains (v)) "skip_forall" else "remove_unused", [acc])) E.Comp (skips, proof) (BuildForall (used, pats, body), proof) EqualityPropagation (formula : Term) : Term def fixpoint_apply (form, subst) def form' = form.Apply (subst) //log (TEMP, $"subst: $form -> $(form')") if (form' === form) form else fixpoint_apply (form', subst) if (formula.Name == "and") def f (_, form, (non_eq, subst)) if (form.Name == "=" && form.Child_1of2.Arity == 0 && form.Child_2of2.Arity == 0) //log (TEMP, $"form = $form") def (a, b) = (fixpoint_apply (form.Child_1of2, subst), fixpoint_apply (form.Child_2of2, subst)) //log (TEMP, $" --> ($a, $b)") if (a === b) (non_eq, subst) else def (a, b) = if (a.Depth < b.Depth) (b, a) else if (a.Depth > b.Depth) (a, b) else if (a.Id < b.Id) (a, b) else (b, a) (non_eq, subst.Add (a.Id, b)) else if (form.Arity == 0 && form.Name == "true") (non_eq, subst) else (form :: non_eq, subst) def (non_eq, subst) = formula.FoldIndexedChildren (([], IntTree.Empty ()), f) def expand (f, t, subst) def t' = fixpoint_apply (t, subst) if (t === t') subst else subst.Replace (f, t') def fixpoint (subst) def subst' = subst.Fold (subst, expand) if (subst' === subst) subst else fixpoint (subst') def subst = fixpoint (subst) def args = non_eq.RevMap (_.Apply (subst)) //def args = args.Sort ((a, b) => a.Name.CompareTo (b.Name)) pool.Get ("and", args) else formula SkolemizeForall (qvars : list [Term], sub : Subst, f : Term, neg : bool) : Term * E // log (TEMP, $ "skol: $qvars $neg $sub $f") match (f.Children) | [vars, pats, body] \ | [vars, body] with pats = null => mutable can_cache = false def normalize = if (Driver.ProofLogging) if (neg) E.Ref ("norm_" + f.Name) else E.Id () else null if (neg == (f.Name == "forall")) def skolem_fn () pool.Get ( pool.FreshFn (qvars.Length), qvars) def sub = vars.Children.FoldLeft (sub, (v, sub) => sub.Replace (v.Id, skolem_fn ())) //when (pats != null) // log (WARN, $ "patterns given for q-forumula used in " // "existential position $f") def (res, proof) = Skolemize (qvars, sub, body, neg, ref can_cache) if (Driver.ProofLogging) def skol = vars.Children.FoldLeft (E.Id (), (v, acc) => E.Comp (E.Comp (E.App ("skolemize", [E.Ref (sub.Get (v.Id).Name)]), normalize), acc)) (res, E.Comp (proof, skol)) else (res, null) else def qvars = vars.Children.FoldLeft (qvars, (v, qvars) => v :: qvars.Filter (_ != v : object)) def pats = if (pats == null) null else Skolemize (qvars, sub, pats, neg, ref can_cache, dont_add_eqtrue = true) [0] def (body, proof) = Skolemize (qvars, sub, body, neg, ref can_cache) def cnf_size = CNFSize (body, false) def lin_size = LinSize (body) def make_forall (body, proof) GrindForall (vars, pats, body, proof) if (cnf_size > Driver.RealCNFThreshold * lin_size) when (Driver.RealCNFThreshold > 0) log (INFO, $ "not using CNF-conversion because of $cnf_size clauses required (size: $lin_size)") def proof = if (Driver.ProofLogging) vars.Children.FoldLeft (proof, (_, acc) => E.Comp (E.App ("skip_forall", [acc]), normalize)) else null make_forall (body, proof) else def cnf (f) match (f.Name) | "and" => def loop (_) | [x] => cnf (x) | x :: xs => def (proof1, clauses1) = cnf (x) def (proof2, clauses2) = loop (xs) def proof = if (Driver.ProofLogging) E.Comp ( clauses1.Tail.FoldLeft (E.Id (), (_, acc) => E.App ("and_comm", [acc])), E.App ("pos_and_comp", [proof1, proof2])) else null (proof, clauses1 + clauses2) | [] => assert (false) loop (f.Children) | "or" => def loop (_) | [x] => cnf (x) | x :: xs => def (proof1, clauses1) = cnf (x) def (proof2, clauses2) = loop (xs) match (clauses2.Rev ()) | (_ :: rest2) as lst2 => mutable res = [] def blow (clause) def join = clause.Tail.FoldLeft (E.Id (), (_, acc) => E.App ("or_comm", [acc])) foreach (e in lst2) res ::= clause + e rest2.FoldLeft (join, (_, acc) => E.App ("or_and_distr", [join, acc])) match (clauses1.Rev ()) | (first :: rest) as lst1 => if (Driver.ProofLogging) def join = rest2.FoldLeft (E.Id (), (_, acc) => E.App ("and_comm", [acc])) def proof = rest.FoldLeft (blow (first), (clause, acc) => E.Comp (join, E.App ("and_or_distr", [blow (clause), acc]))) (E.Comp (proof, E.App ("pos_or_comp", [proof1, proof2])), res) else foreach (c1 in lst1) foreach (c2 in lst2) res ::= c1 + c2 (null, res) | [] => assert (false) | _ => assert (false) | [] => assert (false) loop (f.Children) | _ => (E.Id (), [[f]]) def get_forall = vars.Children.FoldLeft (E.Ref ("and_get"), (_, acc) => E.App ("skip_forall", [acc])) def skip_forall = vars.Children.FoldLeft (E.Ref ("and_skip"), (_, acc) => E.App ("skip_forall", [acc])) def make (_) | clause :: rest => mutable is_true = false def clause = if (Driver.ProofLogging) clause else def ht = Hashtable () def check (l : Term) | Term.E ("not", [idx]) \ | idx => if (ht.Contains (idx)) unless (ht [idx] === l) is_true = true false else ht [idx] = l true clause.Filter (check) if (is_true || clause is []) assert (!Driver.ProofLogging) def formula = pool.Get (if (is_true) "true" else "false", []) match (rest) | [] => ([formula], null) | _ => (formula :: make (rest) [0], null) else def body = match (clause) | [l] => l | _ => pool.Get ("or", clause) match (rest) | [] => def (formula, proof) = make_forall (body, E.Id ()) ([formula], proof) | _ => def (formula, proof) = make_forall (body, get_forall) def (formulas, rest_proof) = make (rest) (formula :: formulas, E.App ("duplicate", [proof, E.Comp (rest_proof, skip_forall)])) | [] => assert (false) def (ground_cnf_proof, clauses) = cnf (body) def cnf_proof = vars.Children.FoldLeft (E.Comp (ground_cnf_proof, proof), (_, acc) => E.Comp (E.App ("skip_forall", [acc]), normalize)) def (formulas, proof) = make (clauses) def formula = match (formulas) | [one] => one | lst => pool.Get ("and", lst) (formula, E.Comp (proof, cnf_proof)) | _ => assert (false) fake_inf : E = E.InfTerm (() => assert (false), true) [Accessor] mutable lemmas : list [ProofGen.Lemma] = [] //mutable sk_id : int Skolemize (qvars : list [Term], sub : Subst, f : Term, neg : bool, can_cache : ref bool, dont_add_eqtrue = false) : Term * E mutable local_can_cache = true def nnf (t) Skolemize (qvars, sub, t, neg, ref local_can_cache) def cache = if (qvars is [] && sub.IsEmpty) if (neg) cache_neg else cache_pos else null def neg_pref = if (neg) "neg_" else "pos_" if (cache != null && cache.Contains (f)) cache [f] else def res = if (sub.Contains (f.Id)) (sub.Get (f.Id), E.Id ()) else match (f.Name) | "not" => if (!neg || !Driver.ProofLogging) Skolemize (qvars, sub, f.OnlyChild, !neg, ref local_can_cache) else def (res, proof) = Skolemize (qvars, sub, f.OnlyChild, !neg, ref local_can_cache) (res, E.Comp (proof, E.App ("nnpp", [fake_inf]))) | "iff" => def (res, proof) = nnf (pool.Get ("and", [ pool.Get ("or", [pool.Get ("not", [f.Child_1of2]), f.Child_2of2]), pool.Get ("or", [pool.Get ("not", [f.Child_2of2]), f.Child_1of2])])) def proof = if (Driver.ProofLogging) E.Comp (proof, E.App (neg_pref + "iff_def", [fake_inf, fake_inf])) else null (res, proof) | "implies" => def (res, proof) = nnf (pool.Get ("or", [pool.Get ("not", [f.Child_1of2]), f.Child_2of2])) def proof = if (Driver.ProofLogging) E.Comp (proof, E.App (neg_pref + "implies_def", [fake_inf, fake_inf])) else null (res, proof) | "and" | "or" => def head = if (neg) if (f.Name == "and") "or" else "and" else f.Name def fn = neg_pref + f.Name + "_comp" def flat (child, rest, proof) if (child.Name == head) def fn = head + "_comm" def build (_) | [] => E.Id () | _ :: xs => E.App (fn, [fake_inf, fake_inf, fake_inf, fake_inf, build (xs)]) def proof = if (Driver.ProofLogging) E.Comp (build (child.Children.Tail), proof) else null (child.Children + rest, proof) else (child :: rest, proof) def loop (_) | [x] => def (x', px) = nnf (x) if (x'.Name == head) (x'.Children, px) else ([x'], px) | a :: b => def (a', pa) = nnf (a) def (b', pb) = loop (b) def proof = if (Driver.ProofLogging) E.App (fn, [fake_inf, fake_inf, fake_inf, fake_inf, pa, pb]) else null flat (a', b', proof) | [] => assert (false) match (f.Children) | [] => (pool.Get (if (f.Name == "and") "true" else "false", []), E.Id ()) | _ => def (children, proof) = loop (f.Children) (pool.Get (head, children), proof) | "exists" | "forall" => local_can_cache = false SkolemizeForall (qvars, sub, f, neg) | _ => def f = f.Apply (sub) def (proof, f) = match (f.Name) | _ when dont_add_eqtrue \ | "true" | "false" | "=" | "<=" | ">=" | "<" | ">" | "distinct" => (E.Id (), f) | _ => (E.Ref (if (neg) "eqtrue_neg" else "eqtrue"), pool.Get ("=", [f, pool.True])) def f = if (Driver.ProofLogging) f // TODO else match (f.Name) | "=" | "<=" | ">=" => if (f.Child_1of2 === f.Child_2of2) log (GRIND, $"simplifing $f to true") pool.Get ("true", []) else f | "<" | ">" => if (f.Child_1of2 === f.Child_2of2) log (GRIND, $"simplifing $f to false") pool.Get ("false", []) else f | _ => f (if (neg) pool.Get ("not", [f]) else f, proof) //log (TEMP, $"skol: $f -> $res") when (!local_can_cache) can_cache = false when (can_cache && cache != null) cache [f] = res res public this (core : Core) pool = core.TermPool public Skolemize (f_orig : Term) : Term assert (lemmas is []) mutable can_cache = true //System.IO.File.WriteAllText ("skol-1.smt", f_orig.ToPrettyString ()) def (f, proof) = Skolemize ([], IntTree.Empty (), f_orig, false, ref can_cache) when (Driver.ProofLogging) lemmas ::= ProofGen.Lemma ("skol", "top-level skolemization+NNF", pool.Get ("implies", [f_orig, f]), proof) def f = if (Driver.EqProp) EqualityPropagation (f) else f //System.IO.File.WriteAllText ("skol-2.smt", f.ToPrettyString ()) f