mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
maintain ownership of dependency
This commit is contained in:
parent
7b8980f82d
commit
974ea7b68d
|
@ -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<dependent_eq> dep_eq_vector;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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<std::pair<mpq, lpvar>>& coeffs, unsigned ext_i);
|
||||
void register_existing_terms();
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue