Final bug fixes on merged program prover - it now matches the perform…

…ance of the unmerged version.

benchmarks/procs/08-reversal-tailrec.wl2

@@ -2,7 +2,7 @@ fields: next;
 
 proc reverse(x, acc)
 precondition: x -> v' * ls[a](v', nil) * acc -> w' * ls[b](w', nil);
-postcondition: [b] <= [c'] : x -> nil * acc -> z' * ls[c'](z', nil);
+postcondition: x -> nil * acc -> z' * ls[c'](z', nil);
 {
 	list := x.next;
 	if list != nil then

src/procedure/procedure_prove.ml

@@ -18,12 +18,16 @@ module Node = Proofnode.Make(Seq)
 
 let prove_all = ref false
 
-let () = F.usage := !F.usage ^ " [-D <file>] [-d(entail|frame|invalid)] [-Lem <int>] -P <file> [-T] [-all | <entry_point>*]"
+let () = F.usage := !F.usage ^ "[-ed/fd <int>] [-D <file>] [-d(entail|frame|invalid)] [-Lem <int>] -P <file> [-T] [-all | <entry_point>*]"
 
 let () = 
   let old_spec_thunk = !F.speclist in
   F.speclist := 
     (fun () -> old_spec_thunk() @ [
+      ("-ed", Arg.Set_int Rules.entl_depth, 
+        ": maximum search depth for entailment sub-prover, default is " ^ (string_of_int !Rules.entl_depth));
+      ("-fd", Arg.Int Sl_abduce.set_depth, 
+        ": maximum depth to unfold predicates to in frame inference, default is " ^ (string_of_int Sl_abduce.max_depth));
       ("-D", Arg.Set_string defs_path, 
         ": read inductive definitions from <file>, default is " ^ !defs_path);
       ("-dentail", Arg.Set Rules.show_entailment_debug, 

src/procedure/procedure_rules.ml

@@ -23,7 +23,7 @@ let show_invalidity_debug = ref false
 let show_entailment_debug = ref false
 let show_frame_debug = ref false
 
-let entl_depth = ref Sl_abduce.max_depth
+let entl_depth = ref 4
 
 (* Wrapper for the entailment prover *)
 let entailment_table : (int * (Slprover.Proof.t option)) EntlSeqHash.t =
@@ -772,8 +772,10 @@ let transform_seq ((pre, cmd, post) as seq) =
           schema_tags in
       let schema_subst = Tagpairs.union schema_subst (Tagpairs.reflect u_tag_theta) in
       let ex_schema = Ord_constraints.subst_tags schema_subst abd_schema in
-      if not (Ord_constraints.verify_schemas (Sl_form.tags pre) ex_schema) 
-        then None else
+      if not (Ord_constraints.verify_schemas (Sl_form.tags pre) ex_schema) then
+        let () = debug (fun () -> "Could not verify constraint schema " ^ (Ord_constraints.to_string ex_schema)) in 
+        None 
+      else
         let pre_with_schema = Sl_form.add_constraints pre ex_schema in
         let subst_avoid_tags =
           Tags.union (Sl_form.tags frame) (Tagpairs.flatten tag_theta) in

src/seplog/sl_abduce.ml

@@ -16,21 +16,21 @@ let mk_axiom unify res =
       Option.mk not_empty "Match")
 
 let ruf_rl = Sl_rules.ruf_rl
-let bounds_intro = Rule.mk_infrule Sl_rules.bounds_intro_rl
-let eq_ex_subst = 
-  Rule.mk_infrule (Seqtactics.relabel "RHS.Ex.Eq." Sl_rules.eq_ex_subst_rule)
+let bounds_intro_rl = Sl_rules.bounds_intro_rl
+let eq_ex_subst_rl = Sl_rules.eq_ex_subst_rule
 let rhs_disj_to_symheaps = Rule.mk_infrule Sl_rules.rhs_disj_to_symheaps_rl
 
+let simplify = 
+  Rule.mk_infrule
+    (Seqtactics.relabel "Simplify"
+        (Seqtactics.repeat 
+          (Seqtactics.first [ bounds_intro_rl ; eq_ex_subst_rl ; ])))
+
 let rules = ref Rule.fail
 let set_defs defs = 
-  rules := Rule.first [
-      rhs_disj_to_symheaps ;
-      bounds_intro ;
-      eq_ex_subst ;
-      Rule.mk_infrule (ruf_rl defs) ;
-    ]
+  rules := Rule.mk_infrule (ruf_rl defs)
 
-let maxdepth = ref 4
+let maxdepth = ref 3
 
 let set_depth d = maxdepth := d
 let max_depth = !maxdepth
@@ -83,7 +83,17 @@ let abd_substs
         Option.dest Blist.empty Fun.id res in
       Blist.bind (f (Ord_constraints.empty, cs')) candidates
     with Not_symheap -> Blist.empty in
-  let rules = Rule.combine_axioms (mk_axiom unifier result) !rules in
+  let axiom = mk_axiom unifier result in
+  let axiom =
+    Rule.first [ 
+      Rule.sequence [
+          Rule.attempt rhs_disj_to_symheaps ;
+          Rule.attempt simplify ;
+          axiom ;
+        ] ;
+      axiom ;
+      ] in
+  let rules = Rule.combine_axioms axiom !rules in
   let proof = Prover.idfs 1 !maxdepth Rule.fail rules (f, f') in
   Option.mk (Option.is_some proof) !result
 
@@ -107,7 +117,17 @@ let abd_bi_substs
         (Sl_unify.Bidirectional.mk_verifier verify))
         (Pair.swap init_state)
     with Not_symheap -> [] in
-  let rules = Rule.combine_axioms (mk_axiom unifier result) !rules in
+  let axiom = mk_axiom unifier result in
+  let axiom =
+    Rule.first [ 
+      Rule.sequence [
+          Rule.attempt rhs_disj_to_symheaps ;
+          Rule.attempt simplify ;
+          axiom ;
+        ] ;
+      axiom ;
+      ] in
+  let rules = Rule.combine_axioms axiom !rules in
   let proof = Prover.idfs 1 !maxdepth Rule.fail rules (f, f') in
   Option.map
     (fun _ -> 

src/seplog/sl_heap.ml

@@ -289,17 +289,18 @@ let univ s f =
   if Sl_term.Map.is_empty theta then f else subst theta f
 
 let subst_existentials h =
-  let aux h' =
-    let (ex_eqs, non_ex_eqs) =
-      Blist.partition
-        (fun p' -> Pair.disj (Pair.map Sl_term.is_exist_var p')) 
-        (Sl_uf.bindings h'.eqs) in
-    if ex_eqs =[] then h' else
-    let ex_eqs = 
-      Blist.map (fun ((x,y) as p) -> if Sl_term.is_exist_var x then p else (y,x)) ex_eqs in
-      let h'' = 
-        { h' with eqs = Sl_uf.of_list non_ex_eqs; _terms=None; _vars=None; _tags=None } in
-      subst (Sl_term.Map.of_list ex_eqs) h'' in
+  let aux h =
+    try
+      let eqs = Sl_uf.bindings h.eqs in
+      let ((x,y) as eq) =
+        Blist.find
+          (fun eq -> Pair.disj (Pair.map Sl_term.is_exist_var eq))
+          eqs in
+      let eqs = Blist.filter (fun eq' -> eq' != eq) eqs in
+      let (x,y) = if Sl_term.is_exist_var x then eq else (y,x) in
+      let h' = { h with eqs = Sl_uf.of_list eqs; _terms=None; _vars=None; _tags=None } in
+      subst (Sl_term.Map.singleton x y) h'
+    with Not_found -> h in
   fixpoint aux h
 
 let norm h =