From a4cf2726fdd58324e9b65e843c3763aefb9fdaa1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Sep 2017 07:35:37 -0700 Subject: [PATCH 1/3] fix seg-fault from #1244 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/smt/asserted_formulas.h | 3 ++- src/smt/smt_conflict_resolution.cpp | 12 ++++++------ 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 70eddcea1..96a98e472 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1946,7 +1946,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); } diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 093680fd9..1f86edb75 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -96,6 +96,8 @@ class asserted_formulas { void max_bv_sharing(); bool canceled() { return m.canceled(); } + void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); + public: asserted_formulas(ast_manager & m, smt_params & p); ~asserted_formulas(); @@ -118,7 +120,6 @@ public: proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); } proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); } - void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); } simplifier & get_simplifier() { return m_simplifier; } void get_assertions(ptr_vector & result); diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 79a1f0416..cb1465d94 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -348,10 +348,8 @@ namespace smt { literal_vector & antecedents = m_tmp_literal_vector; antecedents.reset(); justification2literals_core(js, antecedents); - literal_vector::iterator it = antecedents.begin(); - literal_vector::iterator end = antecedents.end(); - for(; it != end; ++it) - process_antecedent(*it, num_marks); + for (literal l : antecedents) + process_antecedent(l, num_marks); } /** @@ -517,11 +515,13 @@ namespace smt { } 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); switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); + TRACE("conflict", m_ctx.display_clause_detail(tout, cls);); if (cls->is_lemma()) cls->inc_clause_activity(); unsigned num_lits = cls->get_num_literals(); @@ -566,7 +566,7 @@ namespace smt { if (m_ctx.is_marked(l.var())) break; 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";); SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl || // it may also be an (out-of-order) asserted literal From 394d54fa8be9c89c8c35e647ab092bce2a809000 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Sep 2017 09:54:01 -0700 Subject: [PATCH 2/3] fix missin clause generation for ad-hoc handling of conjunction #1245 --- src/sat/tactic/goal2sat.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 0b6ad2c82..1f9dd91d1 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -248,6 +248,7 @@ struct goal2sat::imp { for (unsigned i = 0; i < num; ++i) { m_result_stack[i].neg(); } + mk_clause(m_result_stack.size(), m_result_stack.c_ptr()); } else { for (unsigned i = 0; i < num; ++i) { @@ -278,6 +279,7 @@ struct goal2sat::imp { if (sign) l.neg(); m_result_stack.push_back(l); + TRACE("goal2sat", tout << m_result_stack << "\n";); } } From a7ef33c136c003d0ba0e44ec4553982e2384656b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Sep 2017 11:31:50 -0700 Subject: [PATCH 3/3] fix bug in generation of non-recursive constructor, modular starting point shifts during recursive calls Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index b4f30767f..f86668ea8 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -857,9 +857,9 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector const * constructors = get_datatype_constructors(ty); // step 1) unsigned sz = constructors->size(); - ++m_start; + unsigned start = ++m_start; 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 i = 0; for (; i < num_args; i++) { @@ -872,7 +872,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vectorget_name() << "\n";); unsigned num_args = c->get_arity(); unsigned i = 0;