Holes in proof:

- can now take learned clauses as argument
- returns a whole clause (and not only a literal)
- tested for the vernacular commands
Warning: seems to slow down 8.5 version

1 files changed, 6 insertions, 6 deletions

diff --git a/src/Trace.v b/src/Trace.v
index 3b6ac47..9566c47 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -15,7 +15,7 @@
 
 
 Require Import Bool Int63 PArray.
-Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators.
+Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators Assumptions.
 
 Local Open Scope array_scope.
 Local Open Scope int63_scope.
@@ -335,8 +335,8 @@ Module Euf_Checker.
   | SplDistinctElim (pos:int) (orig:clause_id) (res:_lit)
   (* Offer the possibility to discharge parts of the proof to (manual) Coq proofs.
      WARNING: this breaks extraction. *)
-  | Hole (pos:int) (res:_lit)
-    (p:Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) res)
+  | Hole (pos:int) (prem_id:list clause_id) (prem:list C.t) (concl:C.t)
+    (p:interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) prem concl)
   .
 
   Local Open Scope list_scope.
@@ -362,7 +362,7 @@ Module Euf_Checker.
       | LiaDiseq pos l => S.set_clause s pos (check_diseq t_form t_atom l)
       | SplArith pos orig res l => S.set_clause s pos (check_spl_arith t_form t_atom (S.get s orig) res l)
       | SplDistinctElim pos orig res => S.set_clause s pos (check_distinct_elim t_form t_atom (S.get s orig) res)
-      | @Hole pos res _ => S.set_clause s pos (res::nil)
+      | @Hole pos prem_id prem concl _ => S.set_clause s pos (check_hole s prem_id prem concl)
     end.
 
   Lemma step_checker_correct :
@@ -372,7 +372,7 @@ Module Euf_Checker.
       forall s, S.valid rho s ->
         forall st : step, S.valid rho (step_checker s st).
   Proof.
-    intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos res p]; simpl; try apply S.valid_set_clause; auto.
+    intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos prem_id prem concl p]; simpl; try apply S.valid_set_clause; auto.
     apply S.valid_set_resolve; auto.
     apply valid_check_flatten; auto; intros h1 h2 H.
     rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto.
@@ -392,7 +392,7 @@ Module Euf_Checker.
     apply valid_check_diseq; auto.
     apply valid_check_spl_arith; auto.
     apply valid_check_distinct_elim; auto.
-    unfold C.valid; simpl; unfold rho; rewrite p; auto.
+    apply valid_check_hole; auto.
   Qed.
 
   Definition euf_checker (* t_atom t_form *) s t :=