diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index 5957fd954..81a0796b8 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -32,7 +32,7 @@ namespace smt { */ class context_solver : public seq::simple_solver { smt_params m_params; // must be declared before m_kernel - smt::kernel m_kernel; + kernel m_kernel; arith_value m_arith_value; static smt_params make_seq_len_params() { @@ -55,6 +55,10 @@ namespace smt { // std::cout << "\t" << mk_pp(m_kernel.get_formula(i), m_kernel.m()) << std::endl; // } // std::cout << std::endl; + // std::cout << "Checking" << std::endl; + // for (unsigned i = 0; i < m_kernel.size(); i++) { + // std::cout << mk_pp(m_kernel.get_formula(i), m_kernel.m()) << std::endl; + // } return m_kernel.check(); } @@ -84,14 +88,20 @@ namespace smt { return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int(); } - virtual expr_ref_vector get_unsat_core() { + lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) override { + // TODO: Not ideal + // Replay with assumptions + // std::cout << "Assuming" << std::endl; + // for (unsigned i = 0; i < assumptions.size(); i++) { + // std::cout << mk_pp(assumptions[i].get(), m_kernel.m()) << std::endl; + // } + lbool r = m_kernel.check(assumptions.size(), assumptions.data()); unsigned cnt = m_kernel.get_unsat_core_size(); - expr_ref_vector core(m_kernel.m()); - core.reserve(cnt); + core.resize(cnt); for (unsigned i = 0; i < cnt; i++) { core[i] = m_kernel.get_unsat_core_expr(i); } - return core; + return r; } void reset() override { diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index a5be04fb8..6d923cf14 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -243,6 +243,12 @@ namespace seq { } void nielsen_node::add_constraint(constraint const &c) { + if (graph().get_manager().is_and(c.fml)) { + // this is important, as the subsolver might decompose for returned unsat cores + for (unsigned i = 0; i < to_app(c.fml)->get_num_args(); ++i) { + add_constraint(constraint(to_app(c.fml)->get_arg(i), c.dep, graph().get_manager())); + } + } m_constraints.push_back(c); if (m_graph.m_literal_if_false) { auto lit = m_graph.m_literal_if_false(c.fml); @@ -386,11 +392,12 @@ namespace seq { // nielsen_graph // ----------------------------------------------- - nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver): + nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver, simple_solver &core_solver): m(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_solver(solver), + m_core_solver(core_solver), m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)), m_len_vars(sg.get_manager()), @@ -495,6 +502,7 @@ namespace seq { m_gpower_vars.reset(); m_dep_mgr.reset(); m_solver.reset(); + m_core_solver.reset(); } // ----------------------------------------------------------------------- @@ -1268,7 +1276,7 @@ namespace seq { vector constraints; generate_length_constraints(constraints); for (auto const& lc : constraints) { - m_solver.assert_expr(lc.m_expr); + m_root->add_constraint(lc.to_constraint()); } } @@ -3916,15 +3924,20 @@ namespace seq { } dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* n) { - auto core = m_solver.get_unsat_core(); - SASSERT(!core.empty()); u_map expr_to_dep; - for (unsigned i = 0; i < n->m_parent_ic_count; i++) { + expr_ref_vector assumptions(m); + assumptions.resize(n->constraints().size()); + for (unsigned i = 0; i < assumptions.size(); i++) { auto& c = n->constraints()[i]; expr_to_dep.insert_if_not_there(c.fml->get_id(), c.dep); + assumptions[i] = c.fml; } + expr_ref_vector core(m); + lbool res = m_core_solver.check_with_assumptions(assumptions, core); + VERIFY(res == l_false); + dep_tracker dep = dep_mgr().mk_empty(); - for (const expr * const e : core) { + for (expr* e : core) { dep = dep_mgr().mk_join(dep, expr_to_dep[e->get_id()]); } return dep; @@ -3996,8 +4009,9 @@ namespace seq { IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: sat_path length=" << m_sat_path.size() << "\n";); m_solver.push(); for (nielsen_edge* e : m_sat_path) { - for (auto const& ic : e->side_constraints()) + for (auto const& ic : e->side_constraints()) { m_solver.assert_expr(ic.fml); + } } if (m_sat_node) { for (auto const& ic : m_sat_node->constraints()) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index ab7eeeacf..c35bbf315 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -273,12 +273,12 @@ namespace seq { class simple_solver { public: virtual ~simple_solver() {} - virtual lbool check() = 0; - virtual void assert_expr(expr* e) = 0; - virtual void push() = 0; - virtual void pop(unsigned num_scopes) = 0; - virtual void get_model(model_ref& mdl) { mdl = nullptr; } - virtual expr_ref_vector get_unsat_core() { throw z3_exception(); } + virtual lbool check() = 0; + virtual void assert_expr(expr* e) = 0; + virtual void push() = 0; + virtual void pop(unsigned num_scopes) = 0; + virtual void get_model(model_ref& mdl) { mdl = nullptr; } + virtual lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) { return l_undef; } // Optional bound queries on arithmetic expressions (non-strict integer bounds). // Default implementation reports "unsupported". virtual bool lower_bound(expr* e, rational& lo) const { return false; } @@ -439,24 +439,6 @@ namespace seq { } }; - // kind of length constraint determines propagation strategy - enum class length_kind { - nonneg, // len(x) >= 0: unconditional axiom - eq, // len(lhs) = len(rhs): conditional on string equality - bound // Parikh bound: conditional on regex membership - }; - - // arithmetic length constraint derived from string equations - struct length_constraint { - expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1) - dep_tracker m_dep; // tracks which input constraints contributed - length_kind m_kind; // determines propagation strategy - - length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {} - length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m): - m_expr(e, m), m_dep(dep), m_kind(kind) {} - }; - // ----------------------------------------------- // integer constraint: equality or inequality over length expressions // mirrors ZIPT's IntEq and IntLe @@ -476,6 +458,29 @@ namespace seq { std::ostream& display(std::ostream& out) const; }; + + // kind of length constraint determines propagation strategy + enum class length_kind { + nonneg, // len(x) >= 0: unconditional axiom + eq, // len(lhs) = len(rhs): conditional on string equality + bound // Parikh bound: conditional on regex membership + }; + + // arithmetic length constraint derived from string equations + struct length_constraint { + expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1) + dep_tracker m_dep; // tracks which input constraints contributed + length_kind m_kind; // determines propagation strategy + + length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {} + length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m): + m_expr(e, m), m_dep(dep), m_kind(kind) {} + + constraint to_constraint() const { + return constraint(m_expr, m_dep, m_expr.get_manager()); + } + }; + // edge in the Nielsen graph connecting two nodes // mirrors ZIPT's NielsenEdge class nielsen_edge { @@ -763,6 +768,7 @@ namespace seq { // and optimistically assumes feasibility. // ----------------------------------------------- simple_solver& m_solver; + simple_solver& m_core_solver; // Constraint.Shared: guards re-assertion of root-level constraints. // Set to true after assert_root_constraints_to_solver() is first called. @@ -820,7 +826,7 @@ namespace seq { public: // Construct with a caller-supplied solver. Ownership is NOT transferred; // the caller is responsible for keeping the solver alive. - nielsen_graph(euf::sgraph& sg, simple_solver& solver); + nielsen_graph(euf::sgraph& sg, simple_solver& solver, simple_solver &core_solver); ~nielsen_graph(); void set_literal_if_false(std::function const& lif) { diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index a5ce0dcb7..d61602f15 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -93,6 +93,10 @@ namespace smt { return m_imp->m_kernel.get_num_asserted_formulas(); } + void kernel::get_formulas(ptr_vector& r) const { + return m_imp->m_kernel.get_asserted_formulas(r); + } + expr* kernel::get_formula(unsigned i) const { return m_imp->m_kernel.get_asserted_formula(i); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index ad7787b4f..56208837b 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -34,7 +34,8 @@ namespace smt { m_egraph(m), m_sgraph(m, m_egraph), m_context_solver(m), - m_nielsen(m_sgraph, m_context_solver), + m_core_solver(m), + m_nielsen(m_sgraph, m_context_solver, m_core_solver), m_axioms(m_th_rewriter), m_regex(m_sgraph), m_model(m, m_seq, m_rewriter, m_sgraph), diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 3517ebbe7..7ba78b48d 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -46,6 +46,7 @@ namespace smt { // m_context_solver must be declared before m_nielsen: its address is passed // to the m_nielsen constructor and must remain stable for the object's lifetime. context_solver m_context_solver; + context_solver m_core_solver; seq::nielsen_graph m_nielsen; seq::axioms m_axioms; seq::seq_regex m_regex; // regex membership pre-processing