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

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

cusp added

File size: 33.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [smtFml.c]
4
5  PackageName [smt]
6
7  Synopsis    [Routines for smt function.]
8
9  Author      [Hyondeuk Kim]
10
11  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
12
13  All rights reserved.
14
15  Redistribution and use in source and binary forms, with or without
16  modification, are permitted provided that the following conditions
17  are met:
18
19  Redistributions of source code must retain the above copyright
20  notice, this list of conditions and the following disclaimer.
21
22  Redistributions in binary form must reproduce the above copyright
23  notice, this list of conditions and the following disclaimer in the
24  documentation and/or other materials provided with the distribution.
25
26  Neither the name of the University of Colorado nor the names of its
27  contributors may be used to endorse or promote products derived from
28  this software without specific prior written permission.
29
30  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41  POSSIBILITY OF SUCH DAMAGE.]
42
43******************************************************************************/
44
45#ifdef HAVE_LIBGMP
46
47#include "smt.h"
48
49smtFml_t *
50smt_create_formula(smtFmlType_t ftype, satArray_t * subfmlArr)
51{
52  smtFml_t * fml, * tfml;
53  int i;
54
55  /* check for redundant NOT type */
56  if (ftype == NOT_c && subfmlArr->size == 1) {
57    tfml = (smtFml_t *) subfmlArr->space[0];
58    if (tfml->type == NOT_c) {
59      fml = (smtFml_t *) tfml->subfmlArr->space[0];
60      return fml;
61    }     
62  }
63
64  fml = (smtFml_t *) malloc(sizeof(smtFml_t));
65  fml->id = 0;
66  fml->flag = 0;
67
68  fml->type = ftype;
69 
70  if (subfmlArr == 0) {
71    fml->subfmlArr = 0;
72    return fml;
73  }
74
75  fml->subfmlArr = sat_array_alloc(subfmlArr->size);
76
77  for(i = 0; i < subfmlArr->size; i++) {
78    tfml = (smtFml_t *) subfmlArr->space[i];
79    fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) tfml);
80  }
81
82  fml->aig_node = Aig_NULL;
83  fml->avar = 0;
84  fml->bvar = 0;
85  fml->nvar = 0;
86  fml->nNeg = 0;
87  fml->ins = 0;
88  fml->value = 0;
89
90  if (gvar->fmlArr) {
91    gvar->fmlArr = sat_array_insert(gvar->fmlArr, (long) fml); 
92    fml->id = gvar->fmlArr->size;
93  } 
94
95  return fml;
96}
97
98void
99smt_duplicate_formula(smtFml_t * new_fml, smtFml_t * org)
100{
101  smtFml_t * tfml;
102  int i;
103
104  /* this duplicates the elements of org to new_fml */
105
106  new_fml->id = org->id;
107
108  if (org->flag & TRUE_MASK)
109    new_fml->flag |= TRUE_MASK;
110  else if (org->flag & FALSE_MASK)
111    new_fml->flag |= FALSE_MASK;
112
113  new_fml->type = org->type;
114  new_fml->subfmlArr->size = 0;
115
116  for(i = 0; i < org->subfmlArr->size; i++) {
117    tfml = (smtFml_t *) org->subfmlArr->space[i];
118    new_fml->subfmlArr = sat_array_insert(new_fml->subfmlArr, (long) tfml);
119  }
120 
121  new_fml->aig_node = org->aig_node;
122
123  new_fml->avar = org->avar;
124  new_fml->bvar = org->bvar;
125  new_fml->nvar = org->nvar;
126  new_fml->value = org->value;
127
128  return;
129}
130
131smtFml_t *
132smt_create_identical_formula(smtFml_t * fml)
133{
134  smtFml_t * new_fml, * subfml;
135  int i;
136
137  new_fml = (smtFml_t *) malloc(sizeof(smtFml_t));
138
139  new_fml->id = fml->id;
140  new_fml->flag = fml->flag;
141  new_fml->type = fml->type;
142  new_fml->subfmlArr = sat_array_alloc(fml->subfmlArr->size);
143
144  for(i = 0; i < fml->subfmlArr->size; i++) {
145    subfml = (smtFml_t *) fml->subfmlArr->space[i];
146    new_fml->subfmlArr = sat_array_insert(new_fml->subfmlArr, (long)subfml);
147  }
148
149  new_fml->aig_node = fml->aig_node;
150
151  new_fml->avar = fml->avar;
152  new_fml->bvar = fml->bvar;
153  new_fml->nvar = fml->nvar;
154 
155  new_fml->nNeg = fml->nNeg;
156  new_fml->ins = fml->ins;
157  new_fml->value = fml->value;
158
159  return new_fml;
160}
161
162smtFml_t *
163smt_simplify_formula(smtFml_t * fml)
164{
165  smtFml_t * rfml = 0;
166  smtFml_t * tfml;
167  int i;
168 
169  for(i = 0; i < fml->subfmlArr->size; i++) {
170    tfml = (smtFml_t *) fml->subfmlArr->space[i];
171    if (tfml->type != PRED_c && tfml->type != FVAR_c &&
172        tfml->type != fml->type) {
173      rfml = 0;
174      break;
175    }
176    if (rfml == 0 && tfml->type == fml->type) 
177      rfml = tfml;
178  }
179
180  if (rfml) {
181    for(i = 0; i < fml->subfmlArr->size; i++) {
182      tfml = (smtFml_t *) fml->subfmlArr->space[i];
183      if (tfml != rfml) 
184        rfml->subfmlArr = sat_array_insert(rfml->subfmlArr, (long) tfml);
185    }
186  } else {
187    rfml = fml;
188  }
189
190  return rfml;
191}
192
193void
194smt_increase_subfml_ins(smtFml_t * fml)
195{
196  smtFml_t * subfml;
197  int i;
198
199  for(i = 0; i < fml->subfmlArr->size; i++) {
200    subfml = (smtFml_t *) fml->subfmlArr->space[i];
201    subfml->ins++;
202  }
203}
204
205void
206smt_add_fml_to_array(smtFml_t * fml)
207{
208  if (!(fml->flag & IN_ARR_MASK)) {
209    gvar->fmlArr = sat_array_insert(gvar->fmlArr, (long) fml);
210    fml->flag |= IN_ARR_MASK;
211  }
212}
213
214smtFml_t *
215smt_create_returning_formula(smtFml_t * fml)
216{
217  smtFml_t * rfml;
218
219  /*
220     returning formula is needed for getting parent formula earlier
221     this enables flet to to substitute a var with replace_formula
222  */
223
224  gvar->tfmlArr->size = 0;
225  assert(fml->type!=NONE_c);
226  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fml);
227  rfml = smt_create_formula(NONE_c, gvar->tfmlArr);
228 
229  return rfml;
230}
231
232smtFml_t *
233smt_create_function_symbol(char * fs_name)
234{
235  smtFml_t * fml;
236
237  gvar->tfmlArr->size = 0;
238  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fs_name); 
239  fml = smt_create_formula(FUN_c, gvar->tfmlArr);
240
241  return fml;
242}
243
244smtFml_t *
245smt_create_predicate_symbol(char * ps_name)
246{
247  smtFml_t *fml;
248
249  gvar->tfmlArr->size = 0;
250  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) ps_name); 
251  fml = smt_create_formula(PRED_c, gvar->tfmlArr);
252
253  return fml;
254}
255
256smtFml_t *
257smt_create_constant_predicate_symbol(char * ps_name, int value)
258{
259  smtFml_t *fml;
260
261  gvar->tfmlArr->size = 0;
262  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) ps_name); 
263  fml = smt_create_formula(PRED_c, gvar->tfmlArr);
264
265  if (value==1) fml->flag |= TRUE_MASK;
266  else if (value==0) fml->flag |= FALSE_MASK;
267
268  return fml; 
269}
270
271smtFml_t *
272smt_create_fml_variable(char * fname)
273{
274  smtFml_t *fml;
275
276  gvar->tfmlArr->size = 0;
277  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fname); 
278  fml = smt_create_formula(FVAR_c, gvar->tfmlArr);
279
280  return fml;
281}
282
283smtFml_t *
284smt_create_term_variable(char * fs_name)
285{
286  smtFml_t * fml;
287 
288  gvar->tfmlArr->size = 0;
289  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fs_name); 
290  fml = smt_create_formula(TVAR_c, gvar->tfmlArr);
291
292  return fml;
293}
294
295smtFml_t *
296smt_create_constant_formula(char * cname)
297{
298  smtFml_t * fml;
299  long value;
300
301  gvar->tfmlArr->size = 0;
302  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) cname); 
303  fml = smt_create_formula(NUM_c, gvar->tfmlArr);
304  value = strtol(cname, 0, 10);
305
306  if (errno == ERANGE || value > INT_MAX) {
307    gvar->flag |= MP_CONST_MASK;
308  } else {
309    fml->value = (int) value;
310  }
311
312  return fml;
313}
314
315void
316smt_simplify_term_fml(smtFml_t * fml, st_table * num_table)
317{
318  smtFml_t * subfml, * tfml;
319  char * str;
320  int value = 0;
321  int i;
322
323  if (fml->type == ADD_c) {
324    for(i = 0; i < fml->subfmlArr->size; i++) {
325      subfml = (smtFml_t *) fml->subfmlArr->space[i];
326      if (subfml->type != NUM_c) return; 
327      value += subfml->value;
328    }
329    str = (char *) malloc(sizeof(char) * 10);
330    sprintf(str, "%d", value);
331    /* e.g. : (3 + 4) = 7 */
332    if (st_lookup(num_table, str, (char **)&(tfml))) {
333      free(str);
334      smt_duplicate_formula(fml, tfml);
335    } else {
336      fml->type = NUM_c;
337      fml->subfmlArr->size = 0;
338      fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) str);
339      fml->value = value;
340      st_insert(num_table, str, (char *) fml);
341    }
342
343  } else if (fml->type == SUB_c) {
344    subfml = (smtFml_t *) fml->subfmlArr->space[0];
345    if (subfml->type != NUM_c) return;
346    value = subfml->value;
347    subfml = (smtFml_t *) fml->subfmlArr->space[1];
348    if (subfml->type != NUM_c) return;
349    value = value - subfml->value;
350    if (value < 0) {
351      fprintf(stdout, "simplifier does not handle minus value\n");
352      return;
353    }
354    str = (char *) malloc(sizeof(char) * 10);
355    sprintf(str, "%d", value);
356    /* e.g. : (5 - 4) = 7 */
357    if (st_lookup(num_table, str, (char **)&(tfml))) {
358      free(str);
359      smt_duplicate_formula(fml, tfml);
360    } else {
361      fml->type = NUM_c;
362      fml->subfmlArr->size = 0;
363      fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) str);
364      fml->value = value;
365      st_insert(num_table, str, (char *) fml);
366    }
367  }
368
369  return;
370}
371
372void
373smt_save_flet_pair(smtFml_t * fvar_fml, smtFml_t * fml)
374{
375  smtFlet_t * flet = (smtFlet_t *) malloc(sizeof(smtFlet_t));
376
377  flet->fvar_fml = fvar_fml;
378  flet->fml = fml;
379
380  gvar->fletArr = sat_array_insert(gvar->fletArr, (long) flet);
381}
382
383void
384smt_init_formula_flag(smtManager_t * sm)
385{
386  smtFml_t * fml;
387  int i;
388
389  for(i = 0; i < sm->fmlArr->size; i++) {
390    fml = (smtFml_t *) sm->fmlArr->space[i];
391    fml->flag = 0;
392  }
393}
394
395void
396smt_init_fml_visited_flag(smtManager_t * sm)
397{
398  smtFml_t * fml;
399  int i;
400
401  for(i = 0; i < sm->fmlArr->size; i++) {
402    fml = (smtFml_t *) sm->fmlArr->space[i];
403    fml->flag &= RESET_FML_VISITED_MASK;
404  }
405}
406
407void
408smt_init_fml_queued_flag(smtManager_t * sm)
409{
410  smtFml_t * fml;
411  int i;
412
413  for(i = 0; i < sm->fmlArr->size; i++) {
414    fml = (smtFml_t *) sm->fmlArr->space[i];
415    fml->flag &= RESET_QUEUED_MASK;
416  }
417}
418
419char *
420smt_convert_fml_to_string(smtFml_t * fml) 
421{
422  smtFml_t * fml_a, * fml_b, * fml_c;
423  char * str_a = 0;
424  char * str_b = 0;
425  char * str_c = 0; 
426  char * tstr_a = 0;
427  char * tstr_b = 0;
428  char * tstr_c = 0;
429  char * result = 0;
430  char str_true[5] = "true";
431  char str_false[6] = "false";
432  int i;
433
434  if (fml == 0) {
435    return 0; 
436  }
437   
438  if (smt_is_leaf_fml(fml)) {
439    if (fml->flag & TRUE_MASK) 
440      result = util_strsav(str_true);
441    else if (fml->flag & FALSE_MASK) 
442      result = util_strsav(str_false);
443    else {
444      fml_a = (smtFml_t *) fml->subfmlArr->space[0];
445      result = util_strsav((char *) fml_a);
446    }
447  }
448  else if (fml->type == FLET_c) {
449    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
450    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
451    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
452    str_a = smt_convert_fml_to_string(fml_a);
453    str_b = smt_convert_fml_to_string(fml_b);
454    str_c = smt_convert_fml_to_string(fml_c);
455
456    tstr_a = util_strcat3("(flet ", "(", str_b);
457    tstr_b = util_strcat3(tstr_a, " ", str_c);
458    tstr_c = util_strcat3(tstr_b, ")", " ");
459    result = util_strcat3(tstr_c, str_a, ")");
460  }
461  else if (fml->type == NOT_c) {
462    fml_a = (smtFml_t *) fml->subfmlArr->space[0];   
463    str_a = smt_convert_fml_to_string(fml_a);
464    tstr_a = util_strcat3("not ", str_a, "");
465    result = util_strcat3("(", tstr_a, ")");
466  }
467  else if (fml->type == IMP_c) {
468    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
469    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
470    str_a = smt_convert_fml_to_string(fml_a);
471    str_b = smt_convert_fml_to_string(fml_b);
472    tstr_a = util_strcat3(" -> ", str_a, str_b);
473    result = util_strcat3("(", tstr_a, ")"); 
474  }
475  else if (fml->type == IFF_c) {
476    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
477    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
478    str_a = smt_convert_fml_to_string(fml_a);
479    str_b = smt_convert_fml_to_string(fml_b);
480    tstr_a = util_strcat3("iff ", str_a, " ");
481    tstr_b = util_strcat3(tstr_a, str_b, "");
482    result = util_strcat3("(", tstr_b, ")");
483  }
484  else if (fml->type == AND_c) {
485    tstr_a = util_strcat3("and ", "", "");
486    for(i = 0; i < fml->subfmlArr->size; i++) {
487      fml_a = (smtFml_t *) fml->subfmlArr->space[i];
488      str_a = smt_convert_fml_to_string(fml_a);
489      tstr_b = tstr_a;
490      tstr_a = util_strcat3(tstr_a, str_a, " ");
491      free(tstr_b);
492      free(str_a);
493      tstr_b = 0;
494      str_a = 0;
495    }
496    result = util_strcat3("(", tstr_a, ")");
497  }
498  else if (fml->type == OR_c) {
499    tstr_a = util_strcat3("or ", "", "");
500    for(i = 0; i < fml->subfmlArr->size; i++) {
501      fml_a = (smtFml_t *) fml->subfmlArr->space[i];
502      str_a = smt_convert_fml_to_string(fml_a);
503      tstr_b = tstr_a;
504      tstr_a = util_strcat3(tstr_a, str_a, " ");
505      free(tstr_b);
506      free(str_a);
507      tstr_b=0;
508      str_a=0;
509    }
510    result = util_strcat3("(", tstr_a, ")");
511  }
512  else if (fml->type == XOR_c) {
513    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
514    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
515    str_a = smt_convert_fml_to_string(fml_a);
516    str_b = smt_convert_fml_to_string(fml_b);
517    tstr_a = util_strcat3("xor ", str_a, " ");
518    tstr_b = util_strcat3(tstr_a, str_b, " ");
519    result = util_strcat3("(", tstr_b, ")");
520  }
521  else if (fml->type == NAND_c) {
522    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
523    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
524    str_a = smt_convert_fml_to_string(fml_a);
525    str_b = smt_convert_fml_to_string(fml_b);
526    tstr_a = util_strcat3("nand ", str_a, " ");
527    tstr_b = util_strcat3(tstr_a, str_b, " ");
528    result = util_strcat3("(", tstr_b, ")");
529  }
530  else if (fml->type == ITE_c) {
531    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
532    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
533    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
534    str_a = smt_convert_fml_to_string(fml_a);
535    str_b = smt_convert_fml_to_string(fml_b);
536    str_c = smt_convert_fml_to_string(fml_c);
537   
538    if ( smt_is_term_formula(fml_b) )
539      tstr_a = util_strcat3("ite ", str_a, " ");
540    else
541      tstr_a = util_strcat3("if_then_else ", str_a, " ");
542    tstr_b = util_strcat3(tstr_a, str_b, " ");
543    tstr_c = util_strcat3(tstr_b, str_c, "");
544    result = util_strcat3("(", tstr_c, ")");
545  }
546  else if (fml->type == TITE_c) {
547    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
548    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
549    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
550    str_a = smt_convert_fml_to_string(fml_a);
551    str_b = smt_convert_fml_to_string(fml_b);
552    str_c = smt_convert_fml_to_string(fml_c);
553    tstr_a = util_strcat3("if_then_else ", str_a, " ");
554    tstr_b = util_strcat3(tstr_a, str_b, " ");
555    tstr_c = util_strcat3(tstr_b, str_c, "");
556    result = util_strcat3("(", tstr_c, ")");
557  }
558  else if (fml->type == EQ_c) {
559    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
560    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
561    str_a = smt_convert_fml_to_string(fml_a);
562    str_b = smt_convert_fml_to_string(fml_b);
563    tstr_a = util_strcat3("= ", str_a, " ");
564    tstr_b = util_strcat3(tstr_a, str_b, "");
565    result = util_strcat3("(", tstr_b, ")");
566  }
567  else if (fml->type == NEQ_c) {
568    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
569    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
570    str_a = smt_convert_fml_to_string(fml_a);
571    str_b = smt_convert_fml_to_string(fml_b);
572    tstr_a = util_strcat3("!= ", str_a, " ");
573    tstr_b = util_strcat3(tstr_a, str_b, "");
574    result = util_strcat3("(", tstr_b, ")");
575  }
576  else if (fml->type == LT_c) {
577    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
578    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
579    str_a = smt_convert_fml_to_string(fml_a);
580    str_b = smt_convert_fml_to_string(fml_b);
581    tstr_a = util_strcat3("< ", str_a, " ");
582    tstr_b = util_strcat3(tstr_a, str_b, "");
583    result = util_strcat3("(", tstr_b, ")");
584  }
585  else if (fml->type == GT_c) {
586    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
587    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
588    str_a = smt_convert_fml_to_string(fml_a);
589    str_b = smt_convert_fml_to_string(fml_b);
590    tstr_a = util_strcat3("> ", str_a, " ");
591    tstr_b = util_strcat3(tstr_a, str_b, "");
592    result = util_strcat3("(", tstr_b, ")");
593  }
594  else if (fml->type == LE_c) {
595    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
596    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
597    str_a = smt_convert_fml_to_string(fml_a);
598    str_b = smt_convert_fml_to_string(fml_b);
599    tstr_a = util_strcat3("<= ", str_a, " ");
600    tstr_b = util_strcat3(tstr_a, str_b, "");
601    result = util_strcat3("(", tstr_b, ")");
602  }
603  else if (fml->type == GE_c) {
604    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
605    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
606    str_a = smt_convert_fml_to_string(fml_a);
607    str_b = smt_convert_fml_to_string(fml_b);
608    tstr_a = util_strcat3(">= ", str_a, " ");
609    tstr_b = util_strcat3(tstr_a, str_b, "");
610    result = util_strcat3("(", tstr_b, ")");
611  }
612  else if (fml->type == MUL_c) {
613    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
614    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
615    str_a = smt_convert_fml_to_string(fml_a);
616    str_b = smt_convert_fml_to_string(fml_b);
617    tstr_a = util_strcat3("* ", str_a, " ");
618    tstr_b = util_strcat3(tstr_a, str_b, "");
619    result = util_strcat3("(", tstr_b, ")");
620  }
621  else if (fml->type == DIV_c) {
622    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
623    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
624    str_a = smt_convert_fml_to_string(fml_a);
625    str_b = smt_convert_fml_to_string(fml_b);
626    tstr_a = util_strcat3("/ ", str_a, " ");
627    tstr_b = util_strcat3(tstr_a, str_b, "");
628    result = util_strcat3("(", tstr_b, ")");
629  }
630  else if (fml->type == REM_c) {
631    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
632    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
633    str_a = smt_convert_fml_to_string(fml_a);
634    str_b = smt_convert_fml_to_string(fml_b);
635    tstr_a = util_strcat3("% ", str_a, " ");
636    tstr_b = util_strcat3(tstr_a, str_b, "");
637    result = util_strcat3("(", tstr_b, ")");
638  }
639  else if (fml->type == ADD_c) {
640    tstr_a = util_strcat3("+ ", "", "");
641    for(i = 0; i < fml->subfmlArr->size; i++) {
642      fml_a = (smtFml_t *) fml->subfmlArr->space[i];
643      str_a = smt_convert_fml_to_string(fml_a);
644      tstr_b = tstr_a;
645      tstr_a = util_strcat3(tstr_a, str_a, " ");
646      free(tstr_b);
647      free(str_a);
648      tstr_b = 0;
649      str_a = 0;
650    }
651    result = util_strcat3("(", tstr_a, ")");
652  }
653  else if (fml->type == SUB_c) {
654    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
655    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
656    str_a = smt_convert_fml_to_string(fml_a);
657    str_b = smt_convert_fml_to_string(fml_b);
658    tstr_a = util_strcat3("- ", str_a, " ");
659    tstr_b = util_strcat3(tstr_a, str_b, "");
660    result = util_strcat3("(", tstr_b, ")");
661  }
662  else if (fml->type == MINUS_c) {
663    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
664    str_a = smt_convert_fml_to_string(fml_a);
665    tstr_a = util_strcat3("~ ", str_a, "");
666    result = util_strcat3("(", tstr_a, ")");
667  }
668  else if (fml->type == LET_c) {
669    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
670    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
671    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
672    str_a = smt_convert_fml_to_string(fml_a);
673    str_b = smt_convert_fml_to_string(fml_b);
674    str_c = smt_convert_fml_to_string(fml_c);
675    tstr_a = util_strcat3("let (", str_b, " ");
676    tstr_b = util_strcat3(tstr_a, str_c, ") ");
677    tstr_c = util_strcat3(tstr_b, str_a, "");
678    result = util_strcat3("(", tstr_c, ")");
679  }
680  else if (fml->type == FLET_c) {
681    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
682    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
683    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
684    str_a = smt_convert_fml_to_string(fml_a);
685    str_b = smt_convert_fml_to_string(fml_b);
686    str_c = smt_convert_fml_to_string(fml_c);
687    tstr_a = util_strcat3("flet (", str_b, " ");
688    tstr_b = util_strcat3(tstr_a, str_c, ") ");
689    tstr_c = util_strcat3(tstr_b, str_a, "");
690    result = util_strcat3("(", tstr_c, ")");
691  } else {
692    fprintf(stdout, "ERROR: Wrong FORMULA Type: %d\n", (int) fml->type);
693  }
694
695  if (str_a != 0) {
696    free(str_a);
697  }
698
699  if (str_b != 0) {
700    free(str_b);
701  }
702
703  if (str_c != 0) {
704    free(str_c);
705  }
706
707  if (tstr_a != 0) {
708    free(tstr_a);
709  }
710
711  if (tstr_b != 0) {
712    free(tstr_b);
713  }
714
715  if (tstr_c != 0) {
716    free(tstr_c);
717  }
718
719  return result;
720}
721
722char *
723smt_convert_fml_to_string_with_subfml(
724  smtFmlType_t type, 
725  satArray_t * subfmlArr)
726{
727  smtFml_t * subfml;
728  char * str_a, * str_b, * str_c;
729  int i;
730
731  str_a = (char *) malloc(sizeof(char) * 10); 
732  str_b = (char *) malloc(sizeof(char) * 10); 
733  sprintf(str_a, "%d", (int) type);
734
735  for(i = 0; i < subfmlArr->size; i++) {
736    subfml = (smtFml_t *) subfmlArr->space[i];
737    sprintf(str_b, "%p", subfml);
738    str_c = str_a;
739    str_a = util_strcat3(str_a, str_b, "");
740    free(str_c);
741  }
742
743  free(str_b);
744
745  return str_a;
746}
747
748int
749smt_is_leaf_fml(smtFml_t * fml)
750{
751  int is_leaf;
752 
753  is_leaf = (fml->type == FUN_c) || (fml->type == PRED_c) ||
754    (fml->type == FVAR_c) || (fml->type == TVAR_c) ||
755    (fml->type == NUM_c) ;
756
757  return is_leaf;
758}
759
760int
761smt_is_abstract_leaf_fml(smtFml_t * fml)
762{
763  int is_leaf;
764 
765  is_leaf = (fml->type == PRED_c) || (fml->type == FVAR_c) ||
766    (fml->type == EQ_c) || (fml->type == NEQ_c) || (fml->type == LT_c) ||
767    (fml->type == GT_c) || (fml->type == LE_c) || (fml->type == GE_c);
768
769  return is_leaf;
770}
771
772int
773smt_is_negated_abstract_leaf_fml(smtFml_t * fml)
774{
775  smtFml_t * subfml;
776  int is_leaf;
777
778  if (fml->type != NOT_c) {
779    return 0;
780  } else {
781    subfml = (smtFml_t *) fml->subfmlArr->space[0];
782    is_leaf = (subfml->type == PRED_c) || (subfml->type == FVAR_c) ||
783      (subfml->type == EQ_c) || (subfml->type == NEQ_c) ||
784      (subfml->type == LT_c) || (subfml->type == GT_c) || (subfml->type == LE_c) ||
785      (subfml->type == GE_c);
786  }
787
788  return is_leaf;
789}
790
791int
792smt_is_ite_chain_fml(smtFml_t * fml, int num_fml)
793{
794  smtFml_t * subfml_a, * subfml_b, * subfml_c;
795  smtQueue_t * Q;
796  int i, is_ite_chain = 1;
797
798  assert(fml->type == ITE_c);
799
800  Q = smt_create_queue(num_fml);
801 
802  smt_enqueue(Q, (long) fml);
803   
804  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {
805
806      if (fml->type == ITE_c) {
807        subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
808        subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
809        subfml_c = (smtFml_t *) fml->subfmlArr->space[2];
810       
811        if (subfml_a->type == AND_c) { /* cond : leaf or AND */
812#if 0
813          if (subfml_a->subfmlArr->size == 2) {
814            subfml_d = (smtFml_t *) subfml_a->subfmlArr->space[0];
815            subfml_e = (smtFml_t *) subfml_a->subfmlArr->space[1];
816            if (!smt_is_abstract_leaf_fml(subfml_d) ||
817                !smt_is_abstract_leaf_fml(subfml_e)) {
818              is_ite_chain = 0;
819              break;
820            }
821             
822          } else {
823            is_ite_chain = 0;
824            break;
825          }
826#endif
827          smt_enqueue(Q, (long) subfml_a);
828        } else if (!smt_is_abstract_leaf_fml(subfml_a)) {
829          is_ite_chain = 0;
830          break;
831        } 
832        if (subfml_b->type == AND_c) { /* then : leaf or AND */
833          smt_enqueue(Q, (long) subfml_b);
834        } else if (!smt_is_abstract_leaf_fml(subfml_b)) {
835          is_ite_chain = 0;
836          break;
837        } 
838        /* then : ITE or leaf or AND */
839        if (subfml_c->type == ITE_c || subfml_c->type == AND_c) { 
840          smt_enqueue(Q, (long) subfml_c);
841        } else if (!smt_is_abstract_leaf_fml(subfml_c)) {
842          is_ite_chain = 0;
843          break;
844        } 
845
846      } else if (fml->type == AND_c) {
847        for(i = 0; i < fml->subfmlArr->size; i++) {
848          subfml_a = (smtFml_t *) fml->subfmlArr->space[i];
849
850          if (subfml_a->type == AND_c) {
851            smt_enqueue(Q, (long) subfml_a);
852          } else if (!smt_is_abstract_leaf_fml(subfml_a)) {
853            is_ite_chain = 0;
854            break;
855          }
856        }
857      } else {
858        is_ite_chain = 0;
859        break;
860      }
861      /* } */
862  }
863     
864  smt_free_queue(Q);
865
866  return is_ite_chain;
867}
868
869int
870smt_is_atom_formula(smtFml_t * fml)
871{
872  int is_atom;
873 
874  is_atom = (fml->type == EQ_c) || (fml->type == NEQ_c) || 
875    (fml->type == LT_c) || (fml->type == GT_c) || (fml->type == LE_c) || 
876    (fml->type == GE_c);
877
878  return is_atom;
879}
880
881int
882smt_is_negated_atom_formula(smtFml_t * fml)
883{
884  smtFml_t * subfml;
885  int is_atom;
886
887  if (fml->type != NOT_c) {
888    return 0;
889  } else {
890    subfml = (smtFml_t *) fml->subfmlArr->space[0];
891    is_atom = (subfml->type == EQ_c) || (subfml->type == NEQ_c) ||
892      (subfml->type == LT_c) || (subfml->type == GT_c) ||
893      (subfml->type == LE_c) || (subfml->type == GE_c);
894  }
895
896  return is_atom;
897}
898
899int
900smt_is_boolean_formula(smtFml_t * fml)
901{
902  int is_bool;
903 
904  is_bool = (fml->type == PRED_c) || (fml->type == FVAR_c);
905
906  return is_bool;
907}
908
909int
910smt_is_negated_boolean_formula(smtFml_t * fml)
911{
912  smtFml_t * subfml;
913  int is_bool;
914
915  if (fml->type != NOT_c) {
916    return 0;
917  } else {
918    subfml = (smtFml_t *) fml->subfmlArr->space[0];
919    is_bool = (subfml->type == PRED_c) || (subfml->type == FVAR_c);
920  }
921
922  return is_bool;
923}
924
925int
926smt_is_arith_formula(smtFml_t * fml)
927{
928  if (fml->type == SUB_c || fml->type == ADD_c || fml->type == MUL_c ||
929      fml->type == DIV_c || fml->type == MINUS_c)
930    return 1;
931  else
932    return 0;
933}
934
935int
936smt_is_multi_arith_formula(smtFml_t * fml)
937{
938  if (fml->type == ADD_c || fml->type == MUL_c)
939    return 1;
940  else
941    return 0;
942}
943
944int
945smt_is_binary_arith_formula(smtFml_t * fml)
946{
947  if (fml->type == SUB_c || fml->type == DIV_c)
948    return 1;
949  else
950    return 0;
951}
952
953int
954smt_is_unary_arith_formula(smtFml_t * fml)
955{
956  if (fml->type == MINUS_c)
957    return 1;
958  else
959    return 0;
960}
961
962int
963smt_is_term_formula(smtFml_t * fml)
964{
965  if ( smt_is_arith_formula(fml) || fml->type == FUN_c || 
966       fml->type == NUM_c )
967    return 1;
968  else
969    return 0;
970}
971
972int
973smt_is_bool_atom_fml(smtFml_t * fml)
974{
975  smtFml_t * lfml, * rfml;
976  int is_const = 2, is_true = 2, lvalue, rvalue;
977
978  lfml = (smtFml_t *) fml->subfmlArr->space[0];
979  rfml = (smtFml_t *) fml->subfmlArr->space[1];
980
981  is_const = smt_get_constant_value_in_fml(lfml, &lvalue);
982 
983  if (is_const == 0) return 0;
984 
985  is_const = smt_get_constant_value_in_fml(rfml, &rvalue);
986
987  if (is_const == 0) return 0;
988
989  if (fml->type == EQ_c) {
990    if (lvalue == rvalue) {
991      is_true = 1; /* true */
992    } else {
993      is_true = 0; /* false */
994    }
995  } else if (fml->type == LE_c) {
996    if (lvalue <= rvalue) {
997      is_true = 1; /* true */
998    } else {
999      is_true = 0; /* false */
1000    }
1001  } else if (fml->type == LT_c) {
1002    if (lvalue < rvalue) {
1003      is_true = 1; /* true */
1004    } else {
1005      is_true = 0; /* false */
1006    }
1007  } else if (fml->type == GE_c) {
1008    if (lvalue >= rvalue) {
1009      is_true = 1; /* true */
1010    } else {
1011      is_true = 0; /* false */
1012    }
1013  } else if (fml->type == GT_c) {
1014    if (lvalue > rvalue) {
1015      is_true = 1; /* true */
1016    } else {
1017      is_true = 0; /* false */
1018    }
1019  }
1020
1021  fml->type = PRED_c;
1022
1023  assert(is_true != 2);
1024
1025  if (is_true) {
1026    fml->flag |= TRUE_MASK;
1027  } else {
1028    fml->flag |= FALSE_MASK;
1029  }
1030 
1031  return 1;
1032}
1033
1034int
1035smt_get_constant_value_in_fml(smtFml_t * fml, int * value)
1036{
1037  smtFml_t * lfml, * rfml, * tfml;
1038  int is_const, value_a, value_b;
1039  int i;
1040
1041  if (fml->type == NUM_c) {
1042    *value = fml->value;
1043  } else if (fml->type == MINUS_c) {
1044    tfml = (smtFml_t *) fml->subfmlArr->space[0];
1045    is_const = smt_get_constant_value_in_fml(tfml, &value_a);
1046    if (is_const == 0) return 0;
1047    *value = -value_a;
1048  } else if (fml->type == SUB_c) {
1049    lfml = (smtFml_t *) fml->subfmlArr->space[0];
1050    rfml = (smtFml_t *) fml->subfmlArr->space[1];
1051
1052    is_const = smt_get_constant_value_in_fml(lfml, &value_a);
1053    if (is_const == 0) return 0;
1054    is_const = smt_get_constant_value_in_fml(rfml, &value_b);
1055    if (is_const == 0) return 0;
1056    *value = value_a - value_b;
1057  } else if (fml->type == ADD_c) {
1058    for(i = 0, *value = 0; i < fml->subfmlArr->size; i++) {
1059      tfml = (smtFml_t *) fml->subfmlArr->space[i];
1060      is_const = smt_get_constant_value_in_fml(tfml, &value_a);
1061      if (is_const == 0) return 0;
1062      *value += value_a;
1063    }
1064  } else if (fml->type == MUL_c) {
1065    for(i = 0, *value = 1; i < fml->subfmlArr->size; i++) {
1066      tfml = (smtFml_t *) fml->subfmlArr->space[i];
1067      is_const = smt_get_constant_value_in_fml(tfml, &value_a);
1068      if (is_const == 0) return 0;
1069      *value *= value_a;
1070    }
1071  } else return 0;
1072
1073  return 1;
1074}
1075
1076void
1077smt_convert_eq_fml_to_ineq_fml(smtManager_t * sm)
1078{
1079  smtFml_t * avfml, * fml_a, * fml_b;
1080  satArray_t * avfmlArr = sat_array_alloc(sm->avfmlArr->size * 2);
1081  int existEq = 0;
1082  int i;
1083 
1084  for(i = 0; i < sm->avfmlArr->size; i++) {
1085    avfml = (smtFml_t *) sm->avfmlArr->space[i];
1086    if (avfml->type == EQ_c) {
1087      sm->stats->num_eq2ineq++;
1088
1089      smt_convert_eq_fml_into_ineq_and_fml(sm, avfml);
1090
1091      fml_a = (smtFml_t *) avfml->subfmlArr->space[0];
1092      fml_b = (smtFml_t *) avfml->subfmlArr->space[1];
1093      avfmlArr = sat_array_insert(avfmlArr, (long) fml_a);
1094      avfmlArr = sat_array_insert(avfmlArr, (long) fml_b);     
1095      existEq = 1;
1096
1097    } else if (avfml->type == NEQ_c) {
1098      sm->stats->num_eq2ineq++;
1099
1100      smt_convert_diseq_fml_into_ineq_or_fml(sm, avfml);
1101
1102      fml_a = (smtFml_t *) avfml->subfmlArr->space[0];
1103      fml_b = (smtFml_t *) avfml->subfmlArr->space[1];
1104      avfmlArr = sat_array_insert(avfmlArr, (long) fml_a);
1105      avfmlArr = sat_array_insert(avfmlArr, (long) fml_b);
1106      existEq = 1;
1107
1108    } else if ( smt_is_atom_formula(avfml) ) {
1109      avfmlArr = sat_array_insert(avfmlArr, (long) avfml);
1110    }
1111  }
1112
1113  if (existEq) {
1114    free(sm->avfmlArr);
1115    sm->avfmlArr = avfmlArr;
1116  } else {
1117    free(avfmlArr);
1118  }
1119}
1120
1121void
1122smt_add_flet_pair_formula(smtManager_t * sm)
1123{
1124  smtFml_t * root = sm->fml;
1125  smtFml_t * and_fml, * fvar_fml, * fml, * iff_fml;
1126  smtFlet_t * flet;
1127  int i;
1128 
1129  /* combine root with flet_pair formula */
1130 
1131  gvar->tfmlArr->size = 0;
1132  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) root);
1133  and_fml = smt_create_formula(AND_c, gvar->tfmlArr);
1134  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) and_fml);
1135   
1136  for(i = 0; i < sm->fletArr->size; i++) {
1137    flet = (smtFlet_t *) sm->fletArr->space[i]; 
1138    fvar_fml = flet->fvar_fml;
1139    fml = flet->fml;
1140    /* iff_fml = (fvar_fml <-> fml) */
1141    gvar->tfmlArr->size = 0;
1142    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fvar_fml);
1143    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fml);   
1144    iff_fml = smt_create_formula(IFF_c, gvar->tfmlArr); 
1145    and_fml->subfmlArr = sat_array_insert(and_fml->subfmlArr, (long) iff_fml);
1146    sm->fmlArr = sat_array_insert(sm->fmlArr, (long) iff_fml);
1147  } 
1148 
1149  sm->fml = and_fml;
1150}
1151
1152void 
1153smt_convert_eq_fml_into_ineq_and_fml(smtManager_t * sm, smtFml_t * fml)
1154{
1155  smtFml_t * leq_fml, * geq_fml;
1156
1157  assert(fml->type==EQ_c);
1158
1159  /* ax + by + ... <= c */
1160  leq_fml = smt_create_identical_formula(fml);
1161  leq_fml->type = LE_c;
1162  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) leq_fml);
1163  leq_fml->id = sm->fmlArr->size;
1164  leq_fml->ins = 1;
1165 
1166  /* ax + by + ... >= c */
1167  geq_fml = smt_create_identical_formula(fml);
1168  geq_fml->type = GE_c;
1169  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) geq_fml);
1170  geq_fml->id = sm->fmlArr->size;
1171  geq_fml->ins = 1;
1172   
1173  /* leq_fml /\ geq_fml */
1174  fml->type = AND_c;
1175  fml->subfmlArr->size = 0;
1176  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) leq_fml);
1177  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) geq_fml);
1178}
1179
1180void 
1181smt_convert_diseq_fml_into_ineq_or_fml(smtManager_t * sm, smtFml_t * fml)
1182{
1183  smtFml_t * lt_fml, * gt_fml;
1184
1185  assert(fml->type==NEQ_c);
1186
1187  /* ax + by + ... < c */
1188  lt_fml = smt_create_identical_formula(fml);
1189  lt_fml->type = LT_c;
1190  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) lt_fml);
1191  lt_fml->id = sm->fmlArr->size;
1192  lt_fml->ins = 1;
1193 
1194  /* ax + by + ... > c */
1195  gt_fml = smt_create_identical_formula(fml);
1196  gt_fml->type = GT_c;
1197  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) gt_fml);
1198  gt_fml->id = sm->fmlArr->size;
1199  gt_fml->ins = 1;
1200   
1201  /* lt_fml \/ gt_fml */
1202  fml->type = OR_c;
1203  fml->subfmlArr->size = 0;
1204  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) lt_fml);
1205  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) gt_fml);
1206}
1207
1208satArray_t *
1209smt_gather_bvar_in_fml(smtManager_t * sm, smtFml_t * fml)
1210{
1211  smtFml_t * ufml, * tfml;
1212  smtQueue_t * Q;
1213  satArray_t * bvarArr;
1214  int * bflags;
1215  int i, is_leaf, init_id, flag;
1216
1217  bvarArr = sat_array_alloc(sm->bvarArr->size);
1218
1219  bflags = (int *) malloc(sizeof(int) * sm->bvarArr->size);
1220 
1221  memset(bflags, 0, sizeof(int) * sm->bvarArr->size);
1222
1223  /* init_id = ((smtBvar_t *) sm->bvarArr->space[0])->id; */
1224  if (sm->avarArr) init_id = sm->avarArr->size + 1;
1225  else init_id = 1;
1226
1227  Q = smt_create_queue(sm->fmlArr->size);
1228 
1229  smt_enqueue(Q, (long) fml);
1230   
1231  while( (ufml = (smtFml_t *) smt_dequeue(Q)) ) {
1232
1233    is_leaf = smt_is_abstract_leaf_fml(ufml) || smt_is_leaf_fml(ufml);
1234
1235    if ( (!is_leaf) ) {
1236      for(i = 0; i < ufml->subfmlArr->size; i++) {
1237        tfml = (smtFml_t *) ufml->subfmlArr->space[i];
1238        smt_enqueue(Q, (long) tfml);
1239      }
1240    } else {
1241      if (ufml->bvar) {
1242        flag = bflags[ufml->bvar->id - init_id];
1243        if (!flag) {
1244          bvarArr = sat_array_insert(bvarArr, (long) ufml->bvar);
1245          bflags[ufml->bvar->id - init_id] = 1;
1246        }
1247      }     
1248    }
1249  }
1250
1251  if (Q) smt_free_queue(Q);
1252
1253  if (bflags) free(bflags);
1254
1255  return bvarArr;
1256}
1257
1258void
1259smt_combine_root_fml_with_flet_fml(void)
1260{
1261  smtFml_t * subfml, * fvar_fml, * fml, * iff_fml;
1262  smtFlet_t * flet;
1263  satArray_t * subfmlArr;
1264  int i;
1265
1266  subfmlArr = sat_array_alloc(gvar->fletArr->size * 2);
1267
1268  if (gvar->fml->type == AND_c) {
1269    for(i = 0; i < gvar->fml->subfmlArr->size; i++) {
1270      subfml = (smtFml_t *) gvar->fml->subfmlArr->space[i];
1271      subfmlArr = sat_array_insert(subfmlArr, (long) subfml);
1272    }
1273  } else { 
1274    subfmlArr = sat_array_insert(subfmlArr, (long) gvar->fml);
1275  }
1276   
1277  for(i = 0; i < gvar->fletArr->size; i++) {
1278    flet = (smtFlet_t *) gvar->fletArr->space[i];
1279    fvar_fml = flet->fvar_fml;
1280    fml = flet->fml;
1281
1282    /* iff_fml = (fvar_fml <-> fml) */
1283    gvar->tfmlArr->size = 0;
1284    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fvar_fml);
1285    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fml);   
1286    iff_fml = smt_create_formula(IFF_c, gvar->tfmlArr); 
1287    subfmlArr = sat_array_insert(subfmlArr, (long) iff_fml);
1288    gvar->fmlArr = sat_array_insert(gvar->fmlArr, (long) iff_fml);   
1289  }
1290
1291  if (gvar->fml->type == AND_c) {
1292    free(gvar->fml->subfmlArr);
1293    gvar->fml->subfmlArr = subfmlArr;
1294  } else {
1295    gvar->fml = smt_create_formula(AND_c, subfmlArr);
1296  }
1297}
1298
1299#endif
Note: See TracBrowser for help on using the repository browser.