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

  FileName    [smtSat.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"

#define NEW_BLOCKING

int
smt_call_theory_solver(satManager_t * m, long bound)
{
  smtManager_t * sm = (smtManager_t *) m->SMTManager; 
  int ret_val = 0;

  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) 
    ret_val = smt_call_dl_theory_solver(sm, bound);
  else
    exit(0);
  
  return ret_val;
}

int 
smt_call_dl_theory_solver(smtManager_t * sm, long bound)
{
  satManager_t * cm = sm->cm;
  int needImplication;
  int lit, avar_lit, value;
  int i, id;
  int num_lit = 0;
  
  if(cm->stackPos == 0)	return(0);

  smt_call_dl_theory_solver_preprocess(sm);

  needImplication = 0;

  /* send model to theory solver */
  for(i = bound; i < cm->stackPos; i++) {
    lit = cm->decisionStack[i];
    assert(lit>1);
    id = SATVar(lit);
    value = cm->values[id];
    assert(value != 2);
    
    if (id <= sm->avarArr->size) {
      if (sm->avalues[id] != value) {
	num_lit++;
	avar_lit = (value == 1) ? id : -id;
	sm->litArr = sat_array_insert(sm->litArr, avar_lit);
	sm->avalues[id] = value;
      }
    } 
  }

  if (num_lit == 0) 
    return needImplication;

  if (SATCurLevel(cm)==0) {
    sm->stats->num_lzero_ineq += num_lit;
  }

  needImplication = smt_theory_solve(sm);

  if ((int) sm->stats->num_bf_call%200000 == 0)
    smt_dl_report_intermediate_result(sm);

  if(cm->explanation->size) { /** conflicting case **/

    /** 
     * 1. add blocking clause info CNF database 
     * 2. do conflict analysis with respect to blocking clause
     * 3. backtrack to backtracking level 
     * 4. if needImplication==0, sat && no theory implication
     * 5. if needImplication==1, sat && theory implication
     * 6. if needImplication==2, unsat
     **/
    
    assert(cm->explanation->size>1);

    if(SATCurLevel(cm) == 0) {
      cm->status = 0;
      return 2;
    }

    smt_fit_decision_level_wrt_blocking_clause(cm, cm->explanation); 
#ifdef NEW_BLOCKING
    sat_add_blocking_clause_for_theorem_prover(cm, cm->explanation);
#else
    c = sat_add_blocking_clause(cm, cm->explanation);
    bLevel = sat_conflict_analysis(cm, c);
    sat_undo(cm, bLevel);

    csize = SATSizeClause(c);
    nMarks = 0;
    pLit = &(c->lits[0]);
    for(i = 0; i < csize; i++) { 
      if(cm->values[((*pLit)>>1)] == 2)	{
	nMarks++;
	iLit = (*pLit);
      }
      pLit++;
    }
    if(nMarks > 1) {
      c = sat_add_learned_clause(cm, cm->clearned);
      sat_update_variable_decay(cm);
      sat_update_clause_decay(cm);
    }
    else {
      if(cm->clearned->size == 1) {
        sat_enqueue(cm, iLit, 0);
      }
      else {
        sat_enqueue(cm, iLit, c);
      }
    }
#endif
    needImplication = 2;
  }
 
  return(needImplication);
}

void
smt_call_dl_theory_solver_preprocess(smtManager_t *sm)
{
  satManager_t * cm = sm->cm;

  sm->flag |= SAT_MASK; 
  sm->lemma->size = 0;
  sm->tplits->size = 0;
  sm->cur_index = sm->litArr->size;
  
  if (cm->explanation == 0) cm->explanation = sat_array_alloc(8);
  cm->explanation->size = 0;
}

int
smt_theory_solve(smtManager_t * sm)
{
  int needImplication = 0;

  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {

    if (sm->flag & MP_CONST_MASK) {
#if 1
      needImplication = smt_mp_dl_theory_solve(sm);
#endif      
    } else {      
      if (sm->flag & IDL_MASK) 
	needImplication = smt_idl_theory_solve(sm);
      else if (sm->flag & RDL_MASK) 
	needImplication = smt_rdl_theory_solve(sm);
    }
    
  } else {
    exit(0);
  }
    
  return needImplication;
}

void
smt_fit_decision_level_wrt_blocking_clause(
  satManager_t * m, 
  satArray_t * arr)
{
  long i, csize, *pLit, bLevel;

  csize = arr->size;
  pLit = &(arr->space[0]);
  bLevel = 0;
  for(i = 0; i < csize; i++) {
    if(m->levels[((*pLit)>>1)] > bLevel){
      bLevel = m->levels[((*pLit)>>1)];
    }
    pLit++;
  }
  sat_undo(m, bLevel);
}

int 
smt_get_size_of_atomic_variable(satManager_t * cm)
{
  smtManager_t *sm = (smtManager_t *) cm->SMTManager;

  return(sm->avarArr->size);
}

