From 974ea7b68d925e5404e16402c71bc4ca6832b720 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Apr 2024 17:57:14 -0700 Subject: [PATCH] maintain ownership of dependency --- src/ast/simplifiers/extract_eqs.h | 5 +++-- src/ast/sls/bv_sls_eval.cpp | 6 +----- src/math/lp/lar_solver.h | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 10 ++++++++++ 4 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/ast/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h index 724425d6a..b88a3e8a5 100644 --- a/src/ast/simplifiers/extract_eqs.h +++ b/src/ast/simplifiers/extract_eqs.h @@ -31,8 +31,9 @@ namespace euf { expr* orig; // original expression that encoded equation app* var; // isolated variable expr_ref term; // defined term - expr_dependency* dep; - dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : orig(orig), var(var), term(term), dep(d) {} + expr_dependency_ref dep; + dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : + orig(orig), var(var), term(term), dep(d, term.get_manager()) {} }; typedef vector dep_eq_vector; diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 486b33445..d7ce8e703 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -1996,11 +1996,7 @@ namespace bv { out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; if (is_fixed0(e)) out << "f "; - if (bv.is_bv(e)) - out << wval(e); - else if (m.is_bool(e)) - out << (bval0(e) ? "T" : "F"); - out << "\n"; + display_value(out, e) << "\n"; } terms.reset(); return out; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index ec40fcb24..f223b5cc5 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -393,6 +393,7 @@ public: bool external_is_used(unsigned) const; void pop(unsigned k); unsigned num_scopes() const { return m_trail.get_num_scopes(); } + trail_stack& trail() { return m_trail; } bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side); lpvar add_term(const vector>& coeffs, unsigned ext_i); void register_existing_terms(); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 138c6e646..09e7aa047 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -49,8 +49,18 @@ Notes: #include "parsers/smt2/smt2parser.h" #include "sat/sat_params.hpp" +tactic* mk_tactic_for_logic(ast_manager& m, params_ref const& p, symbol const& logic); +class smt_nested_solver_factory : public solver_factory { +public: + solver* operator()(ast_manager& m, params_ref const& p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const& logic) override { + auto t = mk_tactic_for_logic(m, p, logic); + auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); + return s; + } +}; + tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) { if (logic=="QF_UF") return mk_qfuf_tactic(m, p);