vc_api.cpp

Go to the documentation of this file.

#define GetValue(id) ((id) < 0 ? (d_vars[-(id)].value == -1 ? \
                                   -1 : (1 - d_vars[-(id)].value)) : \
                                 (id < 2) ? id : d_vars[id].value)
#define ABS(x) ((x) < 0 ? -(x) : (x))
#define MAX(x,y) (((x) > (y)) ? (x) : (y))


using namespace std;


bool SVC_API_impl::AddConditions(long lVar)
{
  // Collect vector of nonassertable facts and transform to vector
  // (conjunction) of atomified formulas
  vector<Expr> vecAtomify, vecDynamic, vecStatic;
  if (_verbosity > 1) {
    cout << "AddConditions" << endl;
  }
  // TODO: this becomes a callback
  while (!_nonassertable_facts->Done()) {
    vecAtomify.push_back(_nonassertable_facts->Get());
    if (_verbosity > 2) {
      _pem->Print(cout, vecAtomify.back());
      cout << endl;
    }
  }
  _patomifier->TransformVec(vecAtomify, vecDynamic, vecStatic);
  DebugAssert(vecAtomify.size() == vecDynamic.size(),"");

  // Convert atomified formulas to CNF
  _cnfFormula->Reset();
  int i;
  for (i = 0; i < (int)vecAtomify.size(); i++) {
    _conditions.push_back(vecAtomify[i]);
    _conditionVars.push_back(_cnfConverter->ConvertFormula(vecDynamic[i]));
    DebugAssert(_cnfFormula->_vecFormula.back()->_vecClause.size() == 1,
                "Expected unit clause");
    _cnfFormula->AddLiteral(lVar);
    _cnfFormula->_vecFormula.back()->SetDynamic();
  }
  for (i = 0; i < (int)vecStatic.size(); i++) {
    _cnfConverter->ConvertFormula(vecStatic[i]);
    _cnfFormula->RegisterUnit();
  }
  _cnfFormula->Simplify();
  if (_verbosity > 2) {
    _cnfFormula->Print();
  }
  _cnfConverter->Connect();

  // Update SAT formula
  return _psatapi->AddClauses(*_cnfFormula, _vecMap.size());
}


// Description: Update value in d_vars array                                  //
void SVC_API_impl::UpdateValue(long v, int value)
{
  v++;
  DebugAssert(v < (int)d_vars.size(), "id out of bounds");
  d_vars[v].value = value;
}


// Description: Recursively traverse the DAG looking for a splitter.  Return //
//              true if a splitter is found, false otherwise.  Visted nodes  //
//              are marked by setting their "next" fields to the current     //
//              value of _splitterCacheTag.                                  //
bool SVC_API_impl::FindSplitterRec(long v, int value, long *pv)
{
  int i;
  long tmp;
  bool ret;
  
  if (v == 0 || v == 1) return false;
  DebugAssert(v > 1 && (d_vars[v].value == value || d_vars[v].value == -1),
              "invariant violated");
  
  if (d_vars[v].next == _splitterCacheTag) return false;

  if (d_vars[v].fanins.size() == 0) {
    if (d_vars[v].value != -1) {
      d_vars[v].next = _splitterCacheTag;
      return false;
    }
    else {
      *pv = v;
      return true;
    }
  }
  // TODO:
  else if (d_vars[v].kind == Prop_Var_Manager::PROP_VAR_KIND) {
    // This propositional variable depends on static ITE's introduced by the
    // atomifier.  We handle these ITE's specially in order to catch the
    // corner case when a variable is its own fanin.
    for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
      tmp = d_vars[v].fanins[i];
      DebugAssert(tmp > 0,"Invariant violated");
      DebugAssert(d_vars[tmp].isITE(),"Expected ITE");
      DebugAssert(d_vars[tmp].value == 1,"Expected value 1");
      if (GetValue(d_vars[tmp].fanins[0]) == -1) {
        if (GetValue(d_vars[tmp].fanins[2]) == value) {
          ret = FindSplitterRec(ABS(d_vars[tmp].fanins[0]),
                                d_vars[tmp].fanins[0] < 0 ? 1 : 0, pv);
        }
        else {
          ret = FindSplitterRec(ABS(d_vars[tmp].fanins[0]),
                                d_vars[tmp].fanins[0] < 0 ? 0 : 1, pv);
        }
        if (!ret) {
          cout << _vecMap[ABS(d_vars[tmp].fanins[0])-2] << endl;
          DebugAssert(false,"No controlling input found (1)");
        }         
        return true;
      }
      else if (GetValue(d_vars[tmp].fanins[0])) {
        if (FindSplitterRec(ABS(d_vars[tmp].fanins[0]),
                            d_vars[tmp].fanins[0] < 0 ? 0 : 1, pv)) {
            return true;
        }
        if (ABS(d_vars[tmp].fanins[1]) != v &&
            FindSplitterRec(ABS(d_vars[tmp].fanins[1]),
                            d_vars[tmp].fanins[1] < 0 ? 0 : 1, pv)) {
          return true;
        }
      }
      else {
        if (FindSplitterRec(ABS(d_vars[tmp].fanins[0]),
                            d_vars[tmp].fanins[0] < 0 ? 1 : 0, pv)) {
          return true;
        }
        if (ABS(d_vars[tmp].fanins[2]) != v &&
            FindSplitterRec(ABS(d_vars[tmp].fanins[2]),
                            d_vars[tmp].fanins[1] < 0 ? 0 : 1, pv)) {
          return true;
        }
      }
      d_vars[tmp].next = _splitterCacheTag;
    }
    if (d_vars[v].value != -1) {
      d_vars[v].next = _splitterCacheTag;
      return false;
    }
    else {
      *pv = v;
      return true;
    }
  }

  switch (d_vars[v].kind) {
    case AND:
      if (value) {
        for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
          if (FindSplitterRec(ABS(d_vars[v].fanins[i]),
                            d_vars[v].fanins[i] < 0 ? 0 : 1, pv)) {
            return true;
          }
        }
        DebugAssert(d_vars[v].value == 1,"Output should be justified");
        d_vars[v].next = _splitterCacheTag;
        return false;
      }
      else {
        for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
          if (GetValue(d_vars[v].fanins[i]) != 1) {
            if (FindSplitterRec(ABS(d_vars[v].fanins[i]),
                                d_vars[v].fanins[i] < 0 ? 1 : 0, pv)) {
              return true;
            }
            DebugAssert(d_vars[v].value == 0,"Output should be justified");
            d_vars[v].next = _splitterCacheTag;
            return false;
          }
        }
        DebugAssert(i < (int)d_vars[v].fanins.size(),
                    "No controlling input found (2)");
      }
      break;
    case OR:
      if (!value) {
        for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
          if (FindSplitterRec(ABS(d_vars[v].fanins[i]),
                            d_vars[v].fanins[i] < 0 ? 1 : 0, pv)) {
            return true;
          }
        }
        DebugAssert(d_vars[v].value == 0,"Output should be justified");
        d_vars[v].next = _splitterCacheTag;
        return false;
      }
      else {
        for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
          if (GetValue(d_vars[v].fanins[i]) != 0) {
            if (FindSplitterRec(ABS(d_vars[v].fanins[i]),
                                d_vars[v].fanins[i] < 0 ? 0 : 1, pv)) {
              return true;
            }
            DebugAssert(d_vars[v].value == 1,"Output should be justified");
            d_vars[v].next = _splitterCacheTag;
            return false;
          }
        }
        DebugAssert(i < (int)d_vars[v].fanins.size(),
                    "No controlling input found (3)");
      }
      break;
    case ITE:
      if (GetValue(d_vars[v].fanins[0]) == -1) {
        if (GetValue(d_vars[v].fanins[2]) == value) {
          ret = FindSplitterRec(ABS(d_vars[v].fanins[0]),
                                d_vars[v].fanins[0] < 0 ? 1 : 0, pv);
        }
        else {
          ret = FindSplitterRec(ABS(d_vars[v].fanins[0]),
                                d_vars[v].fanins[0] < 0 ? 0 : 1, pv);
        }
        if (!ret) {
          _pem->Print(cout, _vecMap[v-2]);
          DebugAssert(false,"No controlling input found (4)");
        }         
        return true;
      }
      else if (GetValue(d_vars[v].fanins[0])) {
        if (FindSplitterRec(ABS(d_vars[v].fanins[0]),
                            d_vars[v].fanins[0] < 0 ? 0 : 1, pv)) {
            return true;
        }
        if (FindSplitterRec(ABS(d_vars[v].fanins[1]),
                            d_vars[v].fanins[1] < 0 ? 1-value : value, pv)) {
          return true;
        }
      }
      else {
        if (FindSplitterRec(ABS(d_vars[v].fanins[0]),
                            d_vars[v].fanins[0] < 0 ? 1 : 0, pv)) {
          return true;
        }
        if (FindSplitterRec(ABS(d_vars[v].fanins[2]),
                            d_vars[v].fanins[2] < 0 ? 1-value : value, pv)) {
          return true;
        }
      }
      DebugAssert(d_vars[v].value == value,"Output should be justified");
      d_vars[v].next = _splitterCacheTag;
      return false;
    case IFF:
    case EQ:
      tmp = GetValue(d_vars[v].fanins[0]);
      if (tmp != -1) {
        if (FindSplitterRec(ABS(d_vars[v].fanins[0]),
                            d_vars[v].fanins[0] < 0 ? 1-tmp : tmp, pv)) {
          return true;
        }
        if (!value) tmp = 1 - tmp;
        if (FindSplitterRec(ABS(d_vars[v].fanins[1]),
                            d_vars[v].fanins[1] < 0 ? 1-tmp : tmp, pv)) {
          return true;
        }
        DebugAssert(d_vars[v].value == value,"Output should be justified");
        d_vars[v].next = _splitterCacheTag;
        return false;
      }
      else {
        tmp = GetValue(d_vars[v].fanins[1]);
        if (tmp == -1) tmp = 0;
        if (!value) tmp = 1 - tmp;
        if (FindSplitterRec(ABS(d_vars[v].fanins[0]),
                            d_vars[v].fanins[0] < 0 ? 1-tmp : tmp, pv)) {
          return true;
        }
        DebugAssert(false,"Unable to find controlling input");
      }
      break;
    case IMPLIES:
    default:
      FatalAssert(false,"Not implemented yet");    
  }
  *pv = 0;
  return true;
}


