source: vis_dev/cusp-1.1/src/smt/smt.y @ 23

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

cusp added

File size: 16.6 KB
Line 
1%{
2/**CFile*****************************************************************
3
4  FileName    [smt.y]
5
6  PackageName [smt]
7
8  Synopsis    [Yacc for formula parser.]
9
10  SeeAlso     [smt.h]
11 
12  Author      [Hyondeuk Kim]
13
14  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
15
16  All rights reserved.
17
18  Redistribution and use in source and binary forms, with or without
19  modification, are permitted provided that the following conditions
20  are met:
21
22  Redistributions of source code must retain the above copyright
23  notice, this list of conditions and the following disclaimer.
24
25  Redistributions in binary form must reproduce the above copyright
26  notice, this list of conditions and the following disclaimer in the
27  documentation and/or other materials provided with the distribution.
28
29  Neither the name of the University of Colorado nor the names of its
30  contributors may be used to endorse or promote products derived from
31  this software without specific prior written permission.
32
33  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
34  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
35  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
36  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
37  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
38  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
39  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
40  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
41  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
42  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
43  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
44  POSSIBILITY OF SUCH DAMAGE.]
45
46******************************************************************************/
47
48#ifdef HAVE_LIBGMP
49 
50#include <stdlib.h>
51#include "smt.h"
52
53/*
54 * The following is a workaround for a bug in bison, which generates code
55 * that uses alloca().  Their lengthy sequence of #ifdefs for defining
56 * alloca() does the wrong thing for HPUX (it should do what is defined below)
57 */
58
59#ifdef __hpux
60#  include <alloca.h>
61#endif
62
63#ifndef yytext
64#define yytext SmtYytext
65#endif
66
67  //static char rcsid[] UNUSED = "$Id: smt.y,v 1.6 2009-04-13 11:07:58 hhkim Exp $";
68
69/*---------------------------------------------------------------------------*/
70/* Variable declarations                                                     */
71/*---------------------------------------------------------------------------*/
72
73#include "smtLex.c"
74
75%}
76
77/*---------------------------------------------------------------------------*/
78/*      Grammar declarations                                                 */
79/*---------------------------------------------------------------------------*/
80
81%union {
82  smtFml_t *fml;       
83  char *str;
84}
85
86%type <fml> benchmark bench_name bench_attributes bench_attribute status sort_symbs sort_symb_decls fun_symb_decls fun_symb_decl pred_symb_decls pred_symb_decl an_formulas an_formula quant_vars quant_var quant_symb connective an_atom prop_atom an_terms an_term basic_term annotations annotation
87%type <str> user_value sort_symb_decl sort_symb pred_symb fun_symb attribute fvar var logic_name
88
89%token TRUE_TOK
90%token FALSE_TOK
91%token ITE_TOK
92%token NOT_TOK
93%token IMPLIES_TOK
94%token IF_THEN_ELSE_TOK
95%token AND_TOK
96%token OR_TOK
97%token XOR_TOK
98%token IFF_TOK
99%token EXISTS_TOK
100%token FORALL_TOK
101%token LET_TOK
102%token FLET_TOK
103%token NOTES_TOK
104%token SORTS_TOK
105%token FUNS_TOK
106%token PREDS_TOK
107%token EXTENSIONS_TOK
108%token DEFINITION_TOK
109%token AXIOMS_TOK
110%token LOGIC_TOK
111%token COLON_TOK
112%token LPAREN_TOK
113%token RPAREN_TOK
114%token SAT_TOK
115%token UNSAT_TOK
116%token UNKNOWN_TOK
117%token ASSUMPTION_TOK
118%token FORMULA_TOK
119%token STATUS_TOK
120%token BENCHMARK_TOK
121%token EXTRASORTS_TOK
122%token EXTRAFUNS_TOK
123%token EXTRAPREDS_TOK
124%token LANGUAGE_TOK
125%token DOLLAR_TOK
126%token EQUALS_TOK
127%token DISTINCT_TOK
128%token SEMICOLON_TOK
129%token EOF_TOK
130%token NUMERAL_TOK
131%token VAR_TOK
132%token SYM_TOK
133%token STRING_TOK
134%token AR_SYMB 
135%token USER_VAL_TOK
136
137/* precedence is specified here from lowest to highest */
138
139%nonassoc FORMULA_TOK
140%nonassoc LPAREN_TOK RPAREN_TOK
141%nonassoc OR_TOK XOR_TOK
142%nonassoc AND_TOK
143%nonassoc ITE_TOK IF_THEN_ELSE_TOK IMPLIES_TOK IFF_TOK FLET_TOK LET_TOK
144%nonassoc AR_SYMB EQUALS_TOK DISTINCT_TOK
145%nonassoc VAR_TOK NUMERAL_TOK SYM_TOK TRUE_TOK FALSE_TOK
146%nonassoc NOT_TOK EXISTS_TOK FORALL_TOK
147
148%%
149
150/*---------------------------------------------------------------------------*/
151/*      Grammar rules                                                        */
152/*---------------------------------------------------------------------------*/
153
154benchmark:
155LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
156{
157
158};
159
160bench_name:
161SYM_TOK
162{
163
164};
165
166bench_attributes:
167bench_attribute bench_attributes {/*$1::$2*/}
168| bench_attribute {/*[$1]*/};
169
170bench_attribute:
171COLON_TOK ASSUMPTION_TOK an_formula
172{
173
174}
175| COLON_TOK FORMULA_TOK an_formula
176{
177  /* root fml is the subfml */
178  gvar->fml = (smtFml_t *) ((smtFml_t *) $3)->subfmlArr->space[0];
179}
180| COLON_TOK STATUS_TOK status
181{
182
183}
184| COLON_TOK LOGIC_TOK logic_name
185{
186  if ( !strcmp($3, "QF_IDL") ) {
187    gvar->flag |= IDL_MASK;
188    gvar->epsilon = 1;
189    gvar->epsilonless = 0;
190  } else if ( !strcmp($3, "QF_RDL") ) {
191    gvar->flag |= RDL_MASK; 
192    gvar->epsilon = 0.00001;
193    gvar->epsilonless = 0.000001;
194  } else if ( !strcmp($3, "QF_LIA") ) {
195    gvar->flag |= LIA_MASK;
196    gvar->epsilon = 1;
197    gvar->epsilonless = 0;
198  } else if ( !strcmp($3, "QF_LRA") ) {
199    gvar->flag |= LRA_MASK;
200    gvar->epsilon = 0.00001;
201    gvar->epsilonless = 0.000001;
202  } else {
203    gvar->flag |= UNKNOWN_MASK;
204    smt_print_unknown();
205    exit(0);
206  }
207 
208  free($3); 
209}
210| COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symb_decls RPAREN_TOK {/*EXTRASORTS($4)*/}
211| COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK
212{
213}
214| COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
215{
216}
217| COLON_TOK NOTES_TOK STRING_TOK {/*NOTES($3)*/}
218| annotation {/*ANNOTATION($1)*/};
219
220logic_name:
221SYM_TOK {
222  $$ = util_strsav(yytext);
223};
224
225status:
226SAT_TOK {
227  /*SAT*/
228  gvar->status = 1;
229}
230| UNSAT_TOK {
231  /*UNSAT*/
232  gvar->status = 0;
233}
234| UNKNOWN_TOK {
235  /*UNKNOWN*/
236  gvar->status = 2;
237};
238
239sort_symbs:
240sort_symbs sort_symb
241{
242
243}
244| sort_symb
245{
246
247};
248
249sort_symb_decls:
250sort_symb_decls sort_symb_decl
251{
252
253}
254| sort_symb_decl
255{
256  $$ = (smtFml_t *) $1;
257};
258
259fun_symb_decls:
260fun_symb_decls fun_symb_decl
261{
262  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
263  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);   
264
265  $$ = $1;
266}
267| fun_symb_decl
268{
269  $$ = (smtFml_t *) $1;
270};
271
272fun_symb_decl:
273LPAREN_TOK fun_symb sort_symbs sort_symb annotations RPAREN_TOK
274{
275
276}
277| LPAREN_TOK fun_symb sort_symbs sort_symb RPAREN_TOK
278{
279
280}
281| LPAREN_TOK fun_symb sort_symb annotations RPAREN_TOK
282{
283
284}
285| LPAREN_TOK fun_symb sort_symb RPAREN_TOK
286{
287  /* fun_symb: ex: extrafuns(numerical var) */
288  if (!st_lookup(gvar->fun_table, $2, (char **) &(gvar->tfml))) {
289    /* new fun_symb */
290    gvar->tfml = smt_create_function_symbol($2);
291    st_insert(gvar->fun_table, $2, (char *) gvar->tfml);
292    gvar->nvar = smt_create_numerical_variable($2, gvar->tfml);
293    gvar->nvarArr = sat_array_insert(gvar->nvarArr, (long) gvar->nvar);
294  } else {
295    free($2);
296  }
297
298  free($3);
299
300  $$ = gvar->tfml;
301};
302
303pred_symb_decls:
304pred_symb_decls pred_symb_decl
305{
306  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
307  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml); 
308
309  $$ = $1;
310}
311| pred_symb_decl
312{
313  $$ = $1;
314};
315
316pred_symb_decl:
317LPAREN_TOK pred_symb sort_symbs annotations RPAREN_TOK
318{
319
320}
321| LPAREN_TOK pred_symb annotations RPAREN_TOK
322{
323
324}
325| LPAREN_TOK pred_symb sort_symbs RPAREN_TOK
326{
327
328}
329| LPAREN_TOK pred_symb RPAREN_TOK
330{
331  /* pred_symb: ex: extrapreds(boolean var) */
332  if (!st_lookup(gvar->pred_table, $2, (char **)&(gvar->tfml))) {
333    /* new pred_symb */
334    gvar->tfml = smt_create_predicate_symbol($2);
335    st_insert(gvar->pred_table, $2, (char *) gvar->tfml);
336    gvar->bvar = smt_create_bool_variable($2, gvar->tfml);
337    gvar->bvarArr = sat_array_insert(gvar->bvarArr, (long) gvar->bvar);
338  } else {
339    free($2);
340  }
341
342  $$ = gvar->tfml;
343};
344
345an_formulas:
346an_formulas an_formula
347{
348  /* add an_formula to an_formulas */
349  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
350  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);
351
352  $$ = $1;
353}
354| an_formula
355{
356  $$ = $1;
357};
358
359an_formula:
360an_atom
361{
362  $$ = $1;
363}
364| LPAREN_TOK connective an_formulas annotations RPAREN_TOK
365{
366
367}
368| LPAREN_TOK connective an_formulas RPAREN_TOK
369{
370  gvar->tfml = (smtFml_t *) $3;
371  gvar->tfml->type = (smtFmlType_t) $2;
372  smt_increase_subfml_ins(gvar->tfml);
373
374  $$ = smt_create_returning_formula(gvar->tfml);
375}
376| LPAREN_TOK quant_symb quant_vars an_formula annotations RPAREN_TOK
377{
378
379}
380| LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK
381{
382
383}
384| LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK
385{
386
387}
388| LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK
389{
390  /* replace var in formula with a term */
391  gvar->tfml = (smtFml_t *) $5->subfmlArr->space[0];
392  smt_duplicate_formula((smtFml_t *) $4, gvar->tfml); 
393
394  $$ = $7;
395}
396| LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK
397{
398
399}
400| LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK
401{
402  /* replace var in formula with a formula */
403  gvar->tfml = (smtFml_t *) $5->subfmlArr->space[0];
404  smt_duplicate_formula((smtFml_t *) $4, gvar->tfml);
405
406  if (smt_is_atom_formula((smtFml_t *) $4))
407    gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) $4);
408
409  $$ = $7;
410};
411
412var:
413VAR_TOK
414{
415  /* ?<var_tok>:
416     term variable for let */
417  gvar->str = util_strsav(yytext);
418
419  if (st_lookup(gvar->term_var_table, gvar->str,
420                (char **)&(gvar->tfml))) {
421    free(gvar->str);
422  } else {
423    gvar->tfml = smt_create_term_variable(gvar->str);
424    st_insert(gvar->term_var_table, gvar->str, (char *) gvar->tfml);
425  }
426
427  $$ = (char *) gvar->tfml;
428};
429
430quant_vars:
431quant_vars quant_var
432{
433
434}
435| quant_var
436{
437
438};
439
440quant_var:
441LPAREN_TOK var sort_symb RPAREN_TOK
442{
443 
444};
445
446quant_symb:
447EXISTS_TOK { /*EXISTS*/ }
448| FORALL_TOK { /*FORALL*/ };
449
450connective:
451NOT_TOK
452{
453  $$ = (smtFml_t *) NOT_c;
454}
455| IMPLIES_TOK
456{
457  $$ = (smtFml_t *) IMP_c;
458}
459| IF_THEN_ELSE_TOK
460{
461  $$ = (smtFml_t *) ITE_c;
462}
463| AND_TOK
464{
465  $$ = (smtFml_t *) AND_c;
466}
467| OR_TOK
468{
469  $$ = (smtFml_t *) OR_c;
470}
471| XOR_TOK
472{
473  $$ = (smtFml_t *) XOR_c;
474}
475| IFF_TOK
476{
477  $$ = (smtFml_t *) IFF_c;
478};
479
480an_atom:
481prop_atom
482
483  $$ = $1;
484}
485| LPAREN_TOK prop_atom annotations RPAREN_TOK
486{
487
488}
489| LPAREN_TOK pred_symb an_terms annotations RPAREN_TOK
490{
491
492}
493| LPAREN_TOK pred_symb an_terms RPAREN_TOK
494{
495  /* atom: pred_symb(ex: <, >, ...) terms */
496  gvar->tfml = $3;
497  gvar->tfml->type = smt_get_ar_symbol($2);
498  smt_increase_subfml_ins(gvar->tfml);
499
500  gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) gvar->tfml);
501
502  free($2);
503
504  /* create returning formula */
505  $$ = smt_create_returning_formula(gvar->tfml);
506}
507| LPAREN_TOK EQUALS_TOK an_terms an_term annotations RPAREN_TOK
508{
509
510}
511| LPAREN_TOK EQUALS_TOK an_terms an_term RPAREN_TOK
512{
513  /* equality atom: = terms */
514  gvar->tfml = (smtFml_t *) $4->subfmlArr->space[0];
515  $3->type = EQ_c;
516  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
517  gvar->tfml = $3;
518  smt_increase_subfml_ins(gvar->tfml);
519 
520  gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) gvar->tfml);
521
522  /* create returning formula */
523  $$ = smt_create_returning_formula(gvar->tfml);
524}
525| LPAREN_TOK DISTINCT_TOK an_terms an_term annotations RPAREN_TOK
526{
527
528}
529| LPAREN_TOK DISTINCT_TOK an_terms an_term RPAREN_TOK
530{
531  /* disequality atom: != terms */
532  gvar->tfml = (smtFml_t *) $4->subfmlArr->space[0];
533  $3->type = NEQ_c;
534  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
535  gvar->tfml = $3;
536  gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) gvar->tfml);
537 
538  /* create returning formula */
539  $$ = smt_create_returning_formula(gvar->tfml);
540};
541
542prop_atom:
543TRUE_TOK
544{
545  gvar->str = util_strsav(yytext);
546 
547  if (st_lookup(gvar->pred_table, gvar->str, (char **)&(gvar->tfml))) {
548    free(gvar->str);
549  } else {
550    gvar->tfml = smt_create_constant_predicate_symbol(gvar->str, 1);
551    st_insert(gvar->pred_table, gvar->str, (char *) gvar->tfml);
552  }
553 
554  /* create returning formula */
555  $$ = smt_create_returning_formula(gvar->tfml);
556}
557| FALSE_TOK
558{
559  gvar->str = util_strsav(yytext);
560 
561  if (st_lookup(gvar->pred_table, gvar->str,
562                (char **)&(gvar->tfml))) {
563    free(gvar->str);
564  } else {
565    gvar->tfml = smt_create_constant_predicate_symbol(gvar->str, 0);
566    st_insert(gvar->pred_table, gvar->str, (char *) gvar->tfml);
567  }
568
569  /* create returning formula */
570  $$ = smt_create_returning_formula(gvar->tfml);
571}
572| fvar
573{
574  gvar->tfml = (smtFml_t *) $1;
575   
576  /* create returning formula */
577  $$ = smt_create_returning_formula(gvar->tfml);
578}
579| pred_symb
580{
581  if (st_lookup(gvar->pred_table, $1, (char **)&(gvar->tfml))) {
582    free($1);
583  } else {
584    gvar->tfml = smt_create_predicate_symbol($1);
585    st_insert(gvar->pred_table, $1, (char *) gvar->tfml);
586    gvar->bvar = smt_create_bool_variable($1, gvar->tfml);
587    gvar->bvarArr = sat_array_insert(gvar->bvarArr, (long) gvar->bvar);
588  }
589 
590  /* create returning formula */
591  $$ = smt_create_returning_formula(gvar->tfml);
592};
593
594an_terms:
595an_terms an_term
596{
597  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
598  assert(gvar->tfml->type!=NONE_c);
599  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);
600
601  $$ = $1;
602}
603| an_term
604{
605  $$ = $1;
606};
607
608an_term:
609basic_term
610{
611  $$ = $1;
612}
613| LPAREN_TOK basic_term annotations RPAREN_TOK
614{
615
616}
617| LPAREN_TOK fun_symb an_terms annotations RPAREN_TOK
618{
619
620}
621| LPAREN_TOK fun_symb an_terms RPAREN_TOK
622{
623  /* funtion symbol(ex: +, -, *, /, ...  term */
624  gvar->tfml = $3;
625  gvar->tfml->type = smt_get_ar_symbol($2);
626  smt_increase_subfml_ins(gvar->tfml);
627  free($2);
628
629  /* create returning formula */
630  $$ = smt_create_returning_formula(gvar->tfml);
631}
632| LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK
633{
634
635}
636| LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK
637{
638  gvar->flag |= TERM_ITE_MASK;
639
640  gvar->tfml = (smtFml_t *) $4->subfmlArr->space[0];
641  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
642  gvar->tfml = (smtFml_t *) $5->subfmlArr->space[0];
643  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
644  $3->type = ITE_c;
645
646  /* create returning formula */
647  gvar->tfml = (smtFml_t *) $3;
648  smt_increase_subfml_ins(gvar->tfml);
649  $$ = smt_create_returning_formula(gvar->tfml);
650};
651
652basic_term:
653var
654{
655  gvar->tfml = (smtFml_t *) $1;
656
657  /* create returning formula */
658  $$ = smt_create_returning_formula(gvar->tfml);
659}
660| NUMERAL_TOK
661{
662  /* constant */
663  gvar->str = util_strsav(yytext);
664
665  if (st_lookup(gvar->num_table, gvar->str, (char **)&(gvar->tfml))) {
666    free(gvar->str);
667  } else {
668    gvar->tfml = smt_create_constant_formula(gvar->str);
669    st_insert(gvar->num_table, gvar->str, (char *) gvar->tfml);
670  }
671
672  /* create returning formula */
673  $$ = smt_create_returning_formula(gvar->tfml);
674}
675| fun_symb
676{
677  if (st_lookup(gvar->fun_table, $1, (char **)&(gvar->tfml))) {
678    free($1);
679  } else {
680    if (gvar->flag & IDL_MASK || gvar->flag & LIA_MASK)
681      gvar->tfml = smt_create_function_symbol($1);
682    else if (gvar->flag & RDL_MASK || gvar->flag & LRA_MASK)
683      gvar->tfml = smt_create_function_symbol($1);
684  }
685 
686  /* create returning formula */
687  $$ = smt_create_returning_formula(gvar->tfml);
688};
689
690annotations:
691annotation annotations
692{
693
694}
695| annotation
696{
697  $$ = $1;
698};
699
700annotation:
701attribute
702{
703  $$ = (smtFml_t *) $1;
704}
705| attribute user_value
706{
707
708};
709
710user_value:
711USER_VAL_TOK {};
712
713sort_symb_decl:
714SYM_TOK
715{
716  $$ = util_strsav(yytext);
717};
718
719sort_symb:
720SYM_TOK
721{
722  $$ = util_strsav(yytext);
723};
724
725pred_symb:
726SYM_TOK
727{ /* returns the name of the pred_symb : predicate */
728  $$ = util_strsav(yytext);
729}
730| AR_SYMB
731{ /* returns arith symbol: ex: <, >, =, ... */
732  $$ = util_strsav(yytext);
733};
734
735fun_symb:
736SYM_TOK
737{ /* returns the name of the fun_symb : numerical variable */
738  gvar->str = util_strsav(yytext);
739  assert(gvar->str);
740  $$ = gvar->str;
741}
742| AR_SYMB
743{ /* returns arith symbol: ex: +, -, *, /, ... */
744  gvar->str = util_strsav(yytext);
745  assert(gvar->str);
746  $$ = gvar->str;
747};
748   
749attribute:
750COLON_TOK SYM_TOK
751{
752 
753};
754
755fvar:
756DOLLAR_TOK SYM_TOK
757{
758  gvar->str = util_strsav(yytext);
759
760  /* $<simple_identifier>:
761     intermediate variable that substitutes propostional atom */
762  if (st_lookup(gvar->fml_var_table, gvar->str,
763                (char **)&(gvar->tfml))) {
764    free(gvar->str);
765  } else {
766    gvar->tfml = smt_create_fml_variable(gvar->str);
767    st_insert(gvar->fml_var_table, gvar->str, (char *) gvar->tfml);
768  }
769
770  $$ = (char *) gvar->tfml;   
771};
772
773%%
774 
775#endif
Note: See TracBrowser for help on using the repository browser.