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

/**CFile***********************************************************************

  FileName    [smtCnf.c]

  PackageName [smt]

  Synopsis    [Routines for smt function.]

  Author      [Hyondeuk Kim]

  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]
  
******************************************************************************/

#ifdef HAVE_LIBGMP

#include "smt.h"

void
smt_generate_cnf_main(smtManager_t * sm)
{
  int num_bvar, is_cnf = 0;

  sm->num_var = sm->id2var->size - 1; /* id2var starts from index 1 */

  is_cnf = smt_generate_cnf(sm);
  
  num_bvar = sm->bvarArr->size;

  if (is_cnf == 0) {
    smt_free_clauses(sm->clsArr);
    sm->clsArr->size = 0;
    fprintf(stdout, "SMT Formula is not in CNF format\n");
    smt_generate_cnf_with_aig(sm);

    if (sm->obj == Aig_One || sm->obj == Aig_Zero) return;

  } else {
    sm->flag |= CNF_MASK;
  }

  sm->stats->num_inter_bvar = sm->bvarArr->size - num_bvar;

  return;
}

int
smt_generate_cnf(smtManager_t * sm)
{
  smtFml_t * root = sm->fml;
  smtFml_t * fml, * subfml;
  smtQueue_t * Q;
  int is_leaf, is_cnf = 1;
  int i;

  smt_init_generate_cnf(sm);

  Q = smt_create_queue(sm->fmlArr->size);

  smt_enqueue(Q, (long) root);
  
  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {
    is_leaf = smt_is_abstract_leaf_fml(fml);

    if (is_leaf) {
      smt_create_clause_with_fml(sm, fml);
    } else if (fml->type == NOT_c) {
      subfml = (smtFml_t *) fml->subfmlArr->space[0];
      is_leaf = smt_is_abstract_leaf_fml(subfml);
      if (is_leaf) {
        smt_create_clause_with_fml(sm, fml);
      } else {
        subfml->nNeg++; 
        if (!(subfml->flag & QUEUED_MASK)) {
          smt_enqueue(Q, (long) subfml);
          subfml->flag |= QUEUED_MASK;
        }
      }
    } else if (fml->type == OR_c || fml->type == IMP_c || fml->type == IFF_c) {
      is_cnf = smt_create_clause_with_fml(sm, fml);
      if (!is_cnf) {
        smt_none();
        break;
      }
    } else if (fml->type == AND_c) {

      if ((fml->nNeg) % 2 != 0) {
#if 0
        is_cnf = 0;
        break;
#else 
        is_cnf = smt_create_clause_with_fml(sm, fml); 

        if (is_cnf == 0) {
          smt_none();
          break; 
        }
        continue; /* clause is generated : reached leaf */
#endif
      }

      for(i = 0; i < fml->subfmlArr->size; i++) {
        subfml = (smtFml_t *) fml->subfmlArr->space[i];
        if (subfml->nNeg != 0 && ((subfml->nNeg) % 2 != (fml->nNeg) % 2)) {
          /* Neg # dismatch between multiple parent nodes */
          is_cnf = 0;
          smt_none();
          break;
        }
        subfml->nNeg = fml->nNeg;
        
        if (!(subfml->flag & QUEUED_MASK)) {
          smt_enqueue(Q, (long) subfml);
          subfml->flag |= QUEUED_MASK;
        }       
      }
      if (is_cnf==0) {
        smt_none();
        break;
      }
    } else {
      smt_none();
      is_cnf = 0;
      break;
    }
  }

  smt_free_queue(Q);
  
  return is_cnf;
}


#if 1
void
smt_generate_cnf_with_aig(smtManager_t * sm)
{
  sm->obj = smt_generate_aig(sm);    

#if 0
  smt_print_aig_to_dot_file(sm->bm);
#endif

  if (sm->obj == Aig_One || sm->obj == Aig_Zero) 
    return; 

  smt_convert_aig_into_cnf(sm, sm->obj);

  return;
}


AigEdge_t
smt_generate_aig(smtManager_t * sm)
{
  Aig_Manager_t * bm;
  smtFml_t * root = 0, * fml = 0;
  smtFml_t * subfml_a, * subfml_b, * subfml_c;
  smtAvar_t * avar;
  smtBvar_t * bvar;
  AigEdge_t aig_node = Aig_NULL, cond = Aig_NULL;
  AigEdge_t left = Aig_NULL, right = Aig_NULL;
  satArray_t * fmlArr;
  array_t * aig_nodeArr;
  int i, nfml;
  char * name; 
    
  bm = Aig_initAig(6000);
  
  sm->bm = bm;

  root = sm->fml;

  if (root == 0) {
    return Aig_NULL;
  }
   
  fmlArr = smt_sort_formula_in_bfs_manner(sm, root);

  nfml = fmlArr->size;
  
  /* start from leaf formula to root formula */
  for(i = nfml - 1; i >= 0; i--) {
    fml = (smtFml_t *) fmlArr->space[i];
    
    if (fml->flag & TRUE_MASK) {
      aig_node = Aig_One;

    } else if (fml->flag & FALSE_MASK) {
      aig_node = Aig_Zero;

    } else if (fml->type == PRED_c || fml->type == FVAR_c) {
      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      name = util_strsav((char *) subfml_a);
      aig_node = Aig_FindNodeByName(bm, name);
      
      if (aig_node == Aig_NULL) {
        aig_node = Aig_CreateVarNode(bm, name);
        bvar = fml->bvar;
        bvar->aig_node = aig_node;
      } else { 
        free(name);
      }

    } else if (fml->type == NOT_c) {
      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      if (subfml_a->aig_node != Aig_NULL)
        aig_node = Aig_Not(subfml_a->aig_node);
      else
        exit(0);
    } else if (fml->type == IMP_c) {
      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
      if (subfml_a->aig_node != Aig_NULL)
        left = subfml_a->aig_node;
      else
        exit(0);
      
      if (subfml_b->aig_node != Aig_NULL)
        right = subfml_b->aig_node;
      else
        exit(0);
      
      aig_node = Aig_Then(bm, left, right);
    } else if (fml->type == IFF_c) {

      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];

      if (subfml_a->aig_node != Aig_NULL)
        left = subfml_a->aig_node;
      else
        exit(0);
      
      if (subfml_b->aig_node != Aig_NULL)
        right = subfml_b->aig_node;
      else
        exit(0);
      
      aig_node = Aig_Eq(bm, left, right);
#if 0 
      /* only iff fml with leaf children : bug */
      if ( Aig_isVarNode(bm, left) && Aig_isVarNode(bm, right) ) 
        sm->iff_fmlArr = sat_array_insert(sm->iff_fmlArr, (long) fml);
#endif
    } else if (fml->type == AND_c) {
      aig_nodeArr = smt_gather_aig_node_from_formula_array(fml->subfmlArr);
      aig_node = Aig_AndsInBFSManner(bm, aig_nodeArr);
      array_free(aig_nodeArr);

    } else if (fml->type == OR_c) {
      aig_nodeArr = smt_gather_aig_node_from_formula_array(fml->subfmlArr);
      aig_node = Aig_OrsInBFSManner(bm, aig_nodeArr);
      array_free(aig_nodeArr);

    } else if (fml->type == XOR_c) {
      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
      
      if (subfml_a->aig_node != Aig_NULL)
        left = subfml_a->aig_node;
      else
        exit(0);
      
      if (subfml_b->aig_node != Aig_NULL)
        right = subfml_b->aig_node;
      else
        exit(0);
      
      aig_node = Aig_Xor(bm, left, right);

    } else if (fml->type == NAND_c) {
      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
      if (subfml_a->aig_node != Aig_NULL)
        left = subfml_a->aig_node;
      else
        exit(0);
      
      if (subfml_b->aig_node != Aig_NULL)
        right = subfml_b->aig_node;
      else
        exit(0);
      
      aig_node = Aig_Nand(bm, left, right);

    } else if (fml->type == ITE_c) {
      subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
      subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
      subfml_c = (smtFml_t *) fml->subfmlArr->space[2];
      
      if (subfml_a->aig_node != Aig_NULL)
        cond = subfml_a->aig_node;
      else
        exit(0);
      
      if (subfml_b->aig_node != Aig_NULL)
        left = subfml_b->aig_node;
      else
        exit(0);
      
      if (subfml_c->aig_node != Aig_NULL)
        right = subfml_c->aig_node;
      else
        exit(0);

      aig_node = Aig_Ite(bm, cond, left, right);
#if 0 /* bug */
      is_terminal = smt_is_ite_terminal_case(cond, left, right);

      if (!is_terminal)
        sm->ite_fmlArr = sat_array_insert(sm->ite_fmlArr, (long) fml);
#endif
    } else if (smt_is_atom_formula(fml)) {

      avar = fml->avar;
      name = util_strsav(avar->name);
      aig_node = Aig_FindNodeByName(bm, name);

      if (aig_node == Aig_NULL) {
        aig_node = Aig_CreateVarNode(bm, name);
        subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
        subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
        avar->aig_node = aig_node;
      } else {
        free(name);
      }

    } else {
      fprintf(stdout, "ERROR: No Formula type in AIG type\n");
      fprintf(stdout, "unknown\n");
      exit(0);
    }

    fml->aig_node = aig_node;
  }

  if (fmlArr) free(fmlArr);

  aig_node = fml->aig_node;
  
  return aig_node;
}

