fix handing of ite conditions that have to be included in projection, thanks to bug report by Zak

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/qe/qe_arith.cpp

@@ -120,6 +120,7 @@ namespace qe {
             else if (m.is_ite(t, t1, t2, t3)) {                
                 VERIFY(model.eval(t1, val));
                 SASSERT(m.is_true(val) || m.is_false(val));
+                TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
                 if (m.is_true(val)) {
                     is_linear(model, mul, t2, c, ts); 
                 }

src/qe/qe_mbp.cpp

@@ -107,6 +107,7 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
 class mbp::impl {
     ast_manager& m;
     ptr_vector<project_plugin> m_plugins;
+    expr_mark m_visited;
 
     void add_plugin(project_plugin* p) {
         family_id fid = p->get_family_id();
@@ -175,12 +176,48 @@ class mbp::impl {
         return false;
     }
 
+
+    void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) {
+        TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
+        ptr_vector<expr> todo;
+        if (is_app(fml)) {
+            todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
+        }
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (m_visited.is_marked(e)) {
+                continue;
+            }
+            m_visited.mark(e);
+            if (m.is_bool(e)) {
+                expr_ref val(m);
+                VERIFY(model.eval(e, val));
+                TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";);
+                if (m.is_true(val)) {
+                    fmls.push_back(e);
+                }
+                else {
+                    fmls.push_back(mk_not(m, e));
+                }
+            }
+            else if (is_app(e)) {
+                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            }
+            else {
+                TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";);
+            }
+        }
+    }
+
 public:
 
+
     void extract_literals(model& model, expr_ref_vector& fmls) {
         expr_ref val(m);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;
+            SASSERT(m.is_bool(fml));
             if (m.is_not(fml, nfml) && m.is_distinct(nfml)) {
                 fmls[i] = project_plugin::pick_equality(m, model, nfml);
                 --i;
@@ -205,26 +242,28 @@ public:
                     f1 = mk_not(m, f1);
                     f2 = mk_not(m, f2);
                 }
-                project_plugin::push_back(fmls, f1);
+                fmls[i] = f1;
                 project_plugin::push_back(fmls, f2);
-                project_plugin::erase(fmls, i);
+                --i;
             }
             else if (m.is_implies(fml, f1, f2)) {
                 VERIFY (model.eval(f2, val));
                 if (m.is_true(val)) {
-                    project_plugin::push_back(fmls, f2);
+                    fmls[i] = f2;
                 }
                 else {
-                    project_plugin::push_back(fmls, mk_not(m, f1));
+                    fmls[i] = mk_not(m, f1);
                 }
-                project_plugin::erase(fmls, i);
+                --i;
             }
             else if (m.is_ite(fml, f1, f2, f3)) {
                 VERIFY (model.eval(f1, val));                
                 if (m.is_true(val)) {
+                    project_plugin::push_back(fmls, f1);
                     project_plugin::push_back(fmls, f2);
                 }
                 else {
+                    project_plugin::push_back(fmls, mk_not(m, f1));
                     project_plugin::push_back(fmls, f3);
                 }
                 project_plugin::erase(fmls, i);
@@ -269,17 +308,24 @@ public:
             else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
                 VERIFY (model.eval(f1, val));                
                 if (m.is_true(val)) {
+                    project_plugin::push_back(fmls, f1);
                     project_plugin::push_back(fmls, mk_not(m, f2));
                 }
                 else {
+                    project_plugin::push_back(fmls, mk_not(m, f1));
                     project_plugin::push_back(fmls, mk_not(m, f3));
                 }
                 project_plugin::erase(fmls, i);
             }
+            else if (m.is_not(fml, nfml)) {
+                extract_bools(model, fmls, nfml);
+            }
             else {
+                extract_bools(model, fmls, fml);
                 // TBD other Boolean operations.
             }
         }
+        m_visited.reset();
     }
 
     impl(ast_manager& m):m(m) {
@@ -310,6 +356,7 @@ public:
         app_ref var(m);
         th_rewriter rw(m);
         bool progress = true;
+        TRACE("qe", tout << vars << " " << fmls << "\n";);
         while (progress && !vars.empty()) {
             preprocess_solve(model, vars, fmls);
             app_ref_vector new_vars(m);
@@ -345,6 +392,7 @@ public:
             }
             vars.append(new_vars);
         }
+        TRACE("qe", tout << vars << " " << fmls << "\n";);
     }
 };
     

src/qe/qsat.cpp

@@ -31,6 +31,8 @@ Notes:
 #include "expr_abstract.h"
 #include "qe.h"
 #include "label_rewriter.h"
