本文整理汇总了C++中literalt类的典型用法代码示例。如果您正苦于以下问题:C++ literalt类的具体用法?C++ literalt怎么用?C++ literalt使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了literalt类的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: tvt
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;
}
开发者ID:smaorus,项目名称:rvt,代码行数:35,代码来源:z3_prop.cpp
示例2: l_get
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;
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:28,代码来源:satcheck_booleforce.cpp
示例3: l_get
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());
}
开发者ID:diffblue,项目名称:cbmc,代码行数:7,代码来源:cvc_conv.cpp
示例4: l_get
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;
}
开发者ID:smaorus,项目名称:rvt,代码行数:30,代码来源:boolector_prop.cpp
示例5: f_get
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;
}
}
开发者ID:sarnold,项目名称:cbmc,代码行数:59,代码来源:qbf_squolem_core.cpp
示例6: assert
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);
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:8,代码来源:smt1_prop.cpp
示例7: set_frozen
void satcheck_glucose_simplifiert::set_frozen(literalt a)
{
if(!a.is_constant())
{
add_variables();
solver->setFrozen(a.var_no(), true);
}
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:8,代码来源:satcheck_glucose.cpp
示例8:
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);
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:8,代码来源:satcheck_minisat.cpp
示例9:
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;
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:10,代码来源:smt1_prop.cpp
示例10: m_get
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;
}
开发者ID:sarnold,项目名称:cbmc,代码行数:11,代码来源:qbf_squolem_core.cpp
示例11: lselect
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));
}
开发者ID:diffblue,项目名称:cbmc,代码行数:11,代码来源:aig_prop.cpp
示例12: dplib_literal
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());
}
开发者ID:danpoe,项目名称:cbmc,代码行数:12,代码来源:dplib_prop.cpp
示例13: assert
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);
}
开发者ID:sarnold,项目名称:cbmc,代码行数:12,代码来源:satcheck_minisat2.cpp
示例14: cvc_literal
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());
}
开发者ID:sarnold,项目名称:cbmc,代码行数:12,代码来源:cvc_prop.cpp
示例15: land
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);
}
开发者ID:diffblue,项目名称:cbmc,代码行数:12,代码来源:aig_prop.cpp
示例16: lxor
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));
}
开发者ID:diffblue,项目名称:cbmc,代码行数:14,代码来源:aig_prop.cpp
示例17: l_get
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);
}
开发者ID:sarnold,项目名称:cbmc,代码行数:14,代码来源:qbf_squolem_core.cpp
示例18: if
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;
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:14,代码来源:smt1_prop.cpp
示例19: convert_literal
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 << ")";
}
开发者ID:diffblue,项目名称:cbmc,代码行数:15,代码来源:cvc_conv.cpp
示例20: set_quantifier
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);
}
开发者ID:sarnold,项目名称:cbmc,代码行数:7,代码来源:qbf_squolem_core.cpp
注:本文中的literalt类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论