int
smt_is_ite_terminal_case(
  AigEdge_t cond_node, 
  AigEdge_t then_node, 
  AigEdge_t else_node)
{
  AigEdge_t node_a, node_b, node_c;

  if (cond_node == Aig_One || cond_node == Aig_Zero ||
      then_node == Aig_One || then_node == Aig_Zero ||
      else_node == Aig_One || else_node == Aig_Zero)
    return 1;

  node_a = Aig_NonInvertedEdge(cond_node);
  node_b = Aig_NonInvertedEdge(then_node);
  node_c = Aig_NonInvertedEdge(else_node);
      
  if (node_a == node_b || node_a == node_c || node_b == node_c)
    return 1;

  return 0;
}

void
smt_convert_aig_into_cnf(smtManager_t * sm, AigEdge_t node)
{
  array_t * idArr = array_alloc(int, 10);;
  int negated = 0;

  smt_compute_indegree_for_aig_node(sm);
  
  smt_init_var_id_for_aig_node(sm);
#if 0 /* bug */
  /* mapping ite & iff aig_node to fml */
  smt_check_leaf_node_for_aig_node(sm);
#endif
  smt_convert_aig_into_cnf_sub(sm, node, idArr, &negated);

  smt_add_clause_for_object(sm, node);

  smt_add_clause_for_iff_fml(sm);
  sm->iff_fmlArr->size = 0;
  
  smt_add_clause_for_ite_fml(sm); 
  sm->ite_fmlArr->size = 0;
  
  array_free(idArr);
  
  return;
}

void
smt_compute_indegree_for_aig_node(smtManager_t * sm)
{
  Aig_Manager_t * bm = sm->bm;
  AigEdge_t v, left, right;
  int nodes_size, index;

  nodes_size = bm->nodesArraySize/AigNodeSize;

  sm->node2ins = (int *) malloc(sizeof(int) * nodes_size);

  memset(sm->node2ins, 0, sizeof(int) * nodes_size);

  for(v = AigFirstNodeIndex ; v < bm->nodesArraySize; v+=AigNodeSize){
    left = leftChild(v);
    right = rightChild(v);  
    
    if (left != Aig_NULL && left != Aig_One && left != Aig_Zero) {
      if (Aig_IsInverted(left)) left = Aig_NonInvertedEdge(left);
      assert(left);
      index = AigNodeID(left) - 1;
      sm->node2ins[index]++;
    }

    if (right != Aig_NULL && right != Aig_One && right != Aig_Zero) {
      if (Aig_IsInverted(right)) right = Aig_NonInvertedEdge(right);
      assert(right);
      index = AigNodeID(right) - 1;
      sm->node2ins[index]++;
    }
  }
  
  return;
}

void
smt_init_var_id_for_aig_node(smtManager_t * sm)
{
  Aig_Manager_t * bm = sm->bm;
  AigEdge_t node;
  smtAvar_t * avar;
  smtBvar_t * bvar;
  int nodes_size, index, i;

  nodes_size = bm->nodesArraySize/AigNodeSize;

  sm->node2id = (int *) malloc(sizeof(int) * nodes_size);

  memset(sm->node2id, 0, sizeof(int) * nodes_size);

  sm->aig_zero_id = INT_MAX - 2;
  
  sm->aig_one_id = INT_MAX - 1; 
  
  sm->aig_none = INT_MAX;

  /* var id for avar */
  for(i = 0; i < sm->avarArr->size; i++) {
    avar = (smtAvar_t *) sm->avarArr->space[i];
    node = avar->aig_node;
#if 1
    if (node == Aig_NULL) continue;
#endif
    assert(node != Aig_NULL); /* node may not be assigned due to ite red */
    index = AigNodeID(node) - 1;
    sm->node2id[index] = avar->id;
  }

  /* var id for bvar */
  for(i = 0; i < sm->bvarArr->size; i++) {
    bvar = (smtBvar_t *) sm->bvarArr->space[i];
    node = bvar->aig_node;
    assert(node != Aig_NULL || bvar->flag & BTRUE_MASK || 
           bvar->flag & BFALSE_MASK);
    if (!node) continue;
    index = AigNodeID(node) - 1;
    sm->node2id[index] = bvar->id;
  }
}

void
smt_check_leaf_node_for_aig_node(smtManager_t * sm)
{
  Aig_Manager_t * bm = sm->bm;
  AigEdge_t node;
  smtFml_t * ite_fml, * iff_fml;
  /* satArray_t * ite_fmlArr, * iff_fmlArr; */
  int nodes_size, index, i;

  nodes_size = bm->nodesArraySize/AigNodeSize;

  sm->node2fml = (smtFml_t **) malloc(sizeof(smtFml_t *) * nodes_size);

  memset(sm->node2fml, 0, sizeof(smtFml_t *) * nodes_size);

  /* check ite node as a leaf node in aig */
  for(i = 0; i < sm->ite_fmlArr->size; i++) {
    ite_fml = (smtFml_t *) sm->ite_fmlArr->space[i];
    node = ite_fml->aig_node;
    if (node == Aig_One || node == Aig_Zero) continue;
    assert(node != Aig_NULL); 
    index = AigNodeID(node) - 1;
    if (sm->node2fml[index] == 0) sm->node2fml[index] = ite_fml;
  }

  /* check iff node as a leaf node in aig */
  for(i = 0; i < sm->iff_fmlArr->size; i++) {
    iff_fml = (smtFml_t *) sm->iff_fmlArr->space[i];
    node = iff_fml->aig_node;
    if (node == Aig_One || node == Aig_Zero) continue;
    assert(node != Aig_NULL); 
    index = AigNodeID(node) - 1;
    if (sm->node2fml[index] == 0) sm->node2fml[index] = iff_fml;
  }

  sm->ite_fmlArr->size = 0;
  sm->iff_fmlArr->size = 0;
}

satArray_t *
smt_sort_formula_in_bfs_manner(smtManager_t * sm, smtFml_t * root)
{
  smtFml_t * fml, * tfml;
  smtQueue_t * Q;
  satArray_t * fmlArr = sat_array_alloc(1024);
  int i, is_leaf, id;

  smt_compute_indegree_in_formula(sm);

  Q = smt_create_queue(sm->fmlArr->size);
  
  /* id = sm->avarArr->size + sm->bvarArr->size + 1; */
  id = sm->id2var->size;
  root->id = id;
  fmlArr = sat_array_insert(fmlArr, (long) root);

  smt_enqueue(Q, (long) root);
   
  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {

      is_leaf = smt_is_abstract_leaf_fml(fml);

    if ( (!is_leaf) ) {
      for(i = 0; i < fml->subfmlArr->size; i++) {
        tfml = (smtFml_t *) fml->subfmlArr->space[i];
        tfml->ins--;

        if (tfml->ins <= 0) {
          if (!tfml->avar && !tfml->bvar) {
            /* intermediate variable */
            id++;
            tfml->id = id;
            smt_enqueue(Q, (long) tfml);
          } else {
            if (tfml->bvar) tfml->id = tfml->bvar->id;
            else if (tfml->avar) tfml->id = tfml->avar->id;
            else exit(0);
          } 
          fmlArr = sat_array_insert(fmlArr, (long) tfml);
        }
      }
    }
  }

  if(Q) smt_free_queue(Q);

  return fmlArr;
}

void
smt_compute_indegree_in_formula(smtManager_t * sm)
{
  smtFml_t * root, * fml, * tfml;
  smtQueue_t * Q;
  int i, is_leaf;
  
  for(i = 0; i < sm->fmlArr->size; i++) {
    tfml = (smtFml_t *) sm->fmlArr->space[i];
    tfml->ins = 0; 
  }
  
  Q = smt_create_queue(sm->fmlArr->size);

  root = sm->fml;
  
  smt_enqueue(Q, (long) root);

  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {
    
    is_leaf = smt_is_abstract_leaf_fml(fml);

    if ( (!is_leaf) ) {
      for(i = 0; i < fml->subfmlArr->size; i++) {
        tfml = (smtFml_t *) fml->subfmlArr->space[i];
        if (tfml->ins == 0) {
          smt_enqueue(Q, (long) tfml);
        }
        tfml->ins++;
      }
    }
  }

  if(Q) smt_free_queue(Q);

  return;
}

array_t *
smt_gather_aig_node_from_formula_array(satArray_t * fmlArr)
{
  smtFml_t * tfml;
  int i;
  array_t * aig_nodeArr = array_alloc(AigEdge_t, fmlArr->size);

  for(i = 0; i < fmlArr->size; i++) {
    tfml = (smtFml_t *) fmlArr->space[i];
    array_insert_last(AigEdge_t, aig_nodeArr, tfml->aig_node);    
  }

  return aig_nodeArr;
}

int
smt_convert_aig_into_cnf_sub(
  smtManager_t * sm,
  AigEdge_t node,
  array_t * idArr, /* contains conjuncts in big AND */
  int * negated)
{
  Aig_Manager_t * bm = sm->bm;
  AigEdge_t left, right;
  int var_id, lvar_id, rvar_id;
  int cur_index;
 
  assert(node != Aig_One && node != Aig_Zero);

  if (Aig_IsInverted(node)) {
    *negated = 1;
    node = Aig_NonInvertedEdge(node);
    return -1 * smt_convert_aig_into_cnf_sub(sm, node, idArr, negated);
  }

  if (smt_add_var_id_for_node(sm, node, &var_id, negated)){
    return var_id; /* node is a leaf or already visited */
  }

  cur_index = idArr->num; /* save current idx in idArr */

  left = leftChild(node);
  right = rightChild(node);
  
  /* get left child var id */
  if (left == Aig_One) 
    lvar_id = sm->aig_one_id;
  else if (left == Aig_Zero)
    lvar_id = sm->aig_zero_id;
  else
    lvar_id = smt_convert_aig_into_cnf_sub(sm, left, idArr, negated);

  /* right child var id */
  if (right == Aig_One)
    rvar_id = sm->aig_one_id;
  else if (right == Aig_Zero) 
    rvar_id = sm->aig_zero_id;
  else
    rvar_id = smt_convert_aig_into_cnf_sub(sm, right, idArr, negated);
   
  if (var_id == 0) { /* no var_id for the node */
    if (lvar_id == sm->aig_zero_id) {
      array_insert_last(int, idArr, 0); /* obj is false */
    } else if (lvar_id == sm->aig_one_id) {
      /* nop */
    } else if (lvar_id != sm->aig_none) {
      assert(lvar_id != 0);
      array_insert_last(int, idArr, lvar_id);
    }

    if (rvar_id == sm->aig_zero_id) {
      array_insert_last(int, idArr, 0); /* obj is false */
    } else if (rvar_id == sm->aig_one_id) {
      /* nop */
    } else if (rvar_id != sm->aig_none) {
      assert(rvar_id != 0);
      array_insert_last(int, idArr, rvar_id);
    }

    return sm->aig_none;
  } else {
    smt_generate_clause_with_aig(sm, cur_index, var_id, 
                                 lvar_id, rvar_id, idArr);
    
    return var_id;
  }
}

int
smt_add_var_id_for_node(
  smtManager_t * sm,                                        
  AigEdge_t node,
  int * var_id,
  int * negated)
{
  Aig_Manager_t * bm = sm->bm;
  smtFml_t * fml = 0;
  smtBvar_t * bvar;
  int index;

  index = AigNodeID(node) - 1;

  /* check if node is not negated and not var node */ 
  if ( node != sm->obj && !Aig_isVarNode(sm->bm, node) && 
       (sm->node2fml == 0 || sm->node2fml[index] == 0) &&
       !*negated && node != Aig_One && node != Aig_Zero && 
       sm->node2ins[index] == 1 ) {

    /* does it matter if not fanout free? */
    *var_id = 0;  /* no new intermediate var */
    return 0;

  } 

  if (*negated == 1) *negated = 0; /* reset negated flag */

  if (sm->node2id[index] != 0) { 

    *var_id = sm->node2id[index]; 
    if (sm->node2fml) fml = sm->node2fml[index];

    if ( node != sm->obj || Aig_isVarNode(sm->bm, node) ||
         (sm->node2fml && fml != 0) ) { /* iff & ite case */
      return 1; /* node is a leaf or already visited */
    } else { 
      /* sm->obj = ite node child : node created, but never visited */
      return 0;
    }

  } else {

    /* new intermediate var */
    bvar = smt_create_intermediate_bool_variable(sm, node);
    sm->node2id[index] = bvar->id; 
    *var_id = bvar->id;
    if (sm->node2fml) fml = sm->node2fml[index];

    if ( Aig_isVarNode(bm, node) || (sm->node2fml && fml != 0) ) {

      if (fml) { /* iff & ite case */
        if (fml->type == ITE_c) 
          sm->ite_fmlArr = sat_array_insert(sm->ite_fmlArr, (long) fml);
        else if (fml->type == IFF_c) 
          sm->iff_fmlArr = sat_array_insert(sm->iff_fmlArr, (long) fml);
      }

      return 1; /* iff & ite case */
    } else
      return 0;
  }
}

