mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-05 16:03:46 -07:00
commit a1cc21d77b
7 changed files with 44 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast_smt2_pp.cpp
View file

@ -433,12 +433,14 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
} }
#ifdef DATATYPE_V2 #ifdef DATATYPE_V2
if (get_dtutil().is_datatype(s)) { if (get_dtutil().is_datatype(s)) {
ptr_buffer<format> fs;
unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s); unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
for (unsigned i = 0; i < sz; i++) { if (sz > 0) {
fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i))); ptr_buffer<format> fs;
for (unsigned i = 0; i < sz; i++) {
fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i)));
}
return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());
} }
return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());
} }
#endif #endif
return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); return format_ns::mk_string(get_manager(), s->get_name().str().c_str());

12
src/ast/datatype_decl_plugin.cpp
View file

@ -858,22 +858,18 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
ptr_vector<func_decl> const & constructors = *get_datatype_constructors(ty); ptr_vector<func_decl> const & constructors = *get_datatype_constructors(ty);
// step 1) // step 1)
unsigned sz = constructors.size(); unsigned sz = constructors.size();
++m_start; unsigned start = ++m_start;
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = constructors[(j + m_start) % sz]; func_decl * c = constructors[(j + start) % sz];
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;
for (; i < num_args; i++) { for (; i < num_args && !is_datatype(c->get_domain(i)); i++) {};
sort * T_i = c->get_domain(i);
if (is_datatype(T_i))
break;
}
if (i == num_args) if (i == num_args)
return c; return c;
} }
// step 2) // step 2)
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = constructors[(j + m_start) % sz]; func_decl * c = (*constructors)[(j + start) % sz];
TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";); TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;

38
src/ast/datatype_decl_plugin2.cpp
View file

@ -847,6 +847,7 @@ namespace datatype {
r = 0; r = 0;
ptr_vector<sort> forbidden_set; ptr_vector<sort> forbidden_set;
forbidden_set.push_back(ty); forbidden_set.push_back(ty);
TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";);
r = get_non_rec_constructor_core(ty, forbidden_set); r = get_non_rec_constructor_core(ty, forbidden_set);
SASSERT(forbidden_set.back() == ty); SASSERT(forbidden_set.back() == ty);
SASSERT(r); SASSERT(r);
@ -866,46 +867,53 @@ namespace datatype {
// 1) T_i's are not recursive // 1) T_i's are not recursive
// If there is no such constructor, then we select one that // If there is no such constructor, then we select one that
// 2) each type T_i is not recursive or contains a constructor that does not depend on T // 2) each type T_i is not recursive or contains a constructor that does not depend on T
ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty); ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
// step 1)
unsigned sz = constructors.size(); unsigned sz = constructors.size();
++m_start; TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
tout << "forbidden: ";
for (sort* s : forbidden_set) tout << sort_ref(s, m) << " ";
tout << "\n";
tout << "constructors: " << sz << "\n";
for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n";
);
// step 1)
unsigned start = ++m_start;
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = constructors[(j + m_start) % sz]; func_decl * c = constructors[(j + start) % sz];
TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";);
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;
for (; i < num_args; i++) { for (; i < num_args && !is_datatype(c->get_domain(i)); i++);
sort * T_i = c->get_domain(i); if (i == num_args) {
if (is_datatype(T_i)) TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";);
break;
}
if (i == num_args)
return c; return c;
}
} }
// step 2) // step 2)
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = constructors[(j + m_start) % sz]; func_decl * c = constructors[(j + start) % sz];
TRACE("util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";); TRACE("util_bug", tout << "non_rec_constructor c: " << j << " " << func_decl_ref(c, m) << "\n";);
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;
for (; i < num_args; i++) { for (; i < num_args; i++) {
sort * T_i = c->get_domain(i); sort * T_i = c->get_domain(i);
TRACE("util_bug", tout << "c: " << c->get_name() << " i: " << i << " T_i: " << T_i->get_name() << "\n";); TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";);
if (!is_datatype(T_i)) { if (!is_datatype(T_i)) {
TRACE("util_bug", tout << "T_i is not a datatype\n";); TRACE("util_bug", tout << sort_ref(T_i, m) << " is not a datatype\n";);
continue; continue;
} }
if (std::find(forbidden_set.begin(), forbidden_set.end(), T_i) != forbidden_set.end()) { if (std::find(forbidden_set.begin(), forbidden_set.end(), T_i) != forbidden_set.end()) {
TRACE("util_bug", tout << "T_i is in forbidden_set\n";); TRACE("util_bug", tout << sort_ref(T_i, m) << " is in forbidden_set\n";);
break; break;
} }
forbidden_set.push_back(T_i); forbidden_set.push_back(T_i);
func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set); func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set);
SASSERT(forbidden_set.back() == T_i); SASSERT(forbidden_set.back() == T_i);
forbidden_set.pop_back(); forbidden_set.pop_back();
TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";);
if (nested_c == 0) if (nested_c == 0)
break; break;
TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";);
} }
if (i == num_args) if (i == num_args)
return c; return c;

2
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1952,7 +1952,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
} }
} }
if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) { if (szr == 1 && szl >= 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat); return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
} }

2
src/sat/tactic/goal2sat.cpp
View file

@ -248,6 +248,7 @@ struct goal2sat::imp {
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
m_result_stack[i].neg(); m_result_stack[i].neg();
} }
mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
} }
else { else {
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
@ -278,6 +279,7 @@ struct goal2sat::imp {
if (sign) if (sign)
l.neg(); l.neg();
m_result_stack.push_back(l); m_result_stack.push_back(l);
TRACE("goal2sat", tout << m_result_stack << "\n";);
} }
} }

2
src/smt/asserted_formulas.h
View file

@ -220,6 +220,8 @@ class asserted_formulas {
unsigned depth(expr* e) { return m_expr2depth[e]; } unsigned depth(expr* e) { return m_expr2depth[e]; }
bool pull_cheap_ite_trees(); bool pull_cheap_ite_trees();
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
public: public:
asserted_formulas(ast_manager & m, smt_params & p); asserted_formulas(ast_manager & m, smt_params & p);
~asserted_formulas(); ~asserted_formulas();

12
src/smt/smt_conflict_resolution.cpp
View file

@ -348,10 +348,8 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector; literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset(); antecedents.reset();
justification2literals_core(js, antecedents); justification2literals_core(js, antecedents);
literal_vector::iterator it = antecedents.begin(); for (literal l : antecedents)
literal_vector::iterator end = antecedents.end(); process_antecedent(l, num_marks);
for(; it != end; ++it)
process_antecedent(*it, num_marks);
} }
/** /**
@ -517,11 +515,13 @@ namespace smt {
} }
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n"; TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";); tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification); SASSERT(js != null_b_justification);
switch (js.get_kind()) { switch (js.get_kind()) {
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
clause * cls = js.get_clause(); clause * cls = js.get_clause();
TRACE("conflict", m_ctx.display_clause_detail(tout, cls););
if (cls->is_lemma()) if (cls->is_lemma())
cls->inc_clause_activity(); cls->inc_clause_activity();
unsigned num_lits = cls->get_num_literals(); unsigned num_lits = cls->get_num_literals();
@ -566,7 +566,7 @@ namespace smt {
if (m_ctx.is_marked(l.var())) if (m_ctx.is_marked(l.var()))
break; break;
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(), CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l); tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
tout << "\n";); tout << "\n";);
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl || SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
// it may also be an (out-of-order) asserted literal // it may also be an (out-of-order) asserted literal