Adding support for lemmas in the command verit

6 files changed, 378 insertions, 114 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 88d0769..8eb1b60 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -21,9 +21,10 @@ open Decl_kinds
 open SmtMisc
 open CoqTerms
 open SmtForm
-open SmtCertif
 open SmtTrace
 open SmtAtom
+open SmtBtype
+open SmtCertif
 
 
 let debug = false
@@ -32,8 +33,38 @@ let debug = false
 (******************************************************************************)
 (* Given a verit trace build the corresponding certif and theorem             *)
 (******************************************************************************)
+exception Import_trace of int
+
+let get_val = function
+    Some a -> a
+  | None -> assert false
 
-let import_trace filename first =
+(* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *)
+let print_certif c where=
+  let r = ref c in
+  let out_channel = open_out where in
+  let fmt = Format.formatter_of_out_channel out_channel in
+  let continue = ref true in
+  while !continue do
+    let kind = to_string (!r.kind) in
+    let id = !r.id in
+    let pos = match !r.pos with
+      | None -> "None"
+      | Some p -> string_of_int p in
+    let used = !r.used in
+    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
+    begin match !r.value with
+    | None -> Format.fprintf fmt "None"
+    | Some l -> List.iter (fun f -> Form.to_smt Atom.to_string fmt f;
+                                    Format.fprintf fmt " ") l end;
+    Format.fprintf fmt "\n";
+    match !r.next with
+    | None -> continue := false
+    | Some n -> r := n 
+  done;
+  Format.fprintf fmt "@."; close_out out_channel
+                            
+let import_trace ra' rf' filename first lsmt =
   let chan = open_in filename in
   let lexbuf = Lexing.from_channel chan in
   let confl_num = ref (-1) in
@@ -54,23 +85,29 @@ let import_trace filename first =
   with
     | VeritLexer.Eof ->
        close_in chan;
-       let first =
-         let aux = VeritSyntax.get_clause !first_num in
-          match first, aux.value with
-          | Some (root,l), Some (fl::nil) ->
-            if Form.equal l fl then
-              aux
-            else (
-              aux.kind <- Other (ImmFlatten(root,fl));
-              SmtTrace.link root aux;
-              root
-            )
-          | _,_ -> aux in
-      let confl = VeritSyntax.get_clause !confl_num in
-      SmtTrace.select confl;
-      (* Trace.share_prefix first (2 * last.id); *)
-      occur confl;
-      (alloc first, confl)
+       let cfirst = ref (VeritSyntax.get_clause !first_num) in
+       let confl = ref (VeritSyntax.get_clause !confl_num) in
+       let re_hash = Form.hash_hform (Atom.hash_hatom ra') rf' in
+       begin match first with
+       | None -> ()
+       | Some _ ->
+          let cf, lr = order_roots (VeritSyntax.init_index lsmt re_hash)
+                         !cfirst in
+          cfirst := cf;
+          let to_add = VeritSyntax.qf_to_add (List.tl lr) in
+          let to_add =
+            (match first, !cfirst.value with
+             | Some (root, l), Some [fl] when not (Form.equal l (re_hash fl)) ->
+                let cfirst_value = !cfirst.value in
+                !cfirst.value <- root.value;
+                [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]
+             | _ -> []) @ to_add in
+       match to_add with
+       | [] -> ()
+       | _  -> confl := add_scertifs to_add !cfirst end;
+       select !confl;
+       occur !confl;
+       (alloc !cfirst, !confl)
     | Parsing.Parse_error -> failwith ("Verit.import_trace: parsing error line "^(string_of_int !line))
 
 
@@ -85,8 +122,10 @@ let import_all fsmt fproof =
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
+  let ra' = VeritSyntax.ra' in
+  let rf' = VeritSyntax.rf' in
   let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in
-  let (max_id, confl) = import_trace fproof None in
+  let (max_id, confl) = import_trace ra' rf' fproof None [] in
   (rt, ro, ra, rf, roots, max_id, confl)
 
 
@@ -101,9 +140,9 @@ let checker fsmt fproof = SmtCommands.checker (import_all fsmt fproof)
 (** Given a Coq formula build the proof                                       *)
 (******************************************************************************)
 
-let export out_channel rt ro l =
+let export out_channel rt ro lsmt =
   let fmt = Format.formatter_of_out_channel out_channel in
-  Format.fprintf fmt "(set-logic QF_UFLIA)@.";
+  Format.fprintf fmt "(set-logic UFLIA)@.";
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
@@ -111,47 +150,60 @@ let export out_channel rt ro l =
     Format.fprintf fmt "(declare-sort %s 0)@." s
   ) (SmtBtype.to_list rt);
 