void
smt_generate_clause_with_aig(
  smtManager_t * sm, 
  int cur_index,
  int var_id, 
  int lvar_id, 
  int rvar_id, 
  array_t * idArr)
{
  smtCls_t * cls, * cls_a;
  int aig_one, aig_zero, aig_none;
  int id, i;

  aig_one = sm->aig_one_id;
  aig_zero = sm->aig_zero_id;
  aig_none = sm->aig_none;

  /** --conditions--
      lvar_id: aig_one, aig_zero, var_id, idArr
      rvar_id: aig_one, aig_zero, var_id, idArr 
      lvar_id == aig_one, lvar_id == aig_zero, lvar_id != 0, lvar_id == 0
      rvar_id == aig_one, rvar_id == aig_zero, rvar_id != 0, rvar_id == 0
  **/

  if (lvar_id == aig_one && rvar_id == aig_one) {
    /* cls:(var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (lvar_id == aig_one && rvar_id == aig_zero) {
    /* cls:(-var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (lvar_id == aig_one && rvar_id != aig_none) {
    /* cls:(-rvar_id + var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -rvar_id);
    cls->litArr = sat_array_insert(cls->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* cls:(rvar_id + -var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, rvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (lvar_id == aig_one && rvar_id == aig_none && 
             !(rvar_id == aig_one || rvar_id == aig_zero)) { 
    assert(idArr->num >= cur_index);
    cls_a = smt_create_clause();

    for(i = cur_index; i < idArr->num; i++) {   
      id = array_fetch(int, idArr, i);
      /* cls set1: var_id -> (r1 * r2)  */
      cls = smt_create_clause();
      cls->litArr = sat_array_insert(cls->litArr, id);
      cls->litArr = sat_array_insert(cls->litArr, -var_id);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      /* clasue set2: -var_id -> (-r1 + -r2) */
      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
    }
    idArr->num = cur_index;
    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);

  } else if (lvar_id == aig_zero) {
    /* cls:(-var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  }  else if (lvar_id == aig_none && rvar_id == aig_one && 
             !(lvar_id == aig_one || lvar_id == aig_zero)) {
    assert(idArr->num >= cur_index);
    cls_a = smt_create_clause();

    for(i = cur_index; i < idArr->num; i++) {   
      id = array_fetch(int, idArr, i);
      /* cls set1: var_id -> (l1 * l2)  */
      cls = smt_create_clause();
      cls->litArr = sat_array_insert(cls->litArr, id);
      cls->litArr = sat_array_insert(cls->litArr, -var_id);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      /* clasue set2: -var_id -> (-l1 + -l2) */
      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
    }
    idArr->num=cur_index;
    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);

  } else if (lvar_id == aig_none && rvar_id == aig_zero &&
             !(lvar_id == aig_one || lvar_id == aig_zero)) {
    /* cls:(-var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (lvar_id == aig_none && rvar_id != aig_none &&
           !(lvar_id == aig_one || lvar_id == aig_zero)) {
    assert(idArr->num >= cur_index);
    cls_a = smt_create_clause();
    for(i = cur_index; i < idArr->num; i++) {   
      id = array_fetch(int, idArr, i);
      /* cls set1: var_id -> ((l1 * l2) * rvar_id)  */
      cls = smt_create_clause();
      cls->litArr = sat_array_insert(cls->litArr, id);
      cls->litArr = sat_array_insert(cls->litArr, -var_id);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      /* clasue set2: -var_id -> ((-l1 + -l2) + -rvar_id)*/
      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
    }
    idArr->num = cur_index;
    /* cls set1: var_id -> ((l1 * l2) * rvar_id)  */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, rvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* clasue set2: -var_id -> ((-l1 + -l2) + -rvar_id)*/
    cls_a->litArr = sat_array_insert(cls_a->litArr, -rvar_id);
    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);

  } else if (lvar_id == aig_none && rvar_id == aig_none && 
             !(lvar_id == aig_one || lvar_id == aig_zero) && 
             !(rvar_id == aig_one || rvar_id == aig_zero)) {
    assert(idArr->num >= cur_index);
    cls_a = smt_create_clause();
    for(i = cur_index; i < idArr->num; i++) {   
      id = array_fetch(int, idArr, i);
      /* cls set1: var_id -> ((l1 * l2) * (r1 * r2))  */
      cls = smt_create_clause();
      cls->litArr = sat_array_insert(cls->litArr, id);
      cls->litArr = sat_array_insert(cls->litArr, -var_id);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      /* clasue set2: -var_id -> ((-l1 + -l2) + (-r1 + -r2))*/
      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
    }
    idArr->num = cur_index;
    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);

  } else if (lvar_id != aig_none && rvar_id == aig_one) {
    /* cls:(-lvar_id + var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -lvar_id);
    cls->litArr = sat_array_insert(cls->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* cls:(lvar_id + -var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, lvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (lvar_id != aig_none && rvar_id == aig_zero) {
    /* cls:(-var_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (lvar_id != aig_none && rvar_id == aig_none &&
             !(rvar_id == aig_one || rvar_id == aig_zero)) {
    assert(idArr->num >= cur_index);
    cls_a = smt_create_clause();
    for(i = cur_index; i < idArr->num; i++) {   
      id = array_fetch(int, idArr, i);
      /* cls set1: var_id -> ((r1 * r2) * lvar_id)  */
      cls = smt_create_clause();
      cls->litArr = sat_array_insert(cls->litArr, id);
      cls->litArr = sat_array_insert(cls->litArr, -var_id);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      /* clasue set2: -var_id -> ((-r1 + -r2) + -lvar_id)*/
      cls_a->litArr = sat_array_insert(cls_a->litArr, -id);
    }
    idArr->num = cur_index;
    /* cls set1: var_id -> ((r1 * r2) * lvar_id)  */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, lvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* clasue set2: -var_id -> ((-r1 + -r2) + -lvar_id)*/
    cls_a->litArr = sat_array_insert(cls_a->litArr, -lvar_id);
    cls_a->litArr = sat_array_insert(cls_a->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls_a);

  }  else if (lvar_id != aig_none && rvar_id != aig_none) {
    /* cls set1: -var_id -> (-lvar_id + -rvar_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -lvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -rvar_id);
    cls->litArr = sat_array_insert(cls->litArr, var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* cls set2: var_id -> (lvar_id * rvar_id) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, lvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, rvar_id);
    cls->litArr = sat_array_insert(cls->litArr, -var_id);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else {
    smt_none();
    fprintf(stdout, "ERROR: WRONG AIG TO CNF\n");
    exit(0);
  }
}

void
smt_add_clause_for_object(smtManager_t * sm, AigEdge_t obj)
{
  smtCls_t * cls;
  int index, id, lit;

  index = AigNodeID(obj) - 1;

  id = sm->node2id[index];

  if(Aig_IsInverted(obj)) lit = -id;
  else lit = id;

  cls = smt_create_clause();

  cls->litArr = sat_array_insert(cls->litArr, lit);

  sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
}

void
smt_add_clause_for_iff_fml(smtManager_t * sm)
{
  smtFml_t * fml, * subfml_a, * subfml_b;
  smtBvar_t * bvar;
  array_t * idArr = array_alloc(int, 10);;
  AigEdge_t iff_node, node_a, node_b, obj;
  int i, index, negated;
  int x, y, f;

  obj = sm->obj; /* save obj : sm->obj is temporally used for iff child */
  
  for(i = 0; i < sm->iff_fmlArr->size; i++) {
    fml = (smtFml_t *) sm->iff_fmlArr->space[i];
    subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
    subfml_b = (smtFml_t *) fml->subfmlArr->space[1];

    iff_node = fml->aig_node;
    node_a = subfml_a->aig_node;
    node_b = subfml_b->aig_node;
    assert(iff_node != Aig_NULL);
    assert(node_a != Aig_NULL);
    assert(node_b != Aig_NULL);

    /* iff: f */
    index = AigNodeID(iff_node) - 1;
    f = sm->node2id[index]; 
    if (f == 0) {
      /* nested iff fml: new intermediate var */
      bvar = smt_create_intermediate_bool_variable(sm, iff_node);
      f = bvar->id;
      sm->node2id[index] = f; 
    }

    /* child_a: x */
    if (node_a == Aig_One) 
      x = sm->aig_one_id;
    else if (node_a == Aig_Zero)
      x = sm->aig_zero_id;
    else {
      index = AigNodeID(node_a) - 1;
      x = sm->node2id[index]; 

      if (x == 0) {
        idArr->num = 0;
        negated = 0;
        sm->obj = Aig_NonInvertedEdge(node_a);
        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
        x = sm->node2id[index]; 
        assert(x);
      }

      if (Aig_IsInverted(node_a)) 
        x = -x;
    }
    
    /* child_b: y */
    if (node_b == Aig_One) 
      y = sm->aig_one_id;
    else if (node_b == Aig_Zero)
      y = sm->aig_zero_id;
    else {
      index = AigNodeID(node_b) - 1;
      y = sm->node2id[index]; 

      if (y == 0) {
        idArr->num = 0;
        negated = 0;
        sm->obj = Aig_NonInvertedEdge(node_b);
        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
        y = sm->node2id[index]; 
        assert(y);
      }
      
      if (Aig_IsInverted(node_b)) 
        y = -y;
    }

    smt_add_clause_for_iff_fml_sub(sm, f, x, y); 
  }

  sm->obj = obj; /* restore obj */
  array_free(idArr);

  return;
}

