From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Sat, 27 Oct 2018 20:08:44 +0200
Subject: Adding support for lemmas in the command verit

---
 src/verit/veritLexer.mll | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src/verit/veritLexer.mll')

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 }
-- 
cgit