本文整理汇总了C++中const_literal函数的典型用法代码示例。如果您正苦于以下问题:C++ const_literal函数的具体用法?C++ const_literal怎么用?C++ const_literal使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了const_literal函数的18个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: sticky_right_shift
bvt float_utilst::sticky_right_shift(
const bvt &op,
const bvt &dist,
literalt &sticky)
{
std::size_t d=1;
bvt result=op;
sticky=const_literal(false);
for(std::size_t stage=0; stage<dist.size(); stage++)
{
if(dist[stage]!=const_literal(false))
{
bvt tmp=bv_utils.shift(result, bv_utilst::LRIGHT, d);
bvt lost_bits;
if(d<=result.size())
lost_bits=bv_utils.extract(result, 0, d-1);
else
lost_bits=result;
sticky=prop.lor(
prop.land(dist[stage],prop.lor(lost_bits)),
sticky);
result=bv_utils.select(dist[stage], tmp, result);
}
d=d<<1;
}
return result;
}
开发者ID:diffblue,项目名称:cbmc,代码行数:34,代码来源:float_utils.cpp
示例2: conversion_failed
void boolbvt::convert_cond(const exprt &expr, bvt &bv)
{
const exprt::operandst &operands=expr.operands();
unsigned width=boolbv_width(expr.type());
if(width==0)
return conversion_failed(expr, bv);
bv.resize(width);
// make it free variables
Forall_literals(it, bv)
*it=prop.new_variable();
if(operands.size()<2)
throw "cond takes at least two operands";
if((operands.size()%2)!=0)
throw "number of cond operands must be even";
if(prop.has_set_to())
{
bool condition=true;
literalt previous_cond=const_literal(false);
literalt cond_literal=const_literal(false);
forall_operands(it, expr)
{
if(condition)
{
cond_literal=convert(*it);
cond_literal=prop.land(prop.lnot(previous_cond), cond_literal);
previous_cond=prop.lor(previous_cond, cond_literal);
}
else
{
const bvt &op=convert_bv(*it);
if(bv.size()!=op.size())
{
std::cerr << "result size: " << bv.size()
<< std::endl
<< "operand: " << op.size() << std::endl
<< it->pretty()
<< std::endl;
throw "size of value operand does not match";
}
literalt value_literal=bv_utils.equal(bv, op);
prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
}
condition=!condition;
}
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:59,代码来源:boolbv_cond.cpp
示例3: assert
literalt float_utilst::fraction_rounding_decision(
const std::size_t dest_bits,
const literalt sign,
const bvt &fraction)
{
assert(dest_bits<fraction.size());
// we have too many fraction bits
std::size_t extra_bits=fraction.size()-dest_bits;
// more than two extra bits are superflus, and are
// turned into a sticky bit
literalt sticky_bit=const_literal(false);
if(extra_bits>=2)
{
// We keep most-significant bits, and thus the tail is made
// of least-significant bits.
bvt tail=bv_utils.extract(fraction, 0, extra_bits-2);
sticky_bit=prop.lor(tail);
}
// the rounding bit is the last extra bit
assert(extra_bits>=1);
literalt rounding_bit=fraction[extra_bits-1];
// we get one bit of the fraction for some rounding decisions
literalt rounding_least=fraction[extra_bits];
// round-to-nearest (ties to even)
literalt round_to_even=
prop.land(rounding_bit,
prop.lor(rounding_least, sticky_bit));
// round up
literalt round_to_plus_inf=
prop.land(!sign,
prop.lor(rounding_bit, sticky_bit));
// round down
literalt round_to_minus_inf=
prop.land(sign,
prop.lor(rounding_bit, sticky_bit));
// round to zero
literalt round_to_zero=
const_literal(false);
// now select appropriate one
return prop.lselect(rounding_mode_bits.round_to_even, round_to_even,
prop.lselect(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
prop.lselect(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
prop.lselect(rounding_mode_bits.round_to_zero, round_to_zero,
prop.new_variable())))); // otherwise non-det
}
开发者ID:diffblue,项目名称:cbmc,代码行数:56,代码来源:float_utils.cpp
示例4: lxor
literalt z3_propt::lxor(literalt a, literalt b)
{
if(a==const_literal(false)) return b;
if(b==const_literal(false)) return a;
if(a==const_literal(true)) return lnot(b);
if(b==const_literal(true)) return lnot(a);
literalt o=new_variable();
lxor(a, b, o);
return o;
}
开发者ID:smaorus,项目名称:rvt,代码行数:11,代码来源:z3_prop.cpp
示例5: if
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
示例6: build_constant
bvt float_utilst::build_constant(const ieee_floatt &src)
{
unbiased_floatt result;
result.sign=const_literal(src.get_sign());
result.NaN=const_literal(src.is_NaN());
result.infinity=const_literal(src.is_infinity());
result.exponent=bv_utils.build_constant(src.get_exponent(), spec.e);
result.fraction=bv_utils.build_constant(src.get_fraction(), spec.f+1);
return pack(bias(result));
}
开发者ID:diffblue,项目名称:cbmc,代码行数:12,代码来源:float_utils.cpp
示例7: if
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
示例8: lxor
literalt cvc_propt::lxor(const bvt &bv)
{
if(bv.empty()) return const_literal(false);
if(bv.size()==1) return bv[0];
if(bv.size()==2) return lxor(bv[0], bv[1]);
literalt literal=const_literal(false);
forall_literals(it, bv)
literal=lxor(*it, literal);
return literal;
}
开发者ID:sarnold,项目名称:cbmc,代码行数:13,代码来源:cvc_prop.cpp
示例9: lor
literalt z3_propt::lselect(literalt a, literalt b, literalt c)
{
// a?b:c = (a AND b) OR (/a AND c)
if(a==const_literal(true)) return b;
if(a==const_literal(false)) return c;
if(b==c) return b;
bvt bv;
bv.reserve(2);
bv.push_back(land(a, b));
bv.push_back(land(lnot(a), c));
return lor(bv);
}
开发者ID:smaorus,项目名称:rvt,代码行数:13,代码来源:z3_prop.cpp
示例10:
literalt z3_propt::lxor(const bvt &bv)
{
if(bv.size()==0) return const_literal(false);
if(bv.size()==1) return bv[0];
if(bv.size()==2) return lxor(bv[0], bv[1]);
literalt literal=const_literal(false);
for(unsigned i=0; i<bv.size(); i++)
literal=lxor(bv[i], literal);
return literal;
}
开发者ID:smaorus,项目名称:rvt,代码行数:13,代码来源:z3_prop.cpp
示例11: 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
示例12: 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
示例13: if
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
示例14: lxor
literalt boolector_propt::lxor(literalt a, literalt b)
{
if(a==const_literal(false)) return b;
if(b==const_literal(false)) return a;
if(a==const_literal(true)) return lnot(b);
if(b==const_literal(true)) return lnot(a);
literalt l=new_variable();
BtorExp *result;
result = boolector_xor(boolector_ctx, boolector_literal(a), boolector_literal(b));
boolector_assert(boolector_ctx, boolector_iff(boolector_ctx, boolector_literal(l), result));
return l;
}
开发者ID:smaorus,项目名称:rvt,代码行数:16,代码来源:boolector_prop.cpp
示例15: lxor
literalt dplib_propt::lxor(literalt a, literalt b)
{
if(a==const_literal(false))
return b;
if(b==const_literal(false))
return a;
if(a==const_literal(true))
return !b;
if(b==const_literal(true))
return !a;
literalt o=def_dplib_literal();
out << "!(" << dplib_literal(a) << " <-> " << dplib_literal(b)
<< ");\n\n";
return o;
}
开发者ID:danpoe,项目名称:cbmc,代码行数:17,代码来源:dplib_prop.cpp
示例16: lselect
literalt cvc_propt::lselect(literalt a, literalt b, literalt c)
{
if(a==const_literal(true)) return b;
if(a==const_literal(false)) return c;
if(b==c) return b;
out << "%% lselect" << std::endl;
literalt o=def_cvc_literal();
out << "IF " << cvc_literal(a) << " THEN "
<< cvc_literal(b) << " ELSE "
<< cvc_literal(c) << " ENDIF;"
<< std::endl << std::endl;
return o;
}
开发者ID:sarnold,项目名称:cbmc,代码行数:17,代码来源:cvc_prop.cpp
示例17: boolector_false
BtorExp* boolector_propt::boolector_literal(literalt l)
{
BtorExp *literal_l;
std::string literal_s;
if(l==const_literal(false))
return boolector_false(boolector_ctx);
else if(l==const_literal(true))
return boolector_true(boolector_ctx);
literal_l = convert_literal(l.var_no());
if(l.sign())
return boolector_not(boolector_ctx, literal_l);
return literal_l;
}
开发者ID:smaorus,项目名称:rvt,代码行数:17,代码来源:boolector_prop.cpp
示例18: indices_equal
void arrayst::add_array_Ackermann_constraints()
{
// this is quadratic!
// iterate over arrays
for(unsigned i=0; i<arrays.size(); i++)
{
const index_sett &index_set=index_map[arrays.find_number(i)];
// iterate over indices, 2x!
for(index_sett::const_iterator
i1=index_set.begin();
i1!=index_set.end();
i1++)
for(index_sett::const_iterator
i2=index_set.begin();
i2!=index_set.end();
i2++)
if(i1!=i2)
{
// skip if both are constants
if(i1->is_constant() && i2->is_constant())
continue;
// index equality
equality_exprt indices_equal(*i1, *i2);
if(indices_equal.op0().type()!=
indices_equal.op1().type())
{
indices_equal.op1().
make_typecast(indices_equal.op0().type());
}
literalt indices_equal_lit=convert(indices_equal);
if(indices_equal_lit!=const_literal(false))
{
index_exprt index_expr1;
index_expr1.type()=ns.follow(arrays[i].type()).subtype();
index_expr1.array()=arrays[i];
index_expr1.index()=*i1;
index_exprt index_expr2=index_expr1;
index_expr2.index()=*i2;
equality_exprt values_equal(index_expr1, index_expr2);
bvt implication;
implication.reserve(2);
implication.push_back(prop.lnot(indices_equal_lit));
implication.push_back(convert(values_equal));
prop.lcnf(implication);
}
}
}
}
开发者ID:smaorus,项目名称:rvt,代码行数:57,代码来源:arrays.cpp
注:本文中的const_literal函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论