// Description: Traverse tree recursively looking for nodes that reduce to   //
//              true or false.  Visited nodes with no splitters are marked   //
//              as in FindSplitterRec.  Visited nodes with splitters are     //
//              marked by setting the "prev" field to the current value of   //
//              _splitterCacheTag2.                                          //
bool SVC_API_impl::GetImplicationsRec(long v, long *pv, int *pvalue)
{
  int i;
  long tmp;
  bool ret;
  Expr e;

  if (v == 0 || v == 1) return false;
  DebugAssert(v > 1,"invariant violated");

  if (d_vars[v].next == _splitterCacheTag) return false;
  if (d_vars[v].prev == _splitterCacheTag2) return true;
  d_vars[v].prev = _splitterCacheTag2;

  if (d_vars[v].fanins.size() == 0) {
    if (d_vars[v].value != -1) {
      d_vars[v].next = _splitterCacheTag;
      return false;
    }
    else if (HasSVCExpr(v-1)) {
      e = d_core->simplify(_vecMap[v-2]);
      if (e.isFalse()) == 0) {
        *pv = v;
        *pvalue = 0;
      }
      else if (e.isTrue()) {
        *pv = v;
        *pvalue = 1;
      }
    }
    return true;
  }

  ret = false;
// TODO
  if (d_vars[v].kind == Prop_Var_Manager::PROP_VAR_KIND) {
    bool retTmp;
    for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
      retTmp = false;
      tmp = d_vars[v].fanins[i];
      DebugAssert(tmp > 0,"Invariant violated");
      DebugAssert(d_vars[tmp].isITE(),"Expected ITE");
      DebugAssert(d_vars[tmp].value == 1,"Expected value 1");
      if (d_vars[tmp].next == _splitterCacheTag) continue;
      if (d_vars[tmp].prev == _splitterCacheTag2) {
        ret = true;
        continue;
      }
      d_vars[tmp].prev = _splitterCacheTag2;
      if (GetValue(d_vars[tmp].fanins[0]) == -1) {
        bool retval = GetImplicationsRec(ABS(d_vars[tmp].fanins[0]),pv,pvalue);
        if (*pv != 0) return true;
        DebugAssert(retval,"Expected unjustified");
        retTmp = true;
      }
      else if (GetValue(d_vars[tmp].fanins[0])) {
        if (GetImplicationsRec(ABS(d_vars[tmp].fanins[0]),pv,pvalue)) {
          retTmp = true;
        }
        if (*pv != 0) return true;
        if (ABS(d_vars[tmp].fanins[1]) != v &&
            GetImplicationsRec(ABS(d_vars[tmp].fanins[1]),pv,pvalue)) {
          retTmp = true;
        }
        if (*pv != 0) return true;
      }
      else {
        if (GetImplicationsRec(ABS(d_vars[tmp].fanins[0]),pv,pvalue)) {
          retTmp = true;
        }
        if (*pv != 0) return true;
        if (ABS(d_vars[tmp].fanins[2]) != v &&
            GetImplicationsRec(ABS(d_vars[tmp].fanins[2]),pv,pvalue)) {
          retTmp = true;
        }
        if (*pv != 0) return true;
      }
      if (!retTmp) {
        d_vars[tmp].next = _splitterCacheTag;
      }
      ret = ret || retTmp;
    }
    if (d_vars[v].value != -1) {
      if (!ret) {
        d_vars[v].next = _splitterCacheTag;
        return false;
      }
    }
    else if (HasSVCExpr(v-1)) {
      e = d_core->simplify(_vecMap[v-2]);
      if (e.isFalse()) {
        *pv = v;
        *pvalue = 0;
      }
      else if (e.isTrue()) {
        *pv = v;
        *pvalue = 1;
      }
    }
    return true;
  }

  switch (d_vars[v].kind) {
    case AND:
    case OR:
    case IFF:
    case EQ:
      for (i=0; i < (int)d_vars[v].fanins.size(); i++) {
        if (GetImplicationsRec(ABS(d_vars[v].fanins[i]),pv,pvalue)) {
          ret = true;
        }
        if (*pv != 0) return true;
      }
      if (d_vars[v].value != -1) {
        if (!ret) {
          d_vars[v].next = _splitterCacheTag;
          return false;
        }
      }
      else if (HasSVCExpr(v-1)) {
        e = d_core->simplify(_vecMap[v-2]);
        if (e.isFalse()) {
          *pv = v;
          *pvalue = 0;
        }
        else if (e.isTrue()) {
          *pv = v;
          *pvalue = 1;
        }
      }
      return true;
    case ITE:
      if (GetValue(d_vars[v].fanins[0]) == -1) {
        bool retval = GetImplicationsRec(ABS(d_vars[v].fanins[0]),pv,pvalue);
        if (*pv != 0) return true;
        DebugAssert(retval,"Expected unjustified");
        ret = true;
      }
      else if (GetValue(d_vars[v].fanins[0])) {
        if (GetImplicationsRec(ABS(d_vars[v].fanins[0]),pv,pvalue)) {
          ret = true;
        }
        if (*pv != 0) return true;
        if (GetImplicationsRec(ABS(d_vars[v].fanins[1]),pv,pvalue)) {
          ret = true;
        }
        if (*pv != 0) return true;
      }
      else {
        if (GetImplicationsRec(ABS(d_vars[v].fanins[0]),pv,pvalue)) {
          ret = true;
        }
        if (*pv != 0) return true;
        if (GetImplicationsRec(ABS(d_vars[v].fanins[2]),pv,pvalue)) {
          ret = true;
        }
        if (*pv != 0) return true;
      }
      if (d_vars[v].value != -1) {
        if (!ret) {
          d_vars[v].next = _splitterCacheTag;
          return false;
        }
      }
      else if (HasSVCExpr(v-1)) {
        e = d_core->simplify(_vecMap[v-2]);
        if (e.isFalse()) {
          *pv = v;
          *pvalue = 0;
        }
        else if (e.isTrue()) {
          *pv = v;
          *pvalue = 1;
        }
      }
      return true;
    case IMPLIES:
    default:
      FatalAssert(false,"Not implemented yet");    
  }
  return true;
}


