source: vis_dev/cusp-1.1/src/smt/smtUtil.c @ 74

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

cusp added

File size: 21.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [smtUtil.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
49static jmp_buf timeout_env;
50static int cusp_timeout;       
51static long alarm_lap_time;
52
53smtCls_t *
54smt_create_clause(void)
55{
56  smtCls_t * cls = (smtCls_t *) malloc(sizeof(smtCls_t));
57
58  cls->litArr = sat_array_alloc(8);
59
60  return cls;
61}
62
63smtCls_t *
64smt_duplicate_clause(smtCls_t * cls)
65{
66  smtCls_t * new_cls;
67  int i, lit;
68
69  new_cls = smt_create_clause();
70 
71  for(i = 0; i < cls->litArr->size; i++) {
72    lit = cls->litArr->space[i];
73    new_cls->litArr = sat_array_insert(new_cls->litArr, (long) lit);
74  }
75
76  return new_cls;
77}
78
79smtFmlType_t
80smt_get_ar_symbol(char * str)
81{
82  smtFmlType_t type;
83
84  if ( ! strcmp(str, "=") )
85    type = EQ_c;
86  else if ( ! strcmp(str, "<") )
87    type = LT_c;
88  else if ( ! strcmp(str, ">") )
89    type = GT_c;
90  else if ( ! strcmp(str, "<=") )
91    type = LE_c;
92  else if ( ! strcmp(str, ">=") )
93    type = GE_c;
94  else if ( ! strcmp(str, "+") )
95    type = ADD_c;
96  else if ( ! strcmp(str, "-") )
97    type = SUB_c;
98  else if ( ! strcmp(str, "*") )
99    type = MUL_c;
100  else if ( ! strcmp(str, "~") )
101    type = MINUS_c;
102  else if ( ! strcmp(str, "/") )
103    type = DIV_c;
104  else {
105#ifndef DISABLE_STATISTICS
106    fprintf(stdout, "ERROR: Wrong type: %s\n", str);
107#endif
108    fprintf(stdout, "unknown\n");
109    exit(0);
110  }
111
112  return type;
113}
114
115smtBvar_t *
116smt_create_bool_variable(char * name, smtFml_t * bvfml)
117{
118  smtBvar_t * bvar = (smtBvar_t *) malloc(sizeof(smtBvar_t));
119
120  if (name) 
121    bvar->name = name;
122  else
123    bvar->name = 0;
124
125  if (bvfml) {
126    if (!bvar->name)
127      bvar->name = smt_convert_fml_to_string(bvfml);
128
129    bvfml->bvar = bvar;
130  }
131 
132  bvar->id = 0;
133  bvar->flag = 0;
134  bvar->aig_node = 0;
135
136  return bvar;
137}
138
139smtBvar_t *
140smt_create_intermediate_bool_variable(smtManager_t * sm, AigEdge_t node)
141{
142  Aig_Manager_t * bm = sm->bm;
143  smtBvar_t * bvar;
144  nameType_t * node_name;
145  int var_id;
146
147  sm->num_var++;
148  var_id = sm->num_var; 
149
150  /* bool var */
151  node_name = Aig_NodeReadName(bm, node);
152  bvar = smt_create_bool_variable(0,0);
153  bvar->name = util_strcat3("AIG_", node_name, "");
154  bvar->id = var_id;
155  sm->bvarArr = sat_array_insert(sm->bvarArr, (long) bvar);
156  sm->id2var = sat_array_insert(sm->id2var, (long) bvar);
157  assert(bvar->id == sm->id2var->size-1);
158
159  return bvar;
160}
161
162smtNvar_t *
163smt_create_numerical_variable(char * name, smtFml_t * nvfml)
164{
165  smtNvar_t * nvar = (smtNvar_t *) malloc(sizeof(smtNvar_t));
166
167  if (name) 
168    nvar->name = name;
169  else
170    nvar->name = 0;
171
172  if (nvfml) {
173    if (!nvar->name)
174      nvar->name = smt_convert_fml_to_string(nvfml);
175
176    nvfml->nvar = nvar;
177  }
178   
179  nvar->id = 0;
180  nvar->flag = 0;
181  nvar->avarArr = 0;
182
183  return nvar;
184}
185
186void
187smt_create_dl_atom_variable_main(smtManager_t * sm)
188{
189  smtFml_t * avfml;
190  smtAvar_t * avar, * tavar;
191  smtNvar_t * nvar, * lnvar, * rnvar;
192  st_table * avar_table;
193  int id = 1, size = 0;
194  int i, j;
195 
196  sm->avarArr = sat_array_alloc(sm->avfmlArr->size);
197  sm->id2var = sat_array_alloc(sm->avarArr->size + sm->bvarArr->size + 1);
198  sm->id2var = sat_array_insert(sm->id2var, 0); /* elem starts from idx one */
199
200  if (sm->nvarArr->size) 
201    size = 3 * (sm->avfmlArr->size / sm->nvarArr->size + 1);
202 
203  avar_table = st_init_table(strcmp, st_strhash);
204 
205  for(i = 0; i < sm->avfmlArr->size; i++) {
206    avfml = (smtFml_t *) sm->avfmlArr->space[i];
207    avar = smt_create_atom_variable(avfml);
208
209    if ( !(sm->flag & MP_CONST_MASK) ) {
210      lnvar = (smtNvar_t *) avar->nvars->space[0];
211      rnvar = (smtNvar_t *) avar->nvars->space[1];
212     
213      if (lnvar == rnvar) { /* bool */
214        smt_convert_dl_atom_fml_to_bool_fml(avfml, avar);
215        smt_free_atom_members(avar);
216        free(avar);
217        continue;
218      }
219    }
220
221    if (st_lookup(avar_table, avar->name, (char **)&(tavar))) { 
222      avfml->avar = tavar;
223      smt_free_atom_members(avar);
224      free(avar);
225    } else {
226      avfml->avar = avar;
227      avar->id = id;
228      id++;
229      sm->avarArr = sat_array_insert(sm->avarArr, (long) avar);
230      st_insert(avar_table, avar->name, (char *) avar); 
231      sm->id2var = sat_array_insert(sm->id2var, (long) avar);
232
233      /* generate adjacent avar array */
234      for(j = 0; j < avar->nvars->size; j++) {
235        nvar = (smtNvar_t *) avar->nvars->space[j];
236        if (!nvar->avarArr) nvar->avarArr = sat_array_alloc(size);
237        nvar->avarArr = sat_array_insert(nvar->avarArr, (long) avar);
238      }
239
240      if (avar->type == EQ_c) {
241        if (avar->constant >= 0.0 && avar->constant <= 0.0) 
242          sm->stats->num_eq++;
243        else
244          sm->stats->num_ceq++;
245      } else {
246        sm->stats->num_ineq++;
247      }
248    }
249  }
250
251  st_free_table(avar_table);
252}
253
254void
255smt_convert_dl_atom_fml_to_bool_fml(smtFml_t * fml, smtAvar_t * avar)
256{
257  /* atoms are in the form of x - x <= w */
258
259  fml->type = PRED_c;
260
261  if (avar->type == LE_c) {
262    if (avar->constant >= 0)
263      fml->flag |= TRUE_MASK;
264    else 
265      fml->flag |= FALSE_MASK;
266  } else if (avar->type == LT_c) {
267    if (avar->constant > 0)
268      fml->flag |= TRUE_MASK;
269    else 
270      fml->flag |= FALSE_MASK;
271  } else if (avar->type == GE_c) {
272    if (avar->constant <= 0)
273      fml->flag |= TRUE_MASK;
274    else 
275      fml->flag |= FALSE_MASK;
276  } else if (avar->type == GT_c) {
277    if (avar->constant < 0)
278      fml->flag |= TRUE_MASK;
279    else 
280      fml->flag |= FALSE_MASK;
281  }
282   
283  return;
284}
285
286int
287smt_convert_atom_to_leq_form(smtManager_t * sm, smtAvar_t * avar)
288{
289  smtNvar_t * nvar_a, * nvar_b;
290  double * coeffs;
291  double coeff, coeff_a, coeff_b;
292  int j, k;
293 
294  /* atom is converted into (nvars <= constant) form */
295
296  coeffs = (double *) malloc(sizeof(double) * (sm->nvarArr->size + 1));
297  memset(coeffs, 0, sizeof(double) * (sm->nvarArr->size + 1));
298   
299  /* check redundant nvar in avar */
300  for(j = 0; j < avar->nvars->size-1; j++) {
301    nvar_a = (smtNvar_t *) avar->nvars->space[j];
302   
303    for(k = j+1; k < avar->nvars->size; k++) {
304      nvar_b = (smtNvar_t *) avar->nvars->space[k];
305      if (nvar_a != nvar_b) continue;
306      coeff_a = array_fetch(double, avar->coeffs, j);
307      coeff_b = array_fetch(double, avar->coeffs, k);
308      coeff_a = coeff_a + coeff_b;
309      array_insert(double, avar->coeffs, j, coeff_a);
310      array_insert(double, avar->coeffs, k, 0);
311    }
312  }
313
314  for(j = 0, k = 0; j < avar->coeffs->num; j++) {
315    coeff = array_fetch(double, avar->coeffs, j);
316    nvar_a = (smtNvar_t *) avar->nvars->space[j];
317   
318    if (coeff <= 0 && coeff >= 0) { /* redundant nvar exists */
319      continue;
320    }
321   
322    if (avar->type == GE_c || avar->type == GT_c) {
323      coeff = -coeff;
324      array_insert(double, avar->coeffs, k, coeff);
325    } else {
326      array_insert(double, avar->coeffs, k, coeff);
327    }
328
329    coeffs[nvar_a->id] = coeff;
330
331    if (j != k) { /* redundant nvar exists */
332      avar->nvars->space[k] = (long) nvar_a;
333    }
334   
335    k++;
336  }
337 
338  if (j != k) { /* redundant nvar exists */
339    avar->coeffs->num = k;
340    avar->nvars->size = k;
341  }
342 
343  if (avar->type == GE_c) 
344    avar->constant = -avar->constant;
345  else if (avar->type == LT_c) 
346    avar->constant = avar->constant - sm->epsilon;     
347  else if (avar->type == GT_c) 
348    avar->constant = -avar->constant - sm->epsilon;
349 
350  if (k == 0) { /* avar -> bool */
351    if (avar->constant >= 0) 
352      return 1; /* true */
353    else
354      return 0; /* false */
355  }
356
357  if (k > 1) { /* sort nvar in avar->nvars for upcoming tableau gen */
358    smt_sort_nvar_array_with_id(avar->nvars);
359    for(j = 0; j < avar->coeffs->num; j++) {
360      nvar_a = (smtNvar_t *) avar->nvars->space[j];
361      coeff = coeffs[nvar_a->id];
362      array_insert(double, avar->coeffs, j, coeff);
363    }
364  }
365
366  return 2;
367}
368
369char *
370smt_get_avar_name(smtManager_t * sm, smtAvar_t * avar)
371{
372  smtNvar_t * nvar, * lnvar, * rnvar;
373  double coeff;
374  char * str_a, * str_b, * str_c, * str_d, * avar_name;
375  int i;
376
377  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
378    for(i = 0, lnvar = 0, rnvar = 0; i < avar->nvars->size; i++) {
379      coeff = array_fetch(double, avar->coeffs, i);
380      nvar = (smtNvar_t *) avar->nvars->space[i];
381      if (coeff > 0) lnvar = nvar;
382      else if (coeff < 0) rnvar = nvar;
383      else exit(0);
384    }
385
386    assert(lnvar);
387    assert(rnvar);
388
389    str_a = (char *) malloc(sizeof(char) * 10);
390    str_b = (char *) malloc(sizeof(char) * 10);
391    str_c = (char *) malloc(sizeof(char) * 10);
392    str_d = (char *) malloc(sizeof(char) * 10);
393
394    sprintf(str_a, "%p", lnvar);
395    sprintf(str_b, "%p", rnvar);
396    sprintf(str_c, "%d", (int) avar->type);
397    str_d = util_strcat3(str_a, str_b, str_c);
398    sprintf(str_c, "%g", avar->constant);
399    avar_name = util_strcat3(str_d, str_c, "");
400    free(str_a);
401    free(str_b);
402    free(str_c);
403    free(str_d);
404
405  } else if (sm->flag & LIA_MASK) {
406    /* later */
407    avar_name = avar->name;
408  } else
409    avar_name = 0;
410
411  return avar_name;
412}
413
414char *
415smt_get_neg_avar_name(smtManager_t * sm, smtAvar_t * avar)
416{
417  smtNvar_t * nvar, * lnvar, * rnvar;
418  double coeff;
419  char * str_a, * str_b, * str_c, * str_d, * avar_name = 0;
420  int i;
421
422  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
423    for(i = 0, lnvar = 0, rnvar = 0; i < avar->nvars->size; i++) {
424      coeff = array_fetch(double, avar->coeffs, i);
425      nvar = (smtNvar_t *) avar->nvars->space[i];
426      if (coeff > 0) lnvar = nvar;
427      else if (coeff < 0) rnvar = nvar;
428      else exit(0);
429    }
430
431    assert(lnvar);
432    assert(rnvar);
433
434    str_a = (char *) malloc(sizeof(char) * 10);
435    str_b = (char *) malloc(sizeof(char) * 10);
436    str_c = (char *) malloc(sizeof(char) * 10);
437    str_d = (char *) malloc(sizeof(char) * 10);
438   
439    sprintf(str_a, "%p", lnvar);
440    sprintf(str_b, "%p", rnvar);
441
442    if (avar->type == LE_c) 
443      sprintf(str_c, "%d", GT_c);
444    else if (avar->type == LT_c) 
445      sprintf(str_c, "%d", GE_c);
446    else if (avar->type == GE_c) 
447      sprintf(str_c, "%d", LT_c);
448    else if (avar->type == GT_c) 
449      sprintf(str_c, "%d", LE_c);
450
451    str_d = util_strcat3(str_a, str_b, str_c);
452    sprintf(str_c, "%d", (int) avar->constant);
453    avar_name = util_strcat3(str_d, str_c, "");
454    free(str_a);
455    free(str_b);
456    free(str_c);
457    free(str_d);
458
459  } else if (sm->flag & LIA_MASK) {
460    /* later */
461    avar_name = avar->name;
462  }
463
464  return avar_name;
465}
466
467smtAvar_t *
468smt_create_atom_variable(smtFml_t * avfml)
469{
470  smtAvar_t * avar = (smtAvar_t *) malloc(sizeof(smtAvar_t));
471
472  avar->name = smt_convert_fml_to_string(avfml);
473  avar->id = 0;
474  avar->flag = 0;
475  avar->type = avfml->type;
476  avar->nvars = sat_array_alloc(4);
477  avar->coeffs = array_alloc(double, 4);
478  avar->sis_avars = 0;
479  avar->constant = 0;
480
481  smt_gather_atom_member(avar, avfml);
482
483  if (avar->nvars->size == 1)
484    avar->flag |= BOUND_MASK;
485  else if ( !(avar->flag & LA_MASK) )
486    avar->flag |= UNIT_LA_MASK;
487   
488  avar->aig_node = Aig_NULL;
489 
490  return avar; 
491}
492
493smtAvar_t *
494smt_create_pure_atom_variable(void)
495{
496  smtAvar_t * avar = (smtAvar_t *) malloc(sizeof(smtAvar_t));
497
498  avar->name = 0;
499  avar->id = 0;
500  avar->flag = 0;
501  avar->coeffs = array_alloc(double, 4);
502  avar->nvars = sat_array_alloc(4);
503  avar->constant = 0;
504  avar->aig_node = Aig_NULL;
505 
506  return avar; 
507}
508
509void
510smt_init_atom_variable_values(smtManager_t * sm)
511{
512  int i, size;
513
514  if (!sm->avarArr) return;
515
516  size = sm->avarArr->size + 1;
517
518  sm->avalues = (int *) malloc(sizeof(int) * size);
519
520  for(i = 0; i < size; i++) {
521    sm->avalues[i] = 2;
522  }
523}
524
525void
526smt_assign_boolean_variable_id(smtManager_t * sm)
527{
528  smtBvar_t * bvar;
529  int id;
530  int i;
531 
532  if (sm->avarArr)
533    id = sm->avarArr->size + 1;
534  else
535    id = 1;
536
537  for(i = 0; i < sm->bvarArr->size; i++) {
538    bvar = (smtBvar_t *) sm->bvarArr->space[i];
539    bvar->id = id;
540    id++;
541    sm->id2var = sat_array_insert(sm->id2var, (long) bvar);
542  } 
543}
544
545void
546smt_assign_numerical_variable_id(smtManager_t * sm)
547{
548  smtNvar_t * nvar;
549  int i;
550 
551  for(i = 0; i < sm->nvarArr->size; i++) {
552    nvar = (smtNvar_t *) sm->nvarArr->space[i];
553    nvar->id = i + 1;
554  } 
555}
556
557void
558smt_assign_numerical_variable_id_in_array(satArray_t * nvarArr)
559{
560  smtNvar_t * nvar;
561  int i;
562 
563  for(i = 0; i < nvarArr->size; i++) {
564    nvar = (smtNvar_t *) nvarArr->space[i];
565    nvar->id = i + 1;
566  } 
567}
568
569void
570smt_gather_atom_member(smtAvar_t * avar, smtFml_t * avfml)
571{
572  smtFml_t * lfml, * rfml;
573  double coeff;
574  int nminus;
575
576  lfml = (smtFml_t *) avfml->subfmlArr->space[0];
577  rfml = (smtFml_t *) avfml->subfmlArr->space[1];
578
579  nminus = 0;
580  coeff = 1;
581
582  smt_gather_atom_member_in_fml(avar, lfml, nminus, coeff);
583 
584  nminus = 1;
585  coeff = 1;
586
587  smt_gather_atom_member_in_fml(avar, rfml, nminus, coeff);
588}
589
590void
591smt_gather_atom_member_in_fml(
592  smtAvar_t * avar,
593  smtFml_t * fml,
594  int nminus,
595  double coeff)
596{
597  smtFml_t * lfml, * rfml, * tfml;
598  char * str_a, * str_b;
599  double value = 0, tcoeff = 0;
600  int i;
601
602  if (fml->type == FUN_c) {
603    if (nminus%2 == 1)
604      tcoeff = -coeff; 
605    else if (nminus%2 == 0)
606      tcoeff = coeff;
607
608    array_insert_last(double, avar->coeffs, tcoeff);
609    avar->nvars = sat_array_insert(avar->nvars, (long) fml->nvar);
610    if (tcoeff > 1 || tcoeff < -1) 
611      avar->flag |= LA_MASK;
612   
613  } else if (fml->type == NUM_c) {
614    if(nminus%2 == 1)
615      value = coeff * (double) fml->value;
616    else
617      value = -coeff * (double) fml->value;
618   
619    (avar->constant)+=(double) value;
620   
621  } else if (fml->type == MINUS_c) {
622    nminus++;
623    tfml = (smtFml_t *) fml->subfmlArr->space[0];
624    smt_gather_atom_member_in_fml(avar, tfml, nminus, coeff);
625   
626  } else if (fml->type == SUB_c) {
627    lfml = (smtFml_t *) fml->subfmlArr->space[0];
628    rfml = (smtFml_t *) fml->subfmlArr->space[1];
629   
630    smt_gather_atom_member_in_fml(avar, lfml, nminus, coeff);
631    smt_gather_atom_member_in_fml(avar, rfml, nminus + 1, coeff);
632
633  } else if (fml->type == ADD_c) {
634    for(i = 0; i < fml->subfmlArr->size; i++) {
635      tfml = (smtFml_t *) fml->subfmlArr->space[i];
636      smt_gather_atom_member_in_fml(avar, tfml, nminus, coeff);
637    }
638   
639  } else if (fml->type == MUL_c) {
640    lfml = (smtFml_t *) fml->subfmlArr->space[0];
641    rfml = (smtFml_t *) fml->subfmlArr->space[1];
642
643    if (lfml->type == NUM_c && rfml->type != NUM_c) {
644      /** ex: 3 * (a + b + 2) **/
645      tcoeff = coeff * (double) lfml->value;
646      smt_gather_atom_member_in_fml(avar, rfml, nminus, tcoeff);
647
648    } else if (lfml->type != NUM_c && rfml->type == NUM_c) {
649      /** ex: (a + b + 2) * 3 **/
650      tcoeff = coeff * (double) rfml->value;
651      smt_gather_atom_member_in_fml(avar, lfml, nminus, tcoeff);
652     
653    } else if (lfml->type == MINUS_c && rfml->type != NUM_c) {
654      /** ex: -3 * (a + b + 2) **/
655      nminus++;
656      tfml = (smtFml_t *) lfml->subfmlArr->space[0];
657      tcoeff = coeff * (double) tfml->value;
658      smt_gather_atom_member_in_fml(avar, rfml, nminus, tcoeff);
659
660    } else if (lfml->type != NUM_c && rfml->type == MINUS_c) {
661      /** ex: (a + b + 2) * -3 **/
662      nminus++;
663      tfml = (smtFml_t *) rfml->subfmlArr->space[0];
664      tcoeff = coeff * (double) tfml->value;
665      smt_gather_atom_member_in_fml(avar, lfml, nminus, tcoeff);
666     
667    } else if (lfml->type == NUM_c && rfml->type == NUM_c) {
668      /** ex: 2 * 3 **/
669      value = lfml->value * rfml->value;
670       
671      if(nminus%2 == 1)
672        value = coeff * value;
673      else
674        value = -coeff * value;
675     
676      (avar->constant)+= value;
677     
678    } else if (lfml->type == FUN_c && rfml->type == FUN_c) {
679      fprintf(stdout, "%s * %s: WRONG LINEAR ARITHMETIC ATOM TYPE\n", 
680              lfml->nvar->name, rfml->nvar->name);
681      fprintf(stdout, "unknown\n");
682      exit(0);
683    } else { 
684      fprintf(stdout, "ERROR: WRONG LINEAR ARITHMETIC ATOM TYPE\n");
685      str_a = smt_convert_fml_to_string(lfml);
686      str_b = smt_convert_fml_to_string(rfml);
687      fprintf(stdout, "fml = %s * %s\n", str_a, str_b);
688      fprintf(stdout, "unknown\n");
689      exit(0);
690    }
691
692  } else if (fml->type == DIV_c) {
693    lfml = (smtFml_t *) fml->subfmlArr->space[0];
694    rfml = (smtFml_t *) fml->subfmlArr->space[1];
695   
696    if (lfml->type == NUM_c && rfml->type == NUM_c) {
697      if (rfml->value != 0)
698        value = lfml->value / rfml->value;
699     
700      if(nminus%2 == 1)
701        value = coeff * value;
702      else
703        value = -coeff * value;
704     
705      (avar->constant)+= value;     
706     
707    } else { 
708      fprintf(stdout, "ERROR: WRONG LINEAR ARITHMETIC ATOM TYPE\n");
709      str_a = smt_convert_fml_to_string(lfml);
710      str_b = smt_convert_fml_to_string(rfml);
711      fprintf(stdout, "fml = %s * %s\n", str_a, str_b);
712      fprintf(stdout, "unknown\n");
713      exit(0);
714    }
715   
716  } else {
717    fprintf(stdout, "ERROR: WRONG LINEAR ARITHMETIC ATOM TYPE\n");
718    fprintf(stdout, "unknown\n");
719    exit(0);
720  }
721
722  return;
723}
724
725void
726smt_assign_bool_var_flag(smtManager_t * sm)
727{
728  satManager_t * cm = sm->cm;
729  smtNvar_t * bvar;
730  int i;
731
732  for(i = 0; i < sm->bvarArr->size; i++) {
733    bvar = (smtNvar_t *) sm->bvarArr->space[i];
734    cm->bvars[bvar->id] = 1;
735  }
736}
737
738void
739smt_sort_nvar_array_with_id(satArray_t * arr)
740{
741  /* decreasing */
742  smt_sort_nvar_array_with_id_aux(&(arr->space[0]), arr->size);
743}
744
745void
746smt_sort_nvar_array_with_id_aux(long * arr, long size)
747{
748  smtNvar_t * nvar_a, * nvar_b;
749  long i, j, tmp, bi;
750  long pivot;
751
752  if (size <= 15) { 
753    for(i = 0; i < size-1; i++) {
754      bi = i;
755      for(j = i+1; j < size; j++) {
756        nvar_a = (smtNvar_t *) arr[j];
757        nvar_b = (smtNvar_t *) arr[bi];
758        if (nvar_a->id < nvar_b->id)
759          bi = j;
760      }
761
762      tmp = arr[i];
763      arr[i] = arr[bi];
764      arr[bi] = tmp;
765    }
766  } else {
767    pivot = arr[size>>1];
768    i = -1;
769    j = size;
770
771    while(1) {
772      do {
773        i++; 
774        nvar_a = (smtNvar_t *) arr[i];
775        nvar_b = (smtNvar_t *) pivot;
776      } while(nvar_a->id > nvar_b->id);
777     
778      do {
779        j--;
780        nvar_a = (smtNvar_t *) arr[j];
781        nvar_b = (smtNvar_t *) pivot;
782      } while(nvar_b->id > nvar_a->id);
783
784      if(i>=j)  break;
785      tmp = arr[i];
786      arr[i] = arr[j];
787      arr[j] = tmp;
788    }
789    smt_sort_nvar_array_with_id_aux(arr, i);
790    smt_sort_nvar_array_with_id_aux(&(arr[i]), size-i);
791  }
792}
793
794smtQueue_t *
795smt_create_queue(long MaxElements)
796{
797smtQueue_t *Q;
798
799  Q = (smtQueue_t *) malloc(sizeof(smtQueue_t));
800  if(Q == NULL)
801    fprintf(stderr, "Out of space!!!\n" );
802
803  Q->array = (long *) malloc(sizeof(long)*MaxElements);
804  if(Q->array == NULL)
805    fprintf(stderr, "Out of space!!!\n" );
806  Q->max = MaxElements;
807  Q->size = 0;
808  Q->front = 1;
809  Q->rear = 0;
810  return Q;
811}
812
813void
814smt_init_queue(smtQueue_t * Q)
815{
816  Q->size = 0;
817  Q->front = 1;
818  Q->rear = 0;
819  return;
820}
821
822void
823smt_free_queue(smtQueue_t * Q)
824{
825  if( Q != NULL ) {
826    free(Q->array);
827    free(Q);
828  }
829}
830
831void
832smt_enqueue(
833  smtQueue_t * Q,
834  long v)
835{
836long *arr, *oarr;
837long rear;
838
839  if(Q->size < Q->max) {
840    Q->size++;
841    rear = Q->rear;
842    rear = (++(rear) == Q->max) ? 0 : rear;
843    Q->array[rear] = v;
844    Q->rear = rear;
845  }
846  else {
847    arr = (long *) malloc(sizeof(long)*Q->size*2);
848    if(arr == NULL )
849      fprintf(stderr, "Out of space!!!\n" );
850    oarr = Q->array;
851    if(Q->front > Q->rear) {
852      memcpy(&(arr[1]), &(oarr[Q->front]), 
853             sizeof(long) *(Q->max-Q->front));
854      memcpy(&(arr[Q->size-Q->front+1]), &(oarr[0]), 
855             sizeof(long) *(Q->rear+1));
856    }
857    else if(Q->front < Q->rear) {
858      memcpy(&(arr[1]), &(oarr[Q->front]), sizeof(long) *(Q->size));
859    }
860    free(oarr);
861    Q->array = arr;
862    Q->front = 1;
863    Q->rear = Q->size;
864    Q->max *= 2;
865   
866    Q->size++;
867    rear = Q->rear;
868    rear = (++(rear) == Q->max) ? 0 : rear;
869    Q->array[rear] = v;
870    Q->rear = rear;
871  }
872}
873
874long
875smt_dequeue(smtQueue_t * Q)
876{
877long front;
878long v;
879
880  if(Q->size > 0) {
881    Q->size--;
882    front = Q->front;
883    v = Q->array[front];
884    Q->front = (++(front) == Q->max) ? 0 : front;
885    return v;
886  }
887  else
888    return(0);
889}
890
891int
892smt_timeout(int timeout)
893{
894  if (timeout > 0) {
895    cusp_timeout = timeout;
896    (void) signal(SIGALRM, 
897                  (void(*)(int))smt_timeout_handle);
898    (void) alarm(cusp_timeout);
899    if (setjmp(timeout_env) > 0) {
900      (void) fprintf(stdout, "cusp : timeout occurred after %d seconds.\n", 
901                     cusp_timeout);     
902      alarm(0);
903    }
904  }
905
906  return 0;
907}
908
909void
910smt_timeout_handle(void)
911{
912  int seconds = (int) ((util_cpu_ctime() - alarm_lap_time) / 1000);
913
914  if (seconds < cusp_timeout) {
915    unsigned slack = (unsigned) (cusp_timeout - seconds);
916    (void) signal(SIGALRM, (void(*)(int)) smt_timeout_handle);
917    (void) alarm(slack);
918  } else {
919    longjmp(timeout_env, 1);
920  }
921}
922
923void
924smt_none(void)
925{
926  return;
927}
928
929#endif
Note: See TracBrowser for help on using the repository browser.