re-enable new solve_eqs with bug fixes

Z3Prover · Nov 8, 2022 · 3faca52 · 3faca52
1 parent 9ef78fc
commit 3faca52
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 7 deletions.
diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp
@@ -192,6 +192,8 @@ namespace euf {
                 ++i;
                 if (!is_uninterp_const(arg))
                     continue;
+                if (!a.is_real(arg))
+                    continue;
                 unsigned j = 0;
                 bool nonzero = true;
                 for (expr* arg2 : *to_app(x)) {

diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h
@@ -33,15 +33,15 @@ 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");
 }
 
-#if 0
+#if 1
 inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
     return mk_solve_eqs2_tactic(m, p);
 }
 #endif
 
 
 /*
-  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)")
 */
 
 
diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
@@ -24,14 +24,14 @@ class tactic;
 
 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()) {
     return mk_solve_eqs1_tactic(m, p);
 }
 #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)")
 */
 
 
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
@@ -86,13 +86,13 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
 
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
-        if (in->proofs_enabled())
-            throw tactic_exception("tactic does not support low level proofs");
         init();
         statistics_report sreport(*this);
         tactic_report report(name(), *in);
         m_goal = in.get();
-        m_simp->reduce();
+        if (!in->proofs_enabled())
+            m_simp->reduce();
+        m_goal->elim_true();
         m_goal->inc_depth();
         if (in->models_enabled())
             in->add(m_model_trail->get_model_converter().get());