///////////////////////////////////////////////////////////////////////////////
// Begin public methods                                                      //
///////////////////////////////////////////////////////////////////////////////


// Description: Constructor                                                  //
SVC_API_impl::SVC_API_impl(TheoryCore* core)
  : d_core(core), _vecMap(), _connectQueue(), _conditions(), _conditionVars(),
    _conditionIndex(), d_vars(100), _splitterCacheTag(1), _splitterCacheTag2(1)
{
  // TODO:
  // Set up propositional variable manager
  _ppvm = new Prop_Var_Manager(type_sys, *_pem);
  _ppvm->Init("Prop_Var_Manager", "_p_");
  _pem->DeclareKind(Prop_Var_Manager::PROP_VAR_KIND, *_ppvm, true);

  _pfanout_table = new hash_map<int, vector<Expr>* >;
  _verbosity = 0;

  // Initialize Sat_SVC components
// TODO:
  C_Nucleus::Source<E::Expr_Handle> *psourceOfFreshVars =
    (C_Nucleus::Source<E::Expr_Handle>*)
    basic_sys.GetCR(SVC2::SOURCE_OF_FRESHD_VARS);
  _pisAtomic = (C_Nucleus::Predicate<E::Expr_Handle>*)
    fdrsning_sys.Get(FDRsning::ATOMIC);
  _patomifier = new Atomifier(*_pem, *_prec_tb, *pvar_rec_tb,
                              *psourceOfFreshVars, *freshVarDefs, *_pisAtomic,
                              *pisBool, _vecMap, _pfanout_table, _connectQueue);
  _patomifier->ClearTransformCache();
  _cnfFormula = new CNF_Formula_For_Exprs(*_pem);
  _cnfConverter = new CNF_Converter(*_pem, *_cnfFormula, _vecMap, this,
                                    _pfanout_table, _connectQueue);
  _psatapi = new SAT_API(*this, *_fm_trace, flags);

  Reset();
}


