source: vis_dev/cusp-1.1/src/smt/smtDl.c @ 40

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

cusp added

File size: 38.7 KB
RevLine 
[12]1/**CFile***********************************************************************
2
3  FileName    [smtDl.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
49int
50smt_idl_theory_solve(smtManager_t * sm)
51{
52  smt_bellman_ford_main(sm);
53
54  if (!(sm->flag & SAT_MASK)) { 
55
56    return 2; /* theory unsat */
57
58  } else if (sm->litArr->size < sm->avarArr->size) {
59
60    smt_dl_theory_propagation_main(sm); /* theory sat */
61
62  }
63
64  if (sm->litArr->size == sm->avarArr->size) {
65
66    smt_check_solution(sm);
67   
68  }
69 
70  if (sm->tplits->size) { 
71
72    return 1; /* theory prop exists */
73
74  }
75
76  return 0; /* sat without theory prop */
77}
78
79int
80smt_rdl_theory_solve(smtManager_t * sm)
81{
82  smt_bellman_ford_main(sm);
83
84  if (!(sm->flag & SAT_MASK)) { 
85
86    return 2; /* theory unsat */
87
88  } else if (sm->litArr->size < sm->avarArr->size) {
89
90    smt_dl_theory_propagation_main(sm); /* theory sat */
91
92  } 
93
94  if (sm->litArr->size == sm->avarArr->size) {
95
96    smt_check_solution(sm);
97   
98  }
99 
100  if (sm->tplits->size) { 
101
102    return 1; /* theory prop exists */
103
104  }
105
106  return 0; /* sat without theory prop */
107}
108
109void
110smt_bellman_ford_main(smtManager_t * sm)
111{
112  sm->stats->num_bf_call++;
113
114  smt_generate_constraint_graph(sm);
115
116  smt_bellman_ford_algorithm(sm);
117}
118
119void
120smt_dl_theory_propagation_main(smtManager_t * sm)
121{
122  smt_dl_simple_theory_propagation(sm);
123
124  if ((int) sm->stats->num_bf_call%300 == 0) {
125   
126    smt_init_dl_theory_propagation(sm->cG);
127   
128    if (sm->flag & IDL_MASK)
129      smt_idl_theory_propagation(sm); 
130    else if (sm->flag & RDL_MASK)
131      smt_rdl_theory_propagation(sm); 
132  }
133}
134
135void
136smt_generate_constraint_graph(smtManager_t * sm)
137{
138  smtGraph_t * G;
139  smtVertex_t * src, * dest;
140  smtEdge_t * e;
141  smtAvar_t * avar;
142  smtNvar_t * lnvar, *rnvar;
143  satArray_t *cur_edges; 
144  double weight;
145  int cur_index, lit, id;
146  int vindex, eindex;
147  int i;
148
149  if (sm->cG == 0) smt_init_constraint_graph(sm);   
150
151  G = sm->cG;
152  eindex = G->esize;
153  cur_edges = G->cur_edges;
154  cur_edges->size = 0;
155
156  /* generate edges */
157  cur_index = sm->cur_index;
158
159  for(i = cur_index; i < sm->litArr->size; i++) {
160    lit = sm->litArr->space[i];
161    id = (lit>0) ? lit : -lit;
162    avar = (smtAvar_t *) sm->id2var->space[id];
163    /* filter theory propagated avar */
164    if (avar->flag & TPROP_MASK) continue;
165    assert(avar->type != EQ_c);
166     
167    if (sm->avalues[id] == 1) {
168      lnvar = (smtNvar_t *) avar->nvars->space[0];
169      rnvar = (smtNvar_t *) avar->nvars->space[1];
170      weight = avar->constant;
171    } else {
172      assert(sm->avalues[id] == 0);
173      lnvar = (smtNvar_t *) avar->nvars->space[1];
174      rnvar = (smtNvar_t *) avar->nvars->space[0];
175      weight = -avar->constant - sm->epsilon;
176    }
177
178    vindex = lnvar->id - 1;
179    dest = &(G->vHead[vindex]);
180    vindex = rnvar->id - 1;
181    src =  &(G->vHead[vindex]);
182
183    e = smt_find_edge(src, dest);
184
185    if (e) {
186      if (weight < e->weight) {
187        e->avar->flag |= IMPLIED_MASK;
188        e->implied = sat_array_insert(e->implied, (long) e->avar);
189        e->avar = avar;
190        e->weight = weight;
191        cur_edges = sat_array_insert(cur_edges, (long) e);
192
193      } else {
194        avar->flag |= IMPLIED_MASK;
195        e->implied = sat_array_insert(e->implied, (long) avar);
196      }
197    } else {
198      e = smt_add_edge(G, src, dest, avar, eindex++);
199      e->weight = weight;
200      cur_edges = sat_array_insert(cur_edges, (long) e);
201      G->esize++;
202    }
203  }
204
205  return;
206}
207
208void
209smt_init_constraint_graph(smtManager_t * sm)
210{
211  smtGraph_t * G = sm->cG;
212  int vindex, esize;
213  int i;
214
215  sm->cG = (smtGraph_t *) malloc(sizeof(smtGraph_t));
216  G = sm->cG;
217  memset(G, 0, sizeof(smtGraph_t));
218
219  /* init vertex structure */
220  G->vsize = sm->nvarArr->size;
221  G->vHead = (smtVertex_t *) malloc(sizeof(smtVertex_t) * G->vsize);
222  memset(G->vHead, 0, sizeof(smtVertex_t) * G->vsize);
223  G->nvarArr = sm->nvarArr;
224   
225  for(i = 0; i < G->nvarArr->size; i++) {
226    /*nvar = (smtNvar_t *) G->nvarArr->space[i];*/
227    vindex = i;
228    smt_add_vertex(G, vindex);
229  }
230
231  /* flag */
232  G->flags = (int *) malloc(sizeof(int) * G->vsize);
233  memset(G->flags, 0, sizeof(int) * (G->vsize));
234  /* epsilonless */
235  G->epsilonless = sm->epsilonless;
236  /* path */
237  G->paths = (smtVertex_t **) malloc(sizeof(smtVertex_t *) * G->vsize);
238  memset(G->paths, 0, sizeof(smtVertex_t *) * G->vsize);
239  G->bpaths = (smtVertex_t **) malloc(sizeof(smtVertex_t *) * G->vsize);
240  memset(G->bpaths, 0, sizeof(smtVertex_t *) * G->vsize);
241  G->fpaths = (smtVertex_t **) malloc(sizeof(smtVertex_t *) * G->vsize);
242  memset(G->fpaths, 0, sizeof(smtVertex_t *) * G->vsize);
243  /* dist */
244  smt_init_dists_in_constraint_graph(sm);
245  /* bvArr & fvArr */
246  G->bvArr = sat_array_alloc(G->vsize);
247  G->fvArr = sat_array_alloc(G->vsize);
248  /* queue */
249  G->queue = smt_create_queue(G->vsize);
250  /* init edge structure */
251  G->esize = 0;
252  esize = sm->avarArr->size * 2;
253  G->eHead = (smtEdge_t *) malloc(sizeof(smtEdge_t) * esize);
254  memset(G->eHead, 0, sizeof(smtEdge_t) * esize);
255  G->avarArr = sm->avarArr;
256  G->cur_edges = sat_array_alloc(esize);
257  G->neg_edges = sat_array_alloc(30);
258  G->imp_edges = sat_array_alloc(esize);
259 
260  return;
261}
262
263void
264smt_init_dists_in_constraint_graph(smtManager_t * sm)
265{
266  smtGraph_t * G = sm->cG;
267
268  if (sm->flag & IDL_MASK) {
269    G->idists = (int *) malloc(sizeof(int) * G->vsize);
270    memset(G->idists, 0, sizeof(int) * (G->vsize));
271
272    G->bidists = (int *) malloc(sizeof(int) * G->vsize);
273    G->fidists = (int *) malloc(sizeof(int) * G->vsize);
274    G->rdists = 0;
275    G->brdists = 0;
276    G->frdists = 0;
277  } else if (sm->flag & RDL_MASK) {
278    G->rdists = (double *) malloc(sizeof(double) * G->vsize);
279    memset(G->rdists, 0, sizeof(double) * G->vsize); 
280
281    G->brdists = (double *) malloc(sizeof(double) * G->vsize);
282    G->frdists = (double *) malloc(sizeof(double) * G->vsize);
283    G->idists = 0;
284    G->bidists = 0;
285    G->fidists = 0;
286  } else {
287    exit(0);
288  }
289
290  smt_init_theory_prop_dists(sm);
291}
292
293void
294smt_init_theory_prop_dists(smtManager_t * sm)
295{
296  smtGraph_t * G = sm->cG;
297  int i;
298
299  if (sm->flag & IDL_MASK) {
300    for(i = 0; i < G->vsize; i++) {
301      G->bidists[i] = INT_MAX;
302      G->fidists[i] = INT_MAX;
303    }
304  } else if (sm->flag & RDL_MASK) {
305    for(i = 0; i < G->vsize; i++) {
306      G->brdists[i] = HUGE_VAL;
307      G->frdists[i] = HUGE_VAL;
308    }
309  }
310
311  return;
312}
313
314void
315smt_free_constraint_graph(smtGraph_t * G)
316{
317  if (G->idists) free(G->idists);
318  if (G->rdists) free(G->rdists);
319  if (G->bidists) free(G->bidists);
320  if (G->fidists) free(G->fidists);
321  if (G->brdists) free(G->brdists);
322  if (G->frdists) free(G->frdists);
323
324  smt_free_queue(G->queue);
325  smt_free_vertex(G);
326  smt_free_edge_implied(G->imp_edges);
327 
328  free(G->eHead);
329  free(G->flags);
330  free(G->paths);
331  free(G->bpaths);
332  free(G->fpaths);
333  free(G->bvArr);
334  free(G->fvArr);
335  free(G->cur_edges);
336  free(G->neg_edges);
337
338  free(G);
339}
340
341void
342smt_free_vertex(smtGraph_t * G)
343{
344  smtVertex_t * v;
345  int i;
346 
347  for(i = 0; i < G->vsize; i++) {
348    v = &(G->vHead[i]);
349    free(v->ins);
350    free(v->outs);
351    free(v->targets);
352  }
353
354  free(G->vHead);
355
356  return;
357}
358
359void
360smt_free_edge_implied(satArray_t * edgeArr)
361{
362  smtEdge_t * e;
363  satArray_t * implied;
364  int i;
365 
366  for(i = 0; i < edgeArr->size; i++) {
367    e = (smtEdge_t *) edgeArr->space[i];
368    implied = e->implied;
369    free(implied);
370  }
371
372  free(edgeArr);
373
374  return;
375}
376
377void
378smt_bellman_ford_algorithm(smtManager_t * sm)     
379{
380  smtGraph_t * G = sm->cG;
381  smtVertex_t * v, * src = 0, * dest = 0, *parent = 0;
382  smtEdge_t * e;
383  smtQueue_t * Q;
384  double new_dist = 0, cur_dist = 0, weight = 0;
385  int i, qsize, cycleFound = 0;
386
387  smt_init_bellman_ford_algorithm(sm); 
388
389  Q = G->queue;
390
391  qsize = Q->size;
392
393  while( (v = (smtVertex_t *) smt_dequeue(Q)) ) {
394
395    G->flags[v->index] &= RESET_FRINGE_MASK;
396
397    if (G->flags[v->index] & VISITED_MASK)
398      continue;
399
400    for(i = 0; i < v->outs->size; i++) {
401      e = (smtEdge_t *) v->outs->space[i];
402      src = e->src;
403      dest = e->dest;
404      weight = e->weight;
405
406      if (sm->flag & IDL_MASK) { 
407        new_dist = (double) G->idists[src->index] + weight;
408        cur_dist = (double) G->idists[dest->index];
409      } else if (sm->flag & RDL_MASK) {
410#if 1   /*
411           for rounding error case
412           e.g. cur_dist = -5.0000010000000001
413                new_dist = -5.000001000000001
414        */
415        weight = weight + sm->epsilonless;
416#endif   
417        new_dist = G->rdists[src->index] + weight;
418        cur_dist = G->rdists[dest->index];
419      } else 
420        exit(0);
421
422      if (new_dist < cur_dist) {
423        /* check if src is in the subtree of dest.
424           if this is the case, the negative cycle is detected */
425        parent = G->paths[v->index];
426        while(1) {
427          if (parent == 0)
428            break;
429          else if(parent == dest) {
430            G->paths[dest->index] = v;
431            G->flags[dest->index] &= RESET_VISITED_MASK;
432            cycleFound = 1;
433            break;
434          }
435          parent = G->paths[parent->index];
436        }
437        if (cycleFound) break;
438
439        smt_delete_subtree(G, dest);
440
441        /* relaxation */
442        if (sm->flag & IDL_MASK) 
443          G->idists[dest->index] = (int) new_dist;
444        else if (sm->flag & RDL_MASK) {
445          new_dist = G->rdists[src->index] + e->weight;
446          G->rdists[dest->index] = new_dist;
447        }
448
449        G->paths[dest->index] = src;
450        G->flags[dest->index] &= RESET_VISITED_MASK;
451       
452        if (!(G->flags[dest->index] & FRINGE_MASK)) {
453          G->flags[dest->index] |= FRINGE_MASK; 
454          smt_enqueue(Q, (long) dest);
455        }
456      }
457    }
458
459    if(cycleFound)      break;
460  }
461
462  if(cycleFound) {
463
464    sm->stats->num_bf_conf++;
465
466    sm->flag &= RESET_SAT_MASK;
467
468    smt_collect_edges_in_neg_cycle(G, dest);
469
470    smt_get_lemma_from_neg_cycle(sm, G->neg_edges);
471
472    smt_retrieve_previous_distance(sm);
473
474  } else if (qsize) {
475   
476    smt_update_value_with_current_distance(sm);
477
478  }
479
480  return;
481}
482
483void
484smt_init_bellman_ford_algorithm(smtManager_t * sm)
485{
486  smtGraph_t * G = sm->cG;
487  smtVertex_t * src, * dest;
488  smtEdge_t * e;
489  smtQueue_t * Q;
490  double new_dist = 0, cur_dist = 0, weight = 0;
491  int i;
492
493  memset(G->flags, 0, sizeof(int) * G->vsize);
494  memset(G->paths, 0, sizeof(smtVertex_t *) * G->vsize);
495
496  Q = G->queue;
497  smt_init_queue(Q);
498
499  for(i = 0; i < G->cur_edges->size; i++) {
500    e = (smtEdge_t *) G->cur_edges->space[i];
501    src = e->src;
502    dest = e->dest;
503    weight = e->weight;
504
505    if (sm->flag & IDL_MASK) { 
506      new_dist = (double) G->idists[src->index] + weight;
507      cur_dist = (double) G->idists[dest->index];
508    } else if (sm->flag & RDL_MASK) {
509      new_dist = G->rdists[src->index] + weight;
510      cur_dist = G->rdists[dest->index];
511    } else {
512      exit(0);
513    }
514
515    if(new_dist < cur_dist) {
516      if(!(G->flags[src->index] & FRINGE_MASK)) {
517        G->flags[src->index] |= FRINGE_MASK; /* not in queue */
518        smt_enqueue(Q, (long) src);
519      }
520    }
521  }
522
523  return;
524}
525
526void
527smt_delete_subtree(smtGraph_t * G, smtVertex_t * v)
528{
529  smtEdge_t * e;
530  int i;
531
532  for(i = 0; i < v->outs->size; i++) {
533    e = (smtEdge_t *) v->outs->space[i];
534
535    if(G->paths[e->dest->index] == v) {
536      G->paths[e->dest->index] = 0;
537      G->flags[e->dest->index] |= VISITED_MASK;
538      smt_delete_subtree(G, e->dest);
539    }
540  }
541
542  return;
543}
544
545void
546smt_collect_edges_in_neg_cycle(smtGraph_t * G, smtVertex_t * v)
547{
548  smtVertex_t * src, * dest;
549  smtEdge_t * e;
550
551  dest = v;
552  G->neg_edges->size = 0;
553
554  while(1) {
555    if (G->flags[dest->index] & VISITED_MASK)
556      break;
557    src = G->paths[dest->index];
558    e = smt_find_edge(src, dest);
559    G->neg_edges = sat_array_insert(G->neg_edges, (long) e);
560    G->flags[dest->index] |= VISITED_MASK;
561    dest = src;   
562  }
563
564  return;
565}
566
567void
568smt_get_lemma_from_neg_cycle(smtManager_t * sm, satArray_t * neg_edges)
569{
570  satManager_t *cm = sm->cm;
571  smtAvar_t * avar;
572  smtEdge_t * e;
573  int i, id, sign, value, lit = 0;
574
575  for(i = 0; i < neg_edges->size; i++) {
576    e = (smtEdge_t *) neg_edges->space[i];
577    avar = e->avar;
578    value = sm->avalues[avar->id];
579
580    if (value == 1)
581      lit = avar->id;
582    else if (value == 0)
583      lit = -avar->id;
584    else
585      exit(0);
586   
587    sm->lemma = sat_array_insert(sm->lemma, lit);
588    sign = (lit>0) ? 1 : 0;
589    id = avar->id;
590    cm->explanation = sat_array_insert(cm->explanation, ((id<<1) + sign));
591  }
592 
593  return;
594}
595
596void
597smt_retrieve_previous_distance(smtManager_t * sm)
598{
599  if (sm->flag & IDL_MASK) 
600    memcpy(sm->cG->idists, sm->ivalues, sizeof(int) * (sm->cG->vsize));
601  else if (sm->flag & RDL_MASK)
602    memcpy(sm->cG->rdists, sm->rvalues, sizeof(double) * (sm->cG->vsize));
603
604  return;
605}
606
607void
608smt_update_value_with_current_distance(smtManager_t * sm)
609{
610  if (sm->flag & IDL_MASK) 
611    memcpy(sm->ivalues, sm->cG->idists, sizeof(int) * (sm->cG->vsize));
612  else if (sm->flag & RDL_MASK)
613    memcpy(sm->rvalues, sm->cG->rdists, sizeof(double) * (sm->cG->vsize));
614
615  return;
616}
617
618void
619smt_init_dl_theory_propagation(smtGraph_t * G)
620{
621  memset(G->flags, 0, sizeof(int) * G->vsize);
622}
623
624void
625smt_idl_theory_propagation(smtManager_t * sm)
626{
627  satManager_t * cm = sm->cm;
628  smtGraph_t * G = sm->cG;
629  smtAvar_t * avar;
630  smtNvar_t * lnvar, * rnvar;
631  smtVertex_t * src, * dest;
632  int num_bavar, num_favar;
633  int i, j, id, lit, level, vindex;
634
635  level = cm->decisionStackSeperator->size;
636#if 1
637  if (level == 0) j = 1;
638  else j = 3;
639#else
640  j = 1;
641#endif
642
643  for(i = sm->cur_index; i<sm->litArr->size; i+=j) { 
644
645    lit = sm->litArr->space[i];
646    id = (lit>0) ? lit : -lit;
647    avar = (smtAvar_t *) sm->id2var->space[id];
648
649    if (avar->flag & IMPLIED_MASK || avar->flag & TPROP_MASK) {
650      if (i + j <= 0) {
651        i = sm->cur_index;
652        j = 3;
653      }
654
655      continue;
656    }
657
658    assert(avar->type != EQ_c);
659
660    if (sm->avalues[id] == 1) {
661      lnvar = (smtNvar_t *) avar->nvars->space[0];
662      rnvar = (smtNvar_t *) avar->nvars->space[1];
663    } else {
664      assert(sm->avalues[id] == 0);
665      lnvar = (smtNvar_t *) avar->nvars->space[1];
666      rnvar = (smtNvar_t *) avar->nvars->space[0];
667    }
668
669    vindex = lnvar->id - 1;
670    dest = &(G->vHead[vindex]);
671    vindex = rnvar->id - 1;
672    src =  &(G->vHead[vindex]);
673
674    G->bvArr->size = 0;
675
676    G->fvArr->size = 0;
677
678    num_bavar = 0;
679
680    num_favar = 0;
681
682    smt_idl_gather_backward_reachable_vertex_with_dfs(G, src, &num_bavar);
683
684    smt_idl_gather_forward_reachable_vertex_with_dfs(G, dest, &num_favar);
685   
686    if (num_bavar > num_favar) {
687     
688      smt_idl_theory_propagation_with_bv_arr(sm, avar);
689
690    } else {
691
692      smt_idl_theory_propagation_with_fv_arr(sm, avar);
693
694    }
695
696    smt_idl_init_reachable_vertex(G);
697  }
698
699  return;
700}
701
702void
703smt_rdl_theory_propagation(smtManager_t * sm)
704{
705  satManager_t * cm = sm->cm;
706  smtGraph_t * G = sm->cG;
707  smtAvar_t * avar;
708  smtNvar_t * lnvar, * rnvar;
709  smtVertex_t * src, * dest;
710  int num_bavar, num_favar;
711  int i, j, id, lit, level, vindex;
712
713  level = (int) cm->decisionStackSeperator->size;
714#if 1
715  if (level == 0) j = 1;
716  else j = 3;
717#else
718  j = 1;
719#endif
720
721  for(i = sm->cur_index; i<sm->litArr->size; i+=j) { 
722
723    lit = sm->litArr->space[i];
724    id = (lit>0) ? lit : -lit;
725    avar = (smtAvar_t *) sm->id2var->space[id];
726
727    if (avar->flag & IMPLIED_MASK || avar->flag & TPROP_MASK) {
728      if (i + j <= 0) {
729        i = sm->cur_index;
730        j = 3;
731      }
732
733      continue;
734    }
735
736    if (sm->avalues[id] == 1) {
737      lnvar = (smtNvar_t *) avar->nvars->space[0];
738      rnvar = (smtNvar_t *) avar->nvars->space[1];
739    } else {
740      assert(sm->avalues[id] == 0);
741      lnvar = (smtNvar_t *) avar->nvars->space[1];
742      rnvar = (smtNvar_t *) avar->nvars->space[0];
743    }
744
745    vindex = lnvar->id - 1;
746    dest = &(G->vHead[vindex]);
747    vindex = rnvar->id - 1;
748    src =  &(G->vHead[vindex]);
749
750    G->bvArr->size = 0;
751
752    G->fvArr->size = 0;
753
754    num_bavar = 0;
755
756    num_favar = 0;
757
758    smt_rdl_gather_backward_reachable_vertex_with_dfs(G, src, &num_bavar);
759
760    smt_rdl_gather_forward_reachable_vertex_with_dfs(G, dest, &num_favar);
761   
762    if (num_bavar > num_favar) { 
763
764      smt_rdl_theory_propagation_with_bv_arr(sm, avar);
765
766    } else {
767
768      smt_rdl_theory_propagation_with_fv_arr(sm, avar);
769     
770    }
771
772    smt_rdl_init_reachable_vertex(G); 
773  }
774}
775
776void
777smt_idl_gather_backward_reachable_vertex_with_dfs(
778  smtGraph_t * G, 
779  smtVertex_t * v,
780  int * num_avar)
781{
782  int depth; 
783
784  G->bidists[v->index] = 0;
785  G->bpaths[v->index] = 0;
786  depth = 0;
787
788  smt_idl_traverse_backward_with_dfs(G, v, num_avar, depth);
789}
790
791void
792smt_idl_gather_forward_reachable_vertex_with_dfs(
793  smtGraph_t * G, 
794  smtVertex_t * v,
795  int * num_avar)
796{
797  int depth; 
798
799  G->fidists[v->index] = 0;
800  G->fpaths[v->index] = 0;
801  depth = 0;
802
803  smt_idl_traverse_forward_with_dfs(G, v, num_avar, depth);
804}
805
806void
807smt_rdl_gather_backward_reachable_vertex_with_dfs(
808  smtGraph_t * G, 
809  smtVertex_t * v,
810  int * num_avar)
811{
812  int depth; 
813
814  G->brdists[v->index] = 0;
815  G->bpaths[v->index] = 0;
816  depth = 0;
817
818  smt_rdl_traverse_backward_with_dfs(G, v, num_avar, depth);
819}
820
821void
822smt_rdl_gather_forward_reachable_vertex_with_dfs(
823  smtGraph_t * G, 
824  smtVertex_t * v,
825  int * num_avar)
826{
827  int depth; 
828
829  G->frdists[v->index] = 0;
830  G->fpaths[v->index] = 0;
831  depth = 0;
832
833  smt_rdl_traverse_forward_with_dfs(G, v, num_avar, depth);
834}
835
836void
837smt_idl_traverse_backward_with_dfs(
838  smtGraph_t * G, 
839  smtVertex_t * v, 
840  int * num_avar, 
841  int depth)
842{
843  smtNvar_t * nvar;
844  smtVertex_t * w;
845  smtEdge_t * e;
846  double weight;
847  int i;
848#if 0
849  depth++; 
850#endif
851
852  G->flags[v->index] |= BVISITED_MASK;
853
854  if (!(G->flags[v->index] & BFRINGE_MASK)) {
855    G->bvArr = sat_array_insert(G->bvArr, (long) v);
856    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
857    *num_avar += nvar->avarArr->size;
858    G->flags[v->index] |= BFRINGE_MASK;
859  }
860
861  for(i = 0; i < v->ins->size; i++) {
862    e = (smtEdge_t *) v->ins->space[i];
863    w = e->src;
864    weight = e->weight;
865
866    if (!(G->flags[w->index] & BVISITED_MASK) ||
867        G->bidists[w->index] > G->bidists[v->index] + (int) weight) {
868
869      G->bidists[w->index] = G->bidists[v->index] + (int) weight;
870      G->bpaths[w->index] = v;
871      smt_idl_traverse_backward_with_dfs(G, w, num_avar, depth);     
872    }
873  }
874
875  return;
876}
877
878void
879smt_idl_traverse_forward_with_dfs(
880  smtGraph_t * G, 
881  smtVertex_t * v, 
882  int * num_avar, 
883  int depth)
884{
885  smtNvar_t * nvar;
886  smtVertex_t * w;
887  smtEdge_t * e;
888  double weight;
889  int i;
890#if 0
891  depth++;
892#endif
893
894  G->flags[v->index] |= FVISITED_MASK;
895
896  if (!(G->flags[v->index] & FFRINGE_MASK)) {
897    G->fvArr = sat_array_insert(G->fvArr, (long) v);
898    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
899    *num_avar += nvar->avarArr->size;
900    G->flags[v->index] |= FFRINGE_MASK;
901  }
902
903  for(i = 0; i < v->outs->size; i++) {
904    e = (smtEdge_t *) v->outs->space[i];
905    w = e->dest;
906    weight = e->weight;
907
908    if (!(G->flags[w->index] & FVISITED_MASK) ||
909        G->fidists[w->index] > G->fidists[v->index] + (int) weight) {
910
911      G->fidists[w->index] = G->fidists[v->index] + (int) weight;
912      G->fpaths[w->index] = v;
913      smt_idl_traverse_forward_with_dfs(G, w, num_avar, depth);     
914    }
915  }
916
917  return;
918}
919
920void
921smt_rdl_traverse_backward_with_dfs(
922  smtGraph_t * G, 
923  smtVertex_t * v, 
924  int * num_avar, 
925  int depth)
926{
927  smtNvar_t * nvar;
928  smtVertex_t * w;
929  smtEdge_t * e;
930  double weight;
931  int i;
932#if 0
933  depth++;
934#endif
935
936  G->flags[v->index] |= BVISITED_MASK;
937
938  if (!(G->flags[v->index] & BFRINGE_MASK)) {
939    G->bvArr = sat_array_insert(G->bvArr, (long) v);
940    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
941    *num_avar += nvar->avarArr->size;
942    G->flags[v->index] |= BFRINGE_MASK;
943  }
944
945  for(i = 0; i < v->ins->size; i++) {
946    e = (smtEdge_t *) v->ins->space[i];
947    w = e->src;
948    weight = e->weight + G->epsilonless; 
949
950    if (!(G->flags[w->index] & BVISITED_MASK) ||
951    G->brdists[w->index] > G->brdists[v->index] + weight) {
952
953      G->brdists[w->index] = G->brdists[v->index] + e->weight;
954      G->bpaths[w->index] = v;
955      smt_rdl_traverse_backward_with_dfs(G, w, num_avar, depth);
956     
957    }
958  }
959
960  return;
961}
962
963void
964smt_rdl_traverse_forward_with_dfs(
965  smtGraph_t * G, 
966  smtVertex_t * v, 
967  int * num_avar, 
968  int depth)
969{
970  smtNvar_t * nvar;
971  smtVertex_t * w;
972  smtEdge_t * e;
973  double weight;
974  int i;
975#if 0
976  depth++;
977#endif
978
979  G->flags[v->index] |= FVISITED_MASK;
980
981  if (!(G->flags[v->index] & FFRINGE_MASK)) {
982    G->fvArr = sat_array_insert(G->fvArr, (long) v);
983    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
984    *num_avar += nvar->avarArr->size;
985    G->flags[v->index] |= FFRINGE_MASK;
986  }
987
988  for(i = 0; i < v->outs->size; i++) {
989    e = (smtEdge_t *) v->outs->space[i];
990    w = e->dest;
991
992    weight = e->weight + G->epsilonless; 
993
994    if (!(G->flags[w->index] & FVISITED_MASK) ||
995        G->frdists[w->index] > G->frdists[v->index] + weight) {
996
997      G->frdists[w->index] = G->frdists[v->index] + e->weight;
998      G->fpaths[w->index] = v;
999      smt_rdl_traverse_forward_with_dfs(G, w, num_avar, depth);     
1000    }
1001  }
1002
1003  return;
1004}
1005
1006void
1007smt_idl_gather_backward_reachable_vertex_with_bfs(
1008  smtGraph_t * G, 
1009  smtVertex_t * src,
1010  int * num_avar)
1011{
1012  smtVertex_t * v, * w;
1013  smtEdge_t * e;
1014  smtNvar_t * nvar;
1015  smtQueue_t * Q = G->queue;
1016  double weight;
1017  int i;
1018
1019  G->bidists[src->index] = 0;
1020  G->bpaths[src->index] = 0;
1021
1022  smt_init_queue(Q);
1023
1024  smt_enqueue(Q, (long) src);
1025   
1026  while( (v = (smtVertex_t *) smt_dequeue(Q)) ) {
1027   
1028    G->flags[v->index] &= RESET_BFRINGE_MASK;
1029   
1030    if (!(G->flags[v->index] & BARR_MASK)) {
1031      G->bvArr = sat_array_insert(G->bvArr, (long) v);
1032      nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1033      *num_avar += nvar->avarArr->size;
1034      G->flags[v->index] |= BARR_MASK;
1035    }
1036
1037    for(i = 0; i < v->ins->size; i++) {
1038      e = (smtEdge_t *) v->ins->space[i];
1039      w = e->src;
1040      weight = e->weight;
1041
1042      if (G->bidists[w->index] > G->bidists[v->index] + (int) weight) {
1043
1044        G->bidists[w->index] = G->bidists[v->index] + (int) weight;
1045        G->bpaths[w->index] = v;
1046        if (!(G->flags[w->index] & BFRINGE_MASK)) {
1047          smt_enqueue(Q, (long) w);
1048          G->flags[w->index] |= BFRINGE_MASK;
1049        }       
1050      }
1051    }
1052  }
1053
1054  return;
1055}
1056
1057void
1058smt_rdl_gather_backward_reachable_vertex_with_bfs(
1059  smtGraph_t * G, 
1060  smtVertex_t * src,
1061  int * num_avar)
1062{
1063  smtVertex_t * v, * w;
1064  smtEdge_t * e;
1065  smtNvar_t * nvar;
1066  smtQueue_t * Q = G->queue;
1067  double weight;
1068  int i;
1069
1070  G->brdists[src->index] = 0;
1071  G->bpaths[src->index] = 0;
1072
1073  smt_init_queue(Q);
1074
1075  smt_enqueue(Q, (long) src);
1076   
1077  while( (v = (smtVertex_t *) smt_dequeue(Q)) ) {
1078   
1079    G->flags[v->index] &= RESET_BFRINGE_MASK;
1080   
1081    if (!(G->flags[v->index] & BARR_MASK)) {
1082      G->bvArr = sat_array_insert(G->bvArr, (long) v);
1083      nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1084      *num_avar += nvar->avarArr->size;
1085      G->flags[v->index] |= BARR_MASK;
1086    }
1087
1088    for(i = 0; i < v->ins->size; i++) {
1089      e = (smtEdge_t *) v->ins->space[i];
1090      w = e->src;
1091      weight = e->weight + G->epsilonless; 
1092
1093      if (G->brdists[w->index] > G->brdists[v->index] + weight) {
1094
1095        G->brdists[w->index] = G->brdists[v->index] + e->weight;
1096        G->bpaths[w->index] = v;
1097        if (!(G->flags[w->index] & BFRINGE_MASK)) {
1098          smt_enqueue(Q, (long) w);
1099          G->flags[w->index] |= BFRINGE_MASK;
1100        }       
1101      }
1102    }
1103  }
1104
1105  return;
1106}
1107
1108void
1109smt_idl_gather_forward_reachable_vertex_with_bfs(
1110  smtGraph_t * G, 
1111  smtVertex_t * dest,
1112  int * num_avar)
1113{
1114  smtVertex_t * v, * w;
1115  smtEdge_t * e;
1116  smtNvar_t * nvar;
1117  smtQueue_t * Q = G->queue;
1118  double weight;
1119  int i;
1120
1121  G->fidists[dest->index] = 0;
1122  G->fpaths[dest->index] = 0;
1123
1124  smt_init_queue(Q);
1125
1126  smt_enqueue(Q, (long) dest);
1127   
1128  while( (v = (smtVertex_t *) smt_dequeue(Q)) ) {
1129   
1130    G->flags[v->index] &= RESET_FFRINGE_MASK;
1131   
1132    if (!(G->flags[v->index] & FARR_MASK)) {
1133      G->fvArr = sat_array_insert(G->fvArr, (long) v);
1134      nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1135      *num_avar += nvar->avarArr->size;
1136      G->flags[v->index] |= FARR_MASK;
1137    }
1138
1139    for(i = 0; i < v->outs->size; i++) {
1140      e = (smtEdge_t *) v->outs->space[i];
1141      w = e->dest;
1142      weight = e->weight;
1143
1144      if (G->fidists[w->index] > G->fidists[v->index] + (int) weight) {
1145
1146        G->fidists[w->index] = G->fidists[v->index] + (int) weight;
1147        G->fpaths[w->index] = v;
1148        if (!(G->flags[w->index] & FFRINGE_MASK)) {
1149          smt_enqueue(Q, (long) w);
1150          G->flags[w->index] |= FFRINGE_MASK;
1151        }       
1152      }
1153    }
1154  }
1155
1156  return;
1157}
1158
1159void
1160smt_rdl_gather_forward_reachable_vertex_with_bfs(
1161  smtGraph_t * G, 
1162  smtVertex_t * dest,
1163  int * num_avar)
1164{
1165  smtVertex_t * v, * w;
1166  smtEdge_t * e;
1167  smtNvar_t * nvar;
1168  smtQueue_t * Q = G->queue;
1169  double weight;
1170  int i;
1171
1172  G->frdists[dest->index] = 0;
1173  G->fpaths[dest->index] = 0;
1174
1175  smt_init_queue(Q);
1176
1177  smt_enqueue(Q, (long) dest);
1178   
1179  while( (v = (smtVertex_t *) smt_dequeue(Q)) ) {
1180   
1181    G->flags[v->index] &= RESET_FFRINGE_MASK;
1182   
1183    if (!(G->flags[v->index] & FARR_MASK)) {
1184      G->fvArr = sat_array_insert(G->fvArr, (long) v);
1185      nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1186      *num_avar += nvar->avarArr->size;
1187      G->flags[v->index] |= FARR_MASK;
1188    }
1189
1190    for(i = 0; i < v->outs->size; i++) {
1191      e = (smtEdge_t *) v->outs->space[i];
1192      w = e->dest;
1193      weight = e->weight + G->epsilonless;
1194
1195      if (G->frdists[w->index] > G->frdists[v->index] + weight) {
1196
1197        G->frdists[w->index] = G->frdists[v->index] + e->weight;
1198        G->fpaths[w->index] = v;
1199        if (!(G->flags[w->index] & FFRINGE_MASK)) {
1200          smt_enqueue(Q, (long) w);
1201          G->flags[w->index] |= FFRINGE_MASK;
1202        }       
1203      }
1204    }
1205  }
1206
1207  return;
1208}
1209
1210void
1211smt_idl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar)
1212{
1213  smtGraph_t * G = sm->cG;
1214  smtAvar_t * tmp_avar;
1215  smtNvar_t * nvar;/*, * rnvar, * lnvar;*/
1216  smtNvar_t * tmp_rnvar, * tmp_lnvar;
1217  smtVertex_t * v;
1218  satArray_t * bvArr;
1219  double weight, tmp_weight;
1220  int dist, id;
1221  int i, j;
1222
1223  id = avar->id;
1224
1225  if (sm->avalues[id] == 1) {
1226    /*lnvar = (smtNvar_t *) avar->nvars->space[0];
1227      rnvar = (smtNvar_t *) avar->nvars->space[1];*/
1228    weight = avar->constant;
1229  } else {
1230    assert(sm->avalues[id] == 0);
1231    /*lnvar = (smtNvar_t *) avar->nvars->space[1];
1232      rnvar = (smtNvar_t *) avar->nvars->space[0];*/
1233    weight = -avar->constant - sm->epsilon;
1234  } 
1235
1236  bvArr = G->bvArr;
1237
1238  for(i = 0; i < bvArr->size; i++) { 
1239    v = (smtVertex_t *) bvArr->space[i];
1240    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1241   
1242    for(j = 0; j < nvar->avarArr->size; j++) {
1243      tmp_avar = (smtAvar_t *) nvar->avarArr->space[j]; 
1244      sm->stats->num_tprop_call++;
1245      if (sm->avalues[tmp_avar->id] != 2) continue;
1246      tmp_lnvar = (smtNvar_t *) tmp_avar->nvars->space[0];
1247      tmp_rnvar = (smtNvar_t *) tmp_avar->nvars->space[1];
1248      tmp_weight = tmp_avar->constant;
1249     
1250      if (nvar == tmp_rnvar && G->fidists[tmp_lnvar->id-1] != INT_MAX) {
1251        dist = G->fidists[tmp_lnvar->id-1] + 
1252          G->bidists[tmp_rnvar->id-1] + (int) weight;
1253       
1254        if (dist <= tmp_weight) {
1255          sm->stats->num_tprop++;
1256          /*  x - y <= dist ---> x - y <= weight (dist <= weight)  */
1257          sm->avalues[tmp_avar->id] = 1;
1258          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1259                                        tmp_rnvar, tmp_lnvar);
1260        }
1261      } else if (nvar == tmp_lnvar && 
1262                 G->fidists[tmp_rnvar->id-1] != INT_MAX) {
1263        dist = G->bidists[tmp_lnvar->id-1] + 
1264          G->fidists[tmp_rnvar->id-1] + (int) weight;
1265
1266        if (-dist > tmp_weight) {
1267          sm->stats->num_tprop++;
1268          /*  x - y <= dist ---> y - x <= weight (dist + weight < 0)  */
1269          sm->avalues[tmp_avar->id] = 0;
1270          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1271                                        tmp_lnvar, tmp_rnvar);
1272        }
1273      }
1274    }
1275  }
1276
1277  return;
1278}
1279
1280void
1281smt_idl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar)
1282{
1283  smtGraph_t * G = sm->cG;
1284  smtAvar_t * tmp_avar;
1285  smtNvar_t * nvar;
1286  smtNvar_t * tmp_rnvar, * tmp_lnvar;
1287  smtVertex_t * v;
1288  satArray_t * fvArr;
1289  double weight, tmp_weight;
1290  int dist, id;
1291  int i, j;
1292
1293  id = avar->id;
1294
1295  if (sm->avalues[id] == 1) {
1296    /*lnvar = (smtNvar_t *) avar->nvars->space[0];
1297    rnvar = (smtNvar_t *) avar->nvars->space[1];*/
1298    weight = avar->constant;
1299  } else {
1300    assert(sm->avalues[id] == 0);
1301    /*lnvar = (smtNvar_t *) avar->nvars->space[1];
1302    rnvar = (smtNvar_t *) avar->nvars->space[0];*/
1303    weight = -avar->constant - sm->epsilon;
1304  } 
1305
1306  fvArr = G->fvArr;
1307
1308  for(i = 0; i < fvArr->size; i++) { 
1309    v = (smtVertex_t *) fvArr->space[i];
1310    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1311   
1312    for(j = 0; j < nvar->avarArr->size; j++) {
1313      tmp_avar = (smtAvar_t *) nvar->avarArr->space[j]; 
1314      sm->stats->num_tprop_call++;
1315      if (sm->avalues[tmp_avar->id] != 2) continue;
1316      tmp_lnvar = (smtNvar_t *) tmp_avar->nvars->space[0];
1317      tmp_rnvar = (smtNvar_t *) tmp_avar->nvars->space[1];
1318      tmp_weight = tmp_avar->constant;
1319     
1320      if (nvar == tmp_lnvar && G->bidists[tmp_rnvar->id-1] != INT_MAX) {
1321        dist = G->fidists[tmp_lnvar->id-1] + 
1322          G->bidists[tmp_rnvar->id-1] + (int) weight;
1323       
1324        if (dist <= (int) tmp_weight) {
1325          sm->stats->num_tprop++;
1326          /*  x - y <= dist ---> x - y <= weight (dist <= weight)  */
1327          sm->avalues[tmp_avar->id] = 1;
1328          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1329                                        tmp_rnvar, tmp_lnvar);
1330        }
1331      } else if (nvar == tmp_rnvar && 
1332                 G->bidists[tmp_lnvar->id-1] != INT_MAX) {
1333        dist = G->bidists[tmp_lnvar->id-1] + 
1334          G->fidists[tmp_rnvar->id-1] + (int) weight;
1335
1336        if (-dist > (int) tmp_weight) {
1337          sm->stats->num_tprop++;
1338          /*  x - y <= dist ---> y - x <= weight (dist + weight < 0)  */
1339          sm->avalues[tmp_avar->id] = 0;
1340          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1341                                        tmp_lnvar, tmp_rnvar);
1342        }
1343      }
1344    }
1345  }
1346
1347  return;
1348}
1349
1350void
1351smt_rdl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar)
1352{
1353  smtGraph_t * G = sm->cG;
1354  smtAvar_t * tmp_avar;
1355  smtNvar_t * nvar; /*, * rnvar, * lnvar;*/
1356  smtNvar_t * tmp_rnvar, * tmp_lnvar;
1357  smtVertex_t * v;
1358  satArray_t * bvArr;
1359  double weight, tmp_weight, dist;
1360  int id;
1361  int i, j;
1362
1363  id = avar->id;
1364
1365  if (sm->avalues[id] == 1) {
1366    /*lnvar = (smtNvar_t *) avar->nvars->space[0];
1367      rnvar = (smtNvar_t *) avar->nvars->space[1];*/
1368    weight = avar->constant;
1369  } else {
1370    assert(sm->avalues[id] == 0);
1371    /*lnvar = (smtNvar_t *) avar->nvars->space[1];
1372      rnvar = (smtNvar_t *) avar->nvars->space[0];*/
1373    weight = -avar->constant - sm->epsilon;
1374  } 
1375
1376  bvArr = G->bvArr;
1377
1378  for(i = 0; i < bvArr->size; i++) { 
1379    v = (smtVertex_t *) bvArr->space[i];
1380    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1381   
1382    for(j = 0; j < nvar->avarArr->size; j++) {
1383      tmp_avar = (smtAvar_t *) nvar->avarArr->space[j]; 
1384      sm->stats->num_tprop_call++;
1385      if (sm->avalues[tmp_avar->id] != 2) continue;
1386      tmp_lnvar = (smtNvar_t *) tmp_avar->nvars->space[0];
1387      tmp_rnvar = (smtNvar_t *) tmp_avar->nvars->space[1];
1388      tmp_weight = tmp_avar->constant;
1389     
1390      if (nvar == tmp_rnvar && G->frdists[tmp_lnvar->id-1] < HUGE_VAL) {
1391        dist = G->frdists[tmp_lnvar->id-1] + 
1392          G->brdists[tmp_rnvar->id-1] + weight;
1393       
1394        if (dist <= tmp_weight) {
1395          sm->stats->num_tprop++;
1396          /*  x - y <= dist ---> x - y <= weight (dist <= weight)  */
1397          sm->avalues[tmp_avar->id] = 1;
1398          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1399                                        tmp_rnvar, tmp_lnvar);
1400        }
1401      } else if (nvar == tmp_lnvar && 
1402                 G->frdists[tmp_rnvar->id-1] < HUGE_VAL) {
1403        dist = G->brdists[tmp_lnvar->id-1] + 
1404          G->frdists[tmp_rnvar->id-1] + weight;
1405
1406        if (-dist > tmp_weight) {
1407          sm->stats->num_tprop++;
1408          /*  x - y <= dist ---> y - x <= weight (dist + weight < 0)  */
1409          sm->avalues[tmp_avar->id] = 0;
1410          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1411                                        tmp_lnvar, tmp_rnvar);
1412        }
1413      }
1414    }
1415  }
1416
1417  return;
1418}
1419
1420void
1421smt_rdl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar)
1422{
1423  smtGraph_t * G = sm->cG;
1424  smtAvar_t * tmp_avar;
1425  smtNvar_t * nvar; /*, * rnvar, * lnvar;*/
1426  smtNvar_t * tmp_rnvar, * tmp_lnvar;
1427  smtVertex_t * v;
1428  satArray_t * fvArr;
1429  double weight, tmp_weight, dist;
1430  int id;
1431  int i, j;
1432
1433  id = avar->id;
1434
1435  if (sm->avalues[id] == 1) {
1436    /*lnvar = (smtNvar_t *) avar->nvars->space[0];
1437      rnvar = (smtNvar_t *) avar->nvars->space[1];*/
1438    weight = avar->constant;
1439  } else {
1440    assert(sm->avalues[id] == 0);
1441    /*lnvar = (smtNvar_t *) avar->nvars->space[1];
1442      rnvar = (smtNvar_t *) avar->nvars->space[0];*/
1443    weight = -avar->constant - sm->epsilon;
1444  } 
1445
1446  fvArr = G->fvArr;
1447
1448  for(i = 0; i < fvArr->size; i++) { 
1449    v = (smtVertex_t *) fvArr->space[i];
1450    nvar = (smtNvar_t *) G->nvarArr->space[v->index];
1451   
1452    for(j = 0; j < nvar->avarArr->size; j++) {
1453      tmp_avar = (smtAvar_t *) nvar->avarArr->space[j]; 
1454      sm->stats->num_tprop_call++;
1455      if (sm->avalues[tmp_avar->id] != 2) continue;
1456      tmp_lnvar = (smtNvar_t *) tmp_avar->nvars->space[0];
1457      tmp_rnvar = (smtNvar_t *) tmp_avar->nvars->space[1];
1458      tmp_weight = tmp_avar->constant;
1459     
1460      if (nvar == tmp_lnvar && G->brdists[tmp_rnvar->id-1] < HUGE_VAL) {
1461        dist = G->frdists[tmp_lnvar->id-1] + 
1462          G->brdists[tmp_rnvar->id-1] + weight;
1463       
1464        if (dist <= tmp_weight) {
1465          sm->stats->num_tprop++;
1466          /*  x - y <= dist ---> x - y <= weight (dist <= weight)  */
1467          sm->avalues[tmp_avar->id] = 1;
1468          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1469                                        tmp_rnvar, tmp_lnvar);
1470        }
1471      } else if (nvar == tmp_rnvar && 
1472                 G->brdists[tmp_lnvar->id-1] < HUGE_VAL) {
1473        dist = G->brdists[tmp_lnvar->id-1] + 
1474          G->frdists[tmp_rnvar->id-1] + weight;
1475
1476        if (-dist > tmp_weight) {
1477          sm->stats->num_tprop++;
1478          /*  x - y <= dist ---> y - x <= weight (dist + weight < 0)  */
1479          sm->avalues[tmp_avar->id] = 0;
1480          smt_get_theory_prop_reason(sm, avar, tmp_avar, 
1481                                        tmp_lnvar, tmp_rnvar);
1482        }
1483      }
1484    }
1485  }
1486
1487  return;
1488}
1489
1490void
1491smt_dl_simple_theory_propagation(smtManager_t * sm)
1492{
1493  smtAvar_t * avar, * sis_avar;
1494  smtNvar_t * lnvar, * sis_lnvar;
1495  double weight, sis_weight;
1496  int lit, id;
1497  int i, j;
1498
1499#if 0
1500  level = sm->cm->decisionStackSeperator->size;
1501  skip_tp_cond = level!=0 &&
1502    (smt_gv->color & RDL_MASK && sm->bvarArr->size>100 &&
1503    sm->avarArr->size > 50*sm->bvarArr->size);
1504  if (skip_tp_cond) return;
1505#endif
1506
1507  for(i = sm->cur_index; i < sm->litArr->size; i++) {
1508    lit = sm->litArr->space[i];
1509    id = (lit > 0)? lit : -lit;
1510    avar = (smtAvar_t *) sm->id2var->space[id];
1511
1512    sm->stats->num_simp_tprop_call++;
1513   
1514    if (avar->flag & IMPLIED_MASK || avar->flag & TPROP_MASK)
1515      continue;
1516   
1517    if (sm->avalues[id] == 1) {
1518      lnvar = (smtNvar_t *) avar->nvars->space[0];
1519      weight = avar->constant;
1520    } else {
1521      assert(sm->avalues[id] == 0);
1522      lnvar = (smtNvar_t *) avar->nvars->space[1];
1523      weight = -avar->constant - sm->epsilon;
1524    }
1525
1526    for(j = 0; j < avar->sis_avars->num; j++) { /* check sister avar */
1527      sis_avar = array_fetch(smtAvar_t *, avar->sis_avars, j);
1528      if (sm->avalues[sis_avar->id] != 2) continue;
1529
1530      sis_lnvar = (smtNvar_t *) sis_avar->nvars->space[0];
1531      sis_weight = sis_avar->constant;
1532
1533      if (sis_lnvar == lnvar) {
1534        if (sis_weight >= weight) {
1535          sm->stats->num_simp_tprop++;
1536          sm->avalues[sis_avar->id] = 1;
1537          smt_get_theory_prop_reason(sm, avar, sis_avar, 0, 0);
1538        }
1539      } else {
1540        if (sis_weight < -weight) {
1541          sm->stats->num_simp_tprop++;
1542          sm->avalues[sis_avar->id] = 0;
1543          smt_get_theory_prop_reason(sm, avar, sis_avar, 0, 0);
1544        }
1545      }
1546    }
1547  }
1548
1549  return; 
1550}
1551
1552void
1553smt_get_theory_prop_reason(
1554  smtManager_t * sm,
1555  smtAvar_t * implying, 
1556  smtAvar_t * implied,
1557  smtNvar_t * bnvar,
1558  smtNvar_t * fnvar)
1559{
1560  satManager_t * cm = sm->cm;
1561  smtGraph_t * G = sm->cG;
1562  smtVertex_t * bv, * fv, * path;
1563  smtEdge_t * e;
1564  smtAvar_t * avar;
1565  int sign, id;
1566
1567  /*
1568   * ((implying /\ avars_in_bpath /\ avars_in_fpath)' \/ implied)
1569   */
1570
1571  sm->lemma->size = 0;
1572
1573  /* implied avar */
1574  id = implied->id;
1575  sign = (sm->avalues[id] == 1) ? 0 : 1;
1576  sm->lemma = sat_array_insert(sm->lemma, (id<<1)+sign); 
1577
1578  if (bnvar) {
1579    /* reasons from backward shortest path */
1580    bv = &(G->vHead[bnvar->id-1]);
1581    path = G->bpaths[bv->index];
1582   
1583    while(path) {
1584      e = smt_find_edge(bv, path);
1585      avar = e->avar;
1586      id = avar->id;
1587      sign = (sm->avalues[id] == 1) ? 1 : 0; /* negated */
1588      sm->lemma = sat_array_insert(sm->lemma, (id<<1)+sign); 
1589      bv = path;
1590      path = G->bpaths[bv->index];
1591    }
1592  }
1593   
1594  if (fnvar) {
1595    /* reasons from forward shortest path */
1596    fv = &(G->vHead[fnvar->id-1]);
1597    path = G->fpaths[fv->index];
1598   
1599    while(path) {
1600      e = smt_find_edge(path, fv);
1601      avar = e->avar;
1602      id = avar->id;
1603      sign = (sm->avalues[id] == 1) ? 1 : 0; /* negated */
1604      sm->lemma = sat_array_insert(sm->lemma, (id<<1)+sign);
1605      fv = path;
1606      path = G->fpaths[fv->index];
1607    }
1608  }
1609
1610  /* reason from currently assigned implying */
1611  id = implying->id;
1612  sign = (sm->avalues[id] == 1) ? 1 : 0; /* negated */
1613  sm->lemma = sat_array_insert(sm->lemma, (id<<1)+sign);
1614  assert(sm->lemma->size);
1615
1616  smt_add_theory_clause(cm, implied, sm->lemma); 
1617
1618  return;
1619}
1620
1621void
1622smt_idl_init_reachable_vertex(smtGraph_t * G)
1623{
1624  smtVertex_t * v;
1625  int i;
1626
1627  for(i = 0; i < G->bvArr->size; i++) {
1628    v = (smtVertex_t *) G->bvArr->space[i];
1629
1630    G->flags[v->index] = 0;
1631    G->bpaths[v->index] = 0;
1632    G->fpaths[v->index] = 0;
1633    G->bidists[v->index] = INT_MAX;
1634    G->fidists[v->index] = INT_MAX;
1635  }
1636
1637  for(i = 0; i < G->fvArr->size; i++) {
1638    v = (smtVertex_t *) G->fvArr->space[i];
1639
1640    G->flags[v->index] = 0;
1641    G->bpaths[v->index] = 0;
1642    G->fpaths[v->index] = 0;
1643    G->bidists[v->index] = INT_MAX;
1644    G->fidists[v->index] = INT_MAX;
1645  }
1646}
1647
1648void
1649smt_rdl_init_reachable_vertex(smtGraph_t * G)
1650{
1651  smtVertex_t * v;
1652  int i;
1653
1654  for(i = 0; i < G->bvArr->size; i++) {
1655    v = (smtVertex_t *) G->bvArr->space[i];
1656
1657    G->flags[v->index] = 0;
1658    G->bpaths[v->index] = 0;
1659    G->fpaths[v->index] = 0;
1660    G->brdists[v->index] = HUGE_VAL;
1661    G->frdists[v->index] = HUGE_VAL;
1662  }
1663
1664  for(i = 0; i < G->fvArr->size; i++) {
1665    v = (smtVertex_t *) G->fvArr->space[i];
1666
1667    G->flags[v->index] = 0;
1668    G->bpaths[v->index] = 0;
1669    G->fpaths[v->index] = 0;
1670    G->brdists[v->index] = HUGE_VAL;
1671    G->frdists[v->index] = HUGE_VAL;
1672  }
1673}
1674
1675#endif
Note: See TracBrowser for help on using the repository browser.