-  List.iter (fun (i,cod,dom,op) ->
+  List.iter (fun (i,dom,cod,op) ->
     let s = "op_"^(string_of_int i) in
     VeritSyntax.add_fun s op;
     Format.fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
-    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) cod;
+    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) dom;
     Format.fprintf fmt ") ";
-    SmtBtype.to_smt fmt dom;
+    SmtBtype.to_smt fmt cod;
     Format.fprintf fmt ")@."
   ) (Op.to_list ro);
 
-  Format.fprintf fmt "(assert ";
-  Form.to_smt Atom.to_smt fmt l;
-  Format.fprintf fmt ")@\n(check-sat)@\n(exit)@."
+  List.iter (fun u -> Format.fprintf fmt "(assert ";
+                      Form.to_smt Atom.to_string fmt u;
+                      Format.fprintf fmt ")\n") lsmt;
+
+  Format.fprintf fmt "(check-sat)\n(exit)@."
 
 
 (* val call_verit : Btype.reify_tbl -> Op.reify_tbl -> Form.t -> (Form.t clause * Form.t) -> (int * Form.t clause) *)
-let call_verit rt ro fl root =
-  let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
-  export outchan rt ro fl;
+let call_verit rt ro ra' rf' first lsmt =
+  let filename, outchan = Filename.open_temp_file "verit_coq" ".smt2" in
+  export outchan rt ro lsmt;
   close_out outchan;
   let logfilename = Filename.chop_extension filename ^ ".vtlog" in
-  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename in
+  let wname, woc = Filename.open_temp_file "warnings_verit" ".log" in
+  close_out woc;
+  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename ^ " 2> " ^ wname in
   Format.eprintf "%s@." command;
   let t0 = Sys.time () in
   let exit_code = Sys.command command in
   let t1 = Sys.time () in
   Format.eprintf "Verit = %.5f@." (t1-.t0);
-  if exit_code <> 0 then
-    failwith ("Verit.call_verit: command " ^ command ^
-	        " exited with code " ^ string_of_int exit_code);
-  try
-    import_trace logfilename (Some root)
-  with
-    | VeritSyntax.Sat -> Structures.error "veriT can't prove this"
-
-
-let tactic () =
+  let win = open_in wname in
+  try 
+    if exit_code <> 0 then
+      failwith ("Verit.call_verit: command " ^ command ^
+	          " exited with code " ^ string_of_int exit_code);
+
+    try let _ = input_line win in
+        Structures.error "veriT returns 'unknown'"
+    with End_of_file ->
+          try
+            let res = import_trace ra' rf' logfilename first lsmt in
+            close_in win; Sys.remove wname; res
+          with
+          | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
+  with x -> close_in win; Sys.remove wname; raise x
+
+let tactic lcpl lcepl =
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
-  SmtCommands.tactic call_verit rt ro ra rf
+  let ra' = VeritSyntax.ra' in
+  let rf' = VeritSyntax.rf' in
+  SmtCommands.tactic call_verit rt ro ra rf ra' rf' lcpl lcepl
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 68ee317..95959da 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -1,8 +1,8 @@
 val debug : bool
 val import_trace :
-  string ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> string ->
   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
-  int * SmtAtom.Form.t SmtCertif.clause
+  SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause
 val clear_all : unit -> unit
 val import_all :
   string ->
@@ -22,11 +22,13 @@ val checker : string -> string -> unit
 val export :
   out_channel ->
   SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
-  SmtAtom.Form.t -> unit
+  SmtAtom.Form.t list -> unit
 val call_verit :
   SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
-  SmtAtom.Form.t ->
-  SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+  SmtAtom.Form.t list ->
   int * SmtAtom.Form.t SmtCertif.clause
-val tactic : unit -> Structures.tactic
+val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll
index 2a51a02..80fcc39 100644
--- a/src/verit/veritLexer.mll
+++ b/src/verit/veritLexer.mll
@@ -55,6 +55,7 @@
         "dl_disequality", DLDE;
         "la_disequality", LADE;
         "forall_inst", FINS;
+	"forall", FORALL;
         "exists_inst", EINS;
         "skolem_ex_ax", SKEA;
         "skolem_all_ax", SKAA;