+#include "expr_replacer.h"
+#include "th_rewriter.h"
 
 
 namespace qe {
@@ -674,16 +676,19 @@ namespace qe {
                 is_forall = true;
                 hoist.pull_quantifier(is_forall, fml, vars);
                 m_vars.push_back(vars);
+                filter_vars(vars);
             }
             else {
                 hoist.pull_quantifier(is_forall, fml, vars);
                 m_vars.back().append(vars);
+                filter_vars(vars);
             }
             do {
                 is_forall = !is_forall;
                 vars.reset();
                 hoist.pull_quantifier(is_forall, fml, vars);
                 m_vars.push_back(vars);
+                filter_vars(vars);
             }
             while (!vars.empty());
             SASSERT(m_vars.back().empty()); 
@@ -691,6 +696,101 @@ namespace qe {
             TRACE("qe", tout << fml << "\n";);
         }
 
+        void filter_vars(app_ref_vector const& vars) {
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                m_pred_abs.fmc()->insert(vars[i]->get_decl());
+            }
+        }
+
+#if 0
+        void hoist_ite(expr_ref& fml) {
+            app* ite;
+            scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
+            th_rewriter rewriter(m);
+            while (find_ite(fml, ite)) {
+                expr* cond, *th, *el;
+                VERIFY(m.is_ite(ite, cond, th, el));
+                expr_ref tmp1(fml, m), tmp2(fml, m);
+                replace->apply_substitution(cond, m.mk_true(), tmp1);
+                replace->apply_substitution(cond, m.mk_false(), tmp2);
+                fml = m.mk_ite(cond, tmp1, tmp2);
+                rewriter(fml);
+            }
+        }
+
+        bool find_ite(expr* e, app*& ite) {
+            ptr_vector<expr> todo;
+            todo.push_back(e);
+            ast_mark visited;
+            while(!todo.empty()) {
+                e = todo.back();
+                todo.pop_back();
+                if (visited.is_marked(e)) {
+                    continue;
+                }        
+                visited.mark(e, true);
+                if (m.is_ite(e) && !m.is_bool(e)) {
+                    ite = to_app(e);
+                    return true;
+                }
+                if (is_app(e)) {
+                    app* a = to_app(e);
+                    todo.append(a->get_num_args(), a->get_args());
+                }
+            }
+            return false;
+        }
+
+        // slower
+        void hoist_ite2(expr_ref& fml) {
+            obj_map<expr,expr*> result;
+            expr_ref_vector trail(m);
+            ptr_vector<expr> todo, args;
+            todo.push_back(fml);
+            
+            while (!todo.empty()) {
+                expr* e = todo.back();
+                if (result.contains(e)) {
+                    todo.pop_back();
+                    continue;
+                }
+                if (!is_app(e)) {
+                    todo.pop_back();
+                    result.insert(e, e);
+                    continue;
+                }
+                app* a = to_app(e);
+                expr* r;
+                unsigned sz = a->get_num_args();
+                args.reset();
+                for (unsigned i = 0; i < sz; ++i) {
+                    if (result.find(a->get_arg(i), r)) {
+                        args.push_back(r);
+                    }
+                    else {
+                        todo.push_back(a->get_arg(i));
+                    }
+                }
+                if (sz == args.size()) {
+                    r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
+                    trail.push_back(r);
+                    if (m.is_bool(e) && m.get_basic_family_id() != a->get_family_id()) {
+                        expr_ref fml(r, m);
+                        hoist_ite(fml);
+                        trail.push_back(fml);
+                        r = fml;
+                    }
+                    result.insert(e, r);
+                    todo.pop_back();
+                }                               
+            }
+            fml = result.find(fml);
+        }
+#endif
+
+
+        
+
         void initialize_levels() {
             // initialize levels.
             for (unsigned i = 0; i < m_vars.size(); ++i) {
@@ -941,7 +1041,7 @@ namespace qe {
             expr_ref_vector fmls(m);
             fmls.append(core.size(), core.c_ptr());
             fmls.append(k.size(), k.get_formulas());
-            return check_fmls(fmls);
+            return check_fmls(fmls) || m.canceled();
         }
 
         bool check_fmls(expr_ref_vector const& fmls) {
@@ -953,7 +1053,7 @@ namespace qe {
             lbool is_sat = solver.check();
             CTRACE("qe", is_sat != l_false, 
                    tout << fmls << "\nare not unsat\n";);
-            return (is_sat == l_false);
+            return (is_sat == l_false) || m.canceled();
         }
 
         bool validate_model(expr_ref_vector const& asms) {
@@ -967,7 +1067,7 @@ namespace qe {
         bool validate_model(model& mdl, unsigned sz, expr* const* fmls) {
             expr_ref val(m);
             for (unsigned i = 0; i < sz; ++i) {
-                if (!m_model->eval(fmls[i], val)) {
+                if (!m_model->eval(fmls[i], val) && !m.canceled()) {
                     TRACE("qe", tout << "Formula does not evaluate in model: " << mk_pp(fmls[i], m) << "\n";);
                     return false;
                 } 
@@ -1001,6 +1101,9 @@ namespace qe {
                 TRACE("qe", tout << "Projection is false in model\n";);
                 return false;
             }
+            if (m.canceled()) {
+                return true;
+            }
             for (unsigned i = 0; i < m_avars.size(); ++i) {
                 contains_app cont(m, m_avars[i].get());
                 if (cont(proj)) {
@@ -1029,6 +1132,7 @@ namespace qe {
             return true;
         }
 
+
     public:
         
         qsat(ast_manager& m, params_ref const& p, bool qelim, bool force_elim):
@@ -1070,6 +1174,8 @@ namespace qe {
             expr_ref fml(m);
             mc = 0; pc = 0; core = 0;
             in->get_formulas(fmls);
+
+
             fml = mk_and(m, fmls.size(), fmls.c_ptr());
             
             // for now:
@@ -1091,6 +1197,7 @@ namespace qe {
                 fml = push_not(fml);
             }
             hoist(fml);
+//            hoist_ite(fml); redundant provided theories understand to deal with ite terms.
             m_pred_abs.abstract_atoms(fml, defs);
             fml = m_pred_abs.mk_abstract(fml);
             m_ex.assert_expr(mk_and(defs));

src/tactic/smtlogics/quant_tactics.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include"nlqsat.h"
 #include"ctx_simplify_tactic.h"
 #include"smt_tactic.h"
+#include"elim_term_ite_tactic.h"
 
 static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
     params_ref pull_ite_p;
@@ -112,6 +113,7 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
                                    ));
 #else
     tactic * st = and_then(mk_quant_preprocessor(m),
+                           mk_qe_lite_tactic(m, p),
                            or_else(mk_qsat_tactic(m, p),
                                    and_then(mk_qe_tactic(m), mk_smt_tactic())));
 #endif