void
smt_add_clause_for_iff_fml_sub(smtManager_t * sm, int f, int x, int y)
{
  smtCls_t * cls;

  /* (f -> (x = y)) /\ (f' -> (x = y)') */
  
  if ((x == sm->aig_one_id && y == sm->aig_one_id) ||
      (x == sm->aig_zero_id && y == sm->aig_zero_id)) {
    /* (f) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);

  } else if ((x == sm->aig_one_id && y == sm->aig_zero_id) ||
             (x == sm->aig_zero_id && y == sm->aig_one_id)) {
    /* (f') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);

  } else if (x == sm->aig_one_id) {
    /* (f' \/ y) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f \/ y') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (x == sm->aig_zero_id) {
    /* (f' \/ y') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f \/ x \/ y) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (y == sm->aig_one_id) {
    /* (f' \/ x) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f \/ x') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (y == sm->aig_zero_id) {
    /* (f' \/ x') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f \/ x) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else {
    /* (f' \/ x' \/ y) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f' \/ x \/ y') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f \/ x' \/ y') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (f \/ x \/ y) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }

  return;
}

void
smt_add_clause_for_iff_children(
  smtManager_t * sm, 
  AigEdge_t node_a, 
  AigEdge_t node_b)
{
  Aig_Manager_t  * bm = sm->bm;
  array_t * idArr = array_alloc(int, 10);
  int index, negated;

  /* generate cnf for subfmls of ite fml */

  if (node_a != Aig_NULL && node_a != Aig_One && node_a != Aig_Zero) {
    idArr->num = 0;
    negated = 0;
    index = AigNodeID(node_a) - 1;
    sm->obj = Aig_NonInvertedEdge(node_a);
#if 1
    if ( !Aig_isVarNode(bm, sm->obj) && sm->node2fml[index] == 0 &&
         sm->obj != Aig_One && sm->obj != Aig_Zero )
      smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
#endif
  }

  if (node_b != Aig_NULL && node_b != Aig_One && node_b != Aig_Zero) {
    idArr->num = 0;
    negated = 0;
    index = AigNodeID(node_b) - 1;
    sm->obj = Aig_NonInvertedEdge(node_b);
#if 1
    if ( !Aig_isVarNode(bm, sm->obj) && sm->node2fml[index] == 0 &&
         sm->obj != Aig_One && sm->obj != Aig_Zero )
      smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
#endif
  }

  array_free(idArr);

  return;
}

void
smt_add_clause_for_ite_fml(smtManager_t * sm)
{
  /* require checking aig_one & aig_zero */
  smtFml_t * fml, * subfml_a, * subfml_b, * subfml_c;
  array_t * idArr = array_alloc(int, 10);
  AigEdge_t ite_node, node_a, node_b, node_c, obj;
  int x, y, z, f;
  int i, index, negated;
  
  obj = sm->obj; /* save obj : sm->obj is temporally used for ite child */

  for(i = 0; i < sm->ite_fmlArr->size; i++) {
    fml = (smtFml_t *) sm->ite_fmlArr->space[i];
    subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
    subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
    subfml_c = (smtFml_t *) fml->subfmlArr->space[2];

    ite_node = fml->aig_node;
    node_a = subfml_a->aig_node;
    node_b = subfml_b->aig_node;
    node_c = subfml_c->aig_node;
    assert(ite_node != Aig_NULL);
    assert(node_a != Aig_NULL);
    assert(node_b != Aig_NULL);
    assert(node_c != Aig_NULL);

    /* ite: f */
    if (ite_node == Aig_One || ite_node == Aig_Zero) continue;
    index = AigNodeID(ite_node) - 1;
    f = sm->node2id[index];

    assert(f);

    /* child_a: x */
    if (node_a == Aig_One) 
      x = sm->aig_one_id;
    else if (node_a == Aig_Zero)
      x = sm->aig_zero_id;
    else {
      index = AigNodeID(node_a) - 1;
      x = sm->node2id[index]; 

      if (x == 0) {
#if 1
        idArr->num = 0;
        negated = 0;
        sm->obj = Aig_NonInvertedEdge(node_a);
        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
        x = sm->node2id[index]; 
        assert(x);
#endif
      }
      
      if (Aig_IsInverted(node_a)) 
        x = -x;
    }

    /* child_b: y */
    if (node_b == Aig_One) 
      y = sm->aig_one_id;
    else if (node_b == Aig_Zero)
      y = sm->aig_zero_id;
    else {
      index = AigNodeID(node_b) - 1;
      y = sm->node2id[index]; 
      
      if (y == 0) {
#if 1
        idArr->num = 0;
        negated = 0;
        sm->obj = Aig_NonInvertedEdge(node_b);
        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
        y = sm->node2id[index]; 
        assert(y);
#endif
      }
      
      if (Aig_IsInverted(node_b)) 
        y = -y;
    }

    /* child_c: z */
    if (node_c == Aig_One) 
      z = sm->aig_one_id;
    else if (node_c == Aig_Zero)
      z = sm->aig_zero_id;
    else {
      index = AigNodeID(node_c) - 1;
      z = sm->node2id[index]; 
      if (z == 0) {
#if 1
        idArr->num = 0;
        negated = 0;
        sm->obj = Aig_NonInvertedEdge(node_c);
        smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
        z = sm->node2id[index]; 
        assert(z);
#endif
      }
      
      if (Aig_IsInverted(node_c)) 
        z = -z;
    }

    /*fprintf(stdout, "aig=%ld x=%d y=%d z=%d f=%d\n", 
      fml->aig_node, x, y, z, f);*/

    smt_add_clause_for_ite_fml_sub(sm, x, y, z, f);
  }

  sm->obj = obj; /* restore obj */
  array_free(idArr);

  return;
}

void
smt_add_clause_for_ite_fml_sub(
  smtManager_t * sm, 
  int x, 
  int y, 
  int z, 
  int f)
{
  smtCls_t * cls;
  
  assert(f > 0);
  /* f = ite (x, y, z) */
  if ( !smt_add_clause_for_ite_terminal_case(sm, x, y, z, f) ) {

    assert(x != sm->aig_one_id && x != sm->aig_zero_id);
    assert(y != sm->aig_one_id && y != sm->aig_zero_id);
    assert(z != sm->aig_one_id && z != sm->aig_zero_id);
    assert(f != sm->aig_one_id && f != sm->aig_zero_id);

    /* ((x /\ y) -> f); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* ((x /\ y') -> f'); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* ((x' /\ z) -> f) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    cls->litArr = sat_array_insert(cls->litArr, -z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* ((x' /\ z') -> f') */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    cls->litArr = sat_array_insert(cls->litArr, z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }

  return;
}

int
smt_add_clause_for_ite_terminal_case(
  smtManager_t * sm, 
  int x, 
  int y, 
  int z, 
  int f)
{
  smtCls_t * cls = 0;

  assert( (x >= -sm->num_var && x <= sm->num_var) || 
          x == sm->aig_one_id || x == sm->aig_zero_id );
  assert( (y >= -sm->num_var && y <= sm->num_var) || 
          y == sm->aig_one_id || y == sm->aig_zero_id);
  assert( (z >= -sm->num_var && z <= sm->num_var) || 
          z == sm->aig_one_id || z == sm->aig_zero_id);
  assert( (f >= -sm->num_var && f <= sm->num_var) || 
          f == sm->aig_one_id || f == sm->aig_zero_id);

  /* if (f == x || f == -x || f == y || f == -y || f == z || f == -z) 
     return 1; */

  if ( (x == sm->aig_one_id && y == sm->aig_one_id) ||
       (x == sm->aig_zero_id && z == sm->aig_zero_id) ||
       (y == sm->aig_one_id && z == sm->aig_one_id) ) { 
    /* (f); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if ( (x == sm->aig_one_id && y == sm->aig_zero_id) || 
              (x == sm->aig_zero_id && z == sm->aig_one_id) ||
              (y == sm->aig_zero_id && z == sm->aig_zero_id) ) { 
    /* (-f); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if ( x == sm->aig_one_id ) {
    /* (f <-> y); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if ( x == sm->aig_zero_id ) {
    /* (f <-> z); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if ( y == sm->aig_one_id && z == sm->aig_zero_id ) {
    /* (f <-> x); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if ( y == sm->aig_zero_id && z == sm->aig_one_id ) {
    /* (f <-> -x); */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (y == sm->aig_one_id) {
    /* (f <-> (x \/ z)) */
    /* (f -> (x \/ z)) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    cls->litArr = sat_array_insert(cls->litArr, z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (-f -> -x) /\ (-f -> -z) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (y == sm->aig_zero_id) {
    /* (f <-> (-x /\ z)) */
    /* (f -> -x) /\ (f -> z) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

    /* (-f -> (x \/ -z)) */
    cls = smt_create_clause();    
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    cls->litArr = sat_array_insert(cls->litArr, -z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (z == sm->aig_one_id) {
    /* (f <-> (-x \/ y)) */
    /* (f -> (-x \/ y)) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (-f -> x) /\ (-f -> -y) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (z == sm->aig_zero_id) {
    /* (f <-> (x /\ y)) */
    /* (f -> x) /\ (f -> y) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, x);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, -f);
    cls->litArr = sat_array_insert(cls->litArr, y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    /* (-f -> (-x \/ -y)) */
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, f);
    cls->litArr = sat_array_insert(cls->litArr, -x);
    cls->litArr = sat_array_insert(cls->litArr, -y);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }

  if (cls) return 1;
  else return 0;
}

void
smt_add_clause_for_ite_children(
  smtManager_t * sm, 
  AigEdge_t node_a, 
  AigEdge_t node_b, 
  AigEdge_t node_c)
{
  array_t * idArr = array_alloc(int, 10);
  int negated;

  /* generate cnf for subfmls of ite fml */
  if (node_a != Aig_NULL && node_a != Aig_One && node_a != Aig_Zero) {
    idArr->num = 0;
    negated = 0;
    sm->obj = Aig_NonInvertedEdge(node_a);
    smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
  }
   
  if (node_b != Aig_NULL && node_b != Aig_One && node_b != Aig_Zero) {
    idArr->num = 0;
    negated = 0;
    sm->obj = Aig_NonInvertedEdge(node_b);
    smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
  }

  if (node_c != Aig_NULL && node_c != Aig_One && node_c != Aig_Zero) {
    idArr->num = 0;
    negated = 0;
    sm->obj = Aig_NonInvertedEdge(node_c);
    smt_convert_aig_into_cnf_sub(sm, sm->obj, idArr, &negated);
  }

  array_free(idArr);

  return;
}

void
smt_add_clause_for_ite_chain_fml_main(smtManager_t * sm)
{
  smtFml_t * fml;
  int i;
  
  for(i = 0; i < sm->ite_fmlArr->size; i++) {
    fml = (smtFml_t *) sm->ite_fmlArr->space[i];
    smt_add_clause_for_ite_chain_fml(sm, fml);
  }

  return;
}

void
smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml)
{
  smtFml_t * tfml, * subfml_a, * subfml_b, * subfml_c;
  smtQueue_t * Q;
  satArray_t * condsArr = 0, * thensArr = 0;
  satArray_t * conds = 0, * thens = 0, * elses = 0;
  int num_fml = sm->fmlArr->size;

  assert(fml->type == ITE_c); /* ite(cond, then, else) */

  condsArr = sat_array_alloc(10);
  thensArr = sat_array_alloc(10);

  Q = smt_create_queue(sm->fmlArr->size);
  
  smt_enqueue(Q, (long) fml);
   
  while( (tfml = (smtFml_t *) smt_dequeue(Q)) ) {

    subfml_a = (smtFml_t *) tfml->subfmlArr->space[0];
    subfml_b = (smtFml_t *) tfml->subfmlArr->space[1];
    subfml_c = (smtFml_t *) tfml->subfmlArr->space[2];
    
    if (subfml_a->type == AND_c) { /* cond : leaf or AND */
      conds = smt_get_conjunct_in_fml(subfml_a, num_fml);
      
    } else if (smt_is_abstract_leaf_fml(subfml_a)) {
      conds = sat_array_alloc(4);

      if (subfml_a->bvar)
        conds = sat_array_insert(conds, (long) subfml_a->bvar->id);
      else
        conds = sat_array_insert(conds, (long) subfml_a->avar->id);      
    } 
    
    condsArr = sat_array_insert(condsArr, (long) conds);
    
    if (subfml_b->type == AND_c) { /* then : leaf or AND */
      thens = smt_get_conjunct_in_fml(subfml_b, num_fml);
      
    } else if (smt_is_abstract_leaf_fml(subfml_b)) {
      thens = sat_array_alloc(4);

      if (subfml_b->bvar)
        thens = sat_array_insert(thens, (long) subfml_b->bvar->id);
      else
        thens = sat_array_insert(thens, (long) subfml_b->avar->id);      
    } 

    thensArr = sat_array_insert(thensArr, (long) thens);

    /* then : ITE or leaf or AND */
    if (subfml_c->type == AND_c) { 
      elses = smt_get_conjunct_in_fml(subfml_c, num_fml);
      
    } else if (smt_is_abstract_leaf_fml(subfml_c)) {
      elses = sat_array_alloc(4);

      if (subfml_c->bvar)
        elses = sat_array_insert(elses, (long) subfml_c->bvar->id);
      else
        elses = sat_array_insert(elses, (long) subfml_c->avar->id);
      
    } else if (subfml_c->type == ITE_c) {
      smt_enqueue(Q, (long) subfml_c);
    } 
  }

  smt_add_clause_for_ite_chain_fml_sub(sm, fml, condsArr, thensArr, elses);
      
  if (Q) smt_free_queue(Q);
  if (conds) free(conds);
  if (thens) free(thens);
  if (elses) free(elses);
}

satArray_t *
smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml)
{ 
  smtFml_t * subfml_a, * tfml;
  smtQueue_t * Q;
  satArray_t * cjtArr = sat_array_alloc(4);
  int is_leaf, i;

  assert(fml->type == AND_c);

  Q = smt_create_queue(num_fml);
  
  smt_enqueue(Q, (long) fml);
   
  while( (tfml = (smtFml_t *) smt_dequeue(Q)) ) {

    is_leaf = smt_is_abstract_leaf_fml(tfml);

    if (!is_leaf) {

      assert(tfml->type == AND_c);

      for(i = 0; i < tfml->subfmlArr->size; i++) {
        subfml_a = (smtFml_t *) tfml->subfmlArr->space[i];
        smt_enqueue(Q, (long) subfml_a);
      }

    } else {

      if (tfml->bvar)
        cjtArr = sat_array_insert(cjtArr, (long) tfml->bvar->id);
      else
        cjtArr = sat_array_insert(cjtArr, (long) tfml->avar->id);

    }
  }

  smt_free_queue(Q);

  return cjtArr;
}

/**Function********************************************************************

  Synopsis    []

  Description [ e.g. 
  z = ite (a, b, ite (c, d, ite (e, f, g))) 
  
  ((a /\ b) -> z) /\ ((a /\ b') -> z')) /       \
  ((a' /\ c /\ d) -> z) /\ ((a' /\ c /\ d') -> z')) /\
  ((a' /\ c' /\ e /\ f) -> z) /\ ((a' /\ c' /\ e /\ f') -> z')) /\
  ((a' /\ c' /\ e' /\ g) -> z) /\ ((a' /\ c' /\ e' /\ g') -> z'))

  a, b, c, d, e, f, g can be either a lit or ANDs. 
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/

void
smt_add_clause_for_ite_chain_fml_sub(
  smtManager_t * sm, 
  smtFml_t * ite_fml,
  satArray_t * condsArr, 
  satArray_t * thensArr, 
  satArray_t * elses)
{
  AigEdge_t ite_node;
  smtCls_t * cls;
  satArray_t * conds, * thens;
  int z, cond_id, then_id, else_id;
  int num_comb, index;
  int i, j, k;

  ite_node = ite_fml->aig_node;
  assert(ite_node != Aig_NULL);
  index = AigNodeID(ite_node) - 1;
  z = sm->node2id[index]; /* ite: z */
  
  /* ((conds /\ thens) -> z) */
  for(i = 0; i < condsArr->size; i++) {
    
    cls = smt_create_clause();
    conds = (satArray_t *) condsArr->space[i];
    
    for(j = 0; j < conds->size; j++) {
      cond_id = (int) conds->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) -cond_id);
    }

    thens = (satArray_t *) thensArr->space[i];
    
    for(j = 0; j < thens->size; j++) {
      then_id = (int) thens->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) -then_id);
    }

    cls->litArr = sat_array_insert(cls->litArr, (long) z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }

  /* ((conds /\ thens') -> z') */
  for(i = 0, num_comb = 1; i < condsArr->size; i++) {

    conds = (satArray_t *) condsArr->space[i];
    thens = (satArray_t *) thensArr->space[i];

    num_comb = num_comb * (int) conds->size;
    
    for(j = 0; j < thens->size; j++) {
      cls = smt_create_clause();
      then_id = (int) thens->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) then_id);
    
      for(k = 0; k < conds->size; k++) {
        cond_id = (int) conds->space[k];
        cls->litArr = sat_array_insert(cls->litArr, (long) -cond_id);
      }

      cls->litArr = sat_array_insert(cls->litArr, (long) -z);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    }     
  }

