From 4d55f836540ac4ea5fa4943fed79809ffcfa6601 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Dec 2020 16:59:05 -0800 Subject: [PATCH] misc --- src/ast/arith_decl_plugin.cpp | 1 + src/ast/arith_decl_plugin.h | 1 + src/sat/smt/arith_axioms.cpp | 8 +++++++ src/sat/smt/arith_internalize.cpp | 21 ++++++++++------ src/sat/smt/arith_solver.cpp | 2 +- src/sat/smt/arith_solver.h | 1 + src/sat/smt/euf_internalize.cpp | 7 ++---- src/sat/smt/euf_proof.cpp | 33 ++++++++++++++++++++++--- src/sat/smt/euf_solver.h | 5 +++- src/sat/smt/sat_smt.h | 7 ------ src/sat/smt/sat_th.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 40 ++++++++++++------------------- src/shell/drat_frontend.cpp | 15 +++++++++++- src/smt/theory_lra.cpp | 2 +- src/smt/user_propagator.cpp | 8 +++++-- src/util/vector.h | 8 +++++++ 16 files changed, 107 insertions(+), 54 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 176b2e61e..2aca15420 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -595,6 +595,7 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("abs", OP_ABS)); if (logic == symbol::null || logic == symbol("ALL")) { op_names.push_back(builtin_name("^", OP_POWER)); + op_names.push_back(builtin_name("^0", OP_POWER0)); op_names.push_back(builtin_name("sin", OP_SIN)); op_names.push_back(builtin_name("cos", OP_COS)); op_names.push_back(builtin_name("tan", OP_TAN)); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 19f17cada..54eeea3e0 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -294,6 +294,7 @@ public: bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); } bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); } bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); } + bool is_power0(expr const * n) const { return is_app_of(n, m_afid, OP_POWER0); } bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); } bool is_int(expr const * n) const { return is_int(get_sort(n)); } diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index c037e56cc..c16caf5a1 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -49,6 +49,14 @@ namespace arith { } } + // t = n^0 + void solver::mk_power0_axioms(app* t, app* n) { + expr_ref p0(a.mk_power0(n, t->get_arg(1)), m); + literal eq = eq_internalize(n, a.mk_numeral(rational(0), a.is_int(n))); + add_clause(~eq, eq_internalize(t, p0)); + add_clause(eq, eq_internalize(t, a.mk_numeral(rational(1), a.is_int(t)))); + } + // is_int(x) <=> to_real(to_int(x)) = x void solver::mk_is_int_axiom(expr* n) { expr* x = nullptr; diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index b9370b1fe..308ca6e98 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -265,7 +265,7 @@ namespace arith { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } - else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) { + else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) { found_unsupported(n); } else { @@ -437,12 +437,18 @@ namespace arith { return v; theory_var w = mk_evar(n); internalize_term(n); - svector vars; - for (unsigned i = 0; i < p; ++i) - vars.push_back(register_theory_var_in_lar_solver(w)); - ensure_nla(); - m_solver->register_existing_terms(); - m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr()); + + if (p == 0) { + mk_power0_axioms(t, n); + } + else { + svector vars; + for (unsigned i = 0; i < p; ++i) + vars.push_back(register_theory_var_in_lar_solver(w)); + ensure_nla(); + m_solver->register_existing_terms(); + m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr()); + } return v; } @@ -566,6 +572,7 @@ namespace arith { for (expr* arg : *to_app(e)) args.push_back(e_internalize(arg)); n = ctx.mk_enode(e, args.size(), args.c_ptr()); + ctx.attach_node(n); } return n; } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 3f11d8388..e3022c9a2 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1127,7 +1127,7 @@ namespace arith { set_evidence(ev.ci(), m_core, m_eqs); DEBUG_CODE( if (is_conflict) { - for (literal c : m_core) VERIFY(s().value(c) == l_false); + for (literal c : m_core) VERIFY(s().value(c) == l_true); for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()); }); for (auto const& eq : m_eqs) diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 507080c75..93465ea2d 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -267,6 +267,7 @@ namespace arith { void mk_rem_axiom(expr* dividend, expr* divisor); void mk_bound_axioms(api_bound& b); void mk_bound_axiom(api_bound& b1, api_bound& b2); + void mk_power0_axioms(app* t, app* n); void flush_bound_axioms(); // bounds diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 0dff8380a..614c56459 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -101,11 +101,8 @@ namespace euf { void solver::attach_node(euf::enode* n) { expr* e = n->get_expr(); - sat::literal lit; - if (!m.is_bool(e)) - drat_log_node(e); - else - lit = attach_lit(literal(si.add_bool_var(e), false), e); + if (m.is_bool(e)) + attach_lit(literal(si.add_bool_var(e), false), e); if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) { auto* e_ext = expr2solver(e); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 4295ca2c8..a848bb791 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -27,9 +27,7 @@ namespace euf { m_drat_initialized = true; } - void solver::drat_log_node(expr* e) { - if (!use_drat()) - return; + void solver::drat_log_expr1(expr* e) { if (is_app(e)) { app* a = to_app(e); drat_log_decl(a->get_decl()); @@ -43,12 +41,41 @@ namespace euf { for (expr* arg : *a) get_drat().def_add_arg(arg->get_id()); get_drat().def_end(); + m_drat_asts.insert(e); + push(insert_obj_trail(m_drat_asts, e)); } else { IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n"); } } + void solver::drat_log_expr(expr* e) { + if (m_drat_asts.contains(e)) + return; + ptr_vector::scoped_stack _sc(m_drat_todo); + m_drat_todo.push_back(e); + while (!m_drat_todo.empty()) { + e = m_drat_todo.back(); + unsigned sz = m_drat_todo.size(); + if (is_app(e)) + for (expr* arg : *to_app(e)) + if (!m_drat_asts.contains(arg)) + m_drat_todo.push_back(arg); + if (m_drat_todo.size() != sz) + continue; + drat_log_expr1(e); + m_drat_todo.pop_back(); + } + } + + void solver::drat_bool_def(sat::bool_var v, expr* e) { + if (!use_drat()) + return; + drat_log_expr(e); + get_drat().bool_def(v, e->get_id()); + } + + void solver::drat_log_decl(func_decl* f) { if (f->get_family_id() != null_family_id) return; diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index d134673ee..fe7ea9620 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -157,6 +157,9 @@ namespace euf { void log_antecedents(std::ostream& out, literal l, literal_vector const& r); void log_antecedents(literal l, literal_vector const& r); void drat_log_decl(func_decl* f); + void drat_log_expr(expr* n); + void drat_log_expr1(expr* n); + ptr_vector m_drat_todo; obj_hashtable m_drat_asts; bool m_drat_initialized{ false }; void init_drat(); @@ -289,6 +292,7 @@ namespace euf { bool use_drat() { return s().get_config().m_drat && (init_drat(), true); } sat::drat& get_drat() { return s().get_drat(); } + void drat_bool_def(sat::bool_var v, expr* n); // decompile bool extract_pb(std::function& card, @@ -310,7 +314,6 @@ namespace euf { void unhandled_function(func_decl* f); th_rewriter& get_rewriter() { return m_rewriter; } bool is_shared(euf::enode* n) const; - void drat_log_node(expr* n); // relevancy bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; } diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index 58e33c06d..862236649 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -28,13 +28,6 @@ namespace sat { eframe(expr* e) : m_e(e), m_idx(0) {} }; - struct scoped_stack { - svector& s; - unsigned sz; - scoped_stack(svector& s):s(s), sz(s.size()) {} - ~scoped_stack() { s.shrink(sz); } - }; - class sat_internalizer { public: virtual ~sat_internalizer() {} diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index e53b7ec13..d866995a4 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -24,7 +24,7 @@ namespace euf { bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) { IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n"); flet _is_learned(m_is_redundant, redundant); - sat::scoped_stack _sc(m_stack); + svector::scoped_stack _sc(m_stack); unsigned sz = m_stack.size(); visit(a); while (m_stack.size() > sz) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index e6d0cedd8..88e343d9f 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -58,7 +58,6 @@ struct goal2sat::imp : public sat::sat_internalizer { }; ast_manager & m; pb_util pb; - sat::cut_simplifier* m_aig; svector m_frame_stack; svector m_result_stack; obj_map m_cache; @@ -83,7 +82,6 @@ struct goal2sat::imp : public sat::sat_internalizer { imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): m(_m), pb(m), - m_aig(nullptr), m_solver(s), m_map(map), m_dep2asm(dep2asm), @@ -92,11 +90,15 @@ struct goal2sat::imp : public sat::sat_internalizer { m_default_external(default_external) { updt_params(p); m_true = sat::null_literal; - m_aig = s.get_cut_simplifier(); } ~imp() override {} + + sat::cut_simplifier* aig() { + return m_solver.get_cut_simplifier(); + } + void updt_params(params_ref const & p) { sat_params sp(p); m_ite_extra = p.get_bool("ite_extra", true); @@ -178,7 +180,6 @@ struct goal2sat::imp : public sat::sat_internalizer { if (m_expr2var_replay && m_expr2var_replay->find(n, v)) return v; v = m_solver.add_var(is_ext); - log_node(n); log_def(v, n); if (top_level_relevant() && !is_bool_op(n)) ensure_euf()->track_relevancy(v); @@ -186,19 +187,8 @@ struct goal2sat::imp : public sat::sat_internalizer { } void log_def(sat::bool_var v, expr* n) { - if (m_drat && m_solver.get_drat_ptr()) - m_solver.get_drat_ptr()->bool_def(v, n->get_id()); - } - - void log_node(expr* n) { - if (m_drat && m_solver.get_drat_ptr()) { - if (is_app(n)) { - for (expr* arg : *to_app(n)) - if (m.is_not(arg)) - log_node(arg); - } - ensure_euf()->drat_log_node(n); - } + if (m_drat && m_euf) + ensure_euf()->drat_bool_def(v, n); } sat::literal mk_true() { @@ -413,15 +403,15 @@ struct goal2sat::imp : public sat::sat_internalizer { m_result_stack.push_back(~l); lits = m_result_stack.end() - num - 1; - if (m_aig) { + if (aig()) { aig_lits.reset(); aig_lits.append(num, lits); } // remark: mk_clause may perform destructive updated to lits. // I have to execute it after the binary mk_clause above. mk_clause(num+1, lits); - if (m_aig) - m_aig->add_or(l, num, aig_lits.c_ptr()); + if (aig()) + aig()->add_or(l, num, aig_lits.c_ptr()); m_solver.set_phase(~l); m_result_stack.shrink(old_sz); @@ -468,13 +458,13 @@ struct goal2sat::imp : public sat::sat_internalizer { } m_result_stack.push_back(l); lits = m_result_stack.end() - num - 1; - if (m_aig) { + if (aig()) { aig_lits.reset(); aig_lits.append(num, lits); } mk_clause(num+1, lits); - if (m_aig) { - m_aig->add_and(l, num, aig_lits.c_ptr()); + if (aig()) { + aig()->add_and(l, num, aig_lits.c_ptr()); } m_solver.set_phase(l); if (sign) @@ -516,7 +506,7 @@ struct goal2sat::imp : public sat::sat_internalizer { mk_clause(~t, ~e, l); mk_clause(t, e, ~l); } - if (m_aig) m_aig->add_ite(l, c, t, e); + if (aig()) aig()->add_ite(l, c, t, e); if (sign) l.neg(); @@ -581,7 +571,7 @@ struct goal2sat::imp : public sat::sat_internalizer { mk_clause(~l, ~l1, l2); mk_clause(l, l1, l2); mk_clause(l, ~l1, ~l2); - if (m_aig) m_aig->add_iff(l, l1, l2); + if (aig()) aig()->add_iff(l, l1, l2); if (sign) l.neg(); m_result_stack.push_back(l); diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index 3271a31e1..6778187d2 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -150,7 +150,7 @@ public: check_assertion_redundant(lits); else if (!st.is_sat() && !st.is_deleted()) check_clause(lits); - m_drat.add(lits, st); + // m_drat.add(lits, st); } /** @@ -201,6 +201,19 @@ public: result = dtu.mk_is(f, args[0]); return; } + if (name == "Real" && sz == 4) { + arith_util au(m); + rational num = sexpr->get_child(2)->get_numeral(); + rational den = sexpr->get_child(3)->get_numeral(); + result = au.mk_numeral(num/den, false); + return; + } + if (name == "Int" && sz == 3) { + arith_util au(m); + rational num = sexpr->get_child(2)->get_numeral(); + result = au.mk_numeral(num, true); + return; + } for (unsigned i = 2; i < sz; ++i) { auto* child = sexpr->get_child(i); if (child->is_numeral() && child->get_numeral().is_unsigned()) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c3d348cf7..fa47f5880 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -384,7 +384,7 @@ class theory_lra::imp { vars.push_back(v); ++index; } - else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) { + else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r.is_pos() && r <= 10) { theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned()); coeffs[vars.size()] = coeffs[index]; vars.push_back(v); diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp index 41e521952..4ce19e12c 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/user_propagator.cpp @@ -121,8 +121,12 @@ void user_propagator::propagate() { m_lits.append(m_id2justification[id]); for (auto const& p : prop.m_eqs) m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); - DEBUG_CODE(for (auto const& p : m_eqs) SASSERT(p.first->get_root() == p.second->get_root());); - + DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); + IF_VERBOSE(5, + for (auto lit : m_lits) + verbose_stream() << lit << ":" << ctx.get_assignment(lit) << " "; + verbose_stream() << "\n";); + if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification( ext_theory_conflict_justification( diff --git a/src/util/vector.h b/src/util/vector.h index ccf7d94fe..ef2ec2cd3 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -596,6 +596,14 @@ public: if (s > size()) resize(s); } + + struct scoped_stack { + vector& s; + unsigned sz; + scoped_stack(vector& s):s(s), sz(s.size()) {} + ~scoped_stack() { s.shrink(sz); } + }; + }; template