source: vis_dev/cusp-1.1/src/smt/smtPre.c

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

cusp added

File size: 5.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [smtPre.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 "util.h"
48#include "smt.h"
49
50void
51smt_preprocess(smtManager_t * sm)
52{
53  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) 
54    smt_dl_preprocess(sm);
55  else
56    exit(0); 
57}
58
59void
60smt_update_nvar_adjacent_avar_array(smtManager_t * sm)
61{
62  /* this is included in smt_create_atom_variable_main */
63
64  smtAvar_t * avar;
65  smtNvar_t * nvar;
66  int size, prev_num, cur_num;
67  int i, j;
68
69  if (sm->avarArr->size == 0) return;
70
71  for(i = 0, prev_num = 0; i < sm->nvarArr->size; i++) {
72    nvar = (smtNvar_t *) sm->nvarArr->space[i];
73    if (nvar->avarArr) {
74      prev_num += nvar->avarArr->size;
75      nvar->avarArr->size = 0;
76    }
77  }
78
79  size = 3 * (sm->avarArr->size / sm->nvarArr->size + 1);
80
81  for(i = 0, cur_num = 0; i < sm->avarArr->size; i++) {
82    avar = (smtAvar_t *) sm->avarArr->space[i];
83
84    for(j = 0; j < avar->nvars->size; j++) {
85      nvar = (smtNvar_t *) avar->nvars->space[j];
86      if (!nvar->avarArr) nvar->avarArr = sat_array_alloc(size);
87      if ( sm->avalues[avar->id] == 2 ) {
88        cur_num++;
89        nvar->avarArr = sat_array_insert(nvar->avarArr, (long) avar);
90      }
91    }
92  }
93
94  return;
95}
96
97void
98smt_dl_preprocess(smtManager_t * sm)
99{
100  smt_convert_atom_to_dl_form(sm); 
101
102  smt_generate_avar_sister_array(sm);
103}
104
105void
106smt_convert_atom_to_dl_form(smtManager_t * sm)
107{
108  smtAvar_t * avar;
109  smtNvar_t * nvar_a, * nvar_b;
110  double coeff_a, coeff_b;
111  int i;
112
113  for(i = 0; i < sm->avarArr->size; i++) {
114    avar = (smtAvar_t *) sm->avarArr->space[i];
115    coeff_a = array_fetch(double, avar->coeffs, 0);
116    coeff_b = array_fetch(double, avar->coeffs, 1);
117
118    if (avar->type == GE_c) {
119      avar->constant = -avar->constant;
120      coeff_a = -coeff_a;
121      coeff_b = -coeff_b;     
122    } else if (avar->type == LT_c) {
123      avar->constant = avar->constant - sm->epsilon;     
124    } else if (avar->type == GT_c) {
125      avar->constant = -avar->constant - sm->epsilon;
126      coeff_a = -coeff_a;
127      coeff_b = -coeff_b;
128    }
129
130    if (coeff_a > 0) {
131      assert(coeff_a == 1 && coeff_b == -1);   
132      /* no change */
133    } else {
134      assert(coeff_b == 1 && coeff_a == -1);   
135      array_insert(double, avar->coeffs, 0, 1);
136      array_insert(double, avar->coeffs, 1, -1);
137      nvar_a = (smtNvar_t *) avar->nvars->space[0];
138      nvar_b = (smtNvar_t *) avar->nvars->space[1];
139      /* swap */
140      avar->nvars->space[0] = (long) nvar_b;
141      avar->nvars->space[1] = (long) nvar_a;
142    }
143  }
144
145  return;
146}
147
148void
149smt_generate_avar_sister_array(smtManager_t * sm)
150{
151  smtAvar_t * avar;
152  smtNvar_t * lnvar, * rnvar, * tnvar;
153  array_t * sis_avars;
154  st_table * sis_table = st_init_table(strcmp, st_strhash);
155  char * key;
156  int i;
157
158  sm->sis_table = sis_table;
159
160  for(i = 0; i < sm->avarArr->size; i++) {
161    avar = (smtAvar_t *) sm->avarArr->space[i];
162    lnvar = (smtNvar_t *) avar->nvars->space[0];
163    rnvar = (smtNvar_t *) avar->nvars->space[1];
164
165    if (lnvar->id > rnvar->id) {
166      tnvar = lnvar;
167      lnvar = rnvar;
168      rnvar = tnvar;
169    }
170
171    key = util_strcat3(lnvar->name, rnvar->name, "");
172
173    if (st_lookup(sis_table, key, (char **)&(sis_avars))) {
174      array_insert_last(smtAvar_t *, sis_avars, avar);
175      avar->sis_avars = sis_avars;
176      free(key);
177    } else {
178      sis_avars = array_alloc(smtAvar_t *, 10);
179      array_insert_last(smtAvar_t *, sis_avars, avar); 
180      st_insert(sis_table, key, (char *) sis_avars);
181      avar->sis_avars = sis_avars;
182    }
183  }
184
185  return;
186}
187
188void
189smt_put_la_clause_to_clause_arr(smtManager_t * sm)
190{
191  smtCls_t * cls;
192  int i;
193
194  if (sm->la_clsArr == 0) return;
195
196  for(i = 0; i < sm->la_clsArr->size; i++) {
197    cls = (smtCls_t *) sm->la_clsArr->space[i];
198    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
199  }
200
201  return;
202}
203
204#endif
Note: See TracBrowser for help on using the repository browser.