isolating elim_term_ite inside smt module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/smt/elim_term_ite.cpp

@@ -0,0 +1,160 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    elim_term_ite.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-12.
+
+Revision History:
+
+--*/
+#include"elim_term_ite.h"
+#include"ast_smt2_pp.h"
+
+void elim_term_ite::operator()(expr * n,                        
+                               expr_ref_vector & new_defs,        
+                               proof_ref_vector & new_def_proofs,
+                               expr_ref & r,                     
+                               proof_ref & pr) {
+
+    m_coarse_proofs.reset();
+    m_new_defs       = &new_defs;
+    m_new_def_proofs = &new_def_proofs;
+    reduce_core(n);
+    expr * r2;
+    proof * pr2;
+    get_cached(n, r2, pr2);
+    r = r2;
+    switch (m_manager.proof_mode()) {
+    case PGM_DISABLED:
+        pr = m_manager.mk_undef_proof();
+        break;
+    case PGM_COARSE:
+        remove_duplicates(m_coarse_proofs);
+        pr = n == r2 ? m_manager.mk_oeq_reflexivity(n) : m_manager.mk_apply_defs(n, r, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
+        break;
+    case PGM_FINE:
+        pr = pr2 == 0 ? m_manager.mk_oeq_reflexivity(n) : pr2;
+        break;
+    }
+    m_coarse_proofs.reset();
+}
+
+void elim_term_ite::reduce_core(expr * n) {
+    m_todo.reset();
+    if (!is_cached(n)) {
+        m_todo.push_back(n);
+        while (!m_todo.empty()) {
+            expr * n = m_todo.back();
+            if (is_cached(n)) {
+                m_todo.pop_back();
+            }
+            else if (visit_children(n)) {
+                m_todo.pop_back();
+                reduce1(n);
+            }
+        }
+    }
+}
+
+bool elim_term_ite::visit_children(expr * n) {
+    bool visited = true;
+    unsigned j;
+    switch(n->get_kind()) {
+    case AST_VAR:
+        return true;
+    case AST_APP:
+        j = to_app(n)->get_num_args();
+        while (j > 0) {
+            --j;
+            visit(to_app(n)->get_arg(j), visited);
+        }
+        return visited;
+    case AST_QUANTIFIER: 
+        visit(to_quantifier(n)->get_expr(), visited);
+        return visited;
+    default:
+        UNREACHABLE();
+        return true;
+    }
+}
+
+void elim_term_ite::reduce1(expr * n) {
+    switch (n->get_kind()) {
+    case AST_VAR:
+        cache_result(n, n, 0);
+        break;
+    case AST_APP:
+        reduce1_app(to_app(n));
+        break;
+    case AST_QUANTIFIER:
+        reduce1_quantifier(to_quantifier(n));
+        break;
+    default:
+        UNREACHABLE();
+    }
+}
+
+void elim_term_ite::reduce1_app(app * n) {
+    m_args.reset();
+    
+    func_decl * decl = n->get_decl();
+    proof_ref p1(m_manager);
+    get_args(n, m_args, p1);
+    if (!m_manager.fine_grain_proofs())
+        p1 = 0;
+
+    expr_ref r(m_manager);
+    r = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+    if (m_manager.is_term_ite(r)) {
+        expr_ref   new_def(m_manager);
+        proof_ref  new_def_pr(m_manager);
+        app_ref   new_r(m_manager);
+        proof_ref  new_pr(m_manager);
+        if (m_defined_names.mk_name(r, new_def, new_def_pr, new_r, new_pr)) {
+            CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m_manager) << "\n";);
+            SASSERT(new_def.get() != 0);
+            m_new_defs->push_back(new_def);
+            if (m_manager.fine_grain_proofs()) {
+                m_new_def_proofs->push_back(new_def_pr);
+                new_pr = m_manager.mk_transitivity(p1, new_pr);
+            }
+            else {
+                // [Leo] This looks fishy... why do we add 0 into m_coarse_proofs when fine_grain_proofs are disabled? 
+                new_pr = 0;
+                if (m_manager.proofs_enabled())
+                    m_coarse_proofs.push_back(new_pr);
+            }
+        }
+        else {
+            SASSERT(new_def.get() == 0);
+            if (!m_manager.fine_grain_proofs())
+                new_pr = 0;
+        }
+        cache_result(n, new_r, new_pr);
+    }
+    else {
+        cache_result(n, r, p1);
+    }
+}
+
+void elim_term_ite::reduce1_quantifier(quantifier * q) {
+    expr *  new_body;
+    proof * new_body_pr;
+    get_cached(q->get_expr(), new_body, new_body_pr);
+    
+    quantifier * new_q = m_manager.update_quantifier(q, new_body);
+    proof *      p     = q == new_q ? 0 : m_manager.mk_oeq_quant_intro(q, new_q, new_body_pr);   
+    cache_result(q, new_q, p);
+}
+
+
+

src/smt/elim_term_ite.h

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    elim_term_ite.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-12.
+
+Revision History:
+
+--*/
+#ifndef _ELIM_TERM_ITE_H_
+#define _ELIM_TERM_ITE_H_
+
+#include"simplifier.h"
+#include"defined_names.h"
+
+class elim_term_ite : public simplifier {
+    defined_names &    m_defined_names;
+    proof_ref_vector   m_coarse_proofs;
+    expr_ref_vector *  m_new_defs;
+    proof_ref_vector * m_new_def_proofs;
+    void reduce_core(expr * n);
+    bool visit_children(expr * n);
+    void reduce1(expr * n);
+    void reduce1_app(app * n);
+    void reduce1_quantifier(quantifier * q);
+public:
+    elim_term_ite(ast_manager & m, defined_names & d):simplifier(m), m_defined_names(d), m_coarse_proofs(m) { 
+        m_use_oeq = true; 
+        enable_ac_support(false);
+    }
+    virtual ~elim_term_ite() {}
+    void operator()(expr * n,                          // [IN]
+                    expr_ref_vector & new_defs,        // [OUT] new definitions
+                    proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions 
+                    expr_ref & r,                      // [OUT] resultant expression
+                    proof_ref & pr                     // [OUT] proof for (~ n r)
+                    );
+};
+
+#endif /* _ELIM_TERM_ITE_H_ */
+