source: vis_dev/vis-2.3/src/baig/baigAllSat.c @ 101

Last change on this file since 101 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 76.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [baigAllSat.c]
4
5  PackageName [baig]
6
7  Synopsis    [Routines to check sat-based invariant checking.]
8
9  Author      [HoonSang Jin]
10
11  Copyright [ This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16
17******************************************************************************/
18
19#include "baig.h"
20#include "baigInt.h"
21#include "ntk.h"
22#include "bmc.h"
23#include "sat.h"
24
25static char rcsid[] UNUSED = "$Id: baigAllSat.c,v 1.4 2009/04/11 02:40:01 fabio Exp $";
26static satManager_t *SATcm;
27
28/*---------------------------------------------------------------------------*/
29/* Constant declarations                                                     */
30/*---------------------------------------------------------------------------*/
31
32/**AutomaticStart*************************************************************/
33
34/*---------------------------------------------------------------------------*/
35/* Static function prototypes                                                */
36/*---------------------------------------------------------------------------*/
37static int nodenameCompare( const void * node1, const void * node2);
38static int levelCompare( const void * node1, const void * node2);
39static int indexCompare( const void * node1, const void * node2);
40static int StringCheckIsInteger(char *string, int *value);
41
42/**AutomaticEnd***************************************************************/
43
44
45/*---------------------------------------------------------------------------*/
46/* Definition of exported functions                                          */
47/*---------------------------------------------------------------------------*/
48
49
50/**Function********************************************************************
51
52  Synopsis    [Create data structure for transition relation.]
53
54  Description [Create data structure for transition relation.]
55
56  SideEffects []
57
58  SeeAlso     []
59
60******************************************************************************/
61bAigTransition_t *
62bAigCreateTransitionRelation(
63        Ntk_Network_t *network,
64        mAig_Manager_t *manager)
65{
66bAigTransition_t *t;
67array_t   *bVarList, *mVarList;
68array_t *latcharr;
69Ntk_Node_t *node, *dataInput;
70mAigMvar_t mVar;
71mAigBvar_t bVar;
72st_table *node2MvfAigTable;
73lsGen gen;
74int nLatches, nInputs;
75int i, j, index, index1;
76int mAigId, maxCS;
77bAigEdge_t v;
78bAigEdge_t *cstates, *nstates, *inputs;
79
80  t = ALLOC(bAigTransition_t, 1);
81  memset(t, 0, sizeof(bAigTransition_t));
82  t->network = network;
83  t->manager = manager;
84
85  bVarList = mAigReadBinVarList(manager);
86  mVarList = mAigReadMulVarList(manager);
87
88  latcharr = array_alloc(Ntk_Node_t *, 16);
89  nLatches = 0;
90  Ntk_NetworkForEachLatch(network, gen, node) {
91    mAigId = Ntk_NodeReadMAigId(node);
92    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
93    nLatches += mVar.encodeLength;
94    array_insert_last(Ntk_Node_t *, latcharr, node);
95  }
96  t->nLatches = nLatches;
97
98  node2MvfAigTable = 
99        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
100
101  array_sort(latcharr, nodenameCompare);
102
103  cstates = ALLOC(bAigEdge_t, nLatches);
104  nstates = ALLOC(bAigEdge_t, nLatches);
105  t->tstates = ALLOC(bAigEdge_t, nLatches);
106  t->initials = ALLOC(bAigEdge_t, nLatches);
107
108  nLatches = 0;
109  maxCS = 0;
110  for(j=0; j<array_n(latcharr); j++) {
111    node = array_fetch(Ntk_Node_t *, latcharr, j);
112    mAigId = Ntk_NodeReadMAigId(node);
113    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
114    index = nLatches;
115    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
116      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
117      v = bVar.node;
118      cstates[index++] = v;
119      if(maxCS < v)
120        maxCS = v;
121    }
122
123    dataInput = Ntk_LatchReadDataInput(node);
124    mAigId = Ntk_NodeReadMAigId(dataInput);
125    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
126    index = nLatches;
127    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
128      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
129      v = bVar.node;
130      v = bAig_GetCanonical(manager, v);
131      nstates[index++] = v;
132    }
133
134    dataInput = Ntk_LatchReadInitialInput(node);
135    mAigId = Ntk_NodeReadMAigId(dataInput);
136    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
137    index = nLatches;
138    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
139      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
140      v = bVar.node;
141      v = bAig_GetCanonical(manager, v);
142      t->initials[index++] = v;
143    }
144    nLatches = index;
145  }
146
147  nInputs = 0;
148  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
149    mAigId = Ntk_NodeReadMAigId(node);
150    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
151    nInputs += mVar.encodeLength;
152  }
153  Ntk_NetworkForEachPseudoInput(network, gen, node) {
154    mAigId = Ntk_NodeReadMAigId(node);
155    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
156    nInputs += mVar.encodeLength;
157  }
158  t->nInputs = nInputs;
159
160  inputs = ALLOC(bAigEdge_t, nInputs);
161  nInputs = 0;
162  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
163    mAigId = Ntk_NodeReadMAigId(node);
164    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
165    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
166      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
167      v = bVar.node;
168      inputs[nInputs++] = v;
169    }
170  }
171  Ntk_NetworkForEachPseudoInput(network, gen, node) {
172    mAigId = Ntk_NodeReadMAigId(node);
173    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
174    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
175      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
176      v = bVar.node;
177      inputs[nInputs++] = v;
178    }
179  }
180
181  t->cstates = cstates;
182  t->nstates = nstates;
183  t->inputs = inputs;
184
185  maxCS /= bAigNodeSize;
186  maxCS++;
187  t->csize = maxCS;
188  t->cobj = ALLOC(bAigEdge_t, maxCS);
189  memset(t->cobj, 0, sizeof(bAigEdge_t)*maxCS);
190  t->c2n = ALLOC(bAigEdge_t, maxCS);
191  memset(t->c2n, 0, sizeof(bAigEdge_t)*maxCS);
192  nLatches = t->nLatches;
193  for(i=0; i<nLatches; i++) {
194    v = t->cstates[i];
195    t->c2n[SATnodeID(v)] = t->nstates[i];
196  }
197  memcpy(t->tstates, cstates, sizeof(bAigEdge_t)*t->nLatches);
198
199  t->vinputs = ALLOC(int, t->nInputs);
200  memset(t->vinputs, 0, sizeof(int)*t->nInputs);
201  t->vtstates = ALLOC(int, t->nLatches);
202  memset(t->vtstates, 0, sizeof(int)*t->nLatches);
203 
204  t->avgLits = 0;
205  t->sum = 0;
206  t->interval = 10;
207  t->period = 100;
208  array_free(latcharr);
209
210  return(t);
211}
212
213
214/**Function********************************************************************
215
216  Synopsis    [Create AIG for invariant property.]
217
218  Description [Create AIG for invariant property.]
219
220  SideEffects []
221
222  SeeAlso     []
223
224******************************************************************************/
225bAigEdge_t
226bAig_CreatebAigForInvariant(
227        Ntk_Network_t *network,
228        bAig_Manager_t *manager,
229        Ctlsp_Formula_t *inv)
230{
231bAigEdge_t result, left, right;
232st_table *nodeToMvfAigTable;
233int nodeValue;
234int check;   
235char *nodeNameString;
236char *nodeValueString;
237Ntk_Node_t *node;
238Var_Variable_t *nodeVar;
239MvfAig_Function_t  *tmpMvfAig;
240
241
242  if (inv == NIL(Ctlsp_Formula_t))      return mAig_NULL; 
243  if (inv->type == Ctlsp_TRUE_c)        return mAig_One; 
244  if (inv->type == Ctlsp_FALSE_c)       return mAig_Zero;
245
246  assert(Ctlsp_isPropositionalFormula(inv));
247
248  if (inv->type == Ctlsp_ID_c){
249    nodeNameString  = Ctlsp_FormulaReadVariableName(inv);
250    nodeValueString = Ctlsp_FormulaReadValueName(inv);
251    node = Ntk_NetworkFindNodeByName(network, nodeNameString);
252     
253    if (node == NIL(Ntk_Node_t)) {
254      fprintf(vis_stderr, "sat_inv error: Could not find node corresponding to the name\t %s\n", nodeNameString);
255      return mAig_NULL;
256    }
257
258    nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
259    if (nodeToMvfAigTable == NIL(st_table)){
260      fprintf(vis_stderr, 
261              "sat_inv error: please run build_partiton_maigs first");
262      return mAig_NULL;
263    }
264    tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
265    if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
266      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
267      array_free(tmpMvfAig);
268      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
269    }
270     
271    nodeVar = Ntk_NodeReadVariable(node);
272    if (Var_VariableTestIsSymbolic(nodeVar)) {
273      nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
274      if ( nodeValue == -1 ) {
275        fprintf(vis_stderr, 
276                "Value specified in RHS is not in domain of variable\n");
277        fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
278        return mAig_NULL;
279      }
280    }
281    else { 
282      check = StringCheckIsInteger(nodeValueString, &nodeValue);
283      if( check == 0 ) {
284        fprintf(vis_stderr,"Illegal value in the RHS\n");
285        fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
286        return mAig_NULL;
287      }
288      if( check == 1 ) {
289        fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
290        fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
291        return mAig_NULL;
292      }
293      if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
294        fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
295        fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
296        return mAig_NULL;
297      }
298    }
299    result = bAig_GetCanonical(manager,
300              MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue));
301    return result;
302  }
303
304  left = bAig_CreatebAigForInvariant(network, manager, inv->left);
305  if (left == mAig_NULL){
306    return mAig_NULL;
307  } 
308  right = bAig_CreatebAigForInvariant(network, manager, inv->right);
309
310  if (right == mAig_NULL && inv->type ==Ctlsp_NOT_c ){
311    return mAig_Not(left);
312  } 
313  else if(right == mAig_NULL) {
314    return mAig_NULL;
315  }
316
317  switch(inv->type) {
318    case Ctlsp_OR_c:
319      result = mAig_Or(manager, left, right);
320      break;
321    case Ctlsp_AND_c:
322      result = mAig_And(manager, left, right);
323      break;
324    case Ctlsp_THEN_c:
325      result = mAig_Then(manager, left, right); 
326      break;
327    case Ctlsp_EQ_c:
328      result = mAig_Eq(manager, left, right);
329      break;
330    case Ctlsp_XOR_c:
331      result = mAig_Xor(manager, left, right);
332      break;
333    default:
334      fail("Unexpected LTL type");
335  }
336  return result;
337
338}
339
340/**Function********************************************************************
341
342  Synopsis    [Compute AG.]
343
344  Description [Compute AG.]
345
346  SideEffects []
347
348  SeeAlso     []
349
350******************************************************************************/
351int
352bAigCheckInvariantWithAG(
353        bAigTransition_t *t,
354        bAigEdge_t objective)
355{
356int included, returnFlag;
357bAig_Manager_t *manager;
358satManager_t *cm;
359long frontierNodesBegin;
360
361  manager = t->manager;
362  bAigCleanUpDataFromPreviousExecution(t);
363
364  /** This is for applying SAT-based AX operation **/
365  objective = bAig_Not(objective);
366  t->objective = objective;
367  returnFlag = 0;
368
369  while(1) {
370    /**
371     * This function do nothing in the first iteration,
372     * since no frontier is provided at first.
373     * Instead of frontier, we have complemented objective at first
374     **/
375
376    if(t->verbose > 1) 
377      fprintf(vis_stdout, "** SAT_INV : %d'th pre-image is being computed\n", t->iteration+1);
378
379    frontierNodesBegin = manager->nodesArraySize;
380    if(t->iteration > 0) {
381      bAigBuildObjectiveFromFrontierSet(t);
382      if(t->frontier->num <= 1) {
383        returnFlag = 1; /** property passed **/
384        break;
385      }
386    }
387   
388    cm = bAigCirCUsInterfaceForAX(t);
389    cm->frontierNodesBegin = frontierNodesBegin;
390
391    t->allsat = cm;
392 
393
394    sat_CleanDatabase(cm);
395
396    bAigMarkConeOfInfluenceForAX(t, cm);
397
398    fflush(vis_stdout);
399
400    bAig_ComputeAX(t);
401
402    if(t->verbose > 1) {
403      sat_ReportStatistics(cm, cm->each);
404    }
405
406    included = bAigInclusionTestOnInitialStates(t);
407    if(included == 0) {
408      returnFlag = 2; /** propoerty failed **/
409    }
410
411    /** reched to convergenece **/
412    if(t->frontier->num <= 1) {
413      returnFlag = 1; /** property passed **/
414    }
415
416
417    bAig_PostProcessForAX(t, cm);
418    t->manager->nodesArraySize = frontierNodesBegin;
419    t->allsat = 0;
420
421    if(t->lifting) {
422      sat_FreeManager(t->lifting);
423      t->lifting = 0;
424    }
425
426    if(t->originalFrontier) {
427      sat_ArrayFree(t->originalFrontier);
428      t->originalFrontier = 0;
429    }
430
431    if(returnFlag) {
432      break;
433    }
434    t->iteration++;
435  } 
436
437  if(t->verbose > 0) {
438    fprintf(vis_stdout, "** SAT_INV : Total %d pre-image is computed\n", t->iteration+1);
439  }
440
441  sat_ArrayFree(t->frontier);
442  t->frontier = 0;
443  sat_ArrayFree(t->reached);
444  t->reached = 0;
445
446  fflush(vis_stdout);
447
448  return(returnFlag);
449}
450
451/**Function********************************************************************
452
453  Synopsis    [Reduce the number of blocking clauses based on UNSAT core generation.]
454
455  Description [Reduce the number of blocking clauses based on UNSAT core generation.]
456
457  SideEffects []
458
459  SeeAlso     []
460
461******************************************************************************/
462void
463bAigReduceBlockingClauseWithUnsatCore(bAigTransition_t *t)
464{
465satArray_t *cnfArray;
466satArray_t *coreArray;
467satArray_t *rootArray;
468satOption_t *option;
469satManager_t *cm;
470st_table *mappedTable;
471char filename[1024];
472int flag, i, size;
473bAigEdge_t v, nv, *plit;
474
475  cnfArray = sat_ArrayAlloc(1024);
476  mappedTable = st_init_table(st_numcmp, st_numhash);
477
478  sat_ArrayInsert(cnfArray, 0);
479  cm = t->allsat;
480  /** Collect CNF from frontier of previous run **/
481  for(v = cm->frontierNodesBegin; v<cm->frontierNodesEnd; v+= satNodeSize) {
482    if(!(SATflags(v) & IsCNFMask))      continue;
483    size = SATnumLits(v);
484    plit = (long*)SATfirstLit(v);
485    for(i=0; i<size; i++, plit++) {
486      nv = SATgetNode(*plit);
487      sat_ArrayInsert(cnfArray, nv);
488      nv = SATnormalNode(nv);
489      SATflags(nv) |= VisitedMask;
490    }
491    sat_ArrayInsert(cnfArray, 0);
492  }
493
494  /** Collect transition function(AIG) for CNF translation **/
495  rootArray = sat_ArrayAlloc(t->nLatches);
496  for(i=0; i<t->nLatches; i++) {
497    v = t->nstates[i];
498    v = SATnormalNode(v);
499    if(v>1 && (SATflags(v) & VisitedMask))
500      sat_ArrayInsert(rootArray, v);
501  }
502  for(i=0; i<rootArray->num; i++) {
503    v = rootArray->space[i];
504    SATflags(v) &= ResetVisitedMask;
505  }
506
507  if(cm->maxNodesArraySize > t->manager->maxNodesArraySize) {
508    t->manager->maxNodesArraySize = cm->maxNodesArraySize;
509    t->manager->nameList   = REALLOC(char *, t->manager->nameList  , t->manager->maxNodesArraySize/bAigNodeSize);
510    t->manager->bddIdArray = REALLOC(int ,   t->manager->bddIdArray  , t->manager->maxNodesArraySize/bAigNodeSize);
511    t->manager->bddArray   = REALLOC(bdd_t *, t->manager->bddArray  , t->manager->maxNodesArraySize/bAigNodeSize);
512  }
513  t->manager->maxNodesArraySize = cm->maxNodesArraySize;
514  t->manager->NodesArray = cm->nodesArray;
515  bAig_CreateCNFFromAIG(t->manager, rootArray, cnfArray);
516  sat_ArrayFree(rootArray);
517
518  /** Collect all previous blocking clauses **/
519  for(v = cm->frontierNodesEnd; v<cm->nodesArraySize; v+= satNodeSize) {
520    if(!(SATflags(v) & IsCNFMask))      continue;
521    if(!(SATflags(v) & IsBlockingMask)) continue;
522    size = SATnumLits(v);
523    plit = (long*)SATfirstLit(v);
524    for(i=0; i<size; i++, plit++) {
525      nv = SATgetNode(*plit);
526      sat_ArrayInsert(cnfArray, nv);
527    }
528    sat_ArrayInsert(cnfArray, -v);
529  }
530
531  /** add objecitve into CNF instance **/
532  sat_ArrayInsert(cnfArray, t->objective);
533  sat_ArrayInsert(cnfArray, 0);
534
535  option = sat_InitOption();
536
537  if(t->verbose > 2) {
538    sprintf(filename, "core%d.cnf", t->iteration);
539    sat_WriteCNFFromArray(cnfArray, filename);
540  }
541  coreArray = sat_ArrayAlloc(1024);
542  flag = sat_CNFMainWithArray(option, cnfArray, 1, coreArray, mappedTable);
543
544  if(flag == SAT_SAT)   {
545    sprintf(filename, "core%d.cnf", t->iteration);
546    fprintf(stdout, "ERROR : this instance %s should be UNSAT\n", filename);
547    sat_WriteCNFFromArray(cnfArray, filename);
548  }
549
550  for(i=0; i<coreArray->num; i++) {
551    v = coreArray->space[i];
552    if(st_lookup(mappedTable, (char *)v, &nv)) {
553      /* If a clause is blocking clause then it is in the table **/
554      SATflags(nv) |= InCoreMask;   
555    }
556    /**
557    else {
558      fprintf(stdout, "ERROR : the clause %ld should be in the mapping table\n", v);
559    }
560    **/
561  }
562  for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
563    if(!(SATflags(v) & IsCNFMask))
564      continue;
565    if(!(SATflags(v) & IsBlockingMask))
566      continue;
567    if(!(SATflags(v) & IsFrontierMask))
568      continue;
569    if((SATflags(v) & InCoreMask))
570      continue;
571
572    SATresetInUse(v);
573    if(t->verbose > 4) {
574      fprintf(vis_stdout, "NOTICE : deleted blocking clause\n");
575      sat_PrintNode(cm, v);
576    }
577  }
578
579
580  st_free_table(mappedTable);
581  sat_ArrayFree(cnfArray);
582  sat_ArrayFree(coreArray);
583}
584
585/**Function********************************************************************
586
587  Synopsis    [Check if the initial states are included in conjunction of block clauses.]
588
589  Description [Check if the initial states are included in conjunction of block clauses. It is done by checking satisfiability of formula (I \wedge \neg B).
590 If it is unsatisfiable then all the initial states are included in B.]
591
592  SideEffects []
593
594  SeeAlso     []
595
596******************************************************************************/
597int
598bAigInclusionTestOnInitialStates(bAigTransition_t *t)
599{
600satArray_t *cnfArray;
601satOption_t *option;
602char filename[1024];
603int flag;
604
605  if(t->inclusionInitial == 0)  return(1);
606
607  cnfArray = bAigCreateCNFInstanceForInclusionTestOnInitialStates(t);
608  option = sat_InitOption();
609
610  if(t->verbose > 2) {
611    sprintf(filename, "init%d.cnf", t->iteration);
612    sat_WriteCNFFromArray(cnfArray, filename);
613  }
614  flag = sat_CNFMainWithArray(option, cnfArray, 0, 0, 0);
615  sat_ArrayFree(cnfArray);
616
617  if(flag == SAT_UNSAT) return(1);
618  else                  return(0);
619
620  return(1);
621}
622
623/**Function********************************************************************
624
625  Synopsis    [Create instance for initial states inclusion test]
626
627  Description [Create instance for initial states inclusion test]
628
629  SideEffects []
630
631  SeeAlso     []
632
633******************************************************************************/
634satArray_t *
635bAigCreateCNFInstanceForInclusionTestOnInitialStates(bAigTransition_t *t)
636{
637satArray_t *cnfArray, *frontier;
638satArray_t *andArr, *orArr, *fandArr, *clause;
639satArray_t *rootArray;
640bAigEdge_t v, cv, out, objective;
641bAigEdge_t maxIndex;
642long *space;
643int i, j;
644int nCls;
645
646  maxIndex = 0;
647  for(i=0; i<t->nLatches; i++) {
648    v = t->cstates[i];
649    if(maxIndex < v)    maxIndex = v;
650  }
651  maxIndex += bAigNodeSize;
652 
653  cnfArray = sat_ArrayAlloc(2048);
654  andArr = sat_ArrayAlloc(1024);
655  orArr = sat_ArrayAlloc(1024);
656  fandArr = sat_ArrayAlloc(1024);
657  clause = sat_ArrayAlloc(1024);
658 
659  nCls = 0;
660  frontier = t->frontier; 
661  sat_ArrayInsert(cnfArray, 0);
662  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
663    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
664      space++;
665      i++;
666
667      if(i >= frontier->num) {
668        break;
669      }
670
671      fandArr->num = 0;
672      andArr->num = 0;
673      while(*space > 0) {
674        sat_ArrayInsert(fandArr, *space);
675        i++;
676        space++;
677      }
678      i--;
679      space--;
680
681
682      for(j=0; j<fandArr->num; j++) {
683        v = fandArr->space[j];
684        sat_ArrayInsert(andArr, v);
685      }
686
687      out = maxIndex;
688      maxIndex += bAigNodeSize;
689      sat_ArrayInsert(orArr, out);
690
691      for(j=0; j<andArr->num; j++) {
692        v = andArr->space[j];
693        sat_ArrayInsert(cnfArray, SATnot(v));
694        sat_ArrayInsert(cnfArray, SATnot(out));
695        sat_ArrayInsert(cnfArray, -1); /** seperator **/
696        nCls++;
697      }
698
699      for(j=0; j<andArr->num; j++) {
700        v = andArr->space[j];
701        sat_ArrayInsert(cnfArray, v);
702      }
703      sat_ArrayInsert(cnfArray, out);
704      sat_ArrayInsert(cnfArray, -1);
705      nCls++;
706    }
707  }
708
709  objective = maxIndex;
710  maxIndex += bAigNodeSize;
711  for(i=0; i<orArr->num; i++) {
712    v = orArr->space[i];
713    sat_ArrayInsert(cnfArray, SATnot(v));
714    sat_ArrayInsert(cnfArray, objective);
715    sat_ArrayInsert(cnfArray, -1);
716    nCls++;
717  }
718  for(i=0; i<orArr->num; i++) {
719    v = orArr->space[i];
720    sat_ArrayInsert(cnfArray, v);
721  }
722
723  sat_ArrayInsert(cnfArray, SATnot(objective));
724
725  sat_ArrayInsert(cnfArray, -1);
726  nCls++;
727
728  /** assert objective **/
729  sat_ArrayInsert(cnfArray, objective);
730  sat_ArrayInsert(cnfArray, -1);
731  nCls++;
732
733  sat_ArrayFree(andArr);
734  sat_ArrayFree(orArr);
735  sat_ArrayFree(fandArr);
736  sat_ArrayFree(clause);
737
738
739  /** Collect AIG for CNF translation **/
740  rootArray = sat_ArrayAlloc(t->nLatches);
741  for(i=0; i<t->nLatches; i++) {
742    v = t->initials[i];
743    if(v>1)
744      sat_ArrayInsert(rootArray, v);
745  }
746
747  if(t->allsat->maxNodesArraySize > t->manager->maxNodesArraySize) {
748    t->manager->maxNodesArraySize = t->allsat->maxNodesArraySize;
749    t->manager->nameList   = REALLOC(char *, t->manager->nameList  , t->manager->maxNodesArraySize/bAigNodeSize);
750    t->manager->bddIdArray = REALLOC(int ,   t->manager->bddIdArray  , t->manager->maxNodesArraySize/bAigNodeSize);
751    t->manager->bddArray   = REALLOC(bdd_t *, t->manager->bddArray  , t->manager->maxNodesArraySize/bAigNodeSize);
752  }
753  t->manager->maxNodesArraySize = t->allsat->maxNodesArraySize;
754  t->manager->NodesArray = t->allsat->nodesArray;
755  bAig_CreateCNFFromAIG(t->manager, rootArray, cnfArray);
756  sat_ArrayFree(rootArray);
757
758  /**
759   * connect AIG root and current state variable with equivalence
760   * relation
761   * **/
762  for(i=0; i<t->nLatches; i++) {
763    v = t->initials[i];
764    cv = t->cstates[i];
765    if(v == 0) {
766      sat_ArrayInsert(cnfArray, SATnot(cv));
767      sat_ArrayInsert(cnfArray, -1);
768    }
769    else if(v == 1) {
770      sat_ArrayInsert(cnfArray, cv);
771      sat_ArrayInsert(cnfArray, -1);
772    }
773    else {
774      sat_ArrayInsert(cnfArray, SATnot(v));
775      sat_ArrayInsert(cnfArray, (cv));
776      sat_ArrayInsert(cnfArray, -1);
777      sat_ArrayInsert(cnfArray, (v));
778      sat_ArrayInsert(cnfArray, SATnot(cv));
779      sat_ArrayInsert(cnfArray, -1);
780    }
781  }
782
783  return(cnfArray);
784}
785
786/**Function********************************************************************
787
788  Synopsis    [Create instance for AIG]
789
790  Description [Create instance for AIG]
791
792  SideEffects []
793
794  SeeAlso     []
795
796******************************************************************************/
797void
798bAig_CreateCNFFromAIG(
799        bAig_Manager_t *manager,
800        satArray_t *rootArray,
801        satArray_t *cnfArray)
802{
803int i;
804bAigEdge_t v, left, right;
805
806  for(i=0; i<rootArray->num; i++) {
807    v = rootArray->space[i];
808    bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
809  }
810
811  for(v=bAigFirstNodeIndex ; v<manager->nodesArraySize; v+=bAigNodeSize){
812    if(flags(v) & IsCNFMask) 
813      continue;
814    if(flags(v) & VisitedMask) {
815      /** create CNF for this AIG **/
816      left = leftChild(v);
817      if(left == 2)
818        continue;
819      right = rightChild(v);
820
821      sat_ArrayInsert(cnfArray, SATnot(left));
822      sat_ArrayInsert(cnfArray, SATnot(right));
823      sat_ArrayInsert(cnfArray, (v));
824      sat_ArrayInsert(cnfArray, -1);
825      sat_ArrayInsert(cnfArray, (left));
826      sat_ArrayInsert(cnfArray, SATnot(v));
827      sat_ArrayInsert(cnfArray, -1);
828      sat_ArrayInsert(cnfArray, (right));
829      sat_ArrayInsert(cnfArray, SATnot(v));
830      sat_ArrayInsert(cnfArray, -1);
831    }
832  }
833
834  for(i=0; i<rootArray->num; i++) {
835    v = rootArray->space[i];
836    bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
837  }
838  return;
839}
840                     
841
842
843/**Function********************************************************************
844
845  Synopsis    [Compute AX based on SAT.]
846
847  Description [Compute AX based on SAT.]
848
849  SideEffects []
850
851  SeeAlso     []
852
853******************************************************************************/
854void
855bAig_ComputeAX(bAigTransition_t *t)
856{
857satManager_t *cm;
858long btime, etime;
859
860  btime = util_cpu_time();
861
862  cm = t->allsat;
863  sat_PreProcessingForMixed(cm);
864
865  if(cm->status == 0) {
866    if(t->constrain)
867      bAigCreateSatManagerForLifting(t);
868    else 
869      bAigCreateSatManagerForLiftingUnconstrained(t);
870  /**
871    **/
872    bAigSolveAllSatWithLifting(t);
873    if(t->iteration > 0 && t->reductionUsingUnsat)
874      bAigReduceBlockingClauseWithUnsatCore(t);
875  }
876
877  sat_PostProcessing(cm);
878
879  /** Copy to transition so that they can be used for next iteration **/
880  t->reached = cm->reached;
881  t->frontier = cm->frontier;
882  cm->reached = 0;
883  cm->frontier = 0;
884
885  etime = util_cpu_time();
886  cm->each->satTime = (double)(etime - btime) / 1000.0 ;
887  fflush(vis_stdout);
888  return;
889 
890}
891
892
893/**Function********************************************************************
894
895  Synopsis    [Enumerate solution with lifting.]
896
897  Description [Enumerate solution with lifting.]
898
899  SideEffects []
900
901  SeeAlso     []
902
903******************************************************************************/
904void
905bAigSolveAllSatWithLifting(bAigTransition_t *t)
906{
907satManager_t *cm;
908satLevel_t *d;
909satOption_t *option;
910int level;
911
912  cm = t->allsat;
913
914  d = SATgetDecision(0);
915  cm->implicatedSoFar = d->implied->num;
916  cm->currentTopConflict = 0;
917
918  option = cm->option;
919
920  /**
921  option->decisionHeuristic = 0;
922  option->decisionHeuristic |= DVH_DECISION;
923  **/
924
925  if(cm->status == SAT_UNSAT) {
926    sat_Undo(cm, SATgetDecision(0));
927    return;
928  }
929
930  while(1) {
931    sat_PeriodicFunctions(cm);
932
933    d = sat_MakeDecision(cm);
934
935    if(d == 0)  {
936      bAigBlockingClauseAnalysisBasedOnLifting(t, cm);
937
938      if(cm->currentDecision == -1) {
939        sat_Undo(cm, SATgetDecision(0));
940        cm->status = SAT_UNSAT;
941        return;
942      }
943      d = SATgetDecision(cm->currentDecision);
944    }
945
946    while(1) {
947      sat_ImplicationMain(cm, d);
948
949      if(d->conflict == 0)     
950        break;
951
952      level = sat_ConflictAnalysis(cm, d);
953
954      if(cm->currentDecision == -1) {
955        sat_Undo(cm, SATgetDecision(0));
956        cm->status = SAT_UNSAT;
957        return;
958      }
959
960      d = SATgetDecision(cm->currentDecision);
961    }
962  }
963
964  return;
965}
966
967/**Function********************************************************************
968
969  Synopsis    [Apply minimization based on lifting and create blocking clause.]
970
971  Description [Apply minimization based on lifting and create blocking clause.]
972
973  SideEffects []
974
975  SeeAlso     []
976
977******************************************************************************/
978void
979bAigBlockingClauseAnalysisBasedOnLifting(bAigTransition_t *t, satManager_t *allsat)
980{
981satManager_t *cm;
982satLevel_t *d;
983satArray_t *clauseArray;
984bAigEdge_t v, obj, blocked, fdaLit;
985int objInverted, inverted;
986int i, satisfied;
987int value, tvalue;
988int mLevel, bLevel;
989
990  cm = allsat;
991  for(i=0; i<t->nInputs; i++) {
992    v = t->inputs[i];
993    t->vinputs[i] = SATvalue(v);
994  }
995
996  SATcm = allsat;
997  qsort(t->tstates, t->nLatches, sizeof(bAigEdge_t), levelCompare);
998
999  for(i=0; i<t->nLatches; i++) {
1000    v = t->tstates[i];
1001    t->vtstates[i] = SATvalue(v);
1002  }
1003
1004  /** cm is lifting instance from now on **/
1005  cm = t->lifting;
1006
1007  obj = (bAigEdge_t )cm->obj->space[0];
1008  objInverted = SATisInverted(obj);
1009  obj = SATnormalNode(obj);
1010
1011  d = sat_AllocLevel(cm);
1012  satisfied = 0;
1013
1014  clauseArray = sat_ArrayAlloc(256);
1015  clauseArray->num = 0;
1016
1017  /**
1018   * Propagate primary input variable first,
1019   * since  they can be freely qunatified
1020   **/
1021  for(i=0; i<t->nInputs; i++) {
1022    if(satisfied)       break;
1023    v = t->inputs[i];
1024    if(!(SATflags(v) & CoiMask))        continue;
1025
1026    value = t->vinputs[i];
1027    if(value > 1)       continue;
1028    tvalue = SATvalue(v);
1029    if(tvalue < 2)      continue;
1030
1031    SATvalue(v) = value;
1032    SATmakeImplied(v, d);
1033    sat_Enqueue(cm->queue, v);
1034    SATflags(v) |= InQueueMask;
1035
1036    sat_ImplicationMain(cm, d);
1037
1038    value = SATvalue(obj);
1039    if(value < 2)       satisfied = 1; 
1040  }
1041
1042  /**
1043   * Propagate current state variable to apply greedy minization.
1044   * Save candidates variable for lifting to clauseArray
1045   **/
1046  if(satisfied == 0) {
1047    d = sat_AllocLevel(cm);
1048    for(i=0; i<t->nLatches; i++) {
1049      if(satisfied)     break;
1050      v = t->tstates[i];
1051      if(!(SATflags(v) & CoiMask))      continue;
1052
1053      value = t->vtstates[i];
1054      if(value > 1)     continue; /** exceptional case **/
1055      tvalue = SATvalue(v);
1056 
1057      /**
1058       * If a current state variable is implied by other state variable
1059       * sasignments then it is part of candidate variable
1060       **/
1061      sat_ArrayInsert(clauseArray, v^(!value));
1062 
1063      if(tvalue > 1) {
1064        SATvalue(v) = value;
1065        SATmakeImplied(v, d);
1066        sat_Enqueue(cm->queue, v);
1067        SATflags(v) |= InQueueMask;
1068   
1069        sat_ImplicationMain(cm, d);
1070        value = SATvalue(obj);
1071        if(value < 2)   satisfied = 1; 
1072      }
1073    }
1074  }
1075
1076  value = SATvalue(obj);
1077  if(value > 1) {
1078    fprintf(stdout, "ERROR : Can't justify objective %ld\n", t->objective);
1079    exit(0);
1080  }
1081
1082  if(clauseArray->num == 0) { 
1083    /** the objective is satified with primary input only **/
1084    sat_Backtrack(cm, 0);
1085    cm->currentDecision--;
1086
1087    sat_Backtrack(allsat, 0);
1088    allsat->currentDecision--;
1089    return;
1090  }
1091
1092
1093  bAigCollectAntecdentOfObjective(t, cm, t->objective, clauseArray);
1094
1095  if(clauseArray->num == 0) { 
1096    /** the objective is satified with primary input only **/
1097    fprintf(stdout, "ERROR : This might be the bug after greedy heuristic\n");
1098    sat_Backtrack(cm, 0);
1099    cm->currentDecision--;
1100
1101    return;
1102  }
1103
1104  sat_Backtrack(cm, 0);
1105  d = SATgetDecision(cm->currentDecision);
1106  sat_Undo(cm, d);
1107  cm->currentDecision--;
1108
1109  /**
1110  bAigMinimizationBasedOnLifting(t, t->objective, clauseArray);
1111  **/
1112  if(t->disableLifting == 0)
1113    bAigMinimizationBasedOnLiftingAllAtOnce(t, t->objective, clauseArray);
1114
1115  if(clauseArray->num == 0) { 
1116    /** the objective is satified with primary input only **/
1117    /**
1118    fprintf(stdout, "ERROR : This might be the bug after lifting\n");
1119    **/
1120
1121    if(cm->currentDecision >= 0) {
1122      sat_Backtrack(cm, 0);
1123      cm->currentDecision--;
1124    }
1125
1126    sat_Backtrack(allsat, 0);
1127    allsat->currentDecision--;
1128
1129    return;
1130  }
1131
1132  /** operation on all sat instance **/
1133  cm = t->allsat;
1134
1135  mLevel = 0;
1136  for(i=0; i<clauseArray->num; i++) {
1137    v = clauseArray->space[i];
1138    v = SATnormalNode(v);
1139    if(mLevel < SATlevel(v))
1140      mLevel = SATlevel(v);
1141  }
1142
1143  blocked = sat_AddBlockingClause(cm, clauseArray);
1144  SATflags(blocked) |= IsFrontierMask;
1145
1146  if(t->verbose > 3)
1147    sat_PrintNode(cm, blocked);
1148
1149  sat_Backtrack(cm, mLevel);
1150  d = SATgetDecision(cm->currentDecision);
1151
1152  if(t->verbose > 3) {
1153    qsort(clauseArray->space, clauseArray->num, sizeof(long), indexCompare);
1154    for(i=0; i<clauseArray->num; i++) {
1155      fprintf(stdout, "%ld ", clauseArray->space[i]);
1156    }
1157    fprintf(stdout, "\n");
1158  }
1159
1160  if(bAigCheckExistenceOfUIP(cm, clauseArray, mLevel, &fdaLit, &bLevel)) {
1161    sat_Backtrack(cm, bLevel);
1162
1163    if(SATlevel(fdaLit) == 0) {
1164      sat_Backtrack(cm, 0);
1165      cm->currentDecision = -1;
1166      sat_ArrayFree(clauseArray);
1167      return;
1168    }
1169
1170    d = SATgetDecision(cm->currentDecision);
1171    inverted = SATisInverted(fdaLit);
1172    fdaLit = SATnormalNode(fdaLit);
1173    SATante(fdaLit) = blocked;
1174    SATvalue(fdaLit) = inverted;
1175    SATmakeImplied(fdaLit, d);
1176   
1177    if((SATflags(fdaLit) & InQueueMask)  == 0) {
1178      sat_Enqueue(cm->queue, fdaLit);
1179      SATflags(fdaLit) |= InQueueMask;
1180    }
1181  }
1182  else {
1183    d->conflict = blocked;
1184    sat_ConflictAnalysisWithBlockingClause(cm, d);
1185  }
1186
1187  sat_ArrayFree(clauseArray);
1188  return;
1189}
1190
1191/**Function********************************************************************
1192
1193  Synopsis    [Apply minization based on checking antecedent of objective.]
1194
1195  Description [Apply minization based on checking antecedent of objective.]
1196
1197  SideEffects []
1198
1199  SeeAlso     []
1200
1201******************************************************************************/
1202int
1203bAigCheckExistenceOfUIP(
1204        satManager_t *cm, 
1205        satArray_t *clauseArray, 
1206        int mLevel, 
1207        bAigEdge_t *fdaLit, 
1208        int *bLevel)
1209{
1210int i, nLit, level;
1211int uipFlag;
1212bAigEdge_t v, ante;
1213
1214  nLit = 0;
1215  *bLevel = 0;
1216  *fdaLit = 0;
1217  uipFlag = 0;
1218  for(i=0; i<clauseArray->num; i++) {
1219    v = clauseArray->space[i];
1220    v = SATnormalNode(v);
1221    level = SATlevel(v);
1222    if(level == mLevel) {
1223      nLit++;
1224      if(nLit > 1)
1225        break;
1226
1227      ante = SATante(v);
1228      if(ante == 0) {
1229        uipFlag = 1;
1230        *fdaLit = clauseArray->space[i];
1231      }
1232    }
1233    else if(*bLevel < level)
1234      *bLevel = level;
1235  }
1236
1237  if(nLit > 1)
1238    uipFlag = 0;
1239
1240  if(uipFlag)   return(1);
1241  else          return(0);
1242}
1243
1244/**Function********************************************************************
1245
1246  Synopsis    [Apply minization based on checking antecedent of objective.]
1247
1248  Description [Apply minization based on checking antecedent of objective.]
1249
1250  SideEffects []
1251
1252  SeeAlso     []
1253
1254******************************************************************************/
1255void
1256bAigMinimizationBasedOnLifting(
1257        bAigTransition_t *t, 
1258        bAigEdge_t obj,
1259        satArray_t *orderArray)
1260{
1261satManager_t *allsat, *cm;
1262satLevel_t *d;
1263satArray_t *tmpArray;
1264satArray_t *notLiftableArray;
1265bAigEdge_t v, tv, *plit;
1266bAigEdge_t lastNode, lastLit, ante;
1267int inverted, inserted;
1268int tvalue, value, bLevel;
1269int i, j, size;
1270
1271  cm = t->lifting;
1272  allsat = t->allsat;
1273  /**
1274   * This is for incremental SAT to identified objective dependent conflict
1275   * clauses
1276   **/
1277  cm->option->includeLevelZeroLiteral = 1;
1278  lastLit = cm->literals->last-cm->literals->begin;
1279  lastNode = cm->nodesArraySize;
1280
1281  /**
1282   * Make level 0 implication 
1283   * 1. Primary input since they are not the target of lifting
1284   * 2. Unit and pure literals..
1285   * 3. Complemented objective
1286   **/
1287  d = sat_AllocLevel(cm);
1288  for(i=0; i<t->nInputs; i++) {
1289    v = t->inputs[i];
1290    if(!(SATflags(v) & CoiMask))        continue;
1291    value = t->vinputs[i];
1292
1293    SATvalue(v) = value;
1294    SATmakeImplied(v, d);
1295    sat_Enqueue(cm->queue, v);
1296    SATflags(v) |= InQueueMask;
1297
1298  }
1299  sat_ImplyArray(cm, d, cm->assertion);
1300  sat_ImplyArray(cm, d, cm->unitLits);
1301  sat_ImplyArray(cm, d, cm->pureLits);
1302  sat_ImplyArray(cm, d, cm->auxObj);
1303  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
1304
1305  value = SATisInverted(obj);
1306  v = SATnormalNode(obj);
1307  SATvalue(v) = value;
1308  SATmakeImplied(v, d);
1309  if((SATflags(v) & InQueueMask) == 0) {
1310    sat_Enqueue(cm->queue, v);
1311    SATflags(v) |= InQueueMask;
1312  }
1313  sat_ImplicationMain(cm, d);
1314
1315  /** Apply lifting **/
1316  for(i=0; i<orderArray->num; i++) {
1317    cm->status = 0;
1318
1319    /** check liftability of i'th variable on order array */
1320
1321    tv = orderArray->space[i];
1322    v = SATnormalNode(tv);
1323    value = SATvalue(v);
1324    if(value < 2) { /** implied by other decisions */
1325      continue;
1326    }
1327    value = !SATisInverted(tv);
1328    SATvalue(v) = value;
1329
1330    d = sat_AllocLevel(cm);
1331
1332    SATmakeImplied(v, d);
1333    if((SATflags(v) & InQueueMask) == 0) {
1334      sat_Enqueue(cm->queue, v);
1335      SATflags(v) |= InQueueMask;
1336    }
1337    sat_ImplicationMain(cm, d);
1338  }
1339
1340  /** check liftability of i'th variable on order array */
1341  notLiftableArray = sat_ArrayAlloc(orderArray->num);
1342  for(i=orderArray->num-1; i>=0; i--) {
1343      /** to identify previous decision **/
1344    while(1) {
1345      if(i<0) break;
1346      tv = orderArray->space[i];
1347      v = SATnormalNode(tv);
1348      value = SATvalue(v);
1349      ante = SATante(v);
1350      if(ante) { /** implied by other decisions */
1351        tvalue = !SATisInverted(tv);
1352        if(tvalue == value)
1353          sat_ArrayInsert(notLiftableArray, tv);
1354        i--;
1355        continue;
1356      }
1357      else { /** decision variable **/
1358        sat_Backtrack(cm, SATlevel(v)-1);
1359        break;
1360      }
1361    }
1362    if(i<0)     break;
1363
1364    bLevel = cm->currentDecision;
1365
1366    tv = orderArray->space[i];
1367    value = SATisInverted(tv); /** assign complemented value **/
1368    SATvalue(v) = value;
1369
1370    d = sat_AllocLevel(cm);
1371    SATmakeImplied(v, d);
1372    if((SATflags(v) & InQueueMask) == 0) {
1373      sat_Enqueue(cm->queue, v);
1374      SATflags(v) |= InQueueMask;
1375    }
1376    sat_ImplicationMain(cm, d);
1377
1378    if(d->conflict) { /** the variable can be lifted **/
1379      sat_Backtrack(cm, bLevel);
1380      continue;
1381    }
1382
1383    for(j=0; j<notLiftableArray->num; j++) {
1384      v = notLiftableArray->space[j];
1385      value = !SATisInverted(v);
1386      v = SATnormalNode(v);
1387      tvalue = SATvalue(v);
1388      if(tvalue < 2 && tvalue != value) {
1389        /** the variable can be lifted **/
1390        sat_Backtrack(cm, bLevel);
1391        d->conflict = v;
1392        continue;
1393      }
1394      SATvalue(v) = value;
1395      SATmakeImplied(v, d);
1396      if((SATflags(v) & InQueueMask) == 0) {
1397        sat_Enqueue(cm->queue, v);
1398        SATflags(v) |= InQueueMask;
1399      }
1400      sat_ImplicationMain(cm, d);
1401      if(d->conflict) { /** the variable can be lifted **/
1402        break;
1403      }
1404    }
1405
1406    if(d->conflict) { /** the variable can be lifted **/
1407      sat_Backtrack(cm, bLevel);
1408      continue;
1409    }
1410
1411    bAigSolverForLifting(cm, cm->currentDecision); /** Need further decision **/
1412    /** There is a case that the implication queue is not empty **/
1413    sat_CleanImplicationQueue(cm);
1414    if(cm->status == SAT_SAT) {
1415      sat_ArrayInsert(notLiftableArray, tv); 
1416    }
1417    sat_Backtrack(cm, bLevel);
1418  }
1419
1420  memcpy(orderArray->space, notLiftableArray->space, sizeof(long)*notLiftableArray->num);
1421  orderArray->num = notLiftableArray->num;
1422  sat_ArrayFree(notLiftableArray);
1423
1424  sat_Backtrack(cm, 0);
1425  d = SATgetDecision(cm->currentDecision);
1426  sat_Undo(cm, d);
1427  cm->currentDecision--;
1428  cm->status = 0;
1429
1430
1431  /** Forward clauses from lifting process to allsat process **/
1432  /** Need to review this code **/
1433  tmpArray = sat_ArrayAlloc(64);
1434  for(i=lastNode; i<cm->nodesArraySize; i+=satNodeSize) {
1435    size = SATnumLits(i);
1436    plit = (long*)SATfirstLit(i);
1437    inserted = 0;
1438    tmpArray->num = 0;
1439    for(j=0; j<size; j++, plit++) {
1440      v = SATgetNode(*plit);
1441      inverted = SATisInverted(v);
1442      v = SATnormalNode(v);
1443      value = (allsat->nodesArray[v+satValue]) ;
1444      value = value ^ inverted;
1445      /** To check if the clause is safe to add allsat instance **/
1446      if(value > 0)
1447        inserted = 1;
1448      sat_ArrayInsert(tmpArray, v^(!inverted));
1449    }
1450    if(inserted)
1451      sat_AddConflictClause(allsat, tmpArray, 0);
1452  }
1453  sat_ArrayFree(tmpArray);
1454
1455  return;
1456}
1457
1458/**Function********************************************************************
1459
1460  Synopsis    [Apply minization based on checking antecedent of objective.]
1461
1462  Description [Apply minization based on checking antecedent of objective.]
1463
1464  SideEffects []
1465
1466  SeeAlso     []
1467
1468******************************************************************************/
1469void
1470bAigMinimizationBasedOnLiftingAllAtOnce(
1471        bAigTransition_t *t, 
1472        bAigEdge_t obj,
1473        satArray_t *orderArray)
1474{
1475satManager_t *allsat, *cm;
1476satLevel_t *d;
1477satArray_t *implied;
1478satArray_t *notLiftableArray;
1479bAigEdge_t v, tv;
1480bAigEdge_t lastNode, lastLit;
1481long *space;
1482int value;
1483int i, j, size, num;
1484
1485  cm = t->lifting;
1486  allsat = t->allsat;
1487  /**
1488   * This is for incremental SAT to identified objective dependent conflict
1489   * clauses
1490   **/
1491  cm->option->includeLevelZeroLiteral = 1;
1492  lastLit = cm->literals->last-cm->literals->begin;
1493  lastNode = cm->nodesArraySize;
1494
1495  /**
1496   * Make level 0 implication 
1497   * 1. Primary input since they are not the target of lifting
1498   * 2. Unit and pure literals..
1499   * 3. Complemented objective
1500   **/
1501  d = sat_AllocLevel(cm);
1502  for(i=0; i<t->nInputs; i++) {
1503    v = t->inputs[i];
1504    if(!(SATflags(v) & CoiMask))        continue;
1505    value = t->vinputs[i];
1506
1507    SATvalue(v) = value;
1508    SATmakeImplied(v, d);
1509    sat_Enqueue(cm->queue, v);
1510    SATflags(v) |= InQueueMask;
1511
1512  }
1513  sat_ImplyArray(cm, d, cm->assertion);
1514  sat_ImplyArray(cm, d, cm->unitLits);
1515  sat_ImplyArray(cm, d, cm->pureLits);
1516  sat_ImplyArray(cm, d, cm->auxObj);
1517  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
1518
1519  value = SATisInverted(obj);
1520  v = SATnormalNode(obj);
1521  SATvalue(v) = value;
1522  SATmakeImplied(v, d);
1523  if((SATflags(v) & InQueueMask) == 0) {
1524    sat_Enqueue(cm->queue, v);
1525    SATflags(v) |= InQueueMask;
1526  }
1527  sat_ImplicationMain(cm, d);
1528
1529  /** Apply lifting **/
1530  num = d->implied->num;
1531  notLiftableArray = sat_ArrayAlloc(orderArray->num);
1532  for(i=0; i<orderArray->num; i++) {
1533    cm->status = 0;
1534    d->conflict = 0;
1535
1536    /** check liftability of i'th variable on order array */
1537
1538    tv = orderArray->space[i];
1539    v = SATnormalNode(tv);
1540    value = SATisInverted(tv);
1541    SATvalue(v) = value;
1542
1543    SATmakeImplied(v, d);
1544    if((SATflags(v) & InQueueMask) == 0) {
1545      sat_Enqueue(cm->queue, v);
1546      SATflags(v) |= InQueueMask;
1547    }
1548
1549    for(j=i+1; j<orderArray->num; j++) {
1550      v = orderArray->space[j];
1551      value = !SATisInverted(v);
1552      v = SATnormalNode(v);
1553      SATvalue(v) = value;
1554      SATmakeImplied(v, d);
1555      if((SATflags(v) & InQueueMask) == 0) {
1556        sat_Enqueue(cm->queue, v);
1557        SATflags(v) |= InQueueMask;
1558      }
1559    }
1560
1561    for(j=0; j<notLiftableArray->num; j++) {
1562      v = notLiftableArray->space[j];
1563      value = !SATisInverted(v);
1564      v = SATnormalNode(v);
1565      SATvalue(v) = value;
1566      SATmakeImplied(v, d);
1567      if((SATflags(v) & InQueueMask) == 0) {
1568        sat_Enqueue(cm->queue, v);
1569        SATflags(v) |= InQueueMask;
1570      }
1571    }
1572    sat_ImplicationMain(cm, d);
1573
1574
1575    if(d->conflict == 0) {
1576      bAigSolverForLifting(cm, 0); /** Need further decision **/
1577    /** There is a case that the implication queue is not empty **/
1578      sat_CleanImplicationQueue(cm);
1579    }
1580    else  {
1581      cm->status = SAT_UNSAT;
1582    }
1583
1584    if(cm->status == SAT_SAT) {
1585      sat_ArrayInsert(notLiftableArray, tv); 
1586      sat_Backtrack(cm, 0);
1587    }
1588
1589    d = SATgetDecision(0);
1590    implied = d->implied;
1591    space = implied->space;
1592    size = implied->num;
1593    for(j=num; j<size; j++) {
1594      v = space[j];
1595 
1596      SATvalue(v) = 2;
1597      SATflags(v) &= ResetNewVisitedObjInQueueMask;
1598      SATante(v) = 0;
1599      SATante2(v) = 0;
1600      SATlevel(v) = -1;
1601    }
1602    implied->num = num;
1603    cm->currentDecision = 0;
1604
1605  }
1606
1607  memcpy(orderArray->space, notLiftableArray->space, sizeof(long)*notLiftableArray->num);
1608  orderArray->num = notLiftableArray->num;
1609  sat_ArrayFree(notLiftableArray);
1610
1611
1612  d = SATgetDecision(0);
1613  sat_Undo(cm, d);
1614  cm->status = 0;
1615  cm->currentDecision = -1;
1616
1617#if 0
1618  /** Forward clauses from lifting process to allsat process **/
1619  /** Need to review this code **/
1620  tmpArray = sat_ArrayAlloc(64);
1621  for(i=lastNode; i<cm->nodesArraySize; i+=satNodeSize) {
1622    size = SATnumLits(i);
1623    plit = (long*)SATfirstLit(i);
1624    inserted = 0;
1625    tmpArray->num = 0;
1626    for(j=0; j<size; j++, plit++) {
1627      tv = SATgetNode(*plit);
1628      inverted = SATisInverted(tv);
1629      v = SATnormalNode(tv);
1630      value = (allsat->nodesArray[v+satValue]) ;
1631      value = value ^ inverted;
1632      /** To check if the clause is safe to add allsat instance **/
1633      if(value > 0)
1634        inserted = 1;
1635      sat_ArrayInsert(tmpArray, SATnot(tv));
1636    }
1637    if(inserted)
1638      sat_AddConflictClause(allsat, tmpArray, 0);
1639  }
1640  sat_ArrayFree(tmpArray);
1641#endif
1642
1643  return;
1644}
1645
1646/**Function********************************************************************
1647
1648  Synopsis    [SAT solver for lifting .]
1649
1650  Description [SAT solver for lifting. ]
1651
1652  SideEffects []
1653
1654  SeeAlso     []
1655
1656******************************************************************************/
1657void
1658bAigSolverForLifting(satManager_t *cm, int tLevel)
1659{
1660satLevel_t *d;
1661int level;
1662
1663  d = SATgetDecision(0);
1664  cm->implicatedSoFar = d->implied->num;
1665
1666  while(1) {
1667    d = sat_MakeDecision(cm);
1668
1669    if(d == 0)  {
1670      cm->status = SAT_SAT;
1671      return;
1672    }
1673
1674    while(1) {
1675      sat_ImplicationMain(cm, d);
1676
1677      if(d->conflict == 0)     
1678        break;
1679
1680      level = sat_ConflictAnalysisForLifting(cm, d);
1681
1682      if(cm->currentDecision <= -1) {
1683        cm->status = SAT_UNSAT;
1684        return;
1685      }
1686
1687      d = SATgetDecision(cm->currentDecision);
1688    }
1689  }
1690  return;
1691}
1692
1693/**Function********************************************************************
1694
1695  Synopsis    [Apply minization based on checking antecedent of objective.]
1696
1697  Description [Apply minization based on checking antecedent of objective.]
1698
1699  SideEffects []
1700
1701  SeeAlso     []
1702
1703******************************************************************************/
1704void
1705bAigCollectAntecdentOfObjective(
1706        bAigTransition_t *t, 
1707        satManager_t *cm, 
1708        bAigEdge_t obj, 
1709        satArray_t *clauseArray)
1710{
1711int i, value;
1712bAigEdge_t v;
1713
1714  bAigCollectAntecdentOfObjectiveAux(cm, obj);
1715
1716  clauseArray->num = 0;
1717  for(i=0; i<t->nLatches; i++) {
1718    v = t->tstates[i];
1719    if(SATflags(v) & VisitedMask) {
1720      value = t->vtstates[i];
1721      sat_ArrayInsert(clauseArray, v^(!value));
1722    }
1723  }
1724  /**
1725   * We don't need to reset visited flags, since they will be reset by
1726   * backtracking
1727   **/
1728}
1729
1730/**Function********************************************************************
1731
1732  Synopsis    [Apply minization based on checking antecedent of objective.]
1733
1734  Description [Apply minization based on checking antecedent of objective.]
1735
1736  SideEffects []
1737
1738  SeeAlso     []
1739
1740******************************************************************************/
1741void
1742bAigCollectAntecdentOfObjectiveAux(satManager_t *cm, bAigEdge_t v)
1743{
1744int i, size, completeness;
1745int value, inverted;
1746bAigEdge_t ante, nv, *plit;
1747
1748  if(v == 2)   
1749    return;
1750
1751  v = SATnormalNode(v);
1752  if(SATflags(v) & VisitedMask)
1753    return;
1754
1755  SATflags(v) |= VisitedMask;
1756  ante = SATante(v);
1757  if(ante == 0) 
1758    return;
1759
1760  if(SATflags(ante) & IsCNFMask) {
1761
1762    size = SATnumLits(ante);
1763
1764    completeness = 1;
1765    for(i=0, plit=(bAigEdge_t*)SATfirstLit(ante); i<size; i++, plit++) {
1766      nv = SATgetNode(*plit);
1767      inverted = SATisInverted(nv);
1768      nv = SATnormalNode(nv);
1769      value = SATvalue(nv) ^ inverted;
1770      if(v == nv) {
1771        if(value == 0)  completeness = 0;
1772      }
1773      else {
1774        if(value == 1)  completeness = 0;
1775      }
1776    }
1777    if(completeness == 0) {
1778      fprintf(stdout, "ERROR : incomplete implication graph\n");
1779    }
1780
1781    for(i=0, plit=(bAigEdge_t*)SATfirstLit(ante); i<size; i++, plit++) {
1782      nv = SATgetNode(*plit);
1783      nv = SATnormalNode(nv);
1784      if(SATflags(nv) & VisitedMask)
1785        continue;
1786      bAigCollectAntecdentOfObjectiveAux(cm, nv);
1787    }
1788  }
1789  else {
1790    bAigCollectAntecdentOfObjectiveAux(cm, ante);
1791    ante = SATante2(v);
1792    if(ante)
1793      bAigCollectAntecdentOfObjectiveAux(cm, ante);
1794  }
1795
1796}
1797
1798/**Function********************************************************************
1799
1800  Synopsis    [Create SAT manager for lifting.]
1801
1802  Description [Create SAT manager for lifting.]
1803
1804  SideEffects []
1805
1806  SeeAlso     []
1807
1808******************************************************************************/
1809void
1810bAigCreateSatManagerForLiftingUnconstrained(bAigTransition_t *t)
1811{
1812satManager_t *lifting, *allsat, *cm;
1813bAigEdge_t *lastLit;
1814satOption_t *option;
1815satLiteralDB_t *literals;
1816long objective;
1817
1818  allsat = t->allsat;
1819  lifting = sat_InitManager(0);
1820  t->lifting = lifting;
1821
1822  /** to add blocking clause to lifting instance, modify lastLit **/
1823  cm = allsat;
1824  lastLit = 0;
1825 
1826  /**  To copy circuit structure **/
1827  lifting->nodesArraySize = allsat->frontierNodesBegin;
1828
1829  lifting->initNodesArraySize = lifting->nodesArraySize;
1830  lifting->maxNodesArraySize = lifting->nodesArraySize * 2;
1831
1832  lifting->nodesArray = ALLOC(long, lifting->maxNodesArraySize);
1833  memcpy(lifting->nodesArray, allsat->nodesArray, sizeof(long) * lifting->nodesArraySize);
1834
1835  lifting->HashTable = ALLOC(long, bAig_HashTableSize);
1836  memcpy(lifting->HashTable, allsat->HashTable, sizeof(long)*bAig_HashTableSize);
1837
1838  /** allocate literal pool **/
1839  sat_AllocLiteralsDB(lifting);
1840  literals = lifting->literals;
1841
1842  lifting->comment = ALLOC(char, 2);
1843  lifting->comment[0] = ' ';
1844  lifting->comment[1] = '\0';
1845  lifting->stdErr = allsat->stdErr;
1846  lifting->stdOut = allsat->stdOut;
1847  lifting->status = 0;
1848  lifting->orderedVariableArray = 0;
1849  lifting->unitLits = sat_ArrayAlloc(16);
1850  lifting->pureLits = sat_ArrayAlloc(16);
1851  lifting->option = 0;
1852  lifting->each = 0;
1853  lifting->decisionHead = 0;
1854  lifting->variableArray = 0;
1855  lifting->queue = 0;
1856  lifting->BDDQueue = 0;
1857  lifting->unusedAigQueue = 0;
1858
1859  option = sat_InitOption();
1860  lifting->option = option;
1861  option->verbose = 0;
1862
1863  /** this is important because of incrementality **/
1864  option->decisionHeuristic = 0;
1865  option->decisionHeuristic |= DVH_DECISION;
1866
1867  lifting->each = sat_InitStatistics();
1868
1869  if(t->originalFrontier || t->allsat->reached) {
1870    objective = bAigBuildComplementedObjectiveWithCNF(
1871          t, lifting, t->originalFrontier, t->allsat->reached);
1872    objective = SATnot(objective);
1873  }
1874  else {
1875    lifting->initNumVariables = lifting->nodesArraySize;
1876    if(lifting->variableArray == 0) {
1877      lifting->variableArray = ALLOC(satVariable_t, lifting->initNumVariables+1);
1878      memset(lifting->variableArray, 0, 
1879              sizeof(satVariable_t) * (lifting->initNumVariables+1));
1880    }
1881    sat_CleanDatabase(lifting);
1882
1883    if(t->allsat->assertion) t->lifting->assertion = sat_ArrayDuplicate(t->allsat->assertion);
1884    if(t->allsat->auxObj)    t->lifting->auxObj = sat_ArrayDuplicate(t->allsat->auxObj);
1885    objective = allsat->obj->space[0];
1886    sat_MarkTransitiveFaninForNode(lifting, objective, CoiMask);
1887  }
1888
1889
1890  sat_PreProcessingForMixedNoCompact(lifting);
1891
1892  if(lifting->obj)      sat_ArrayFree(lifting->obj);   
1893  lifting->obj = sat_ArrayAlloc(1);
1894  sat_ArrayInsert(lifting->obj, (objective));
1895
1896  /*
1897   * reset score of PI
1898   * Since the scores of PI and current state variables are high than
1899   * other variables because of blocking clauses that forwarded from
1900   * prevous image step.
1901  for(i=0; i<t->nInputs; i++) {
1902    v = t->inputs[i];
1903    var = lifting->variableArray[SATnodeID(v)];
1904    var.scores[0] = 0;
1905    var.scores[1] = 0;
1906  }
1907  for(i=0; i<t->nLatches; i++) {
1908    v = t->cstates[i];
1909    var = lifting->variableArray[SATnodeID(v)];
1910    var.scores[0] = 0;
1911    var.scores[1] = 0;
1912  }
1913   **/
1914
1915  /**
1916   * To apply greedy minimization, the objective is not asserted
1917   * The complemented objective will be asserted during lifting
1918   * process
1919   **/
1920
1921
1922  lifting->currentDecision = -1;
1923
1924}
1925
1926/**Function********************************************************************
1927
1928  Synopsis    [Create SAT manager for lifting.]
1929
1930  Description [Create SAT manager for lifting.]
1931
1932  SideEffects []
1933
1934  SeeAlso     []
1935
1936******************************************************************************/
1937void
1938bAigCreateSatManagerForLifting(bAigTransition_t *t)
1939{
1940satManager_t *lifting, *allsat, *cm;
1941bAigEdge_t *lastLit, v;
1942satOption_t *option;
1943satLiteralDB_t *literals;
1944int size, dir;
1945int nCls, nLits, index;
1946long *space;
1947
1948  allsat = t->allsat;
1949  lifting = sat_InitManager(0);
1950  t->lifting = lifting;
1951
1952  /** to add blocking clause to lifting instance, modify lastLit **/
1953  cm = allsat;
1954  lastLit = 0;
1955 
1956  if(t->constrain) {
1957    /**
1958    if(allsat->nodesArraySize != allsat->frontierNodesEnd){
1959      v = allsat->frontierNodesEnd-satNodeSize;
1960      lastLit = SATfirstLit(v);
1961      lastLit += SATnumLits(v);
1962      lastLit++;
1963    }
1964    lifting->nodesArraySize = allsat->frontierNodesEnd;
1965    **/
1966    if(allsat->nodesArraySize != allsat->frontierNodesEnd){
1967      v = allsat->nodesArraySize-satNodeSize;
1968      lastLit = (bAigEdge_t *) SATfirstLit(v);
1969      lastLit += SATnumLits(v);
1970      lastLit++;
1971    }
1972    lifting->nodesArraySize = allsat->nodesArraySize;
1973 
1974  }
1975  else {
1976/**   
1977 *  To copy circuit, frontier, and all blocking clauses
1978 *    lifting->nodesArraySize = allsat->nodesArraySize;
1979 **/
1980    /**  To copy circuit structure **/
1981    lifting->nodesArraySize = allsat->frontierNodesBegin;
1982  }
1983
1984  /**
1985   * We save the frontier SAT first in allsat instance and
1986   * blocking clauses geenrated from previous runs.
1987   **/
1988  lifting->initNodesArraySize = lifting->nodesArraySize;
1989  lifting->maxNodesArraySize = lifting->nodesArraySize * 2;
1990
1991  lifting->nodesArray = ALLOC(long, lifting->maxNodesArraySize);
1992  memcpy(lifting->nodesArray, allsat->nodesArray, sizeof(long) * lifting->nodesArraySize);
1993
1994  lifting->HashTable = ALLOC(long, bAig_HashTableSize);
1995  memcpy(lifting->HashTable, allsat->HashTable, sizeof(long)*bAig_HashTableSize);
1996
1997  literals = ALLOC(satLiteralDB_t, 1);
1998  lifting->literals = literals;
1999
2000  if(lastLit > 0) {
2001    size = lastLit - allsat->literals->begin;
2002  }
2003  else {
2004    size = 0;
2005  }
2006
2007  if(size > 1) { /** there are clauses for objective **/
2008    literals->begin = ALLOC(long, size*4);
2009    literals->end = literals->begin + size*4;
2010    memcpy(literals->begin, allsat->literals->begin, sizeof(long)*size);
2011    literals->last = literals->begin + size;
2012    literals->initialSize = literals->begin+size-1;
2013  }
2014  else { /** there is no extra logic for objective **/
2015    size = 1024 * 1024;
2016    literals->begin = ALLOC(long, size);
2017    *(literals->begin) = 0;
2018    literals->last = literals->begin + 1;
2019    literals->end = literals->begin + size;
2020    literals->initialSize = literals->last;
2021  }
2022
2023  lifting->initNumVariables = allsat->initNumVariables;
2024  lifting->initNumClauses = allsat->initNumClauses;
2025  lifting->initNumLiterals = allsat->initNumLiterals;
2026  lifting->comment = ALLOC(char, 2);
2027  lifting->comment[0] = ' ';
2028  lifting->comment[1] = '\0';
2029  lifting->stdErr = allsat->stdErr;
2030  lifting->stdOut = allsat->stdOut;
2031  lifting->status = 0;
2032  lifting->orderedVariableArray = 0;
2033  lifting->unitLits = sat_ArrayAlloc(16);
2034  lifting->pureLits = sat_ArrayAlloc(16);
2035  lifting->option = 0;
2036  lifting->each = 0;
2037  lifting->decisionHead = 0;
2038  lifting->variableArray = 0;
2039  lifting->queue = 0;
2040  lifting->BDDQueue = 0;
2041  lifting->unusedAigQueue = 0;
2042
2043  option = sat_InitOption();
2044  lifting->option = option;
2045  option->verbose = 0;
2046
2047  /** this is important because of incrementality **/
2048  option->decisionHeuristic = 0;
2049  option->decisionHeuristic |= DVH_DECISION;
2050
2051  lifting->each = sat_InitStatistics();
2052
2053  sat_CleanDatabase(lifting);
2054
2055  if(lifting->variableArray == 0) {
2056    lifting->variableArray = ALLOC(satVariable_t, lifting->initNumVariables+1);
2057    memset(lifting->variableArray, 0, 
2058            sizeof(satVariable_t) * (lifting->initNumVariables+1));
2059  }
2060
2061  cm = lifting;
2062  nCls = nLits = 0;
2063  for(space = literals->begin; space < literals->last; space++) {
2064    if(*space < 0) {
2065      v = -(*space);
2066      space++;
2067      SATfirstLit(v) = (long) space;
2068      index = 0;
2069      while(1) {
2070        if(*space < 0)  break;
2071        dir = SATgetDir(*space);
2072        nLits++;
2073        if(dir == -2){
2074          space++;
2075          index++;
2076          continue;
2077        }
2078        SATunsetWL(space);
2079        sat_AddWL(cm, v, index, dir);
2080        space++;
2081        index++;
2082      }
2083      nCls++;
2084    }
2085  }
2086  lifting->initNumClauses = nCls;
2087  lifting->initNumLiterals = nLits;
2088
2089  if(allsat->assertion) lifting->assertion = sat_ArrayDuplicate(allsat->assertion);
2090  if(allsat->auxObj)    lifting->auxObj = sat_ArrayDuplicate(allsat->auxObj);
2091
2092  bAigMarkConeOfInfluenceForAX(t, lifting);
2093
2094
2095  bAigPreProcessingForLiftingInstance(t, lifting) ;
2096
2097  /*
2098   * reset score of PI
2099   * Since the scores of PI and current state variables are high than
2100   * other variables because of blocking clauses that forwarded from
2101   * prevous image step.
2102  for(i=0; i<t->nInputs; i++) {
2103    v = t->inputs[i];
2104    var = lifting->variableArray[SATnodeID(v)];
2105    var.scores[0] = 0;
2106    var.scores[1] = 0;
2107  }
2108  for(i=0; i<t->nLatches; i++) {
2109    v = t->cstates[i];
2110    var = lifting->variableArray[SATnodeID(v)];
2111    var.scores[0] = 0;
2112    var.scores[1] = 0;
2113  }
2114   **/
2115
2116  /**
2117   * To apply greedy minimization, the objective is not asserted
2118   * The complemented objective will be asserted during lifting
2119   * process
2120   **/
2121
2122  if(lifting->obj)      sat_ArrayFree(lifting->obj);   
2123  lifting->obj = sat_ArrayDuplicate(allsat->obj);
2124
2125  lifting->currentDecision = -1;
2126
2127}
2128/**Function********************************************************************
2129
2130  Synopsis    [ Pre-processing to run CirCUs with AIG and CNF]
2131
2132  Description [ Pre-processing to run CirCUs with AIG and CNF]
2133
2134  SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]
2135
2136  SeeAlso     [ sat_PostProcessing ]
2137
2138******************************************************************************/
2139void
2140bAigPreProcessingForLiftingInstance(bAigTransition_t *t, satManager_t *cm) 
2141{
2142satLevel_t *d;
2143int i;
2144long v;
2145
2146
2147  /** create implication queue **/
2148  cm->queue = sat_CreateQueue(1024);
2149  cm->BDDQueue = sat_CreateQueue(1024);
2150  cm->unusedAigQueue = sat_CreateQueue(1024);
2151
2152  /**
2153  create variable array : one can reduce size of variable array using
2154  mapping. for fanout free internal node....
2155  **/
2156
2157  if(cm->variableArray == 0) {
2158    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
2159    memset(cm->variableArray, 0, 
2160            sizeof(satVariable_t) * (cm->initNumVariables+1));
2161  }
2162
2163  if(cm->auxArray == 0)
2164    cm->auxArray = sat_ArrayAlloc(1024);
2165  if(cm->nonobjUnitLitArray == 0)
2166    cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
2167  if(cm->objUnitLitArray == 0)
2168    cm->objUnitLitArray = sat_ArrayAlloc(128);
2169
2170  /** compact fanout of AIG node
2171  sat_CompactFanout(cm);
2172  **/
2173
2174  cm->initNodesArraySize = cm->nodesArraySize;
2175  cm->beginConflict = cm->nodesArraySize;
2176
2177  if(cm->option->allSatMode) {
2178    sat_RestoreFrontierClauses(cm);
2179    sat_RestoreBlockingClauses(cm);
2180  }
2181
2182  /** Initial score **/
2183  sat_InitScoreForMixed(cm);
2184
2185  /** create decision stack **/
2186  if(cm->decisionHeadSize == 0) {
2187    cm->decisionHeadSize = 32;
2188    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
2189    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
2190  }
2191  cm->currentDecision = -1;
2192
2193  /** to avoid purify warning **/
2194  SATvalue(2) = 2;
2195  SATflags(0) = 0;
2196
2197  /** incremental SAT.... **/
2198  if(cm->option->incTraceObjective) { 
2199    sat_RestoreForwardedClauses(cm, 0);
2200  }
2201  else if(cm->option->incAll) {
2202    sat_RestoreForwardedClauses(cm, 1);
2203  }
2204
2205  if(cm->option->incTraceObjective) {
2206    sat_MarkObjectiveFlagToArray(cm, cm->obj);
2207    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
2208  }
2209
2210  /** Level 0 decision.... **/
2211  d = sat_AllocLevel(cm);
2212
2213  sat_ApplyForcedAssignmentMain(cm, d);
2214
2215  if(cm->status == SAT_UNSAT)
2216    return;
2217
2218  /**
2219   * There is a case that circuit consists of single objective node
2220   **/
2221  for(i=0; i<cm->pureLits->num; i++) {
2222    v = cm->pureLits->space[i];
2223    if(v == t->objective) {
2224      for(;i<cm->pureLits->num; i++) {
2225        cm->pureLits->space[i] = cm->pureLits->space[i+1];
2226      }
2227      cm->pureLits->num--;
2228      break;
2229    }
2230  }
2231
2232  sat_ImplyArray(cm, d, cm->assertion);
2233  sat_ImplyArray(cm, d, cm->unitLits);
2234  sat_ImplyArray(cm, d, cm->pureLits);
2235  sat_ImplyArray(cm, d, cm->auxObj);
2236  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
2237  sat_ImplyArray(cm, d, cm->obj);
2238
2239  sat_ImplicationMain(cm, d);
2240  if(d->conflict) {
2241    cm->status = SAT_UNSAT;
2242  }
2243
2244  if(cm->status == 0) {
2245    if(cm->option->incDistill) {
2246      sat_IncrementalUsingDistill(cm);
2247    }
2248  }
2249
2250}
2251
2252/**Function********************************************************************
2253
2254  Synopsis    [Post processing after computing AX.]
2255
2256  Description [Free sat manager...]
2257
2258  SideEffects []
2259
2260  SeeAlso     []
2261
2262******************************************************************************/
2263void
2264bAig_PostProcessForAX(bAigTransition_t *t, satManager_t *cm)
2265{
2266bAig_Manager_t *manager;
2267
2268  manager = t->manager;
2269  if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
2270    manager->maxNodesArraySize = cm->maxNodesArraySize;
2271    manager->nameList   = REALLOC(char *, manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
2272    manager->bddIdArray = REALLOC(int ,   manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
2273    manager->bddArray   = REALLOC(bdd_t *, manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
2274  }
2275
2276  manager->maxNodesArraySize = cm->maxNodesArraySize;
2277  manager->NodesArray = cm->nodesArray;
2278  manager->literals = cm->literals;
2279  cm->literals->last = cm->literals->initialSize;
2280
2281  cm->nodesArray = 0;
2282  cm->literals = 0;
2283  cm->HashTable = 0;
2284
2285  sat_FreeManager(cm);
2286
2287  /** reset objective for next iteration **/
2288  t->objective = 0; 
2289}
2290
2291/**Function********************************************************************
2292
2293  Synopsis    [Mark cone of influence for AX.]
2294
2295  Description [Mark cone of influence for objective and intermediate variable that are created for complement frontier.]
2296
2297  SideEffects []
2298
2299  SeeAlso     []
2300
2301******************************************************************************/
2302void
2303bAigMarkConeOfInfluenceForAX(bAigTransition_t *t, satManager_t *cm)
2304{
2305satArray_t *arr;
2306int i;
2307bAigEdge_t v;
2308
2309  sat_MarkTransitiveFaninForNode(cm, t->objective, CoiMask);
2310
2311  if(t->tVariables) {
2312    arr = t->tVariables;
2313    for(i=0; i<arr->num; i++) {
2314      v = arr->space[i];
2315      SATflags(v) |= CoiMask;
2316    }
2317  }
2318
2319  if(t->auxObj) {
2320    arr = t->auxObj;
2321    for(i=0; i<arr->num; i++) {
2322      v = arr->space[i];
2323      sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
2324    }
2325  }
2326
2327  if(t->objArr) {
2328    arr = t->objArr;
2329    for(i=0; i<arr->num; i++) {
2330      v = arr->space[i];
2331      sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
2332    }
2333  }
2334
2335}
2336
2337/**Function********************************************************************
2338
2339  Synopsis    [Make interface for CirCUs to compute AX.]
2340
2341  Description [Make interface for CirCUs to compute AX.]
2342
2343  SideEffects []
2344
2345  SeeAlso     []
2346
2347******************************************************************************/
2348satManager_t *
2349bAigCirCUsInterfaceForAX(bAigTransition_t *t)
2350{
2351satManager_t *cm;
2352bAig_Manager_t *manager;
2353satOption_t *option;
2354int i;
2355bAigEdge_t v;
2356
2357  manager = t->manager;
2358  cm = sat_InitManager(0);
2359  memset(cm, 0, sizeof(satManager_t));
2360
2361  cm->nodesArraySize = manager->nodesArraySize;
2362  cm->initNodesArraySize = manager->nodesArraySize;
2363  cm->maxNodesArraySize = manager->maxNodesArraySize;
2364  cm->nodesArray = manager->NodesArray;
2365  cm->HashTable = manager->HashTable;
2366  cm->literals = manager->literals;
2367  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
2368  cm->initNumClauses = 0;
2369  cm->initNumLiterals = 0;
2370  cm->comment = ALLOC(char, 2);
2371  cm->comment[0] = ' ';
2372  cm->comment[1] = '\0';
2373  cm->stdErr = vis_stderr;
2374  cm->stdOut = vis_stdout;
2375  cm->status = 0;
2376  cm->orderedVariableArray = 0;
2377  cm->unitLits = sat_ArrayAlloc(16);
2378  cm->pureLits = sat_ArrayAlloc(16);
2379  cm->option = 0;
2380  cm->each = 0;
2381  cm->decisionHead = 0;
2382  cm->variableArray = 0;
2383  cm->queue = 0;
2384  cm->BDDQueue = 0;
2385  cm->unusedAigQueue = 0;
2386
2387  option = sat_InitOption();
2388  cm->option = option;
2389  option->verbose = 0;
2390
2391  cm->each = sat_InitStatistics();
2392  sat_AllocLiteralsDB(cm);
2393
2394  cm->obj = sat_ArrayAlloc(1);
2395  sat_ArrayInsert(cm->obj, t->objective);
2396
2397  if(t->auxObj && t->auxObj->num) {
2398    cm->auxObj = sat_ArrayAlloc(t->auxObj->num);
2399    for(i=0; i<t->auxObj->num; i++) {
2400      v = t->auxObj->space[i];
2401      sat_ArrayInsert(cm->auxObj, v);
2402    }
2403  }
2404  cm->option->allSatMode = 1;
2405
2406  /**
2407   * Copy to reachable states and frontier to satManager 
2408   * so that they can be used to build current instance.
2409   **/
2410  cm->reached = t->reached;
2411  cm->frontier = t->frontier;
2412  t->reached = 0;
2413  t->frontier = 0;
2414
2415  return(cm);
2416
2417}
2418
2419/**Function********************************************************************
2420
2421  Synopsis    [Build new objective from frontier set by complementing blocking cluases]
2422
2423  Description [Build new objective from frontier set by complementing blocking cluases, the frontier array of bAigTransition_t save the blocking clause as clause form. The structure of frontier array is as follows.
2424      clause seperator, literals in clause, clause seperator, ..., clause seperator ]
2425
2426  SideEffects []
2427
2428  SeeAlso     []
2429
2430******************************************************************************/
2431bAigEdge_t
2432bAigBuildObjectiveFromFrontierSet(bAigTransition_t *t)
2433{
2434mAig_Manager_t *manager;
2435satArray_t *frontier;
2436satArray_t *clause;
2437satArray_t *andArr, *orArr;
2438satArray_t *fandArr;
2439satArray_t *fArr;
2440int i, j, nCls, removeFlag;
2441int inverted;
2442long *space, index;
2443bAigEdge_t v, tv, out, objective;
2444 
2445  manager = t->manager;
2446
2447  andArr = sat_ArrayAlloc(1024);
2448  fandArr = sat_ArrayAlloc(1024);
2449  clause = sat_ArrayAlloc(1024);
2450
2451  if(t->coiStates == 0) 
2452    t->coiStates = ALLOC(bAigEdge_t, sizeof(bAigEdge_t) * t->csize);
2453  memset(t->coiStates, 0, sizeof(bAigEdge_t)*t->csize);
2454
2455  if(t->tVariables) t->tVariables->num = 0;
2456  else              t->tVariables = sat_ArrayAlloc(1024);
2457  fArr = sat_ArrayAlloc(1024);
2458  orArr = t->tVariables;
2459
2460  nCls = 0;
2461  frontier = t->frontier; 
2462  sat_ArrayInsert(fArr, 0);
2463  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
2464    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
2465      space++;
2466      i++;
2467
2468      if(i >= frontier->num) {
2469        break;
2470      }
2471
2472      removeFlag = 0;
2473      fandArr->num = 0;
2474      andArr->num = 0;
2475      while(*space > 0) {
2476#if 0
2477        v = *space;
2478        inverted = SATisInverted(v);
2479        tv = SATnormalNode(v);
2480        index = SATnodeID(tv);
2481        if(index > t->csize) {
2482          fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
2483          exit(0);
2484        }
2485        v = t->c2n[index];
2486        v = v ^ (inverted);
2487        if(v == 0) {  /** skip **/
2488        }
2489        else if(v == 1)  /** trivially satisfied **/
2490          removeFlag = 1;
2491        else if(removeFlag == 0) {
2492          sat_ArrayInsert(andArr, v);
2493          t->coiStates[index] = 1;
2494        }
2495#endif
2496
2497        sat_ArrayInsert(fandArr, *space);
2498        i++;
2499        space++;
2500      }
2501      i--;
2502      space--;
2503
2504
2505      removeFlag = 0;
2506      for(j=0; j<fandArr->num; j++) {
2507        v = fandArr->space[j];
2508        inverted = SATisInverted(v);
2509        tv = SATnormalNode(v);
2510        index = SATnodeID(tv);
2511        if(index > t->csize) {
2512          fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
2513          exit(0);
2514        }
2515        v = t->c2n[index];
2516        v = v ^ (inverted);
2517
2518        if(t->verbose > 4)
2519          fprintf(stdout, "%ld(%ld) ",fandArr->space[j], v); 
2520        if(v == 0) {  /** skip **/
2521          andArr->space[j] = 0;
2522        }
2523        else if(v == 1)  /** trivially satisfied **/
2524          removeFlag = 1;
2525        else  {
2526          sat_ArrayInsert(andArr, v);
2527          t->coiStates[index] = 1;
2528        }
2529      }
2530      if(t->verbose > 4)
2531        fprintf(stdout, "\n");
2532
2533      if(removeFlag)
2534        continue;
2535
2536     
2537      if(t->verbose > 4) {
2538        fprintf(stdout, "%ld-> ", andArr->num);
2539        for(j=0; j<andArr->num; j++) {
2540          v = andArr->space[j];
2541          fprintf(stdout, "%ld ", v);
2542        }
2543        fprintf(stdout, "\n");
2544      }
2545
2546      out = bAig_CreateNode(manager, 2, 2);
2547      sat_ArrayInsert(orArr, out);
2548
2549      for(j=0; j<andArr->num; j++) {
2550        v = andArr->space[j];
2551        sat_ArrayInsert(fArr, SATnot(v));
2552        sat_ArrayInsert(fArr, SATnot(out));
2553        sat_ArrayInsert(fArr, -1); /** seperator **/
2554        nCls++;
2555      }
2556
2557      for(j=0; j<andArr->num; j++) {
2558        v = andArr->space[j];
2559        sat_ArrayInsert(fArr, v);
2560      }
2561      sat_ArrayInsert(fArr, out);
2562      sat_ArrayInsert(fArr, -1);
2563      nCls++;
2564    }
2565  }
2566
2567  objective = bAig_CreateNode(manager, 2, 2);
2568  for(i=0; i<orArr->num; i++) {
2569    v = orArr->space[i];
2570    sat_ArrayInsert(fArr, SATnot(v));
2571    sat_ArrayInsert(fArr, objective);
2572    sat_ArrayInsert(fArr, -1);
2573    nCls++;
2574  }
2575  for(i=0; i<orArr->num; i++) {
2576    v = orArr->space[i];
2577    sat_ArrayInsert(fArr, v);
2578  }
2579
2580  sat_ArrayInsert(fArr, SATnot(objective));
2581
2582  sat_ArrayInsert(fArr, -1);
2583  nCls++;
2584
2585  if(orArr->num == 0) {
2586    fArr->num = 0;
2587  }
2588
2589  if(t->verbose > 0) {
2590    fprintf(vis_stdout, "** SAT_INV : %ld number of frontier blocking clauses are processed\n", orArr->num);
2591    fprintf(vis_stdout, "** SAT_INV : %d number of clauses are added to build objective\n", nCls);
2592  }
2593
2594  sat_ArrayFree(andArr);
2595  sat_ArrayFree(fandArr);
2596  sat_ArrayFree(clause);
2597
2598  t->originalFrontier = frontier;
2599  t->frontier = fArr;
2600  t->objective = objective;
2601
2602  if(t->objArr == 0) 
2603    t->objArr = sat_ArrayAlloc(t->nLatches);
2604  t->objArr->num = 0;
2605  for(i=0; i<t->csize; i++) {
2606    if(t->coiStates[i]) {
2607      sat_ArrayInsert(t->objArr, SATnormalNode(t->c2n[i]));
2608    }
2609  }
2610
2611
2612  return(objective);
2613}
2614
2615bAigEdge_t
2616bAigBuildComplementedObjectiveWithCNF(
2617        bAigTransition_t *t, 
2618        satManager_t *cm,
2619        satArray_t *narr,
2620        satArray_t *carr)
2621{
2622satArray_t *clause;
2623satArray_t *andArr, *orArr;
2624satArray_t *fandArr;
2625satArray_t *fArr, *arr;
2626satArray_t *frontier;
2627int i, j, nCls, removeFlag;
2628int inverted;
2629long *space, index;
2630bAigEdge_t v, tv, out, objective;
2631bAigEdge_t obj1, obj2;
2632 
2633  andArr = sat_ArrayAlloc(1024);
2634  fandArr = sat_ArrayAlloc(1024);
2635  clause = sat_ArrayAlloc(1024);
2636
2637  if(t->coiStates == 0) 
2638    t->coiStates = ALLOC(bAigEdge_t, sizeof(bAigEdge_t) * t->csize);
2639  memset(t->coiStates, 0, sizeof(bAigEdge_t)*t->csize);
2640
2641  if(t->tVariables) t->tVariables->num = 0;
2642  else              t->tVariables = sat_ArrayAlloc(1024);
2643  fArr = sat_ArrayAlloc(1024);
2644
2645  orArr =sat_ArrayAlloc(1024);
2646
2647  sat_ArrayInsert(fArr, 0);
2648  nCls = 0;
2649  frontier = narr;
2650
2651
2652  if(frontier) {
2653  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
2654    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
2655      space++;
2656      i++;
2657
2658      if(i >= frontier->num) {
2659        break;
2660      }
2661
2662      removeFlag = 0;
2663      fandArr->num = 0;
2664      andArr->num = 0;
2665      while(*space > 0) {
2666        sat_ArrayInsert(fandArr, *space);
2667        i++;
2668        space++;
2669      }
2670      i--;
2671      space--;
2672
2673
2674      removeFlag = 0;
2675      for(j=0; j<fandArr->num; j++) {
2676        v = fandArr->space[j];
2677        inverted = SATisInverted(v);
2678        tv = SATnormalNode(v);
2679        index = SATnodeID(tv);
2680        if(index > t->csize) {
2681          fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
2682          exit(0);
2683        }
2684        v = t->c2n[index];
2685        v = v ^ (inverted);
2686
2687        if(t->verbose > 4)
2688          fprintf(stdout, "%ld(%ld) ",fandArr->space[j], v); 
2689        if(v == 0) {  /** skip **/
2690          andArr->space[j] = 0;
2691        }
2692        else if(v == 1)  /** trivially satisfied **/
2693          removeFlag = 1;
2694        else  {
2695          sat_ArrayInsert(andArr, v);
2696          t->coiStates[index] = 1;
2697        }
2698      }
2699      if(t->verbose > 4)
2700        fprintf(stdout, "\n");
2701
2702      if(removeFlag)
2703        continue;
2704
2705     
2706      if(t->verbose > 4) {
2707        fprintf(stdout, "%ld-> ", andArr->num);
2708        for(j=0; j<andArr->num; j++) {
2709          v = andArr->space[j];
2710          fprintf(stdout, "%ld ", v);
2711        }
2712        fprintf(stdout, "\n");
2713      }
2714
2715      out = sat_CreateNode(cm, 2, 2);
2716      sat_ArrayInsert(orArr, out);
2717      sat_ArrayInsert(t->tVariables, out);
2718
2719      for(j=0; j<andArr->num; j++) {
2720        v = andArr->space[j];
2721        sat_ArrayInsert(fArr, SATnot(v));
2722        sat_ArrayInsert(fArr, SATnot(out));
2723        sat_ArrayInsert(fArr, -1); /** seperator **/
2724        nCls++;
2725      }
2726
2727      for(j=0; j<andArr->num; j++) {
2728        v = andArr->space[j];
2729        sat_ArrayInsert(fArr, v);
2730      }
2731      sat_ArrayInsert(fArr, out);
2732      sat_ArrayInsert(fArr, -1);
2733      nCls++;
2734    }
2735  }
2736  }
2737
2738  obj1 = sat_CreateNode(cm, 2, 2);
2739  for(i=0; i<orArr->num; i++) {
2740    v = orArr->space[i];
2741    sat_ArrayInsert(fArr, SATnot(v));
2742    sat_ArrayInsert(fArr, obj1);
2743    sat_ArrayInsert(fArr, -1);
2744    nCls++;
2745  }
2746  for(i=0; i<orArr->num; i++) {
2747    v = orArr->space[i];
2748    sat_ArrayInsert(fArr, v);
2749  }
2750
2751  sat_ArrayInsert(fArr, SATnot(obj1));
2752
2753  sat_ArrayInsert(fArr, -1);
2754  nCls++;
2755
2756#if 1
2757  frontier = carr;
2758  if(frontier) {
2759  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
2760    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
2761      space++;
2762      i++;
2763
2764      if(i >= frontier->num) {
2765        break;
2766      }
2767
2768      fandArr->num = 0;
2769      andArr->num = 0;
2770      while(*space > 0) {
2771        sat_ArrayInsert(fandArr, *space);
2772        i++;
2773        space++;
2774      }
2775      i--;
2776      space--;
2777
2778
2779      if(t->verbose > 4) {
2780        fprintf(stdout, "%ld-> ", andArr->num);
2781        for(j=0; j<andArr->num; j++) {
2782          v = andArr->space[j];
2783          fprintf(stdout, "%ld ", v);
2784        }
2785        fprintf(stdout, "\n");
2786      }
2787
2788      out = sat_CreateNode(cm, 2, 2);
2789      sat_ArrayInsert(orArr, out);
2790      sat_ArrayInsert(t->tVariables, out);
2791
2792      for(j=0; j<andArr->num; j++) {
2793        v = andArr->space[j];
2794        sat_ArrayInsert(fArr, SATnot(v));
2795        sat_ArrayInsert(fArr, SATnot(out));
2796        sat_ArrayInsert(fArr, -1); /** seperator **/
2797        nCls++;
2798      }
2799
2800      for(j=0; j<andArr->num; j++) {
2801        v = andArr->space[j];
2802        sat_ArrayInsert(fArr, v);
2803      }
2804      sat_ArrayInsert(fArr, out);
2805      sat_ArrayInsert(fArr, -1);
2806      nCls++;
2807    }
2808  }
2809  }
2810
2811  obj2 = sat_CreateNode(cm, 2, 2);
2812  for(i=0; i<orArr->num; i++) {
2813    v = orArr->space[i];
2814    sat_ArrayInsert(fArr, SATnot(v));
2815    sat_ArrayInsert(fArr, obj2);
2816    sat_ArrayInsert(fArr, -1);
2817    nCls++;
2818  }
2819  for(i=0; i<orArr->num; i++) {
2820    v = orArr->space[i];
2821    sat_ArrayInsert(fArr, v);
2822  }
2823
2824  sat_ArrayInsert(fArr, SATnot(obj2));
2825
2826  sat_ArrayInsert(fArr, -1);
2827  nCls++;
2828  #endif
2829
2830  sat_ArrayInsert(t->tVariables, obj1);
2831  sat_ArrayInsert(t->tVariables, obj2);
2832  objective = sat_CreateNode(cm, 2, 2);
2833  sat_ArrayInsert(fArr, SATnot(obj1));
2834  sat_ArrayInsert(fArr, SATnot(obj2));
2835  sat_ArrayInsert(fArr, objective);
2836  sat_ArrayInsert(fArr, -1);
2837  sat_ArrayInsert(fArr, (obj1));
2838  sat_ArrayInsert(fArr, SATnot(objective));
2839  sat_ArrayInsert(fArr, -1);
2840  sat_ArrayInsert(fArr, (obj2));
2841  sat_ArrayInsert(fArr, SATnot(objective));
2842  sat_ArrayInsert(fArr, -1);
2843
2844  if(orArr->num == 0) {
2845    fArr->num = 0;
2846  }
2847
2848  if(t->verbose > 0) {
2849    fprintf(vis_stdout, "** SAT_INV : %ld number of frontier blocking clauses are processed\n", orArr->num);
2850    fprintf(vis_stdout, "** SAT_INV : %d number of clauses are added to build objective\n", nCls);
2851  }
2852
2853  sat_ArrayFree(andArr);
2854  sat_ArrayFree(fandArr);
2855  sat_ArrayFree(clause);
2856
2857  cm->initNumVariables = cm->nodesArraySize;
2858  if(cm->variableArray == 0) {
2859    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
2860    memset(cm->variableArray, 0, 
2861            sizeof(satVariable_t) * (cm->initNumVariables+1));
2862  }
2863  sat_RestoreClauses(cm, fArr);
2864  sat_CleanDatabase(cm);
2865
2866
2867  if(t->allsat->assertion) t->lifting->assertion = sat_ArrayDuplicate(t->allsat->assertion);
2868  if(t->allsat->auxObj)    t->lifting->auxObj = sat_ArrayDuplicate(t->allsat->auxObj);
2869
2870  sat_MarkTransitiveFaninForNode(cm, objective, CoiMask);
2871
2872  for(i=0; i<t->csize; i++) {
2873    if(t->coiStates[i]) {
2874      sat_MarkTransitiveFaninForNode(cm, SATnormalNode(t->c2n[i]), CoiMask);
2875    }
2876  }
2877
2878  if(t->tVariables) {
2879    arr = t->tVariables;
2880    for(i=0; i<arr->num; i++) {
2881      v = arr->space[i];
2882      SATflags(v) |= CoiMask;
2883    }
2884  }
2885
2886  if(t->auxObj) {
2887    arr = t->auxObj;
2888    for(i=0; i<arr->num; i++) {
2889      v = arr->space[i];
2890      sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
2891    }
2892  }
2893  return(objective);
2894}
2895
2896/**Function********************************************************************
2897
2898  Synopsis    [Function to clean data of bAigTransition_t generated from previous execution]
2899
2900  Description [Function to clean data of bAigTransition_t generated from previous execution]
2901
2902  SideEffects []
2903
2904  SeeAlso     []
2905
2906******************************************************************************/
2907void
2908bAigCleanUpDataFromPreviousExecution(bAigTransition_t *t)
2909{
2910  if(t->frontier) {
2911    sat_ArrayFree(t->frontier);
2912    t->frontier = 0;
2913  }
2914  if(t->reached) {
2915    sat_ArrayFree(t->reached);
2916    t->reached = 0;
2917  }
2918
2919  t->objective = 0;
2920  t->iteration = 0;
2921  t->nBlocked = 0;
2922  t->sum = 0;
2923  t->avgLits = 0;
2924
2925}
2926/**Function********************************************************************
2927
2928  Synopsis    [Function to print information of bAigTransition_t]
2929
2930  Description [Function to print information of bAigTransition_t]
2931
2932  SideEffects []
2933
2934  SeeAlso     []
2935
2936******************************************************************************/
2937void
2938bAigPrintTransitionInfo(bAigTransition_t *t)
2939{
2940int i;
2941
2942  fprintf(vis_stdout, "Transition relation information in terms of AIG\n");
2943  fprintf(vis_stdout, "objective : %ld\n", t->objective);
2944  fprintf(vis_stdout, "number of primary inputs : %d\n", t->nInputs);
2945  fprintf(vis_stdout, "number of states variables : %d\n", t->nLatches);
2946
2947  fprintf(vis_stdout, "primary inputs :");
2948  for(i=0; i<t->nInputs; i++) {
2949    fprintf(vis_stdout, "%5ld ", t->inputs[i]);
2950    if((i+1)%10 == 0 && i > 0) 
2951      fprintf(vis_stdout, "\n                ");
2952  }
2953  fprintf(vis_stdout, "\n");
2954
2955  fprintf(vis_stdout, "state variables :");
2956  for(i=0; i<t->nLatches; i++) {
2957    fprintf(vis_stdout, "%5ld(%5ld):%5ld ", 
2958            t->cstates[i], t->initials[i], t->nstates[i]);
2959    if((i+1)%3 == 0 && i > 0) 
2960      fprintf(vis_stdout, "\n                 ");
2961  }
2962  fprintf(vis_stdout, "\n");
2963}
2964
2965/**Function********************************************************************
2966
2967  Synopsis    [Function to arrange node to the alphabetic order ]
2968
2969  Description [Function to arrange node to the alphabetic order ]
2970
2971  SideEffects []
2972
2973  SeeAlso     []
2974
2975******************************************************************************/
2976static int
2977nodenameCompare(
2978  const void * node1,
2979  const void * node2)
2980{
2981Ntk_Node_t *v1, *v2;
2982char *name1, *name2;
2983
2984  v1 = *(Ntk_Node_t **)(node1);
2985  v2 = *(Ntk_Node_t **)(node2);
2986  name1 = Ntk_NodeReadName(v1);
2987  name2 = Ntk_NodeReadName(v2);
2988 
2989  return (strcmp(name1, name2));
2990} 
2991
2992/**Function********************************************************************
2993
2994  Synopsis    [Function to check if given string is integer]
2995
2996  Description [Function to check if given string is integer]
2997
2998  SideEffects []
2999
3000  SeeAlso     []
3001
3002******************************************************************************/
3003static int
3004StringCheckIsInteger(
3005  char *string,
3006  int *value)
3007{
3008  char *ptr;
3009  long l;
3010 
3011  l = strtol (string, &ptr, 0) ;
3012  if(*ptr != '\0')
3013    return 0;
3014  if ((l > MAXINT) || (l < -1 - MAXINT))
3015    return 1 ;
3016  *value = (int) l;
3017  return 2 ;
3018}
3019
3020/**Function********************************************************************
3021
3022  Synopsis    [Function to check the deicison level of variable ]
3023
3024  Description [Function to check the deicison level of variable ]
3025
3026  SideEffects []
3027
3028  SeeAlso     []
3029
3030******************************************************************************/
3031static int
3032levelCompare(
3033  const void * node1,
3034  const void * node2)
3035{
3036  bAigEdge_t v1, v2;
3037  int l1, l2;
3038
3039  v1 = *(bAigEdge_t *)(node1);
3040  v2 = *(bAigEdge_t *)(node2);
3041  l1 = SATcm->variableArray[SATnodeID(v1)].level;
3042  l2 = SATcm->variableArray[SATnodeID(v2)].level;
3043 
3044  if(l1 == l2)  return(v1 > v2);
3045  return (l1 > l2);
3046} 
3047/**Function********************************************************************
3048
3049  Synopsis    [Function to check the index ]
3050
3051  Description [Function to check the index ]
3052
3053  SideEffects []
3054
3055  SeeAlso     []
3056
3057******************************************************************************/
3058static int
3059indexCompare(
3060  const void * node1,
3061  const void * node2)
3062{
3063  bAigEdge_t v1, v2;
3064
3065  v1 = *(bAigEdge_t *)(node1);
3066  v2 = *(bAigEdge_t *)(node2);
3067 
3068  return(v1 > v2);
3069} 
3070
Note: See TracBrowser for help on using the repository browser.