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

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

cusp added
File size: 64.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [smtCnf.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
49void
50smt_generate_cnf_main(smtManager_t * sm)
51{
52  int num_bvar, is_cnf = 0;
53
54  sm->num_var = sm->id2var->size - 1; /* id2var starts from index 1 */
55
56  is_cnf = smt_generate_cnf(sm);
57 
58  num_bvar = sm->bvarArr->size;
59
60  if (is_cnf == 0) {
61    smt_free_clauses(sm->clsArr);
62    sm->clsArr->size = 0;
63    fprintf(stdout, "SMT Formula is not in CNF format\n");
64    smt_generate_cnf_with_aig(sm);
65
66    if (sm->obj == Aig_One || sm->obj == Aig_Zero) return;
67
68  } else {
69    sm->flag |= CNF_MASK;
70  }
71
72  sm->stats->num_inter_bvar = sm->bvarArr->size - num_bvar;
73
74  return;
75}
76
77int
78smt_generate_cnf(smtManager_t * sm)
79{
80  smtFml_t * root = sm->fml;
81  smtFml_t * fml, * subfml;
82  smtQueue_t * Q;
83  int is_leaf, is_cnf = 1;
84  int i;
85
86  smt_init_generate_cnf(sm);
87
88  Q = smt_create_queue(sm->fmlArr->size);
89
90  smt_enqueue(Q, (long) root);
91 
92  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {
93    is_leaf = smt_is_abstract_leaf_fml(fml);
94
95    if (is_leaf) {
96      smt_create_clause_with_fml(sm, fml);
97    } else if (fml->type == NOT_c) {
98      subfml = (smtFml_t *) fml->subfmlArr->space[0];
99      is_leaf = smt_is_abstract_leaf_fml(subfml);
100      if (is_leaf) {
101        smt_create_clause_with_fml(sm, fml);
102      } else {
103        subfml->nNeg++; 
104        if (!(subfml->flag & QUEUED_MASK)) {
105          smt_enqueue(Q, (long) subfml);
106          subfml->flag |= QUEUED_MASK;
107        }
108      }
109    } else if (fml->type == OR_c || fml->type == IMP_c || fml->type == IFF_c) {
110      is_cnf = smt_create_clause_with_fml(sm, fml);
111      if (!is_cnf) {
112        smt_none();
113        break;
114      }
115    } else if (fml->type == AND_c) {
116
117      if ((fml->nNeg) % 2 != 0) {
118#if 0
119        is_cnf = 0;
120        break;
121#else
122        is_cnf = smt_create_clause_with_fml(sm, fml); 
123
124        if (is_cnf == 0) {
125          smt_none();
126          break; 
127        }
128        continue; /* clause is generated : reached leaf */
129#endif
130      }
131
132      for(i = 0; i < fml->subfmlArr->size; i++) {
133        subfml = (smtFml_t *) fml->subfmlArr->space[i];
134        if (subfml->nNeg != 0 && ((subfml->nNeg) % 2 != (fml->nNeg) % 2)) {
135          /* Neg # dismatch between multiple parent nodes */
136          is_cnf = 0;
137          smt_none();
138          break;
139        }
140        subfml->nNeg = fml->nNeg;
141       
142        if (!(subfml->flag & QUEUED_MASK)) {
143          smt_enqueue(Q, (long) subfml);
144          subfml->flag |= QUEUED_MASK;
145        }       
146      }
147      if (is_cnf==0) {
148        smt_none();
149        break;
150      }
151    } else {
152      smt_none();
153      is_cnf = 0;
154      break;
155    }
156  }
157
158  smt_free_queue(Q);
159 
160  return is_cnf;
161}
162
163
164#if 1
165void
166smt_generate_cnf_with_aig(smtManager_t * sm)
167{
168  sm->obj = smt_generate_aig(sm);   
169
170#if 0
171  smt_print_aig_to_dot_file(sm->bm);
172#endif
173
174  if (sm->obj == Aig_One || sm->obj == Aig_Zero) 
175    return; 
176
177  smt_convert_aig_into_cnf(sm, sm->obj);
178
179  return;
180}
181
182
183AigEdge_t
184smt_generate_aig(smtManager_t * sm)
185{
186  Aig_Manager_t * bm;
187  smtFml_t * root = 0, * fml = 0;
188  smtFml_t * subfml_a, * subfml_b, * subfml_c;
189  smtAvar_t * avar;
190  smtBvar_t * bvar;
191  AigEdge_t aig_node = Aig_NULL, cond = Aig_NULL;
192  AigEdge_t left = Aig_NULL, right = Aig_NULL;
193  satArray_t * fmlArr;
194  array_t * aig_nodeArr;
195  int i, nfml;
196  char * name; 
197   
198  bm = Aig_initAig(6000);
199 
200  sm->bm = bm;
201
202  root = sm->fml;
203
204  if (root == 0) {
205    return Aig_NULL;
206  }
207   
208  fmlArr = smt_sort_formula_in_bfs_manner(sm, root);
209
210  nfml = fmlArr->size;
211 
212  /* start from leaf formula to root formula */
213  for(i = nfml - 1; i >= 0; i--) {
214    fml = (smtFml_t *) fmlArr->space[i];
215   
216    if (fml->flag & TRUE_MASK) {
217      aig_node = Aig_One;
218
219    } else if (fml->flag & FALSE_MASK) {
220      aig_node = Aig_Zero;
221
222    } else if (fml->type == PRED_c || fml->type == FVAR_c) {
223      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
224      name = util_strsav((char *) subfml_a);
225      aig_node = Aig_FindNodeByName(bm, name);
226     
227      if (aig_node == Aig_NULL) {
228        aig_node = Aig_CreateVarNode(bm, name);
229        bvar = fml->bvar;
230        bvar->aig_node = aig_node;
231      } else { 
232        free(name);
233      }
234
235    } else if (fml->type == NOT_c) {
236      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
237      if (subfml_a->aig_node != Aig_NULL)
238        aig_node = Aig_Not(subfml_a->aig_node);
239      else
240        exit(0);
241    } else if (fml->type == IMP_c) {
242      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
243      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
244      if (subfml_a->aig_node != Aig_NULL)
245        left = subfml_a->aig_node;
246      else
247        exit(0);
248     
249      if (subfml_b->aig_node != Aig_NULL)
250        right = subfml_b->aig_node;
251      else
252        exit(0);
253     
254      aig_node = Aig_Then(bm, left, right);
255    } else if (fml->type == IFF_c) {
256
257      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
258      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
259
260      if (subfml_a->aig_node != Aig_NULL)
261        left = subfml_a->aig_node;
262      else
263        exit(0);
264     
265      if (subfml_b->aig_node != Aig_NULL)
266        right = subfml_b->aig_node;
267      else
268        exit(0);
269     
270      aig_node = Aig_Eq(bm, left, right);
271#if 0 
272      /* only iff fml with leaf children : bug */
273      if ( Aig_isVarNode(bm, left) && Aig_isVarNode(bm, right) )
274        sm->iff_fmlArr = sat_array_insert(sm->iff_fmlArr, (long) fml);
275#endif
276    } else if (fml->type == AND_c) {
277      aig_nodeArr = smt_gather_aig_node_from_formula_array(fml->subfmlArr);
278      aig_node = Aig_AndsInBFSManner(bm, aig_nodeArr);
279      array_free(aig_nodeArr);
280
281    } else if (fml->type == OR_c) {
282      aig_nodeArr = smt_gather_aig_node_from_formula_array(fml->subfmlArr);
283      aig_node = Aig_OrsInBFSManner(bm, aig_nodeArr);
284      array_free(aig_nodeArr);
285
286    } else if (fml->type == XOR_c) {
287      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
288      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
289     
290      if (subfml_a->aig_node != Aig_NULL)
291        left = subfml_a->aig_node;
292      else
293        exit(0);
294     
295      if (subfml_b->aig_node != Aig_NULL)
296        right = subfml_b->aig_node;
297      else
298        exit(0);
299     
300      aig_node = Aig_Xor(bm, left, right);
301
302    } else if (fml->type == NAND_c) {
303      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
304      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
305      if (subfml_a->aig_node != Aig_NULL)
306        left = subfml_a->aig_node;
307      else
308        exit(0);
309     
310      if (subfml_b->aig_node != Aig_NULL)
311        right = subfml_b->aig_node;
312      else
313        exit(0);
314     
315      aig_node = Aig_Nand(bm, left, right);
316
317    } else if (fml->type == ITE_c) {
318      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
319      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
320      subfml_c = (smtFml_t *) fml->subfmlArr->space[2];
321     
322      if (subfml_a->aig_node != Aig_NULL)
323        cond = subfml_a->aig_node;
324      else
325        exit(0);
326     
327      if (subfml_b->aig_node != Aig_NULL)
328        left = subfml_b->aig_node;
329      else
330        exit(0);
331     
332      if (subfml_c->aig_node != Aig_NULL)
333        right = subfml_c->aig_node;
334      else
335        exit(0);
336
337      aig_node = Aig_Ite(bm, cond, left, right);
338#if 0 /* bug */
339      is_terminal = smt_is_ite_terminal_case(cond, left, right);
340
341      if (!is_terminal)
342        sm->ite_fmlArr = sat_array_insert(sm->ite_fmlArr, (long) fml);
343#endif
344    } else if (smt_is_atom_formula(fml)) {
345
346      avar = fml->avar;
347      name = util_strsav(avar->name);
348      aig_node = Aig_FindNodeByName(bm, name);
349
350      if (aig_node == Aig_NULL) {
351        aig_node = Aig_CreateVarNode(bm, name);
352        subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
353        subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
354        avar->aig_node = aig_node;
355      } else {
356        free(name);
357      }
358
359    } else {
360      fprintf(stdout, "ERROR: No Formula type in AIG type\n");
361      fprintf(stdout, "unknown\n");
362      exit(0);
363    }
364
365    fml->aig_node = aig_node;
366  }
367
368  if (fmlArr) free(fmlArr);
369
370  aig_node = fml->aig_node;
371 
372  return aig_node;
373}
374
375int
376smt_is_ite_terminal_case(
377  AigEdge_t cond_node, 
378  AigEdge_t then_node, 
379  AigEdge_t else_node)
380{
381  AigEdge_t node_a, node_b, node_c;
382
383  if (cond_node == Aig_One || cond_node == Aig_Zero ||
384      then_node == Aig_One || then_node == Aig_Zero ||
385      else_node == Aig_One || else_node == Aig_Zero)
386    return 1;
387
388  node_a = Aig_NonInvertedEdge(cond_node);
389  node_b = Aig_NonInvertedEdge(then_node);
390  node_c = Aig_NonInvertedEdge(else_node);
391     
392  if (node_a == node_b || node_a == node_c || node_b == node_c)
393    return 1;
394
395  return 0;
396}
397
398void
399smt_convert_aig_into_cnf(smtManager_t * sm, AigEdge_t node)
400{
401  array_t * idArr = array_alloc(int, 10);;
402  int negated = 0;
403
404  smt_compute_indegree_for_aig_node(sm);
405 
406  smt_init_var_id_for_aig_node(sm);
407#if 0 /* bug */
408  /* mapping ite & iff aig_node to fml */
409  smt_check_leaf_node_for_aig_node(sm);
410#endif
411  smt_convert_aig_into_cnf_sub(sm, node, idArr, &negated);
412
413  smt_add_clause_for_object(sm, node);
414
415  smt_add_clause_for_iff_fml(sm);
416  sm->iff_fmlArr->size = 0;
417 
418  smt_add_clause_for_ite_fml(sm); 
419  sm->ite_fmlArr->size = 0;
420 
421  array_free(idArr);
422 
423  return;
424}
425
426void
427smt_compute_indegree_for_aig_node(smtManager_t * sm)
428{
429  Aig_Manager_t * bm = sm->bm;
430  AigEdge_t v, left, right;
431  int nodes_size, index;
432
433  nodes_size = bm->nodesArraySize/AigNodeSize;
434
435  sm->node2ins = (int *) malloc(sizeof(int) * nodes_size);
436
437  memset(sm->node2ins, 0, sizeof(int) * nodes_size);
438
439  for(v = AigFirstNodeIndex ; v < bm->nodesArraySize; v+=AigNodeSize){
440    left = leftChild(v);
441    right = rightChild(v); 
442   
443    if (left != Aig_NULL && left != Aig_One && left != Aig_Zero) {
444      if (Aig_IsInverted(left)) left = Aig_NonInvertedEdge(left);
445      assert(left);
446      index = AigNodeID(left) - 1;
447      sm->node2ins[index]++;
448    }
449
450    if (right != Aig_NULL && right != Aig_One && right != Aig_Zero) {
451      if (Aig_IsInverted(right)) right = Aig_NonInvertedEdge(right);
452      assert(right);
453      index = AigNodeID(right) - 1;
454      sm->node2ins[index]++;
455    }
456  }
457 
458  return;
459}
460
461void
462smt_init_var_id_for_aig_node(smtManager_t * sm)
463{
464  Aig_Manager_t * bm = sm->bm;
465  AigEdge_t node;
466  smtAvar_t * avar;
467  smtBvar_t * bvar;
468  int nodes_size, index, i;
469
470  nodes_size = bm->nodesArraySize/AigNodeSize;
471
472  sm->node2id = (int *) malloc(sizeof(int) * nodes_size);
473
474  memset(sm->node2id, 0, sizeof(int) * nodes_size);
475
476  sm->aig_zero_id = INT_MAX - 2;
477 
478  sm->aig_one_id = INT_MAX - 1; 
479 
480  sm->aig_none = INT_MAX;
481
482  /* var id for avar */
483  for(i = 0; i < sm->avarArr->size; i++) {
484    avar = (smtAvar_t *) sm->avarArr->space[i];
485    node = avar->aig_node;
486#if 1
487    if (node == Aig_NULL) continue;
488#endif
489    assert(node != Aig_NULL); /* node may not be assigned due to ite red */
490    index = AigNodeID(node) - 1;
491    sm->node2id[index] = avar->id;
492  }
493
494  /* var id for bvar */
495  for(i = 0; i < sm->bvarArr->size; i++) {
496    bvar = (smtBvar_t *) sm->bvarArr->space[i];
497    node = bvar->aig_node;
498    assert(node != Aig_NULL || bvar->flag & BTRUE_MASK || 
499           bvar->flag & BFALSE_MASK);
500    if (!node) continue;
501    index = AigNodeID(node) - 1;
502    sm->node2id[index] = bvar->id;
503  }
504}
505
506void
507smt_check_leaf_node_for_aig_node(smtManager_t * sm)
508{
509  Aig_Manager_t * bm = sm->bm;
510  AigEdge_t node;
511  smtFml_t * ite_fml, * iff_fml;
512  /* satArray_t * ite_fmlArr, * iff_fmlArr; */
513  int nodes_size, index, i;
514
515  nodes_size = bm->nodesArraySize/AigNodeSize;
516
517  sm->node2fml = (smtFml_t **) malloc(sizeof(smtFml_t *) * nodes_size);
518
519  memset(sm->node2fml, 0, sizeof(smtFml_t *) * nodes_size);
520
521  /* check ite node as a leaf node in aig */
522  for(i = 0; i < sm->ite_fmlArr->size; i++) {
523    ite_fml = (smtFml_t *) sm->ite_fmlArr->space[i];
524    node = ite_fml->aig_node;
525    if (node == Aig_One || node == Aig_Zero) continue;
526    assert(node != Aig_NULL); 
527    index = AigNodeID(node) - 1;
528    if (sm->node2fml[index] == 0) sm->node2fml[index] = ite_fml;
529  }
530
531  /* check iff node as a leaf node in aig */
532  for(i = 0; i < sm->iff_fmlArr->size; i++) {
533    iff_fml = (smtFml_t *) sm->iff_fmlArr->space[i];
534    node = iff_fml->aig_node;
535    if (node == Aig_One || node == Aig_Zero) continue;
536    assert(node != Aig_NULL); 
537    index = AigNodeID(node) - 1;
538    if (sm->node2fml[index] == 0) sm->node2fml[index] = iff_fml;
539  }
540
541  sm->ite_fmlArr->size = 0;
542  sm->iff_fmlArr->size = 0;
543}
544
545satArray_t *
546smt_sort_formula_in_bfs_manner(smtManager_t * sm, smtFml_t * root)
547{
548  smtFml_t * fml, * tfml;
549  smtQueue_t * Q;
550  satArray_t * fmlArr = sat_array_alloc(1024);
551  int i, is_leaf, id;
552
553  smt_compute_indegree_in_formula(sm);
554
555  Q = smt_create_queue(sm->fmlArr->size);
556 
557  /* id = sm->avarArr->size + sm->bvarArr->size + 1; */
558  id = sm->id2var->size;
559  root->id = id;
560  fmlArr = sat_array_insert(fmlArr, (long) root);
561
562  smt_enqueue(Q, (long) root);
563   
564  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {
565
566      is_leaf = smt_is_abstract_leaf_fml(fml);
567
568    if ( (!is_leaf) ) {
569      for(i = 0; i < fml->subfmlArr->size; i++) {
570        tfml = (smtFml_t *) fml->subfmlArr->space[i];
571        tfml->ins--;
572
573        if (tfml->ins <= 0) {
574          if (!tfml->avar && !tfml->bvar) {
575            /* intermediate variable */
576            id++;
577            tfml->id = id;
578            smt_enqueue(Q, (long) tfml);
579          } else {
580            if (tfml->bvar) tfml->id = tfml->bvar->id;
581            else if (tfml->avar) tfml->id = tfml->avar->id;
582            else exit(0);
583          } 
584          fmlArr = sat_array_insert(fmlArr, (long) tfml);
585        }
586      }
587    }
588  }
589
590  if(Q) smt_free_queue(Q);
591
592  return fmlArr;
593}
594
595void
596smt_compute_indegree_in_formula(smtManager_t * sm)
597{
598  smtFml_t * root, * fml, * tfml;
599  smtQueue_t * Q;
600  int i, is_leaf;
601 
602  for(i = 0; i < sm->fmlArr->size; i++) {
603    tfml = (smtFml_t *) sm->fmlArr->space[i];
604    tfml->ins = 0; 
605  }
606 
607  Q = smt_create_queue(sm->fmlArr->size);
608
609  root = sm->fml;
610 
611  smt_enqueue(Q, (long) root);
612
613  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {
614   
615    is_leaf = smt_is_abstract_leaf_fml(fml);
616
617    if ( (!is_leaf) ) {
618      for(i = 0; i < fml->subfmlArr->size; i++) {
619        tfml = (smtFml_t *) fml->subfmlArr->space[i];
620        if (tfml->ins == 0) {
621          smt_enqueue(Q, (long) tfml);
622        }
623        tfml->ins++;
624      }
625    }
626  }
627
628  if(Q) smt_free_queue(Q);
629
630  return;
631}
632
633array_t *
634smt_gather_aig_node_from_formula_array(satArray_t * fmlArr)
635{
636  smtFml_t * tfml;
637  int i;
638  array_t * aig_nodeArr = array_alloc(AigEdge_t, fmlArr->size);
639
640  for(i = 0; i < fmlArr->size; i++) {
641    tfml = (smtFml_t *) fmlArr->space[i];
642    array_insert_last(AigEdge_t, aig_nodeArr, tfml->aig_node);   
643  }
644
645  return aig_nodeArr;
646}
647
648int
649smt_convert_aig_into_cnf_sub(
650  smtManager_t * sm,
651  AigEdge_t node,
652  array_t * idArr, /* contains conjuncts in big AND */
653  int * negated)
654{
655  Aig_Manager_t * bm = sm->bm;
656  AigEdge_t left, right;
657  int var_id, lvar_id, rvar_id;
658  int cur_index;
659 
660  assert(node != Aig_One && node != Aig_Zero);
661
662  if (Aig_IsInverted(node)) {
663    *negated = 1;
664    node = Aig_NonInvertedEdge(node);
665    return -1 * smt_convert_aig_into_cnf_sub(sm, node, idArr, negated);
666  }
667
668  if (smt_add_var_id_for_node(sm, node, &var_id, negated)){
669    return var_id; /* node is a leaf or already visited */
670  }
671
672  cur_index = idArr->num; /* save current idx in idArr */
673
674  left = leftChild(node);
675  right = rightChild(node);
676 
677  /* get left child var id */
678  if (left == Aig_One) 
679    lvar_id = sm->aig_one_id;
680  else if (left == Aig_Zero)
681    lvar_id = sm->aig_zero_id;
682  else
683    lvar_id = smt_convert_aig_into_cnf_sub(sm, left, idArr, negated);
684
685  /* right child var id */
686  if (right == Aig_One)
687    rvar_id = sm->aig_one_id;
688  else if (right == Aig_Zero) 
689    rvar_id = sm->aig_zero_id;
690  else
691    rvar_id = smt_convert_aig_into_cnf_sub(sm, right, idArr, negated);
692   
693  if (var_id == 0) { /* no var_id for the node */
694    if (lvar_id == sm->aig_zero_id) {
695      array_insert_last(int, idArr, 0); /* obj is false */
696    } else if (lvar_id == sm->aig_one_id) {
697      /* nop */
698    } else if (lvar_id != sm->aig_none) {
699      assert(lvar_id != 0);
700      array_insert_last(int, idArr, lvar_id);
701    }
702
703    if (rvar_id == sm->aig_zero_id) {
704      array_insert_last(int, idArr, 0); /* obj is false */
705    } else if (rvar_id == sm->aig_one_id) {
706      /* nop */
707    } else if (rvar_id != sm->aig_none) {
708      assert(rvar_id != 0);
709      array_insert_last(int, idArr, rvar_id);
710    }
711
712    return sm->aig_none;
713  } else {
714    smt_generate_clause_with_aig(sm, cur_index, var_id, 
715                                 lvar_id, rvar_id, idArr);
716   
717    return var_id;
718  }
719}
720
721int
722smt_add_var_id_for_node(
723  smtManager_t * sm,                                       
724  AigEdge_t node,
725  int * var_id,
726  int * negated)
727{
728  Aig_Manager_t * bm = sm->bm;
729  smtFml_t * fml = 0;
730  smtBvar_t * bvar;
731  int index;
732
733  index = AigNodeID(node) - 1;
734
735  /* check if node is not negated and not var node */ 
736  if ( node != sm->obj && !Aig_isVarNode(sm->bm, node) && 
737       (sm->node2fml == 0 || sm->node2fml[index] == 0) &&
738       !*negated && node != Aig_One && node != Aig_Zero && 
739       sm->node2ins[index] == 1 ) {
740
741    /* does it matter if not fanout free? */
742    *var_id = 0;  /* no new intermediate var */
743    return 0;
744
745  } 
746
747  if (*negated == 1) *negated = 0; /* reset negated flag */
748
749  if (sm->node2id[index] != 0) { 
750
751    *var_id = sm->node2id[index]; 
752    if (sm->node2fml) fml = sm->node2fml[index];
753
754    if ( node != sm->obj || Aig_isVarNode(sm->bm, node) ||
755         (sm->node2fml && fml != 0) ) { /* iff & ite case */
756      return 1; /* node is a leaf or already visited */
757    } else { 
758      /* sm->obj = ite node child : node created, but never visited */
759      return 0;
760    }
761
762  } else {
763
764    /* new intermediate var */
765    bvar = smt_create_intermediate_bool_variable(sm, node);
766    sm->node2id[index] = bvar->id; 
767    *var_id = bvar->id;
768    if (sm->node2fml) fml = sm->node2fml[index];
769
770    if ( Aig_isVarNode(bm, node) || (sm->node2fml && fml != 0) ) {
771
772      if (fml) { /* iff & ite case */
773        if (fml->type == ITE_c) 
774          sm->ite_fmlArr = sat_array_insert(sm->ite_fmlArr, (long) fml);
775        else if (fml->type == IFF_c) 
776          sm->iff_fmlArr = sat_array_insert(sm->iff_fmlArr, (long) fml);
777      }
778
779      return 1; /* iff & ite case */
780    } else
781      return 0;
782  }
783}
784
785void
786smt_generate_clause_with_aig(
787  smtManager_t * sm, 
788  int cur_index,
789  int var_id, 
790  int lvar_id, 
791  int rvar_id, 
792  array_t * idArr)
793{
794  smtCls_t * cls, * cls_a;
795  int aig_one, aig_zero, aig_none;
796  int id, i;
797
798  aig_one = sm->aig_one_id;
799  aig_zero = sm->aig_zero_id;
800  aig_none = sm->aig_none;
801
802  /** --conditions--
803      lvar_id: aig_one, aig_zero, var_id, idArr
804      rvar_id: aig_one, aig_zero, var_id, idArr
805      lvar_id == aig_one, lvar_id == aig_zero, lvar_id != 0, lvar_id == 0
806      rvar_id == aig_one, rvar_id == aig_zero, rvar_id != 0, rvar_id == 0
807  **/
808
809  if (lvar_id == aig_one && rvar_id == aig_one) {
810    /* cls:(var_id) */
811    cls = smt_create_clause();
812    cls->litArr = sat_array_insert(cls->litArr, var_id);
813    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
814
815  } else if (lvar_id == aig_one && rvar_id == aig_zero) {
816    /* cls:(-var_id) */
817    cls = smt_create_clause();
818    cls->litArr = sat_array_insert(cls->litArr, -var_id);
819    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
820
821  } else if (lvar_id == aig_one && rvar_id != aig_none) {
822    /* cls:(-rvar_id + var_id) */
823    cls = smt_create_clause();
824    cls->litArr = sat_array_insert(cls->litArr, -rvar_id);
825    cls->litArr = sat_array_insert(cls->litArr, var_id);
826    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
827    /* cls:(rvar_id + -var_id) */
828    cls = smt_create_clause();
829    cls->litArr = sat_array_insert(cls->litArr, rvar_id);
830    cls->litArr = sat_array_insert(cls->litArr, -var_id);
831    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
832
833  } else if (lvar_id == aig_one && rvar_id == aig_none && 
834             !(rvar_id == aig_one || rvar_id == aig_zero)) { 
835    assert(idArr->num >= cur_index);
836    cls_a = smt_create_clause();
837
838    for(i = cur_index; i < idArr->num; i++) {   
839      id = array_fetch(int, idArr, i);
840      /* cls set1: var_id -> (r1 * r2)  */
841      cls = smt_create_clause();
842      cls->litArr = sat_array_insert(cls->litArr, id);
843      cls->litArr = sat_array_insert(cls->litArr, -var_id);
844      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
845      /* clasue set2: -var_id -> (-r1 + -r2) */
846      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
847    }
848    idArr->num = cur_index;
849    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
850    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);
851
852  } else if (lvar_id == aig_zero) {
853    /* cls:(-var_id) */
854    cls = smt_create_clause();
855    cls->litArr = sat_array_insert(cls->litArr, -var_id);
856    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
857
858  }  else if (lvar_id == aig_none && rvar_id == aig_one && 
859             !(lvar_id == aig_one || lvar_id == aig_zero)) {
860    assert(idArr->num >= cur_index);
861    cls_a = smt_create_clause();
862
863    for(i = cur_index; i < idArr->num; i++) {   
864      id = array_fetch(int, idArr, i);
865      /* cls set1: var_id -> (l1 * l2)  */
866      cls = smt_create_clause();
867      cls->litArr = sat_array_insert(cls->litArr, id);
868      cls->litArr = sat_array_insert(cls->litArr, -var_id);
869      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
870      /* clasue set2: -var_id -> (-l1 + -l2) */
871      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
872    }
873    idArr->num=cur_index;
874    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
875    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);
876
877  } else if (lvar_id == aig_none && rvar_id == aig_zero &&
878             !(lvar_id == aig_one || lvar_id == aig_zero)) {
879    /* cls:(-var_id) */
880    cls = smt_create_clause();
881    cls->litArr = sat_array_insert(cls->litArr, -var_id);
882    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
883
884  } else if (lvar_id == aig_none && rvar_id != aig_none &&
885           !(lvar_id == aig_one || lvar_id == aig_zero)) {
886    assert(idArr->num >= cur_index);
887    cls_a = smt_create_clause();
888    for(i = cur_index; i < idArr->num; i++) {   
889      id = array_fetch(int, idArr, i);
890      /* cls set1: var_id -> ((l1 * l2) * rvar_id)  */
891      cls = smt_create_clause();
892      cls->litArr = sat_array_insert(cls->litArr, id);
893      cls->litArr = sat_array_insert(cls->litArr, -var_id);
894      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
895      /* clasue set2: -var_id -> ((-l1 + -l2) + -rvar_id)*/
896      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
897    }
898    idArr->num = cur_index;
899    /* cls set1: var_id -> ((l1 * l2) * rvar_id)  */
900    cls = smt_create_clause();
901    cls->litArr = sat_array_insert(cls->litArr, rvar_id);
902    cls->litArr = sat_array_insert(cls->litArr, -var_id);
903    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
904    /* clasue set2: -var_id -> ((-l1 + -l2) + -rvar_id)*/
905    cls_a->litArr = sat_array_insert(cls_a->litArr, -rvar_id);
906    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
907    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);
908
909  } else if (lvar_id == aig_none && rvar_id == aig_none && 
910             !(lvar_id == aig_one || lvar_id == aig_zero) && 
911             !(rvar_id == aig_one || rvar_id == aig_zero)) {
912    assert(idArr->num >= cur_index);
913    cls_a = smt_create_clause();
914    for(i = cur_index; i < idArr->num; i++) {   
915      id = array_fetch(int, idArr, i);
916      /* cls set1: var_id -> ((l1 * l2) * (r1 * r2))  */
917      cls = smt_create_clause();
918      cls->litArr = sat_array_insert(cls->litArr, id);
919      cls->litArr = sat_array_insert(cls->litArr, -var_id);
920      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
921      /* clasue set2: -var_id -> ((-l1 + -l2) + (-r1 + -r2))*/
922      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
923    }
924    idArr->num = cur_index;
925    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
926    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);
927
928  } else if (lvar_id != aig_none && rvar_id == aig_one) {
929    /* cls:(-lvar_id + var_id) */
930    cls = smt_create_clause();
931    cls->litArr = sat_array_insert(cls->litArr, -lvar_id);
932    cls->litArr = sat_array_insert(cls->litArr, var_id);
933    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
934    /* cls:(lvar_id + -var_id) */
935    cls = smt_create_clause();
936    cls->litArr = sat_array_insert(cls->litArr, lvar_id);
937    cls->litArr = sat_array_insert(cls->litArr, -var_id);
938    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
939
940  } else if (lvar_id != aig_none && rvar_id == aig_zero) {
941    /* cls:(-var_id) */
942    cls = smt_create_clause();
943    cls->litArr = sat_array_insert(cls->litArr, -var_id);
944    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
945
946  } else if (lvar_id != aig_none && rvar_id == aig_none &&
947             !(rvar_id == aig_one || rvar_id == aig_zero)) {
948    assert(idArr->num >= cur_index);
949    cls_a = smt_create_clause();
950    for(i = cur_index; i < idArr->num; i++) {   
951      id = array_fetch(int, idArr, i);
952      /* cls set1: var_id -> ((r1 * r2) * lvar_id)  */
953      cls = smt_create_clause();
954      cls->litArr = sat_array_insert(cls->litArr, id);
955      cls->litArr = sat_array_insert(cls->litArr, -var_id);
956      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
957      /* clasue set2: -var_id -> ((-r1 + -r2) + -lvar_id)*/
958      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
959    }
960    idArr->num = cur_index;
961    /* cls set1: var_id -> ((r1 * r2) * lvar_id)  */
962    cls = smt_create_clause();
963    cls->litArr = sat_array_insert(cls->litArr, lvar_id);
964    cls->litArr = sat_array_insert(cls->litArr, -var_id);
965    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
966    /* clasue set2: -var_id -> ((-r1 + -r2) + -lvar_id)*/
967    cls_a->litArr = sat_array_insert(cls_a->litArr, -lvar_id);
968    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
969    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);
970
971  }  else if (lvar_id != aig_none && rvar_id != aig_none) {
972    /* cls set1: -var_id -> (-lvar_id + -rvar_id) */
973    cls = smt_create_clause();
974    cls->litArr = sat_array_insert(cls->litArr, -lvar_id);
975    cls->litArr = sat_array_insert(cls->litArr, -rvar_id);
976    cls->litArr = sat_array_insert(cls->litArr, var_id);
977    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
978    /* cls set2: var_id -> (lvar_id * rvar_id) */
979    cls = smt_create_clause();
980    cls->litArr = sat_array_insert(cls->litArr, lvar_id);
981    cls->litArr = sat_array_insert(cls->litArr, -var_id);
982    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
983 
984    cls = smt_create_clause();
985    cls->litArr = sat_array_insert(cls->litArr, rvar_id);
986    cls->litArr = sat_array_insert(cls->litArr, -var_id);
987    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
988
989  } else {
990    smt_none();
991    fprintf(stdout, "ERROR: WRONG AIG TO CNF\n");
992    exit(0);
993  }
994}
995
996void
997smt_add_clause_for_object(smtManager_t * sm, AigEdge_t obj)
998{
999  smtCls_t * cls;
1000  int index, id, lit;
1001
1002  index = AigNodeID(obj) - 1;
1003
1004  id = sm->node2id[index];
1005
1006  if(Aig_IsInverted(obj)) lit = -id;
1007  else lit = id;
1008
1009  cls = smt_create_clause();
1010
1011  cls->litArr = sat_array_insert(cls->litArr, lit);
1012
1013  sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1014}
1015
1016void
1017smt_add_clause_for_iff_fml(smtManager_t * sm)
1018{
1019  smtFml_t * fml, * subfml_a, * subfml_b;
1020  smtBvar_t * bvar;
1021  array_t * idArr = array_alloc(int, 10);;
1022  AigEdge_t iff_node, node_a, node_b, obj;
1023  int i, index, negated;
1024  int x, y, f;
1025
1026  obj = sm->obj; /* save obj : sm->obj is temporally used for iff child */
1027 
1028  for(i = 0; i < sm->iff_fmlArr->size; i++) {
1029    fml = (smtFml_t *) sm->iff_fmlArr->space[i];
1030    subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
1031    subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
1032
1033    iff_node = fml->aig_node;
1034    node_a = subfml_a->aig_node;
1035    node_b = subfml_b->aig_node;
1036    assert(iff_node != Aig_NULL);
1037    assert(node_a != Aig_NULL);
1038    assert(node_b != Aig_NULL);
1039
1040    /* iff: f */
1041    index = AigNodeID(iff_node) - 1;
1042    f = sm->node2id[index]; 
1043    if (f == 0) {
1044      /* nested iff fml: new intermediate var */
1045      bvar = smt_create_intermediate_bool_variable(sm, iff_node);
1046      f = bvar->id;
1047      sm->node2id[index] = f; 
1048    }
1049
1050    /* child_a: x */
1051    if (node_a == Aig_One) 
1052      x = sm->aig_one_id;
1053    else if (node_a == Aig_Zero)
1054      x = sm->aig_zero_id;
1055    else {
1056      index = AigNodeID(node_a) - 1;
1057      x = sm->node2id[index]; 
1058
1059      if (x == 0) {
1060        idArr->num = 0;
1061        negated = 0;
1062        sm->obj = Aig_NonInvertedEdge(node_a);
1063        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1064        x = sm->node2id[index]; 
1065        assert(x);
1066      }
1067
1068      if (Aig_IsInverted(node_a)) 
1069        x = -x;
1070    }
1071   
1072    /* child_b: y */
1073    if (node_b == Aig_One) 
1074      y = sm->aig_one_id;
1075    else if (node_b == Aig_Zero)
1076      y = sm->aig_zero_id;
1077    else {
1078      index = AigNodeID(node_b) - 1;
1079      y = sm->node2id[index]; 
1080
1081      if (y == 0) {
1082        idArr->num = 0;
1083        negated = 0;
1084        sm->obj = Aig_NonInvertedEdge(node_b);
1085        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1086        y = sm->node2id[index]; 
1087        assert(y);
1088      }
1089     
1090      if (Aig_IsInverted(node_b)) 
1091        y = -y;
1092    }
1093
1094    smt_add_clause_for_iff_fml_sub(sm, f, x, y); 
1095  }
1096
1097  sm->obj = obj; /* restore obj */
1098  array_free(idArr);
1099
1100  return;
1101}
1102
1103void
1104smt_add_clause_for_iff_fml_sub(smtManager_t * sm, int f, int x, int y)
1105{
1106  smtCls_t * cls;
1107
1108  /* (f -> (x = y)) /\ (f' -> (x = y)') */
1109 
1110  if ((x == sm->aig_one_id && y == sm->aig_one_id) ||
1111      (x == sm->aig_zero_id && y == sm->aig_zero_id)) {
1112    /* (f) */
1113    cls = smt_create_clause();
1114    cls->litArr = sat_array_insert(cls->litArr, f);
1115
1116  } else if ((x == sm->aig_one_id && y == sm->aig_zero_id) ||
1117             (x == sm->aig_zero_id && y == sm->aig_one_id)) {
1118    /* (f') */
1119    cls = smt_create_clause();
1120    cls->litArr = sat_array_insert(cls->litArr, -f);
1121
1122  } else if (x == sm->aig_one_id) {
1123    /* (f' \/ y) */
1124    cls = smt_create_clause();
1125    cls->litArr = sat_array_insert(cls->litArr, -f);
1126    cls->litArr = sat_array_insert(cls->litArr, y);
1127    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1128    /* (f \/ y') */
1129    cls = smt_create_clause();
1130    cls->litArr = sat_array_insert(cls->litArr, f);
1131    cls->litArr = sat_array_insert(cls->litArr, -y);
1132    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1133
1134  } else if (x == sm->aig_zero_id) {
1135    /* (f' \/ y') */
1136    cls = smt_create_clause();
1137    cls->litArr = sat_array_insert(cls->litArr, -f);
1138    cls->litArr = sat_array_insert(cls->litArr, -y);
1139    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1140    /* (f \/ x \/ y) */
1141    cls = smt_create_clause();
1142    cls->litArr = sat_array_insert(cls->litArr, f);
1143    cls->litArr = sat_array_insert(cls->litArr, y);
1144    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1145
1146  } else if (y == sm->aig_one_id) {
1147    /* (f' \/ x) */
1148    cls = smt_create_clause();
1149    cls->litArr = sat_array_insert(cls->litArr, -f);
1150    cls->litArr = sat_array_insert(cls->litArr, x);
1151    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1152    /* (f \/ x') */
1153    cls = smt_create_clause();
1154    cls->litArr = sat_array_insert(cls->litArr, f);
1155    cls->litArr = sat_array_insert(cls->litArr, -x);
1156    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1157
1158  } else if (y == sm->aig_zero_id) {
1159    /* (f' \/ x') */
1160    cls = smt_create_clause();
1161    cls->litArr = sat_array_insert(cls->litArr, -f);
1162    cls->litArr = sat_array_insert(cls->litArr, -x);
1163    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1164    /* (f \/ x) */
1165    cls = smt_create_clause();
1166    cls->litArr = sat_array_insert(cls->litArr, f);
1167    cls->litArr = sat_array_insert(cls->litArr, x);
1168    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1169
1170  } else {
1171    /* (f' \/ x' \/ y) */
1172    cls = smt_create_clause();
1173    cls->litArr = sat_array_insert(cls->litArr, -f);
1174    cls->litArr = sat_array_insert(cls->litArr, -x);
1175    cls->litArr = sat_array_insert(cls->litArr, y);
1176    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1177    /* (f' \/ x \/ y') */
1178    cls = smt_create_clause();
1179    cls->litArr = sat_array_insert(cls->litArr, -f);
1180    cls->litArr = sat_array_insert(cls->litArr, x);
1181    cls->litArr = sat_array_insert(cls->litArr, -y);
1182    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1183    /* (f \/ x' \/ y') */
1184    cls = smt_create_clause();
1185    cls->litArr = sat_array_insert(cls->litArr, f);
1186    cls->litArr = sat_array_insert(cls->litArr, -x);
1187    cls->litArr = sat_array_insert(cls->litArr, -y);
1188    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1189    /* (f \/ x \/ y) */
1190    cls = smt_create_clause();
1191    cls->litArr = sat_array_insert(cls->litArr, f);
1192    cls->litArr = sat_array_insert(cls->litArr, x);
1193    cls->litArr = sat_array_insert(cls->litArr, y);
1194    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1195  }
1196
1197  return;
1198}
1199
1200void
1201smt_add_clause_for_iff_children(
1202  smtManager_t * sm, 
1203  AigEdge_t node_a, 
1204  AigEdge_t node_b)
1205{
1206  Aig_Manager_t  * bm = sm->bm;
1207  array_t * idArr = array_alloc(int, 10);
1208  int index, negated;
1209
1210  /* generate cnf for subfmls of ite fml */
1211
1212  if (node_a != Aig_NULL && node_a != Aig_One && node_a != Aig_Zero) {
1213    idArr->num = 0;
1214    negated = 0;
1215    index = AigNodeID(node_a) - 1;
1216    sm->obj = Aig_NonInvertedEdge(node_a);
1217#if 1
1218    if ( !Aig_isVarNode(bm, sm->obj) && sm->node2fml[index] == 0 &&
1219         sm->obj != Aig_One && sm->obj != Aig_Zero )
1220      smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1221#endif
1222  }
1223
1224  if (node_b != Aig_NULL && node_b != Aig_One && node_b != Aig_Zero) {
1225    idArr->num = 0;
1226    negated = 0;
1227    index = AigNodeID(node_b) - 1;
1228    sm->obj = Aig_NonInvertedEdge(node_b);
1229#if 1
1230    if ( !Aig_isVarNode(bm, sm->obj) && sm->node2fml[index] == 0 &&
1231         sm->obj != Aig_One && sm->obj != Aig_Zero )
1232      smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1233#endif
1234  }
1235
1236  array_free(idArr);
1237
1238  return;
1239}
1240
1241void
1242smt_add_clause_for_ite_fml(smtManager_t * sm)
1243{
1244  /* require checking aig_one & aig_zero */
1245  smtFml_t * fml, * subfml_a, * subfml_b, * subfml_c;
1246  array_t * idArr = array_alloc(int, 10);
1247  AigEdge_t ite_node, node_a, node_b, node_c, obj;
1248  int x, y, z, f;
1249  int i, index, negated;
1250 
1251  obj = sm->obj; /* save obj : sm->obj is temporally used for ite child */
1252
1253  for(i = 0; i < sm->ite_fmlArr->size; i++) {
1254    fml = (smtFml_t *) sm->ite_fmlArr->space[i];
1255    subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
1256    subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
1257    subfml_c = (smtFml_t *) fml->subfmlArr->space[2];
1258
1259    ite_node = fml->aig_node;
1260    node_a = subfml_a->aig_node;
1261    node_b = subfml_b->aig_node;
1262    node_c = subfml_c->aig_node;
1263    assert(ite_node != Aig_NULL);
1264    assert(node_a != Aig_NULL);
1265    assert(node_b != Aig_NULL);
1266    assert(node_c != Aig_NULL);
1267
1268    /* ite: f */
1269    if (ite_node == Aig_One || ite_node == Aig_Zero) continue;
1270    index = AigNodeID(ite_node) - 1;
1271    f = sm->node2id[index];
1272
1273    assert(f);
1274
1275    /* child_a: x */
1276    if (node_a == Aig_One) 
1277      x = sm->aig_one_id;
1278    else if (node_a == Aig_Zero)
1279      x = sm->aig_zero_id;
1280    else {
1281      index = AigNodeID(node_a) - 1;
1282      x = sm->node2id[index]; 
1283
1284      if (x == 0) {
1285#if 1
1286        idArr->num = 0;
1287        negated = 0;
1288        sm->obj = Aig_NonInvertedEdge(node_a);
1289        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1290        x = sm->node2id[index]; 
1291        assert(x);
1292#endif
1293      }
1294     
1295      if (Aig_IsInverted(node_a)) 
1296        x = -x;
1297    }
1298
1299    /* child_b: y */
1300    if (node_b == Aig_One) 
1301      y = sm->aig_one_id;
1302    else if (node_b == Aig_Zero)
1303      y = sm->aig_zero_id;
1304    else {
1305      index = AigNodeID(node_b) - 1;
1306      y = sm->node2id[index]; 
1307     
1308      if (y == 0) {
1309#if 1
1310        idArr->num = 0;
1311        negated = 0;
1312        sm->obj = Aig_NonInvertedEdge(node_b);
1313        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1314        y = sm->node2id[index]; 
1315        assert(y);
1316#endif
1317      }
1318     
1319      if (Aig_IsInverted(node_b)) 
1320        y = -y;
1321    }
1322
1323    /* child_c: z */
1324    if (node_c == Aig_One) 
1325      z = sm->aig_one_id;
1326    else if (node_c == Aig_Zero)
1327      z = sm->aig_zero_id;
1328    else {
1329      index = AigNodeID(node_c) - 1;
1330      z = sm->node2id[index]; 
1331      if (z == 0) {
1332#if 1
1333        idArr->num = 0;
1334        negated = 0;
1335        sm->obj = Aig_NonInvertedEdge(node_c);
1336        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1337        z = sm->node2id[index]; 
1338        assert(z);
1339#endif
1340      }
1341     
1342      if (Aig_IsInverted(node_c)) 
1343        z = -z;
1344    }
1345
1346    /*fprintf(stdout, "aig=%ld x=%d y=%d z=%d f=%d\n",
1347      fml->aig_node, x, y, z, f);*/
1348
1349    smt_add_clause_for_ite_fml_sub(sm, x, y, z, f);
1350  }
1351
1352  sm->obj = obj; /* restore obj */
1353  array_free(idArr);
1354
1355  return;
1356}
1357
1358void
1359smt_add_clause_for_ite_fml_sub(
1360  smtManager_t * sm, 
1361  int x, 
1362  int y, 
1363  int z, 
1364  int f)
1365{
1366  smtCls_t * cls;
1367 
1368  assert(f > 0);
1369  /* f = ite (x, y, z) */
1370  if ( !smt_add_clause_for_ite_terminal_case(sm, x, y, z, f) ) {
1371
1372    assert(x != sm->aig_one_id && x != sm->aig_zero_id);
1373    assert(y != sm->aig_one_id && y != sm->aig_zero_id);
1374    assert(z != sm->aig_one_id && z != sm->aig_zero_id);
1375    assert(f != sm->aig_one_id && f != sm->aig_zero_id);
1376
1377    /* ((x /\ y) -> f); */
1378    cls = smt_create_clause();
1379    cls->litArr = sat_array_insert(cls->litArr, f);
1380    cls->litArr = sat_array_insert(cls->litArr, -x);
1381    cls->litArr = sat_array_insert(cls->litArr, -y);
1382    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1383    /* ((x /\ y') -> f'); */
1384    cls = smt_create_clause();
1385    cls->litArr = sat_array_insert(cls->litArr, -f);
1386    cls->litArr = sat_array_insert(cls->litArr, -x);
1387    cls->litArr = sat_array_insert(cls->litArr, y);
1388    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1389    /* ((x' /\ z) -> f) */
1390    cls = smt_create_clause();
1391    cls->litArr = sat_array_insert(cls->litArr, f);
1392    cls->litArr = sat_array_insert(cls->litArr, x);
1393    cls->litArr = sat_array_insert(cls->litArr, -z);
1394    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1395    /* ((x' /\ z') -> f') */
1396    cls = smt_create_clause();
1397    cls->litArr = sat_array_insert(cls->litArr, -f);
1398    cls->litArr = sat_array_insert(cls->litArr, x);
1399    cls->litArr = sat_array_insert(cls->litArr, z);
1400    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1401  }
1402
1403  return;
1404}
1405
1406int
1407smt_add_clause_for_ite_terminal_case(
1408  smtManager_t * sm, 
1409  int x, 
1410  int y, 
1411  int z, 
1412  int f)
1413{
1414  smtCls_t * cls = 0;
1415
1416  assert( (x >= -sm->num_var && x <= sm->num_var) || 
1417          x == sm->aig_one_id || x == sm->aig_zero_id );
1418  assert( (y >= -sm->num_var && y <= sm->num_var) || 
1419          y == sm->aig_one_id || y == sm->aig_zero_id);
1420  assert( (z >= -sm->num_var && z <= sm->num_var) || 
1421          z == sm->aig_one_id || z == sm->aig_zero_id);
1422  assert( (f >= -sm->num_var && f <= sm->num_var) || 
1423          f == sm->aig_one_id || f == sm->aig_zero_id);
1424
1425  /* if (f == x || f == -x || f == y || f == -y || f == z || f == -z)
1426     return 1; */
1427
1428  if ( (x == sm->aig_one_id && y == sm->aig_one_id) ||
1429       (x == sm->aig_zero_id && z == sm->aig_zero_id) ||
1430       (y == sm->aig_one_id && z == sm->aig_one_id) ) { 
1431    /* (f); */
1432    cls = smt_create_clause();
1433    cls->litArr = sat_array_insert(cls->litArr, f);
1434    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1435
1436  } else if ( (x == sm->aig_one_id && y == sm->aig_zero_id) || 
1437              (x == sm->aig_zero_id && z == sm->aig_one_id) ||
1438              (y == sm->aig_zero_id && z == sm->aig_zero_id) ) { 
1439    /* (-f); */
1440    cls = smt_create_clause();
1441    cls->litArr = sat_array_insert(cls->litArr, -f);
1442    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1443
1444  } else if ( x == sm->aig_one_id ) {
1445    /* (f <-> y); */
1446    cls = smt_create_clause();
1447    cls->litArr = sat_array_insert(cls->litArr, -f);
1448    cls->litArr = sat_array_insert(cls->litArr, y);
1449    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1450    cls = smt_create_clause();
1451    cls->litArr = sat_array_insert(cls->litArr, f);
1452    cls->litArr = sat_array_insert(cls->litArr, -y);
1453    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1454
1455  } else if ( x == sm->aig_zero_id ) {
1456    /* (f <-> z); */
1457    cls = smt_create_clause();
1458    cls->litArr = sat_array_insert(cls->litArr, -f);
1459    cls->litArr = sat_array_insert(cls->litArr, z);
1460    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1461    cls = smt_create_clause();
1462    cls->litArr = sat_array_insert(cls->litArr, f);
1463    cls->litArr = sat_array_insert(cls->litArr, -z);
1464    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1465
1466  } else if ( y == sm->aig_one_id && z == sm->aig_zero_id ) {
1467    /* (f <-> x); */
1468    cls = smt_create_clause();
1469    cls->litArr = sat_array_insert(cls->litArr, -f);
1470    cls->litArr = sat_array_insert(cls->litArr, x);
1471    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1472    cls = smt_create_clause();
1473    cls->litArr = sat_array_insert(cls->litArr, f);
1474    cls->litArr = sat_array_insert(cls->litArr, -x);
1475    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1476
1477  } else if ( y == sm->aig_zero_id && z == sm->aig_one_id ) {
1478    /* (f <-> -x); */
1479    cls = smt_create_clause();
1480    cls->litArr = sat_array_insert(cls->litArr, -f);
1481    cls->litArr = sat_array_insert(cls->litArr, -x);
1482    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1483    cls = smt_create_clause();
1484    cls->litArr = sat_array_insert(cls->litArr, f);
1485    cls->litArr = sat_array_insert(cls->litArr, x);
1486    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1487
1488  } else if (y == sm->aig_one_id) {
1489    /* (f <-> (x \/ z)) */
1490    /* (f -> (x \/ z)) */
1491    cls = smt_create_clause();
1492    cls->litArr = sat_array_insert(cls->litArr, -f);
1493    cls->litArr = sat_array_insert(cls->litArr, x);
1494    cls->litArr = sat_array_insert(cls->litArr, z);
1495    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1496    /* (-f -> -x) /\ (-f -> -z) */
1497    cls = smt_create_clause();
1498    cls->litArr = sat_array_insert(cls->litArr, f);
1499    cls->litArr = sat_array_insert(cls->litArr, -x);
1500    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1501    cls = smt_create_clause();
1502    cls->litArr = sat_array_insert(cls->litArr, f);
1503    cls->litArr = sat_array_insert(cls->litArr, -z);
1504    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1505
1506  } else if (y == sm->aig_zero_id) {
1507    /* (f <-> (-x /\ z)) */
1508    /* (f -> -x) /\ (f -> z) */
1509    cls = smt_create_clause();
1510    cls->litArr = sat_array_insert(cls->litArr, -f);
1511    cls->litArr = sat_array_insert(cls->litArr, -x);
1512    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1513    cls = smt_create_clause();
1514    cls->litArr = sat_array_insert(cls->litArr, -f);
1515    cls->litArr = sat_array_insert(cls->litArr, z);
1516    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1517
1518    /* (-f -> (x \/ -z)) */
1519    cls = smt_create_clause();   
1520    cls->litArr = sat_array_insert(cls->litArr, f);
1521    cls->litArr = sat_array_insert(cls->litArr, x);
1522    cls->litArr = sat_array_insert(cls->litArr, -z);
1523    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1524
1525  } else if (z == sm->aig_one_id) {
1526    /* (f <-> (-x \/ y)) */
1527    /* (f -> (-x \/ y)) */
1528    cls = smt_create_clause();
1529    cls->litArr = sat_array_insert(cls->litArr, -f);
1530    cls->litArr = sat_array_insert(cls->litArr, -x);
1531    cls->litArr = sat_array_insert(cls->litArr, y);
1532    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1533    /* (-f -> x) /\ (-f -> -y) */
1534    cls = smt_create_clause();
1535    cls->litArr = sat_array_insert(cls->litArr, f);
1536    cls->litArr = sat_array_insert(cls->litArr, x);
1537    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1538    cls = smt_create_clause();
1539    cls->litArr = sat_array_insert(cls->litArr, f);
1540    cls->litArr = sat_array_insert(cls->litArr, -y);
1541    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1542
1543  } else if (z == sm->aig_zero_id) {
1544    /* (f <-> (x /\ y)) */
1545    /* (f -> x) /\ (f -> y) */
1546    cls = smt_create_clause();
1547    cls->litArr = sat_array_insert(cls->litArr, -f);
1548    cls->litArr = sat_array_insert(cls->litArr, x);
1549    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1550    cls = smt_create_clause();
1551    cls->litArr = sat_array_insert(cls->litArr, -f);
1552    cls->litArr = sat_array_insert(cls->litArr, y);
1553    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1554    /* (-f -> (-x \/ -y)) */
1555    cls = smt_create_clause();
1556    cls->litArr = sat_array_insert(cls->litArr, f);
1557    cls->litArr = sat_array_insert(cls->litArr, -x);
1558    cls->litArr = sat_array_insert(cls->litArr, -y);
1559    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1560  }
1561
1562  if (cls) return 1;
1563  else return 0;
1564}
1565
1566void
1567smt_add_clause_for_ite_children(
1568  smtManager_t * sm, 
1569  AigEdge_t node_a, 
1570  AigEdge_t node_b, 
1571  AigEdge_t node_c)
1572{
1573  array_t * idArr = array_alloc(int, 10);
1574  int negated;
1575
1576  /* generate cnf for subfmls of ite fml */
1577  if (node_a != Aig_NULL && node_a != Aig_One && node_a != Aig_Zero) {
1578    idArr->num = 0;
1579    negated = 0;
1580    sm->obj = Aig_NonInvertedEdge(node_a);
1581    smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1582  }
1583   
1584  if (node_b != Aig_NULL && node_b != Aig_One && node_b != Aig_Zero) {
1585    idArr->num = 0;
1586    negated = 0;
1587    sm->obj = Aig_NonInvertedEdge(node_b);
1588    smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1589  }
1590
1591  if (node_c != Aig_NULL && node_c != Aig_One && node_c != Aig_Zero) {
1592    idArr->num = 0;
1593    negated = 0;
1594    sm->obj = Aig_NonInvertedEdge(node_c);
1595    smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
1596  }
1597
1598  array_free(idArr);
1599
1600  return;
1601}
1602
1603void
1604smt_add_clause_for_ite_chain_fml_main(smtManager_t * sm)
1605{
1606  smtFml_t * fml;
1607  int i;
1608 
1609  for(i = 0; i < sm->ite_fmlArr->size; i++) {
1610    fml = (smtFml_t *) sm->ite_fmlArr->space[i];
1611    smt_add_clause_for_ite_chain_fml(sm, fml);
1612  }
1613
1614  return;
1615}
1616
1617void
1618smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml)
1619{
1620  smtFml_t * tfml, * subfml_a, * subfml_b, * subfml_c;
1621  smtQueue_t * Q;
1622  satArray_t * condsArr = 0, * thensArr = 0;
1623  satArray_t * conds = 0, * thens = 0, * elses = 0;
1624  int num_fml = sm->fmlArr->size;
1625
1626  assert(fml->type == ITE_c); /* ite(cond, then, else) */
1627
1628  condsArr = sat_array_alloc(10);
1629  thensArr = sat_array_alloc(10);
1630
1631  Q = smt_create_queue(sm->fmlArr->size);
1632 
1633  smt_enqueue(Q, (long) fml);
1634   
1635  while( (tfml = (smtFml_t *) smt_dequeue(Q)) ) {
1636
1637    subfml_a = (smtFml_t *) tfml->subfmlArr->space[0];
1638    subfml_b = (smtFml_t *) tfml->subfmlArr->space[1];
1639    subfml_c = (smtFml_t *) tfml->subfmlArr->space[2];
1640   
1641    if (subfml_a->type == AND_c) { /* cond : leaf or AND */
1642      conds = smt_get_conjunct_in_fml(subfml_a, num_fml);
1643     
1644    } else if (smt_is_abstract_leaf_fml(subfml_a)) {
1645      conds = sat_array_alloc(4);
1646
1647      if (subfml_a->bvar)
1648        conds = sat_array_insert(conds, (long) subfml_a->bvar->id);
1649      else
1650        conds = sat_array_insert(conds, (long) subfml_a->avar->id);     
1651    } 
1652   
1653    condsArr = sat_array_insert(condsArr, (long) conds);
1654   
1655    if (subfml_b->type == AND_c) { /* then : leaf or AND */
1656      thens = smt_get_conjunct_in_fml(subfml_b, num_fml);
1657     
1658    } else if (smt_is_abstract_leaf_fml(subfml_b)) {
1659      thens = sat_array_alloc(4);
1660
1661      if (subfml_b->bvar)
1662        thens = sat_array_insert(thens, (long) subfml_b->bvar->id);
1663      else
1664        thens = sat_array_insert(thens, (long) subfml_b->avar->id);     
1665    } 
1666
1667    thensArr = sat_array_insert(thensArr, (long) thens);
1668
1669    /* then : ITE or leaf or AND */
1670    if (subfml_c->type == AND_c) { 
1671      elses = smt_get_conjunct_in_fml(subfml_c, num_fml);
1672     
1673    } else if (smt_is_abstract_leaf_fml(subfml_c)) {
1674      elses = sat_array_alloc(4);
1675
1676      if (subfml_c->bvar)
1677        elses = sat_array_insert(elses, (long) subfml_c->bvar->id);
1678      else
1679        elses = sat_array_insert(elses, (long) subfml_c->avar->id);
1680     
1681    } else if (subfml_c->type == ITE_c) {
1682      smt_enqueue(Q, (long) subfml_c);
1683    } 
1684  }
1685
1686  smt_add_clause_for_ite_chain_fml_sub(sm, fml, condsArr, thensArr, elses);
1687     
1688  if (Q) smt_free_queue(Q);
1689  if (conds) free(conds);
1690  if (thens) free(thens);
1691  if (elses) free(elses);
1692}
1693
1694satArray_t *
1695smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml)
1696{ 
1697  smtFml_t * subfml_a, * tfml;
1698  smtQueue_t * Q;
1699  satArray_t * cjtArr = sat_array_alloc(4);
1700  int is_leaf, i;
1701
1702  assert(fml->type == AND_c);
1703
1704  Q = smt_create_queue(num_fml);
1705 
1706  smt_enqueue(Q, (long) fml);
1707   
1708  while( (tfml = (smtFml_t *) smt_dequeue(Q)) ) {
1709
1710    is_leaf = smt_is_abstract_leaf_fml(tfml);
1711
1712    if (!is_leaf) {
1713
1714      assert(tfml->type == AND_c);
1715
1716      for(i = 0; i < tfml->subfmlArr->size; i++) {
1717        subfml_a = (smtFml_t *) tfml->subfmlArr->space[i];
1718        smt_enqueue(Q, (long) subfml_a);
1719      }
1720
1721    } else {
1722
1723      if (tfml->bvar)
1724        cjtArr = sat_array_insert(cjtArr, (long) tfml->bvar->id);
1725      else
1726        cjtArr = sat_array_insert(cjtArr, (long) tfml->avar->id);
1727
1728    }
1729  }
1730
1731  smt_free_queue(Q);
1732
1733  return cjtArr;
1734}
1735
1736/**Function********************************************************************
1737
1738  Synopsis    []
1739
1740  Description [ e.g.
1741  z = ite (a, b, ite (c, d, ite (e, f, g)))
1742 
1743  ((a /\ b) -> z) /\ ((a /\ b') -> z')) /       \
1744  ((a' /\ c /\ d) -> z) /\ ((a' /\ c /\ d') -> z')) /\
1745  ((a' /\ c' /\ e /\ f) -> z) /\ ((a' /\ c' /\ e /\ f') -> z')) /\
1746  ((a' /\ c' /\ e' /\ g) -> z) /\ ((a' /\ c' /\ e' /\ g') -> z'))
1747
1748  a, b, c, d, e, f, g can be either a lit or ANDs.
1749  ]
1750
1751  SideEffects []
1752
1753  SeeAlso     []
1754
1755******************************************************************************/
1756
1757void
1758smt_add_clause_for_ite_chain_fml_sub(
1759  smtManager_t * sm, 
1760  smtFml_t * ite_fml,
1761  satArray_t * condsArr, 
1762  satArray_t * thensArr, 
1763  satArray_t * elses)
1764{
1765  AigEdge_t ite_node;
1766  smtCls_t * cls;
1767  satArray_t * conds, * thens;
1768  int z, cond_id, then_id, else_id;
1769  int num_comb, index;
1770  int i, j, k;
1771
1772  ite_node = ite_fml->aig_node;
1773  assert(ite_node != Aig_NULL);
1774  index = AigNodeID(ite_node) - 1;
1775  z = sm->node2id[index]; /* ite: z */
1776 
1777  /* ((conds /\ thens) -> z) */
1778  for(i = 0; i < condsArr->size; i++) {
1779   
1780    cls = smt_create_clause();
1781    conds = (satArray_t *) condsArr->space[i];
1782   
1783    for(j = 0; j < conds->size; j++) {
1784      cond_id = (int) conds->space[j];
1785      cls->litArr = sat_array_insert(cls->litArr, (long) -cond_id);
1786    }
1787
1788    thens = (satArray_t *) thensArr->space[i];
1789   
1790    for(j = 0; j < thens->size; j++) {
1791      then_id = (int) thens->space[j];
1792      cls->litArr = sat_array_insert(cls->litArr, (long) -then_id);
1793    }
1794
1795    cls->litArr = sat_array_insert(cls->litArr, (long) z);
1796    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1797  }
1798
1799  /* ((conds /\ thens') -> z') */
1800  for(i = 0, num_comb = 1; i < condsArr->size; i++) {
1801
1802    conds = (satArray_t *) condsArr->space[i];
1803    thens = (satArray_t *) thensArr->space[i];
1804
1805    num_comb = num_comb * (int) conds->size;
1806   
1807    for(j = 0; j < thens->size; j++) {
1808      cls = smt_create_clause();
1809      then_id = (int) thens->space[j];
1810      cls->litArr = sat_array_insert(cls->litArr, (long) then_id);
1811   
1812      for(k = 0; k < conds->size; k++) {
1813        cond_id = (int) conds->space[k];
1814        cls->litArr = sat_array_insert(cls->litArr, (long) -cond_id);
1815      }
1816
1817      cls->litArr = sat_array_insert(cls->litArr, (long) -z);
1818      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1819    }     
1820  }
1821
1822#if 0 /* complete ite conversion : generate too many clauses
1823         contain bug
1824       */
1825
1826  /* ((conds' /\ elses) -> z) */
1827  for(i = 0; i < num_comb; i++) {
1828    cls = smt_create_clause();
1829   
1830    for(j = 0, index = i; j < condsArr->size; j++) {
1831      conds = (satArray_t *) condsArr->space[j];
1832      quo = index / conds->size;
1833      rem = index % conds->size;
1834      cond_id = (int) conds->space[rem];
1835      cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
1836      index = quo;
1837    }
1838
1839    for(j = 0; j < elses->size; j++) {
1840      else_id = (int) elses->space[j];
1841      cls->litArr = sat_array_insert(cls->litArr, (long) -else_id);
1842    }
1843
1844    cls->litArr = sat_array_insert(cls->litArr, (long) z);
1845    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1846  }
1847
1848  /* ((conds' /\ elses') -> z') */ 
1849  for(i = 0; i < num_comb; i++) {
1850
1851    for(j = 0; j < elses->size; j++) {
1852      cls = smt_create_clause();
1853
1854      for(k = 0, index = i; k < condsArr->size; k++) {
1855        conds = (satArray_t *) condsArr->space[k];
1856        quo = index / conds->size;
1857        rem = index % conds->size;
1858        cond_id = (int) conds->space[rem];
1859        cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
1860        index = quo;
1861      }
1862
1863      else_id = (int) elses->space[j];
1864      cls->litArr = sat_array_insert(cls->litArr, (long) else_id);
1865      cls->litArr = sat_array_insert(cls->litArr, (long) -z);
1866      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1867    }   
1868  }
1869
1870#else /* assumption : conditions are all disjoint */
1871  conds = (satArray_t *) condsArr->space[condsArr->size-1];
1872
1873  /* ((conds' /\ elses) -> z) */
1874  for(i = 0; i < conds->size; i++) {
1875    cls = smt_create_clause();
1876    cond_id = (int) conds->space[i];
1877    cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
1878   
1879    for(j = 0; j < elses->size; j++) {
1880      else_id = (int) elses->space[j];
1881      cls->litArr = sat_array_insert(cls->litArr, (long) -else_id);
1882    }
1883   
1884    cls->litArr = sat_array_insert(cls->litArr, (long) z);
1885    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1886  } 
1887
1888  /* ((conds' /\ elses') -> z') */
1889  for(i = 0; i < conds->size; i++) {
1890    cond_id = (int) conds->space[i];
1891   
1892    for(j = 0; j < elses->size; j++) {
1893      else_id = (int) elses->space[j];
1894
1895      cls = smt_create_clause();
1896      cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
1897      cls->litArr = sat_array_insert(cls->litArr, (long) else_id);
1898      cls->litArr = sat_array_insert(cls->litArr, (long) -z);
1899      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1900    }
1901  }
1902#endif
1903
1904  return;
1905}
1906
1907#endif
1908
1909void
1910smt_init_generate_cnf(smtManager_t * sm)
1911{
1912  smtFml_t * fml;
1913  int i;
1914
1915  for(i = 0; i < sm->fmlArr->size; i++) {
1916    fml = (smtFml_t *) sm->fmlArr->space[i];
1917    fml->flag &= RESET_QUEUED_MASK;
1918    fml->nNeg = 0;
1919  }
1920}
1921
1922int
1923smt_create_clause_with_fml(smtManager_t * sm, smtFml_t * fml)
1924{
1925  smtCls_t * cls = 0;
1926  smtFml_t * subfml;
1927  array_t * cjts;
1928  int is_cls, is_true;
1929  int is_cnf = 1;
1930
1931  cjts = array_alloc(int, 4);
1932
1933  /* fml type : leaf, not leaf, or, imply, iff */
1934
1935  if (smt_is_atom_formula(fml) || smt_is_boolean_formula(fml)) {
1936    /* atom fml || bool fml */
1937    cls = smt_create_clause();
1938    is_true = smt_put_lit_to_clause(cls, fml);
1939    if (is_true == 1) {
1940      free(cls->litArr);
1941      free(cls);
1942    } else if (is_true == 0) {
1943      fprintf(stdout, "unsat : unit clause with (false) exists\n");
1944      exit(0);
1945    } else 
1946      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1947
1948  } else if (fml->type == NOT_c) { /* not fml */
1949    cls = smt_create_clause();
1950    subfml = (smtFml_t *) fml->subfmlArr->space[0];
1951    subfml->nNeg++;
1952    is_true = smt_put_lit_to_clause(cls, subfml); /* right? */
1953    if (is_true == 1) {
1954      free(cls->litArr);
1955      free(cls);
1956    } else if (is_true == 0) {
1957      fprintf(stdout, "unsat : unit clause with (false) exists\n");
1958      exit(0);
1959    } else 
1960      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1961    subfml->nNeg--;
1962       
1963  } else if (fml->type == AND_c && ((fml->nNeg) % 2 != 0)) { /* not and fml */
1964    cls = smt_create_clause();
1965    /* gather lits from or fml */
1966    is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
1967   
1968    if (is_cnf) {
1969      if (cls->litArr->size)
1970        sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1971      else {
1972        free(cls->litArr);
1973        free(cls);
1974      }
1975    } else {
1976      free(cls->litArr);
1977      free(cls);
1978      is_cnf = 0;;
1979    }   
1980  } else if (fml->type == OR_c) { /* or fml */
1981    if ((fml->nNeg % 2) != 0) {
1982      array_free(cjts);
1983      return 0; /* may need to handle later */
1984    }
1985   
1986    /* if cls created, there exists and in or fml */
1987    is_cls = smt_create_clause_with_ands_in_or_fml(sm, fml);
1988   
1989    if (!is_cls) {
1990      cls = smt_create_clause();
1991      /* gather lits from or fml */
1992      is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
1993     
1994      if (is_cnf) {
1995        if (cls->litArr->size) 
1996          sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
1997        else {
1998          free(cls->litArr);
1999          free(cls);
2000        }         
2001      } else {
2002        free(cls->litArr);
2003        free(cls);
2004        is_cnf = 0;
2005      }   
2006    }
2007  } else if (fml->type == IMP_c) { /* imp fml */
2008    if ((fml->nNeg % 2) != 0) {
2009      array_free(cjts);
2010      return 0; /* may need to handle later */   
2011    }
2012    cls = smt_create_clause();
2013    /* gather lits from or fml */
2014    is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
2015   
2016    if (is_cnf) {
2017      assert(cls->litArr->size);
2018      cls->litArr->space[0] = -cls->litArr->space[0]; /* (a -> b) <-> (a' \/ b) */
2019      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
2020    } else {
2021      free(cls->litArr);
2022      free(cls);
2023      is_cnf = 0;
2024    }   
2025  } else if (fml->type == IFF_c) { /* iff fml */
2026    if ((fml->nNeg % 2) != 0) {
2027      array_free(cjts);
2028      return 0; /* may need to handle later */   
2029    }
2030    cls = smt_create_clause(); /* (a <-> b) */
2031    /* gather lits from or fml */
2032    is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
2033   
2034    if (is_cnf) {
2035      assert(cls->litArr->size);
2036      cls->litArr->space[0] = -cls->litArr->space[0]; /* (a -> b) <-> (a' \/ b) */
2037      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
2038      /* (a' -> b') */
2039      cls = smt_create_clause();
2040      /* gather lits from or fml */
2041      smt_put_lits_to_clause(cls, fml, cjts);
2042      cls->litArr->space[1] = -cls->litArr->space[1]; /* (a' -> b') <-> (a \/ b') */
2043    } else {
2044      free(cls->litArr);
2045      free(cls);
2046      is_cnf = 0;
2047    }   
2048  }
2049
2050  if (is_cnf && cjts->num) {
2051    /* (a \/ b \/ (c /\ d)) <-> ((a \/ b \/ c) /\ (a \/ b \/ d)) */
2052    assert(cls);
2053    smt_create_clause_with_conjuncts(sm, cls, cjts);
2054  }
2055
2056  array_free(cjts);
2057
2058  return is_cnf;
2059}
2060
2061int
2062smt_put_lit_to_clause(smtCls_t * cls, smtFml_t * fml)
2063{
2064  long lit = 0;
2065
2066  if (fml->flag & TRUE_MASK) {
2067    if (fml->nNeg % 2 == 0) return 1; /* true */
2068    else return 0; /* not true */
2069
2070  } else if (fml->flag & FALSE_MASK) {
2071    if (fml->nNeg % 2 == 0) return 0; /* false */
2072    else return 1; /* not false */
2073
2074  } else if (smt_is_atom_formula(fml)) { /* atom fml */
2075    if (fml->nNeg % 2 == 0) lit = fml->avar->id;
2076    else lit = -fml->avar->id;
2077
2078  } else if (smt_is_boolean_formula(fml)) { /* bool fml */
2079    if (fml->nNeg % 2 == 0) {
2080      lit = fml->bvar->id;
2081    } else {
2082      lit = -fml->bvar->id;
2083    }
2084
2085  } else {
2086    exit(0);
2087  }
2088
2089  cls->litArr = sat_array_insert(cls->litArr, lit);
2090
2091  return 2;
2092}
2093
2094int
2095smt_put_lits_to_clause(smtCls_t * cls, smtFml_t * fml, array_t * cjts)
2096{
2097  smtFml_t * subfml, * tfml;
2098  int is_cnf = 1;
2099  int i;
2100
2101  for(i = 0; i < fml->subfmlArr->size; i++) {
2102    subfml = (smtFml_t *) fml->subfmlArr->space[i];
2103       
2104    if ((fml->nNeg) % 2 == 0) { /* OR_c, IMP_c, IFF_c */
2105      if (subfml->flag & TRUE_MASK) {
2106        cls->litArr->size = 0;
2107        break;
2108      } else if (subfml->flag & FALSE_MASK) {
2109        /* unit clause (false) : consider later */
2110        continue;
2111      } if (smt_is_atom_formula(subfml)) {
2112        cls->litArr = sat_array_insert(cls->litArr, subfml->avar->id);
2113      } else if (smt_is_boolean_formula(subfml)) {
2114        cls->litArr = sat_array_insert(cls->litArr, subfml->bvar->id);
2115      } else if (smt_is_negated_atom_formula(subfml)) {
2116        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2117        cls->litArr = sat_array_insert(cls->litArr, -tfml->avar->id);
2118      } else if (smt_is_negated_boolean_formula(subfml)) {
2119        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2120        if (tfml->flag & TRUE_MASK) continue;
2121        else if (tfml->flag & FALSE_MASK) {
2122          cls->litArr->size = 0;
2123          break;
2124        } else
2125          cls->litArr = sat_array_insert(cls->litArr, -tfml->bvar->id);
2126      } else if (subfml->type == OR_c) {
2127        is_cnf = smt_put_lits_to_clause(cls, subfml, cjts);
2128        if (is_cnf == 0)
2129          break;     
2130      } else if (subfml->type == NOT_c) {
2131        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2132        tfml->nNeg++;
2133        if (tfml->type == AND_c && ((tfml->nNeg) % 2 != 0)) {
2134          /* e.g. (a \/ (b /\ c)' \/ d) <-> (a \/ b' \/ c' \/ d) */
2135          is_cnf = smt_put_lits_to_clause(cls, tfml, cjts);
2136          if (is_cnf) tfml->nNeg--;
2137          else break;     
2138
2139        } else {
2140          is_cnf = 0;
2141          break;
2142        }
2143      } else if (subfml->type == AND_c && cjts->num == 0) {
2144        /* (a \/ b \/ (c /\ d)) <-> ((a \/ b \/ c) /\ (a \/ b \/ d)) */
2145        is_cnf = smt_gather_conjuncts_in_and_fml(subfml, cjts);
2146        if (is_cnf == 0) 
2147          break;
2148      } else {
2149        is_cnf = 0;
2150        break;
2151      }
2152    } else { /* AND_c */
2153      if (smt_is_atom_formula(subfml)) {
2154        cls->litArr = sat_array_insert(cls->litArr, -subfml->avar->id);
2155      } else if (smt_is_boolean_formula(subfml)) {
2156        cls->litArr = sat_array_insert(cls->litArr, -subfml->bvar->id);
2157      } else if (smt_is_negated_atom_formula(subfml)) {
2158        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2159        cls->litArr = sat_array_insert(cls->litArr, tfml->avar->id);
2160      } else if (smt_is_negated_boolean_formula(subfml)) {
2161        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2162        cls->litArr = sat_array_insert(cls->litArr, tfml->bvar->id);
2163      } else {
2164        is_cnf = 0;
2165        break;
2166      }
2167    }
2168  }
2169
2170  return is_cnf;
2171}
2172
2173void
2174smt_create_clause_with_conjuncts(
2175  smtManager_t * sm, 
2176  smtCls_t * cls, 
2177  array_t * cjts)
2178{
2179  smtCls_t * tcls;
2180  int i, lit;
2181
2182  tcls = cls;
2183
2184  for(i = 0; i < cjts->num; i++) {
2185    lit = array_fetch(int, cjts, i);
2186    tcls->litArr = sat_array_insert(tcls->litArr, lit);
2187    tcls = smt_duplicate_clause(cls); /* new cls */
2188    sm->clsArr = sat_array_insert(sm->clsArr, (long) tcls);
2189  }
2190
2191  return;
2192}
2193
2194int
2195smt_gather_conjuncts_in_and_fml(smtFml_t * fml, array_t * cjts)
2196{
2197  smtFml_t * subfml;
2198  int is_cnf = 1;
2199  int i;
2200
2201  for(i = 0; i < fml->subfmlArr->size; i++) {
2202    subfml = (smtFml_t *) fml->subfmlArr->space[i];
2203
2204    if (smt_is_atom_formula(subfml)) {
2205      array_insert_last(int, cjts, subfml->avar->id);
2206    } else if (smt_is_negated_atom_formula(subfml)) {
2207      subfml = (smtFml_t *) subfml->subfmlArr->space[0];
2208      array_insert_last(int, cjts, -subfml->avar->id);
2209    } else if (smt_is_boolean_formula(subfml)) {
2210      array_insert_last(int, cjts, subfml->bvar->id);
2211    } else if (smt_is_negated_boolean_formula(subfml)) {
2212      subfml = (smtFml_t *) subfml->subfmlArr->space[0];
2213      array_insert_last(int, cjts, -subfml->bvar->id);
2214    } else {
2215      is_cnf = 0;
2216      break;
2217    }
2218  }
2219
2220  return is_cnf;
2221}
2222
2223/**Function********************************************************************
2224
2225  Synopsis    []
2226
2227  Description [ e.g.
2228  (a \/ (b /\ c)) <-> ((a \/ b) /\ (a \/ c))
2229  ]
2230
2231  SideEffects []
2232
2233  SeeAlso     []
2234
2235******************************************************************************/
2236
2237int
2238smt_create_clause_with_ands_in_or_fml(smtManager_t * sm, smtFml_t * fml)
2239{
2240  smtCls_t * cls;
2241  smtFml_t * subfml, * tfml;
2242  satArray_t * litArr;
2243  array_t * cjts = 0;
2244  int cjt, lit, is_cls = 1;
2245  int i, j;
2246
2247  litArr = sat_array_alloc(10);
2248
2249  for(i = 0; i < fml->subfmlArr->size; i++) {
2250    subfml = (smtFml_t *) fml->subfmlArr->space[i];
2251
2252    if (subfml->type == AND_c) {
2253      if (cjts) {
2254        is_cls = 0;
2255        break;
2256      }
2257      /* cjts = smt_gather_conjuncts_in_and_fml(subfml); */
2258      cjts = array_alloc(int, 4);
2259      is_cls = smt_gather_conjuncts_in_and_fml(subfml, cjts);
2260      if (is_cls == 0) {
2261        array_free(cjts);
2262        cjts = 0;
2263        break;
2264      }
2265      /* if (cjts == 0) {
2266        is_cls = 0;
2267        break;
2268        }*/
2269     
2270    } else if (subfml->flag & TRUE_MASK) {
2271
2272    } else if (subfml->flag & FALSE_MASK) {
2273
2274    }
2275
2276    else if (smt_is_atom_formula(subfml)) {
2277      litArr = sat_array_insert(litArr, subfml->avar->id);
2278    } else if (smt_is_boolean_formula(subfml)) {
2279      if (subfml->flag & TRUE_MASK) {
2280        litArr->size = 0;
2281        break;
2282      } else if (subfml->flag & FALSE_MASK) {
2283        /* unit clause (false) : consider later */
2284        continue;
2285      } else
2286        litArr = sat_array_insert(litArr, subfml->bvar->id);
2287    } else if (smt_is_negated_atom_formula(subfml)) {
2288      tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2289      litArr = sat_array_insert(litArr, -tfml->avar->id);
2290    } else if (smt_is_negated_boolean_formula(subfml)) {
2291      tfml = (smtFml_t *) subfml->subfmlArr->space[0];
2292      if (tfml->flag & TRUE_MASK) {
2293        /* unit clause (false) : consider later */
2294        continue;
2295      } else if (tfml->flag & FALSE_MASK) {
2296        litArr->size = 0;
2297        break; 
2298      } else
2299        litArr = sat_array_insert(litArr, -tfml->bvar->id);
2300    } else {
2301      is_cls = 0;
2302      break;
2303    }
2304  }
2305
2306  if (is_cls == 0 || cjts == 0) {
2307    is_cls = 0;
2308    free(litArr);
2309    return is_cls;
2310  }
2311
2312  /* create clause */
2313  for(i = 0; i < cjts->num; i++) {
2314    cjt = array_fetch(int, cjts, i);
2315    cls = smt_create_clause();
2316    cls->litArr = sat_array_insert(cls->litArr, (long) cjt);
2317
2318    for(j = 0; j < litArr->size; j++) {
2319      lit = (int) litArr->space[j];
2320      cls->litArr = sat_array_insert(cls->litArr, (long) lit);
2321    }
2322    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
2323  }
2324
2325  free(litArr);
2326
2327  return is_cls;
2328}
2329
2330#endif
Note: See TracBrowser for help on using the repository browser.