max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/tools/super): replace ↣ with ^.

Browse source 
The plan is to delete the funny arrow ↣ notation and keep only ^.
This commit is contained in:
Leonardo de Moura 2016-12-16 19:14:05 -08:00
parent 85ae8ce307
commit 63ec7cd6cf
20 changed files with 435 additions and 435 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/tools/super/cdcl.lean
View file

@ -8,11 +8,11 @@ open tactic expr monad super
private meta def theory_solver_of_tactic (th_solver : tactic unit) : cdcl.solver (option cdcl.proof_term) :=
do s ← state_t.read, ♯do
hyps ← return $ s↣trail↣for (λe, e↣hyp),
subgoal ← mk_meta_var s↣local_false,
hyps ← return $ s^.trail^.for (λe, e^.hyp),
subgoal ← mk_meta_var s^.local_false,
goals ← get_goals,
set_goals [subgoal],
hvs ← for hyps (λhyp, assertv hyp↣local_pp_name hyp↣local_type hyp),
hvs ← for hyps (λhyp, assertv hyp^.local_pp_name hyp^.local_type hyp),
solved ← (do th_solver, now, return tt) <|> return ff,
set_goals goals,
if solved then do
@ -30,7 +30,7 @@ res ← cdcl.solve (theory_solver_of_tactic th_solver) local_false clauses,
match res with
| (cdcl.result.unsat proof) := exact proof
| (cdcl.result.sat interp) :=
let interp' := do e ← interp↣to_list, [if e↣2 = tt then e↣1 else not_ e↣1] in
let interp' := do e ← interp^.to_list, [if e.2 = tt then e.1 else not_ e.1] in
do pp_interp ← pp interp',
fail (to_fmt "satisfying assignment: " ++ pp_interp)
end

144
library/tools/super/cdcl_solver.lean
View file

