mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

re-enable new solve_eqs with bug fixes

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-08 14:17:17 -08:00
parent 9ef78fcfa7
commit 3faca52c40
4 changed files with 9 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/extract_eqs.cpp
View file

@ -192,6 +192,8 @@ namespace euf {
++i; ++i;
if (!is_uninterp_const(arg)) if (!is_uninterp_const(arg))
continue; continue;
if (!a.is_real(arg))
continue;
unsigned j = 0; unsigned j = 0;
bool nonzero = true; bool nonzero = true;
for (expr* arg2 : *to_app(x)) { for (expr* arg2 : *to_app(x)) {

4
src/tactic/core/solve_eqs2_tactic.h
View file

@ -33,7 +33,7 @@ inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = param
return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs"); return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
} }
#if 0 #if 1
inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
return mk_solve_eqs2_tactic(m, p); return mk_solve_eqs2_tactic(m, p);
} }
@ -41,7 +41,7 @@ inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = para
/* /*
ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs2_tactic(m, p)") ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
*/ */

4
src/tactic/core/solve_eqs_tactic.h
View file

@ -24,14 +24,14 @@ class tactic;
tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref());
#if 1 #if 0
inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
return mk_solve_eqs1_tactic(m, p); return mk_solve_eqs1_tactic(m, p);
} }
#endif #endif
/* /*
ADD_TACTIC("solve-eqs1", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)") ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)")
*/ */

6
src/tactic/dependent_expr_state_tactic.h
View file

@ -86,13 +86,13 @@ public:
void operator()(goal_ref const & in, void operator()(goal_ref const & in,
goal_ref_buffer & result) override { goal_ref_buffer & result) override {
if (in->proofs_enabled())
throw tactic_exception("tactic does not support low level proofs");
init(); init();
statistics_report sreport(*this); statistics_report sreport(*this);
tactic_report report(name(), *in); tactic_report report(name(), *in);
m_goal = in.get(); m_goal = in.get();
m_simp->reduce(); if (!in->proofs_enabled())
m_simp->reduce();
m_goal->elim_true();
m_goal->inc_depth(); m_goal->inc_depth();
if (in->models_enabled()) if (in->models_enabled())
in->add(m_model_trail->get_model_converter().get()); in->add(m_model_trail->get_model_converter().get());