@@ -105,6 +106,7 @@ let alpha = [ 'a'-'z' 'A' - 'Z' ]
 let blank = [' ' '\t']
 let newline = ['\n' '\r']
 let var = alpha (alpha|digit|'_')*
+let atvar = '@' var
 let bindvar = '?' var+
 let int = '-'? digit+
 
@@ -136,7 +138,9 @@ rule token = parse
   | "distinct"                 { DIST }
 
   | "Formula is Satisfiable"   { SAT }
-
+  | "Tindex_" (int as i)       { TINDEX (int_of_string i) }
+  | "Int"     	      	       { TINT }
+  | "Bool"		       { TBOOL }
   | int                        { try INT (int_of_string (Lexing.lexeme lexbuf))
 	                         with _ -> 
                                    BIGINT 
@@ -147,4 +151,6 @@ rule token = parse
                                    | Not_found -> VAR v }
   | bindvar                    { BINDVAR (Lexing.lexeme lexbuf) }
 
+  | atvar 		       { ATVAR (Lexing.lexeme lexbuf) }
+
   | eof                        { raise Eof }
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 799c32d..4ea6cd6 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -15,6 +15,7 @@
 
 
 %{
+  open SmtBtype 
   open SmtAtom
   open SmtForm
   open VeritSyntax
@@ -29,13 +30,20 @@
 %token COLON SHARP
 %token LPAR RPAR
 %token NOT XOR ITE EQ LT LEQ GT GEQ PLUS MINUS MULT OPP LET DIST
-%token INPU DEEP TRUE FALS ANDP ANDN ORP ORN XORP1 XORP2 XORN1 XORN2 IMPP IMPN1 IMPN2 EQUP1 EQUP2 EQUN1 EQUN2 ITEP1 ITEP2 ITEN1 ITEN2 EQRE EQTR EQCO EQCP DLGE LAGE LATA DLDE LADE FINS EINS SKEA SKAA QNTS QNTM RESO AND NOR OR NAND XOR1 XOR2 NXOR1 NXOR2 IMP NIMP1 NIMP2 EQU1 EQU2 NEQU1 NEQU2 ITE1 ITE2 NITE1 NITE2 TPAL TLAP TPLE TPNE TPDE TPSA TPIE TPMA TPBR TPBE TPSC TPPP TPQT TPQS TPSK SUBP HOLE
+%token TBOOL TINT
+%token<int> TINDEX
+%token INPU DEEP TRUE FALS ANDP ANDN ORP ORN XORP1 XORP2 XORN1 XORN2 IMPP IMPN1 IMPN2 EQUP1 EQUP2 EQUN1 EQUN2 ITEP1 ITEP2 ITEN1 ITEN2 EQRE EQTR EQCO EQCP DLGE LAGE LATA DLDE LADE FINS EINS SKEA SKAA QNTS QNTM RESO AND NOR OR NAND XOR1 XOR2 NXOR1 NXOR2 IMP NIMP1 NIMP2 EQU1 EQU2 NEQU1 NEQU2 ITE1 ITE2 NITE1 NITE2 TPAL TLAP TPLE TPNE TPDE TPSA TPIE TPMA TPBR TPBE TPSC TPPP TPQT TPQS TPSK SUBP HOLE FORALL
 %token <int> INT
 %token <Big_int.big_int> BIGINT
-%token <string> VAR BINDVAR
+%token <string> VAR BINDVAR ATVAR
+
 
 /* type de "retour" du parseur : une clause */
 %type <int> line
+/*
+%type <VeritSyntax.atom_form_lit> term
+%start term
+*/
 %start line
 
 
@@ -45,9 +53,13 @@ line:
   | SAT                                                    { raise Sat }
   | INT COLON LPAR typ clause                   RPAR EOL   { mk_clause ($1,$4,$5,[]) }
   | INT COLON LPAR typ clause clause_ids_params RPAR EOL   { mk_clause ($1,$4,$5,$6) }
+  | INT COLON LPAR TPQT LPAR SHARP INT COLON LPAR forall_decl RPAR RPAR INT RPAR EOL { add_solver $7 $10; add_ref $7 $1; mk_clause ($1, Tpqt, [], [$13]) }
+  | INT COLON LPAR FINS LPAR SHARP INT COLON LPAR OR LPAR NOT SHARP INT RPAR lit RPAR RPAR RPAR EOL
+  { mk_clause ($1, Fins, [snd $16], [get_ref $14]) }
 ;
 
 typ:
+  | TPBR                                                   { Tpbr  }
   | INPU                                                   { Inpu  }
   | DEEP                                                   { Deep  }
   | TRUE                                                   { True  }
@@ -80,7 +92,6 @@ typ:
   | LATA                                                   { Lata  }
   | DLDE                                                   { Dlde  }
   | LADE                                                   { Lade  }
-  | FINS                                                   { Fins  }
   | EINS                                                   { Eins  }
   | SKEA                                                   { Skea  }
   | SKAA                                                   { Skaa  }
@@ -114,11 +125,9 @@ typ:
   | TPSA                                                   { Tpsa  }
   | TPIE                                                   { Tpie  }
   | TPMA                                                   { Tpma  }
-  | TPBR                                                   { Tpbr  }
   | TPBE                                                   { Tpbe  }
   | TPSC                                                   { Tpsc  }
   | TPPP                                                   { Tppp  }
-  | TPQT                                                   { Tpqt  }
   | TPQS                                                   { Tpqs  }
   | TPSK                                                   { Tpsk  }
   | SUBP                                                   { Subp  }
@@ -127,7 +136,7 @@ typ:
 
 clause:
   | LPAR          RPAR                                     { [] }
-  | LPAR lit_list RPAR                                     { $2 }
+  | LPAR lit_list RPAR                                     { let _, l = list_dec $2 in l }
 ;
 
 lit_list:
@@ -135,67 +144,105 @@ lit_list:
   | lit lit_list                                           { $1::$2 }
 ;
 
-lit:   /* returns a SmtAtom.Form.t */
-  | name_term                                              { lit_of_atom_form_lit rf $1 }
-  | LPAR NOT lit RPAR                                      { Form.neg $3 }
+lit:   /* returns a SmtAtom.Form.t option */
+  | name_term                                              { let decl, t = $1 in decl, lit_of_atom_form_lit rf (decl, t) }
+  | LPAR NOT lit RPAR                                      { apply_dec Form.neg $3 }
+;
+
+nlit:   
+  | LPAR NOT lit RPAR                                      { apply_dec Form.neg $3 }
+;
+
+var_atvar:   
+  | VAR			                                   { $1 }
+  | ATVAR			                           { $1 }
 ;
 
-name_term:   /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */
+name_term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | SHARP INT                                              { get_solver $2 }
-  | SHARP INT COLON LPAR term RPAR                         { let res = $5 in add_solver $2 res; res }
-  | TRUE                                                   { Form Form.pform_true }
-  | FALS                                                   { Form Form.pform_false }
-  | VAR                                                    { Atom (Atom.get ra (Aapp (get_fun $1,[||]))) }
-  | BINDVAR                                                { Hashtbl.find hlets $1 }
-  | INT                                                    { Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | SHARP INT COLON LPAR term RPAR                         { let u = $5 in add_solver $2 u; u }
+  | TRUE                                                   { true, Form Form.pform_true }
+  | FALS                                                   { true, Form Form.pform_false }
+  | var_atvar						   { let x = $1 in match find_opt_qvar x with
+    					                   | Some bt -> false, Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
+							   | None -> true, Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
+  | BINDVAR                                                { true, Hashtbl.find hlets $1 }
+  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
+;
+
+tvar:
+  | TINT						   { TZ }
+  | TBOOL						   { Tbool }
+  | TINDEX						   { Tindex (indexed_type_of_int $1) }
+
+var_decl_list:
+  | LPAR var_atvar tvar RPAR				   { add_qvar $2 $3; [$2, $3] }
+  | LPAR var_atvar tvar RPAR var_decl_list		   { add_qvar $2 $3; ($2, $3)::$5 }
 ;
 
-term:   /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */
+forall_decl:
+  | FORALL LPAR var_decl_list RPAR name_term		   { clear_qvar (); false, Form (Fapp (Fforall $3, [|lit_of_atom_form_lit rf $5|])) }
+; 
+
+term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | LPAR term RPAR                                         { $2 }
 
   /* Formulae */
-  | TRUE                                                   { Form Form.pform_true }
-  | FALS                                                   { Form Form.pform_false }
-  | AND lit_list                                           { Form (Fapp (Fand, Array.of_list $2)) }
-  | OR lit_list                                            { Form (Fapp (For, Array.of_list $2)) }
-  | IMP lit_list                                           { Form (Fapp (Fimp, Array.of_list $2)) }
-  | XOR lit_list                                           { Form (Fapp (Fxor, Array.of_list $2)) }
-  | ITE lit_list                                           { Form (Fapp (Fite, Array.of_list $2)) }
+  | TRUE                                                   { true, Form Form.pform_true }
+  | FALS                                                   { true, Form Form.pform_false }
+  | AND lit_list                                           { apply_dec (fun x -> Form (Fapp (Fand, Array.of_list x))) (list_dec $2) }
+  | OR lit_list                                            { apply_dec (fun x -> Form (Fapp (For, Array.of_list x))) (list_dec $2) }
+  | IMP lit_list                                           { apply_dec (fun x -> Form (Fapp (Fimp, Array.of_list x))) (list_dec $2) }
+  | XOR lit_list                                           { apply_dec (fun x -> Form (Fapp (Fxor, Array.of_list x))) (list_dec $2) }
+  | ITE lit_list                                           { apply_dec (fun x -> Form (Fapp (Fite, Array.of_list x))) (list_dec $2) }
+  | forall_decl                                            { $1 }
 
   /* Atoms */
-  | INT                                                    { Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { Atom (Atom.hatom_Z_of_bigint ra $1) }
-  | LT name_term name_term                                 { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_lt ra h1 h2) | _,_ -> assert false }
-  | LEQ name_term name_term                                { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_le ra h1 h2) | _,_ -> assert false }
-  | GT name_term name_term                                 { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_gt ra h1 h2) | _,_ -> assert false }
-  | GEQ name_term name_term                                { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_ge ra h1 h2) | _,_ -> assert false }
-  | PLUS name_term name_term                               { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_plus ra h1 h2) | _,_ -> assert false }
-  | MULT name_term name_term                               { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_mult ra h1 h2) | _,_ -> assert false }
-  | MINUS name_term name_term                              { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_minus ra h1 h2) | _,_ -> assert false }
-  | MINUS name_term                                        { match $2 with | Atom h -> Atom (Atom.mk_opp ra h) | _ -> assert false }
-  | OPP name_term                                          { match $2 with | Atom h -> Atom (Atom.mk_opp ra h) | _ -> assert false }
-  | DIST args                                              { let a = Array.of_list $2 in Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a) }
-  | VAR                                                    { Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
-  | VAR args                                               { Atom (Atom.get ra (Aapp (get_fun $1, Array.of_list $2))) }
+  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | LT name_term name_term                                 { apply_bdec_atom (Atom.mk_lt ra) $2 $3 }
+  | LEQ name_term name_term                                { apply_bdec_atom (Atom.mk_le ra) $2 $3 }
+  | GT name_term name_term                                 { apply_bdec_atom (Atom.mk_gt ra) $2 $3 }
+  | GEQ name_term name_term                                { apply_bdec_atom (Atom.mk_ge ra) $2 $3 }
+  | PLUS name_term name_term                               { apply_bdec_atom (Atom.mk_plus ra) $2 $3 }
+  | MULT name_term name_term                               { apply_bdec_atom (Atom.mk_mult ra) $2 $3 }
+  | MINUS name_term name_term                              { apply_bdec_atom (Atom.mk_minus ra) $2 $3}
+  | MINUS name_term                                        { apply_dec_atom (fun d a -> Atom.mk_neg ra a) $2 }
+  | OPP name_term                                          { apply_dec_atom (fun d a -> Atom.mk_opp ra ~declare:d a) $2 }
+  | DIST args                                              { let da, la = list_dec $2 in
+    	 						     let a = Array.of_list la in
+							     da, Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) ~declare:da a) }
+  | VAR                                                    {let x = $1 in match find_opt_qvar x with
+    							     | Some bt -> false, Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
+							     | None -> true, Atom (Atom.get ra (Aapp (get_fun $1, [||])))}
+  | VAR args                                               { let f = $1 in let a = $2 in match find_opt_qvar f with
+    							     | Some bt -> let op = dummy_indexed_op (Rel_name f) [||] bt in
+							       	       	  false, Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a)))))
+      							     | None -> let dl, l = list_dec $2 in
+							       	       dl, Atom (Atom.get ra ~declare:dl (Aapp (get_fun f, Array.of_list l))) }
+
 
   /* Both */