@ -101,7 +101,7 @@ meta def initial (local_false : expr) : state := {
}
meta def watches_for (st : state) (pl : prop_lit) : watch_map :=
(st↣watches↣find pl)↣get_or_else (rb_map.mk _ _)
(st^.watches^.find pl)^.get_or_else (rb_map.mk _ _)
end state
@ -113,14 +113,14 @@ meta def fail {A B} [has_to_format B] (b : B) : solver A :=
♯ @tactic.fail A B _ b
meta def get_local_false : solver expr :=
do st ← state_t.read, return st↣local_false
do st ← state_t.read, return st^.local_false
meta def mk_var_core (v : prop_var) (ph : bool) : solver unit := do
state_t.modify $ λst, match st↣vars↣find v with
state_t.modify $ λst, match st^.vars^.find v with
| (some _) := st
| none := { st with
vars := st↣vars↣insert v ⟨ph, none⟩,
unassigned := st↣unassigned↣insert v v
vars := st^.vars^.insert v ⟨ph, none⟩,
unassigned := st^.unassigned^.insert v v
}
end
@ -130,36 +130,36 @@ meta def set_conflict (proof : proof_term) : solver unit :=
state_t.modify $ λst, { st with conflict := some proof }
meta def has_conflict : solver bool :=
do st ← state_t.read, return st↣conflict↣is_some
do st ← state_t.read, return st^.conflict^.is_some
meta def push_trail (elem : trail_elem) : solver unit := do
st ← state_t.read,
match st↣vars↣find elem↣var with
| none := fail $ "unknown variable: " ++ elem↣var↣to_string
| some ⟨_, some _⟩ := fail $ "adding already assigned variable to trail: " ++ elem↣var↣to_string
match st^.vars^.find elem^.var with
| none := fail $ "unknown variable: " ++ elem^.var^.to_string
| some ⟨_, some _⟩ := fail $ "adding already assigned variable to trail: " ++ elem^.var^.to_string
| some ⟨_, none⟩ :=
state_t.write { st with
vars := st↣vars↣insert elem↣var ⟨elem↣phase, some elem↣hyp⟩,
unassigned := st↣unassigned↣erase elem↣var,
trail := elem :: st↣trail,
unitp_queue := elem↣var :: st↣unitp_queue
vars := st^.vars^.insert elem^.var ⟨elem^.phase, some elem^.hyp⟩,
unassigned := st^.unassigned^.erase elem^.var,
trail := elem :: st^.trail,
unitp_queue := elem^.var :: st^.unitp_queue
}
end
meta def pop_trail_core : solver (option trail_elem) := do
st ← state_t.read,
match st↣trail with
match st^.trail with
| elem :: rest := do
state_t.write { st with trail := rest,
vars := st↣vars↣insert elem↣var ⟨elem↣phase, none⟩,
unassigned := st↣unassigned↣insert elem↣var elem↣var,
vars := st^.vars^.insert elem^.var ⟨elem^.phase, none⟩,
unassigned := st^.unassigned^.insert elem^.var elem^.var,
unitp_queue := [] },
return $ some elem
| [] := return none
end
meta def is_decision_level_zero : solver bool :=
do st ← state_t.read, return $ st↣trail↣for_all $ λelem, ¬elem↣is_decision
do st ← state_t.read, return $ st^.trail^.for_all $ λelem, ¬elem^.is_decision
meta def revert_to_decision_level_zero : unit → solver unit | () := do
is_dl0 ← is_decision_level_zero,
@ -170,11 +170,11 @@ meta def formula_of_lit (local_false : expr) (v : prop_var) (ph : bool) :=
if ph then v else imp v local_false
meta def lookup_var (v : prop_var) : solver (option var_state) :=
do st ← state_t.read, return $ st↣vars↣find v
do st ← state_t.read, return $ st^.vars^.find v
meta def add_propagation (v : prop_var) (ph : bool) (just : proof_term) (just_is_dn : bool) : solver unit :=
do v_st ← lookup_var v, local_false ← get_local_false, match v_st with
| none := fail $ "propagating unknown variable: " ++ v↣to_string
| none := fail $ "propagating unknown variable: " ++ v^.to_string
| some ⟨assg_ph, some proof⟩ :=
if ph = assg_ph then
return ()
@ -198,11 +198,11 @@ hyp ← return $ local_const hyp_name hyp_name binder_info.default (formula_of_l
push_trail $ trail_elem.dec v ph hyp
meta def lookup_lit (l : clause.literal) : solver (option (bool × proof_hyp)) :=
do var_st_opt ← lookup_var l↣formula, match var_st_opt with
do var_st_opt ← lookup_var l^.formula, match var_st_opt with
| none := return none
| some ⟨ph, none⟩ := return none
| some ⟨ph, some proof⟩ :=
return $ some (if l↣is_neg then bnot ph else ph, proof)
return $ some (if l^.is_neg then bnot ph else ph, proof)
end
meta def lit_is_false (l : clause.literal) : solver bool :=
@ -215,57 +215,57 @@ meta def lit_is_not_false (l : clause.literal) : solver bool :=
do isf ← lit_is_false l, return $ bnot isf
meta def cls_is_false (c : clause) : solver bool :=
lift list.band $ mapm lit_is_false c↣get_lits
lift list.band $ mapm lit_is_false c^.get_lits
private meta def unit_propg_cls' : clause → solver (option prop_var) | c :=
if c↣num_lits = 0 then return (some c↣proof)
else let hd := c↣get_lit 0 in
if c^.num_lits = 0 then return (some c^.proof)
else let hd := c^.get_lit 0 in
do lit_st ← lookup_lit hd, match lit_st with
| some (ff, isf_prf) := unit_propg_cls' (c↣inst isf_prf)
| some (ff, isf_prf) := unit_propg_cls' (c^.inst isf_prf)
| _ := return none
end
meta def unit_propg_cls : clause → solver unit | c :=
do has_confl ← has_conflict,
if has_confl then return () else
if c↣num_lits = 0 then do set_conflict c↣proof
else let hd := c↣get_lit 0 in
if c^.num_lits = 0 then do set_conflict c^.proof
else let hd := c^.get_lit 0 in
do lit_st ← lookup_lit hd, match lit_st with
| some (ff, isf_prf) := unit_propg_cls (c↣inst isf_prf)
| some (ff, isf_prf) := unit_propg_cls (c^.inst isf_prf)
| some (tt, _) := return ()
| none :=
do fls_prf_opt ← unit_propg_cls' (c↣inst (expr.mk_var 0)),
do fls_prf_opt ← unit_propg_cls' (c^.inst (expr.mk_var 0)),
match fls_prf_opt with
| some fls_prf := do
fls_prf' ← return $ lam `H binder_info.default c↣type↣binding_domain fls_prf,
if hd↣is_neg then
add_propagation hd↣formula ff fls_prf' ff
fls_prf' ← return $ lam `H binder_info.default c^.type^.binding_domain fls_prf,
if hd^.is_neg then
add_propagation hd^.formula ff fls_prf' ff
else
add_propagation hd↣formula tt fls_prf' tt
add_propagation hd^.formula tt fls_prf' tt
| none := return ()
end
end
private meta def modify_watches_for (pl : prop_lit) (f : watch_map → watch_map) : solver unit :=
state_t.modify $ λst, { st with
watches := st↣watches↣insert pl $ f $ st↣watches_for pl
watches := st^.watches^.insert pl $ f $ st^.watches_for pl
}
private meta def add_watch (n : name) (c : clause) (i j : ℕ) : solver unit :=
let l := c↣get_lit i, pl := prop_lit.of_cls_lit l in
modify_watches_for pl $ λw, w↣insert n (i,j,c)
let l := c^.get_lit i, pl := prop_lit.of_cls_lit l in
modify_watches_for pl $ λw, w^.insert n (i,j,c)
private meta def remove_watch (n : name) (c : clause) (i : ℕ) : solver unit :=
let l := c↣get_lit i, pl := prop_lit.of_cls_lit l in
modify_watches_for pl $ λw, w↣erase n
let l := c^.get_lit i, pl := prop_lit.of_cls_lit l in
modify_watches_for pl $ λw, w^.erase n
private meta def set_watches (n : name) (c : clause) : solver unit :=
if c↣num_lits = 0 then
set_conflict c↣proof
else if c↣num_lits = 1 then
if c^.num_lits = 0 then
set_conflict c^.proof
else if c^.num_lits = 1 then
unit_propg_cls c
else do
not_false_lits ← filter (λi, lit_is_not_false (c↣get_lit i)) (list.range c↣num_lits),
not_false_lits ← filter (λi, lit_is_not_false (c^.get_lit i)) (list.range c^.num_lits),
match not_false_lits with
| [] := do
add_watch n c 0 1,
@ -287,38 +287,38 @@ remove_watch n c i₂,
set_watches n c
meta def mk_clause (c : clause) : solver unit := do
c ← ♯c↣distinct,
for c↣get_lits (λl, mk_var l↣formula),
c ← ♯c^.distinct,
for c^.get_lits (λl, mk_var l^.formula),
revert_to_decision_level_zero (),
state_t.modify $ λst, { st with clauses := c :: st↣clauses },
state_t.modify $ λst, { st with clauses := c :: st^.clauses },
c_name ← ♯mk_fresh_name,
set_watches c_name c
meta def unit_propg_var (v : prop_var) : solver unit :=
do st ← state_t.read, if st↣conflict↣is_some then return () else
match st↣vars↣find v with
| some ⟨ph, none⟩ := fail $ "propagating unassigned variable: " ++ v↣to_string
| none := fail $ "unknown variable: " ++ v↣to_string
do st ← state_t.read, if st^.conflict^.is_some then return () else
match st^.vars^.find v with
| some ⟨ph, none⟩ := fail $ "propagating unassigned variable: " ++ v^.to_string
| none := fail $ "unknown variable: " ++ v^.to_string
| some ⟨ph, some _⟩ :=
let watches := st↣watches_for $ prop_lit.of_var_and_phase v (bnot ph) in
for' watches↣to_list $ λw, update_watches w↣1 w↣2↣2↣2 w↣2↣1 w↣2↣2↣1
let watches := st^.watches_for $ prop_lit.of_var_and_phase v (bnot ph) in
for' watches^.to_list $ λw, update_watches w.1 w.2.2.2 w.2.1 w.2.2.1
end
meta def analyze_conflict' (local_false : expr) : proof_term → list trail_elem → clause
| proof (trail_elem.dec v ph hyp :: es) :=
let abs_prf := abstract_local proof hyp↣local_uniq_name in
let abs_prf := abstract_local proof hyp^.local_uniq_name in
if has_var abs_prf then
clause.close_const (analyze_conflict' proof es) hyp
else
analyze_conflict' proof es
| proof (trail_elem.propg v ph l_prf hyp :: es) :=
let abs_prf := abstract_local proof hyp↣local_uniq_name in
let abs_prf := abstract_local proof hyp^.local_uniq_name in
if has_var abs_prf then
analyze_conflict' (app (lam hyp↣local_pp_name binder_info.default (formula_of_lit local_false v ph) abs_prf) l_prf) es
analyze_conflict' (app (lam hyp^.local_pp_name binder_info.default (formula_of_lit local_false v ph) abs_prf) l_prf) es
else
analyze_conflict' proof es
| proof (trail_elem.dbl_neg_propg v ph l_prf hyp :: es) :=
let abs_prf := abstract_local proof hyp↣local_uniq_name in
let abs_prf := abstract_local proof hyp^.local_uniq_name in
if has_var abs_prf then
analyze_conflict' (app l_prf (lambdas [hyp] proof)) es
else
@ -326,12 +326,12 @@ meta def analyze_conflict' (local_false : expr) : proof_term → list trail_elem
| proof [] := ⟨0, 0, proof, local_false, local_false⟩
meta def analyze_conflict (proof : proof_term) : solver clause :=
do st ← state_t.read, return $ analyze_conflict' st↣local_false proof st↣trail
do st ← state_t.read, return $ analyze_conflict' st^.local_false proof st^.trail
meta def add_learned (c : clause) : solver unit := do
prf_abbrev_name ← ♯mk_fresh_name,
c' ← return { c with proof := local_const prf_abbrev_name prf_abbrev_name binder_info.default c↣type },
state_t.modify $ λst, { st with learned := ⟨c', c↣proof⟩ :: st↣learned },
c' ← return { c with proof := local_const prf_abbrev_name prf_abbrev_name binder_info.default c^.type },
state_t.modify $ λst, { st with learned := ⟨c', c^.proof⟩ :: st^.learned },
c_name ← ♯mk_fresh_name,
set_watches c_name c'
@ -341,7 +341,7 @@ if ¬isf then
state_t.modify (λst, { st with conflict := none })
else do
removed_elem ← pop_trail_core,
if removed_elem↣is_some then
if removed_elem^.is_some then
backtrack_with conflict_clause
else
return ()
@ -349,14 +349,14 @@ else do
meta def replace_learned_clauses' : proof_term → list learned_clause → proof_term
| proof [] := proof
| proof (⟨c, actual_proof⟩ :: lcs) :=
let abs_prf := abstract_local proof c↣proof↣local_uniq_name in
let abs_prf := abstract_local proof c^.proof^.local_uniq_name in
if has_var abs_prf then
replace_learned_clauses' (elet c↣proof↣local_pp_name c↣type actual_proof abs_prf) lcs
replace_learned_clauses' (elet c^.proof^.local_pp_name c^.type actual_proof abs_prf) lcs
else
replace_learned_clauses' proof lcs
meta def replace_learned_clauses (proof : proof_term) : solver proof_term :=
do st ← state_t.read, return $ replace_learned_clauses' proof st↣learned
do st ← state_t.read, return $ replace_learned_clauses' proof st^.learned
meta inductive result
| unsat : proof_term → result
@ -366,8 +366,8 @@ variable theory_solver : solver (option proof_term)
meta def unit_propg : unit → solver unit | () := do
st ← state_t.read,
if st↣conflict↣is_some then return () else
match st↣unitp_queue with
if st^.conflict^.is_some then return () else
match st^.unitp_queue with
| [] := return ()
| (v::vs) := do
state_t.write { st with unitp_queue := vs },
@ -378,28 +378,28 @@ end
private meta def run' : unit → solver result | () := do
unit_propg (),
st ← state_t.read,
match st↣conflict with
match st^.conflict with
| some conflict := do
conflict_clause ← analyze_conflict conflict,
if conflict_clause↣num_lits = 0 then do
proof ← replace_learned_clauses conflict_clause↣proof,
if conflict_clause^.num_lits = 0 then do
proof ← replace_learned_clauses conflict_clause^.proof,
return (result.unsat proof)
else do
backtrack_with conflict_clause,
add_learned conflict_clause,
run' ()
| none :=
match st↣unassigned↣min with
match st^.unassigned^.min with
| none := do
theory_conflict ← theory_solver,
match theory_conflict with
| some conflict := do set_conflict conflict, run' ()
| none := return $ result.sat (st↣vars↣for (λvar_st, var_st↣phase))
| none := return $ result.sat (st^.vars^.for (λvar_st, var_st^.phase))
end
| some unassigned :=
match st↣vars↣find unassigned with
match st^.vars^.find unassigned with
| some ⟨ph, none⟩ := do add_decision unassigned ph, run' ()
| _ := fail $ "unassigned variable is assigned: " ++ unassigned↣to_string
| _ := fail $ "unassigned variable is assigned: " ++ unassigned^.to_string
end
end
end
@ -408,6 +408,6 @@ meta def run : solver result := run' theory_solver ()
meta def solve (local_false : expr) (clauses : list clause) : tactic result := do
res ← (do for clauses mk_clause, run theory_solver) (state.initial local_false),
return res↣1
return res.1
end cdcl

54
library/tools/super/clause.lean
View file

@ -26,7 +26,7 @@ namespace clause
private meta def tactic_format (c : clause) : tactic format := do
prf_fmt : format ← pp (proof c),
type_fmt ← pp (type c),
loc_fls_fmt ← pp c↣local_false,
loc_fls_fmt ← pp c^.local_false,
return $ prf_fmt ++ to_fmt " : " ++ type_fmt ++ to_fmt " (" ++
to_fmt (num_quants c) ++ to_fmt " quants, "
++ to_fmt (num_lits c) ++ to_fmt " lits)"
@ -39,7 +39,7 @@ meta def inst (c : clause) (e : expr) : clause :=
(if num_quants c > 0
then mk (num_quants c - 1) (num_lits c)
else mk 0 (num_lits c - 1))
(app (proof c) e) (instantiate_var (binding_body (type c)) e) c↣local_false
(app (proof c) e) (instantiate_var (binding_body (type c)) e) c^.local_false
meta def instn (c : clause) (es : list expr) : clause :=
foldr (λe c', inst c' e) c es
@ -59,11 +59,11 @@ match e with
let abst_type' := abstract_local (type c) (local_uniq_name e) in
let type' := pi pp binder_info.default t (abstract_local (type c) uniq) in
let abs_prf := abstract_local (proof c) uniq in
let proof' := lambdas [e] c↣proof in
let proof' := lambdas [e] c^.proof in
if num_quants c > 0 ∨ has_var abst_type' then
{ c with num_quants := c↣num_quants + 1, proof := proof', type := type' }
{ c with num_quants := c^.num_quants + 1, proof := proof', type := type' }
else
{ c with num_lits := c↣num_lits + 1, proof := proof', type := type' }
{ c with num_lits := c^.num_lits + 1, proof := proof', type := type' }
| _ := ⟨0, 0, default expr, default expr, default expr⟩
end
@ -92,8 +92,8 @@ private meta def parse_clause (local_false : expr) : expr → expr → tactic cl
lc_n ← mk_fresh_name,
lc ← return $ local_const lc_n n bi d,
c ← parse_clause (app proof lc) (instantiate_var b lc),
return $ c↣close_const $ local_const lc_n n binder_info.default d
| proof (app (const ``not []) formula) := parse_clause proof (formula↣imp false_)
return $ c^.close_const $ local_const lc_n n binder_info.default d
| proof (app (const ``not []) formula) := parse_clause proof (formula^.imp false_)
| proof type :=
if type = local_false then do
return { num_quants := 0, num_lits := 0, proof := proof, type := type, local_false := local_false }
@ -133,7 +133,7 @@ meta def is_neg : literal → bool
| (left _) := tt
| (right _) := ff
meta def is_pos (l : literal) : bool := bnot l↣is_neg
meta def is_pos (l : literal) : bool := bnot l^.is_neg
meta def to_formula (l : literal) : tactic expr :=
if is_neg l then mk_mapp ``not [some (formula l)]
@ -145,30 +145,30 @@ meta def type_str : literal → string
meta instance : has_to_tactic_format literal :=
⟨λl, do
pp_f ← pp l↣formula,
return $ to_fmt l↣type_str ++ " (" ++ pp_f ++ ")"⟩
pp_f ← pp l^.formula,
return $ to_fmt l^.type_str ++ " (" ++ pp_f ++ ")"⟩
end literal
private meta def get_binding_body : expr → ℕ → expr
| e 0 := e
| e (i+1) := get_binding_body e↣binding_body i
| e (i+1) := get_binding_body e^.binding_body i
meta def get_binder (e : expr) (i : nat) :=
binding_domain (get_binding_body e i)
meta def validate (c : clause) : tactic unit := do
concl ← return $ get_binding_body c↣type c↣num_binders,
unify concl c↣local_false
<|> (do pp_concl ← pp concl, pp_lf ← pp c↣local_false,
concl ← return $ get_binding_body c^.type c^.num_binders,
unify concl c^.local_false
<|> (do pp_concl ← pp concl, pp_lf ← pp c^.local_false,
fail $ to_fmt "wrong local false: " ++ pp_concl ++ " =!= " ++ pp_lf),
type' ← infer_type c↣proof,
unify c↣type type' <|> (do pp_ty ← pp c↣type, pp_ty' ← pp type',
type' ← infer_type c^.proof,
unify c^.type type' <|> (do pp_ty ← pp c^.type, pp_ty' ← pp type',
fail (to_fmt "wrong type: " ++ pp_ty ++ " =!= " ++ pp_ty'))
meta def get_lit (c : clause) (i : nat) : literal :=
let bind := get_binder (type c) (num_quants c + i) in
match is_local_not c↣local_false bind with
match is_local_not c^.local_false bind with
| some formula := literal.right formula
| none := literal.left bind
end
@ -177,10 +177,10 @@ meta def lits_where (c : clause) (p : literal → bool) : list nat :=
list.filter (λl, p (get_lit c l)) (range (num_lits c))
meta def get_lits (c : clause) : list literal :=
list.map (get_lit c) (range c↣num_lits)
list.map (get_lit c) (range c^.num_lits)
meta def is_maximal (gt : expr → expr → bool) (c : clause) (i : nat) : bool :=
list.empty (list.filter (λj, gt (get_lit c j)↣formula (get_lit c i)↣formula) (range c↣num_lits))
list.empty (list.filter (λj, gt (get_lit c j)^.formula (get_lit c i)^.formula) (range c^.num_lits))
meta def normalize (c : clause) : tactic clause := do
opened ← open_constn c (num_binders c),
@ -195,9 +195,9 @@ meta def whnf_head_lit (c : clause) : tactic clause := do
atom' ← whnf $ literal.formula $ get_lit c 0,
return $
if literal.is_neg (get_lit c 0) then
{ c with type := imp atom' (binding_body c↣type) }
{ c with type := imp atom' (binding_body c^.type) }
else
{ c with type := imp (app (const ``not []) atom') c↣type↣binding_body }
{ c with type := imp (app (const ``not []) atom') c^.type^.binding_body }
end clause
@ -239,16 +239,16 @@ clause.inst_mvars $ clause.close_constn qf' bs
private meta def distinct' (local_false : expr) : list expr → expr → clause
| [] proof := ⟨ 0, 0, proof, local_false, local_false ⟩
| (h::hs) proof :=
let (dups, rest) := partition (λh' : expr, h↣local_type = h'↣local_type) hs,
let (dups, rest) := partition (λh' : expr, h^.local_type = h'^.local_type) hs,
proof_wo_dups := foldl (λproof (h' : expr),
instantiate_var (abstract_local proof h'↣local_uniq_name) h)
instantiate_var (abstract_local proof h'^.local_uniq_name) h)
proof dups in
(distinct' rest proof_wo_dups)↣close_const h
(distinct' rest proof_wo_dups)^.close_const h
meta def distinct (c : clause) : tactic clause := do
(qf, vs) ← c↣open_constn c↣num_quants,
(fls, hs) ← qf↣open_constn qf↣num_lits,
return $ (distinct' c↣local_false hs fls↣proof)↣close_constn vs
(qf, vs) ← c^.open_constn c^.num_quants,
(fls, hs) ← qf^.open_constn qf^.num_lits,
return $ (distinct' c^.local_false hs fls^.proof)^.close_constn vs
end clause

58
library/tools/super/clause_ops.lean
View file

@ -12,61 +12,61 @@ meta def on_left_at {m} [monad m] (c : clause) (i : ℕ)
[has_monad_lift_t tactic m]
-- f gets a type and returns a list of proofs of that type
(f : expr → m (list (list expr × expr))) : m (list clause) := do
op : clause × list expr ← ♯c↣open_constn (c↣num_quants + i),
♯ @guard tactic _ (op↣1↣get_lit 0)↣is_neg _,
new_hyps ← f (op↣1↣get_lit 0)↣formula,
return $ new_hyps↣for (λnew_hyp,
(op↣1↣inst new_hyp↣2)↣close_constn (op↣2 ++ new_hyp↣1))
op : clause × list expr ← ♯c^.open_constn (c^.num_quants + i),
♯ @guard tactic _ (op.1^.get_lit 0)^.is_neg _,
new_hyps ← f (op.1^.get_lit 0)^.formula,
return $ new_hyps^.for (λnew_hyp,
(op.1^.inst new_hyp.2)^.close_constn (op.2 ++ new_hyp.1))
meta def on_left_at_dn {m} [monad m] [alternative m] (c : clause) (i : ℕ)
[has_monad_lift_t tactic m]
-- f gets a hypothesis of ¬type and returns a list of proofs of false
(f : expr → m (list (list expr × expr))) : m (list clause) := do
qf : clause × list expr ← ♯c↣open_constn c↣num_quants,
op : clause × list expr ← ♯qf↣1↣open_constn c↣num_lits,
lci ← (op↣2↣nth i)↣to_monad,
♯ @guard tactic _ (qf↣1↣get_lit i)↣is_neg _,
h ← ♯ mk_local_def `h $ imp (qf↣1↣get_lit i)↣formula c↣local_false,
qf : clause × list expr ← ♯c^.open_constn c^.num_quants,
op : clause × list expr ← ♯qf.1^.open_constn c^.num_lits,
lci ← (op.2^.nth i)^.to_monad,
♯ @guard tactic _ (qf.1^.get_lit i)^.is_neg _,
h ← ♯ mk_local_def `h $ imp (qf.1^.get_lit i)^.formula c^.local_false,
new_hyps ← f h,
return $ new_hyps↣for $ λnew_hyp,
(((clause.mk 0 0 new_hyp↣2 c↣local_false c↣local_false)↣close_const h)↣inst
(op↣1↣close_const lci)↣proof)↣close_constn
(qf↣2 ++ op↣2↣remove_nth i ++ new_hyp↣1)
return $ new_hyps^.for $ λnew_hyp,
(((clause.mk 0 0 new_hyp.2 c^.local_false c^.local_false)^.close_const h)^.inst
(op.1^.close_const lci)^.proof)^.close_constn
(qf.2 ++ op.2^.remove_nth i ++ new_hyp.1)
meta def on_right_at {m} [monad m] (c : clause) (i : ℕ)
[has_monad_lift_t tactic m]
-- f gets a hypothesis and returns a list of proofs of false
(f : expr → m (list (list expr × expr))) : m (list clause) := do
op : clause × list expr ← ♯c↣open_constn (c↣num_quants + i),
♯ @guard tactic _ ((op↣1↣get_lit 0)↣is_pos) _,
h ← ♯ mk_local_def `h (op↣1↣get_lit 0)↣formula,
op : clause × list expr ← ♯c^.open_constn (c^.num_quants + i),
♯ @guard tactic _ ((op.1^.get_lit 0)^.is_pos) _,
h ← ♯ mk_local_def `h (op.1^.get_lit 0)^.formula,
new_hyps ← f h,
return $ new_hyps↣for (λnew_hyp,
(op↣1↣inst (lambdas [h] new_hyp↣2))↣close_constn (op↣2 ++ new_hyp↣1))
return $ new_hyps^.for (λnew_hyp,
(op.1^.inst (lambdas [h] new_hyp.2))^.close_constn (op.2 ++ new_hyp.1))
meta def on_right_at' {m} [monad m] (c : clause) (i : ℕ)
[has_monad_lift_t tactic m]
-- f gets a hypothesis and returns a list of proofs
(f : expr → m (list (list expr × expr))) : m (list clause) := do
op : clause × list expr ← ♯c↣open_constn (c↣num_quants + i),
♯ @guard tactic _ ((op↣1↣get_lit 0)↣is_pos) _,
h ← ♯ mk_local_def `h (op↣1↣get_lit 0)↣formula,
op : clause × list expr ← ♯c^.open_constn (c^.num_quants + i),
♯ @guard tactic _ ((op.1^.get_lit 0)^.is_pos) _,
h ← ♯ mk_local_def `h (op.1^.get_lit 0)^.formula,
new_hyps ← f h,
for new_hyps (λnew_hyp, do
type ← ♯ infer_type new_hyp↣2,
nh ← ♯ mk_local_def `nh $ imp type c↣local_false,
return $ (op↣1↣inst (lambdas [h] (app nh new_hyp↣2)))↣close_constn (op↣2 ++ new_hyp↣1 ++ [nh]))
type ← ♯ infer_type new_hyp.2,
nh ← ♯ mk_local_def `nh $ imp type c^.local_false,
return $ (op.1^.inst (lambdas [h] (app nh new_hyp.2)))^.close_constn (op.2 ++ new_hyp.1 ++ [nh]))
meta def on_first_right (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
first $ do i ← list.range c↣num_lits, [on_right_at c i f]
first $ do i ← list.range c^.num_lits, [on_right_at c i f]
meta def on_first_right' (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
first $ do i ← list.range c↣num_lits, [on_right_at' c i f]
first $ do i ← list.range c^.num_lits, [on_right_at' c i f]
meta def on_first_left (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
first $ do i ← list.range c↣num_lits, [on_left_at c i f]
first $ do i ← list.range c^.num_lits, [on_left_at c i f]
meta def on_first_left_dn (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
first $ do i ← list.range c↣num_lits, [on_left_at_dn c i f]
first $ do i ← list.range c^.num_lits, [on_left_at_dn c i f]
end super

62
library/tools/super/clausifier.lean
View file

@ -23,26 +23,26 @@ on_first_left c $ λtype, do
meta def inf_whnf_r (c : clause) : tactic (list clause) :=
on_first_right c $ λha, do
a' ← whnf_core transparency.reducible ha↣local_type,
guard $ a' ≠ ha↣local_type,
hna ← mk_local_def `hna (imp a' c↣local_false),
a' ← whnf_core transparency.reducible ha^.local_type,
guard $ a' ≠ ha^.local_type,
hna ← mk_local_def `hna (imp a' c^.local_false),
return [([hna], app hna ha)]
set_option eqn_compiler.max_steps 500
meta def inf_false_l (c : clause) : tactic (list clause) :=
first $ do i ← list.range c↣num_lits,
if c↣get_lit i = clause.literal.left false_
first $ do i ← list.range c^.num_lits,
if c^.get_lit i = clause.literal.left false_
then [return []]
else []
meta def inf_false_r (c : clause) : tactic (list clause) :=
on_first_right c $ λhf,
if hf↣local_type = c↣local_false
if hf^.local_type = c^.local_false
then return [([], hf)]
else match hf↣local_type with
else match hf^.local_type with
| const ``false [] := do
pr ← mk_app ``false.rec [c↣local_false, hf],
pr ← mk_app ``false.rec [c^.local_false, hf],
return [([], pr)]
| _ := failed
end
@ -55,8 +55,8 @@ on_first_left c $ λt,
end
meta def inf_true_r (c : clause) : tactic (list clause) :=
first $ do i ← list.range c↣num_lits,
if c↣get_lit i = clause.literal.right (const ``true [])
first $ do i ← list.range c^.num_lits,
if c^.get_lit i = clause.literal.right (const ``true [])
then [return []]
else []
@ -71,9 +71,9 @@ on_first_left c $ λtype,
meta def inf_not_r (c : clause) : tactic (list clause) :=
on_first_right c $ λhna,
match hna↣local_type with
match hna^.local_type with
| app (const ``not []) a := do
hnna ← mk_local_def `h (imp (imp a false_) c↣local_false),
hnna ← mk_local_def `h (imp (imp a false_) c^.local_false),
return [([hnna], app hnna hna)]
| _ := failed
end
@ -97,11 +97,11 @@ on_first_right' c $ λhyp, do
meta def inf_or_r (c : clause) : tactic (list clause) :=
on_first_right c $ λhab,
match hab↣local_type with
match hab^.local_type with
| (app (app (const ``or []) a) b) := do
hna ← mk_local_def `l (imp a c↣local_false),
hnb ← mk_local_def `r (imp b c↣local_false),
proof ← mk_app ``or.elim [a, b, c↣local_false, hab, hna, hnb],
hna ← mk_local_def `l (imp a c^.local_false),
hnb ← mk_local_def `r (imp b c^.local_false),
proof ← mk_app ``or.elim [a, b, c^.local_false, hab, hna, hnb],
return [([hna, hnb], proof)]
| _ := failed
end
@ -120,7 +120,7 @@ on_first_left c $ λab,
meta def inf_all_r (c : clause) : tactic (list clause) :=
on_first_right' c $ λhallb,
match hallb↣local_type with
match hallb^.local_type with
| (pi n bi a b) := do
ha ← mk_local_def `x a,
return [([ha], app hallb ha)]
@ -144,10 +144,10 @@ lemma imp_l_c {F : Prop} {a b} : ((a → b) → F) → ((a → F) → F) :=
meta def inf_imp_l (c : clause) : tactic (list clause) :=
on_first_left_dn c $ λhnab,
match hnab↣local_type with
match hnab^.local_type with
| (pi _ _ (pi _ _ a b) _) :=
if b↣has_var then failed else do
hna ← mk_local_def `na (imp a c↣local_false),
if b^.has_var then failed else do
hna ← mk_local_def `na (imp a c^.local_false),
pf ← first (do r ← [``super.imp_l, ``super.imp_l', ``super.imp_l_c],
[mk_app r [hnab, hna]]),
hb ← mk_local_def `b b,
@ -178,26 +178,26 @@ assume hab hnenb,
meta def inf_all_l (c : clause) : tactic (list clause) :=
on_first_left_dn c $ λhnallb,
match hnallb↣local_type with
match hnallb^.local_type with
| pi _ _ (pi n bi a b) _ := do
enb ← mk_mapp ``Exists [none, some $ lam n binder_info.default a (imp b c↣local_false)],
hnenb ← mk_local_def `h (imp enb c↣local_false),
enb ← mk_mapp ``Exists [none, some $ lam n binder_info.default a (imp b c^.local_false)],
hnenb ← mk_local_def `h (imp enb c^.local_false),
pr ← mk_app ``super.demorgan' [hnallb, hnenb],
return [([hnenb], pr)]
| _ := failed
end
meta def inf_ex_r (c : clause) : tactic (list clause) := do
(qf, ctx) ← c↣open_constn c↣num_quants,
(qf, ctx) ← c^.open_constn c^.num_quants,
skolemized ← on_first_right' qf $ λhexp,
match hexp↣local_type with
match hexp^.local_type with
| (app (app (const ``Exists [u]) d) p) := do
sk_sym_name_pp ← get_unused_name `sk (some 1),
inh_lc ← mk_local' `w binder_info.implicit d,
sk_sym ← mk_local_def sk_sym_name_pp (pis (ctx ++ [inh_lc]) d),
sk_p ← whnf_core transparency.none $ app p (app_of_list sk_sym (ctx ++ [inh_lc])),
sk_ax ← mk_mapp ``Exists [some (local_type sk_sym),
some (lambdas [sk_sym] (pis (ctx ++ [inh_lc]) (imp hexp↣local_type sk_p)))],
some (lambdas [sk_sym] (pis (ctx ++ [inh_lc]) (imp hexp^.local_type sk_p)))],
sk_ax_name ← get_unused_name `sk_axiom (some 1), assert sk_ax_name sk_ax,
nonempt_of_inh ← mk_mapp ``nonempty.intro [some d, some inh_lc],
eps ← mk_mapp ``classical.epsilon [some d, some nonempt_of_inh, some p],
@ -209,7 +209,7 @@ skolemized ← on_first_right' qf $ λhexp,
return [([inh_lc], app_of_list sk_ax' (ctx ++ [inh_lc, hexp]))]
| _ := failed
end,
return $ skolemized↣for (λs, s↣close_constn ctx)
return $ skolemized^.for (λs, s^.close_constn ctx)
meta def first_some {a : Type} : list (tactic (option a)) → tactic (option a)
| [] := return none
@ -219,7 +219,7 @@ private meta def get_clauses_core' (rules : list (clause → tactic (list clause
: list clause → tactic (list clause) | cs :=
lift list.join $ do
for cs $ λc, do first $
rules↣for (λr, r c >>= get_clauses_core') ++ [return [c]]
rules^.for (λr, r c >>= get_clauses_core') ++ [return [c]]
meta def get_clauses_core (rules : list (clause → tactic (list clause))) (initial : list clause)
: tactic (list clause) := do
@ -268,10 +268,10 @@ monad.for l (clause.of_proof local_false)
meta def clausification_inf : inf_decl := inf_decl.mk 0 $
λgiven, list.foldr orelse (return ()) $
do r ← clausification_rules_classical,
[do cs ← ♯ r given↣c,
[do cs ← ♯ r given^.c,
cs' ← ♯ get_clauses_classical cs,
for' cs' (λc, mk_derived c given↣sc↣sched_now >>= add_inferred),
remove_redundant given↣id []]
for' cs' (λc, mk_derived c given^.sc^.sched_now >>= add_inferred),
remove_redundant given^.id []]
end super

20
library/tools/super/datatypes.lean
View file

@ -11,12 +11,12 @@ namespace super
meta def has_diff_constr_eq_l (c : clause) : tactic bool := do
env ← get_env,
return $ list.bor $ do
l ← c↣get_lits,
guard l↣is_neg,
return $ match is_eq l↣formula with
l ← c^.get_lits,
guard l^.is_neg,
return $ match is_eq l^.formula with
| some (lhs, rhs) :=
if env↣is_constructor_app lhs ∧ env↣is_constructor_app rhs ∧
lhs↣get_app_fn↣const_name ≠ rhs↣get_app_fn↣const_name then
if env^.is_constructor_app lhs ∧ env^.is_constructor_app rhs ∧
lhs^.get_app_fn^.const_name ≠ rhs^.get_app_fn^.const_name then
tt
else
ff
@ -24,16 +24,16 @@ return $ list.bor $ do
end
meta def diff_constr_eq_l_pre := preprocessing_rule $
filter (λc, lift bnot $♯ has_diff_constr_eq_l c↣c)
filter (λc, lift bnot $♯ has_diff_constr_eq_l c^.c)
meta def try_no_confusion_eq_r (c : clause) (i : ℕ) : tactic (list clause) :=
on_right_at' c i $ λhyp,
match is_eq hyp↣local_type with
match is_eq hyp^.local_type with
| some (lhs, rhs) := do
env ← get_env,
lhs ← whnf lhs, rhs ← whnf rhs,
guard $ env↣is_constructor_app lhs ∧ env↣is_constructor_app rhs,
pr ← mk_app (lhs↣get_app_fn↣const_name↣get_prefix <.> "no_confusion") [false_, lhs, rhs, hyp],
guard $ env^.is_constructor_app lhs ∧ env^.is_constructor_app rhs,
pr ← mk_app (lhs^.get_app_fn^.const_name^.get_prefix <.> "no_confusion") [false_, lhs, rhs, hyp],
-- FIXME: change to local false ^^
ty ← infer_type pr, ty ← whnf ty,
pr ← to_expr `(@eq.mpr _ %%ty rfl %%pr), -- FIXME
@ -43,6 +43,6 @@ on_right_at' c i $ λhyp,
@[super.inf]
meta def datatype_infs : inf_decl := inf_decl.mk 10 $ take given, do
sequence' (do i ← list.range given↣c↣num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given↣c i])
sequence' (do i ← list.range given^.c^.num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given^.c i])
end super

8
library/tools/super/defs.lean
View file

@ -21,8 +21,8 @@ on_left_at c i $ λt, do
meta def try_unfold_def_right (c : clause) (i : ℕ) : tactic (list clause) :=
on_right_at c i $ λh, do
t' ← try_unfold_one_def h↣local_type,
hnt' ← mk_local_def `h (imp t' c↣local_false),
t' ← try_unfold_one_def h^.local_type,
hnt' ← mk_local_def `h (imp t' c^.local_false),
return [([hnt'], app hnt' h)]
@[super.inf]
@ -30,7 +30,7 @@ meta def unfold_def_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ d
r ← [try_unfold_def_right, try_unfold_def_left],
-- NOTE: we cannot restrict to selected literals here
-- as this might prevent factoring, e.g. _n>0_ ∨ is_pos(0)
i ← list.range given↣c↣num_lits,
[inf_if_successful 3 given (r given↣c i)]
i ← list.range given^.c^.num_lits,
[inf_if_successful 3 given (r given^.c i)]
end super

20
library/tools/super/equality.lean
View file

@ -10,33 +10,33 @@ namespace super
meta def try_unify_eq_l (c : clause) (i : nat) : tactic clause := do
guard $ clause.literal.is_neg (clause.get_lit c i),
qf ← clause.open_metan c c↣num_quants,
match is_eq (qf↣1↣get_lit i)↣formula with
qf ← clause.open_metan c c^.num_quants,
match is_eq (qf.1^.get_lit i)^.formula with
| none := failed
| some (lhs, rhs) := do
unify lhs rhs,
ty ← infer_type lhs,
univ ← infer_univ ty,
refl ← return $ app_of_list (const ``eq.refl [univ]) [ty, lhs],
opened ← clause.open_constn qf↣1 i,
clause.meta_closure qf↣2 $ clause.close_constn (opened↣1↣inst refl) opened↣2
opened ← clause.open_constn qf.1 i,
clause.meta_closure qf.2 $ clause.close_constn (opened.1^.inst refl) opened.2
end
@[super.inf]
meta def unify_eq_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do
i ← given↣selected,
[inf_if_successful 0 given (do u ← try_unify_eq_l given↣c i, return [u])]
i ← given^.selected,
[inf_if_successful 0 given (do u ← try_unify_eq_l given^.c i, return [u])]
meta def has_refl_r (c : clause) : bool :=
list.bor $ do
literal ← c↣get_lits,
guard literal↣is_pos,
match is_eq literal↣formula with
literal ← c^.get_lits,
guard literal^.is_pos,
match is_eq literal^.formula with
| some (lhs, rhs) := [decidable.to_bool (lhs = rhs)]
| none := []
end
meta def refl_r_pre : prover unit :=
preprocessing_rule $ take new, return $ filter (λc, ¬has_refl_r c↣c) new
preprocessing_rule $ take new, return $ filter (λc, ¬has_refl_r c^.c) new
end super

22
library/tools/super/factoring.lean
View file

@ -15,37 +15,37 @@ opened ← clause.open_constn c i,
return $ clause.close_constn (clause.inst opened.1 e) opened.2
private meta def try_factor' (c : clause) (i j : nat) : tactic clause := do
qf ← clause.open_metan c c↣num_quants,
unify_lit (qf↣1↣get_lit i) (qf↣1↣get_lit j),
qf ← clause.open_metan c c^.num_quants,
unify_lit (qf.1^.get_lit i) (qf.1^.get_lit j),
qfi ← clause.inst_mvars qf.1,
guard $ clause.is_maximal gt qfi i,
at_j ← clause.open_constn qf.1 j,
hyp_i ← option.to_monad (list.nth at_j.2 i),
clause.meta_closure qf↣2 $ (at_j↣1↣inst hyp_i)↣close_constn at_j↣2
clause.meta_closure qf.2 $ (at_j.1^.inst hyp_i)^.close_constn at_j.2
meta def try_factor (c : clause) (i j : nat) : tactic clause :=
if i > j then try_factor' gt c j i else try_factor' gt c i j
meta def try_infer_factor (c : derived_clause) (i j : nat) : prover unit := do
f ← ♯ try_factor gt c↣c i j,
ss ← ♯ does_subsume f c↣c,
f ← ♯ try_factor gt c^.c i j,
ss ← ♯ does_subsume f c^.c,
if ss then do
f ← mk_derived f c↣sc↣sched_now,
f ← mk_derived f c^.sc^.sched_now,
add_inferred f,
remove_redundant c↣id [f]
remove_redundant c^.id [f]
else do
inf_score 1 [c↣sc] >>= mk_derived f >>= add_inferred
inf_score 1 [c^.sc] >>= mk_derived f >>= add_inferred
@[super.inf]
meta def factor_inf : inf_decl := inf_decl.mk 40 $
take given, do gt ← get_term_order, sequence' $ do
i ← given↣selected,
j ← list.range given↣c↣num_lits,
i ← given^.selected,
j ← list.range given^.c^.num_lits,
return $ try_infer_factor gt given i j <|> return ()
meta def factor_dup_lits_pre := preprocessing_rule $ take new, do
♯ for new $ λdc, do
dist ← dc↣c↣distinct,
dist ← dc^.c^.distinct,
return { dc with c := dist }
end super

18
library/tools/super/inhabited.lean
View file

@ -10,15 +10,15 @@ namespace super
meta def try_nonempty_lookup_left (c : clause) : tactic (list clause) :=
on_first_left_dn c $ λhnx,
match is_local_not c↣local_false hnx↣local_type with
match is_local_not c^.local_false hnx^.local_type with
| some type := do
univ ← infer_univ type,
lf_univ ← infer_univ c↣local_false,
lf_univ ← infer_univ c^.local_false,
guard $ lf_univ = level.zero,
inst ← mk_instance (app (const ``nonempty [univ]) type),
instt ← infer_type inst,
return [([], app_of_list (const ``nonempty.elim [univ])
[type, c↣local_false, inst, hnx])]
[type, c^.local_false, inst, hnx])]
| _ := failed
end
@ -33,13 +33,13 @@ on_first_left c $ λprop,
meta def try_nonempty_right (c : clause) : tactic (list clause) :=
on_first_right c $ λhnonempty,
match hnonempty↣local_type with
match hnonempty^.local_type with
| (app (const ``nonempty [u]) type) := do
lf_univ ← infer_univ c↣local_false,
lf_univ ← infer_univ c^.local_false,
guard $ lf_univ = level.zero,
hnx ← mk_local_def `nx (imp type c↣local_false),
hnx ← mk_local_def `nx (imp type c^.local_false),
return [([hnx], app_of_list (const ``nonempty.elim [u])
[type, c↣local_false, hnonempty, hnx])]
[type, c^.local_false, hnonempty, hnx])]
| _ := failed
end
@ -54,7 +54,7 @@ on_first_left c $ λprop,
meta def try_inhabited_right (c : clause) : tactic (list clause) :=
on_first_right' c $ λhinh,
match hinh↣local_type with
match hinh^.local_type with
| (app (const ``inhabited [u]) type) :=
return [([], app_of_list (const ``inhabited.default [u]) [type, hinh])]
| _ := failed
@ -65,6 +65,6 @@ meta def inhabited_infs : inf_decl := inf_decl.mk 10 $ take given, do
for' [try_nonempty_lookup_left,
try_nonempty_left, try_nonempty_right,
try_inhabited_left, try_inhabited_right] $ λr,
simp_if_successful given (r given↣c)
simp_if_successful given (r given^.c)
end super

8
library/tools/super/misc_preprocessing.lean
View file

@ -9,20 +9,20 @@ open expr list monad
namespace super
meta def is_taut (c : clause) : tactic bool := do
qf ← c^.open_constn c↣num_quants,
qf ← c^.open_constn c^.num_quants,
return $ list.bor $ do
l1 ← qf^.1^.get_lits, guard l1^.is_neg,
l2 ← qf^.1^.get_lits, guard l2^.is_pos,
[decidable.to_bool $ l1^.formula = l2^.formula]
meta def tautology_removal_pre : prover unit :=
preprocessing_rule $ λnew, filter (λc, lift bnot $♯ is_taut c↣c) new
preprocessing_rule $ λnew, filter (λc, lift bnot $♯ is_taut c^.c) new
meta def remove_duplicates : list derived_clause → list derived_clause
| [] := []
| (c :: cs) :=
let (same_type, other_type) := partition (λc' : derived_clause, c'↣c↣type = c↣c↣type) cs in
{ c with sc := foldl score.min c↣sc (same_type↣for $ λc, c↣sc) } :: remove_duplicates other_type
let (same_type, other_type) := partition (λc' : derived_clause, c'^.c^.type = c^.c^.type) cs in
{ c with sc := foldl score.min c^.sc (same_type^.for $ λc, c^.sc) } :: remove_duplicates other_type
meta def remove_duplicates_pre : prover unit :=
preprocessing_rule $ λnew,

10
library/tools/super/prover.lean
View file

@ -45,16 +45,16 @@ meta def run_prover_loop
sequence' preprocessing_rules,
new ← take_newly_derived, for' new register_as_passive,
♯ when (is_trace_enabled_for `super) $ for' new $ λn,
tactic.trace { n with c := { (n↣c) with proof := const (mk_simple_name " derived") [] } },
needs_sat_run ← flip monad.lift state_t.read (λst, st↣needs_sat_run),
tactic.trace { n with c := { (n^.c) with proof := const (mk_simple_name " derived") [] } },
needs_sat_run ← flip monad.lift state_t.read (λst, st^.needs_sat_run),
if needs_sat_run then do
res ← do_sat_run,
match res with
| some proof := return (some proof)
| none := do
model ← flip monad.lift state_t.read (λst, st↣current_model),
model ← flip monad.lift state_t.read (λst, st^.current_model),
♯ when (is_trace_enabled_for `super) (do
pp_model ← pp (model↣to_list↣for (λlit, if lit↣2 = tt then lit↣1 else not_ lit↣1)),
pp_model ← pp (model^.to_list^.for (λlit, if lit.2 = tt then lit.1 else not_ lit.1)),
trace $ to_fmt "sat model: " ++ pp_model),
run_prover_loop i
end
@ -110,7 +110,7 @@ namespace tactic.interactive
meta def with_lemmas (ls : types.raw_ident_list) : tactic unit := monad.for' ls $ λl, do
p ← mk_const l,
t ← infer_type p,
n ← get_unused_name p↣get_app_fn↣const_name none,
n ← get_unused_name p^.get_app_fn^.const_name none,
tactic.assertv n t p
meta def super (extra_clause_names : types.raw_ident_list)

198
library/tools/super/prover_state.lean
View file

@ -22,27 +22,27 @@ def prio.never : ℕ := 2
def sched_default (sc : score) : score := { sc with priority := prio.default }
def sched_now (sc : score) : score := { sc with priority := prio.immediate }
def inc_cost (sc : score) (n : ℕ) : score := { sc with cost := sc↣cost + n }
def inc_cost (sc : score) (n : ℕ) : score := { sc with cost := sc^.cost + n }
def min (a b : score) : score :=
{ priority := nat.min a↣priority b↣priority,
in_sos := a↣in_sos && b↣in_sos,
cost := nat.min a↣cost b↣cost,
age := nat.min a↣age b↣age }
{ priority := nat.min a^.priority b^.priority,
in_sos := a^.in_sos && b^.in_sos,
cost := nat.min a^.cost b^.cost,
age := nat.min a^.age b^.age }
def combine (a b : score) : score :=
{ priority := nat.max a↣priority b↣priority,
in_sos := a↣in_sos && b↣in_sos,
cost := a↣cost + b↣cost,
age := nat.max a↣age b↣age }
{ priority := nat.max a^.priority b^.priority,
in_sos := a^.in_sos && b^.in_sos,
cost := a^.cost + b^.cost,
age := nat.max a^.age b^.age }
end score
namespace score
meta instance : has_to_string score :=
⟨λe, "[" ++ to_string e↣priority ++
"," ++ to_string e↣cost ++
"," ++ to_string e↣age ++
",sos=" ++ to_string e↣in_sos ++ "]"⟩
⟨λe, "[" ++ to_string e^.priority ++
"," ++ to_string e^.cost ++
"," ++ to_string e^.age ++
",sos=" ++ to_string e^.in_sos ++ "]"⟩
end score
def clause_id := ℕ
@ -63,17 +63,17 @@ namespace derived_clause
meta instance : has_to_tactic_format derived_clause :=
⟨λc, do
c_fmt ← pp c↣c,
ass_fmt ← pp (c↣assertions↣for (λa, a↣local_type)),
c_fmt ← pp c^.c,
ass_fmt ← pp (c^.assertions^.for (λa, a^.local_type)),
return $
to_string c↣sc ++ " " ++
to_string c^.sc ++ " " ++
c_fmt ++ " <- " ++ ass_fmt ++
" (selected: " ++ to_fmt c↣selected ++
" (selected: " ++ to_fmt c^.selected ++
")"
⟩
meta def clause_with_assertions (ac : derived_clause) : clause :=
ac↣c↣close_constn ac↣assertions
ac^.c^.close_constn ac^.assertions
end derived_clause
@ -85,8 +85,8 @@ namespace locked_clause
meta instance : has_to_tactic_format locked_clause :=
⟨λc, do
c_fmt ← pp c↣dc,
reasons_fmt ← pp (c↣reasons↣for (λr, r↣for (λa, a↣local_type))),
c_fmt ← pp c^.dc,
reasons_fmt ← pp (c^.reasons^.for (λr, r^.for (λa, a^.local_type))),
return $ c_fmt ++ " (locked in case of: " ++ reasons_fmt ++ ")"
⟩
@ -111,12 +111,12 @@ private meta def join_with_nl : list format → format :=
list.foldl (λx y, x ++ format.line ++ y) format.nil
private meta def prover_state_tactic_fmt (s : prover_state) : tactic format := do
active_fmts ← mapm pp $ rb_map.values s↣active,
passive_fmts ← mapm pp $ rb_map.values s↣passive,
new_fmts ← mapm pp s↣newly_derived,
locked_fmts ← mapm pp s↣locked,
sat_fmts ← mapm pp s↣sat_solver↣clauses,
prec_fmts ← mapm pp s↣prec,
active_fmts ← mapm pp $ rb_map.values s^.active,
passive_fmts ← mapm pp $ rb_map.values s^.passive,
new_fmts ← mapm pp s^.newly_derived,
locked_fmts ← mapm pp s^.locked,
sat_fmts ← mapm pp s^.sat_solver^.clauses,
prec_fmts ← mapm pp s^.prec,
return (join_with_nl
([to_fmt "active:"] ++ map (append (to_fmt " ")) active_fmts ++
[to_fmt "passive:"] ++ map (append (to_fmt " ")) passive_fmts ++
@ -150,21 +150,21 @@ alternative.mk (@monad.map _ _)
meta def selection_strategy := derived_clause → prover derived_clause
meta def get_active : prover (rb_map clause_id derived_clause) :=
do state ← state_t.read, return state↣active
do state ← state_t.read, return state^.active
meta def add_active (a : derived_clause) : prover unit :=
do state ← state_t.read,
state_t.write { state with active := state↣active↣insert a↣id a }
state_t.write { state with active := state^.active^.insert a^.id a }
meta def get_passive : prover (rb_map clause_id derived_clause) :=
lift passive state_t.read
meta def get_precedence : prover (list expr) :=
do state ← state_t.read, return state↣prec
do state ← state_t.read, return state^.prec
meta def get_term_order : prover (expr → expr → bool) := do
state ← state_t.read,
return $ lpo (prec_gt_of_name_list (map name_of_funsym state↣prec))
return $ lpo (prec_gt_of_name_list (map name_of_funsym state^.prec))
private meta def set_precedence (new_prec : list expr) : prover unit :=
do state ← state_t.read, state_t.write { state with prec := new_prec }
@ -172,31 +172,31 @@ do state ← state_t.read, state_t.write { state with prec := new_prec }
meta def register_consts_in_precedence (consts : list expr) := do
p ← get_precedence,
p_set ← return (rb_map.set_of_list (map name_of_funsym p)),
new_syms ← return $ list.filter (λc, ¬p_set↣contains (name_of_funsym c)) consts,
new_syms ← return $ list.filter (λc, ¬p_set^.contains (name_of_funsym c)) consts,
set_precedence (new_syms ++ p)
meta def in_sat_solver {A} (cmd : cdcl.solver A) : prover A := do
state ← state_t.read,
result ← ♯ cmd state↣sat_solver,
state_t.write { state with sat_solver := result↣2 },
return result↣1
result ← ♯ cmd state^.sat_solver,
state_t.write { state with sat_solver := result.2 },
return result.1
meta def collect_ass_hyps (c : clause) : prover (list expr) :=
let lcs := contained_lconsts c↣proof in
let lcs := contained_lconsts c^.proof in
do st ← state_t.read,
return (do
hs ← st↣sat_hyps↣values,
h ← [hs↣1, hs↣2],
guard $ lcs↣contains h↣local_uniq_name,
hs ← st^.sat_hyps^.values,
h ← [hs.1, hs.2],
guard $ lcs^.contains h^.local_uniq_name,
[h])
meta def get_clause_count : prover ℕ :=
do s ← state_t.read, return s↣clause_counter
do s ← state_t.read, return s^.clause_counter
meta def get_new_cls_id : prover clause_id := do
state ← state_t.read,
state_t.write { state with clause_counter := state↣clause_counter + 1 },
return state↣clause_counter
state_t.write { state with clause_counter := state^.clause_counter + 1 },
return state^.clause_counter
meta def mk_derived (c : clause) (sc : score) : prover derived_clause := do
ass ← collect_ass_hyps c,
@ -204,31 +204,31 @@ id ← ♯ get_new_cls_id,
return { id := id, c := c, selected := [], assertions := ass, sc := sc }
meta def add_inferred (c : derived_clause) : prover unit := do
c' ← ♯c↣c↣normalize, c' ← return { c with c := c' },
register_consts_in_precedence (contained_funsyms c'↣c↣type)↣values,
c' ← ♯c^.c^.normalize, c' ← return { c with c := c' },
register_consts_in_precedence (contained_funsyms c'^.c^.type)^.values,
state ← state_t.read,
state_t.write { state with newly_derived := c' :: state↣newly_derived }
state_t.write { state with newly_derived := c' :: state^.newly_derived }
-- FIXME: what if we've seen the variable before, but with a weaker score?
meta def mk_sat_var (v : expr) (suggested_ph : bool) (suggested_ev : score) : prover unit :=
do st ← state_t.read, if st↣sat_hyps↣contains v then return () else do
do st ← state_t.read, if st^.sat_hyps^.contains v then return () else do
hpv ← ♯ mk_local_def `h v,
hnv ← ♯ mk_local_def `hn $ imp v st↣local_false,
state_t.modify $ λst, { st with sat_hyps := st↣sat_hyps↣insert v (hpv, hnv) },
hnv ← ♯ mk_local_def `hn $ imp v st^.local_false,
state_t.modify $ λst, { st with sat_hyps := st^.sat_hyps^.insert v (hpv, hnv) },
in_sat_solver $ cdcl.mk_var_core v suggested_ph,
match v with
| (pi _ _ _ _) := do
c ← ♯ clause.of_proof st↣local_false hpv,
c ← ♯ clause.of_proof st^.local_false hpv,
mk_derived c suggested_ev >>= add_inferred
| _ := do cp ← ♯ clause.of_proof st↣local_false hpv, mk_derived cp suggested_ev >>= add_inferred,
cn ← ♯ clause.of_proof st↣local_false hnv, mk_derived cn suggested_ev >>= add_inferred
| _ := do cp ← ♯ clause.of_proof st^.local_false hpv, mk_derived cp suggested_ev >>= add_inferred,
cn ← ♯ clause.of_proof st^.local_false hnv, mk_derived cn suggested_ev >>= add_inferred
end
meta def get_sat_hyp_core (v : expr) (ph : bool) : prover (option expr) :=
flip monad.lift state_t.read $ λst,
match st↣sat_hyps↣find v with
match st^.sat_hyps^.find v with
| some (hp, hn) := some $ if ph then hp else hn
| none := none
end
@ -237,30 +237,30 @@ meta def get_sat_hyp (v : expr) (ph : bool) : prover expr :=
do hyp_opt ← get_sat_hyp_core v ph,
match hyp_opt with
| some hyp := return hyp
| none := prover.fail $ "unknown sat variable: " ++ v↣to_string
| none := prover.fail $ "unknown sat variable: " ++ v^.to_string
end
meta def add_sat_clause (c : clause) (suggested_ev : score) : prover unit := do
c ← ♯ c↣distinct,
c ← ♯ c^.distinct,
already_added ← flip monad.lift state_t.read $ λst, decidable.to_bool $
c↣type ∈ st↣sat_solver↣clauses↣for (λd, d↣type),
c^.type ∈ st^.sat_solver^.clauses^.for (λd, d^.type),
if already_added then return () else do
for c↣get_lits $ λl, mk_sat_var l↣formula l↣is_neg suggested_ev,
for c^.get_lits $ λl, mk_sat_var l^.formula l^.is_neg suggested_ev,
in_sat_solver $ cdcl.mk_clause c,
state_t.modify $ λst, { st with needs_sat_run := tt }
meta def sat_eval_lit (v : expr) (pol : bool) : prover bool :=
do v_st ← flip monad.lift state_t.read $ λst, st↣current_model↣find v,
do v_st ← flip monad.lift state_t.read $ λst, st^.current_model^.find v,
match v_st with
| some ph := return $ if pol then ph else bnot ph
| none := return tt
end
meta def sat_eval_assertion (assertion : expr) : prover bool :=
do lf ← flip monad.lift state_t.read $ λst, st↣local_false,
match is_local_not lf assertion↣local_type with
do lf ← flip monad.lift state_t.read $ λst, st^.local_false,
match is_local_not lf assertion^.local_type with
| some v := sat_eval_lit v ff
| none := sat_eval_lit assertion↣local_type tt
| none := sat_eval_lit assertion^.local_type tt
end
meta def sat_eval_assertions : list expr → prover bool
@ -272,33 +272,33 @@ return ff
| [] := return tt
private meta def intern_clause (c : derived_clause) : prover derived_clause := do
hyp_name ← ♯ get_unused_name (mk_simple_name $ "clause_" ++ to_string c↣id↣to_nat) none,
c' ← return $ c↣c↣close_constn c↣assertions,
♯ assertv hyp_name c'↣type c'↣proof,
hyp_name ← ♯ get_unused_name (mk_simple_name $ "clause_" ++ to_string c^.id^.to_nat) none,
c' ← return $ c^.c^.close_constn c^.assertions,
♯ assertv hyp_name c'^.type c'^.proof,
proof' ← ♯ get_local hyp_name,
type ← ♯ infer_type proof', -- FIXME: otherwise ""
return { c with c := { (c↣c : clause) with proof := app_of_list proof' c↣assertions } }
return { c with c := { (c^.c : clause) with proof := app_of_list proof' c^.assertions } }
meta def register_as_passive (c : derived_clause) : prover unit := do
c ← intern_clause c,
ass_v ← sat_eval_assertions c↣assertions,
if c↣c↣num_quants = 0 ∧ c↣c↣num_lits = 0 then
add_sat_clause c↣clause_with_assertions c↣sc
ass_v ← sat_eval_assertions c^.assertions,
if c^.c^.num_quants = 0 ∧ c^.c^.num_lits = 0 then
add_sat_clause c^.clause_with_assertions c^.sc
else if ¬ass_v then do
state_t.modify $ λst, { st with locked := ⟨c, []⟩ :: st↣locked }
state_t.modify $ λst, { st with locked := ⟨c, []⟩ :: st^.locked }
else do
state_t.modify $ λst, { st with passive := st↣passive↣insert c↣id c }
state_t.modify $ λst, { st with passive := st^.passive^.insert c^.id c }
meta def remove_passive (id : clause_id) : prover unit :=
do state ← state_t.read, state_t.write { state with passive := state↣passive↣erase id }
do state ← state_t.read, state_t.write { state with passive := state^.passive^.erase id }
meta def move_locked_to_passive : prover unit := do
locked ← flip monad.lift state_t.read (λst, st↣locked),
locked ← flip monad.lift state_t.read (λst, st^.locked),
new_locked ← flip filter locked (λlc, do
reason_vals ← mapm sat_eval_assertions lc↣reasons,
c_val ← sat_eval_assertions lc↣dc↣assertions,
if reason_vals↣for_all (λr, r = ff) ∧ c_val then do
state_t.modify $ λst, { st with passive := st↣passive↣insert lc↣dc↣id lc↣dc },
reason_vals ← mapm sat_eval_assertions lc^.reasons,
c_val ← sat_eval_assertions lc^.dc^.assertions,
if reason_vals^.for_all (λr, r = ff) ∧ c_val then do
state_t.modify $ λst, { st with passive := st^.passive^.insert lc^.dc^.id lc^.dc },
return ff
else
return tt
@ -306,23 +306,23 @@ new_locked ← flip filter locked (λlc, do
state_t.modify $ λst, { st with locked := new_locked }
meta def move_active_to_locked : prover unit :=
do active ← get_active, for' active↣values $ λac, do
c_val ← sat_eval_assertions ac↣assertions,
do active ← get_active, for' active^.values $ λac, do
c_val ← sat_eval_assertions ac^.assertions,
if ¬c_val then do
state_t.modify $ λst, { st with
active := st↣active↣erase ac↣id,
locked := ⟨ac, []⟩ :: st↣locked
active := st^.active^.erase ac^.id,
locked := ⟨ac, []⟩ :: st^.locked
}
else
return ()
meta def move_passive_to_locked : prover unit :=
do passive ← flip monad.lift state_t.read $ λst, st↣passive, for' passive↣to_list $ λpc, do
c_val ← sat_eval_assertions pc↣2↣assertions,
do passive ← flip monad.lift state_t.read $ λst, st^.passive, for' passive^.to_list $ λpc, do
c_val ← sat_eval_assertions pc.2^.assertions,
if ¬c_val then do
state_t.modify $ λst, { st with
passive := st↣passive↣erase pc↣1,
locked := ⟨pc↣2, []⟩ :: st↣locked
passive := st^.passive^.erase pc.1,
locked := ⟨pc.2, []⟩ :: st^.locked
}
else
return ()
@ -344,21 +344,21 @@ end
meta def take_newly_derived : prover (list derived_clause) := do
state ← state_t.read,
state_t.write { state with newly_derived := [] },
return state↣newly_derived
return state^.newly_derived
meta def remove_redundant (id : clause_id) (parents : list derived_clause) : prover unit := do
guard $ parents↣for_all $ λp, p↣id ≠ id,
red ← flip monad.lift state_t.read (λst, st↣active↣find id),
guard $ parents^.for_all $ λp, p^.id ≠ id,
red ← flip monad.lift state_t.read (λst, st^.active^.find id),
match red with
| none := return ()
| some red := do
let reasons := parents↣for (λp, p↣assertions),
assertion := red↣assertions in
if reasons↣for_all $ λr, r↣subset_of assertion then do
state_t.modify $ λst, { st with active := st↣active↣erase id }
let reasons := parents^.for (λp, p^.assertions),
assertion := red^.assertions in
if reasons^.for_all $ λr, r^.subset_of assertion then do
state_t.modify $ λst, { st with active := st^.active^.erase id }
else do
state_t.modify $ λst, { st with active := st↣active↣erase id,
locked := ⟨red, reasons⟩ :: st↣locked }
state_t.modify $ λst, { st with active := st^.active^.erase id,
locked := ⟨red, reasons⟩ :: st^.locked }
end
meta def inference := derived_clause → prover unit
@ -372,7 +372,7 @@ meta def seq_inferences : list inference → inference
| (inf::infs) := λgiven, do
inf given,
now_active ← get_active,
if rb_map.contains now_active given↣id then
if rb_map.contains now_active given^.id then
seq_inferences infs given
else
return ()
@ -381,15 +381,15 @@ meta def simp_inference (simpl : derived_clause → prover (option clause)) : in
λgiven, do maybe_simpld ← simpl given,
match maybe_simpld with
| some simpld := do
derived_simpld ← mk_derived simpld given↣sc↣sched_now,
derived_simpld ← mk_derived simpld given^.sc^.sched_now,
add_inferred derived_simpld,
remove_redundant given↣id []
remove_redundant given^.id []
| none := return ()
end
meta def preprocessing_rule (f : list derived_clause → prover (list derived_clause)) : prover unit := do
state ← state_t.read,
newly_derived' ← f state↣newly_derived,
newly_derived' ← f state^.newly_derived,
state' ← state_t.read,
state_t.write { state' with newly_derived := newly_derived' }
@ -406,7 +406,7 @@ meta def empty (local_false : expr) : prover_state :=
meta def initial (local_false : expr) (clauses : list clause) : tactic prover_state := do
after_setup ← for' clauses (λc,
let in_sos := decidable.to_bool ((contained_lconsts c↣proof)↣size = 0) in
let in_sos := decidable.to_bool ((contained_lconsts c^.proof)^.size = 0) in
do mk_derived c { priority := score.prio.immediate, in_sos := in_sos,
age := 0, cost := 0 } >>= add_inferred
) $ empty local_false,
@ -425,14 +425,14 @@ return $ list.foldl score.combine { priority := score.prio.default,
meta def inf_if_successful (add_cost : ℕ) (parent : derived_clause) (tac : tactic (list clause)) : prover unit :=
(do inferred ← ♯tac,
for' inferred $ λc,
inf_score add_cost [parent↣sc] >>= mk_derived c >>= add_inferred)
inf_score add_cost [parent^.sc] >>= mk_derived c >>= add_inferred)
<|> return ()
meta def simp_if_successful (parent : derived_clause) (tac : tactic (list clause)) : prover unit :=
(do inferred ← ♯tac,
for' inferred $ λc,
mk_derived c parent↣sc↣sched_now >>= add_inferred,
remove_redundant parent↣id [])
mk_derived c parent^.sc^.sched_now >>= add_inferred,
remove_redundant parent^.id [])
<|> return ()
end super

40
library/tools/super/resolution.lean
View file

@ -16,43 +16,43 @@ variables (i1 i2 : nat)
-- c1 : ... → ¬a → ...
-- c2 : ... → a → ...
meta def try_resolve : tactic clause := do
qf1 ← c1↣open_metan c1↣num_quants,
qf2 ← c2↣open_metan c2↣num_quants,
qf1 ← c1^.open_metan c1^.num_quants,
qf2 ← c2^.open_metan c2^.num_quants,
-- FIXME: using default transparency unifies m*n with (x*y*z)*w here ???
unify_core transparency.reducible (qf1↣1↣get_lit i1)↣formula (qf2↣1↣get_lit i2)↣formula,
qf1i ← qf1↣1↣inst_mvars,
unify_core transparency.reducible (qf1.1^.get_lit i1)^.formula (qf2.1^.get_lit i2)^.formula,
qf1i ← qf1.1^.inst_mvars,
guard $ clause.is_maximal gt qf1i i1,
op1 ← qf1↣1↣open_constn i1,
op2 ← qf2↣1↣open_constn c2↣num_lits,
a_in_op2 ← (op2↣2↣nth i2)↣to_monad,
op1 ← qf1.1^.open_constn i1,
op2 ← qf2.1^.open_constn c2^.num_lits,
a_in_op2 ← (op2.2^.nth i2)^.to_monad,
clause.meta_closure (qf1.2 ++ qf2.2) $
(op1↣1↣inst (op2↣1↣close_const a_in_op2)↣proof)↣close_constn (op1↣2 ++ op2↣2↣remove_nth i2)
(op1.1^.inst (op2.1^.close_const a_in_op2)^.proof)^.close_constn (op1.2 ++ op2.2^.remove_nth i2)
meta def try_add_resolvent : prover unit := do
c' ← ♯ try_resolve gt ac1↣c ac2↣c i1 i2,
inf_score 1 [ac1↣sc, ac2↣sc] >>= mk_derived c' >>= add_inferred
c' ← ♯ try_resolve gt ac1^.c ac2^.c i1 i2,
inf_score 1 [ac1^.sc, ac2^.sc] >>= mk_derived c' >>= add_inferred
meta def maybe_add_resolvent : prover unit :=
try_add_resolvent gt ac1 ac2 i1 i2 <|> return ()
meta def resolution_left_inf : inference :=
take given, do active ← get_active, sequence' $ do
given_i ← given↣selected,
guard $ clause.literal.is_neg (given↣c↣get_lit given_i),
given_i ← given^.selected,
guard $ clause.literal.is_neg (given^.c^.get_lit given_i),
other ← rb_map.values active,
guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
other_i ← other↣selected,
guard $ clause.literal.is_pos (other↣c↣get_lit other_i),
guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
other_i ← other^.selected,
guard $ clause.literal.is_pos (other^.c^.get_lit other_i),
[maybe_add_resolvent gt other given other_i given_i]
meta def resolution_right_inf : inference :=
take given, do active ← get_active, sequence' $ do
given_i ← given↣selected,
guard $ clause.literal.is_pos (given↣c↣get_lit given_i),
given_i ← given^.selected,
guard $ clause.literal.is_pos (given^.c^.get_lit given_i),
other ← rb_map.values active,
guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
other_i ← other↣selected,
guard $ clause.literal.is_neg (other↣c↣get_lit other_i),
guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
other_i ← other^.selected,
guard $ clause.literal.is_neg (other^.c^.get_lit other_i),
[maybe_add_resolvent gt given other given_i other_i]
@[super.inf]

30
library/tools/super/selection.lean
View file

@ -9,25 +9,25 @@ namespace super
meta def simple_selection_strategy (f : (expr → expr → bool) → clause → list ℕ) : selection_strategy :=
take dc, do gt ← get_term_order, return $
if dc↣selected↣empty ∧ dc↣c↣num_lits > 0
then { dc with selected := f gt dc↣c }
if dc^.selected^.empty ∧ dc^.c^.num_lits > 0
then { dc with selected := f gt dc^.c }
else dc
meta def dumb_selection : selection_strategy :=
simple_selection_strategy $ λgt c,
match c↣lits_where clause.literal.is_neg with
| [] := list.range c↣num_lits
match c^.lits_where clause.literal.is_neg with
| [] := list.range c^.num_lits
| neg_lit::_ := [neg_lit]
end
meta def selection21 : selection_strategy :=
simple_selection_strategy $ λgt c,
let maximal_lits := list.filter_maximal (λi j,
gt (c↣get_lit i)↣formula (c↣get_lit j)↣formula) (list.range c↣num_lits) in
gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) (list.range c^.num_lits) in
if list.length maximal_lits = 1 then maximal_lits else
let neg_lits := list.filter (λi, (c↣get_lit i)↣is_neg) (list.range c↣num_lits),
let neg_lits := list.filter (λi, (c^.get_lit i)^.is_neg) (list.range c^.num_lits),
maximal_neg_lits := list.filter_maximal (λi j,
gt (c↣get_lit i)↣formula (c↣get_lit j)↣formula) neg_lits in
gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) neg_lits in
if ¬maximal_neg_lits^.empty then
list.taken 1 maximal_neg_lits
else
@ -36,20 +36,20 @@ else
meta def selection22 : selection_strategy :=
simple_selection_strategy $ λgt c,
let maximal_lits := list.filter_maximal (λi j,
gt (c↣get_lit i)↣formula (c↣get_lit j)↣formula) (list.range c↣num_lits),
maximal_lits_neg := list.filter (λi, (c↣get_lit i)↣is_neg) maximal_lits in
gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) (list.range c^.num_lits),
maximal_lits_neg := list.filter (λi, (c^.get_lit i)^.is_neg) maximal_lits in
if ¬maximal_lits_neg^.empty then
list.taken 1 maximal_lits_neg
else
maximal_lits
meta def clause_weight (c : derived_clause) : nat :=
(c↣c↣get_lits↣for (λl, expr_size l↣formula + if l↣is_pos then 10 else 1))↣sum
(c^.c^.get_lits^.for (λl, expr_size l^.formula + if l^.is_pos then 10 else 1))^.sum
meta def find_minimal_by (passive : rb_map clause_id derived_clause)
{A} [has_ordering A]
(f : derived_clause → A) : clause_id :=
match rb_map.min $ rb_map.of_list $ passive↣values↣for $ λc, (f c, c↣id) with
match rb_map.min $ rb_map.of_list $ passive^.values^.for $ λc, (f c, c^.id) with
| some id := id
| none := nat.zero
end
@ -59,16 +59,16 @@ meta def age_of_clause_id : name → ℕ
| _ := 0
meta def find_minimal_weight (passive : rb_map clause_id derived_clause) : clause_id :=
find_minimal_by passive $ λc, (c↣sc↣priority, clause_weight c + c↣sc↣cost, c↣sc↣age, c↣id)
find_minimal_by passive $ λc, (c^.sc^.priority, clause_weight c + c^.sc^.cost, c^.sc^.age, c^.id)
meta def find_minimal_age (passive : rb_map clause_id derived_clause) : clause_id :=
find_minimal_by passive $ λc, (c↣sc↣priority, c↣sc↣age, c↣id)
find_minimal_by passive $ λc, (c^.sc^.priority, c^.sc^.age, c^.id)
meta def weight_clause_selection : clause_selection_strategy :=
take iter, do state ← state_t.read, return $ find_minimal_weight state↣passive
take iter, do state ← state_t.read, return $ find_minimal_weight state^.passive
meta def oldest_clause_selection : clause_selection_strategy :=
take iter, do state ← state_t.read, return $ find_minimal_age state↣passive
take iter, do state ← state_t.read, return $ find_minimal_age state^.passive
meta def age_weight_clause_selection (thr mod : ℕ) : clause_selection_strategy :=
take iter, if iter % mod < thr then

8
library/tools/super/simp.lean
View file

@ -17,7 +17,7 @@ meta def simplify_capturing_assumptions (type : expr) : tactic (expr × expr ×
(type', heq) ← simplify default_simplify_config [] type,
hyps ← return $ contained_lconsts type,
hyps' ← return $ contained_lconsts_list [type', heq],
add_hyps ← return $ list.filter (λn : expr, ¬hyps↣contains n↣local_uniq_name) hyps'↣values,
add_hyps ← return $ list.filter (λn : expr, ¬hyps^.contains n^.local_uniq_name) hyps'^.values,
return (type', heq, add_hyps)
meta def try_simplify_left (c : clause) (i : ℕ) : tactic (list clause) :=
@ -29,7 +29,7 @@ on_left_at c i $ λtype, do
meta def try_simplify_right (c : clause) (i : ℕ) : tactic (list clause) :=
on_right_at' c i $ λhyp, do
(type', heq, add_hyps) ← simplify_capturing_assumptions hyp↣local_type,
(type', heq, add_hyps) ← simplify_capturing_assumptions hyp^.local_type,
heqtype ← infer_type heq,
heqsymm ← mk_app ``eq.symm [heq],
prf ← mk_app ``eq.mpr [heqsymm, hyp],
@ -38,7 +38,7 @@ on_right_at' c i $ λhyp, do
@[super.inf]
meta def simp_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do
r ← [try_simplify_right, try_simplify_left],
i ← list.range given↣c↣num_lits,
[inf_if_successful 2 given (r given↣c i)]
i ← list.range given^.c^.num_lits,
[inf_if_successful 2 given (r given^.c i)]
end super

56
library/tools/super/splitting.lean
View file

@ -11,57 +11,57 @@ namespace super
private meta def find_components : list expr → list (list (expr × ℕ)) → list (list (expr × ℕ))
| (e::es) comps :=
let (contain_e, do_not_contain_e) :=
partition (λc : list (expr × ℕ), c↣exists_ $ λf,
(abstract_local f↣1 e↣local_uniq_name)↣has_var) comps in
partition (λc : list (expr × ℕ), c^.exists_ $ λf,
(abstract_local f.1 e^.local_uniq_name)^.has_var) comps in
find_components es $ list.join contain_e :: do_not_contain_e
| _ comps := comps
meta def get_components (hs : list expr) : list (list expr) :=
(find_components hs (hs↣zip_with_index↣for $ λh, [h]))↣for $ λc,
(sort_on (λh : expr × ℕ, h↣2) c)↣for $ λh, h↣1
(find_components hs (hs^.zip_with_index^.for $ λh, [h]))^.for $ λc,
(sort_on (λh : expr × ℕ, h.2) c)^.for $ λh, h.1
meta def extract_assertions : clause → prover (clause × list expr) | c :=
if c↣num_lits = 0 then return (c, [])
else if c↣num_quants ≠ 0 then do
qf ← ♯ c↣open_constn c↣num_quants,
qf_wo_as ← extract_assertions qf↣1,
return (qf_wo_as↣1↣close_constn qf↣2, qf_wo_as↣2)
if c^.num_lits = 0 then return (c, [])
else if c^.num_quants ≠ 0 then do
qf ← ♯ c^.open_constn c^.num_quants,
qf_wo_as ← extract_assertions qf.1,
return (qf_wo_as.1^.close_constn qf.2, qf_wo_as.2)
else do
hd ← return $ c↣get_lit 0,
hyp_opt ← get_sat_hyp_core hd↣formula hd↣is_neg,
hd ← return $ c^.get_lit 0,
hyp_opt ← get_sat_hyp_core hd^.formula hd^.is_neg,
match hyp_opt with
| some h := do
wo_as ← extract_assertions (c↣inst h),
return (wo_as↣1, h :: wo_as↣2)
wo_as ← extract_assertions (c^.inst h),
return (wo_as.1, h :: wo_as.2)
| _ := do
op ← ♯c↣open_const,
op_wo_as ← extract_assertions op↣1,
return (op_wo_as↣1↣close_const op↣2, op_wo_as↣2)
op ← ♯c^.open_const,
op_wo_as ← extract_assertions op.1,
return (op_wo_as.1^.close_const op.2, op_wo_as.2)
end
meta def mk_splitting_clause' (empty_clause : clause) : list (list expr) → tactic (list expr × expr)
| [] := return ([], empty_clause↣proof)
| ([p] :: comps) := do p' ← mk_splitting_clause' comps, return (p::p'↣1, p'↣2)
| [] := return ([], empty_clause^.proof)
| ([p] :: comps) := do p' ← mk_splitting_clause' comps, return (p::p'.1, p'.2)
| (comp :: comps) := do
(hs, p') ← mk_splitting_clause' comps,
hnc ← mk_local_def `hnc (imp (pis comp empty_clause↣local_false) empty_clause↣local_false),
hnc ← mk_local_def `hnc (imp (pis comp empty_clause^.local_false) empty_clause^.local_false),
p'' ← return $ app hnc (lambdas comp p'),
return (hnc::hs, p'')
meta def mk_splitting_clause (empty_clause : clause) (comps : list (list expr)) : tactic clause := do
(hs, p) ← mk_splitting_clause' empty_clause comps,
return $ { empty_clause with proof := p }↣close_constn hs
return $ { empty_clause with proof := p }^.close_constn hs
@[super.inf]
meta def splitting_inf : inf_decl := inf_decl.mk 30 $ take given, do
lf ← flip monad.lift state_t.read $ λst, st↣local_false,
op ← ♯ given↣c↣open_constn given↣c↣num_binders,
if list.bor (given↣c↣get_lits↣for $ λl, (is_local_not lf l↣formula)↣is_some) then return () else
let comps := get_components op↣2 in
if comps↣length < 2 then return () else do
splitting_clause ← ♯ mk_splitting_clause op↣1 comps,
lf ← flip monad.lift state_t.read $ λst, st^.local_false,
op ← ♯ given^.c^.open_constn given^.c^.num_binders,
if list.bor (given^.c^.get_lits^.for $ λl, (is_local_not lf l^.formula)^.is_some) then return () else
let comps := get_components op.2 in
if comps^.length < 2 then return () else do
splitting_clause ← ♯ mk_splitting_clause op.1 comps,
ass ← collect_ass_hyps splitting_clause,
add_sat_clause (splitting_clause↣close_constn ass) given↣sc↣sched_default,
remove_redundant given↣id []
add_sat_clause (splitting_clause^.close_constn ass) given^.sc^.sched_default,
remove_redundant given^.id []
end super

32
library/tools/super/subsumption.lean
View file

@ -11,29 +11,29 @@ namespace super
private meta def try_subsume_core : list clause.literal → list clause.literal → tactic unit
| [] _ := skip
| small large := first $ do
i ← small↣zip_with_index, j ← large↣zip_with_index,
i ← small^.zip_with_index, j ← large^.zip_with_index,
return $ do
unify_lit i.1 j.1,
try_subsume_core (small↣remove_nth i.2) (large↣remove_nth j.2)
try_subsume_core (small^.remove_nth i.2) (large^.remove_nth j.2)
-- FIXME: this is incorrect if a quantifier is unused
meta def try_subsume (small large : clause) : tactic unit := do
small_open ← clause.open_metan small (clause.num_quants small),
large_open ← clause.open_constn large (clause.num_quants large),
guard $ small↣num_lits ≤ large↣num_lits,
try_subsume_core small_open↣1↣get_lits large_open↣1↣get_lits
guard $ small^.num_lits ≤ large^.num_lits,
try_subsume_core small_open.1^.get_lits large_open.1^.get_lits
meta def does_subsume (small large : clause) : tactic bool :=
(try_subsume small large >> return tt) <|> return ff
meta def does_subsume_with_assertions (small large : derived_clause) : prover bool := do
if small↣assertions↣subset_of large↣assertions then do
♯ does_subsume small↣c large↣c
if small^.assertions^.subset_of large^.assertions then do
♯ does_subsume small^.c large^.c
else
return ff
meta def any_tt {m : Type → Type} [monad m] (active : rb_map clause_id derived_clause) (pred : derived_clause → m bool) : m bool :=
active↣fold (return ff) $ λk a cont, do
active^.fold (return ff) $ λk a cont, do
v ← pred a, if v then return tt else cont
meta def any_tt_list {m : Type → Type} [monad m] {A} (pred : A → m bool) : list A → m bool
@ -43,19 +43,19 @@ meta def any_tt_list {m : Type → Type} [monad m] {A} (pred : A → m bool) : l
@[super.inf]
meta def forward_subsumption : inf_decl := inf_decl.mk 20 $
take given, do active ← get_active,
sequence' $ do a ← active↣values,
guard $ a↣id ≠ given↣id,
sequence' $ do a ← active^.values,
guard $ a^.id ≠ given^.id,
return $ do
ss ← ♯ does_subsume a↣c given↣c,
ss ← ♯ does_subsume a^.c given^.c,
if ss
then remove_redundant given↣id [a]
then remove_redundant given^.id [a]
else return ()
meta def forward_subsumption_pre : prover unit := preprocessing_rule $ λnew, do
active ← get_active, filter (λn, do
do ss ← any_tt active (λa,
if a↣assertions↣subset_of n↣assertions then do
♯ does_subsume a↣c n↣c
if a^.assertions^.subset_of n^.assertions then do
♯ does_subsume a^.c n^.c
else
-- TODO: move to locked
return ff),
@ -76,7 +76,7 @@ meta def subsumption_interreduction : list derived_clause → prover (list deriv
meta def subsumption_interreduction_pre : prover unit :=
preprocessing_rule $ λnew,
let new' := list.sort_on (λc : derived_clause, c↣c↣num_lits) new in
let new' := list.sort_on (λc : derived_clause, c^.c^.num_lits) new in
subsumption_interreduction new'
meta def keys_where_tt {m} {K V : Type} [monad m] (active : rb_map K V) (pred : V → m bool) : m (list K) :=
@ -86,7 +86,7 @@ meta def keys_where_tt {m} {K V : Type} [monad m] (active : rb_map K V) (pred :
@[super.inf]
meta def backward_subsumption : inf_decl := inf_decl.mk 20 $ λgiven, do
active ← get_active,
ss ← ♯ keys_where_tt active (λa, does_subsume given↣c a↣c),
sequence' $ do id ← ss, guard (id ≠ given↣id), [remove_redundant id [given]]
ss ← ♯ keys_where_tt active (λa, does_subsume given^.c a^.c),
sequence' $ do id ← ss, guard (id ≠ given^.id), [remove_redundant id [given]]
end super

70
library/tools/super/superposition.lean
View file

@ -11,8 +11,8 @@ namespace super
meta def get_rwr_positions : expr → list (list ℕ)
| (app a b) := [[]] ++
do arg ← list.zip_with_index (get_app_args (app a b)),
pos ← get_rwr_positions arg↣1,
[arg↣2 :: pos]
pos ← get_rwr_positions arg.1,
[arg.2 :: pos]
| (var _) := []
| e := [[]]
@ -27,8 +27,8 @@ end
meta def replace_position (v : expr) : expr → list ℕ → expr
| (app a b) (p::ps) :=
let args := get_app_args (app a b) in
match args↣nth p with
| some arg := app_of_list a↣get_app_fn $ args↣update_nth p $ replace_position arg ps
match args^.nth p with
| some arg := app_of_list a^.get_app_fn $ args^.update_nth p $ replace_position arg ps
| none := app a b
end
| e [] := v
@ -43,7 +43,7 @@ variable ltr : bool
variable congr_ax : name
lemma {u v w} sup_ltr (F : Type u) (A : Type v) (a1 a2) (f : A → Type w) : (f a1 → F) → f a2 → a1 = a2 → F :=
take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq↣symm)
take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq^.symm)
lemma {u v w} sup_rtl (F : Type u) (A : Type v) (a1 a2) (f : A → Type w) : (f a1 → F) → f a2 → a2 = a1 → F :=
take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq)
@ -54,11 +54,11 @@ match is_eq e with
end
meta def try_sup : tactic clause := do
guard $ (c1↣get_lit i1)↣is_pos,
qf1 ← c1↣open_metan c1↣num_quants,
qf2 ← c2↣open_metan c2↣num_quants,
(rwr_from, rwr_to) ← (is_eq_dir (qf1↣1↣get_lit i1)↣formula ltr)↣to_monad,
atom ← return (qf2↣1↣get_lit i2)↣formula,
guard $ (c1^.get_lit i1)^.is_pos,
qf1 ← c1^.open_metan c1^.num_quants,
qf2 ← c2^.open_metan c2^.num_quants,
(rwr_from, rwr_to) ← (is_eq_dir (qf1.1^.get_lit i1)^.formula ltr)^.to_monad,
atom ← return (qf2.1^.get_lit i2)^.formula,
eq_type ← infer_type rwr_from,
atom_at_pos_type ← infer_type $ get_position atom pos,
unify eq_type atom_at_pos_type,
@ -69,52 +69,52 @@ guard $ ¬gt rwr_to' rwr_from',
rwr_ctx_varn ← mk_fresh_name,
abs_rwr_ctx ← return $
lam rwr_ctx_varn binder_info.default eq_type
(if (qf2↣1↣get_lit i2)↣is_neg
(if (qf2.1^.get_lit i2)^.is_neg
then replace_position (mk_var 0) atom pos
else imp (replace_position (mk_var 0) atom pos) c2↣local_false),
lf_univ ← infer_univ c1↣local_false,
else imp (replace_position (mk_var 0) atom pos) c2^.local_false),
lf_univ ← infer_univ c1^.local_false,
univ ← infer_univ eq_type,
atom_univ ← infer_univ atom,
op1 ← qf1↣1↣open_constn i1,
op2 ← qf2↣1↣open_constn c2↣num_lits,
hi2 ← (op2↣2↣nth i2)↣to_monad,
op1 ← qf1.1^.open_constn i1,
op2 ← qf2.1^.open_constn c2^.num_lits,
hi2 ← (op2.2^.nth i2)^.to_monad,
new_atom ← whnf $ app abs_rwr_ctx rwr_to',
new_hi2 ← return $ local_const hi2↣local_uniq_name `H binder_info.default new_atom,
new_hi2 ← return $ local_const hi2^.local_uniq_name `H binder_info.default new_atom,
new_fin_prf ←
return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1↣local_false, eq_type, rwr_from, rwr_to,
abs_rwr_ctx, (op2↣1↣close_const hi2)↣proof, new_hi2],
clause.meta_closure (qf1↣2 ++ qf2↣2) $ (op1↣1↣inst new_fin_prf)↣close_constn (op1↣2 ++ op2↣2↣update_nth i2 new_hi2)
return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1^.local_false, eq_type, rwr_from, rwr_to,
abs_rwr_ctx, (op2.1^.close_const hi2)^.proof, new_hi2],
clause.meta_closure (qf1.2 ++ qf2.2) $ (op1.1^.inst new_fin_prf)^.close_constn (op1.2 ++ op2.2^.update_nth i2 new_hi2)
meta def rwr_positions (c : clause) (i : nat) : list (list ℕ) :=
get_rwr_positions (c↣get_lit i)↣formula
get_rwr_positions (c^.get_lit i)^.formula
meta def try_add_sup : prover unit :=
(do c' ← ♯ try_sup gt ac1↣c ac2↣c i1 i2 pos ltr congr_ax,
inf_score 2 [ac1↣sc, ac2↣sc] >>= mk_derived c' >>= add_inferred)
(do c' ← ♯ try_sup gt ac1^.c ac2^.c i1 i2 pos ltr congr_ax,
inf_score 2 [ac1^.sc, ac2^.sc] >>= mk_derived c' >>= add_inferred)
<|> return ()
meta def superposition_back_inf : inference :=
take given, do active ← get_active, sequence' $ do
given_i ← given↣selected,
guard (given↣c↣get_lit given_i)↣is_pos,
option.to_monad $ is_eq (given↣c↣get_lit given_i)↣formula,
given_i ← given^.selected,
guard (given^.c^.get_lit given_i)^.is_pos,
option.to_monad $ is_eq (given^.c^.get_lit given_i)^.formula,
other ← rb_map.values active,
guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
other_i ← other↣selected,
pos ← rwr_positions other↣c other_i,
guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
other_i ← other^.selected,
pos ← rwr_positions other^.c other_i,
-- FIXME(gabriel): ``sup_ltr fails to resolve at runtime
[do try_add_sup gt given other given_i other_i pos tt ``super.sup_ltr,
try_add_sup gt given other given_i other_i pos ff ``super.sup_rtl]
meta def superposition_fwd_inf : inference :=
take given, do active ← get_active, sequence' $ do
given_i ← given↣selected,
given_i ← given^.selected,
other ← rb_map.values active,
guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
other_i ← other↣selected,
guard (other↣c↣get_lit other_i)↣is_pos,
option.to_monad $ is_eq (other↣c↣get_lit other_i)↣formula,
pos ← rwr_positions given↣c given_i,
guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
other_i ← other^.selected,
guard (other^.c^.get_lit other_i)^.is_pos,
option.to_monad $ is_eq (other^.c^.get_lit other_i)^.formula,
pos ← rwr_positions given^.c given_i,
[do try_add_sup gt other given other_i given_i pos tt ``super.sup_ltr,
try_add_sup gt other given other_i given_i pos ff ``super.sup_rtl]

4
library/tools/super/utils.lean
View file

@ -60,10 +60,10 @@ def exists_ {A} (l : list A) (p : A → Prop) [decidable_pred p] : bool :=
list.any l (λx, to_bool (p x))
def subset_of {A} [decidable_eq A] (xs ys : list A) :=
xs↣for_all (λx, x ∈ ys)
xs^.for_all (λx, x ∈ ys)
def filter_maximal {A} (gt : A → A → bool) (l : list A) : list A :=
filter (λx, l↣for_all (λy, ¬gt y x)) l
filter (λx, l^.for_all (λy, ¬gt y x)) l
private def zip_with_index' {A} : ℕ → list A → list (A × ℕ)
| _ nil := nil