#if 0 /* complete ite conversion : generate too many clauses 
         contain bug
       */

  /* ((conds' /\ elses) -> z) */
  for(i = 0; i < num_comb; i++) {
    cls = smt_create_clause();
    
    for(j = 0, index = i; j < condsArr->size; j++) {
      conds = (satArray_t *) condsArr->space[j];
      quo = index / conds->size;
      rem = index % conds->size;
      cond_id = (int) conds->space[rem];
      cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
      index = quo;
    }

    for(j = 0; j < elses->size; j++) {
      else_id = (int) elses->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) -else_id);
    }

    cls->litArr = sat_array_insert(cls->litArr, (long) z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }

  /* ((conds' /\ elses') -> z') */  
  for(i = 0; i < num_comb; i++) {

    for(j = 0; j < elses->size; j++) {
      cls = smt_create_clause();

      for(k = 0, index = i; k < condsArr->size; k++) {
        conds = (satArray_t *) condsArr->space[k];
        quo = index / conds->size;
        rem = index % conds->size;
        cond_id = (int) conds->space[rem];
        cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
        index = quo;
      }

      else_id = (int) elses->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) else_id);
      cls->litArr = sat_array_insert(cls->litArr, (long) -z);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    }    
  }

#else /* assumption : conditions are all disjoint */
  conds = (satArray_t *) condsArr->space[condsArr->size-1];

  /* ((conds' /\ elses) -> z) */
  for(i = 0; i < conds->size; i++) {
    cls = smt_create_clause();
    cond_id = (int) conds->space[i];
    cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
    
    for(j = 0; j < elses->size; j++) {
      else_id = (int) elses->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) -else_id);
    }
    
    cls->litArr = sat_array_insert(cls->litArr, (long) z);
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }  

  /* ((conds' /\ elses') -> z') */
  for(i = 0; i < conds->size; i++) {
    cond_id = (int) conds->space[i];
    
    for(j = 0; j < elses->size; j++) {
      else_id = (int) elses->space[j];

      cls = smt_create_clause();
      cls->litArr = sat_array_insert(cls->litArr, (long) cond_id);
      cls->litArr = sat_array_insert(cls->litArr, (long) else_id);
      cls->litArr = sat_array_insert(cls->litArr, (long) -z);
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    }
  }
