mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

use expr-vectors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-21 16:07:10 -08:00
parent 87a1e2b30e
commit edffdf857c
4 changed files with 24 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast_smt2_pp.cpp
View file

@ -1031,10 +1031,8 @@ class smt2_printer {
void reset_expr2alias_stack() {
SASSERT(!m_expr2alias_stack.empty());
ptr_vector<expr2alias>::iterator it = m_expr2alias_stack.begin();
ptr_vector<expr2alias>::iterator end = m_expr2alias_stack.end();
for (; it != end; ++it)
(*it)->reset();
for (expr2alias * e : m_expr2alias_stack)
e->reset();
m_expr2alias = m_expr2alias_stack[0];
}

6
src/model/model_pp.cpp
View file

@ -31,10 +31,8 @@ static void display_uninterp_sorts(std::ostream & out, model_core const & md) {
sort * s = md.get_uninterpreted_sort(i);
out << "(define-sort " << mk_pp(s, m);
ptr_vector<expr> const & univ = md.get_universe(s);
ptr_vector<expr>::const_iterator it = univ.begin();
ptr_vector<expr>::const_iterator end = univ.end();
for (; it != end; ++it) {
out << " " << mk_ismt2_pp(*it, m);
for (expr* e : univ) {
out << " " << mk_ismt2_pp(e, m);
}
out << ")\n";
}

18
src/tactic/generic_model_converter.cpp
View file

@ -19,6 +19,7 @@ Notes:
--*/
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "ast/ast_util.h"
#include "tactic/generic_model_converter.h"
#include "model/model_v2_pp.h"
#include "model/model_evaluator.h"
@ -101,19 +102,32 @@ struct min_app_idx_proc {
void generic_model_converter::operator()(expr_ref& fml) {
min_app_idx_proc min_proc(m_first_idx);
for_each_expr(min_proc, fml);
expr_ref_vector fmls(m);
fmls.push_back(fml);
unsigned min_idx = min_proc.m_min;
for (unsigned i = m_add_entries.size(); i-- > min_idx;) {
entry const& e = m_add_entries[i];
unsigned arity = e.m_f->get_arity();
if (arity == 0) {
fml = m.mk_and(fml, m.mk_eq(m.mk_const(e.m_f), e.m_def));
fmls.push_back(m.mk_eq(m.mk_const(e.m_f), e.m_def));
}
else {
NOT_IMPLEMENTED_YET();
expr_ref_vector args(m);
sort_ref_vector sorts(m);
svector<symbol> names;
for (unsigned i = 0; i < arity; ++i) {
sorts.push_back(e.m_f->get_domain(i));
names.push_back(symbol(i));
args.push_back(m.mk_var(i, sorts.back()));
}
expr_ref lhs(m.mk_app(e.m_f, arity, args.c_ptr()), m);
expr_ref body(m.mk_eq(lhs, e.m_def), m);
fmls.push_back(m.mk_forall(arity, sorts.c_ptr(), names.c_ptr(), body));
}
if (m_first_idx[e.m_f] == i) {
m_first_idx.remove(e.m_f);
}
m_add_entries.pop_back();
}
fml = mk_and(fmls);
}

8
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -304,8 +304,8 @@ private:
void flush_assertions() const {
if (m_assertions.empty()) return;
bound_manager& bm = *m_bounds.back();
for (unsigned i = 0; i < m_assertions.size(); ++i) {
bm(m_assertions[i].get());
for (expr* a : m_assertions) {
bm(a);
}
TRACE("int2bv", bm.display(tout););
expr_safe_replace sub(m);
@ -316,8 +316,8 @@ private:
m_solver->assert_expr(m_assertions);
}
else {
for (unsigned i = 0; i < m_assertions.size(); ++i) {
sub(m_assertions[i].get(), fml1);
for (expr* a : m_assertions) {
sub(a, fml1);
m_rewriter(fml1, fml2, proof);
if (m.canceled()) {
m_rewriter.reset();