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

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

cusp added

File size: 13.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [smtSat.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
49#define NEW_BLOCKING
50
51int
52smt_call_theory_solver(satManager_t * m, long bound)
53{
54  smtManager_t * sm = (smtManager_t *) m->SMTManager; 
55  int ret_val = 0;
56
57  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) 
58    ret_val = smt_call_dl_theory_solver(sm, bound);
59  else
60    exit(0);
61 
62  return ret_val;
63}
64
65int 
66smt_call_dl_theory_solver(smtManager_t * sm, long bound)
67{
68  satManager_t * cm = sm->cm;
69  int needImplication;
70  int lit, avar_lit, value;
71  int i, id;
72  int num_lit = 0;
73 
74  if(cm->stackPos == 0) return(0);
75
76  smt_call_dl_theory_solver_preprocess(sm);
77
78  needImplication = 0;
79
80  /* send model to theory solver */
81  for(i = bound; i < cm->stackPos; i++) {
82    lit = cm->decisionStack[i];
83    assert(lit>1);
84    id = SATVar(lit);
85    value = cm->values[id];
86    assert(value != 2);
87   
88    if (id <= sm->avarArr->size) {
89      if (sm->avalues[id] != value) {
90        num_lit++;
91        avar_lit = (value == 1) ? id : -id;
92        sm->litArr = sat_array_insert(sm->litArr, avar_lit);
93        sm->avalues[id] = value;
94      }
95    } 
96  }
97
98  if (num_lit == 0) 
99    return needImplication;
100
101  if (SATCurLevel(cm)==0) {
102    sm->stats->num_lzero_ineq += num_lit;
103  }
104
105  needImplication = smt_theory_solve(sm);
106
107  if ((int) sm->stats->num_bf_call%200000 == 0)
108    smt_dl_report_intermediate_result(sm);
109
110  if(cm->explanation->size) { /** conflicting case **/
111
112    /**
113     * 1. add blocking clause info CNF database
114     * 2. do conflict analysis with respect to blocking clause
115     * 3. backtrack to backtracking level
116     * 4. if needImplication==0, sat && no theory implication
117     * 5. if needImplication==1, sat && theory implication
118     * 6. if needImplication==2, unsat
119     **/
120   
121    assert(cm->explanation->size>1);
122
123    if(SATCurLevel(cm) == 0) {
124      cm->status = 0;
125      return 2;
126    }
127
128    smt_fit_decision_level_wrt_blocking_clause(cm, cm->explanation); 
129#ifdef NEW_BLOCKING
130    sat_add_blocking_clause_for_theorem_prover(cm, cm->explanation);
131#else
132    c = sat_add_blocking_clause(cm, cm->explanation);
133    bLevel = sat_conflict_analysis(cm, c);
134    sat_undo(cm, bLevel);
135
136    csize = SATSizeClause(c);
137    nMarks = 0;
138    pLit = &(c->lits[0]);
139    for(i = 0; i < csize; i++) { 
140      if(cm->values[((*pLit)>>1)] == 2) {
141        nMarks++;
142        iLit = (*pLit);
143      }
144      pLit++;
145    }
146    if(nMarks > 1) {
147      c = sat_add_learned_clause(cm, cm->clearned);
148      sat_update_variable_decay(cm);
149      sat_update_clause_decay(cm);
150    }
151    else {
152      if(cm->clearned->size == 1) {
153        sat_enqueue(cm, iLit, 0);
154      }
155      else {
156        sat_enqueue(cm, iLit, c);
157      }
158    }
159#endif
160    needImplication = 2;
161  }
162 
163  return(needImplication);
164}
165
166void
167smt_call_dl_theory_solver_preprocess(smtManager_t *sm)
168{
169  satManager_t * cm = sm->cm;
170
171  sm->flag |= SAT_MASK; 
172  sm->lemma->size = 0;
173  sm->tplits->size = 0;
174  sm->cur_index = sm->litArr->size;
175 
176  if (cm->explanation == 0) cm->explanation = sat_array_alloc(8);
177  cm->explanation->size = 0;
178}
179
180int
181smt_theory_solve(smtManager_t * sm)
182{
183  int needImplication = 0;
184
185  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
186
187    if (sm->flag & MP_CONST_MASK) {
188#if 1
189      needImplication = smt_mp_dl_theory_solve(sm);
190#endif     
191    } else {     
192      if (sm->flag & IDL_MASK) 
193        needImplication = smt_idl_theory_solve(sm);
194      else if (sm->flag & RDL_MASK) 
195        needImplication = smt_rdl_theory_solve(sm);
196    }
197   
198  } else {
199    exit(0);
200  }
201   
202  return needImplication;
203}
204
205void
206smt_fit_decision_level_wrt_blocking_clause(
207  satManager_t * m, 
208  satArray_t * arr)
209{
210  long i, csize, *pLit, bLevel;
211
212  csize = arr->size;
213  pLit = &(arr->space[0]);
214  bLevel = 0;
215  for(i = 0; i < csize; i++) {
216    if(m->levels[((*pLit)>>1)] > bLevel){
217      bLevel = m->levels[((*pLit)>>1)];
218    }
219    pLit++;
220  }
221  sat_undo(m, bLevel);
222}
223
224int 
225smt_get_size_of_atomic_variable(satManager_t * cm)
226{
227  smtManager_t *sm = (smtManager_t *) cm->SMTManager;
228
229  return(sm->avarArr->size);
230}
231
232void
233smt_theory_undo(satManager_t * cm)
234{
235  smtManager_t *sm = (smtManager_t *) cm->SMTManager;
236
237  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
238    smt_dl_theory_undo(sm);
239  } else {
240    exit(0);
241  }
242}
243
244void
245smt_dl_theory_undo(smtManager_t * sm)
246{
247  satManager_t * cm = sm->cm;
248  smtGraph_t * G = sm->cG;
249  smtAvar_t * avar;
250  int lit, id;
251  int i; 
252
253  if (sm->litArr->size > 0) {
254    /*
255       init for smt_get_right_end_edge
256       ignore unassigned edges
257    */
258    G->esize = smt_get_right_end_edge_index(sm) + 1;
259  }
260
261  for(i = sm->litArr->size-1; i >= 0; i--) {
262    lit = sm->litArr->space[i];
263    id = (lit > 0) ? lit : -lit;
264
265    if(cm->values[id] != 2) { 
266      sm->litArr->size = i + 1;
267      break;
268    }
269    avar = (smtAvar_t *) sm->id2var->space[id];
270
271    /* check if avar is theory propagated */
272    if (avar->flag & TPROP_MASK || avar->flag & IMPLIED_MASK) {
273      sm->avalues[id] = 2;
274      avar->flag &= RESET_TPROP_MASK;
275      avar->flag &= RESET_IMPLIED_MASK;
276
277      if(i==0) {
278        sm->litArr->size=0;
279        break;
280      }
281      continue;
282    }
283
284    /* update constraint graph */
285    smt_update_edge_in_constraint_graph(sm, avar);
286
287    /* reset avar */
288    sm->avalues[id] = 2;   
289
290    if(i==0) { 
291      sm->litArr->size=0;
292      break;
293    }
294  }
295
296  sm->cur_index = sm->litArr->size;
297
298  return;
299}
300
301void
302smt_update_edge_in_constraint_graph(smtManager_t * sm, smtAvar_t * avar)
303{
304  satManager_t * cm = sm->cm;
305  smtGraph_t * G = sm->cG;
306  smtVertex_t * src, * dest;
307  smtAvar_t * implied, * replacing = 0;
308  smtNvar_t * lnvar, * rnvar;
309  smtEdge_t *e;
310  double iweight = 0, min_weight = 0;
311  int dest_index, src_index;
312  int id, i;
313
314  id = avar->id;
315
316  if (sm->avalues[id] == 1) {
317    lnvar = (smtNvar_t *) avar->nvars->space[0];
318    rnvar = (smtNvar_t *) avar->nvars->space[1];
319  } else {
320    assert(sm->avalues[id] == 0);
321    lnvar = (smtNvar_t *) avar->nvars->space[1];
322    rnvar = (smtNvar_t *) avar->nvars->space[0];
323  }
324 
325  src_index = rnvar->id - 1;
326  dest_index = lnvar->id - 1;
327  src = &(G->vHead[src_index]);
328  dest = &(G->vHead[dest_index]);
329  e = smt_find_edge(src, dest);
330   
331  /**
332     pick strongest implied atom for the replace
333     implied is ordered in strength
334  **/
335
336  for(i = e->implied->size-1; i >= 0; i--) {
337    implied = (smtAvar_t *) e->implied->space[i];
338    if (cm->values[implied->id] == 2) continue;
339
340    if (sm->avalues[implied->id] == 1) {
341      iweight = implied->constant;
342    } else if (sm->avalues[implied->id] == 0) {
343      iweight = -implied->constant - sm->epsilon;
344    } else
345      exit(0);
346   
347    min_weight = iweight;
348    replacing = implied;
349    e->implied->size = i;
350
351    break;     
352  }
353 
354  if (replacing == 0) { /* no assigned implied atom */
355
356    smt_delete_edge_in_constraint_graph(sm, e);
357
358  } else { /* replace edge : check replacing avar */
359
360    e->avar = replacing;
361    e->weight = min_weight;
362    e->avar->flag &= RESET_IMPLIED_MASK;
363
364  }
365 
366  return;
367}
368
369void
370smt_delete_edge_in_constraint_graph(smtManager_t * sm, smtEdge_t * e)
371{
372  smtGraph_t * G = sm->cG;
373  smtVertex_t * src, * dest;
374  smtEdge_t * rend_edge, * out, * in;
375  int size, index;
376  int i;
377
378  src = e->src;
379  dest = e->dest;
380
381  size = src->outs->size;
382
383  /* delete from outgoing edge list of src */
384  for(i = 0; i < size; i++) {
385    out = (smtEdge_t *) src->outs->space[i];
386    if (out == e) {
387      src->outs->space[i] = src->outs->space[size-1];
388      src->outs->size--;
389      break;
390    }
391  }
392
393  size = dest->ins->size;
394
395  /* delete from incoming edge list of dest */
396  for(i = 0; i < size; i++) {
397    in = (smtEdge_t *) dest->ins->space[i];
398    if (in == e) {
399      dest->ins->space[i] = dest->ins->space[size-1];
400      dest->ins->size--;
401      break;
402    }
403  }
404
405  e->implied->size = 0;
406  e->avar = 0;
407  e->weight = 0;
408
409  index = e->index;
410
411  if (index >= G->esize) return;
412  else rend_edge = smt_get_right_end_edge(sm);
413
414  /** move last edge to deleted edge location **/
415  if (rend_edge && rend_edge->index > index) {
416    smt_put_right_end_edge_to_deleted(e, rend_edge);
417    e->index = index;   
418  } 
419
420  G->esize--;
421
422  return;
423}
424
425smtEdge_t *
426smt_get_right_end_edge(smtManager_t * sm)
427{
428  satManager_t * cm = sm->cm;
429  smtGraph_t * G = sm->cG;
430  smtEdge_t * e;
431  smtAvar_t * avar;
432  int i, j;
433 
434  for(i = G->esize-1; i >= 0; i--) { 
435    e = &(G->eHead[i]);   
436    avar = e->avar;
437    if (avar && cm->values[avar->id] != 2) {
438      return e;
439    }
440
441    /* check implied list if the implied one is assigned */
442    for(j = 0; j < e->implied->size; j++) {
443      avar = (smtAvar_t *) e->implied->space[j];
444      if (sm->avalues[avar->id] != 2) {
445        return e;
446      }
447    }
448    e->implied->size = 0;
449  }   
450
451  return 0;
452}
453
454int
455smt_get_right_end_edge_index(smtManager_t * sm)
456{
457  satManager_t * cm = sm->cm;
458  smtGraph_t * G = sm->cG;
459  smtEdge_t * e;
460  smtAvar_t * avar;
461  int i, j;
462
463  for(i = G->esize-1; i >= 0; i--) {
464    e = &(G->eHead[i]);   
465    avar = e->avar;
466    if (cm->values[avar->id] != 2) {
467      return i;
468    }
469    /* check implied list if the implied one is assigned */
470    for(j = 0; j < e->implied->size; j++) {
471      avar = (smtAvar_t *) e->implied->space[j];
472      if (cm->values[avar->id] != 2) {
473        return i;
474      }
475    }
476    e->implied->size = 0;
477  }
478
479  return 0;
480}
481
482void
483smt_put_right_end_edge_to_deleted(
484  smtEdge_t * deleted, 
485  smtEdge_t * rend_edge)
486{
487  smtVertex_t * src, * dest;
488  smtEdge_t * e;
489  satArray_t * dimplied;
490  int i;
491
492  src = rend_edge->src;
493  dest = rend_edge->dest;
494
495  /* update outs of src */
496  for(i = 0; i < src->outs->size; i++) {
497    e = (smtEdge_t *) src->outs->space[i];
498    if (e == rend_edge) {
499      src->outs->space[i] = (long) deleted;
500      break;
501    }
502  }
503
504  /* update ins of dest */
505  for(i = 0; i < dest->ins->size; i++) {
506    e = (smtEdge_t *) dest->ins->space[i];
507    if (e == rend_edge) {
508      dest->ins->space[i] = (long) deleted;
509      break;
510    }
511  }
512
513  /* keep the index */
514  deleted->src = rend_edge->src;
515  deleted->dest = rend_edge->dest;
516 
517  dimplied = deleted->implied;
518  deleted->implied = rend_edge->implied;
519  rend_edge->implied = dimplied;
520
521  deleted->avar = rend_edge->avar;
522
523  deleted->weight = rend_edge->weight;
524
525  return;
526}
527
528void
529smt_add_theory_clause(
530  satManager_t * cm, 
531  smtAvar_t * avar, 
532  satArray_t * litArr)
533{
534  long i, j, v, lit;
535  long clevel;
536  int addClause, sign;
537  satClause_t * c;
538  smtManager_t * sm = (smtManager_t *) cm->SMTManager;
539
540  addClause = 0;
541  clevel = SATCurLevel(cm);
542
543  if(clevel == 0) {
544    assert(sm->avalues[avar->id] != 2);
545    if (sm->avalues[avar->id] == 0) {
546      sign = 1;
547      sat_enqueue(cm, (avar->id<<1)+sign, 0); 
548      avar->flag |= TPROP_MASK;
549      sm->litArr = sat_array_insert(sm->litArr, -avar->id);
550      sm->tplits = sat_array_insert(sm->tplits, -avar->id);
551
552    } else if (sm->avalues[avar->id] == 1){
553      sign = 0;
554      sat_enqueue(cm, (avar->id<<1)+sign, 0); 
555      avar->flag |= TPROP_MASK;
556      sm->litArr = sat_array_insert(sm->litArr, avar->id);
557      sm->tplits = sat_array_insert(sm->tplits, avar->id);
558    }
559
560    return;
561  }
562
563  for(i=j=0; i < litArr->size; i++) {
564    lit = litArr->space[i];
565    v = lit >> 1;
566    if(cm->levels[v] != 0) {
567      if(cm->levels[v] == clevel)
568        addClause = 1;
569      litArr->space[j++] = lit;
570    }
571  }
572  litArr->size -= (i-j);
573
574  if(addClause == 0 || litArr->size < 2) {
575    sm->avalues[avar->id] = 2;
576
577    return;
578  }
579
580  if (sm->avalues[avar->id] == 0) {
581    sign = 1;
582    sat_enqueue(cm, (avar->id<<1)+sign, 0); 
583    avar->flag |= TPROP_MASK;
584    sm->litArr = sat_array_insert(sm->litArr, -avar->id);
585    sm->tplits = sat_array_insert(sm->tplits, -avar->id);
586
587  } else {
588    sign = 0;
589    sat_enqueue(cm, (avar->id<<1)+sign, 0); 
590    avar->flag |= TPROP_MASK;
591    sm->litArr = sat_array_insert(sm->litArr, avar->id);
592    sm->tplits = sat_array_insert(sm->tplits, avar->id);
593  }
594
595  c = sat_add_theory_clause(cm, litArr);
596
597  cm->antes[avar->id] = c;
598
599  return;
600}
601
602#endif
Note: See TracBrowser for help on using the repository browser.