#endif

  return;
}

#endif

void
smt_init_generate_cnf(smtManager_t * sm)
{
  smtFml_t * fml;
  int i;

  for(i = 0; i < sm->fmlArr->size; i++) {
    fml = (smtFml_t *) sm->fmlArr->space[i];
    fml->flag &= RESET_QUEUED_MASK;
    fml->nNeg = 0;
  }
}

int
smt_create_clause_with_fml(smtManager_t * sm, smtFml_t * fml)
{
  smtCls_t * cls = 0;
  smtFml_t * subfml;
  array_t * cjts;
  int is_cls, is_true;
  int is_cnf = 1;

  cjts = array_alloc(int, 4);

  /* fml type : leaf, not leaf, or, imply, iff */

  if (smt_is_atom_formula(fml) || smt_is_boolean_formula(fml)) {
    /* atom fml || bool fml */
    cls = smt_create_clause();
    is_true = smt_put_lit_to_clause(cls, fml);
    if (is_true == 1) {
      free(cls->litArr);
      free(cls);
    } else if (is_true == 0) {
      fprintf(stdout, "unsat : unit clause with (false) exists\n");
      exit(0);
    } else 
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);

  } else if (fml->type == NOT_c) { /* not fml */
    cls = smt_create_clause();
    subfml = (smtFml_t *) fml->subfmlArr->space[0];
    subfml->nNeg++;
    is_true = smt_put_lit_to_clause(cls, subfml); /* right? */
    if (is_true == 1) {
      free(cls->litArr);
      free(cls);
    } else if (is_true == 0) {
      fprintf(stdout, "unsat : unit clause with (false) exists\n");
      exit(0);
    } else 
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    subfml->nNeg--;
        
  } else if (fml->type == AND_c && ((fml->nNeg) % 2 != 0)) { /* not and fml */
    cls = smt_create_clause();
    /* gather lits from or fml */
    is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
    
    if (is_cnf) {
      if (cls->litArr->size)
        sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      else {
        free(cls->litArr);
        free(cls);
      }
    } else {
      free(cls->litArr);
      free(cls);
      is_cnf = 0;;
    }    
  } else if (fml->type == OR_c) { /* or fml */
    if ((fml->nNeg % 2) != 0) {
      array_free(cjts);
      return 0; /* may need to handle later */
    }
    
    /* if cls created, there exists and in or fml */
    is_cls = smt_create_clause_with_ands_in_or_fml(sm, fml);
    
    if (!is_cls) {
      cls = smt_create_clause();
      /* gather lits from or fml */
      is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
      
      if (is_cnf) {
        if (cls->litArr->size) 
          sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
        else {
          free(cls->litArr);
          free(cls);
        }         
      } else {
        free(cls->litArr);
        free(cls);
        is_cnf = 0;
      }    
    }
  } else if (fml->type == IMP_c) { /* imp fml */
    if ((fml->nNeg % 2) != 0) {
      array_free(cjts);
      return 0; /* may need to handle later */   
    }
    cls = smt_create_clause();
    /* gather lits from or fml */
    is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
    
    if (is_cnf) {
      assert(cls->litArr->size);
      cls->litArr->space[0] = -cls->litArr->space[0]; /* (a -> b) <-> (a' \/ b) */
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
    } else {
      free(cls->litArr);
      free(cls);
      is_cnf = 0;
    }    
  } else if (fml->type == IFF_c) { /* iff fml */
    if ((fml->nNeg % 2) != 0) {
      array_free(cjts);
      return 0; /* may need to handle later */   
    }
    cls = smt_create_clause(); /* (a <-> b) */
    /* gather lits from or fml */
    is_cnf = smt_put_lits_to_clause(cls, fml, cjts);
    
    if (is_cnf) {
      assert(cls->litArr->size);
      cls->litArr->space[0] = -cls->litArr->space[0]; /* (a -> b) <-> (a' \/ b) */
      sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
      /* (a' -> b') */
      cls = smt_create_clause();
      /* gather lits from or fml */
      smt_put_lits_to_clause(cls, fml, cjts);
      cls->litArr->space[1] = -cls->litArr->space[1]; /* (a' -> b') <-> (a \/ b') */
    } else {
      free(cls->litArr);
      free(cls);
      is_cnf = 0;
    }    
  }

  if (is_cnf && cjts->num) {
    /* (a \/ b \/ (c /\ d)) <-> ((a \/ b \/ c) /\ (a \/ b \/ d)) */
    assert(cls);
    smt_create_clause_with_conjuncts(sm, cls, cjts);
  }

  array_free(cjts);

  return is_cnf;
}

int
smt_put_lit_to_clause(smtCls_t * cls, smtFml_t * fml)
{
  long lit = 0;

  if (fml->flag & TRUE_MASK) {
    if (fml->nNeg % 2 == 0) return 1; /* true */
    else return 0; /* not true */

  } else if (fml->flag & FALSE_MASK) {
    if (fml->nNeg % 2 == 0) return 0; /* false */
    else return 1; /* not false */

  } else if (smt_is_atom_formula(fml)) { /* atom fml */
    if (fml->nNeg % 2 == 0) lit = fml->avar->id;
    else lit = -fml->avar->id;

  } else if (smt_is_boolean_formula(fml)) { /* bool fml */
    if (fml->nNeg % 2 == 0) {
      lit = fml->bvar->id;
    } else {
      lit = -fml->bvar->id;
    }

  } else {
    exit(0);
  }

  cls->litArr = sat_array_insert(cls->litArr, lit);

  return 2;
}

