prerr_endline (Pp.pp_bag bag);
prerr_endline "========================================";
;;
+
+let select = function
+ | [] -> None
+ | x::tl -> Some (x, tl)
+;;
+
+let nparamod metasenv subst context t table =
+ prerr_endline "========================================";
+ let module C = struct
+ let metasenv = metasenv
+ let subst = subst
+ let context = context
+ end
+ in
+ let module B = NCicBlob.NCicBlob(C) in
+ let module Pp = Pp.Pp (B) in
+ let module FU = FoUnif.Founif(B) in
+ let module IDX = Index.Index(B) in
+ let module Sup = Superposition.Superposition(B) in
+ let module Utils = FoUtils.Utils(B) in
+
+ let rec given_clause bag maxvar actives passives g_actives g_passives =
+
+ (* keep goals demodulated w.r.t. actives and check if solved *)
+ (* we may move this at the end of infer_right and simplify with
+ * just new_clauses *)
+ let bag, g_actives =
+ List.fold_left
+ (fun (bag,acc) c ->
+ let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in
+ bag, c::acc)
+ (bag,[]) g_actives
+ in
+
+ (* backward step *)
+ let bag, maxvar, g_actives, g_passives =
+ match select g_passives with
+ | None -> bag, maxvar, g_actives, g_passives
+ | Some (g_current, g_passives) ->
+ let bag, g_current =
+ Sup.backward_simplify maxvar (snd actives) bag g_current
+ in
+ let bag, maxvar, new_goals =
+ Sup.infer_left bag maxvar g_current actives
+ in
+ bag, maxvar, g_current::g_actives, g_passives @ new_goals
+ in
+
+ (* forward step *)
+ let bag, maxvar, actives, passives =
+ match select passives with
+ | None -> bag, maxvar, actives, passives
+ | Some (current, passives) ->
+ match Sup.forward_simplify (snd actives) bag current with
+ | None -> bag, maxvar, actives, passives
+ | Some (bag, current) ->
+ let bag, maxvar, actives, new_clauses =
+ Sup.infer_right bag maxvar current actives
+ in
+ bag, maxvar, actives, passives @ new_clauses
+ in
+
+ given_clause bag maxvar actives passives g_actives g_passives
+ in
+
+ let mk_clause bag maxvar ty =
+ let ty = B.embed ty in
+ let proof = B.embed (NCic.Rel ~-1) in
+ let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
+ let bag, c = Utils.add_to_bag bag c in
+ bag, maxvar, c
+ in
+ let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
+ let g_actives = [] in
+ let g_passives = [goal] in
+ let passives, bag, maxvar =
+ List.fold_left
+ (fun (cl, bag, maxvar) t ->
+ let bag, maxvar, c = mk_clause bag maxvar t in
+ c::cl, bag, maxvar)
+ ([], bag, maxvar) table
+ in
+ let actives = [], IDX.DT.empty in
+ try given_clause bag maxvar actives passives g_actives g_passives
+ with Sup.Success _ -> prerr_endline "YES!"
+;;
;;
let string_of_rule = function
- | Terms.SuperpositionRight -> "SupR"
- | Terms.SuperpositionLeft -> "SupL"
- | Terms.Demodulation -> "Demod"
+ | Terms.Superposition -> "Super"
+ | Terms.Demodulation -> "Demod"
;;
let string_of_direction = function
(string_of_rule rule)
id1 id2 (String.concat
"," (List.map string_of_int p)))
-
;;
let pp_bag ~formatter:f bag =
module Order = Orderings.Orderings(B)
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
+
+ exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
let rec list_first f = function
| [] -> None
else Some (bag, clause)
;;
+ (* this is like forward_simplify but raises Success *)
+ let backward_simplify maxvar table bag clause =
+ let bag, clause = demodulate bag clause table in
+ if is_identity_clause clause then raise (Success (bag, maxvar, clause))
+ else bag, clause
+ ;;
+
(* =================== inference ===================== *)
- let superposition_right table varlist subterm pos context =
+ (* this is OK for both the sup_left and sup_right inference steps *)
+ let superposition table varlist subterm pos context =
let cands = IDX.DT.retrieve_unifiables table subterm in
HExtlib.filter_map
(fun (dir, (id,lit,vl,_ (*as uc*))) ->
bag, maxvar, res
;;
- let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
+ let superposition_with_table bag maxvar (id,selected,vl,_) table =
match selected with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,Terms.Lt) ->
- fold_build_new_clause bag maxvar id Terms.SuperpositionRight
+ fold_build_new_clause bag maxvar id Terms.Superposition
(fun _ -> true)
(all_positions [3]
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
- r (superposition_right table vl))
+ r (superposition table vl))
| Terms.Equation (l,r,ty,Terms.Gt) ->
- fold_build_new_clause bag maxvar id Terms.SuperpositionRight
+ fold_build_new_clause bag maxvar id Terms.Superposition
(fun _ -> true)
(all_positions [2]
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
- l (superposition_right table vl))
+ l (superposition table vl))
| Terms.Equation (l,r,ty,Terms.Incomparable) ->
- fold_build_new_clause bag maxvar id Terms.SuperpositionRight
+ fold_build_new_clause bag maxvar id Terms.Superposition
(function (* Riazanov: p.33 condition (iv) *)
| Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq ->
Order.compare_terms l r <> Terms.Eq
| _ -> assert false)
((all_positions [3]
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
- r (superposition_right table vl)) @
+ r (superposition table vl)) @
(all_positions [2]
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
- l (superposition_right table vl)))
+ l (superposition table vl)))
| _ -> assert false
;;
* (and is not the identity) *)
let infer_right bag maxvar current (alist,atable) =
let ctable = IDX.index_unit_clause IDX.DT.empty current in
+ let bag, (alist, atable) =
+ let bag, alist =
+ HExtlib.filter_map_acc (forward_simplify ctable) bag alist
+ in
+ bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
+ in
let bag, maxvar, new_clauses =
List.fold_left
(fun (bag, maxvar, acc) active ->
let bag, maxvar, newc =
- superposition_right_with_table bag maxvar active ctable
+ superposition_with_table bag maxvar active ctable
in
bag, maxvar, newc @ acc)
(bag, maxvar, []) alist
in
let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
let bag, maxvar, additional_new_clauses =
- superposition_right_with_table bag maxvar fresh_current atable
+ superposition_with_table bag maxvar fresh_current atable
in
let new_clauses = new_clauses @ additional_new_clauses in
let bag, new_clauses =
bag, maxvar, (alist, atable), new_clauses
;;
+ let infer_left bag maxvar goal (_alist, atable) =
+ let bag, maxvar, new_goals =
+ superposition_with_table bag maxvar goal atable
+ in
+ let bag, new_goals =
+ List.fold_left
+ (fun (bag, acc) g ->
+ let bag, g = demodulate bag g atable in
+ bag, g :: acc)
+ (bag, []) new_goals
+ in
+ bag, maxvar, List.rev new_goals
+ ;;
+
end
(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-
module Superposition (B : Terms.Blob) :
sig
+ exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+
(* The returned active set is the input one + the selected clause *)
val infer_right :
B.t Terms.bag ->
int -> (* maxvar *)
- B.t Terms.unit_clause -> (* selected *)
+ B.t Terms.unit_clause -> (* selected passive *)
Index.Index(B).active_set ->
B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
+ val infer_left :
+ B.t Terms.bag ->
+ int -> (* maxvar *)
+ B.t Terms.unit_clause -> (* selected goal *)
+ Index.Index(B).active_set ->
+ B.t Terms.bag * int * B.t Terms.unit_clause list
+
+ val demodulate :
+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
+
+ val forward_simplify :
+ Index.Index(B).DT.t ->
+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ (B.t Terms.bag * B.t Terms.unit_clause) option
+
+ (* may raise success *)
+ val backward_simplify :
+ int ->
+ Index.Index(B).DT.t ->
+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ B.t Terms.bag * B.t Terms.unit_clause
+
end
type comparison = Lt | Eq | Gt | Incomparable
-type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type rule = Superposition | Demodulation
type direction = Left2Right | Right2Left | Nodir
type position = int list
type comparison = Lt | Eq | Gt | Incomparable
-type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type rule = Superposition | Demodulation
(* A Discrimination tree is a map: foterm |-> (dir, clause) *)
type direction = Left2Right | Right2Left | Nodir
include "nat/plus.ma".
+ntheorem boo:
+ ((λx.x = x) ?) → 0 = 0.
+##[ #H; nwhd in H ⊢ %; nauto by H.
+
ntheorem foo:
((λx.x + 0 = x) ?) →
((λx,y.x + S y = S (x + y)) ? ?) →
((λx,y.y + x = x + y) ? ?) →
∀x. ((λz. x + x = z + S z) ?).
-##[ #H; #H1; #H2; #x; nnormalize in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file
+##[ #H; #H1; #H2; #x; nwhd in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file
projects / helm.git / commitdiff