Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

lib/ast.h

@@ -832,6 +832,7 @@ inline bool is_app(ast const * n)        { return n->get_kind() == AST_APP; }
 inline bool is_var(ast const * n)        { return n->get_kind() == AST_VAR; }
 inline bool is_quantifier(ast const * n) { return n->get_kind() == AST_QUANTIFIER; }
 inline bool is_forall(ast const * n)     { return is_quantifier(n) && static_cast<quantifier const *>(n)->is_forall(); }
+inline bool is_exists(ast const * n)     { return is_quantifier(n) && static_cast<quantifier const *>(n)->is_exists(); }
 
 // -----------------------------------
 //

lib/dl_mk_coalesce.cpp

@@ -20,8 +20,8 @@ Notes:
 
  Implements proof rule of the form:
 
-    a(x) & q(x) -> p(x)       b(y) & q(y) -> p(y)
+    a(x) & q(x) -> p(x),       b(y) & q(y) -> p(y)
-    ---------------------------------------------
+    ----------------------------------------------
            (a(z) \/ b(z)) & q(z) -> p(z)
 
  

lib/lib.vcxproj

@@ -754,6 +754,7 @@
     <ClCompile Include="qe_bv_plugin.cpp" />
     <ClCompile Include="qe_datatype_plugin.cpp" />
     <ClCompile Include="qe_dl_plugin.cpp" />
+    <ClCompile Include="qe_lite.cpp" />
     <ClCompile Include="qe_sat_tactic.cpp" />
     <ClCompile Include="qe_tactic.cpp" />
     <ClCompile Include="qffpa_tactic.cpp" />
@@ -1161,6 +1162,7 @@
     <ClInclude Include="pull_ite_tree.h" />
     <ClInclude Include="pull_quant.h" />
     <ClInclude Include="push_app_ite.h" />
+    <ClInclude Include="qe_lite.h" />
     <ClInclude Include="qe_sat_tactic.h" />
     <ClInclude Include="qfnra_sign.h" />
     <ClInclude Include="qfuf_strategy.h" />

lib/pdr_context.cpp

@@ -41,6 +41,7 @@ Notes:
 #include "model_smt2_pp.h"
 #include "dl_mk_rule_inliner.h"
 #include "ast_smt2_pp.h"