-  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | Atom h1, Atom h2 when (match Atom.type_of h1 with | Tbool -> false | _ -> true) -> Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2) | _, _ -> Form (Fapp (Fiff, [|lit_of_atom_form_lit rf t1; lit_of_atom_form_lit rf t2|])) }
-  /* This rule introduces lots of shift/reduce conflicts */
-  | EQ lit lit                                             { let t1 = $2 in let t2 = $3 in Form (Fapp (Fiff, [|t1; t2|])) }
+  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Atom h1), (decl2, Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Atom (Atom.mk_eq ra decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|lit_of_atom_form_lit rf (decl1, t1); lit_of_atom_form_lit rf (decl2, t2)|])) }
+  | EQ nlit lit                                            { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|t1; t2|])) }
+  | EQ name_term nlit                                      { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|lit_of_atom_form_lit rf (decl1, t1); t2|])) }
   | LET LPAR bindlist RPAR name_term                       { $3; $5 }
-  | BINDVAR                                                { Hashtbl.find hlets $1 }
+  | BINDVAR                                                { true, Hashtbl.find hlets $1 }
+;
+
+blit:   
+  | name_term                                              { $1 } 
+  | LPAR NOT lit RPAR                                      { apply_dec (fun l -> Lit (Form.neg l)) $3 }
 ;
 
 bindlist:
-  | LPAR BINDVAR name_term RPAR                            { Hashtbl.add hlets $2 $3 }
-  | LPAR BINDVAR lit RPAR                                  { Hashtbl.add hlets $2 (Lit $3) }
-  | LPAR BINDVAR name_term RPAR bindlist                   { Hashtbl.add hlets $2 $3; $5 }
-  | LPAR BINDVAR lit RPAR bindlist                         { Hashtbl.add hlets $2 (Lit $3); $5 }
+  | LPAR BINDVAR blit RPAR	                           { Hashtbl.add hlets $2 (snd $3) }
+  | LPAR BINDVAR blit RPAR bindlist                        { Hashtbl.add hlets $2 (snd $3); $5 }
 
 args:
-  | name_term                                              { match $1 with Atom h -> [h] | _ -> assert false }
-  | name_term args                                         { match $1 with Atom h -> h::$2 | _ -> assert false }
+  | name_term                                              { match $1 with decl, Atom h -> [decl, h] | _ -> assert false }
+  | name_term args                                         { match $1 with decl, Atom h -> (decl, h)::$2 | _ -> assert false }
 ;
 
 clause_ids_params:
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index b598e2c..5d79016 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -203,16 +203,76 @@ let get_clause id =
 let add_clause id cl = Hashtbl.add clauses id cl
 let clear_clauses () = Hashtbl.clear clauses
 