// Description: Destructor                                                   //
SVC_API_impl::~SVC_API_impl()
{
  delete _psatapi;
  delete _cnfConverter;
  delete _cnfFormula;
  delete _patomifier;
  hash_map<int, vector<Expr>* >::iterator i, iend;
  for (i = _pfanout_table->begin(), iend = _pfanout_table->end(); i != iend; ++i) {
    if ((*i).second) delete (*i).second;
  }
  delete _pfanout_table;
}


// Description: Main SAT checking procedure                             //
bool SVC_API_impl::CheckSat(const Expr& e)
{
  // If the formula is TRUE or FALSE, return
  // without entering the heart of the SAT code.
  if (e.isBoolConst()) return e.isFalse();

  // Transform vector (conjunction) of formulas to vector (conjunction) of
  // atomified formulas
  vector<Expr> vecAtomify, vecDynamic, vecStatic;
  if (_verbosity) {
    cout << "SAT_SVC: Atomifying" << endl;
  }
  vecAtomify.push_back(e);
  _patomifier->TransformVec(vecAtomify, vecDynamic, vecStatic);
  DebugAssert(vecDynamic.size() == 1,"");

  // Convert atomified formulas to CNF
  vector<Expr>::const_iterator i;
  if (_verbosity) {
    cout << "SAT_SVC: Converting to CNF" << endl;
  }
  _cnfFormula->Reset();
  _conditions.push_back(e);
  _conditionVars.push_back(_cnfConverter->ConvertFormula(vecDynamic[0]));
  for (i = vecStatic.begin(); i != vecStatic.end(); ++i) {
    _cnfConverter->ConvertFormula(*i);
    _cnfFormula->RegisterUnit();
  }
  _cnfFormula->Simplify();
  if (_verbosity > 2) {
    _cnfFormula->Print();
  }
  _cnfConverter->Connect();

  // Run SAT
  if (_verbosity) {
    cout << "SAT_SVC: Starting SAT" << endl;
  }
  bool result = _psatapi->RunSAT(*_cnfFormula, _vecMap.size(), _verbosity) == SAT_API::UNSAT;
  if (result) {
    Reset();
  }
  else {
    _ready = false;
  }
  return result;
}


