let rec add s atm =
let atm', rho' = Combine.simplify (s.eqs, s.p) atm in
if Atom.is_true atm' then
Status.Valid(rho')
else if Atom.is_false atm' then
let rho = Jst.dep2 rho' (Jst.axiom atm) in
let tau = cone_of_influence s atm rho in
Status.Inconsistent(tau)
else
(try
Term.Var.k := s.upper;
let fct' = (atm', Jst.dep2 rho' (Jst.axiom atm)) in
let (eqs', p') = Combine.process fct' (s.eqs, s.p) in
if Combine.E.eq s.eqs eqs' &&
Partition.eq s.p p'
then
Status.Valid(rho')
else
let s' = {
ctxt = atm :: s.ctxt;
upper = !Term.Var.k;
p = p';
eqs = eqs'
}
in
Status.Ok(s')
with
| Jst.Inconsistent(rho) ->
let tau = cone_of_influence s atm rho in
Status.Inconsistent(tau))
and cone_of_influence s atm rho =
let inconsistency = match Jst.Mode.get () with
| Jst.Mode.Dep -> Jst.axioms_of rho
| Jst.Mode.No -> Atom.Set.add atm (ctxt2atoms s)
in
let inconsistency' =
match !coi_enabled with
| 1 ->
syntactic_cone_of_influence atm inconsistency
| 2 ->
semantic_cone_of_influence atm inconsistency
| _ ->
if !semantic_coi_min >= 0 &&
(Atom.Set.cardinal inconsistency) >= !semantic_coi_min
then
semantic_cone_of_influence atm inconsistency
else if !syntactic_coi_min >= 0 &&
(Atom.Set.cardinal inconsistency) >= !syntactic_coi_min
then
syntactic_cone_of_influence atm inconsistency
else
inconsistency
in
let savings =
if inconsistency == inconsistency' then 1. else
let n = float_of_int (Atom.Set.cardinal inconsistency')
and m = float_of_int (Atom.Set.cardinal inconsistency) in
n /. m
in
if !statistics then
begin
incr(num_of_inconsistencies);
total_savings := !total_savings +. savings;
end;
adjust_coi savings;
Jst.of_axioms inconsistency'
and adjust_coi savings =
if savings > 0.97 then
begin
if !semantic_coi_min >= 0 && !semantic_coi_min <= 150 then
begin
semantic_coi_min := !semantic_coi_min + 1;
if false && !verbose then
Format.eprintf "\n Adjusting min for semantic COI to %d" !semantic_coi_min
end
else if !syntactic_coi_min >= 0 && !semantic_coi_min <= 150 then
begin
syntactic_coi_min := !syntactic_coi_min + 1;
if false && !verbose then
Format.eprintf "\n Adjusting min for syntactic COI to %d" !syntactic_coi_min
end
end
else if savings < 0.90 then
begin
if !semantic_coi_min > 0 then
begin
semantic_coi_min := !semantic_coi_min - 1;
if false && !verbose then
Format.eprintf "\n Adjusting min for semantic COI to %d" !semantic_coi_min
end
else if !syntactic_coi_min > 0 then
begin
syntactic_coi_min := !syntactic_coi_min - 1;
if false && !verbose then
Format.eprintf "\n Adjusting min for syntactic COI to %d" !syntactic_coi_min
end
end
and ctxt2atoms s =
List.fold_right Atom.Set.add s.ctxt Atom.Set.empty
and syntactic_cone_of_influence atm inconsistency =
let visited = ref (Atom.Set.singleton atm) in
let todo = Stack.create () in
let rec loop () =
try
let current = Stack.pop todo in
Atom.Set.iter
(fun atm ->
if not(Atom.Set.mem atm !visited) &&
Atom.is_connected atm current
then
begin
visited := Atom.Set.add atm !visited;
Stack.push atm todo
end)
inconsistency;
loop ()
with
Stack.Empty -> !visited
in
Stack.push atm todo;
let inconsistency' = loop () in
trace_coi inconsistency' inconsistency;
inconsistency'
and semantic_cone_of_influence atm inconsistency =
let visited = ref (Atom.Set.singleton atm) in
let s = ref empty in
let todo = Stack.create () in
let rec loop () =
try
let current = Stack.pop todo in
Atom.Set.iter
(fun atm ->
if not(Atom.Set.mem atm !visited) &&
Atom.is_connected atm current
then
match add !s atm with
| Status.Valid _ -> ()
| Status.Ok(s') ->
s := s';
visited := Atom.Set.add atm !visited;
Stack.push atm todo
| Status.Inconsistent _ ->
raise(Found(Atom.Set.add atm !visited)))
inconsistency;
loop ()
with
Stack.Empty -> !visited
in
Stack.push atm todo;
let proofmode = Jst.Mode.get () in
try
Jst.Mode.set Jst.Mode.No;
let inconsistency' = try loop () with Found(atms) -> atms in
Jst.Mode.set proofmode;
inconsistency'
with
exc ->
Jst.Mode.set proofmode;
raise exc
and trace_coi atms1 atms2 =
Trace.msg "coi" "COI"
(Atom.Set.cardinal atms1, Atom.Set.cardinal atms2)
(Pretty.pair Pretty.number Pretty.number)