-let mk_clause (id,typ,value,ids_params) =
+
+(* <ref_cl> maps solver integers to id integers. *)
+let ref_cl : (int, int) Hashtbl.t = Hashtbl.create 17
+let get_ref i = Hashtbl.find ref_cl i
+let add_ref i j = Hashtbl.add ref_cl i j
+let clear_ref () = Hashtbl.clear ref_cl
+
+(* Recognizing and modifying clauses depending on a forall_inst clause. *)
+                                 
+let rec fins_lemma ids_params =
+  match ids_params with
+    [] -> raise Not_found
+  | h :: t -> let cl_target = repr (get_clause h) in
+              match cl_target.kind with
+                Other (Forall_inst (lemma, _)) -> lemma
+              | _ -> fins_lemma t
+
+let rec find_remove_lemma lemma ids_params =
+  let eq_lemma h = eq_clause lemma (get_clause h) in
+  list_find_remove eq_lemma ids_params 
+
+(* Removes the lemma in a list of ids containing an instance of this lemma *)                   
+let rec merge ids_params =
+  let rest_opt = try let lemma = fins_lemma ids_params in
+                     let _, rest = find_remove_lemma lemma ids_params in
+                     Some rest
+                 with Not_found -> None in
+  match rest_opt with
+    None -> ids_params
+  | Some r -> merge r
+
+let to_add = ref []
+                     
+let rec mk_clause (id,typ,value,ids_params) =
   let kind =
     match typ with
+    | Tpbr ->
+       begin match ids_params with
+       | [id] ->
+          Same (get_clause id)
+       | _ -> failwith "unexpected form of tmp_betared" end
+    | Tpqt ->
+       begin match ids_params with
+       | [id] ->
+          Same (get_clause id)
+       | _ -> failwith "unexpected form of tmp_qnt_tidy" end
+    | Fins ->
+       begin match value, ids_params with
+        | [inst], [ref_th] when Form.is_pos inst ->
+           let cl_th = get_clause ref_th in
+           Other (Forall_inst (repr cl_th, inst))
+        | _ -> failwith "unexpected form of forall_inst" end
+    | Or ->
+       (match ids_params with
+        | [id_target] ->
+           let cl_target = get_clause id_target in
+           begin match cl_target.kind with
+           | Other (Forall_inst _) -> Same cl_target
+           | _ -> Other (ImmBuildDef cl_target) end
+        | _ -> assert false)
     (* Resolution *)
     | Reso ->