// Description: Push scope                                                   //
void SVC_API_impl::Push()
{
  if (_verbosity > 2) {
    cout << "SVC_API: Push" << endl;
  }
  d_core->getCM()->push();
  _conditionIndex.push_back(_conditionVars.size());
  DebugAssert(_conditionVars.size() == _conditions.size(),
              "condition size mismatch");
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: SVC_API_impl::Pop                                               //
// Author: Clark Barrett                                                     //
// Created: Wed Sep 26 19:43:16 2001                                         //
// Description: Pop scope                                                    //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
void SVC_API_impl::Pop()
{
  if (_verbosity > 2) {
    cout << "SVC_API: Pop" << endl;
  }
  d_core->getCM()->pop();

  // Reset context-dependent state
  _splitterCacheTag++;
  while ((int)_conditionVars.size() != _conditionIndex.back()) {
    _conditionVars.pop_back();
    _conditions.pop_back();
  }
  _conditionIndex.pop_back();
}


// Description: Asserts the SVC expr associated with lVar (if any).          //
//              Returns true unless conditions added are inconsistent.       //
bool SVC_API_impl::SVCAssert(long lVar)
{
  DebugAssert(lVar > 0,"SVC_API::Assert 1");
  if (_verbosity > 2) {
    cout << "SVC_API: Assert " << lVar << endl;
  }
  UpdateValue(lVar,1);
  DebugAssert((unsigned)lVar <= _vecMap.size(),"SVC_API::Assert 2");
  Expr e = _vecMap[lVar-1];
  if (e.isNull()) return true;

  if (_verbosity > 2) {
    cout << " A " << e << endl;
  }
  d_core->addFact(d_core->assumpRule(e));

  if (!IsStable()) {
    if (_verbosity > 1) {
      cout << "Condition added" << endl;
    }
    return AddConditions(-lVar);
  }
  return true;
}


// Description: Denies the SVC expr associated with lVar (if any).           //
//              Returns true unless conditions added are inconsistent.       //
bool SVC_API_impl::SVCDeny(long lVar)
{
  DebugAssert(lVar > 0,"SVC_API::Deny 1");
  if (_verbosity > 2) {
    cout << "SVC_API: Deny " << lVar << endl;
  }
  UpdateValue(lVar,0);
  DebugAssert((unsigned)lVar <= _vecMap.size(),"SVC_API::Deny 2");
  Expr e = _vecMap[lVar-1];
  if (e.IsNull()) return true;

  if (_verbosity > 2) {
    cout << " D " << e << endl;
  }

  d_core->addFact(d_core->assumpRule(!e));

  if (!IsStable()) {
    if (_verbosity > 1) {
      cout << "Condition added" << endl;
    }
    return AddConditions(lVar);
  }
  return true;
}


// Description: Get a vector of the assumptions used in the last proof step. //
//              This is used to produce conflict clauses.                    //
bool SVC_API_impl::GetConfClause(vector<int>* literals)
{
  DebugAssert(literals->size() == 0, "Expected size = 0");
  vector<Expr> assumptions, expr_literals, dummy;
  Expr e;

  // TODO: Get the assumptions

  int numvars = _vecMap.size();
  _patomifier->TransformVec(assumptions, expr_literals, dummy);
  DebugAssert(numvars == (int)_vecMap.size(),
              "New vars created in conflict clause");
  bool invert;
  int var;
  while (!expr_literals.empty()) {
    e = expr_literals.back();
    expr_literals.pop_back();
    invert = false;
    if (e.isNot()) {
      e = e[0];
      invert = true;
    }
    DebugAssert(e.isVar(), "expected prop var");
    //TODO: figure out this
    var = (int)_pem->GetKindSpecificData(e);
    if (invert) var = -var;
    literals->push_back(var);

  }
  return true;
}


// Description: Check whether the context is consistent.                     //
bool SVC_API_impl::IsConsistent()
{
  bool inconsistent = !d_core->inconsistent();
  if (_verbosity > 2) {
    if (inconsistent) {
      cout << "Inconsistent" << endl;
    }
  }
  return !inconsistent;
}


// Description: Returns whether the variable has an associated SVC expr.     //
bool SVC_API_impl::HasSVCExpr(long lVar)
{
  DebugAssert(lVar > 0 && (unsigned)lVar <= _vecMap.size(),"");
  return !(_vecMap[lVar-1].IsNull());
}


bool SVC_API_impl::OKToSplit(long lVar)
{
  return (HasSVCExpr(lVar) && d_vars[lVar+1].prev == _splitterCacheTag2);
}


// Description: Reset variable v                                             //
void SVC_API_impl::ResetVariable(long v)
{
  d_vars[++v].value = -1;
  d_vars[v].next = 0;
  d_vars[v].prev = 0;
}


// Description: Record each child of a propositional expression e as a fanin //
//              in the d_vars vector.                                         //
void SVC_API_impl::Connect(const Expr& e, long v)
{
  int i;
  Expr eChild;
  int kind;
  long childID;
  v++;
  if ((int)d_vars.size() <= v) d_vars.resize(v+1);
  d_vars[v].kind = e.getKind();
  for (i=0; i < e.arity(); ++i) {
    eChild = e[i];
    kind = eChild.getKind();
    switch (kind) {
      case FALSE:
        childID = 0;
        break;
      case TRUE:
        childID = 1;
        break;
      case NOT:
        eChild = eChild[0];
        kind = eChild.getKind();
        //TODO:
        FatalAssert(kind == PROP_VAR_KIND,"Prop Var expected");
        childID = -((long)_pem->GetKindSpecificData(eChild, &kind))-1;
        break;
      default:
        Assert(kind == Prop_Var_Manager::PROP_VAR_KIND,"Prop Var expected");
        childID = (long)_pem->GetKindSpecificData(eChild, &kind)+1;
        break;
    }
    d_vars[v].fanins.push_back(childID);
    if (childID < 0) childID = -childID;
    d_vars[childID].fanouts.push_back(v);
  }
}


// Description: Connect the variable associated with eFrom to the variable   //
//              associated with eTo.                                         //
void SVC_API_impl::Connect1(const Expr& eFrom,
                            const Expr& eTo)
{
  int kind;
  long idFrom, idTo;
  //TODO:
  idFrom = (long)_pem->GetKindSpecificData(eFrom, &kind)+1;
  idTo = (long)_pem->GetKindSpecificData(eTo, &kind)+1;
  if ((int)d_vars.size() <= MAX(idFrom,idTo)) d_vars.resize(MAX(idFrom,idTo)+1);
  d_vars[idFrom].fanouts.push_back(idTo);
  d_vars[idTo].fanins.push_back(idFrom);
  d_vars[idTo].kind = Prop_Var_Manager::PROP_VAR_KIND;
}


// Description: Find a splitter by calling FindSplitterRec.                  //
bool SVC_API_impl::FindSplitter(long *v)
{
  long var;
  int i;
  for (i=0; i < (int)_conditions.size(); i++) {
    var = _conditionVars[i]+1;
    if (FindSplitterRec(var, d_vars[var].value, v)) {
      break;
    }
  }
  if (i == (int)_conditions.size()) return false;
  (*v)--;
  return true;
}


// Description: Look for nodes in the DAG which reduce to true or false.  If //
//              one is found, return it in pv with pvalue set to 1 if it     //
//              reduces to true, 0 if it reduces to false.                   //
void SVC_API_impl::GetImplications(long *pv, int *pvalue)
{
  long var;
  int i;
  _splitterCacheTag2++;
  *pv = 0;
  for (i=0; i < (int)_conditions.size(); i++) {
    var = _conditionVars[0]+1;
    GetImplicationsRec(var,pv,pvalue);
    if (*pv != 0) {
      (*pv)--;
      return;
    }
  }
}


// Description: Print variable associated with lVar                          //
void SVC_API_impl::PrintVar(long lVar)
{
  Expr e = _vecMap[lVar-1];
  if (!e.isNull()) {
    cout << e;
  }
}


// Description: Print expr e with its type.                                  //
void SVC_API_impl::PrintWithType(const Expr& e)
{
  cout << e << " : " << e.getType().getExpr() << ";" << endl;
}


// Description: Reset and prepare to check another formula.                  //
void SVC_API_impl::Reset(void)
{
  _psatapi->Reset();
  _pfanout_table->clear();
  _vecMap.clear(); 
  _connectQueue.clear();
  _conditions.clear();
  _conditionVars.clear();
  _conditionIndex.clear();
  _conditionIndex.push_back(0);
  _patomifier->ClearTransformCache();
  _cnfConverter->Reset();

  // Reset Propositional Variable Manager and create dummy var with id 0
  // TODO:
  _ppvm->Reset();
  _pem->CreateExpr(Prop_Var_Manager::PROP_VAR_KIND);
  _ready = true;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: SVC_API_impl::Ready                                             //
// Author: Clark Barrett                                                     //
// Created: Mon Feb 11 17:29:45 2002                                         //
// Description: Return true iff ready to check another formula.              //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
bool SVC_API_impl::Ready(void)
{
  return _ready;
}


}

---