void
smt_theory_undo(satManager_t * cm)
{
  smtManager_t *sm = (smtManager_t *) cm->SMTManager;

  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
    smt_dl_theory_undo(sm);
  } else {
    exit(0);
  }
}

void
smt_dl_theory_undo(smtManager_t * sm)
{
  satManager_t * cm = sm->cm;
  smtGraph_t * G = sm->cG;
  smtAvar_t * avar;
  int lit, id;
  int i;  

  if (sm->litArr->size > 0) {
    /* 
       init for smt_get_right_end_edge 
       ignore unassigned edges 
    */
    G->esize = smt_get_right_end_edge_index(sm) + 1;
  }

  for(i = sm->litArr->size-1; i >= 0; i--) {
    lit = sm->litArr->space[i];
    id = (lit > 0) ? lit : -lit;

    if(cm->values[id] != 2) { 
      sm->litArr->size = i + 1;
      break;
    }
    avar = (smtAvar_t *) sm->id2var->space[id];

    /* check if avar is theory propagated */
    if (avar->flag & TPROP_MASK || avar->flag & IMPLIED_MASK) {
      sm->avalues[id] = 2;
      avar->flag &= RESET_TPROP_MASK;
      avar->flag &= RESET_IMPLIED_MASK;

      if(i==0) {
	sm->litArr->size=0;
	break;
      }
      continue;
    }

    /* update constraint graph */
    smt_update_edge_in_constraint_graph(sm, avar);

    /* reset avar */
    sm->avalues[id] = 2;    

    if(i==0) { 
      sm->litArr->size=0;
      break;
    }
  }

  sm->cur_index = sm->litArr->size;

  return;
}

void
smt_update_edge_in_constraint_graph(smtManager_t * sm, smtAvar_t * avar)
{
  satManager_t * cm = sm->cm;
  smtGraph_t * G = sm->cG;
  smtVertex_t * src, * dest;
  smtAvar_t * implied, * replacing = 0;
  smtNvar_t * lnvar, * rnvar;
  smtEdge_t *e;
  double iweight = 0, min_weight = 0;
  int dest_index, src_index;
  int id, i;

  id = avar->id;

  if (sm->avalues[id] == 1) {
    lnvar = (smtNvar_t *) avar->nvars->space[0];
    rnvar = (smtNvar_t *) avar->nvars->space[1];
  } else {
    assert(sm->avalues[id] == 0);
    lnvar = (smtNvar_t *) avar->nvars->space[1];
    rnvar = (smtNvar_t *) avar->nvars->space[0];
  }
  
  src_index = rnvar->id - 1;
  dest_index = lnvar->id - 1;
  src = &(G->vHead[src_index]);
  dest = &(G->vHead[dest_index]);
  e = smt_find_edge(src, dest);
    
  /** 
     pick strongest implied atom for the replace 
     implied is ordered in strength
  **/

  for(i = e->implied->size-1; i >= 0; i--) {
    implied = (smtAvar_t *) e->implied->space[i];
    if (cm->values[implied->id] == 2) continue;

    if (sm->avalues[implied->id] == 1) {
      iweight = implied->constant;
    } else if (sm->avalues[implied->id] == 0) {
      iweight = -implied->constant - sm->epsilon;
    } else
      exit(0);
    
    min_weight = iweight;
    replacing = implied;
    e->implied->size = i;

    break;      
  }
  
  if (replacing == 0) { /* no assigned implied atom */

    smt_delete_edge_in_constraint_graph(sm, e);

  } else { /* replace edge : check replacing avar */

    e->avar = replacing;
    e->weight = min_weight;
    e->avar->flag &= RESET_IMPLIED_MASK;

  }
  
  return;
}

void
smt_delete_edge_in_constraint_graph(smtManager_t * sm, smtEdge_t * e)
{
  smtGraph_t * G = sm->cG;
  smtVertex_t * src, * dest;
  smtEdge_t * rend_edge, * out, * in;
  int size, index;
  int i;

  src = e->src;
  dest = e->dest;

  size = src->outs->size;

  /* delete from outgoing edge list of src */
  for(i = 0; i < size; i++) {
    out = (smtEdge_t *) src->outs->space[i];
    if (out == e) {
      src->outs->space[i] = src->outs->space[size-1];
      src->outs->size--;
      break;
    }
  }

  size = dest->ins->size;

  /* delete from incoming edge list of dest */
  for(i = 0; i < size; i++) {
    in = (smtEdge_t *) dest->ins->space[i];
    if (in == e) {
      dest->ins->space[i] = dest->ins->space[size-1];
      dest->ins->size--;
      break;
    }
  }

  e->implied->size = 0;
  e->avar = 0;
  e->weight = 0;

  index = e->index;

  if (index >= G->esize) return;
  else rend_edge = smt_get_right_end_edge(sm);

  /** move last edge to deleted edge location **/
  if (rend_edge && rend_edge->index > index) {
    smt_put_right_end_edge_to_deleted(e, rend_edge);
    e->index = index;    
  } 

  G->esize--;

  return;
}

