tvt z3_propt::l_get(literalt a) const
{
  tvt result=tvt(false);
  std::string literal;
  Z3_ast z3_literal;
  size_t found;

  if(a.is_true())
    return tvt(true);
  else if(a.is_false())
    return tvt(false);

  literal = "l"+i2string(a.var_no());

  map_prop_varst::const_iterator cache_result=map_prop_vars.find(literal.c_str());
  if(cache_result!=map_prop_vars.end())
  {
    //std::cout << "Cache hit on " << cache_result->first << "\n";
	z3_literal = cache_result->second;
    Z3_app app = Z3_to_app(z3_ctx, z3_literal);
    Z3_func_decl d = Z3_get_app_decl(z3_ctx, app);
    literal = Z3_func_decl_to_string(z3_ctx, d);

    found=literal.find("true");

    if (found!=std::string::npos)
      result=tvt(true);
    else
      result=tvt(false);
  }

  if (a.sign()) result=!result;

  return result;
}

tvt satcheck_booleforce_baset::l_get(literalt a) const
{
  assert(status==SAT);

  if(a.is_true())
    return tvt(true);
  else if(a.is_false())
    return tvt(false);

  tvt result;
  unsigned v=a.var_no();

  assert(v<no_variables());

  int r=booleforce_deref(v);

  if(r>0)
    result=tvt(true);
  else if(r<0)
    result=tvt(false);
  else
    result=tvt(tvt::tv_enumt::TV_UNKNOWN);

  if(a.sign())
    result=!result;

  return result;
}

tvt cvc_convt::l_get(literalt l) const
{
    if(l.is_true()) return tvt(true);
    if(l.is_false()) return tvt(false);
    assert(l.var_no()<boolean_assignment.size());
    return tvt(boolean_assignment[l.var_no()]^l.sign());
}

tvt boolector_propt::l_get(literalt a) const
{
  tvt result=tvt(false);
  std::string literal;
  BtorExp *boolector_literal;
  size_t found;

  if(a.is_true())
    return tvt(true);
  else if(a.is_false())
    return tvt(false);

  literal_cachet::const_iterator cache_result=literal_cache.find(a.var_no());
  if(cache_result!=literal_cache.end())
    boolector_literal = cache_result->second;
  else
	return tvt(tvt::TV_UNKNOWN);

  literal = boolector_bv_assignment(boolector_ctx, boolector_literal);
  found=literal.find("1");

  if (found!=std::string::npos)
    result=tvt(true);
  else
	result=tvt(false);

  if (a.sign()) result=!result;

  return result;
}

const exprt qbf_squolem_coret::f_get(literalt l)
{
  if(squolem->isUniversal(l.var_no()))
  {
    assert(l.var_no()!=0);
    variable_mapt::const_iterator it=variable_map.find(l.var_no());

    if(it==variable_map.end())
      throw "Variable map error";

    const exprt &sym=it->second.first;
    unsigned index=it->second.second;

    exprt extract_expr(ID_extractbit, typet(ID_bool));
    extract_expr.copy_to_operands(sym);
    typet uint_type(ID_unsignedbv);
    uint_type.set(ID_width, 32);
    extract_expr.copy_to_operands(from_integer(index, uint_type));

    if(l.sign()) extract_expr.negate();

    return extract_expr;
  }

  function_cachet::const_iterator it=function_cache.find(l.var_no());
  if(it!=function_cache.end())
  {
    #if 0
    std::cout << "CACHE HIT for " << l.dimacs() << std::endl;
    #endif

    if(l.sign())
      return not_exprt(it->second);
    else
      return it->second;
  }
  else
  {
    WitnessStack *wsp = squolem->getModelFunction(Literal(l.dimacs()));
    exprt res;

    if(wsp==NULL || wsp->empty())
    {
//      res=exprt(ID_nondet_bool, typet(ID_bool));
      res=false_exprt(); // just set it to zero
    }
    else if(wsp->pSize<=wsp->nSize)
      res=f_get_cnf(wsp);
    else
      res=f_get_dnf(wsp);

    function_cache[l.var_no()] = res;

    if(l.sign())
      return not_exprt(res);
    else
      return res;
  }
}

void smt1_propt::set_assignment(literalt literal, bool value)
{
  if(literal.is_true() || literal.is_false()) return;

  unsigned v=literal.var_no();
  assert(v<assignment.size());
  assignment[v]=tvt(value);
}

void satcheck_glucose_simplifiert::set_frozen(literalt a)
{
  if(!a.is_constant())
  {
    add_variables();
    solver->setFrozen(a.var_no(), true);
  }
}

