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

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

cusp added

File size: 21.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [smt.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
49smtGlobalVar_t * gvar;
50
51/**Function********************************************************************
52
53  Synopsis    [Smt main function]
54 
55  Description []
56
57  SideEffects []
58
59  SeeAlso     []
60
61******************************************************************************/
62
63int
64smt_main(char * filename, int timeout, int is_model)
65{
66  smtManager_t * sm;
67  long btime, etime;
68
69  btime = util_cpu_time();
70 
71  /* read smt */
72  smt_read(filename);
73
74  /* init */
75  sm = smt_init();
76
77  if (sm == 0) {
78    free(filename);
79    return 0; /* simple aig case */
80  }
81
82  /* timeout */
83  smt_timeout(timeout);
84 
85  /* preprocess */
86  smt_preprocess(sm);
87 
88  /* solve */
89  smt_solve(sm);
90
91  etime = util_cpu_time();
92 
93  sm->stats->solve_time = (double)(etime - btime) / 1000.0;
94 
95  /* report */
96  smt_report(sm, is_model); 
97 
98  /* postprocess */
99  smt_postprocess(sm);
100
101  free(filename);
102
103  return 0;
104}
105
106
107/**Function********************************************************************
108
109  Synopsis    [Parsing function for smt file]
110 
111  Description [Parse smt file and create formula structure for the parse tree]
112
113  SideEffects []
114
115  SeeAlso     []
116
117******************************************************************************/
118
119void
120smt_read(char * str)
121{
122  FILE * fp;
123  char * filename;
124 
125  if (str) 
126    filename = strdup(str);
127  else
128    filename = 0;
129
130  if (filename) {
131    if(!(fp = fopen(filename, "r"))) {
132      fprintf(stderr, "ERROR : Can't open SMT file %s\n", filename);
133      exit(0);
134    }
135  } else {
136    if(!(fp = stdin)) {
137      fprintf(stderr, "ERROR : Can't open SMT file %s\n", filename);
138      exit(0);
139    }
140  }
141
142  gvar = (smtGlobalVar_t *) malloc(sizeof(smtGlobalVar_t));
143 
144  smt_init_global_variable(filename);
145
146  SmtFileSetup(fp);
147
148  (void) SmtYyparse();
149
150  if (gvar->fletArr->size)
151    smt_combine_root_fml_with_flet_fml();
152
153  return;
154}
155
156/**Function********************************************************************
157
158  Synopsis    [Smt structure initialization]
159   
160  Description [Initialize smt structure]
161
162  SideEffects []
163
164  SeeAlso     []
165
166******************************************************************************/
167
168smtManager_t *
169smt_init(void)
170{
171  smtManager_t * sm;
172 
173  if (gvar->flag & IDL_MASK || gvar->flag & RDL_MASK)
174    sm = smt_dl_init();
175  else {
176    fprintf(stdout, "ERROR : Unsupported logic\n");
177    exit(0);
178  }
179
180  if ( !(sm->flag & CNF_MASK) ) {
181    if (sm->obj == Aig_One || sm->obj == Aig_Zero) {
182      /* root aig is either true or false */
183      if (sm->obj == Aig_Zero) sm->flag &= RESET_SAT_MASK;
184
185      smt_report(sm, 0);
186
187      smt_postprocess(sm);
188
189      return 0;
190    }   
191  }
192
193  return sm;
194}
195
196/**Function********************************************************************
197
198  Synopsis    [Difference logic structure initialization]
199 
200  Description [Initialize difference logic structure]
201
202  SideEffects []
203
204  SeeAlso     []
205
206******************************************************************************/
207
208smtManager_t *
209smt_dl_init(void)
210{
211  smtManager_t * sm;
212 
213  sm = smt_init_manager();
214#if 1
215  smt_convert_eq_fml_to_ineq_fml(sm);
216#endif
217  smt_create_dl_atom_variable_main(sm);
218 
219  smt_init_atom_variable_values(sm);
220
221  smt_init_numerical_variable_values(sm);
222
223#if 0
224  smt_print_atomic_predicate_variable(sm);
225 
226  smt_print_boolean_variable(sm);
227
228  smt_print_flet_pair(sm);
229#endif
230
231  smt_assign_boolean_variable_id(sm); 
232
233  smt_assign_numerical_variable_id(sm);
234
235  if (sm->flag & MP_CONST_MASK) {
236    smt_mp_init(sm);
237    smt_mp_assign_atom_constants(sm);
238#if 0
239    smt_mp_print_atom_constants(sm);
240#endif
241  }
242
243  smt_generate_cnf_main(sm);
244
245  return sm;
246}
247
248/**Function********************************************************************
249
250  Synopsis    [Solving function]
251 
252  Description [Solve smt problem]
253
254  SideEffects []
255
256  SeeAlso     []
257
258******************************************************************************/
259
260void
261smt_solve(smtManager_t * sm)
262{
263  satManager_t * cm;
264
265  smt_circus_interface(sm);
266
267  cm = sm->cm;
268
269  if (cm->simplify) {
270
271    smt_assign_bool_var_flag(sm);
272
273  } 
274
275  if(cm->status == 2) {
276    sat_circus_solve(cm);
277  }
278 
279  assert(cm->status != 2);
280
281  sat_report_result(cm);
282
283  smt_check_result(sm);
284}
285
286/**Function********************************************************************
287
288  Synopsis    [Result reporting function]
289 
290  Description [Print result of smt problem]
291
292  SideEffects []
293
294  SeeAlso     []
295
296******************************************************************************/
297
298void
299smt_report(smtManager_t * sm, int is_model)
300{
301  /* smt_check_result(sm); -> smt_solve */
302
303  smt_report_result(sm, is_model);
304}
305
306/**Function********************************************************************
307
308  Synopsis    [Post process]
309 
310  Description [Free global variable structure and smt structure]
311
312  SideEffects []
313
314  SeeAlso     []
315
316******************************************************************************/
317
318void
319smt_postprocess(smtManager_t * sm)
320{
321  smt_free_global_variable();
322
323  smt_free_manager(sm);
324}
325
326/**Function********************************************************************
327
328  Synopsis    [Global variable initialization]
329 
330  Description [Initialize global variable]
331
332  SideEffects []
333
334  SeeAlso     []
335
336******************************************************************************/
337
338void
339smt_init_global_variable(char * filename)
340{
341  gvar->fml = 0;
342  gvar->tfml = 0;
343  gvar->nvar = 0;
344
345  gvar->fmlArr = sat_array_alloc(1000);
346  gvar->tfmlArr = sat_array_alloc(4);
347  gvar->avfmlArr = sat_array_alloc(1000);
348  gvar->bvarArr = sat_array_alloc(1000);
349  gvar->nvarArr = sat_array_alloc(1000);
350  gvar->fletArr = sat_array_alloc(1000);
351
352  gvar->epsilon = 0;
353  gvar->epsilonless = 0;
354
355  gvar->flag = 0;
356  gvar->status = 2;
357  gvar->filename = filename;
358  gvar->str = 0;
359 
360  gvar->fun_table = st_init_table(strcmp, st_strhash);
361  gvar->pred_table = st_init_table(strcmp, st_strhash);
362  gvar->fml_var_table = st_init_table(strcmp, st_strhash);
363  gvar->term_var_table = st_init_table(strcmp, st_strhash);
364  gvar->term_table = st_init_table(strcmp, st_strhash);
365  gvar->num_table = st_init_table(strcmp, st_strhash);
366}
367
368/**Function********************************************************************
369
370  Synopsis    [Global variable structure freeing function]
371 
372  Description [Free global variable structure]
373
374  SideEffects []
375
376  SeeAlso     []
377
378******************************************************************************/
379
380void
381smt_free_global_variable(void)
382{
383  if (gvar->tfmlArr)
384    free(gvar->tfmlArr);
385
386  if (gvar->fun_table)
387    st_free_table(gvar->fun_table);
388
389  if (gvar->pred_table)
390    st_free_table(gvar->pred_table);
391
392  if (gvar->fml_var_table) {
393    smt_free_key_in_table(gvar->fml_var_table);
394    st_free_table(gvar->fml_var_table);
395  }
396
397  if (gvar->term_var_table) {
398    smt_free_key_in_table(gvar->term_var_table);
399    st_free_table(gvar->term_var_table);
400  }
401
402  if (gvar->term_table)
403    st_free_table(gvar->term_table);
404
405  if (gvar->num_table) {
406    smt_free_key_in_table(gvar->num_table);
407    st_free_table(gvar->num_table);
408  }
409 
410}
411
412/**Function********************************************************************
413
414  Synopsis    [St_table key freeing function]
415 
416  Description [Free keys in st_table]
417
418  SideEffects []
419
420  SeeAlso     []
421
422******************************************************************************/
423
424void
425smt_free_key_in_table(st_table * table)
426{
427  st_generator * gen;
428  char * key;
429
430  st_foreach_item(table, gen, (char **)&key, 0) {
431    free(key);
432  }
433 
434  return;
435}
436
437/**Function********************************************************************
438
439  Synopsis    [St_table key freeing function]
440 
441  Description [Free keys and arrays in st_table]
442
443  SideEffects []
444
445  SeeAlso     []
446
447******************************************************************************/
448
449void
450smt_free_key_with_array_in_table(st_table * table)
451{
452  st_generator * gen;
453  array_t * arr;
454  char * key;
455
456  st_foreach_item(table, gen, (char **)&key, (char **)&arr) {
457    free(key);
458    array_free(arr);
459  }
460 
461  return;
462}
463
464/**Function********************************************************************
465
466  Synopsis    [Smt manager initialization]
467 
468  Description [Initialize smt manager structure]
469
470  SideEffects []
471
472  SeeAlso     []
473
474******************************************************************************/
475
476smtManager_t *
477smt_init_manager(void)
478{
479  smtManager_t * sm;
480
481  sm = (smtManager_t *) malloc(sizeof(smtManager_t));
482
483  sm->clsArr = sat_array_alloc(2000);
484  sm->la_clsArr = 0;
485  sm->avarArr = 0;
486  sm->bvarArr = gvar->bvarArr;
487  sm->nvarArr = gvar->nvarArr;
488  sm->tmp_nvars = 0;
489  sm->tab_avars = 0;
490  sm->tab_nvars = 0;
491  sm->slacks = 0;
492  sm->basics = 0;
493  sm->fmlArr = gvar->fmlArr;
494  sm->avfmlArr = gvar->avfmlArr;
495  sm->iff_fmlArr = sat_array_alloc(gvar->fmlArr->size);
496  sm->ite_fmlArr = sat_array_alloc(gvar->fmlArr->size);
497  sm->fletArr = gvar->fletArr;
498  sm->id2var = 0;
499  sm->id2slack = 0;
500  sm->node2id = 0;
501  sm->node2ins = 0;
502  sm->node2fml = 0;
503  sm->sis_table = 0;
504  sm->fml_table = st_init_table(strcmp, st_strhash);
505 
506  gvar->bvarArr = 0;
507  gvar->nvarArr = 0;
508  gvar->fmlArr = 0;
509  gvar->avfmlArr = 0;
510  gvar->fletArr = 0;
511 
512  sm->fml = gvar->fml;
513  sm->stats = smt_init_stats();
514  sm->flag = gvar->flag;
515  sm->flag |= SAT_MASK;
516 
517  gvar->fml = 0;
518  gvar->flag = 0;
519
520  if (sm->flag & IDL_MASK) {
521    sm->epsilon = 1;
522    sm->epsilonless = 0;
523  } else { /* RDL */
524    sm->epsilon = 0.000001;
525    sm->epsilonless = 0.0000001;
526  }
527
528  sm->litArr = sat_array_alloc(sm->avfmlArr->size);
529  sm->lemma = sat_array_alloc(32);
530  sm->tplits = sat_array_alloc(32);
531 
532  sm->bm = 0;
533  sm->cm = 0;
534  sm->cG = 0;
535  sm->mp = 0;
536  sm->tab = 0;
537  sm->bounds = 0;
538 
539  sm->filename = gvar->filename;
540  gvar->filename = 0;
541
542  sm->cur_index = 0;
543  sm->limit = 300;
544 
545  return sm;
546}
547
548/**Function********************************************************************
549
550  Synopsis    [Smt manager freeing function]
551 
552  Description [Free smt manager structure]
553
554  SideEffects []
555
556  SeeAlso     []
557
558******************************************************************************/
559
560void
561smt_free_manager(smtManager_t * sm)
562{
563  smt_free_clauses(sm->clsArr);
564  smt_free_atom_variables(sm->avarArr);
565  smt_free_bool_variables(sm->bvarArr);
566  smt_free_numerical_variables(sm->nvarArr);
567  smt_free_formulas(sm->fmlArr);
568 
569  if (sm->clsArr) free(sm->clsArr);
570  if (sm->avarArr) free(sm->avarArr);
571  if (sm->bvarArr) free(sm->bvarArr);
572  if (sm->nvarArr) free(sm->nvarArr);
573  if (sm->fmlArr) free(sm->fmlArr);
574  if (sm->avfmlArr) free(sm->avfmlArr);
575  if (sm->fletArr) free(sm->fletArr);
576  if (sm->iff_fmlArr) free(sm->iff_fmlArr);
577  if (sm->ite_fmlArr) free(sm->ite_fmlArr);
578  if (sm->id2var) free(sm->id2var);
579  if (sm->node2id) free(sm->node2id);
580  if (sm->node2fml) free(sm->node2fml);
581  if (sm->stats) free(sm->stats);
582  if (sm->litArr) free(sm->litArr);
583  if (sm->lemma) free(sm->lemma);
584  if (sm->tplits) free(sm->tplits);
585  if (sm->filename) free(sm->filename);
586 
587  if (sm->avalues) free(sm->avalues);
588  if (sm->ivalues) free(sm->ivalues);
589  if (sm->rvalues) free(sm->rvalues);
590  if (sm->prvalues) free(sm->prvalues);
591  if (sm->node2ins) free(sm->node2ins);
592  if (sm->sis_table) {
593    smt_free_key_with_array_in_table(sm->sis_table);
594    st_free_table(sm->sis_table); 
595  }
596  if (sm->fml_table) {
597    smt_free_key_in_table(sm->fml_table);
598    st_free_table(sm->fml_table); 
599  }
600
601  if (sm->cm) sat_free_manager(sm->cm);
602  if (sm->bm) Aig_quit(sm->bm);
603  if (sm->mp) smt_mp_free(sm->mp);
604  if (sm->cG) smt_free_constraint_graph(sm->cG);
605
606  free(sm);
607}
608
609/**Function********************************************************************
610
611  Synopsis    [Clauses freeing function]
612 
613  Description [Free clauses in clause array]
614
615  SideEffects []
616
617  SeeAlso     []
618
619******************************************************************************/
620
621void
622smt_free_clauses(satArray_t * clsArr) 
623{
624  smtCls_t * cls;
625  int i;
626
627  for(i = 0; i < clsArr->size; i++) {
628    cls = (smtCls_t *) clsArr->space[i];
629    free(cls->litArr);
630    free(cls);
631  }
632
633  return;
634}
635
636/**Function********************************************************************
637
638  Synopsis    [Atom variable freeing function]
639 
640  Description [Free atom variables in array]
641
642  SideEffects []
643
644  SeeAlso     []
645
646******************************************************************************/
647
648void
649smt_free_atom_variables(satArray_t * avarArr) 
650{
651  smtAvar_t * avar;
652  int i;
653
654  for(i = 0; i < avarArr->size; i++) {
655    avar = (smtAvar_t *) avarArr->space[i];
656    smt_free_atom_members(avar);
657    free(avar);
658  }
659
660  return;
661}
662
663/**Function********************************************************************
664
665  Synopsis    [Atom variable member freeing function]
666 
667  Description [Free atom variable members]
668
669  SideEffects []
670
671  SeeAlso     []
672
673******************************************************************************/
674
675void
676smt_free_atom_members(smtAvar_t * avar)
677{
678  free(avar->name);
679  free(avar->nvars);
680  array_free(avar->coeffs);
681 
682  return;
683}
684
685/**Function********************************************************************
686
687  Synopsis    [Boolean variable freeing function]
688 
689  Description [Free boolean variables in array]
690
691  SideEffects []
692
693  SeeAlso     []
694
695******************************************************************************/
696
697void
698smt_free_bool_variables(satArray_t * bvarArr) 
699{
700  smtBvar_t * bvar;
701  int i;
702
703  for(i = 0; i < bvarArr->size; i++) {
704    bvar = (smtBvar_t *) bvarArr->space[i];
705    free(bvar->name);
706    free(bvar);
707  }
708
709  return;
710}
711
712/**Function********************************************************************
713
714  Synopsis    [Numerical variable freeing function]
715 
716  Description [Free numerical variables in array]
717
718  SideEffects []
719
720  SeeAlso     []
721
722******************************************************************************/
723
724void
725smt_free_numerical_variables(satArray_t * nvarArr) 
726{
727  smtNvar_t * nvar;
728  int i;
729
730  for(i = 0; i < nvarArr->size; i++) {
731    nvar = (smtNvar_t *) nvarArr->space[i];
732    free(nvar->name);
733    free(nvar->avarArr);
734    free(nvar);
735  }
736
737  return;
738}
739
740/**Function********************************************************************
741
742  Synopsis    [Formula freeing function]
743 
744  Description [Free formula structure in array]
745
746  SideEffects []
747
748  SeeAlso     []
749
750******************************************************************************/
751
752void
753smt_free_formulas(satArray_t * fmlArr) 
754{
755  smtFml_t * fml;
756  int i;
757
758  for(i = 0; i < fmlArr->size; i++) {
759    fml = (smtFml_t *) fmlArr->space[i];
760    free(fml->subfmlArr);
761    free(fml);
762  }
763
764  return;
765}
766
767/**Function********************************************************************
768
769  Synopsis    [Numerical variables' values initialization]
770 
771  Description [Initialize numerical variables' values]
772
773  SideEffects []
774
775  SeeAlso     []
776
777******************************************************************************/
778
779void
780smt_init_numerical_variable_values(smtManager_t * sm)
781{
782  smtNvar_t * nvar;
783  satArray_t * new_nvarArr = sat_array_alloc(sm->nvarArr->size);
784  int i, j, size;
785
786  /* update nvarArr by checking unused nvar */
787  for(i = 0, j = 1; i < sm->nvarArr->size; i++) {
788    nvar = (smtNvar_t *) sm->nvarArr->space[i];
789    if (nvar->avarArr) {
790      nvar->id = j;
791      new_nvarArr = sat_array_insert(new_nvarArr, (long) nvar);
792      j++;
793    } else {
794      /* free(nvar) */
795    }
796  }
797
798  free(sm->nvarArr);
799  sm->nvarArr = new_nvarArr;
800
801  if (sm->flag & IDL_MASK) {
802    sm->ivalues = (int *) malloc(sizeof(int) * (sm->nvarArr->size+1));
803    memset(sm->ivalues, 0, sizeof(int)*(sm->nvarArr->size));
804    sm->rvalues = 0;
805    sm->prvalues = 0;
806  } else { /* RDL */
807    sm->ivalues = 0;
808    size = sm->nvarArr->size + 1;
809
810    /* require update : may shrink later */
811    sm->rvalues = (double *) malloc(sizeof(double) * size);
812    memset(sm->rvalues, 0, sizeof(double) * size);   
813    sm->prvalues = 0;
814  }
815 
816  return;
817}
818
819/**Function********************************************************************
820
821  Synopsis    [Statistics structure initialization]
822 
823  Description [Initialize statistics structure]
824
825  SideEffects []
826
827  SeeAlso     []
828
829******************************************************************************/
830
831smtStats_t *
832smt_init_stats(void)
833{
834  smtStats_t * stats;
835
836  stats = (smtStats_t *)malloc(sizeof(smtStats_t));
837
838  stats->solve_time = 0;
839  stats->num_bf_call = 0;
840  stats->num_bf_conf = 0;
841  stats->num_assert_call = 0;
842  stats->num_assert_conf = 0;
843  stats->num_check_call = 0;
844  stats->num_check_conf = 0;
845
846  stats->num_tprop_call = 0;
847  stats->num_tprop = 0;
848  stats->num_simp_tprop_call = 0;
849  stats->num_simp_tprop = 0;
850
851  stats->num_avar = 0;
852  stats->num_eq = 0;
853  stats->num_ceq = 0;
854  stats->num_ineq = 0;
855  stats->num_eq2ineq = 0;
856  stats->num_lzero_eq = 0;
857  stats->num_lzero_ineq = 0;
858  stats->num_inter_bvar = 0;
859  stats->num_velm_cand = 0;
860  stats->num_static_cls = 0;
861  stats->num_static_pred = 0;
862  stats->num_row = 0;
863  stats->num_col = 0;
864
865  return stats;
866}
867
868/**Function********************************************************************
869
870  Synopsis    [Smt & Sat interface]
871 
872  Description [Generate sat structure with smt structure]
873
874  SideEffects []
875
876  SeeAlso     []
877
878******************************************************************************/
879
880void
881smt_circus_interface(smtManager_t * sm)
882{
883  satManager_t * cm = sat_init_manager();
884
885  cm->SMTManager = (long *) sm;
886
887  sm->cm = cm;
888
889  cm->nClauses = sm->clsArr->size;
890
891  cm->nVars = sm->num_var;
892
893  sat_create_database(cm);
894
895  smt_circus_cnf_interface(sm);
896}
897
898/**Function********************************************************************
899
900  Synopsis    [Cnf Generating function]
901 
902  Description [Generate Cnf with smt structure]
903
904  SideEffects []
905
906  SeeAlso     []
907
908******************************************************************************/
909
910void
911smt_circus_cnf_interface(smtManager_t * sm)
912{
913  satManager_t *cm = sm->cm;
914  smtCls_t *cls;
915  satClause_t *c;
916  satArray_t *clsArr = sm->clsArr;
917  satArray_t *litArr = sat_array_alloc(100);
918  long id, lit, sign;
919  int i, j;
920
921  for(i = 0; i < clsArr->size; i++) {
922    litArr->size = 0; 
923    cls = (smtCls_t *) sm->clsArr->space[i];
924
925    for(j = 0; j < cls->litArr->size; j++) {
926      lit = cls->litArr->space[j];
927      if (lit==0) continue;
928      sign = (lit<0) ? 1 : 0;
929      id = (lit<0) ? -lit : lit;
930      litArr = sat_array_insert(litArr, ((id<<1) + sign));
931    }
932
933    c = sat_add_clause(cm, litArr, 0);
934    sat_init_variable_activity(cm, c);
935  }
936 
937#if 1
938  for(i = 1; i <= cm->nVars; i++) {
939    sat_heap_insert(cm, cm->variableHeap, i);
940  }
941#else
942  if (sm->flag & CNF_MASK) {
943    for(i = 1; i <= cm->nVars; i++) {
944      sat_heap_insert(cm, cm->variableHeap, i);
945    }
946  } else { /* somehow causes # of var reduction : no effect to efficiency */
947    satArray_t * ordered = smt_get_decision_order(sm);
948    for(i = 0; i <= ordered->size; i++) {
949      id = (int) ordered->space[i];
950      sat_heap_insert(cm, cm->variableHeap, i);
951    }
952  }
953#endif
954 
955  free(litArr);
956}
957
958/**Function********************************************************************
959
960  Synopsis    [Variable ording for sat decision]
961 
962  Description [Order variables for sat decision]
963
964  SideEffects []
965
966  SeeAlso     []
967
968******************************************************************************/
969
970satArray_t *
971smt_get_decision_order(smtManager_t * sm)
972{
973  satManager_t * cm = sm->cm;
974  smtAvar_t * avar;
975  smtBvar_t * bvar;
976  satArray_t * idArr = sat_array_alloc(sm->id2var->size);
977  int id, i;
978
979  /* bvar first order */
980  for(i = 0; i < sm->bvarArr->size; i++) {
981    bvar = (smtBvar_t *) sm->bvarArr->space[i];
982    idArr = sat_array_insert(idArr, bvar->id);
983  }
984
985  for(i = 0; i < sm->avarArr->size; i++) {
986    avar = (smtAvar_t *) sm->avarArr->space[i];
987    idArr = sat_array_insert(idArr, avar->id);
988  }
989
990  for(i = 0; i < idArr->size; i++) {
991    id = (int) idArr->space[i];
992    cm->activity[id] = (double) idArr->size-i;
993  }
994
995  return idArr;
996}
997
998#endif
Note: See TracBrowser for help on using the repository browser.