diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 50dd3d6eb..0306f7a37 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3110,7 +3110,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro app const * cls = to_app(f1); unsigned num_args = cls->get_num_args(); #ifdef Z3DEBUG - svector found; + bool_vector found; #endif ast_mark mark; for (unsigned i = 0; i < num_args; i++) { diff --git a/src/ast/expr2polynomial.h b/src/ast/expr2polynomial.h index 8becf55dd..b11365509 100644 --- a/src/ast/expr2polynomial.h +++ b/src/ast/expr2polynomial.h @@ -100,7 +100,7 @@ protected: }; class default_expr2polynomial : public expr2polynomial { - svector m_is_int; + bool_vector m_is_int; public: default_expr2polynomial(ast_manager & am, polynomial::manager & pm); ~default_expr2polynomial() override; diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index 863f2c57e..255fdfb1f 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -34,9 +34,9 @@ public: ptr_vector m_fs; expr_ref_vector m_defs; expr_ref_vector m_conds; - svector m_ineq; // true if the macro is based on an inequality instead of equality. - svector m_satisfy; - svector m_hint; // macro did not contain all universal variables in the quantifier. + bool_vector m_ineq; // true if the macro is based on an inequality instead of equality. + bool_vector m_satisfy; + bool_vector m_hint; // macro did not contain all universal variables in the quantifier. friend class macro_util; ast_manager & get_manager() { return m_conds.get_manager(); } diff --git a/src/ast/static_features.h b/src/ast/static_features.h index f7a59ca00..361ec35a8 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -112,7 +112,7 @@ struct static_features { u_map m_expr2formula_depth; unsigned m_num_theories; - svector m_theories; // mapping family_id -> bool + bool_vector m_theories; // mapping family_id -> bool symbol m_label_sym; symbol m_pattern_sym; diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index 6b995c8cf..4750c6da8 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -440,7 +440,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_produ inv[mv.dst()].push_back(move_t(m, mv.dst(), mv.src(), mv.t())); } - svector back_reachable(n, false); + bool_vector back_reachable(n, false); for (unsigned f : final) { back_reachable[f] = true; } diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp index 1ead43d70..ccc5b67d2 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -748,7 +748,7 @@ namespace dd { void bdd_manager::gc() { m_free_nodes.reset(); IF_VERBOSE(13, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";); - svector reachable(m_nodes.size(), false); + bool_vector reachable(m_nodes.size(), false); for (unsigned i = m_bdd_stack.size(); i-- > 0; ) { reachable[m_bdd_stack[i]] = true; m_todo.push_back(m_bdd_stack[i]); diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index e00ab6a0f..224de5ee2 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -952,12 +952,12 @@ namespace dd { } bool pdd_manager::is_reachable(PDD p) { - svector reachable(m_nodes.size(), false); + bool_vector reachable(m_nodes.size(), false); compute_reachable(reachable); return reachable[p]; } - void pdd_manager::compute_reachable(svector& reachable) { + void pdd_manager::compute_reachable(bool_vector& reachable) { for (unsigned i = m_pdd_stack.size(); i-- > 0; ) { reachable[m_pdd_stack[i]] = true; m_todo.push_back(m_pdd_stack[i]); @@ -994,7 +994,7 @@ namespace dd { m_free_nodes.reset(); SASSERT(well_formed()); IF_VERBOSE(13, verbose_stream() << "(pdd :gc " << m_nodes.size() << ")\n";); - svector reachable(m_nodes.size(), false); + bool_vector reachable(m_nodes.size(), false); compute_reachable(reachable); for (unsigned i = m_nodes.size(); i-- > pdd_no_op; ) { if (!reachable[i]) { diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 86e569b09..b24f95c6d 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -227,7 +227,7 @@ namespace dd { bool var_is_leaf(PDD p, unsigned v); bool is_reachable(PDD p); - void compute_reachable(svector& reachable); + void compute_reachable(bool_vector& reachable); void try_gc(); void reserve_var(unsigned v); bool well_formed(); diff --git a/src/math/hilbert/hilbert_basis.h b/src/math/hilbert/hilbert_basis.h index 54208d268..cb4dd146e 100644 --- a/src/math/hilbert/hilbert_basis.h +++ b/src/math/hilbert/hilbert_basis.h @@ -88,7 +88,7 @@ class hilbert_basis { reslimit& m_limit; vector m_ineqs; // set of asserted inequalities - svector m_iseq; // inequalities that are equalities + bool_vector m_iseq; // inequalities that are equalities num_vector m_store; // store of vectors svector m_basis; // vector of current basis svector m_free_list; // free list of unused storage diff --git a/src/math/lp/factorization.cpp b/src/math/lp/factorization.cpp index f74663f06..c4e8fb90b 100644 --- a/src/math/lp/factorization.cpp +++ b/src/math/lp/factorization.cpp @@ -75,7 +75,7 @@ void const_iterator_mon::advance_mask() { const_iterator_mon::self_type const_iterator_mon::operator++() { self_type i = *this; operator++(1); return i; } const_iterator_mon::self_type const_iterator_mon::operator++(int) { advance_mask(); return *this; } -const_iterator_mon::const_iterator_mon(const svector& mask, const factorization_factory *f) : +const_iterator_mon::const_iterator_mon(const bool_vector& mask, const factorization_factory *f) : m_mask(mask), m_ff(f) , m_full_factorization_returned(false) diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h index e21a53044..78f3ab1a4 100644 --- a/src/math/lp/factorization.h +++ b/src/math/lp/factorization.h @@ -77,7 +77,7 @@ public: struct const_iterator_mon { // fields - svector m_mask; + bool_vector m_mask; const factorization_factory * m_ff; bool m_full_factorization_returned; @@ -97,7 +97,7 @@ struct const_iterator_mon { self_type operator++(); self_type operator++(int); - const_iterator_mon(const svector& mask, const factorization_factory *f); + const_iterator_mon(const bool_vector& mask, const factorization_factory *f); bool operator==(const self_type &other) const; bool operator!=(const self_type &other) const; @@ -119,15 +119,15 @@ struct factorization_factory { m_vars(vars), m_monic(m) { } - svector get_mask() const { + bool_vector get_mask() const { // we keep the last element always in the first factor to avoid // repeating a pair twice, that is why m_mask is shorter by one then m_vars return m_vars.size() != 2 ? - svector(m_vars.size() - 1, false) + bool_vector(m_vars.size() - 1, false) : - svector(1, true); // init mask as in the end() since the full iteration will do the job + bool_vector(1, true); // init mask as in the end() since the full iteration will do the job } const_iterator_mon begin() const { @@ -135,7 +135,7 @@ struct factorization_factory { } const_iterator_mon end() const { - svector mask(m_vars.size() - 1, true); + bool_vector mask(m_vars.size() - 1, true); auto it = const_iterator_mon(mask, this); it.m_full_factorization_returned = true; return it; diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 09c00ef36..8da02e94e 100644 --- a/src/math/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -74,7 +74,7 @@ class var_eqs { trail_stack m_stack; mutable svector m_todo; - mutable svector m_marked; + mutable bool_vector m_marked; mutable unsigned_vector m_marked_trail; mutable svector m_justtrail; diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 4f7a6ab8c..7f4d26c8d 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -1272,7 +1272,7 @@ namespace polynomial { SASSERT(sz == num_vars()); DEBUG_CODE({ // check whether xs is really a permutation - svector found; + bool_vector found; found.resize(num_vars(), false); for (unsigned i = 0; i < sz; i++) { SASSERT(xs[i] < num_vars()); @@ -3218,7 +3218,7 @@ namespace polynomial { } }; - svector m_found_vars; + bool_vector m_found_vars; void vars(polynomial const * p, var_vector & xs) { xs.reset(); m_found_vars.reserve(num_vars(), false); diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h index 816914545..712dabba5 100644 --- a/src/math/polynomial/upolynomial_factorization_int.h +++ b/src/math/polynomial/upolynomial_factorization_int.h @@ -138,7 +138,7 @@ namespace upolynomial { // the factors to select from factors_type const & m_factors; // which factors are enabled - svector m_enabled; + bool_vector m_enabled; // the size of the current selection int m_current_size; // the current selection: indices at positions < m_current_size, other values are maxed out diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index 30442fc58..7311850ab 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -85,7 +85,7 @@ namespace opt { static const unsigned m_objective_id = 0; vector m_var2row_ids; vector m_var2value; - svector m_var2is_int; + bool_vector m_var2is_int; vector m_new_vars; unsigned_vector m_lub, m_glb, m_mod; unsigned_vector m_above, m_below; diff --git a/src/math/simplex/network_flow_def.h b/src/math/simplex/network_flow_def.h index 4a7d00a23..594c01652 100644 --- a/src/math/simplex/network_flow_def.h +++ b/src/math/simplex/network_flow_def.h @@ -224,7 +224,7 @@ namespace smt { node src = m_graph.get_source(m_enter_id); node tgt = m_graph.get_target(m_enter_id); svector path; - svector against; + bool_vector against; m_tree->get_path(src, tgt, path, against); SASSERT(path.size() >= 1); for (unsigned i = 0; i < path.size(); ++i) { @@ -241,7 +241,7 @@ namespace smt { m_delta.set_invalid(); edge_id leave_id = null_edge_id; svector path; - svector against; + bool_vector against; m_tree->get_path(src, tgt, path, against); SASSERT(path.size() >= 1); for (unsigned i = 0; i < path.size(); ++i) { diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index ec514df8f..798dd22ca 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -476,7 +476,7 @@ private: interval_manager m_im; scoped_numeral_vector m_num_buffer; - svector m_is_int; + bool_vector m_is_int; ptr_vector m_defs; vector m_wlist; diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index fe1f101b1..1b9a5cce8 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -153,7 +153,7 @@ namespace datalog { mk_rule_core(fml1, pr, rules, name); } - void rule_manager::mk_negations(app_ref_vector& body, svector& is_negated) { + void rule_manager::mk_negations(app_ref_vector& body, bool_vector& is_negated) { for (unsigned i = 0; i < body.size(); ++i) { expr* e = body[i].get(), *e1; if (m.is_not(e, e1) && m_ctx.is_predicate(e1)) { @@ -628,7 +628,7 @@ namespace datalog { } if (change) { app_ref_vector tail(m); - svector tail_neg; + bool_vector tail_neg; for (unsigned i = 0; i < ut_len; ++i) { tail.push_back(r->get_tail(i)); tail_neg.push_back(r->is_neg_tail(i)); @@ -660,7 +660,7 @@ namespace datalog { var_counter vctr; app_ref_vector tail(m); - svector tail_neg; + bool_vector tail_neg; app_ref head(r->get_head(), m); vctr.count_vars(head); @@ -811,7 +811,7 @@ namespace datalog { expr_ref tmp(m); app_ref new_head(m); app_ref_vector new_tail(m); - svector tail_neg; + bool_vector tail_neg; var_subst vs(m, false); tmp = vs(r->get_head(), sz, es); new_head = to_app(tmp); diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 45b75c254..1c17b8b3a 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -124,7 +124,7 @@ namespace datalog { app_ref_vector m_body; app_ref m_head; expr_ref_vector m_args; - svector m_neg; + bool_vector m_neg; hnf m_hnf; qe_lite m_qe; label_rewriter m_rwr; @@ -158,7 +158,7 @@ namespace datalog { void bind_variables(expr* fml, bool is_forall, expr_ref& result); - void mk_negations(app_ref_vector& body, svector& is_negated); + void mk_negations(app_ref_vector& body, bool_vector& is_negated); void mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name); diff --git a/src/muz/base/dl_rule_transformer.cpp b/src/muz/base/dl_rule_transformer.cpp index 9206efef6..c610d95b9 100644 --- a/src/muz/base/dl_rule_transformer.cpp +++ b/src/muz/base/dl_rule_transformer.cpp @@ -132,7 +132,7 @@ namespace datalog { // //------------------------------ - void rule_transformer::plugin::remove_duplicate_tails(app_ref_vector& tail, svector& tail_neg) + void rule_transformer::plugin::remove_duplicate_tails(app_ref_vector& tail, bool_vector& tail_neg) { //one set for positive and one for negative obj_hashtable tail_apps[2]; diff --git a/src/muz/base/dl_rule_transformer.h b/src/muz/base/dl_rule_transformer.h index 2bcc1da5c..331e76e6a 100644 --- a/src/muz/base/dl_rule_transformer.h +++ b/src/muz/base/dl_rule_transformer.h @@ -108,7 +108,7 @@ namespace datalog { /** Removes duplicate tails. */ - static void remove_duplicate_tails(app_ref_vector& tail, svector& tail_neg); + static void remove_duplicate_tails(app_ref_vector& tail, bool_vector& tail_neg); }; }; diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index d3460738c..26020eacf 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -135,7 +135,7 @@ namespace datalog { ddnf_node::hash m_hash; ddnf_node::eq m_eq; ddnf_nodes m_nodes; - svector m_marked; + bool_vector m_marked; stats m_stats; public: ddnf_mgr(unsigned n): m_noderefs(*this), m_internalized(false), m_tbv(n), @@ -338,7 +338,7 @@ namespace datalog { } ptr_vector todo; todo.push_back(m_root); - svector done(m_noderefs.size(), false); + bool_vector done(m_noderefs.size(), false); while (!todo.empty()) { ddnf_node& n = *todo.back(); if (done[n.get_id()]) { diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 0724d471a..45c712f7c 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -724,7 +724,7 @@ protected: dtoken parse_body(app* head) { app_ref_vector body(m_manager); - svector polarity_vect; + bool_vector polarity_vect; dtoken tok = m_lexer->next_token(); while (tok != TK_ERROR && tok != TK_EOS) { if (tok == TK_PERIOD) { diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 9e2f23977..667640051 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -582,7 +582,7 @@ namespace datalog { const unsigned_vector m_cols2; bool m_all_neg_bound; //all columns are bound at least once bool m_overlap; //one column in negated table is bound multiple times - svector m_bound; + bool_vector m_bound; convenient_negation_filter_fn(const base_object & tgt, const base_object & neg_t, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols) diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 42434942c..7b6a46796 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -92,12 +92,12 @@ namespace datalog { family_id finite_product_relation_plugin::get_relation_kind(finite_product_relation & r, const bool * table_columns) { const relation_signature & sig = r.get_signature(); - svector table_cols_vect(sig.size(), table_columns); + bool_vector table_cols_vect(sig.size(), table_columns); return m_spec_store.get_relation_kind(sig, rel_spec(table_cols_vect)); } void finite_product_relation_plugin::get_all_possible_table_columns(relation_manager & rmgr, - const relation_signature & s, svector & table_columns) { + const relation_signature & s, bool_vector & table_columns) { SASSERT(table_columns.empty()); unsigned s_sz = s.size(); for(unsigned i=0; i table_columns; + bool_vector table_columns; get_all_possible_table_columns(s, table_columns); #ifndef _EXTERNAL_RELEASE unsigned s_sz = s.size(); @@ -275,7 +275,7 @@ namespace datalog { SASSERT(join_fun); scoped_rel res_table = (*join_fun)(t, *idx_singleton); - svector table_cols(sig.size(), true); + bool_vector table_cols(sig.size(), true); finite_product_relation * res = mk_empty(sig, table_cols.c_ptr()); //this one does not need to be deleted -- it will be taken over by \c res in the \c init function @@ -301,7 +301,7 @@ namespace datalog { idx_singleton_fact.push_back(0); idx_singleton->add_fact(idx_singleton_fact); - svector table_cols(sig.size(), false); + bool_vector table_cols(sig.size(), false); finite_product_relation * res = mk_empty(sig, table_cols.c_ptr()); relation_vector rels; @@ -378,7 +378,7 @@ namespace datalog { scoped_ptr m_tjoined_second_rel_remover; //determines which columns of the result are table columns and which are in the inner relation - svector m_res_table_columns; + bool_vector m_res_table_columns; public: class join_maker : public table_row_mutator_fn { @@ -529,7 +529,7 @@ namespace datalog { scoped_ptr m_inner_rel_union; //determines which columns of the result are table columns and which are in the inner relation - svector m_res_table_columns; + bool_vector m_res_table_columns; public: project_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * removed_cols) : convenient_relation_project_fn(r.get_signature(), col_cnt, removed_cols) { @@ -665,7 +665,7 @@ namespace datalog { unsigned_vector m_rel_permutation; //determines which columns of the result are table columns and which are in the inner relation - svector m_res_table_columns; + bool_vector m_res_table_columns; public: rename_fn(const finite_product_relation & r, unsigned cycle_len, const unsigned * permutation_cycle) : convenient_relation_rename_fn(r.get_signature(), cycle_len, permutation_cycle) { @@ -2156,7 +2156,7 @@ namespace datalog { return true; } unsigned sig_sz = rels.back()->get_signature().size(); - svector table_cols(sig_sz, true); + bool_vector table_cols(sig_sz, true); ptr_vector::iterator it = rels.begin(); ptr_vector::iterator end = rels.end(); @@ -2221,7 +2221,7 @@ namespace datalog { scoped_rel moved_cols_trel = rmgr.get_table_relation_plugin(moved_cols_table->get_plugin()).mk_from_table(moved_cols_sig, moved_cols_table); - svector moved_cols_table_flags(moved_cols_sig.size(), false); + bool_vector moved_cols_table_flags(moved_cols_sig.size(), false); scoped_rel moved_cols_rel = get_plugin().mk_empty(moved_cols_sig, moved_cols_table_flags.c_ptr()); diff --git a/src/muz/rel/dl_finite_product_relation.h b/src/muz/rel/dl_finite_product_relation.h index 750ac325f..f59f923cf 100644 --- a/src/muz/rel/dl_finite_product_relation.h +++ b/src/muz/rel/dl_finite_product_relation.h @@ -36,10 +36,10 @@ namespace datalog { public: struct rel_spec { family_id m_inner_kind; //null_family_id means we don't care about the kind - svector m_table_cols; + bool_vector m_table_cols; rel_spec() : m_inner_kind(null_family_id) {} - rel_spec(const svector& table_cols) + rel_spec(const bool_vector& table_cols) : m_inner_kind(null_family_id), m_table_cols(table_cols) {} bool operator==(const rel_spec & o) const { @@ -74,8 +74,8 @@ namespace datalog { family_id get_relation_kind(finite_product_relation & r, const bool * table_columns); static void get_all_possible_table_columns(relation_manager & rmgr, const relation_signature & s, - svector & table_columns); - void get_all_possible_table_columns(const relation_signature & s, svector & table_columns) { + bool_vector & table_columns); + void get_all_possible_table_columns(const relation_signature & s, bool_vector & table_columns) { get_all_possible_table_columns(get_manager(), s, table_columns); } diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index e1a1d40b9..5aa2b54c9 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -644,10 +644,10 @@ namespace datalog { relation_signature sig; rmgr.from_predicate(e_decl, sig); - svector inner_sieve(sz-1, true); + bool_vector inner_sieve(sz-1, true); inner_sieve.push_back(false); - svector expl_sieve(sz-1, false); + bool_vector expl_sieve(sz-1, false); expl_sieve.push_back(true); sieve_relation_plugin & sieve_plugin = sieve_relation_plugin::get_plugin(rmgr); @@ -715,7 +715,7 @@ namespace datalog { app_ref e_head(get_e_lit(r->get_head(), head_var), m_manager); app_ref_vector e_tail(m_manager); - svector neg_flags; + bool_vector neg_flags; unsigned pos_tail_sz = r->get_positive_tail_size(); for (unsigned i=0; iget_head(); ptr_vector new_tail; - svector new_negs; + bool_vector new_negs; unsigned tail_sz = r->get_tail_size(); for (unsigned i=0; iget_tail(i)); diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index f89b2150c..69330fd46 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -711,7 +711,7 @@ namespace datalog { } ptr_vector tail(content); - svector negs(tail.size(), false); + bool_vector negs(tail.size(), false); unsigned or_len = orig_r->get_tail_size(); for (unsigned i=orig_r->get_positive_tail_size(); i < or_len; i++) { tail.push_back(orig_r->get_tail(i)); diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp index c4c8959ef..b47a151c6 100644 --- a/src/muz/rel/dl_sieve_relation.cpp +++ b/src/muz/rel/dl_sieve_relation.cpp @@ -149,7 +149,7 @@ namespace datalog { } void sieve_relation_plugin::extract_inner_columns(const relation_signature & s, relation_plugin & inner, - svector & inner_columns) { + bool_vector & inner_columns) { SASSERT(inner_columns.size()==s.size()); unsigned n = s.size(); relation_signature inner_sig_singleton; @@ -168,7 +168,7 @@ namespace datalog { } void sieve_relation_plugin::collect_inner_signature(const relation_signature & s, - const svector & inner_columns, relation_signature & inner_sig) { + const bool_vector & inner_columns, relation_signature & inner_sig) { SASSERT(inner_columns.size()==s.size()); inner_sig.reset(); unsigned n = s.size(); @@ -183,7 +183,7 @@ namespace datalog { relation_signature & inner_sig) { UNREACHABLE(); #if 0 - svector inner_cols(s.size()); + bool_vector inner_cols(s.size()); extract_inner_columns(s, inner_cols.c_ptr()); collect_inner_signature(s, inner_cols, inner_sig); #endif @@ -228,7 +228,7 @@ namespace datalog { UNREACHABLE(); return nullptr; #if 0 - svector inner_cols(s.size()); + bool_vector inner_cols(s.size()); extract_inner_columns(s, inner_cols.c_ptr()); return mk_empty(s, inner_cols.c_ptr()); #endif @@ -236,7 +236,7 @@ namespace datalog { sieve_relation * sieve_relation_plugin::mk_empty(const relation_signature & s, relation_plugin & inner_plugin) { SASSERT(!inner_plugin.is_sieve_relation()); //it does not make sense to make a sieve of a sieve - svector inner_cols(s.size()); + bool_vector inner_cols(s.size()); extract_inner_columns(s, inner_plugin, inner_cols); relation_signature inner_sig; collect_inner_signature(s, inner_cols, inner_sig); @@ -248,14 +248,14 @@ namespace datalog { relation_signature empty_sig; relation_plugin& plugin = get_manager().get_appropriate_plugin(s); relation_base * inner = plugin.mk_full(p, empty_sig, null_family_id); - svector inner_cols; + bool_vector inner_cols; inner_cols.resize(s.size(), false); return mk_from_inner(s, inner_cols, inner); } sieve_relation * sieve_relation_plugin::full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) { SASSERT(!inner_plugin.is_sieve_relation()); //it does not make sense to make a sieve of a sieve - svector inner_cols(s.size()); + bool_vector inner_cols(s.size()); extract_inner_columns(s, inner_plugin, inner_cols); relation_signature inner_sig; collect_inner_signature(s, inner_cols, inner_sig); @@ -267,7 +267,7 @@ namespace datalog { sieve_relation_plugin & m_plugin; unsigned_vector m_inner_cols_1; unsigned_vector m_inner_cols_2; - svector m_result_inner_cols; + bool_vector m_result_inner_cols; scoped_ptr m_inner_join_fun; public: @@ -347,7 +347,7 @@ namespace datalog { class sieve_relation_plugin::transformer_fn : public convenient_relation_transformer_fn { - svector m_result_inner_cols; + bool_vector m_result_inner_cols; scoped_ptr m_inner_fun; public: @@ -383,7 +383,7 @@ namespace datalog { } } - svector result_inner_cols = r.m_inner_cols; + bool_vector result_inner_cols = r.m_inner_cols; project_out_vector_columns(result_inner_cols, col_cnt, removed_cols); relation_signature result_sig; @@ -419,7 +419,7 @@ namespace datalog { unsigned_vector inner_permutation; collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity); - svector result_inner_cols = r.m_inner_cols; + bool_vector result_inner_cols = r.m_inner_cols; permutate_by_cycle(result_inner_cols, cycle_len, permutation_cycle); relation_signature result_sig; diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h index 2d89faa5b..cc2038767 100644 --- a/src/muz/rel/dl_sieve_relation.h +++ b/src/muz/rel/dl_sieve_relation.h @@ -31,7 +31,7 @@ namespace datalog { friend class sieve_relation; public: struct rel_spec { - svector m_inner_cols; + bool_vector m_inner_cols; family_id m_inner_kind; /** @@ -70,9 +70,9 @@ namespace datalog { family_id get_relation_kind(sieve_relation & r, const bool * inner_columns); void extract_inner_columns(const relation_signature & s, relation_plugin & inner, - svector & inner_columns); + bool_vector & inner_columns); void extract_inner_signature(const relation_signature & s, relation_signature & inner_sig); - void collect_inner_signature(const relation_signature & s, const svector & inner_columns, + void collect_inner_signature(const relation_signature & s, const bool_vector & inner_columns, relation_signature & inner_sig); public: static symbol get_name() { return symbol("sieve_relation"); } @@ -89,7 +89,7 @@ namespace datalog { family_id get_relation_kind(const relation_signature & sig, const bool * inner_columns, family_id inner_kind); - family_id get_relation_kind(const relation_signature & sig, const svector & inner_columns, + family_id get_relation_kind(const relation_signature & sig, const bool_vector & inner_columns, family_id inner_kind) { SASSERT(sig.size()==inner_columns.size()); return get_relation_kind(sig, inner_columns.c_ptr(), inner_kind); @@ -108,7 +108,7 @@ namespace datalog { sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns, relation_base * inner_rel); - sieve_relation * mk_from_inner(const relation_signature & s, const svector & inner_columns, + sieve_relation * mk_from_inner(const relation_signature & s, const bool_vector & inner_columns, relation_base * inner_rel) { SASSERT(inner_columns.size()==s.size()); return mk_from_inner(s, inner_columns.c_ptr(), inner_rel); @@ -148,7 +148,7 @@ namespace datalog { friend class sieve_relation_plugin::union_fn; friend class sieve_relation_plugin::filter_fn; - svector m_inner_cols; + bool_vector m_inner_cols; unsigned_vector m_sig2inner; unsigned_vector m_inner2sig; diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index ea292a29e..cf7161275 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1112,7 +1112,7 @@ namespace datalog { SASSERT(joined_col_cnt > 0 || neg.get_signature().size() == 0); m_is_subtract = (joined_col_cnt == t.get_signature().size()); m_is_subtract &= (joined_col_cnt == neg.get_signature().size()); - svector found(joined_col_cnt, false); + bool_vector found(joined_col_cnt, false); for (unsigned i = 0; m_is_subtract && i < joined_col_cnt; ++i) { m_is_subtract = !found[t_cols[i]] && (t_cols[i] == neg_cols[i]); found[t_cols[i]] = true; diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 3fd44c69c..8924c6c53 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -239,9 +239,8 @@ void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res) vars.shrink(j); } - TRACE("spacer", tout << "Skolemizing: "; - for (auto v : vars) tout << " " << mk_pp(v, m) << " "; - tout << "\nfrom " << mk_pp(fml, m) << "\n"; + TRACE("spacer", tout << "Skolemizing: " << vars << "\n"; + tout << "from " << mk_pp(fml, m) << "\n"; ); app_ref_vector pinned(m); @@ -868,7 +867,7 @@ const datalog::rule *pred_transformer::find_rule(model &model) { const datalog::rule *pred_transformer::find_rule(model &model, bool& is_concrete, - vector& reach_pred_used, + bool_vector& reach_pred_used, unsigned& num_reuse_reach) { // find a rule whose tag is true in the model; @@ -1188,14 +1187,13 @@ expr_ref pred_transformer::get_origin_summary (model &mdl, // (skip quantified lemmas cause we can't validate them in the model) // TBD: for quantified lemmas use current instances flatten_and(summary); - for (auto *s : summary) { + + for (auto* s : summary) { if (!is_quantifier(s) && !mdl.is_true(s)) { - TRACE("spacer", tout << "Summary not true in the model: " - << mk_pp(s, m) << "\n";); - // return expr_ref(m); + TRACE("spacer", tout << "Summary not true in the model: " << mk_pp(s, m) << "\n";); } } - + // -- pick an implicant expr_ref_vector lits(m); compute_implicant_literals (mdl, summary, lits); @@ -1209,12 +1207,10 @@ void pred_transformer::add_cover(unsigned level, expr* property, bool bg) // replace bound variables by local constants. expr_ref result(property, m), v(m), c(m); expr_substitution sub(m); - proof_ref pr(m); - pr = m.mk_asserted(m.mk_true()); for (unsigned i = 0; i < sig_size(); ++i) { c = m.mk_const(pm.o2n(sig(i), 0)); v = m.mk_var(i, sig(i)->get_range()); - sub.insert(v, c, pr); + sub.insert(v, c); } scoped_ptr rep = mk_default_expr_replacer(m, false); rep->set_substitution(&sub); @@ -1224,13 +1220,14 @@ void pred_transformer::add_cover(unsigned level, expr* property, bool bg) // add the property. expr_ref_vector lemmas(m); flatten_and(result, lemmas); - for (unsigned i = 0, sz = lemmas.size(); i < sz; ++i) { - add_lemma(lemmas.get(i), level, bg); + for (expr * f: lemmas) { + add_lemma(f, level, bg); } } -void pred_transformer::propagate_to_infinity (unsigned level) -{m_frames.propagate_to_infinity (level);} +void pred_transformer::propagate_to_infinity (unsigned level) { + m_frames.propagate_to_infinity (level); +} // compute a conjunction of all background facts void pred_transformer::get_pred_bg_invs(expr_ref_vector& out) { @@ -1274,7 +1271,9 @@ bool pred_transformer::is_blocked (pob &n, unsigned &uses_level) // XXX quic3: not all lemmas are asserted at the post-condition lbool res = m_solver->check_assumptions (post, _aux, _aux, 0, nullptr, 0); - if (res == l_false) { uses_level = m_solver->uses_level(); } + if (res == l_false) { + uses_level = m_solver->uses_level(); + } return res == l_false; } @@ -1298,10 +1297,9 @@ bool pred_transformer::is_qblocked (pob &n) { // assert all lemmas bool has_quant = false; - for (unsigned i = 0, sz = frame_lemmas.size (); i < sz; ++i) - { - has_quant = has_quant || is_quantifier(frame_lemmas.get(i)); - s->assert_expr(frame_lemmas.get(i)); + for (expr* f : frame_lemmas) { + has_quant |= is_quantifier(f); + s->assert_expr(f); } if (!has_quant) return false; @@ -1335,7 +1333,7 @@ void pred_transformer::mbp(app_ref_vector &vars, expr_ref &fml, model &mdl, lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, model_ref* model, unsigned& uses_level, bool& is_concrete, datalog::rule const*& r, - vector& reach_pred_used, + bool_vector& reach_pred_used, unsigned& num_reuse_reach) { TRACE("spacer", @@ -1388,14 +1386,8 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, } } - TRACE ("spacer", - if (!reach_assumps.empty ()) { - tout << "reach assumptions\n"; - for (unsigned i = 0; i < reach_assumps.size (); i++) { - tout << mk_pp (reach_assumps.get (i), m) << "\n"; - } - } - ); + CTRACE("spacer", !reach_assumps.empty(), + tout << "reach assumptions\n" << reach_assumps << "\n";); // check local reachability; // result is either sat (with some reach assumps) or @@ -1404,24 +1396,15 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, lbool is_sat = m_solver->check_assumptions (post, reach_assumps, m_transition_clause, 1, &bg, 0); - TRACE ("spacer", - if (!reach_assumps.empty ()) { - tout << "reach assumptions used\n"; - for (unsigned i = 0; i < reach_assumps.size (); i++) { - tout << mk_pp (reach_assumps.get (i), m) << "\n"; - } - } - ); + CTRACE("spacer", !reach_assumps.empty(), + tout << "reach assumptions\n" << reach_assumps << "\n";); if (is_sat == l_true || is_sat == l_undef) { if (core) { core->reset(); } if (model && model->get()) { r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach); - TRACE ("spacer", tout << "reachable " - << "is_concrete " << is_concrete << " rused: "; - for (unsigned i = 0, sz = reach_pred_used.size (); i < sz; ++i) - tout << reach_pred_used [i]; - tout << "\n";); + TRACE("spacer", + tout << "reachable " << r << " is_concrete " << is_concrete << " rused: " << reach_pred_used << "\n";); } return is_sat; @@ -2924,8 +2907,6 @@ expr_ref context::get_answer() } } - - expr_ref context::mk_unsat_answer() const { expr_ref_vector refs(m); @@ -2935,7 +2916,6 @@ expr_ref context::mk_unsat_answer() const return ex.to_expr(); } - proof_ref context::get_ground_refutation() const { if (m_last_result != l_true) { IF_VERBOSE(0, verbose_stream() @@ -3272,7 +3252,7 @@ bool context::is_reachable(pob &n) bool is_concrete; const datalog::rule * r = nullptr; // denotes which predecessor's (along r) reach facts are used - vector reach_pred_used; + bool_vector reach_pred_used; unsigned num_reuse_reach = 0; unsigned saved = n.level (); @@ -3382,7 +3362,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) bool is_concrete; const datalog::rule * r = nullptr; // denotes which predecessor's (along r) reach facts are used - vector reach_pred_used; + bool_vector reach_pred_used; unsigned num_reuse_reach = 0; @@ -3694,11 +3674,7 @@ reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r) TRACE ("spacer", tout << "Reach fact, before QE:\n"; tout << mk_pp (res, m) << "\n"; - tout << "Vars:\n"; - for (unsigned i = 0; i < vars.size(); ++i) { - tout << mk_pp(vars.get (i), m) << "\n"; - } - ); + tout << "Vars:\n" << vars << "\n";); { timeit _timer1 (is_trace_enabled("spacer_timeit"), @@ -3711,10 +3687,7 @@ reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r) TRACE ("spacer", tout << "Reach fact, after QE project:\n"; tout << mk_pp (res, m) << "\n"; - tout << "Vars:\n"; - for (unsigned i = 0; i < vars.size(); ++i) { - tout << mk_pp(vars.get (i), m) << "\n"; - } + tout << "Vars:\n" << vars << "\n"; ); SASSERT (vars.empty ()); @@ -3733,7 +3706,7 @@ reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r) */ bool context::create_children(pob& n, datalog::rule const& r, model &mdl, - const vector &reach_pred_used, + const bool_vector &reach_pred_used, pob_ref_buffer &out) { scoped_watch _w_ (m_create_children_watch); @@ -4075,13 +4048,12 @@ inline bool pob_lt_proc::operator() (const pob *pn1, const pob *pn2) const if (p1->get_id() != p2->get_id()) { return p1->get_id() < p2->get_id(); } if (n1.pt().head()->get_id() == n2.pt().head()->get_id()) { - IF_VERBOSE (1, - verbose_stream () - << "dup: " << n1.pt ().head ()->get_name () - << "(" << n1.level () << ", " << n1.depth () << ") " - << p1->get_id () << "\n"; + IF_VERBOSE(1, + verbose_stream() + << "dup: " << n1.pt().head()->get_name() + << "(" << n1.level() << ", " << n1.depth() << ") " + << p1->get_id() << "\n";); //<< " p1: " << mk_pp (const_cast(p1), m) << "\n" - ); } // XXX see comment below on identical nodes diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 62075ebcb..2e4a63474 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -487,7 +487,7 @@ public: bool is_ctp_blocked(lemma *lem); const datalog::rule *find_rule(model &mdl); const datalog::rule *find_rule(model &mev, bool& is_concrete, - vector& reach_pred_used, + bool_vector& reach_pred_used, unsigned& num_reuse_reach); expr* get_transition(datalog::rule const& r) { pt_rule *p; @@ -530,7 +530,7 @@ public: lbool is_reachable(pob& n, expr_ref_vector* core, model_ref *model, unsigned& uses_level, bool& is_concrete, datalog::rule const*& r, - vector& reach_pred_used, + bool_vector& reach_pred_used, unsigned& num_reuse_reach); bool is_invariant(unsigned level, lemma* lem, unsigned& solver_level, @@ -1010,7 +1010,7 @@ class context { lbool expand_pob(pob &n, pob_ref_buffer &out); bool create_children(pob& n, const datalog::rule &r, model &mdl, - const vector& reach_pred_used, + const bool_vector& reach_pred_used, pob_ref_buffer &out); /** diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index b6e0933aa..e6abfdbf1 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -211,8 +211,8 @@ namespace spacer_qe { expr_ref_vector m_terms; vector m_coeffs; vector m_divs; - svector m_strict; - svector m_eq; + bool_vector m_strict; + bool_vector m_eq; scoped_ptr m_var; bool is_linear(rational const& mul, expr* t, rational& c, expr_ref_vector& ts) { diff --git a/src/muz/transforms/dl_mk_backwards.cpp b/src/muz/transforms/dl_mk_backwards.cpp index 986367337..0aa3c4d9a 100644 --- a/src/muz/transforms/dl_mk_backwards.cpp +++ b/src/muz/transforms/dl_mk_backwards.cpp @@ -38,7 +38,7 @@ namespace datalog { rule_ref new_rule(rm); app_ref_vector tail(m); app_ref head(m); - svector neg; + bool_vector neg; app_ref query(m); query = m.mk_fresh_const("Q", m.mk_bool_sort()); result->set_output_predicate(query->get_decl()); diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 06eea7fce..6613b6551 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -64,7 +64,7 @@ namespace datalog { expr_ref_vector revsub(m), conjs(m); rl.get_vars(m, sorts); revsub.resize(sorts.size()); - svector valid(sorts.size(), true); + bool_vector valid(sorts.size(), true); for (unsigned i = 0; i < sub.size(); ++i) { expr* e = sub[i]; sort* s = m.get_sort(e); @@ -116,7 +116,7 @@ namespace datalog { expr_ref_vector conjs1(m), conjs(m); rule_ref res(rm); bool_rewriter bwr(m); - svector is_neg; + bool_vector is_neg; tgt->get_vars(m, sorts1); src.get_vars(m, sorts2); diff --git a/src/muz/transforms/dl_mk_coi_filter.h b/src/muz/transforms/dl_mk_coi_filter.h index 4fe7033bd..d8f22ce18 100644 --- a/src/muz/transforms/dl_mk_coi_filter.h +++ b/src/muz/transforms/dl_mk_coi_filter.h @@ -32,7 +32,7 @@ namespace datalog { ast_manager & m; context & m_context; vector m_new_tail; - svector m_new_tail_neg; + bool_vector m_new_tail_neg; rule_set * bottom_up(rule_set const & source); rule_set * top_down(rule_set const & source); diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index b5dfb84ec..732fd7262 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -106,7 +106,7 @@ namespace datalog { m_current = r; app * new_head = r->get_head(); app_ref_vector new_tail(m); - svector new_is_negated; + bool_vector new_is_negated; unsigned sz = r->get_tail_size(); bool rule_modified = false; for (unsigned i = 0; i < sz; i++) { diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.h b/src/muz/transforms/dl_mk_interp_tail_simplifier.h index 0d4c65d11..b8af0ae4e 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.h +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.h @@ -38,7 +38,7 @@ namespace datalog { unifier m_unif; app_ref m_head; app_ref_vector m_tail; - svector m_neg; + bool_vector m_neg; rule * m_rule; void apply(app * a, app_ref& res); @@ -76,7 +76,7 @@ namespace datalog { app_ref_vector m_tail; expr_ref_vector m_itail_members; expr_ref_vector m_conj; - svector m_tail_neg; + bool_vector m_tail_neg; normalizer_cfg* m_cfg; normalizer_rw* m_rw; diff --git a/src/muz/transforms/dl_mk_karr_invariants.h b/src/muz/transforms/dl_mk_karr_invariants.h index cf021efda..f5c3b57b3 100644 --- a/src/muz/transforms/dl_mk_karr_invariants.h +++ b/src/muz/transforms/dl_mk_karr_invariants.h @@ -34,7 +34,7 @@ namespace datalog { struct matrix { vector > A; vector b; - svector eq; + bool_vector eq; unsigned size() const { return A.size(); } void reset() { A.reset(); b.reset(); eq.reset(); } matrix& operator=(matrix const& other); diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp index 1aea7be45..e0895981f 100644 --- a/src/muz/transforms/dl_mk_loop_counter.cpp +++ b/src/muz/transforms/dl_mk_loop_counter.cpp @@ -73,7 +73,7 @@ namespace datalog { rule_ref new_rule(rm); app_ref_vector tail(m); app_ref head(m); - svector neg; + bool_vector neg; rule_counter& vc = rm.get_counter(); for (unsigned i = 0; i < sz; ++i) { tail.reset(); @@ -129,7 +129,7 @@ namespace datalog { rule_ref new_rule(rm); app_ref_vector tail(m); app_ref head(m); - svector neg; + bool_vector neg; for (unsigned i = 0; i < sz; ++i) { tail.reset(); neg.reset(); diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index 0de37a4ce..5ad637c59 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -187,7 +187,7 @@ namespace datalog { void mk_magic_sets::create_magic_rules(app * head, unsigned tail_cnt, app * const * tail, bool const* negated, rule_set& result) { //TODO: maybe include relevant interpreted predicates from the original rule ptr_vector new_tail; - svector negations; + bool_vector negations; new_tail.push_back(create_magic_literal(head)); new_tail.append(tail_cnt, tail); negations.push_back(false); @@ -231,7 +231,7 @@ namespace datalog { } ptr_vector new_tail; - svector negations; + bool_vector negations; while (new_tail.size()!=processed_tail_len) { bool intentional = false; int curr_index = pop_bound(exten_tails, r, bound_vars); diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp index 0e2e4991a..acdf0bff0 100644 --- a/src/muz/transforms/dl_mk_magic_symbolic.cpp +++ b/src/muz/transforms/dl_mk_magic_symbolic.cpp @@ -77,7 +77,7 @@ namespace datalog { rule_ref new_rule(rm); app_ref_vector tail(m); app_ref head(m); - svector neg; + bool_vector neg; for (unsigned i = 0; i < sz; ++i) { rule & r = *source.get_rule(i); unsigned utsz = r.get_uninterpreted_tail_size(); diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index dafb0ddd5..7eb46a943 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -39,7 +39,7 @@ namespace datalog { func_decl_ref_vector m_new_funcs; vector m_subst; vector m_sorts; - vector > m_bound; + vector m_bound; public: @@ -56,7 +56,7 @@ namespace datalog { void get_units(obj_map& units) override { units.reset(); } - void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector const& bound) { + void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, bool_vector const& bound) { m_old_funcs.push_back(old_p); m_new_funcs.push_back(new_p); m_subst.push_back(sub); @@ -71,7 +71,7 @@ namespace datalog { func_decl* q = m_old_funcs[i].get(); expr_ref_vector const& sub = m_subst[i]; sort_ref_vector const& sorts = m_sorts[i]; - svector const& is_bound = m_bound[i]; + bool_vector const& is_bound = m_bound[i]; func_interp* f = old_model->get_func_interp(p); expr_ref body(m); unsigned arity_q = q->get_arity(); @@ -177,7 +177,7 @@ namespace datalog { func_decl* new_p = nullptr; if (!m_old2new.find(old_p, new_p)) { expr_ref_vector sub(m), vars(m); - svector bound; + bool_vector bound; sort_ref_vector domain(m), sorts(m); expr_ref arg(m); for (unsigned i = 0; i < sz; ++i) { diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 317f13ff8..ce69dad85 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -91,7 +91,7 @@ namespace datalog { void rule_unifier::apply( rule const& r, bool is_tgt, unsigned skipped_index, - app_ref_vector& res, svector& res_neg) { + app_ref_vector& res, bool_vector& res_neg) { unsigned rule_len = r.get_tail_size(); for (unsigned i = 0; i < rule_len; i++) { if (i != skipped_index) { //i can never be UINT_MAX, so we'll never skip if we're not supposed to @@ -107,7 +107,7 @@ namespace datalog { SASSERT(m_ready); app_ref new_head(m); app_ref_vector tail(m); - svector tail_neg; + bool_vector tail_neg; rule_ref simpl_rule(m_rm); apply(tgt.get_head(), true, new_head); apply(tgt, true, tail_index, tail, tail_neg); @@ -647,8 +647,8 @@ namespace datalog { } void mk_rule_inliner::add_rule(rule_set const& source, rule* r, unsigned i) { - svector& can_remove = m_head_visitor.can_remove(); - svector& can_expand = m_head_visitor.can_expand(); + bool_vector& can_remove = m_head_visitor.can_remove(); + bool_vector& can_expand = m_head_visitor.can_expand(); app* head = r->get_head(); func_decl* headd = head->get_decl(); m_head_visitor.add_position(head, i); @@ -705,8 +705,8 @@ namespace datalog { } // set up unification index. - svector& can_remove = m_head_visitor.can_remove(); - svector& can_expand = m_head_visitor.can_expand(); + bool_vector& can_remove = m_head_visitor.can_remove(); + bool_vector& can_expand = m_head_visitor.can_expand(); for (unsigned i = 0; i < sz; ++i) { add_rule(*rules, acc[i].get(), i); @@ -727,7 +727,7 @@ namespace datalog { m_subst.reserve_vars(max_var+1); m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), 2+m_head_index.get_approx_num_regs())); - svector valid; + bool_vector valid; valid.reset(); valid.resize(sz, true); diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h index 9146343fa..8cf738bd8 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.h +++ b/src/muz/transforms/dl_mk_rule_inliner.h @@ -76,7 +76,7 @@ namespace datalog { unless skipped_index is equal to UINT_MAX */ void apply(rule const& r, bool is_tgt, unsigned skipped_index, app_ref_vector& res, - svector& res_neg); + bool_vector& res_neg); }; @@ -85,15 +85,15 @@ namespace datalog { class visitor : public st_visitor { context& m_context; unsigned_vector m_unifiers; - svector m_can_remove, m_can_expand; + bool_vector m_can_remove, m_can_expand; obj_map m_positions; public: visitor(context& c, substitution & s): st_visitor(s), m_context(c) { (void) m_context; } bool operator()(expr* e) override; void reset() { m_unifiers.reset(); } void reset(unsigned sz); - svector& can_remove() { return m_can_remove; } - svector& can_expand() { return m_can_expand; } + bool_vector& can_remove() { return m_can_remove; } + bool_vector& can_expand() { return m_can_expand; } unsigned_vector const& add_position(expr* e, unsigned j); unsigned_vector const& del_position(expr* e, unsigned j); unsigned_vector const& get_unifiers() { return m_unifiers; } diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index 978a22eda..3405769bb 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -127,7 +127,7 @@ namespace datalog { rule_ref new_rule(rm); app_ref_vector tail(m); app_ref head(m); - svector neg; + bool_vector neg; ptr_vector vars; ref smc; if (m_ctx.get_model_converter()) { diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.cpp b/src/muz/transforms/dl_mk_separate_negated_tails.cpp index c50aba827..6da5a7931 100644 --- a/src/muz/transforms/dl_mk_separate_negated_tails.cpp +++ b/src/muz/transforms/dl_mk_separate_negated_tails.cpp @@ -80,7 +80,7 @@ namespace datalog { unsigned tsz = r.get_tail_size(); app_ref_vector tail(m); app_ref p(m); - svector neg; + bool_vector neg; for (unsigned i = 0; i < ptsz; ++i) { tail.push_back(r.get_tail(i)); neg.push_back(false); diff --git a/src/muz/transforms/dl_mk_slice.h b/src/muz/transforms/dl_mk_slice.h index 0bc58c95a..c06d55dff 100644 --- a/src/muz/transforms/dl_mk_slice.h +++ b/src/muz/transforms/dl_mk_slice.h @@ -35,10 +35,10 @@ namespace datalog { context& m_ctx; ast_manager& m; rule_manager& rm; - svector m_input; - svector m_output; + bool_vector m_input; + bool_vector m_output; expr_ref_vector m_solved_vars; - svector m_var_is_sliceable; + bool_vector m_var_is_sliceable; obj_map m_predicates; obj_map m_sliceable; ast_ref_vector m_pinned; diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index c970aedeb..4c5a08eb5 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -125,7 +125,7 @@ namespace datalog { app_ref head(r->get_head(), m); app_ref_vector tail(m); - svector tail_neg; + bool_vector tail_neg; for(unsigned i=0; iget_tail(i); diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index 348c9b5de..809b44c17 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -101,7 +101,7 @@ namespace datalog { app_ref replacing = product_application(apps); ptr_vector new_tail; - svector new_tail_neg; + bool_vector new_tail_neg; unsigned n = r.get_tail_size() - apps.size() + 1; unsigned tail_idx = 0; new_tail.resize(n); @@ -176,7 +176,7 @@ namespace datalog { void mk_synchronize::add_rec_tail(vector< ptr_vector > & recursive_calls, app_ref_vector & new_tail, - svector & new_tail_neg, + bool_vector & new_tail_neg, unsigned & tail_idx) { unsigned max_sz = 0; for (auto &rc : recursive_calls) @@ -200,7 +200,7 @@ namespace datalog { } void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail, - svector & new_tail_neg, + bool_vector & new_tail_neg, unsigned & tail_idx) { for (unsigned i = 0, sz = r.get_positive_tail_size(); i < sz; ++i) { app* tail = r.get_tail(i); @@ -287,7 +287,7 @@ namespace datalog { } app_ref_vector new_tail(m); - svector new_tail_neg; + bool_vector new_tail_neg; new_tail.resize(product_tail_length); new_tail_neg.resize(product_tail_length); unsigned tail_idx = -1; diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 77f45e91f..6850533bb 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -109,9 +109,9 @@ namespace datalog { void add_rec_tail(vector< ptr_vector > & recursive_calls, app_ref_vector & new_tail, - svector & new_tail_neg, unsigned & tail_idx); + bool_vector & new_tail_neg, unsigned & tail_idx); void add_non_rec_tail(rule & r, app_ref_vector & new_tail, - svector & new_tail_neg, + bool_vector & new_tail_neg, unsigned & tail_idx); rule_ref product_rule(rule_ref_vector const & rules); diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp index 7844c3144..6be75fc2c 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.cpp +++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp @@ -205,7 +205,7 @@ namespace datalog { SASSERT(dtail_args.size()==dtail_pred->get_arity()); app_ref dtail(m.mk_app(dtail_pred, dtail_args.size(), dtail_args.c_ptr()), m); - svector tails_negated; + bool_vector tails_negated; app_ref_vector tails(m); unsigned tail_len = r->get_tail_size(); for (unsigned i = 0; i < tail_len; i++) { diff --git a/src/nlsat/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h index cae15f4e1..e1af7b46c 100644 --- a/src/nlsat/nlsat_assignment.h +++ b/src/nlsat/nlsat_assignment.h @@ -30,7 +30,7 @@ namespace nlsat { */ class assignment : public polynomial::var2anum { scoped_anum_vector m_values; - svector m_assigned; + bool_vector m_assigned; public: assignment(anum_manager & _m):m_values(_m) {} virtual ~assignment() {} diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 672b732ee..45ad7e71c 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -258,7 +258,7 @@ namespace nlsat { \brief Add literal p != 0 into m_result. */ ptr_vector m_zero_fs; - svector m_is_even; + bool_vector m_is_even; void add_zero_assumption(polynomial_ref & p) { // If p is of the form p1^n1 * ... * pk^nk, // then only the factors that are zero in the current interpretation needed to be considered. diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index fcd2df74d..748829025 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -114,10 +114,10 @@ namespace nlsat { unsigned_vector m_levels; // bool_var -> level svector m_justifications; vector m_bwatches; // bool_var (that are not attached to atoms) -> clauses where it is maximal - svector m_dead; // mark dead boolean variables + bool_vector m_dead; // mark dead boolean variables id_gen m_bid_gen; - svector m_is_int; // m_is_int[x] is true if variable is integer + bool_vector m_is_int; // m_is_int[x] is true if variable is integer vector m_watches; // var -> clauses where variable is maximal interval_set_vector m_infeasible; // var -> to a set of interval where the variable cannot be assigned to. atom_vector m_var2eq; // var -> to asserted equality @@ -497,7 +497,7 @@ namespace nlsat { SASSERT(m_is_int.size() == m_inv_perm.size()); } - svector m_found_vars; + bool_vector m_found_vars; void vars(literal l, var_vector& vs) { vs.reset(); atom * a = m_atoms[l.var()]; @@ -835,7 +835,7 @@ namespace nlsat { ineq_atom& ia = *to_ineq_atom(a); unsigned sz = ia.size(); ptr_vector ps; - svector is_even; + bool_vector is_even; for (unsigned i = 0; i < sz; ++i) { ps.push_back(ia.p(i)); is_even.push_back(ia.is_even(i)); @@ -2400,7 +2400,7 @@ namespace nlsat { new_inv_perm[ext_x] = p[m_inv_perm[ext_x]]; m_perm.set(new_inv_perm[ext_x], ext_x); } - svector is_int; + bool_vector is_int; is_int.swap(m_is_int); for (var x = 0; x < sz; x++) { m_is_int.setx(p[x], is_int[x], false); @@ -2698,7 +2698,7 @@ namespace nlsat { u_map b2l; scoped_literal_vector lits(m_solver); - svector even; + bool_vector even; unsigned num_atoms = m_atoms.size(); for (unsigned j = 0; j < num_atoms; ++j) { atom* a = m_atoms[j]; diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 796510ce2..291ec26d8 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -78,7 +78,7 @@ namespace opt { svector m_labels; //const expr_ref_vector m_soft; //vector m_weights; - //svector m_assignment; // truth assignment to soft constraints + //bool_vector m_assignment; // truth assignment to soft constraints params_ref m_params; // config public: diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 9eda063e9..8eb238854 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -78,7 +78,7 @@ namespace opt { vector m_objective_values; sref_vector m_models; expr_ref_vector m_objective_terms; - svector m_valid_objectives; + bool_vector m_valid_objectives; bool m_dump_benchmarks; static unsigned m_dump_count; statistics m_stats; diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index 615be9ac9..c433f56d3 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -108,8 +108,8 @@ namespace smt { rational m_penalty; // current penalty of soft constraints rational m_best_penalty; vector m_hard_occ, m_soft_occ; // variable occurrence - svector m_assignment; // current assignment. - svector m_best_assignment; + bool_vector m_assignment; // current assignment. + bool_vector m_best_assignment; expr_ref_vector m_trail; obj_map m_decl2var; // map declarations to Boolean variables. ptr_vector m_var2decl; // reverse map @@ -188,7 +188,7 @@ namespace smt { IF_VERBOSE(1, verbose_stream() << "(pb.sls initial penalty: " << m_best_penalty << ")\n"; verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems() << " penalty: " << m_penalty << ")\n";); - svector assignment(m_assignment); + bool_vector assignment(m_assignment); for (unsigned round = 0; round < 40; ++round) { init_max_flips(); while (m_max_flips > 0) { diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 9d1c2f7e7..0fe618e01 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -415,7 +415,7 @@ namespace qe { expr_ref_vector m_trail; // trail for generated terms expr_ref_vector m_args; ptr_vector m_todo; // stack of formulas to visit - svector m_pols; // stack of polarities + bool_vector m_pols; // stack of polarities bool_rewriter m_rewriter; public: diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 481a72816..31fd64059 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -244,7 +244,7 @@ namespace qe { */ app_ref_vector uflia_mbi::get_arith_vars(expr_ref_vector const& lits) { app_ref_vector avars(m); - svector seen; + bool_vector seen; arith_util a(m); for (expr* e : subterms(lits)) { if ((m.is_eq(e) && a.is_int_real(to_app(e)->get_arg(0))) || a.is_arith_expr(e)) { diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index fb7e32254..50f12fe71 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -295,7 +295,7 @@ namespace sat { bool m_clause_removed; bool m_constraint_removed; literal_vector m_roots; - svector m_root_vars; + bool_vector m_root_vars; unsigned_vector m_weights; svector m_wlits; bool subsumes(card& c1, card& c2, literal_vector& comp); diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp index 5068ef330..beb4131aa 100644 --- a/src/sat/sat_aig_cuts.cpp +++ b/src/sat/sat_aig_cuts.cpp @@ -742,7 +742,7 @@ namespace sat { * Assume only the first definition for a node is used for all cuts. */ void aig_cuts::cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c) { - svector visited(m_aig.size(), false); + bool_vector visited(m_aig.size(), false); for (unsigned u : c) visited[u] = true; unsigned_vector todo; todo.push_back(v); @@ -797,7 +797,7 @@ namespace sat { reslimit lim; solver s; unsigned_vector vars; - svector is_var; + bool_vector is_var; validator(aig_cuts& t):t(t),s(p, lim) { p.set_bool("cut_simplifier", false); diff --git a/src/sat/sat_anf_simplifier.h b/src/sat/sat_anf_simplifier.h index 5169a4438..d30428311 100644 --- a/src/sat/sat_anf_simplifier.h +++ b/src/sat/sat_anf_simplifier.h @@ -66,12 +66,12 @@ namespace sat { solver& s; config m_config; - svector m_relevant; + bool_vector m_relevant; stats m_stats; statistics m_st; unsigned_vector m_eval_cache; unsigned m_eval_ts; - svector m_used_for_evaluation; + bool_vector m_used_for_evaluation; void clauses2anf(pdd_solver& solver); void anf2clauses(pdd_solver& solver); diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 0e4472c93..91bfde2a5 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -170,7 +170,7 @@ namespace sat { CASSERT("asymm_branch", s.check_invariant()); TRACE("asymm_branch_detail", s.display(tout);); report rpt(*this); - svector saved_phase(s.m_phase); + bool_vector saved_phase(s.m_phase); bool change = true; unsigned counter = 0; diff --git a/src/sat/sat_bcd.h b/src/sat/sat_bcd.h index 5363364d3..643a8b8ad 100644 --- a/src/sat/sat_bcd.h +++ b/src/sat/sat_bcd.h @@ -43,8 +43,8 @@ namespace sat { svector m_L, m_R, m_live_clauses, m_new_L; clause_vector m_bin_clauses; svector m_rbits; - svector m_marked; - svector m_removed; // set of clauses removed (not considered in clause set during BCE) + bool_vector m_marked; + bool_vector m_removed; // set of clauses removed (not considered in clause set during BCE) void init(use_list& ul); void register_clause(clause* cls); diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 61b4a6f46..e6c7f40c4 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -30,7 +30,7 @@ namespace sat { random_gen& m_rand; unsigned m_num_vars; vector m_dag; - svector m_roots; + bool_vector m_roots; svector m_left, m_right; literal_vector m_root, m_parent; bool m_learned; diff --git a/src/sat/sat_binspr.h b/src/sat/sat_binspr.h index 7531e592c..743174c1d 100644 --- a/src/sat/sat_binspr.h +++ b/src/sat/sat_binspr.h @@ -43,7 +43,7 @@ namespace sat { unsigned m_stopped_at; vector m_use_list; unsigned m_limit1, m_limit2; - svector m_mark, m_mark2; + bool_vector m_mark, m_mark2; literal_vector m_must_candidates, m_may_candidates; unsigned m_state; diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 3c7e2b0e3..78e0d8cd6 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -78,7 +78,7 @@ namespace sat { pbcoeff(unsigned id, unsigned coeff): m_constraint_id(id), m_coeff(coeff) {} }; - typedef svector bool_vector; + typedef bool_vector bool_vector; typedef svector coeff_vector; @@ -139,7 +139,7 @@ namespace sat { local_search_config m_config; vector m_vars; // variables - svector m_best_phase; // best value in round + bool_vector m_best_phase; // best value in round svector m_units; // unit clauses vector m_constraints; // all constraints literal_vector m_assumptions; // temporary assumptions diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index dfd947f1f..8e3f5bddb 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2082,7 +2082,7 @@ namespace sat { } } - bool lookahead::backtrack(literal_vector& trail, svector & is_decision) { + bool lookahead::backtrack(literal_vector& trail, bool_vector & is_decision) { m_cube_state.m_backtracks++; while (inconsistent()) { if (trail.empty()) return false; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 21246f790..f1bae9667 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -175,7 +175,7 @@ namespace sat { struct cube_state { bool m_first; - svector m_is_decision; + bool_vector m_is_decision; literal_vector m_cube; double m_freevars_threshold; double m_psat_threshold; @@ -540,7 +540,7 @@ namespace sat { void assign(literal l); void propagated(literal l); bool backtrack(literal_vector& trail); - bool backtrack(literal_vector& trail, svector & is_decision); + bool backtrack(literal_vector& trail, bool_vector & is_decision); lbool search(); void init_model(); std::ostream& display_binary(std::ostream& out) const; diff --git a/src/sat/sat_lut_finder.h b/src/sat/sat_lut_finder.h index 1ccd842aa..917cce4cb 100644 --- a/src/sat/sat_lut_finder.h +++ b/src/sat/sat_lut_finder.h @@ -37,7 +37,7 @@ namespace sat { clause_filter(unsigned f, clause* cp): m_filter(f), m_clause(cp) {} }; - typedef svector bool_vector; + typedef bool_vector bool_vector; unsigned m_max_lut_size; vector> m_clause_filters; // index of clauses. uint64_t m_combination; // bit-mask of parities that have been found diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 585f8c312..93a078818 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -90,7 +90,7 @@ namespace sat { private: vector m_entries; // entries accumulated during SAT search unsigned m_exposed_lim; // last entry that was exposed to model converter. - svector m_mark; // literals that are used in asserted clauses. + bool_vector m_mark; // literals that are used in asserted clauses. solver const* m_solver; elim_stackv m_elim_stack; diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index 34116a111..e66ac170a 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -36,7 +36,7 @@ namespace sat { unsigned m_size; unsigned m_tail; unsigned_vector m_heads; - svector m_at_end; + bool_vector m_at_end; void next(unsigned& index); unsigned get_owner(unsigned index) const { return m_vectors[index]; } unsigned get_length(unsigned index) const { return m_vectors[index+1]; } diff --git a/src/sat/sat_prob.h b/src/sat/sat_prob.h index a2fdbb4e1..803d8bae9 100644 --- a/src/sat/sat_prob.h +++ b/src/sat/sat_prob.h @@ -59,7 +59,7 @@ namespace sat { clause_allocator m_alloc; clause_vector m_clause_db; svector m_clauses; - svector m_values, m_best_values; + bool_vector m_values, m_best_values; unsigned m_best_min_unsat; vector m_use_list; unsigned_vector m_flat_use_list; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index ff7c0228a..3b3a18e80 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1002,7 +1002,7 @@ namespace sat { literal_vector m_intersection; // current resolution intersection literal_vector m_tautology; // literals that are used in blocking tautology literal_vector m_new_intersection; - svector m_in_intersection; + bool_vector m_in_intersection; unsigned m_ala_qhead; clause_wrapper m_clause; unsigned m_ala_cost; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index f95b316d4..38c8f97eb 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -118,11 +118,11 @@ namespace sat { vector m_watches; svector m_assignment; svector m_justification; - svector m_decision; - svector m_mark; - svector m_lit_mark; - svector m_eliminated; - svector m_external; + bool_vector m_decision; + bool_vector m_mark; + bool_vector m_lit_mark; + bool_vector m_eliminated; + bool_vector m_external; unsigned_vector m_touched; unsigned m_touch_index; literal_vector m_replay_assign; @@ -137,9 +137,9 @@ namespace sat { int m_action; double m_step_size; // phase - svector m_phase; - svector m_best_phase; - svector m_prev_phase; + bool_vector m_phase; + bool_vector m_best_phase; + bool_vector m_prev_phase; svector m_assigned_since_gc; search_state m_search_state; unsigned m_search_unsat_conflicts; diff --git a/src/sat/sat_unit_walk.h b/src/sat/sat_unit_walk.h index 3ad35a7a3..620805873 100644 --- a/src/sat/sat_unit_walk.h +++ b/src/sat/sat_unit_walk.h @@ -55,7 +55,7 @@ namespace sat { solver& s; local_search m_ls; random_gen m_rand; - svector m_phase; + bool_vector m_phase; svector m_phase_tf; var_priority m_priorities; unsigned m_luby_index; diff --git a/src/sat/sat_xor_finder.h b/src/sat/sat_xor_finder.h index caab9dd7a..b863ecfd9 100644 --- a/src/sat/sat_xor_finder.h +++ b/src/sat/sat_xor_finder.h @@ -37,7 +37,7 @@ namespace sat { clause_filter(unsigned f, clause* cp): m_filter(f), m_clause(cp) {} }; - typedef svector bool_vector; + typedef bool_vector bool_vector; unsigned m_max_xor_size; vector> m_clause_filters; // index of clauses. unsigned m_combination; // bit-mask of parities that have been found diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index c66147756..fb244b6c5 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -1385,7 +1385,7 @@ public: template bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) { svector bfs_todo; - svector bfs_mark; + bool_vector bfs_mark; bfs_mark.resize(m_assignment.size(), false); bfs_todo.push_back(bfs_elem(source, -1, null_edge_id)); diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index 6b937d8f2..9efae9b89 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -334,7 +334,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result) ptr_vector todo; ptr_vector names; - svector is_checked; + bool_vector is_checked; svector parent_ids, self_ids; expr_ref_vector fresh_vars(m); expr_ref_vector trail(m); @@ -484,7 +484,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r ptr_vector todo; ptr_vector names; - svector is_checked; + bool_vector is_checked; svector parent_ids, self_ids; expr_ref_vector fresh_vars(m); expr_ref_vector trail(m); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index cb74d7c66..5d8fde430 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -797,7 +797,7 @@ namespace { code_tree * m_tree; unsigned m_num_choices; bool m_is_tmp_tree; - svector m_mp_already_processed; + bool_vector m_mp_already_processed; obj_map m_matched_exprs; struct pcheck_checked { @@ -3106,10 +3106,10 @@ namespace { // m_is_plbl[f] is true, then when f(c_1, ..., c_n) becomes relevant, // for each c_i. c_i->get_root()->lbls().insert(lbl_hash(f)) - svector m_is_plbl; + bool_vector m_is_plbl; // m_is_clbl[f] is true, then when n=f(c_1, ..., c_n) becomes relevant, // n->get_root()->lbls().insert(lbl_hash(f)) - svector m_is_clbl; // children labels + bool_vector m_is_clbl; // children labels // auxiliary field used to update data-structures... typedef ptr_vector func_decls; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4f1980c58..babb57605 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3989,7 +3989,7 @@ namespace smt { #ifdef Z3DEBUG expr_ref_vector expr_lits(m); - svector expr_signs; + bool_vector expr_signs; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; if (get_assignment(l) != l_false) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index f970925fb..625ed92ac 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1200,7 +1200,7 @@ namespace smt { bool is_relevant_core(expr * n) const { return m_relevancy_propagator->is_relevant(n); } - svector m_relevant_conflict_literals; + bool_vector m_relevant_conflict_literals; void record_relevancy(unsigned n, literal const* lits); void restore_relevancy(unsigned n, literal const* lits); diff --git a/src/smt/smt_quick_checker.h b/src/smt/smt_quick_checker.h index d3af8e2e0..2ba505923 100644 --- a/src/smt/smt_quick_checker.h +++ b/src/smt/smt_quick_checker.h @@ -42,7 +42,7 @@ namespace smt { ast_manager & m_manager; bool m_conservative; unsigned m_num_vars; - svector m_already_found; // mapping from var_idx -> bool + bool_vector m_already_found; // mapping from var_idx -> bool vector m_candidates; // mapping from var_idx -> set of candidates vector m_tmp_candidates; // auxiliary mapping from var_idx -> set of candidates diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index 78b556130..8ba5e754f 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -60,7 +60,7 @@ namespace smt { void get_descendants(node_id start, svector & descendants); virtual void update(edge_id enter_id, edge_id leave_id); - void get_path(node_id start, node_id end, svector & path, svector & against); + void get_path(node_id start, node_id end, svector & path, bool_vector & against); bool in_subtree_t2(node_id child); bool check_well_formed(); diff --git a/src/smt/spanning_tree_base.h b/src/smt/spanning_tree_base.h index 1ad98b79c..fe407f87b 100644 --- a/src/smt/spanning_tree_base.h +++ b/src/smt/spanning_tree_base.h @@ -43,7 +43,7 @@ namespace smt { virtual void get_descendants(node_id start, svector & descendants) = 0; virtual void update(edge_id enter_id, edge_id leave_id) = 0; - virtual void get_path(node_id start, node_id end, svector & path, svector & against) = 0; + virtual void get_path(node_id start, node_id end, svector & path, bool_vector & against) = 0; virtual bool in_subtree_t2(node_id child) = 0; virtual bool check_well_formed() = 0; diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index c49ffcd3c..e299e3028 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -67,7 +67,7 @@ namespace smt { } template - void thread_spanning_tree::get_path(node_id start, node_id end, svector & path, svector & against) { + void thread_spanning_tree::get_path(node_id start, node_id end, svector & path, bool_vector & against) { node_id join = get_common_ancestor(start, end); path.reset(); while (start != join) { @@ -282,7 +282,7 @@ namespace smt { // Check that m_thread traverses each node. // This gets checked using union-find as well. - svector found(m_thread.size(), false); + bool_vector found(m_thread.size(), false); found[root] = true; for (node_id x = m_thread[root]; x != root; x = m_thread[x]) { SASSERT(x != m_thread[x]); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 9b3b7bc57..55a4e9cf3 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1850,7 +1850,7 @@ namespace smt { if (get_context().inconsistent()) return true; // property is only valid if the context is not in a conflict. if (is_root(v) && is_bv(v)) { - svector bits[2]; + bool_vector bits[2]; unsigned num_bits = 0; unsigned bv_sz = get_bv_size(v); bits[0].resize(bv_sz, false); @@ -1878,7 +1878,7 @@ namespace smt { zero_one_bits const & _bits = m_zero_one_bits[v]; SASSERT(_bits.size() == num_bits); - svector already_found; + bool_vector already_found; already_found.resize(bv_sz, false); for (auto & zo : _bits) { SASSERT(find(zo.m_owner) == v); diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h index 941a409fa..e552ab4fc 100644 --- a/src/smt/theory_dense_diff_logic.h +++ b/src/smt/theory_dense_diff_logic.h @@ -124,7 +124,7 @@ namespace smt { atoms m_bv2atoms; edges m_edges; // list of asserted edges matrix m_matrix; - svector m_is_int; + bool_vector m_is_int; vector m_cell_trail; svector m_scopes; bool m_non_diff_logic_exprs; diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 3dee2aa3d..7bc8d4281 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -175,7 +175,7 @@ namespace smt { ptr_vector m_eq_prop_infos; app_ref_vector m_terms; - svector m_signs; + bool_vector m_signs; ptr_vector m_atoms; ptr_vector m_asserted_atoms; // set of asserted atoms @@ -337,7 +337,7 @@ namespace smt { virtual void new_diseq_eh(theory_var v1, theory_var v2, justification& j); - bool decompose_linear(app_ref_vector& args, svector& signs); + bool decompose_linear(app_ref_vector& args, bool_vector& signs); bool is_sign(expr* n, bool& sign); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 37f9cf7f8..73f6981d3 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -399,7 +399,7 @@ void theory_diff_logic::del_atoms(unsigned old_size) { template -bool theory_diff_logic::decompose_linear(app_ref_vector& terms, svector& signs) { +bool theory_diff_logic::decompose_linear(app_ref_vector& terms, bool_vector& signs) { for (unsigned i = 0; i < terms.size(); ++i) { app* n = terms.get(i); bool sign; diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index abd8e4284..7908ca879 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -356,9 +356,9 @@ namespace smt { literal_vector m_antecedents; tracked_uint_set m_active_var_set; expr_ref_vector m_antecedent_exprs; - svector m_antecedent_signs; + bool_vector m_antecedent_signs; expr_ref_vector m_cardinality_exprs; - svector m_cardinality_signs; + bool_vector m_cardinality_signs; void normalize_active_coeffs(); void inc_coeff(literal l, int offset); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index fc6e32774..3534ce610 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -1033,7 +1033,7 @@ namespace smt { unsigned sz = g.get_num_nodes(); svector nodes; num_children.resize(sz, 0); - svector processed(sz, false); + bool_vector processed(sz, false); for (unsigned i = 0; i < sz; ++i) nodes.push_back(i); while (!nodes.empty()) { dl_var v = nodes.back(); diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index 53172b07e..4a293afd3 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -47,7 +47,7 @@ namespace smt { /** \brief return the complement of variables that are currently assigned. */ - void theory_wmaxsat::get_assignment(svector& result) { + void theory_wmaxsat::get_assignment(bool_vector& result) { result.reset(); if (!m_found_optimal) { diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index b2b28ef3d..2f146373c 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -53,12 +53,12 @@ namespace smt { bool m_can_propagate; bool m_normalize; rational m_den; // lcm of denominators for rational weights. - svector m_assigned, m_enabled; + bool_vector m_assigned, m_enabled; stats m_stats; public: theory_wmaxsat(ast_manager& m, generic_model_converter& mc); ~theory_wmaxsat() override; - void get_assignment(svector& result); + void get_assignment(bool_vector& result); expr* assert_weighted(expr* fml, rational const& w); void disable_var(expr* var); bool_var register_var(app* var, bool attach); diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index b838a7127..a2ca66af2 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -202,7 +202,7 @@ class diff_neq_tactic : public tactic { } } - svector m_forbidden; + bool_vector m_forbidden; // make sure m_forbidden.size() > max upper bound void init_forbidden() { diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp index db6270b35..9a29bf905 100644 --- a/src/test/bit_vector.cpp +++ b/src/test/bit_vector.cpp @@ -23,7 +23,7 @@ Revision History: static void tst1() { bit_vector v1; - svector v2; + bool_vector v2; unsigned n = rand()%10000; for (unsigned i = 0; i < n; i++) { int op = rand()%6; diff --git a/src/test/diff_logic.cpp b/src/test/diff_logic.cpp index 0564fbfbe..2ea382e19 100644 --- a/src/test/diff_logic.cpp +++ b/src/test/diff_logic.cpp @@ -86,7 +86,7 @@ static void tst2() { ENSURE(!g.is_feasible()); TRACE("diff_logic", g.display(tout);); struct proc { - svector found; + bool_vector found; proc(): found(7, false) { } diff --git a/src/test/doc.cpp b/src/test/doc.cpp index aaa69fa92..13892a192 100644 --- a/src/test/doc.cpp +++ b/src/test/doc.cpp @@ -300,7 +300,7 @@ class test_doc_cls { d->neg().push_back(t); } fml1 = mk_and(m, fmls.size(), fmls.c_ptr()); - svector to_merge(N, false); + bool_vector to_merge(N, false); bit_vector discard_cols; discard_cols.resize(N, false); unsigned num_bits = 1; diff --git a/src/test/uint_set.cpp b/src/test/uint_set.cpp index bcab106cc..656eaf1b3 100644 --- a/src/test/uint_set.cpp +++ b/src/test/uint_set.cpp @@ -22,7 +22,7 @@ Revision History: static void tst1(unsigned n) { uint_set s1; - svector s2(n, false); + bool_vector s2(n, false); unsigned size = 0; unsigned num_op = rand()%1000; diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index f8500dfa9..0c53ce18f 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -156,7 +156,7 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec = 5) { static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, mpbq_vector const & uppers, unsigned expected_sz, rational const * expected_roots) { ENSURE(expected_sz == roots.size() + lowers.size()); - svector visited; + bool_vector visited; visited.resize(expected_sz, false); for (unsigned i = 0; i < expected_sz; i++) { rational const & r = expected_roots[i]; diff --git a/src/util/min_cut.h b/src/util/min_cut.h index 51a330126..433670786 100644 --- a/src/util/min_cut.h +++ b/src/util/min_cut.h @@ -44,7 +44,7 @@ public: private: - typedef svector bool_vector; + typedef bool_vector bool_vector; struct edge { unsigned node; unsigned weight; edge(unsigned n, unsigned w): node(n), weight(w) {} edge(): node(0), weight(0) {} }; typedef svector edge_vector; diff --git a/src/util/trail.h b/src/util/trail.h index 984281e5a..ada4d263f 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -258,10 +258,10 @@ public: template class set_bitvector_trail : public trail { - svector & m_vector; + bool_vector & m_vector; unsigned m_idx; public: - set_bitvector_trail(svector & v, unsigned idx): + set_bitvector_trail(bool_vector & v, unsigned idx): m_vector(v), m_idx(idx) { SASSERT(m_vector[m_idx] == false); diff --git a/src/util/vector.h b/src/util/vector.h index 4ba5d929b..8a9e824b4 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -31,6 +31,7 @@ using unsigned_vector = old_svector; using char_vector = old_svector; using signed_char_vector = old_svector; using double_vector = old_svector; +using bool_vector = old_svector; template inline std::ostream& operator<<(std::ostream& out, old_svector const& v) {