void satcheck_minisat1_baset::set_assignment(literalt a, bool value)
{
  unsigned v=a.var_no();
  bool sign=a.sign();
  solver->model.growTo(v+1);
  value^=sign;
  solver->model[v]=lbool(value);
}

tvt smt1_propt::l_get(literalt literal) const
{
  if(literal.is_true()) return tvt(true);
  if(literal.is_false()) return tvt(false);

  unsigned v=literal.var_no();
  if(v>=assignment.size()) return tvt(tvt::TV_UNKNOWN);
  tvt r=assignment[v];
  return literal.sign()?!r:r;
}

qbf_squolem_coret::modeltypet qbf_squolem_coret::m_get(literalt a) const
{
  if(squolem->modelIsTrue(a.var_no()))
    return M_TRUE;
  else if(squolem->modelIsFalse(a.var_no()))
    return M_FALSE;
  else if(squolem->modelIsComplex(a.var_no()))
    return M_COMPLEX;
  else
    return M_DONTCARE;
}

literalt aig_prop_baset::lselect(literalt a, literalt b, literalt c)
{  // a?b:c = (a AND b) OR (/a AND c)
  if(a.is_true()) return b;
  if(a.is_false()) return c;
  if(b==c) return b;

  // This produces unnecessary clauses and variables
  // See convert_node for where this overhead is removed

  return lor(land(a, b), land(neg(a), c));
}

std::string dplib_propt::dplib_literal(literalt l)
{
  if(l==const_literal(false))
    return "FALSE";
  else if(l==const_literal(true))
    return "TRUE";

  if(l.sign())
    return "(NOT l"+std::to_string(l.var_no())+")";

  return "l"+std::to_string(l.var_no());
}

void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
{
  assert(!a.is_constant());

  unsigned v=a.var_no();
  bool sign=a.sign();

  // MiniSat2 kills the model in case of UNSAT
  solver->model.growTo(v+1);
  value^=sign;
  solver->model[v]=Minisat::lbool(value);
}

std::string cvc_propt::cvc_literal(literalt l)
{
  if(l==const_literal(false))
    return "FALSE";
  else if(l==const_literal(true))
    return "TRUE";

  if(l.sign())
    return "(NOT l"+i2string(l.var_no())+")";  

  return "l"+i2string(l.var_no());
}

literalt aig_prop_baset::land(literalt a, literalt b)
{
  if(a.is_true()) return b;
  if(b.is_true()) return a;
  if(a.is_false()) return a;
  if(b.is_false()) return b;

  if(a==neg(b)) return const_literal(false);
  if(a==b) return a;

  return dest.new_and_node(a, b);
}

literalt aig_prop_baset::lxor(literalt a, literalt b)
{
  if(a.is_false()) return b;
  if(b.is_false()) return a;
  if(a.is_true()) return neg(b);
  if(b.is_true()) return neg(a);

  if(a==b) return const_literal(false);
  if(a==neg(b)) return const_literal(true);

  // This produces up to three nodes!
  // See convert_node for where this overhead is removed
  return lor(land(a, neg(b)), land(neg(a), b));
}

tvt qbf_squolem_coret::l_get(literalt a) const
{
  if(a.is_true())
    return tvt(tvt::TV_TRUE);
  else if(a.is_false())
    return tvt(tvt::TV_FALSE);
  else if(squolem->modelIsTrue(a.var_no()))
    return tvt(tvt::TV_TRUE);
  else if(squolem->modelIsFalse(a.var_no()) ||
          squolem->modelIsDontCare(a.var_no()))
    return tvt(tvt::TV_FALSE);
  else
    return tvt(tvt::TV_UNKNOWN);
}

std::string smt1_propt::smt1_literal(literalt l)
{
  if(l==const_literal(false))
    return "false";
  else if(l==const_literal(true))
    return "true";
    
  std::string v="B"+i2string(l.var_no());

  if(l.sign())
    return "(not "+v+")";  

  return v;
}

void cvc_convt::convert_literal(const literalt l)
{
    if(l==const_literal(false))
        out << "FALSE";
    else if(l==const_literal(true))
        out << "TRUE";

    if(l.sign())
        out << "(NOT ";

    out << "l" << l.var_no();

    if(l.sign())
        out << ")";
}

void qbf_squolem_coret::set_quantifier(
  const quantifiert::typet type,
  const literalt l)
{
  qdimacs_cnft::set_quantifier(type, l);
  squolem->requantifyVariable(l.var_no(), type==quantifiert::UNIVERSAL);
}