本文整理汇总了C++中literal类的典型用法代码示例。如果您正苦于以下问题:C++ literal类的具体用法?C++ literal怎么用?C++ literal使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了literal类的10个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: display_literal_info
void context::display_literal_info(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr());
if (l.sign())
out << " (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ") ";
else
out << " " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << " ";
out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n";
}
开发者ID:extremecoders-re,项目名称:z3,代码行数:8,代码来源:smt_context_pp.cpp
示例2: TRACE
bool context::check_watch_list(literal l) const {
watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]);
l.neg();
watch_list::clause_iterator it = wl.begin_clause();
watch_list::clause_iterator end = wl.end_clause();
for (; it != end; ++it) {
clause * cls = *it;
TRACE("watch_list", tout << "l: "; display_literal(tout, l); tout << "\n";
display_clause(tout, cls); tout << "\n";);
SASSERT(l == cls->get_literal(0) || l == cls->get_literal(1));
}
开发者ID:veleek,项目名称:z3,代码行数:11,代码来源:smt_context_inv.cpp
示例3: display_literal
void context::display_watch_list(std::ostream & out, literal l) const {
display_literal(out, l); out << " watch_list:\n";
watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]);
watch_list::clause_iterator it = wl.begin_clause();
watch_list::clause_iterator end = wl.end_clause();
for (; it != end; ++it) {
display_clause(out, *it); out << "\n";
}
}
开发者ID:extremecoders-re,项目名称:z3,代码行数:9,代码来源:smt_context_pp.cpp
示例4: insert_p
void superposition::insert_p(clause * cls, literal & l, unsigned i) {
l.set_p_indexed(true);
expr * atom = l.atom();
if (!m_manager.is_eq(atom))
return;
if (l.is_oriented())
insert_p(cls, l.is_left() ? l.lhs() : l.rhs(), i);
else {
insert_p(cls, l.lhs(), i);
insert_p(cls, l.rhs(), i);
}
}
开发者ID:Moondee,项目名称:Artemis,代码行数:12,代码来源:spc_superposition.cpp
示例5: s
/**
\brief Return true if l is a maximal selected literal in the clause, given a substitution s.
s(l) is considered maximal selected literal if there is no
selected literal l' in the clause such s(l') is greater than s(l).
*/
bool clause::is_sel_maximal(order & o, literal const & l, unsigned offset, substitution * s) const {
if (!l.is_selected())
return false;
unsigned num_lits = get_num_literals();
for (unsigned i = 0; i < num_lits; i++) {
literal const & l_prime = m_lits[i];
if (l != l_prime && l_prime.is_selected() && greater(o, l_prime, l, offset, s))
return false;
}
return true;
}
开发者ID:Moondee,项目名称:Artemis,代码行数:17,代码来源:spc_clause.cpp
示例6: insert_r
void superposition::insert_r(clause * cls, literal & l, unsigned i) {
l.set_r_indexed(true);
expr * atom = l.atom();
if (m_manager.is_eq(atom)) {
expr * lhs = l.lhs();
expr * rhs = l.rhs();
if (l.is_oriented()) {
bool left = true;
if (!l.is_left()) {
left = false;
std::swap(lhs, rhs);
}
insert_r(cls, lhs, i, left);
}
else {
insert_r(cls, lhs, i, true);
insert_r(cls, rhs, i, false);
}
}
else {
insert_r(cls, atom, i, false);
}
m_subst.reserve_vars(m_r.get_approx_num_regs());
}
开发者ID:Moondee,项目名称:Artemis,代码行数:24,代码来源:spc_superposition.cpp
示例7: norm
inline literal norm(literal_vector const & roots, literal l) {
if (l.sign())
return ~roots[l.var()];
else
return roots[l.var()];
}
开发者ID:jackluo923,项目名称:juxta,代码行数:6,代码来源:sat_elim_eqs.cpp
示例8: literal
literal(literal<U, Domain> const &u)
: base_type(terminal_type::make(u.get()))
{}
开发者ID:0xDEC0DE8,项目名称:mcsema,代码行数:3,代码来源:literal.hpp
示例9: operator
void repr_printer::operator()(const literal &n) {
print_name("Literal", n.id());
}
开发者ID:bryancatanzaro,项目名称:copperhead-compiler,代码行数:3,代码来源:repr_printer.cpp
示例10: operator
bool operator()(literal const & l1, literal const & l2) const {
if (l1.is_ground() > l2.is_ground())
return true;
if (l1.is_ground() != l2.is_ground())
return false;
if (l1.get_approx_depth() > l2.get_approx_depth())
return true;
if (l1.get_approx_depth() != l2.get_approx_depth())
return false;
if (l1.get_approx_sym_count() > l2.get_approx_sym_count())
return true;
if (l1.get_approx_sym_count() != l2.get_approx_sym_count())
return false;
if (l1.get_approx_const_count() > l2.get_approx_const_count())
return true;
if (l1.get_approx_const_count() != l2.get_approx_const_count())
return false;
return l1.get_id() < l2.get_id();
}
开发者ID:Moondee,项目名称:Artemis,代码行数:19,代码来源:spc_clause.cpp
注:本文中的literal类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论