+#include "qe_lite.h"
 
 namespace pdr {
 
@@ -124,7 +125,7 @@ namespace pdr {
 
     datalog::rule const& pred_transformer::find_rule(model_core const& model) const {
         obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
-        TRACE("pdr",
+        TRACE("pdr_verbose",
               for (; it != end; ++it) {
                   expr* pred = it->m_key;
                   tout << mk_pp(pred, m) << ":\n";
@@ -394,7 +395,6 @@ namespace pdr {
         lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
         if (is_sat == l_true && core) {            
             core->reset();
-            model2cube(*model, *core);
             n.set_model(model);
         }
         return is_sat;
@@ -522,6 +522,7 @@ namespace pdr {
         expr_ref_vector conj(m);
         app_ref_vector& var_reprs = *(alloc(app_ref_vector, m));
         qinst* qi = 0;
+        ptr_vector<app> aux_vars;
                 
         unsigned ut_size = rule.get_uninterpreted_tail_size();
         unsigned t_size  = rule.get_tail_size();   
@@ -534,7 +535,7 @@ namespace pdr {
             init_atom(pts, rule.get_tail(i), var_reprs, conj, i);
         }                  
         for (unsigned i = ut_size; i < t_size; ++i) {
-            ground_free_vars(rule.get_tail(i), var_reprs);
+            ground_free_vars(rule.get_tail(i), var_reprs, aux_vars);
         }
         SASSERT(check_filled(var_reprs));
         expr_ref_vector tail(m);
@@ -585,6 +586,7 @@ namespace pdr {
             m_rule2qinst.insert(&rule, qi);            
         }
         m_rule2inst.insert(&rule,&var_reprs);
+        m_rule2vars.insert(&rule, aux_vars);
     }
 
     bool pred_transformer::check_filled(app_ref_vector const& v) const {
@@ -595,7 +597,7 @@ namespace pdr {
     }
 
     // create constants for free variables in tail.
-    void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars) {
+    void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars) {
         ptr_vector<sort> sorts;
         get_free_vars(e, sorts);
         while (vars.size() < sorts.size()) {
@@ -604,6 +606,7 @@ namespace pdr {
         for (unsigned i = 0; i < sorts.size(); ++i) {
             if (sorts[i] && !vars[i].get()) {
                 vars[i] = m.mk_fresh_const("aux", sorts[i]);
+                aux_vars.push_back(vars[i].get());
             }
         }
     }
@@ -693,34 +696,6 @@ namespace pdr {
         }        
     }
 
-    void pred_transformer::model2cube(app* c, expr* val, expr_ref_vector& res) const {
-        if (m.is_bool(val)) {
-            res.push_back(m.is_true(val)?c:m.mk_not(c));
-        }
-        else {
-            res.push_back(m.mk_eq(c, val));
-        }
-    }
-
-    void pred_transformer::model2cube(const model_core& mdl, func_decl * d, expr_ref_vector& res) const {
-        expr_ref interp(m);
-        get_value_from_model(mdl, d, interp);   
-        app* c = m.mk_const(d);
-        model2cube(c, interp, res);
-    }
-
-    void pred_transformer::model2cube(const model_core & mdl, expr_ref_vector & res) const {
-        unsigned sz = mdl.get_num_constants();
-        for (unsigned i = 0; i < sz; i++) {
-            func_decl * d = mdl.get_constant(i);                        
-            SASSERT(d->get_arity()==0);
-            if (!m_solver.is_aux_symbol(d)) {
-                model2cube(mdl, d, res);
-            }
-        }   
-    }
-
-
     // ----------------
     // model_node
 
@@ -1102,7 +1077,6 @@ namespace pdr {
     }
 
     context::~context() {
-        reset_model_generalizers();
         reset_core_generalizers();
         reset();
     }
@@ -1164,7 +1138,6 @@ namespace pdr {
 
     void context::update_rules(datalog::rule_set& rules) {
         decl2rel rels;
-        init_model_generalizers(rules);
         init_core_generalizers(rules);
         init_rules(rules, rels); 
         decl2rel::iterator it = rels.begin(), end = rels.end();
@@ -1289,25 +1262,6 @@ namespace pdr {
     };
 
 
-    void context::reset_model_generalizers() {
-        std::for_each(m_model_generalizers.begin(), m_model_generalizers.end(), delete_proc<model_generalizer>());
-        m_model_generalizers.reset();
-    }
-
-    void context::init_model_generalizers(datalog::rule_set& rules) {
-        reset_model_generalizers();
-        classifier_proc classify(m, rules);
-        if (classify.is_bool_arith()) {
-            m_model_generalizers.push_back(alloc(bool_model_evaluation_generalizer, *this, m));
-        }
-        else {
-            m_model_generalizers.push_back(alloc(model_evaluation_generalizer, *this, m));
-        }
-        if (m_params.get_bool(":use-precondition-generalizer", false)) {
-            m_model_generalizers.push_back(alloc(model_precond_generalizer, *this));
-        }
-    }
-
     void context::reset_core_generalizers() {
         std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
         m_core_generalizers.reset();
@@ -1553,13 +1507,8 @@ namespace pdr {
                     close_node(n);
                 }
                 else {
-                    TRACE("pdr", tout << "node: " << &n << "\n"; 
+                    TRACE("pdr", tout << "node: " << &n << "\n";); 
-                          expr_ref cb(m.mk_and(cube.size(),cube.c_ptr()), m); 
+                    create_children(n);
-                          tout << mk_pp(cb.get(), m) << "\n";);
-                    for (unsigned i = 0; i < m_model_generalizers.size(); ++i) {
-                        (*m_model_generalizers[i])(n, cube);
-                    }
-                    create_children(n, m_pm.mk_and(cube));
                 }
                 break;
             case l_false: {
@@ -1630,40 +1579,6 @@ namespace pdr {
         }
     }
 
-    // create children states from model cube.
-    void context::create_children(model_node& n, expr* model) {        
-        expr_ref_vector literals(m), sub_lits(m);
-        expr_ref o_cube(m), n_cube(m);
-        datalog::flatten_and(model, literals);
-        ptr_vector<func_decl> preds;
-        unsigned level = n.level();
-        SASSERT(level > 0);
-        n.pt().find_predecessors(n.model(), preds);
-        n.pt().remove_predecessors(literals);
-        TRACE("pdr", 
-              model_v2_pp(tout, n.model());
-              tout << "Model cube\n";
-              tout << mk_pp(model, m) << "\n";
-              tout << "Predecessors\n";
-              for (unsigned i = 0; i < preds.size(); ++i) {
-                  tout << preds[i]->get_name() << "\n";
-              }
-             );
-        for (unsigned i = 0; i < preds.size(); ++i) {            
-            pred_transformer& pt = *m_rels.find(preds[i]);
-            SASSERT(pt.head() == preds[i]);
-            assign_ref_vector(sub_lits, literals);
-            m_pm.filter_o_atoms(sub_lits, i);            
-            o_cube = m_pm.mk_and(sub_lits);
-            m_pm.formula_o2n(o_cube, n_cube, i);
-            model_node* child = alloc(model_node, &n, n_cube, pt, level-1);
-            ++m_stats.m_num_nodes;
-            m_search.add_leaf(*child);            
-        }
-        check_pre_closed(n);
-        
-        TRACE("pdr", m_search.display(tout););
-    }
 
     /**
        \brief create children states from model cube.
@@ -1713,35 +1628,126 @@ namespace pdr {
        - Create sub-goals for L0 and L1.
 
     */
-    void context::create_children2(model_node& n, expr* psi) {        
+    void context::create_children(model_node& n) {        
         SASSERT(n.level() > 0);
  
         pred_transformer& pt = n.pt();
-        model_core const& M = n.model();
+        model_ref M = n.model_ptr();
-        datalog::rule const& r = pt.find_rule(M);
+        datalog::rule const& r = pt.find_rule(*M);
         expr* T   = pt.get_transition(r);
         expr* phi = n.state();
 
-        ternary_model_evaluator tmev(m);
+        IF_VERBOSE(2, verbose_stream() << "Model:\n";
-        expr_ref_vector mdl(m);
+                   model_smt2_pp(verbose_stream(), m, *M, 0);
-        ptr_vector<expr> forms;
+                   verbose_stream() << "\n";
+                   verbose_stream() << "Transition:\n" << mk_pp(T, m) << "\n";
+                   verbose_stream() << "Phi:\n" << mk_pp(phi, m) << "\n";);
+                      
+        model_evaluator mev(m);
+        expr_ref_vector mdl(m), forms(m), Phi(m);
         forms.push_back(T);
         forms.push_back(phi);
-        datalog::flatten_and(psi, mdl);
+        datalog::flatten_and(forms);        
-        expr_ref_vector Phi = tmev.minimize_literals(forms, mdl);
+        ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
-
+        if (m_params.get_bool(":use-model-generalizer", false)) {
+            Phi.append(mev.minimize_model(forms1, M));
+        }
+        else {
+            Phi.append(mev.minimize_literals(forms1, M));
+        }
         ptr_vector<func_decl> preds;
         pt.find_predecessors(r, preds);
         pt.remove_predecessors(Phi);
 
-        expr_ref_vector vars(m);
+        app_ref_vector vars(m);
         unsigned sig_size = pt.head()->get_arity();
         for (unsigned i = 0; i < sig_size; ++i) {
             vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0)));
         }
-        // TBD: reduce_vars(vars, Phi);
+        ptr_vector<app> aux_vars;
+        pt.get_aux_vars(r, aux_vars);
+        vars.append(aux_vars.size(), aux_vars.c_ptr());
+
+        qe_lite qe(m);
+        expr_ref phi1 = m_pm.mk_and(Phi);
+        qe(vars, phi1);
+
+        IF_VERBOSE(2, 
+                   verbose_stream() << "Vars:\n";
+                   for (unsigned i = 0; i < vars.size(); ++i) {
+                       verbose_stream() << mk_pp(vars[i].get(), m) << "\n";
+                   }
+                   verbose_stream() << "Literals\n";
+                   verbose_stream() << mk_pp(m_pm.mk_and(Phi), m) << "\n";
+                   verbose_stream() << "Reduced\n" << mk_pp(phi1, m) << "\n";);
+        
+        if (!vars.empty()) {
+            // also fresh names for auxiliary variables in body?
+            expr_substitution sub(m);
+            expr_ref tmp(m);
+            proof_ref pr(m);
+            pr = m.mk_asserted(m.mk_true());
+
+            for (unsigned i = 0; i < vars.size(); ++i) {                
+                M->eval(vars[i]->get_decl(), tmp);                
+                sub.insert(vars[i].get(), tmp, pr);
+            }
+            scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+            rep->set_substitution(&sub);
+            (*rep)(phi1);
+            IF_VERBOSE(2, verbose_stream() << "Projected:\n" << mk_pp(phi1, m) << "\n";);
+        }
+        Phi.reset();
+        datalog::flatten_and(phi1, Phi);
+        unsigned_vector indices;
+        vector<expr_ref_vector> child_states;
+        child_states.resize(preds.size(), expr_ref_vector(m));
+        for (unsigned i = 0; i < Phi.size(); ++i) {            
+            m_pm.collect_indices(Phi[i].get(), indices);    
+            if (indices.size() == 0) {
+                IF_VERBOSE(2, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";);
+            }
+            else if (indices.size() == 1) {
+                child_states[indices.back()].push_back(Phi[i].get());
+            }
+            else {
+                expr_substitution sub(m);
+                expr_ref tmp(m);
+                proof_ref pr(m);
+                pr = m.mk_asserted(m.mk_true());
+                vector<ptr_vector<app> > vars;
+                m_pm.collect_variables(Phi[i].get(), vars);
+                SASSERT(vars.size() == indices.back()+1);
+                for (unsigned j = 1; j < indices.size(); ++j) {
+                    ptr_vector<app> const& vs = vars[indices[j]];
+                    for (unsigned k = 0; k < vs.size(); ++k) {
+                        M->eval(vs[k]->get_decl(), tmp);
+                        sub.insert(vs[k], tmp, pr);
+                        child_states[indices[j]].push_back(m.mk_eq(vs[k], tmp));
+                    }
+                }
+                tmp = Phi[i].get();
+                scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+                rep->set_substitution(&sub);
+                (*rep)(tmp);
+                child_states[indices[0]].push_back(tmp);
+            }
+        }
+        
+        expr_ref n_cube(m);
+        for (unsigned i = 0; i < preds.size(); ++i) {            
+            pred_transformer& pt = *m_rels.find(preds[i]);
+            SASSERT(pt.head() == preds[i]);           
+            expr_ref o_cube = m_pm.mk_and(child_states[i]);            
+            m_pm.formula_o2n(o_cube, n_cube, i);
+            model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1);
+            ++m_stats.m_num_nodes;
+            m_search.add_leaf(*child); 
+            IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+        }
+        check_pre_closed(n);
+
 
-        // TBD ...
         TRACE("pdr", m_search.display(tout););
     }
 
@@ -1754,9 +1760,6 @@ namespace pdr {
         st.update("PDR max depth", m_stats.m_max_depth);
         m_pm.collect_statistics(st);
 
-        for (unsigned i = 0; i < m_model_generalizers.size(); ++i) {
-            m_model_generalizers[i]->collect_statistics(st);
-        }
         for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {
             m_core_generalizers[i]->collect_statistics(st);
         }

lib/pdr_context.h

@@ -60,6 +60,7 @@ namespace pdr {
         };
 
         typedef obj_map<datalog::rule const, expr*> rule2expr;
+        typedef obj_map<datalog::rule const, ptr_vector<app> > rule2apps;
 
         manager&                     pm;        // pdr-manager
         ast_manager&                 m;         // manager
@@ -77,6 +78,7 @@ namespace pdr {
         qinst_map                    m_rule2qinst;      // map tag to quantifier instantiation.
         rule2inst                    m_rule2inst;       // map rules to instantiations of indices
         rule2expr                    m_rule2transition; // map rules to transition 
+        rule2apps                    m_rule2vars;       // map rule to auxiliary variables
         expr_ref                     m_transition;      // transition relation.
         expr_ref                     m_initial_state;   // initial state.
         reachable_cache              m_reachable; 
@@ -94,10 +96,7 @@ namespace pdr {
         void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init,                                      
                        ptr_vector<datalog::rule const>& rules, expr_ref_vector& transition);
         void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx);
-        void ground_free_vars(expr* e, app_ref_vector& vars);
+        void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
-
-        void model2cube(const model_core& md, func_decl * d, expr_ref_vector& res) const;
-        void model2cube(app* c, expr* val, expr_ref_vector& res) const;
 
         void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
 
@@ -137,6 +136,7 @@ namespace pdr {
         void find_predecessors(model_core const& model, ptr_vector<func_decl>& preds) const;
         datalog::rule const& find_rule(model_core const& model) const;
         expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); }
+        void  get_aux_vars(datalog::rule const& r, ptr_vector<app>& vs) { m_rule2vars.find(&r, vs); }
 
         bool propagate_to_next_level(unsigned level);
         void add_property(expr * lemma, unsigned lvl);  // add property 'p' to state at level.
@@ -154,8 +154,6 @@ namespace pdr {
         manager& get_pdr_manager() const { return pm; }
         ast_manager& get_manager() const { return m; }
 
-        void model2cube(const model_core & mdl, expr_ref_vector & res) const;
-
         void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
 
         void close(expr* e);
@@ -194,7 +192,8 @@ namespace pdr {
         ptr_vector<model_node> const& children() { return m_children; }
         pred_transformer& pt() const { return m_pt; }
         model_node* parent() const { return m_parent; }
-        model_core const& model() const { return *m_model; }
+        model* model_ptr() const { return m_model.get(); }
+        model const& model() const { return *m_model; }
         unsigned index() const;
 
         bool is_closed() const { return m_closed; }
@@ -262,18 +261,6 @@ namespace pdr {
 
     class context;
 
-    // 'state' is satisifiable with predecessor 'cube'. 
-    // Generalize predecessor still forcing satisfiability.
-    class model_generalizer {
-    protected:
-        context& m_ctx;
-    public:
-        model_generalizer(context& ctx): m_ctx(ctx) {}
-        virtual ~model_generalizer() {}
-        virtual void operator()(model_node& n, expr_ref_vector& cube) = 0;
-        virtual void collect_statistics(statistics& st) {}
-    };
-
     // 'state' is unsatisfiable at 'level' with 'core'. 
     // Minimize or weaken core.
     class core_generalizer {
@@ -301,7 +288,6 @@ namespace pdr {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
-
         
         front_end_params&    m_fparams;
         params_ref const&    m_params;
@@ -315,7 +301,6 @@ namespace pdr {
         model_search         m_search;
         lbool                m_last_result;
         unsigned             m_inductive_lvl;
-        ptr_vector<model_generalizer> m_model_generalizers;
         ptr_vector<core_generalizer>  m_core_generalizers;
         stats                m_stats;
         volatile bool        m_cancel;
@@ -332,8 +317,7 @@ namespace pdr {
         void check_pre_closed(model_node& n);
         void expand_node(model_node& n);
         lbool expand_state(model_node& n, expr_ref_vector& cube);
-        void create_children(model_node& n, expr* cube);
+        void create_children(model_node& n);
-        void create_children2(model_node& n, expr* cube);
         expr_ref mk_sat_answer() const;
         expr_ref mk_unsat_answer() const;
         
@@ -343,7 +327,6 @@ namespace pdr {
 
         // Initialization
         class classifier_proc;
-        void init_model_generalizers(datalog::rule_set& rules); 
         void init_core_generalizers(datalog::rule_set& rules);
 
         bool check_invariant(unsigned lvl);
@@ -355,7 +338,6 @@ namespace pdr {
 
         void simplify_formulas();
 
-        void reset_model_generalizers();
         void reset_core_generalizers();
 
     public:       

lib/pdr_dl_interface.cpp

@@ -202,7 +202,7 @@ void dl_interface::collect_params(param_descrs& p) {
     p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); 
     p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
     p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
-    PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions"););
+    p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
     PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););
     PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"););
     PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"););

lib/pdr_generalizers.cpp

@@ -28,66 +28,6 @@ Revision History:
 
 namespace pdr {
 
-    static void solve_for_next_vars(expr_ref& F, model_node& n, expr_substitution& sub) {
-        ast_manager& m = F.get_manager();
-        manager& pm = n.pt().get_pdr_manager();
-        const model_core & mdl = n.model();
-        unsigned sz = mdl.get_num_constants();
-        expr_ref_vector refs(m);
-
-        for (unsigned i = 0; i < sz; i++) {
-             func_decl * d = mdl.get_constant(i);    
-             expr_ref interp(m);
-             ptr_vector<app> cs;
-             if (m.is_bool(d->get_range())) {
-                get_value_from_model(mdl, d, interp);  
-                app* c = m.mk_const(d);
-                refs.push_back(c);
-                refs.push_back(interp);
-                sub.insert(c, interp);
-             }
-        }
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-        rep->set_substitution(&sub);
-        (*rep)(F);
-        th_rewriter rw(m);
-        rw(F);
-        ptr_vector<expr> todo;
-        todo.push_back(F);
-        expr* e1, *e2;
-        while (!todo.empty()) {
-            expr* e = todo.back();
-            todo.pop_back();
-            if (m.is_and(e)) {
-                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
-            }
-            else if ((m.is_eq(e, e1, e2) && pm.is_n(e1) && pm.is_o_formula(e2)) ||
-                     (m.is_eq(e, e2, e1) && pm.is_n(e1) && pm.is_o_formula(e2))) {
-                sub.insert(e1, e2);
-                TRACE("pdr", tout << mk_pp(e1, m) << " |-> " << mk_pp(e2, m) << "\n";);
-            }
-        }
-    }
-
-    //
-    // eliminate conjuncts from cube as long as state is satisfied.
-    // 
-    void model_evaluation_generalizer::operator()(model_node& n, expr_ref_vector& cube) {
-        ptr_vector<expr> forms;
-        forms.push_back(n.state());
-        forms.push_back(n.pt().transition());
-        m_model_evaluator.minimize_model(forms, cube);
-    }
-
-    //
-    // eliminate conjuncts from cube as long as state is satisfied.
-    // 
-    void bool_model_evaluation_generalizer::operator()(model_node& n, expr_ref_vector& cube) {
-        ptr_vector<expr> forms;
-        forms.push_back(n.state());
-        forms.push_back(n.pt().transition());
-        m_model_evaluator.minimize_model(forms, cube);
-    }
 
     //
     // main propositional induction generalizer.
@@ -203,31 +143,6 @@ namespace pdr {
         m_farkas_learner.collect_statistics(st);
     }
 
-    void model_precond_generalizer::operator()(model_node& n, expr_ref_vector& cube) {
-        ast_manager& m  = n.pt().get_manager();
-        manager& pm = n.pt().get_pdr_manager();
-        expr_ref A(m), state(m);
-        expr_ref_vector states(m);
-        A = n.pt().get_formulas(n.level(), true);   
-
-        // extract substitution for next-state variables.
-        expr_substitution sub(m);        
-        solve_for_next_vars(A, n, sub);
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-        rep->set_substitution(&sub);
-        A = m.mk_and(A, n.state());
-        (*rep)(A);                
-
-        datalog::flatten_and(A, states);
-
-        for (unsigned i = 0; i < states.size(); ++i) {
-            expr* s = states[i].get();
-            if (pm.is_o_formula(s) && pm.is_homogenous_formula(s)) {
-                cube.push_back(s);
-            }
-        }
-        TRACE("pdr", for (unsigned i = 0; i < cube.size(); ++i) tout << mk_pp(cube[i].get(), m) << "\n";);
-    }
 
     /**
               < F, phi, i + 1 >

lib/pdr_generalizers.h

@@ -25,14 +25,6 @@ Revision History:
 
 namespace pdr {
 
-    class bool_model_evaluation_generalizer : public model_generalizer {        
-        ternary_model_evaluator m_model_evaluator;
-    public:
-        bool_model_evaluation_generalizer(context& ctx, ast_manager& m) : model_generalizer(ctx), m_model_evaluator(m) {}
-        virtual ~bool_model_evaluation_generalizer() {}
-        virtual void operator()(model_node& n, expr_ref_vector& cube);
-    };
-
     class core_bool_inductive_generalizer : public core_generalizer {
         unsigned m_failure_limit;
     public:
@@ -50,21 +42,6 @@ namespace pdr {
         virtual void collect_statistics(statistics& st) const;
     };
 
-    class model_precond_generalizer : public model_generalizer {
-    public:
-        model_precond_generalizer(context& ctx): model_generalizer(ctx) {}
-        virtual ~model_precond_generalizer() {}
-        virtual void operator()(model_node& n, expr_ref_vector& cube);
-    };
-
-    class model_evaluation_generalizer : public model_generalizer {        
-        th_rewriter_model_evaluator m_model_evaluator;
-    public:        
-        model_evaluation_generalizer(context& ctx, ast_manager& m) : model_generalizer(ctx), m_model_evaluator(m) {}
-        virtual ~model_evaluation_generalizer() {}
-        virtual void operator()(model_node& n, expr_ref_vector& cube);
-    };
-
     class core_multi_generalizer : public core_generalizer {
         core_bool_inductive_generalizer m_gen;
     public:

lib/pdr_manager.h

@@ -223,6 +223,20 @@ namespace pdr {
         bool is_homogenous_formula(expr * e) const {
             return m_mux.is_homogenous_formula(e);
         }
+
+        /**
+            Collect indices used in expression.
+        */
+        void collect_indices(expr* e, unsigned_vector& indices) const {
+            m_mux.collect_indices(e, indices);
+        }
+
+        /**
+            Collect used variables of each index.
+        */
+        void collect_variables(expr* e, vector<ptr_vector<app> >& vars) const {
+            m_mux.collect_variables(e, vars);
+        }
         
         /**
            Return true iff both s1 and s2 are either "n" or "o" of the same index.
@@ -275,8 +289,6 @@ namespace pdr {
         bool try_get_state_and_value_from_atom(expr * atom, app *& state, app_ref& value);
         bool try_get_state_decl_from_atom(expr * atom, func_decl *& state);
         
-        void get_state_cube_from_model(const model_core & mdl, expr_ref_vector & cube) const
-        {  return m_mux.get_muxed_cube_from_model(mdl, cube); }
         
         std::string pp_model(const model_core & mdl) const
             {  return m_mux.pp_model(mdl); }

lib/pdr_sym_mux.cpp

@@ -228,6 +228,76 @@ bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const
     return true;
 }
 
+class sym_mux::index_collector {
+    sym_mux const& m_parent;
+    svector<bool> m_indices;
+public:
+    index_collector(sym_mux const& s): 
+      m_parent(s) {}
+
+    void operator()(expr * e) {    
+        if (is_app(e)) {
+            func_decl * sym = to_app(e)->get_decl();
+            unsigned idx;
+            if (m_parent.try_get_index(sym, idx)) { 
+                SASSERT(idx > 0);
+                --idx;
+                if (m_indices.size() <= idx) {
+                    m_indices.resize(idx+1, false);
+                }
+                m_indices[idx] = true;
+            }
+        }
+    }
+
+    void extract(unsigned_vector& indices) {
+        for (unsigned i = 0; i < m_indices.size(); ++i) {
+            if (m_indices[i]) {
+                indices.push_back(i);
+            }
+        }
+    }
+};
+
+
+
+void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const {
+    indices.reset();
+    index_collector collector(*this);
+    for_each_expr(collector, m_visited, e);
+    m_visited.reset();
+    collector.extract(indices);
+}
+
+class sym_mux::variable_collector {
+    sym_mux const& m_parent;
+    vector<ptr_vector<app> >& m_vars;
+public:
+    variable_collector(sym_mux const& s, vector<ptr_vector<app> >& vars): 
+      m_parent(s), m_vars(vars) {}
+
+    void operator()(expr * e) {    
+        if (is_app(e)) {
+            func_decl * sym = to_app(e)->get_decl();
+            unsigned idx;
+            if (m_parent.try_get_index(sym, idx)) { 
+                SASSERT(idx > 0);
+                --idx;
+                if (m_vars.size() <= idx) {
+                    m_vars.resize(idx+1, ptr_vector<app>());
+                }
+                m_vars[idx].push_back(to_app(e));
+            }
+        }
+    }
+};
+
+void sym_mux::collect_variables(expr* e, vector<ptr_vector<app> >& vars) const {
+    vars.reset();
+    variable_collector collector(*this, vars);
+    for_each_expr(collector, m_visited, e);
+    m_visited.reset();
+}
 
 class sym_mux::hmg_checker {
     const sym_mux & m_parent;
@@ -445,38 +515,6 @@ void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const {
     }
 }
 
-void sym_mux::get_muxed_cube_from_model(const model_core & mdl, expr_ref_vector & res) const
-{
-    res.reset();
-    unsigned sz = mdl.get_num_constants();
-    for (unsigned i = 0; i < sz; i++) {
-        func_decl * d = mdl.get_constant(i);
-
-        if(!is_muxed(d) || m_non_model_syms.contains(get_primary(d))) { continue; }
-
-        SASSERT(d->get_arity()==0);
-        expr_ref interp(m);
-        get_value_from_model(mdl, d, interp);
-
-        app_ref constant(m.mk_const(d), m);
-        app_ref lit(m);
-        if(m.is_bool(d->get_range())) {
-            if(m.is_true(interp)) {
-                lit = constant;
-            }
-            else {
-                SASSERT(m.is_false(interp));
-                lit = m.mk_not(constant);
-            }
-        }
-        else {
-            lit = m.mk_eq(constant, interp);
-        }
-        res.push_back(lit);
-    }
-    //LOGV(5, " got cube "<<pp_cube(res, m));
-}
-
 class sym_mux::decl_idx_comparator
 {
     const sym_mux & m_parent;

lib/pdr_sym_mux.h

@@ -86,6 +86,8 @@ private:
     class hmg_checker;
     class nonmodel_sym_checker;
     class index_renamer_cfg;
+    class index_collector;
+    class variable_collector;
 
     std::string get_suffix(unsigned i) const;
     void ensure_tuple_size(func_decl * prim, unsigned sz) const;
@@ -184,6 +186,15 @@ public:
     */
     bool contains(expr * e, unsigned idx) const;
 
+    /**
+        Collect indices used in expression.
+    */
+    void collect_indices(expr* e, unsigned_vector& indices) const;
+
+    /**
+        Collect used variables of each index.
+    */
+    void collect_variables(expr* e, vector<ptr_vector<app> >& vars) const;
 
     /**
     Convert symbol sym which has to be of src_idx variant into variant tgt_idx.

lib/pdr_util.h

@@ -170,34 +170,15 @@ void vect_set_union(ref_vector<Type,Mgr> & tgt, ref_vector<Type,Mgr> & src, Comp
 }
 
 
-class model_evaluator_base {
-protected:
-    virtual void check_model(ptr_vector<expr> const & formulas, 
-                             expr_ref_vector & model, bool & has_unknown, bool & has_false) = 0;
-public:
-    virtual void minimize_model(ptr_vector<expr> const & formulas, expr_ref_vector & model);
-};
 
-class th_rewriter_model_evaluator : public model_evaluator_base {
+class model_evaluator {
-    class expr_rewriter_cfg;
-    ast_manager& m;
-    th_rewriter  m_rewriter;
-    
-    void setup_assignment(expr_ref_vector const& model, obj_map<expr,expr*>& assignment);
-
-protected:
-    virtual void check_model(ptr_vector<expr> const & formulas, 
-                             expr_ref_vector & model, bool & has_unknown, 
-                             bool & has_false);
-public:
-    th_rewriter_model_evaluator(ast_manager& m) : m(m), m_rewriter(m) {}
-};
-
-class ternary_model_evaluator  : public model_evaluator_base {
     ast_manager& m;
     arith_util   m_arith;
     bv_util      m_bv;
-    obj_map<expr,rational> m_values;
+    obj_map<expr,rational> m_numbers;
+    expr_ref_vector        m_refs;
+    obj_map<expr, expr*>   m_values;
+    model_ref m_model;
 
     //00 -- non-visited
     //01 -- X
@@ -209,16 +190,17 @@ class ternary_model_evaluator  : public model_evaluator_base {
     unsigned m_level2;
     expr_mark m_visited;
 
-    void setup_model(expr_ref_vector const& model);
-    void add_model(expr* e);
-    void del_model(expr* e);
-    
-    bool get_assignment(expr* e, expr*& var, expr*& val);
 
+    void reset();
+    void setup_model(model_ref& model);
+    void assign_value(expr* e, expr* v);
     void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
-    void process_formula(app* e, ptr_vector<expr> todo, ptr_vector<expr>& tocollect);
+    void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
-    void prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model);
+    expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
-    void prune_by_probing(ptr_vector<expr> const & formulas, expr_ref_vector& model);
+    void eval_arith(app* e);
+    void eval_basic(app* e);
+    void eval_iff(app* e, expr* arg1, expr* arg2);
+    void inherit_value(expr* e, expr* v);
 
     //00 -- non-visited
     //01 -- X
@@ -234,27 +216,34 @@ class ternary_model_evaluator  : public model_evaluator_base {
     inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
     inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
     inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
-    inline rational const& get_value(expr* x) const { return m_values.find(x); }
+    inline rational const& get_number(expr* x) const { return m_numbers.find(x); }
-    inline void set_value(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_values.insert(x,v); }
+    inline void set_number(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); }
-
+    inline expr* get_value(expr* x) { return m_values.find(x); }
+    inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); }
 
+    
 protected:
+
     bool check_model(ptr_vector<expr> const & formulas);
-    virtual void check_model(ptr_vector<expr> const & formulas, expr_ref_vector & model, 
-        bool & has_unknown, bool & has_false) {
-            UNREACHABLE();
-    }
 
 public:
-    ternary_model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m) {}
+    model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m), m_refs(m) {}
-    virtual void minimize_model(ptr_vector<expr> const & formulas, expr_ref_vector & model);
+
+    /**
+       \brief extract equalities from model that suffice to satisfy formula.
+
+       \pre model satisfies formulas
+    */
+
+    expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
 
     /**
        \brief extract literals from formulas that satisfy formulas.
 
        \pre model satisfies formulas
     */
-    expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, expr_ref_vector const & model);
+    expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
+
 
     // for_each_expr visitor.
     void operator()(expr* e) {} 
@@ -262,11 +251,6 @@ public:
 
 void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);
 
-/**
-If the solver argument is non-zero, we will exclude its auxiliary symbols from the generated cube.
-*/
-void get_cube_from_model(const model_core & mdl, expr_ref_vector & res, pdr::prop_solver& solver);
-
 }
 
 #endif

lib/qe_lite.cpp

@@ -0,0 +1,536 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    qe_lite.cpp
+
+Abstract:
+
+    Light weight partial quantifier-elimination procedure
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-10-17
+
+Revision History:
+
+ - TBD: integrate Fourier Motzkin elimination
+        integrate Gaussean elimination
+
+--*/
+#include "qe_lite.h"
+#include "expr_abstract.h"
+#include "used_vars.h"
+#include"occurs.h"
+#include"for_each_expr.h"
+#include"rewriter_def.h"
+#include"ast_pp.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+#include"tactical.h"
+#include"bool_rewriter.h"
+#include"var_subst.h"
+
+class der2 {
+    ast_manager &   m;
+    var_subst       m_subst;
+    expr_ref_buffer m_new_exprs;
+    
+    ptr_vector<expr> m_map;
+    int_vector       m_pos2var;
+    ptr_vector<var>  m_inx2var;
+    unsigned_vector  m_order;
+    expr_ref_vector  m_subst_map;
+    expr_ref_buffer  m_new_args;
+
+    /**
+       \brief Return true if e can be viewed as a variable disequality. 
+       Store the variable id in v and the definition in t.
+       For example:
+
+          if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T.
+          if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T).
+              (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))),
+              and can be viewed as a disequality.
+    */
+    bool is_var_diseq(expr * e, unsigned num_decls, var *& v, expr_ref & t);
+
+    /**
+       \brief Return true if e can be viewed as a variable equality.
+    */
+    bool is_var_eq(expr * e, unsigned num_decls, var *& v, expr_ref & t);
+
+    bool is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t);
+
+    void get_elimination_order();
+    void create_substitution(unsigned sz);
+    void apply_substitution(quantifier * q, expr_ref & r);
+    void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr);
+    void elim_unused_vars(expr_ref& r, proof_ref &pr);
+
+public:
+    der2(ast_manager & m):m(m),m_subst(m),m_new_exprs(m),m_subst_map(m),m_new_args(m) {}
+    void operator()(quantifier * q, expr_ref & r, proof_ref & pr);
+    void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr);
+    ast_manager& get_manager() const { return m; }
+};
+
+static bool is_var(expr * e, unsigned num_decls) {
+    return is_var(e) && to_var(e)->get_idx() < num_decls;
+}
+
+static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {
+    expr* e1;
+    return m.is_not(e, e1) && is_var(e1, num_decls);
+}
+
+bool der2::is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t) {
+    if (check_eq) {
+        return is_var_eq(e, num_decls, v, t);
+    }
+    else {
+        return is_var_diseq(e, num_decls, v, t);
+    }    
+}
+
+bool der2::is_var_eq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
+    expr* lhs, *rhs;
+    
+    // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases    
+    if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
+        // (iff (not VAR) t) (iff t (not VAR)) cases
+        if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls) && m.is_bool(lhs)) {
+            if (!is_neg_var(m, lhs, num_decls)) {
+                std::swap(lhs, rhs);
+            }
+            if (!is_neg_var(m, lhs, num_decls)) {
+                return false;
+            }
+            v = to_var(lhs);
+            t = m.mk_not(rhs);
+            m_new_exprs.push_back(t);
+            TRACE("der", tout << mk_pp(e, m) << "\n";);
+            return true;
+        }
+        if (!is_var(lhs, num_decls))
+            std::swap(lhs, rhs);
+        if (!is_var(lhs, num_decls))
+            return false;
+        v = to_var(lhs);
+        t = rhs;
+        TRACE("der", tout << mk_pp(e, m) << "\n";);
+        return true;
+    }
+
+    // (ite cond (= VAR t) (= VAR t2)) case
+    expr* cond, *e2, *e3;
+    if (m.is_ite(e, cond, e2, e3)) {
+        if (is_var_eq(e2, num_decls, v, t)) {
+            expr_ref t2(m);
+            var* v2;
+            if (is_var_eq(e3, num_decls, v2, t2) && v2 == v) {
+                t = m.mk_ite(cond, t, t2);
+                m_new_exprs.push_back(t);
+                return true;
+            }
+        }
+        return false;
+    }
+
+    // VAR = true case
+    if (is_var(e, num_decls)) {
+        t = m.mk_true();
+        v = to_var(e);
+        TRACE("der", tout << mk_pp(e, m) << "\n";);
+        return true;
+    }
+
+    // VAR = false case
+    if (is_neg_var(m, e, num_decls)) {
+        t = m.mk_false();
+        v = to_var(to_app(e)->get_arg(0));
+        TRACE("der", tout << mk_pp(e, m) << "\n";);
+        return true;
+    }
+
+    return false;
+}
+
+/**
+   \brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or 
+                                (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)).
+   The last case can be viewed 
+*/
+bool der2::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
+    expr* e1;
+    if (m.is_not(e, e1)) {
+        return is_var_eq(e, num_decls, v, t);
+    }
+    else if (is_var_eq(e, num_decls, v, t) && m.is_bool(v)) { 
+        bool_rewriter(m).mk_not(t, t);
+        m_new_exprs.push_back(t);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+void der2::elim_unused_vars(expr_ref& r, proof_ref& pr) {
+    if (is_quantifier(r)) {
+        quantifier * q = to_quantifier(r);
+        ::elim_unused_vars(m, q, r);
+        if (m.proofs_enabled()) {
+            proof * p1 = m.mk_elim_unused_vars(q, r);
+            pr = m.mk_transitivity(pr, p1);
+        }
+    }
+}
+
+/**
+   Reduce the set of definitions in quantifier.
+   Then eliminate variables that have become unused
+*/
+void der2::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
+    TRACE("der", tout << mk_pp(q, m) << "\n";);    
+    pr = 0;
+    r  = q;
+    reduce_quantifier(q, r, pr);    
+    if (r != q) {
+        elim_unused_vars(r, pr);
+    }
+}
+
+void der2::reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) {   
+    r = q;
+    // Keep applying reduce_quantifier1 until r doesn't change anymore
+    do {
+        proof_ref curr_pr(m);
+        q  = to_quantifier(r);
+        reduce_quantifier1(q, r, curr_pr);
+        if (m.proofs_enabled()) {
+            pr = m.mk_transitivity(pr, curr_pr);
+        }
+    } while (q != r && is_quantifier(r));
+
+    m_new_exprs.reset();
+}
+
+void der2::reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) {    
+    expr * e = q->get_expr();
+    unsigned num_decls = q->get_num_decls();
+    var * v = 0;
+    expr_ref t(m);    
+    unsigned num_args = 1;
+    expr* const* args = &e;
+    if ((q->is_forall() && m.is_or(e)) ||
+        (q->is_exists() && m.is_and(e))) {
+        num_args = to_app(e)->get_num_args();
+        args     = to_app(e)->get_args();
+    }
+
+    unsigned def_count = 0;
+    unsigned largest_vinx = 0;
+    
+    m_map.reset();
+    m_pos2var.reset();
+    m_inx2var.reset();    
+    m_pos2var.reserve(num_args, -1);
+    
+    // Find all definitions
+    for (unsigned i = 0; i < num_args; i++) {
+        if (is_var_def(q->is_exists(), args[i], num_decls, v, t)) {
+            unsigned idx = v->get_idx();
+            if(m_map.get(idx, 0) == 0) {
+                m_map.reserve(idx + 1, 0);
+                m_inx2var.reserve(idx + 1, 0);                
+                m_map[idx] = t;
+                m_inx2var[idx] = v;
+                m_pos2var[i] = idx;
+                def_count++;
+                largest_vinx = std::max(idx, largest_vinx); 
+            }
+        }
+    }
+    
+    if (def_count > 0) {
+        get_elimination_order();
+        SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
+        
+        if (!m_order.empty()) {            
+            create_substitution(largest_vinx + 1);
+            apply_substitution(q, r);
+        }
+        else {
+            r = q;
+        }
+    }
+    else {
+        TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";);
+        r = q;
+    }
+ 
+    if (m.proofs_enabled()) {
+        pr = r == q ? 0 : m.mk_der(q, r);
+    }    
+}
+
+static void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
+    order.reset();
+    
+    // eliminate self loops, and definitions containing quantifiers.
+    bool found = false;
+    for (unsigned i = 0; i < definitions.size(); i++) {
+        var * v  = vars[i];
+        expr * t = definitions[i];
+        if (t == 0 || has_quantifiers(t) || occurs(v, t))
+            definitions[i] = 0;
+        else
+            found = true; // found at least one candidate
+    }
+    
+    if (!found)
+        return;
+
+    typedef std::pair<expr *, unsigned> frame;
+    svector<frame> todo;
+
+    expr_fast_mark1 visiting;
+    expr_fast_mark2 done;
+
+    unsigned vidx, num;
+
+    for (unsigned i = 0; i < definitions.size(); i++) {
+        if (definitions[i] == 0)
+            continue;
+        var * v = vars[i];
+        SASSERT(v->get_idx() == i);
+        SASSERT(todo.empty());
+        todo.push_back(frame(v, 0));
+        while (!todo.empty()) {
+        start:
+            frame & fr = todo.back();
+            expr * t   = fr.first;
+            if (t->get_ref_count() > 1 && done.is_marked(t)) {
+                todo.pop_back();
+                continue;
+            }
+            switch (t->get_kind()) {
+            case AST_VAR:
+                vidx = to_var(t)->get_idx();
+                if (fr.second == 0) {
+                    CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
+                    // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
+                    if (definitions.get(vidx, 0) != 0) {
+                        if (visiting.is_marked(t)) {
+                            // cycle detected: remove t
+                            visiting.reset_mark(t);
+                            definitions[vidx] = 0;
+                        }
+                        else {
+                            visiting.mark(t);
+                            fr.second = 1;
+                            todo.push_back(frame(definitions[vidx], 0));
+                            goto start;
+                        }
+                    }
+                }
+                else {
+                    SASSERT(fr.second == 1);
+                    if (definitions.get(vidx, 0) != 0) {
+                        visiting.reset_mark(t);
+                        order.push_back(vidx);
+                    }
+                    else {
+                        // var was removed from the list of candidate vars to elim cycle
+                        // do nothing
+                    }
+                }
+                if (t->get_ref_count() > 1)
+                    done.mark(t);
+                todo.pop_back();
+                break;
+            case AST_QUANTIFIER:
+                UNREACHABLE();
+                todo.pop_back();
+                break;
+            case AST_APP:
+                num = to_app(t)->get_num_args();
+                while (fr.second < num) {
+                    expr * arg = to_app(t)->get_arg(fr.second);
+                    fr.second++;
+                    if (arg->get_ref_count() > 1 && done.is_marked(arg))
+                        continue;
+                    todo.push_back(frame(arg, 0));
+                    goto start;
+                }
+                if (t->get_ref_count() > 1)
+                    done.mark(t);
+                todo.pop_back();
+                break;
+            default:
+                UNREACHABLE();
+                todo.pop_back();
+                break;
+            }
+        }
+    }
+}
+
+void der2::get_elimination_order() {
+    m_order.reset();
+
+    TRACE("top_sort",
+        tout << "DEFINITIONS: " << std::endl;
+        for(unsigned i = 0; i < m_map.size(); i++)
+            if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl;
+      );
+
+    // der2::top_sort ts(m);
+    der_sort_vars(m_inx2var, m_map, m_order);
+
+    TRACE("der", 
+            tout << "Elimination m_order:" << std::endl;
+            for(unsigned i=0; i<m_order.size(); i++)
+            {
+                if (i != 0) tout << ",";
+                tout << m_order[i];
+            }
+            tout << std::endl;            
+          );
+}
+
+void der2::create_substitution(unsigned sz) {
+    m_subst_map.reset();
+    m_subst_map.resize(sz, 0);
+
+    for(unsigned i = 0; i < m_order.size(); i++) {
+        expr_ref cur(m_map[m_order[i]], m);
+
+        // do all the previous substitutions before inserting
+        expr_ref r(m);
+        m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);
+
+        unsigned inx = sz - m_order[i]- 1;
+        SASSERT(m_subst_map[inx]==0);
+        m_subst_map[inx] = r;
+    }
+}
+
+void der2::apply_substitution(quantifier * q, expr_ref & r) {
+    expr * e = q->get_expr();
+    unsigned num_args=to_app(e)->get_num_args(); 
+    bool_rewriter rw(m);
+    
+    // get a new expression
+    m_new_args.reset();
+    for(unsigned i = 0; i < num_args; i++) {
+        int x = m_pos2var[i];
+        if (x != -1 && m_map[x] != 0) 
+            continue; // this is a disequality with definition (vanishes)
+                
+        m_new_args.push_back(to_app(e)->get_arg(i));
+    }
+
+    expr_ref t(m);
+    if (q->is_forall()) {
+        rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t);
+    }
+    else {
+        rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t);
+    }
+    expr_ref new_e(m);    
+    m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e);
+    
+    // don't forget to update the quantifier patterns
+    expr_ref_buffer  new_patterns(m);
+    expr_ref_buffer  new_no_patterns(m);
+    for (unsigned j = 0; j < q->get_num_patterns(); j++) {
+        expr_ref new_pat(m);
+        m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat);
+        new_patterns.push_back(new_pat);
+    }
+
+    for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
+        expr_ref new_nopat(m);
+        m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat);
+        new_no_patterns.push_back(new_nopat);
+    }
+
+    r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), 
+                            new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
+}
+
+
+
+
+
+class qe_lite::impl {
+    ast_manager& m;
+    der2         m_der;
+
+public:
+    impl(ast_manager& m): m(m), m_der(m) {}
+    
+    void operator()(app_ref_vector& vars, expr_ref& fml) {
+        expr_ref tmp(fml);
+        quantifier_ref q(m);
+        proof_ref pr(m);     
+        symbol qe_lite("QE");
+        expr_abstract(m, 0, vars.size(), (expr*const*)vars.c_ptr(), fml, tmp);
+        ptr_vector<sort> sorts;
+        svector<symbol> names;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            sorts.push_back(m.get_sort(vars[i].get()));
+            names.push_back(vars[i]->get_decl()->get_name());
+        }
+        q = m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qe_lite);
+        m_der.reduce_quantifier(q, tmp, pr);
+        // assumes m_der just updates the quantifier and does not change things more.
+        if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) {
+            used_vars used;
+            tmp = to_quantifier(tmp)->get_expr();
+            used.process(tmp);
+            var_subst vs(m, true);
+            vs(tmp, vars.size(), (expr*const*)vars.c_ptr(), fml);
+            // collect set of variables that were used.
+            unsigned j = 0;
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                if (used.contains(vars.size()-i-1)) {
+                    vars[j] = vars[i];
+                    ++j;
+                }
+            }
+            vars.resize(j);            
+        }        
+        else {
+            fml = tmp;
+        }
+    }
+
+    void operator()(expr_ref& fml, proof_ref& pr) {
+        // TODO apply der everywhere as a rewriting rule.
+        // TODO add cancel method.
+        if (is_quantifier(fml)) {
+            m_der(to_quantifier(fml), fml, pr);
+        }
+    }
+
+};
+
+qe_lite::qe_lite(ast_manager& m) {
+    m_impl = alloc(impl, m);
+}
+
+qe_lite::~qe_lite() {
+    dealloc(m_impl);
+}
+
+void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) {
+    (*m_impl)(vars, fml);
+}
+
+void qe_lite::operator()(expr_ref& fml, proof_ref& pr) {
+    (*m_impl)(fml, pr);
+}

lib/qe_lite.h

@@ -0,0 +1,49 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    qe_lite.h
+
+Abstract:
+
+    Light weight partial quantifier-elimination procedures 
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-10-17
+
+Revision History:
+
+
+--*/
+
+#ifndef __QE_LITE_H__
+#define __QE_LITE_H__
+
+#include "ast.h"
+
+class qe_lite {
+    class impl;
+    impl * m_impl;
+public:
+    qe_lite(ast_manager& m);
+
+    ~qe_lite();
+
+    /**
+       \brief
+       Apply light-weight quantifier elimination 
+       on constants provided as vector of variables. 
+       Return the updated formula and updated set of variables that were not eliminated.
+
+    */
+    void operator()(app_ref_vector& vars, expr_ref& fml);
+
+    /**
+        \brief full rewriting based light-weight quantifier elimination round.
+    */
+    void operator()(expr_ref& fml, proof_ref& pr);
+};
+
+#endif __QE_LITE_H__