+       let ids_params = merge ids_params in
        (match ids_params with
         | cl1::cl2::q ->
            let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in
            Res res
-        | _ -> assert false)
+        | [fins_id] -> Same (get_clause fins_id)
+        | [] -> assert false)
+
     (* Roots *)
     | Inpu -> Root
     (* Cnf conversion *)
@@ -238,7 +298,7 @@ let mk_clause (id,typ,value,ids_params) =
        (match value with
         | l::_ -> Other (BuildProj (l,1))
         | _ -> assert false)
-    | Nand | Or | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
+    | Nand | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
        (match ids_params with
         | [id] -> Other (ImmBuildDef (get_clause id))
         | _ -> assert false)
@@ -291,7 +351,6 @@ let mk_clause (id,typ,value,ids_params) =
     | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
     (* Not implemented *)
     | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
-    | Fins -> failwith "VeritSyntax.ml: rule forall_inst not implemented yet"
     | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet"
     | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet"
     | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet"
@@ -300,11 +359,9 @@ let mk_clause (id,typ,value,ids_params) =
     | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet"
     | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet"
     | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet"
-    | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared not implemented yet"
     | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet"
     | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet"
     | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet"
-    | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy not implemented yet"
     | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet"
     | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet"
     | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet"
@@ -323,12 +380,36 @@ type atom_form_lit =
   | Form of SmtAtom.Form.pform
   | Lit of SmtAtom.Form.t
 
+(* functions for applying on a pair with a boolean when the boolean indicates
+   if the entire term should be declared in the tables *)
 let lit_of_atom_form_lit rf = function
-  | Atom a -> Form.get rf (Fatom a)
-  | Form f -> Form.get rf f
-  | Lit l -> l
-
-let solver : (int,atom_form_lit) Hashtbl.t = Hashtbl.create 17
+  | decl, Atom a -> Form.get ~declare:decl rf (Fatom a)
+  | decl, Form f -> begin match f with
+                    | Fapp (Fforall _, _) when decl -> failwith "decl is true on a forall"
+                    | _ -> Form.get ~declare:decl rf f end
+  | decl, Lit l -> l
+
+let apply_dec f (decl, a) = decl, f a
+
+let rec list_dec = function
+  | [] -> true, []
+  | (decl_h, h) :: t ->
+     let decl_t, l_t = list_dec t in
+     decl_h && decl_t, h :: l_t
+    
+let apply_dec_atom f = function
+  | decl, Atom h -> decl, Atom (f decl h)
+  | _ -> assert false
+
+let apply_bdec_atom f o1 o2 =
+  match o1, o2 with
+  | (decl1, Atom h1), (decl2, Atom h2) ->
+     let decl = decl1 && decl2 in
+     decl, Atom (f decl h1 h2)
+  | _ -> assert false
+
+
+let solver : (int, (bool * atom_form_lit)) Hashtbl.t = Hashtbl.create 17
 let get_solver id =
   try Hashtbl.find solver id
   with | Not_found -> failwith ("VeritSyntax.get_solver : solver variable number "^(string_of_int id)^" not found\n")
@@ -349,18 +430,66 @@ let get_fun id =
 let add_fun id cl = Hashtbl.add funs id cl
 let clear_funs () = Hashtbl.clear funs
 
