本文整理汇总了C++中unsigned_vector类的典型用法代码示例。如果您正苦于以下问题:C++ unsigned_vector类的具体用法?C++ unsigned_vector怎么用?C++ unsigned_vector使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了unsigned_vector类的14个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: pop_bound
/**
\brief From \c cont which is list of indexes of tail literals of rule \c r, select
the index pointing to a literal with at least one bound variable that will be the next
bound literal in the process of creating an adorned rule. If all literals are unbound,
return -1.
*/
int mk_magic_sets::pop_bound(unsigned_vector & cont, rule * r, const var_idx_set & bound_vars) {
float best_cost;
int candidate_index = -1;
unsigned n = cont.size();
for (unsigned i=0; i<n; i++) {
app * lit = r->get_tail(cont[i]);
unsigned bound_cnt = get_bound_arg_count(lit, bound_vars);
if (bound_cnt==0) {
continue;
}
float cost = get_unbound_cost(lit, bound_vars);
if (candidate_index==-1 || cost<best_cost) {
best_cost = cost;
candidate_index = i;
}
}
if (candidate_index==-1) {
return -1;
}
if (candidate_index != static_cast<int>(n-1)) {
std::swap(cont[candidate_index], cont[n-1]);
}
unsigned res = cont.back();
cont.pop_back();
return res;
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:32,代码来源:dl_mk_magic_sets.cpp
示例2: sort_core
void sort_core(svector<Numeral> & as, unsigned_vector & xs, numeral_buffer<Numeral, numeral_manager> & buffer) {
std::sort(xs.begin(), xs.end());
unsigned num = as.size();
for (unsigned i = 0; i < num; i++) {
m().swap(as[i], buffer[xs[i]]);
}
}
开发者ID:killbug2004,项目名称:Snippets,代码行数:7,代码来源:euclidean_solver.cpp
示例3: collect_indices
void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const
{
indices.reset();
index_collector collector(*this);
for_each_expr(collector, m_visited, e);
m_visited.reset();
collector.extract(indices);
}
开发者ID:chadbrewbaker,项目名称:z3,代码行数:8,代码来源:spacer_sym_mux.cpp
示例4: extract
void extract(unsigned_vector& indices)
{
for (unsigned i = 0; i < m_indices.size(); ++i) {
if (m_indices[i]) {
indices.push_back(i);
}
}
}
开发者ID:chadbrewbaker,项目名称:z3,代码行数:8,代码来源:spacer_sym_mux.cpp
示例5: get_renaming_args
void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig,
expr_ref_vector & renaming_arg) {
ast_manager & m = renaming_arg.get_manager();
unsigned sz = map.size();
unsigned ofs = sz-1;
renaming_arg.resize(sz, static_cast<expr *>(0));
for(unsigned i=0; i<sz; i++) {
if(map[i]!=UINT_MAX) {
renaming_arg.set(ofs-i, m.mk_var(map[i], orig_sig[i]));
}
}
}
开发者ID:Jornason,项目名称:z3,代码行数:12,代码来源:dl_base.cpp
示例6: accumulate
void accumulate(tbv const& t, unsigned_vector& acc) {
ddnf_node* n = find(t);
ptr_vector<ddnf_node> todo;
todo.push_back(n);
while (!todo.empty()) {
n = todo.back();
todo.pop_back();
unsigned id = n->get_id();
if (m_marked[id]) continue;
acc.push_back(id);
m_marked[id] = true;
unsigned sz = n->num_children();
for (unsigned i = 0; i < sz; ++i) {
todo.push_back((*n)[i]);
}
}
}
开发者ID:EinNarr,项目名称:z3,代码行数:17,代码来源:ddnf.cpp
示例7: expand_column_vector
void udoc_relation::expand_column_vector(unsigned_vector& v, const udoc_relation* other) const {
unsigned_vector orig;
orig.swap(v);
for (unsigned i = 0; i < orig.size(); ++i) {
unsigned col, limit;
if (orig[i] < get_num_cols()) {
col = column_idx(orig[i]);
limit = col + column_num_bits(orig[i]);
} else {
unsigned idx = orig[i] - get_num_cols();
col = get_num_bits() + other->column_idx(idx);
limit = col + other->column_num_bits(idx);
}
for (; col < limit; ++col) {
v.push_back(col);
}
}
}
开发者ID:greatmazinger,项目名称:z3,代码行数:18,代码来源:udoc_relation.cpp
示例8:
void tactic2solver::pop_core(unsigned n) {
unsigned new_lvl = m_scopes.size() - n;
unsigned old_sz = m_scopes[new_lvl];
m_assertions.shrink(old_sz);
m_scopes.shrink(new_lvl);
m_result = 0;
}
开发者ID:perillaseed,项目名称:z3,代码行数:7,代码来源:tactic2solver.cpp
示例9: pop
void pop(unsigned num_scopes) {
SASSERT(m_bounds.empty()); // bounds must be flushed before pop.
if (num_scopes > 0) {
SASSERT(num_scopes <= m_enum_consts_lim.size());
unsigned new_sz = m_enum_consts_lim.size() - num_scopes;
unsigned lim = m_enum_consts_lim[new_sz];
for (unsigned i = m_enum_consts.size(); i > lim; ) {
--i;
func_decl* f = m_enum_consts[i].get();
func_decl* f_fresh = m_enum2bv.find(f);
m_bv2enum.erase(f_fresh);
m_enum2bv.erase(f);
m_enum2def.erase(f);
}
m_enum_consts_lim.resize(new_sz);
m_enum_consts.resize(lim);
m_enum_defs.resize(lim);
m_enum_bvs.resize(lim);
}
m_rw.reset();
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:21,代码来源:enum2bv_rewriter.cpp
示例10: display_results
static void display_results() {
if (g_opt) {
for (unsigned i = 0; i < g_handles.size(); ++i) {
expr_ref lo = g_opt->get_lower(g_handles[i]);
expr_ref hi = g_opt->get_upper(g_handles[i]);
if (lo == hi) {
std::cout << " " << lo << "\n";
}
else {
std::cout << " [" << lo << ":" << hi << "]\n";
}
}
}
}
开发者ID:greatmazinger,项目名称:z3,代码行数:14,代码来源:opt_frontend.cpp
示例11: group_by
void group_by(table_fact const& in, table_fact& out) {
out.reset();
for (unsigned i = 0; i < m_group_by_cols.size(); ++i) {
out.push_back(in[m_group_by_cols[i]]);
}
}
开发者ID:killbug2004,项目名称:Snippets,代码行数:6,代码来源:dl_base.cpp
示例12: operator
virtual void operator()(table_base& _t) {
lazy_table& t = get(_t);
t.set(alloc(lazy_table_filter_identical, m_cols.size(), m_cols.c_ptr(), t));
}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:4,代码来源:dl_lazy_table.cpp
示例13: push
void push() {
m_enum_consts_lim.push_back(m_enum_consts.size());
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:3,代码来源:enum2bv_rewriter.cpp
示例14: scope_level
unsigned scope_level() const override { return m_scopes.size(); }
开发者ID:NikolajBjorner,项目名称:z3,代码行数:1,代码来源:ctx_simplify_tactic.cpp
注:本文中的unsigned_vector类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论