source: vis_dev/cusp-1.1/src/smt/smt.l @ 64

Last change on this file since 64 was 12, checked in by cecile, 13 years ago

cusp added

File size: 6.2 KB
Line 
1%{
2/**CFile***********************************************************************
3
4  FileName    [smt.l]
5 
6  PackageName [smt]
7
8  Synopsis    [Lexical analyzer for formula parser. See smt.h for syntax.]
9
10  Author      [Hyondeuk Kim]
11
12  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
13
14  All rights reserved.
15
16  Redistribution and use in source and binary forms, with or without
17  modification, are permitted provided that the following conditions
18  are met:
19
20  Redistributions of source code must retain the above copyright
21  notice, this list of conditions and the following disclaimer.
22
23  Redistributions in binary form must reproduce the above copyright
24  notice, this list of conditions and the following disclaimer in the
25  documentation and/or other materials provided with the distribution.
26
27  Neither the name of the University of Colorado nor the names of its
28  contributors may be used to endorse or promote products derived from
29  this software without specific prior written permission.
30
31  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
32  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
33  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
34  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
35  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
36  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
37  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
38  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
39  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
40  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
41  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
42  POSSIBILITY OF SUCH DAMAGE.]
43
44******************************************************************************/
45
46#ifdef HAVE_LIBGMP
47
48#include "smtRead.h"
49
50/*---------------------------------------------------------------------------*/
51/* Constant declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54/*---------------------------------------------------------------------------*/
55/* Variable declarations                                                     */
56/*---------------------------------------------------------------------------*/
57
58
59/**AutomaticStart*************************************************************/
60
61/*---------------------------------------------------------------------------*/
62/* Static function prototypes                                                */
63/*---------------------------------------------------------------------------*/
64
65
66/**AutomaticEnd***************************************************************/
67
68
69
70/*---------------------------------------------------------------------------*/
71/* Definition of internal functions                                          */
72/*---------------------------------------------------------------------------*/
73
74/**Function********************************************************************
75
76  Synopsis    [Initializes global variables for parsing file.]
77
78  SideEffects []
79
80******************************************************************************/
81void
82SmtFileSetup(
83  FILE * fp)
84{
85  SmtYyin             = fp;
86}
87
88/*---------------------------------------------------------------------------*/
89/* Definition of static functions                                            */
90/*---------------------------------------------------------------------------*/
91
92/**Function********************************************************************
93
94  Synopsis    [Prints error message and sets global error flag.]
95
96  SideEffects []
97
98******************************************************************************/
99static void
100SmtYyerror(
101  char * errmsg)
102{
103  (void) fprintf(stderr, "%s in with token \"%s\"\n", errmsg, yytext);
104}
105
106%}
107
108/*---------------------------------------------------------------------------*/
109/*      Lexical analyzer rules                                               */
110/*---------------------------------------------------------------------------*/
111
112%option noyywrap
113
114/* substitution strings */
115/* alnum is the same set in alnumsymbol in io.l except [ and ] being
116removed here for the until operator */
117/* - , =, and ; are intentionally removed
118   - is used for -> and <->
119   = is used for foo = bar
120   ; is used for delimitters */
121/* ( and ) are intentionally removed since they are used as parentheses */
122/* +, *, and ^ have to be used surrounded by spaces
123since they are symbols. ! can be attached immediately w/o spaces though
124since it is not a symbol */
125/*alnum         [A-Za-z0-9\^\?\|\/\$\<\>~@\_#\$%\"\'\.]**/
126/*num             [0-9]+*/
127%%
128
129[ \t\n\r]       ;
130
131"#".*   ;   
132
133true { return(TRUE_TOK); }
134false { return(FALSE_TOK); }
135ite { return(ITE_TOK); }
136not { return(NOT_TOK); }
137implies { return(IMPLIES_TOK); }
138if_then_else { return(IF_THEN_ELSE_TOK); }
139and { return(AND_TOK); }
140or { return(OR_TOK); }
141xor { return(XOR_TOK); }
142iff { return(IFF_TOK); }
143exists { return(EXISTS_TOK); }
144forall { return(FORALL_TOK); }
145let { return(LET_TOK); }
146flet { return(FLET_TOK); }
147[\"][^\"]*[\"] { return(STRING_TOK); }
148[\{][^\{]*[\}] { return(USER_VAL_TOK); }
149notes { return(NOTES_TOK); }
150sorts { return(SORTS_TOK); }
151funs { return(FUNS_TOK); }
152preds { return(PREDS_TOK); }
153extensions { return(EXTENSIONS_TOK); }
154definition { return(DEFINITION_TOK); }
155axioms { return(AXIOMS_TOK); }
156logic { return(LOGIC_TOK); }
157":" { return(COLON_TOK); }
158"(" { return(LPAREN_TOK); }
159")" { return(RPAREN_TOK); }
160sat { return(SAT_TOK); }
161unsat { return(UNSAT_TOK); }
162unknown { return(UNKNOWN_TOK); }
163assumption { return(ASSUMPTION_TOK); }
164formula { return(FORMULA_TOK); }
165status { return(STATUS_TOK); }
166benchmark { return(BENCHMARK_TOK); }
167extrasorts { return(EXTRASORTS_TOK); }
168extrafuns { return(EXTRAFUNS_TOK); }
169extrapreds { return(EXTRAPREDS_TOK); }
170language { return(LANGUAGE_TOK); }
171"=" { return(EQUALS_TOK); }
172distinct { return(DISTINCT_TOK); }
173"$" { return(DOLLAR_TOK); }
174
175
176[\=\<\>\&@#\+\-\*\/%\|~]+               { return(AR_SYMB); }
177[0-9]+                                  { return(NUMERAL_TOK); }
178[?][a-zA-Z][a-zA-Z\.\_0-9]*             { return(VAR_TOK); }
179[a-zA-Z\/][a-zA-Z\.\'\-\+\/\_\\0-9]*    { return(SYM_TOK); }
180
181
182%%
183
184#endif
Note: See TracBrowser for help on using the repository browser.