int
smt_put_lits_to_clause(smtCls_t * cls, smtFml_t * fml, array_t * cjts)
{
  smtFml_t * subfml, * tfml;
  int is_cnf = 1;
  int i;

  for(i = 0; i < fml->subfmlArr->size; i++) {
    subfml = (smtFml_t *) fml->subfmlArr->space[i];
        
    if ((fml->nNeg) % 2 == 0) { /* OR_c, IMP_c, IFF_c */
      if (subfml->flag & TRUE_MASK) {
        cls->litArr->size = 0;
        break;
      } else if (subfml->flag & FALSE_MASK) {
        /* unit clause (false) : consider later */
        continue;
      } if (smt_is_atom_formula(subfml)) {
        cls->litArr = sat_array_insert(cls->litArr, subfml->avar->id);
      } else if (smt_is_boolean_formula(subfml)) {
        cls->litArr = sat_array_insert(cls->litArr, subfml->bvar->id);
      } else if (smt_is_negated_atom_formula(subfml)) {
        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
        cls->litArr = sat_array_insert(cls->litArr, -tfml->avar->id);
      } else if (smt_is_negated_boolean_formula(subfml)) {
        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
        if (tfml->flag & TRUE_MASK) continue;
        else if (tfml->flag & FALSE_MASK) {
          cls->litArr->size = 0;
          break;
        } else
          cls->litArr = sat_array_insert(cls->litArr, -tfml->bvar->id);
      } else if (subfml->type == OR_c) {
        is_cnf = smt_put_lits_to_clause(cls, subfml, cjts);
        if (is_cnf == 0)
          break;      
      } else if (subfml->type == NOT_c) {
        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
        tfml->nNeg++;
        if (tfml->type == AND_c && ((tfml->nNeg) % 2 != 0)) {
          /* e.g. (a \/ (b /\ c)' \/ d) <-> (a \/ b' \/ c' \/ d) */
          is_cnf = smt_put_lits_to_clause(cls, tfml, cjts);
          if (is_cnf) tfml->nNeg--;
          else break;     

        } else {
          is_cnf = 0;
          break;
        }
      } else if (subfml->type == AND_c && cjts->num == 0) {
        /* (a \/ b \/ (c /\ d)) <-> ((a \/ b \/ c) /\ (a \/ b \/ d)) */
        is_cnf = smt_gather_conjuncts_in_and_fml(subfml, cjts);
        if (is_cnf == 0) 
          break;
      } else {
        is_cnf = 0;
        break;
      }
    } else { /* AND_c */
      if (smt_is_atom_formula(subfml)) {
        cls->litArr = sat_array_insert(cls->litArr, -subfml->avar->id);
      } else if (smt_is_boolean_formula(subfml)) {
        cls->litArr = sat_array_insert(cls->litArr, -subfml->bvar->id);
      } else if (smt_is_negated_atom_formula(subfml)) {
        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
        cls->litArr = sat_array_insert(cls->litArr, tfml->avar->id);
      } else if (smt_is_negated_boolean_formula(subfml)) {
        tfml = (smtFml_t *) subfml->subfmlArr->space[0];
        cls->litArr = sat_array_insert(cls->litArr, tfml->bvar->id);
      } else {
        is_cnf = 0;
        break;
      }
    }
  }

  return is_cnf;
}

void
smt_create_clause_with_conjuncts(
  smtManager_t * sm, 
  smtCls_t * cls, 
  array_t * cjts)
{
  smtCls_t * tcls;
  int i, lit;

  tcls = cls;

  for(i = 0; i < cjts->num; i++) {
    lit = array_fetch(int, cjts, i);
    tcls->litArr = sat_array_insert(tcls->litArr, lit);
    tcls = smt_duplicate_clause(cls); /* new cls */
    sm->clsArr = sat_array_insert(sm->clsArr, (long) tcls);
  }

  return;
}

int
smt_gather_conjuncts_in_and_fml(smtFml_t * fml, array_t * cjts)
{
  smtFml_t * subfml;
  int is_cnf = 1;
  int i;

  for(i = 0; i < fml->subfmlArr->size; i++) {
    subfml = (smtFml_t *) fml->subfmlArr->space[i];

    if (smt_is_atom_formula(subfml)) {
      array_insert_last(int, cjts, subfml->avar->id);
    } else if (smt_is_negated_atom_formula(subfml)) {
      subfml = (smtFml_t *) subfml->subfmlArr->space[0];
      array_insert_last(int, cjts, -subfml->avar->id);
    } else if (smt_is_boolean_formula(subfml)) {
      array_insert_last(int, cjts, subfml->bvar->id);
    } else if (smt_is_negated_boolean_formula(subfml)) {
      subfml = (smtFml_t *) subfml->subfmlArr->space[0];
      array_insert_last(int, cjts, -subfml->bvar->id);
    } else {
      is_cnf = 0;
      break;
    }
  }

  return is_cnf;
}

/**Function********************************************************************

  Synopsis    []

  Description [ e.g. 
  (a \/ (b /\ c)) <-> ((a \/ b) /\ (a \/ c))
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/

int
smt_create_clause_with_ands_in_or_fml(smtManager_t * sm, smtFml_t * fml)
{
  smtCls_t * cls;
  smtFml_t * subfml, * tfml;
  satArray_t * litArr;
  array_t * cjts = 0;
  int cjt, lit, is_cls = 1;
  int i, j;

  litArr = sat_array_alloc(10);

  for(i = 0; i < fml->subfmlArr->size; i++) {
    subfml = (smtFml_t *) fml->subfmlArr->space[i];

    if (subfml->type == AND_c) {
      if (cjts) {
        is_cls = 0;
        break;
      }
      /* cjts = smt_gather_conjuncts_in_and_fml(subfml); */
      cjts = array_alloc(int, 4);
      is_cls = smt_gather_conjuncts_in_and_fml(subfml, cjts);
      if (is_cls == 0) {
        array_free(cjts);
        cjts = 0;
        break;
      }
      /* if (cjts == 0) {
        is_cls = 0;
        break;
        }*/
      
    } else if (subfml->flag & TRUE_MASK) {

    } else if (subfml->flag & FALSE_MASK) {

    }

    else if (smt_is_atom_formula(subfml)) {
      litArr = sat_array_insert(litArr, subfml->avar->id);
    } else if (smt_is_boolean_formula(subfml)) {
      if (subfml->flag & TRUE_MASK) {
        litArr->size = 0;
        break;
      } else if (subfml->flag & FALSE_MASK) {
        /* unit clause (false) : consider later */
        continue;
      } else
        litArr = sat_array_insert(litArr, subfml->bvar->id);
    } else if (smt_is_negated_atom_formula(subfml)) {
      tfml = (smtFml_t *) subfml->subfmlArr->space[0];
      litArr = sat_array_insert(litArr, -tfml->avar->id);
    } else if (smt_is_negated_boolean_formula(subfml)) {
      tfml = (smtFml_t *) subfml->subfmlArr->space[0];
      if (tfml->flag & TRUE_MASK) {
        /* unit clause (false) : consider later */
        continue;
      } else if (tfml->flag & FALSE_MASK) {
        litArr->size = 0;
        break;  
      } else
        litArr = sat_array_insert(litArr, -tfml->bvar->id);
    } else {
      is_cls = 0;
      break;
    }
  }

  if (is_cls == 0 || cjts == 0) {
    is_cls = 0;
    free(litArr);
    return is_cls;
  }

  /* create clause */
  for(i = 0; i < cjts->num; i++) {
    cjt = array_fetch(int, cjts, i);
    cls = smt_create_clause();
    cls->litArr = sat_array_insert(cls->litArr, (long) cjt);

    for(j = 0; j < litArr->size; j++) {
      lit = (int) litArr->space[j];
      cls->litArr = sat_array_insert(cls->litArr, (long) lit);
    }
    sm->clsArr = sat_array_insert(sm->clsArr, (long) cls);
  }

  free(litArr);

  return is_cls;
}

#endif