-
+let qvar_tbl : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 10
+let find_opt_qvar s = try Some (Hashtbl.find qvar_tbl s)
+                      with Not_found -> None
+let add_qvar s bt = Hashtbl.add qvar_tbl s bt
+let clear_qvar () = Hashtbl.clear qvar_tbl
+
+let string_hform = Form.to_string ~pi:true (Atom.to_string ~pi:true )
+
+(* Finding the index of a root in <lsmt> modulo the <re_hash> function. 
+   This function is used by SmtTrace.order_roots *)
+let init_index lsmt re_hash =
+  let form_index_init_rank : (int, int) Hashtbl.t = Hashtbl.create 20 in
+  let add = Hashtbl.add form_index_init_rank in
+  let find = Hashtbl.find form_index_init_rank in
+  let rec walk rank = function
+    | [] -> ()
+    | h::t -> add (Form.to_lit h) rank;
+              walk (rank+1) t in
+  walk 1 lsmt;
+  fun hf -> let re_hf = re_hash hf in
+            try find (Form.to_lit re_hf)
+            with Not_found ->
+              let oc = open_out "/tmp/input_not_found.log" in
+              (List.map string_hform lsmt)
+              |> List.iter (Printf.fprintf oc "%s\n");
+              Printf.fprintf oc "\n%s\n" (string_hform re_hf);
+              flush oc; close_out oc;
+              failwith "not found: log available"
+
+let qf_to_add lr =
+  let is_forall l = match Form.pform l with
+    | Fapp (Fforall _, _) -> true
+    | _ -> false in
+  let rec qf_lemmas = function
+    | [] -> []
+    | ({value = Some [l]} as r)::t when not (is_forall l) ->
+       (Other (Qf_lemma (r, l)), r.value, r) :: qf_lemmas t
+    | _::t -> qf_lemmas t in
+  qf_lemmas lr
+                       
 let ra = Atom.create ()
 let rf = Form.create ()
+let ra' = Atom.create ()
+let rf' = Form.create ()
 
 let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
 
+let clear_mk_clause () = 
+  to_add := [];
+  clear_ref ()
 
 let clear () =
+  clear_qvar ();
+  clear_mk_clause ();
   clear_clauses ();
   clear_solver ();
   clear_btypes ();
   clear_funs ();
   Atom.clear ra;
   Form.clear rf;
+  Atom.clear ra';
+  Form.clear rf';
   Hashtbl.clear hlets
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index c7bf659..27a7ee3 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -21,15 +21,30 @@ type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2
 val get_clause : int -> SmtAtom.Form.t SmtCertif.clause
 val add_clause : int -> SmtAtom.Form.t SmtCertif.clause -> unit
 
+val add_ref : int -> int -> unit
+val get_ref : int -> int
+val to_add : (int * SmtAtom.Form.t list) list ref
+
 val mk_clause : SmtCertif.clause_id * typ * SmtAtom.Form.t list * SmtCertif.clause_id list -> SmtCertif.clause_id
 
 type atom_form_lit =
   | Atom of SmtAtom.Atom.t
   | Form of SmtAtom.Form.pform
   | Lit of SmtAtom.Form.t
-val lit_of_atom_form_lit : SmtAtom.Form.reify -> atom_form_lit -> SmtAtom.Form.t
-val get_solver : int -> atom_form_lit
-val add_solver : int -> atom_form_lit -> unit
+val lit_of_atom_form_lit : SmtAtom.Form.reify -> bool * atom_form_lit -> SmtAtom.Form.t
+
+val apply_dec_atom : (bool -> SmtAtom.hatom -> SmtAtom.hatom) ->
+                     bool * atom_form_lit -> bool * atom_form_lit
+val apply_bdec_atom :
+  (bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) ->
+  bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit
+
+val apply_dec : ('a -> 'b) -> bool * 'a -> bool * 'b
+val list_dec : (bool * 'a) list -> bool * 'a list
+
+
+val get_solver : int -> bool * atom_form_lit
+val add_solver : int -> bool * atom_form_lit -> unit
 
 val get_btype : string -> SmtBtype.btype
 val add_btype : string -> SmtBtype.btype -> unit
@@ -37,8 +52,21 @@ val add_btype : string -> SmtBtype.btype -> unit
 val get_fun : string -> SmtAtom.indexed_op
 val add_fun : string -> SmtAtom.indexed_op -> unit
 
+val find_opt_qvar : string -> SmtBtype.btype option 
+val add_qvar : string -> SmtBtype.btype -> unit
+val clear_qvar : unit -> unit
+
+val string_hform : SmtAtom.Form.t -> string
+
+val init_index : SmtAtom.Form.t list -> (SmtAtom.Form.t -> SmtAtom.Form.t) ->
+                 SmtAtom.Form.t -> int
+
+val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCertif.clause_kind * SmtAtom.Form.t list option * SmtAtom.Form.t SmtCertif.clause) list
+                                     
 val ra : SmtAtom.Atom.reify_tbl
 val rf : SmtAtom.Form.reify
+val ra' : SmtAtom.Atom.reify_tbl
+val rf' : SmtAtom.Form.reify
 
 val hlets : (string, atom_form_lit) Hashtbl.t