smtEdge_t *
smt_get_right_end_edge(smtManager_t * sm)
{
  satManager_t * cm = sm->cm;
  smtGraph_t * G = sm->cG;
  smtEdge_t * e;
  smtAvar_t * avar;
  int i, j;
  
  for(i = G->esize-1; i >= 0; i--) { 
    e = &(G->eHead[i]);    
    avar = e->avar;
    if (avar && cm->values[avar->id] != 2) {
      return e;
    }

    /* check implied list if the implied one is assigned */
    for(j = 0; j < e->implied->size; j++) {
      avar = (smtAvar_t *) e->implied->space[j];
      if (sm->avalues[avar->id] != 2) {
	return e;
      }
    }
    e->implied->size = 0;
  }    

  return 0;
}

int
smt_get_right_end_edge_index(smtManager_t * sm)
{
  satManager_t * cm = sm->cm;
  smtGraph_t * G = sm->cG;
  smtEdge_t * e;
  smtAvar_t * avar;
  int i, j;

  for(i = G->esize-1; i >= 0; i--) {
    e = &(G->eHead[i]);    
    avar = e->avar;
    if (cm->values[avar->id] != 2) {
      return i;
    }
    /* check implied list if the implied one is assigned */
    for(j = 0; j < e->implied->size; j++) {
      avar = (smtAvar_t *) e->implied->space[j];
      if (cm->values[avar->id] != 2) {
	return i;
      }
    }
    e->implied->size = 0;
  }

  return 0;
}

void
smt_put_right_end_edge_to_deleted(
  smtEdge_t * deleted, 
  smtEdge_t * rend_edge)
{
  smtVertex_t * src, * dest;
  smtEdge_t * e;
  satArray_t * dimplied;
  int i;

  src = rend_edge->src;
  dest = rend_edge->dest;

  /* update outs of src */
  for(i = 0; i < src->outs->size; i++) {
    e = (smtEdge_t *) src->outs->space[i];
    if (e == rend_edge) {
      src->outs->space[i] = (long) deleted;
      break;
    }
  }

  /* update ins of dest */
  for(i = 0; i < dest->ins->size; i++) {
    e = (smtEdge_t *) dest->ins->space[i];
    if (e == rend_edge) {
      dest->ins->space[i] = (long) deleted;
      break;
    }
  }

  /* keep the index */
  deleted->src = rend_edge->src;
  deleted->dest = rend_edge->dest;
  
  dimplied = deleted->implied;
  deleted->implied = rend_edge->implied;
  rend_edge->implied = dimplied;

  deleted->avar = rend_edge->avar;

  deleted->weight = rend_edge->weight;

  return;
}

void
smt_add_theory_clause(
  satManager_t * cm, 
  smtAvar_t * avar, 
  satArray_t * litArr)
{
  long i, j, v, lit;
  long clevel;
  int addClause, sign;
  satClause_t * c;
  smtManager_t * sm = (smtManager_t *) cm->SMTManager;

  addClause = 0;
  clevel = SATCurLevel(cm);

  if(clevel == 0) {
    assert(sm->avalues[avar->id] != 2);
    if (sm->avalues[avar->id] == 0) {
      sign = 1;
      sat_enqueue(cm, (avar->id<<1)+sign, 0); 
      avar->flag |= TPROP_MASK;
      sm->litArr = sat_array_insert(sm->litArr, -avar->id);
      sm->tplits = sat_array_insert(sm->tplits, -avar->id);

    } else if (sm->avalues[avar->id] == 1){
      sign = 0;
      sat_enqueue(cm, (avar->id<<1)+sign, 0); 
      avar->flag |= TPROP_MASK;
      sm->litArr = sat_array_insert(sm->litArr, avar->id);
      sm->tplits = sat_array_insert(sm->tplits, avar->id);
    }

    return;
  }

  for(i=j=0; i < litArr->size; i++) {
    lit = litArr->space[i];
    v = lit >> 1;
    if(cm->levels[v] != 0) {
      if(cm->levels[v] == clevel)
        addClause = 1;
      litArr->space[j++] = lit;
    }
  }
  litArr->size -= (i-j);

  if(addClause == 0 || litArr->size < 2) {
    sm->avalues[avar->id] = 2;

    return;
  }

  if (sm->avalues[avar->id] == 0) {
    sign = 1;
    sat_enqueue(cm, (avar->id<<1)+sign, 0); 
    avar->flag |= TPROP_MASK;
    sm->litArr = sat_array_insert(sm->litArr, -avar->id);
    sm->tplits = sat_array_insert(sm->tplits, -avar->id);

  } else {
    sign = 0;
    sat_enqueue(cm, (avar->id<<1)+sign, 0); 
    avar->flag |= TPROP_MASK;
    sm->litArr = sat_array_insert(sm->litArr, avar->id);
    sm->tplits = sat_array_insert(sm->tplits, avar->id);
  }

  c = sat_add_theory_clause(cm, litArr);

  cm->antes[avar->id] = c;

  return;
}

#endif