Commits

Nikolaj Bjorner committed ff4b9da

fix solution generation for quantified integer arithmetic. Added unit tests

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

Comments (0)

Files changed (6)

src/muz_qe/qe.cpp

 #include "cooperate.h"
 #include "tactical.h"
 #include "model_v2_pp.h"
+#include "obj_hashtable.h"
 
 
 namespace qe {
     };
 
     // ----------------------------
+    // def_vector
+
+    void def_vector::normalize() {
+        // apply nested definitions into place.
+        ast_manager& m = m_vars.get_manager();
+        expr_substitution sub(m);
+        scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
+        if (size() <= 1) {
+            return;
+        }
+        for (unsigned i = size(); i > 0; ) {
+            --i;
+            expr_ref e(m);
+            e = def(i);
+            rep->set_substitution(&sub);
+            (*rep)(e);
+            sub.insert(m.mk_const(var(i)), e);
+            def_ref(i) = e;
+        }
+    }        
+
+    void def_vector::project(unsigned num_vars, app* const* vars) {
+        obj_hashtable<func_decl> fns;
+        for (unsigned i = 0; i < num_vars; ++i) {
+            fns.insert(vars[i]->get_decl());
+        }
+        for (unsigned i = 0; i < size(); ++i) {
+            if (fns.contains(m_vars[i].get())) {
+                // 
+                // retain only first occurrence of eliminated variable.
+                // later occurrences are just recycling the name.
+                // 
+                fns.remove(m_vars[i].get());
+            }
+            else {
+                for (unsigned j = i+1; j < size(); ++j) {
+                    m_vars[j-1] = m_vars[j];
+                    m_defs[j-1] = m_defs[j];
+                }
+                m_vars.pop_back();
+                m_defs.pop_back();
+                --i;
+            }
+        }
+    }
+
+    // ----------------------------
+    // guarded_defs
+
+    std::ostream& guarded_defs::display(std::ostream& out) const {
+        ast_manager& m = m_guards.get_manager();
+        for (unsigned i = 0; i < size(); ++i) {            
+            for (unsigned j = 0; j < defs(i).size(); ++j) {
+                out << defs(i).var(j)->get_name() << " := " << mk_pp(defs(i).def(j), m) << "\n";
+            }
+            out << "if " << mk_pp(guard(i), m) << "\n";
+        }       
+        return out;
+    }
+
+    bool guarded_defs::inv() {
+        return m_defs.size() == m_guards.size();
+    }
+
+    void guarded_defs::add(expr* guard, def_vector const& defs) {
+        SASSERT(inv());
+        m_defs.push_back(defs);
+        m_guards.push_back(guard);
+        m_defs.back().normalize();
+        SASSERT(inv());
+    }
+
+    void guarded_defs::project(unsigned num_vars, app* const* vars) {
+        for (unsigned i = 0; i < size(); ++i) {
+            m_defs[i].project(num_vars, vars);
+        }
+    }
+
+    // ----------------------------
     // Obtain atoms in NNF formula.
     
     class nnf_collect_atoms {
     
         virtual lbool eliminate_exists(
             unsigned num_vars, app* const* vars, 
-            expr_ref& fml, app_ref_vector& free_vars, bool get_first, def_vector* defs) = 0;
+            expr_ref& fml, app_ref_vector& free_vars, bool get_first, guarded_defs* defs) = 0;
 
         virtual void set_assumption(expr* fml) = 0;
 
             }
         }
 
-        bool get_leaf_rec(expr_ref& fml, def_vector& defs) {
+        void get_leaves_rec(def_vector& defs, guarded_defs& gdefs) {
             expr* f = this->fml();
+            unsigned sz = defs.size();
+            defs.append(def());
             if (m_children.empty() && f && !m.is_false(f) &&
                 m_vars.empty() && !has_var()) {
-                fml = f;
-                return true;
+                gdefs.add(f, defs); 
             }
-            unsigned sz = defs.size();
-            for (unsigned i = 0; i < m_children.size(); ++i) {
-                search_tree* st = m_children[i];
-                defs.append(st->def());
-                if (st->get_leaf_rec(fml, defs)) {
-                    return true;
+            else {
+                for (unsigned i = 0; i < m_children.size(); ++i) {
+                    m_children[i]->get_leaves_rec(defs, gdefs);
                 }
-                defs.shrink(sz);
             }
-            return false;
+            defs.shrink(sz);
         }
 
-        void get_leaf(expr_ref& fml, def_vector& defs) {
-            get_leaf_rec(fml, defs);
-
-            // apply nested definitions into place.
-            expr_substitution sub(m);
-            scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
-            for (unsigned i = defs.size(); i > 0; ) {
-                --i;
-                expr_ref e(m);
-                e = defs.def(i);
-                rep->set_substitution(&sub);
-                (*rep)(e);
-                sub.insert(m.mk_const(defs.var(i)), e);
-                defs.def_ref(i) = e;
-            }            
+        void get_leaves(guarded_defs& gdefs) {
+            def_vector defs(m);
+            get_leaves_rec(defs, gdefs);
         }
 
         void reset() {
 
         app_ref_vector               m_new_vars;     // variables added by solvers
         bool                         m_get_first;    // get first satisfying branch.
-        def_vector*                  m_defs;
+        guarded_defs*                m_defs;
         nnf_normalizer               m_nnf;          // nnf conversion
 
     
 
         void check(unsigned num_vars, app* const* vars, 
                    expr* assumption, expr_ref& fml, bool get_first,
-                   app_ref_vector& free_vars, def_vector* defs) {
+                   app_ref_vector& free_vars, guarded_defs* defs) {
 
             reset();
             m_solver.push();
                 expr_ref_vector result(m);
                 m_root.get_leaves(result);
                 m_bool_rewriter.mk_or(result.size(), result.c_ptr(), fml);
-            }
-            else if (defs) {
-                m_root.get_leaf(fml, *defs);
+            }            
+
+            if (defs) {
+                m_root.get_leaves(*defs);
+                defs->project(num_vars, vars);
             }
             
             TRACE("qe", 
     private:
 
         void final_check(model_evaluator& model_eval) {
-            TRACE("qe", tout << (m_fml?"fml":"null") << "\n";);
+            TRACE("qe", tout << "\n";);
             while (can_propagate_assignment(model_eval)) {
                 propagate_assignment(model_eval);
             }
             m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, 0);
         }
 
-        lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, def_vector* defs) {
+        lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, guarded_defs* defs) {
             return m_qe.eliminate_exists(num_vars, vars, fml, m_free_vars, get_first, defs);
         }
     
 
         void propagate_assignment(model_evaluator& model_eval) {
             if (m_fml) {
-                update_current(model_eval, true);
+                update_status st = update_current(model_eval, true);
             }
         }
 
 
         virtual lbool eliminate_exists(
             unsigned num_vars, app* const* vars, expr_ref& fml, 
-            app_ref_vector& free_vars, bool get_first, def_vector* defs) {
+            app_ref_vector& free_vars, bool get_first, guarded_defs* defs) {
             if (get_first) {
                 return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs);
             }
 
         lbool eliminate_block(
             unsigned num_vars, app* const* vars, expr_ref& fml, 
-            app_ref_vector& free_vars, bool get_first, def_vector* defs) {
+            app_ref_vector& free_vars, bool get_first, guarded_defs* defs) {
               
             checkpoint();
             
 
     };
 
-
-
-#if 0
-    //
-    // Instantiation based quantifier elimination procedure.
-    // try a few loops of checking satisfiability.
-    // substitute in model values for bound variables.
-    // 
-    class quant_elim_inst : public quant_elim {
-        ast_manager& 
-    public:
-        quant_elim_inst(ast_manager& m): m(m) {}
-
-        virtual lbool eliminate_exists(
-            unsigned num_vars, app* const* vars, 
-            expr_ref& fml, app_ref_vector& free_vars, bool get_first, def_vector* defs) {
-            
-        }
-
-        virtual void set_assumption(expr* fml) {}
-
-        virtual void collect_statistics(statistics & st) const {
-            m_solver.collect_statistics(st);
-        }
-
-        virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) {
-            if (is_forall) {
-                fml = m.mk_not(fml);
-                r = eliminate_exists(num_vars, vars, fml, free_vars, false, defs);
-                fml = m.mk_not(fml);
-            }
-            else {
-                r = eliminate_exists(num_vars, vars, fml, free_vars, false, defs);
-            }
-        }
-
-        virtual void set_cancel(bool f) {
-            m_solver.set_cancel(f);
-        }
-
-        virtual void updt_params(params_ref const& p) {
-            m_solver.updt_params(p);
-        }
-
-    };
-#endif
-
-
     // ------------------------------------------------
     // expr_quant_elim
 
     lbool expr_quant_elim::first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) {
         app_ref_vector fvs(m);
         init_qe();
-        return m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &defs);
+        guarded_defs gdefs(m);
+        lbool res = m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &gdefs);
+        if (gdefs.size() > 0) {
+            defs.reset();
+            defs.append(gdefs.defs(0));
+            fml = gdefs.guard(0);
+        }
+        return res;
     }
 
-    bool expr_quant_elim::solve_for_var(app* var, expr* _fml, expr_ref_vector& terms, expr_ref_vector& fmls) {
-        expr_ref assms(m.mk_true(), m);
-        func_decl* v = var->get_decl();
-        init_qe();  
-        while (true) {
-            def_vector defs(m);
-            app_ref_vector fvs(m);
-            m_qe->set_assumption(assms);
-            expr_ref fml(_fml, m);
-            lbool is_sat = m_qe->eliminate_exists(1, &var, fml, fvs, true, &defs);
-            switch (is_sat) {
-            case l_false: return true;
-            case l_undef: return false;
-            default: break;                
-            }
-            bool found = false;
-            for (unsigned i = 0; !found && i < defs.size(); ++i) {
-                if (defs.var(i) == v) {
-                    terms.push_back(defs.def(i));
-                    fmls.push_back(fml);
-                    found = true;
-                }
-            }
-            if (!found) {
-                NOT_IMPLEMENTED_YET();
-            }
-            assms = m.mk_and(assms, m.mk_not(fml));
-        }
-        return true;
+    bool expr_quant_elim::solve_for_var(app* var, expr* fml, guarded_defs& defs) {
+        return solve_for_vars(1,&var, fml, defs);
     }
 
+    bool expr_quant_elim::solve_for_vars(unsigned num_vars, app* const* vars, expr* _fml, guarded_defs& defs) {
+        app_ref_vector fvs(m);
+        expr_ref fml(_fml, m);
+        TRACE("qe", tout << mk_pp(fml, m) << "\n";);
+        init_qe();  
+        lbool is_sat = m_qe->eliminate_exists(num_vars, vars, fml, fvs, false, &defs);
+        return is_sat != l_undef;
+    }
 
     void expr_quant_elim::set_cancel(bool f) {
         if (m_qe) {
     class def_vector {
         func_decl_ref_vector m_vars;
         expr_ref_vector      m_defs;
+        def_vector& operator=(def_vector const& other);
     public:
         def_vector(ast_manager& m): m_vars(m), m_defs(m) {}
+        def_vector(def_vector const& other): m_vars(other.m_vars), m_defs(other.m_defs) {}
         void push_back(func_decl* v, expr* e) {
             m_vars.push_back(v);
             m_defs.push_back(e);
         func_decl* var(unsigned i) const { return m_vars[i]; }
         expr*  def(unsigned i) const { return m_defs[i]; }
         expr_ref_vector::element_ref  def_ref(unsigned i) { return m_defs[i]; }
+        void normalize();
+        void project(unsigned num_vars, app* const* vars);
+    };
+
+    /**
+       \brief Guarded definitions.
+
+       A realizer to a an existential quantified formula is a disjunction
+       together with a substitution from the existentially quantified variables
+       to terms such that:
+       1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.
+       2. Each guard is equivalent to fml where 'vars' are replaced by the substitution associated
+          with the guard.       
+    */
+
+    class guarded_defs {
+        expr_ref_vector    m_guards;
+        vector<def_vector> m_defs;
+        bool inv();
+    public:
+        guarded_defs(ast_manager& m): m_guards(m) { SASSERT(inv()); }
+        void add(expr* guard, def_vector const& defs);
+        unsigned size() const { return m_guards.size(); }
+        def_vector const& defs(unsigned i) const { return m_defs[i]; }
+        expr* guard(unsigned i) const { return m_guards[i]; }
+        std::ostream& display(std::ostream& out) const;
+        void project(unsigned num_vars, app* const* vars);
     };
 
     class quant_elim; 
            \brief solve for (exists (var) fml).
            Return false if operation failed.
            Return true  and list of pairs (t_i, fml_i) in <terms, fmls>
-                          such that fml[t_1] \/ ... \/ fml[t_n] == (exists (var) fml)
-                          and       fml_i == fml[t_1]
+                          such that fml_1 \/ ... \/ fml_n == (exists (var) fml)
+                          and       fml_i => fml[t_i]
          */
-        bool solve_for_var(app* var, expr* fml, expr_ref_vector& terms, expr_ref_vector& fmls);
+        bool solve_for_var(app* var, expr* fml, guarded_defs& defs);
+
+        bool solve_for_vars(unsigned num_vars, app* const* vars, expr* fml, guarded_defs& defs);
 
 
         void set_cancel(bool f);

src/muz_qe/qe_arith_plugin.cpp

             simplify(result);
         }
 
-        expr_ref mk_idiv(expr* a, numeral const & k) {            
-            if (k.is_one()) {
-                return expr_ref(a, m);
-            }
-            expr_ref result(m);
-            result = m_arith.mk_idiv(a, m_arith.mk_numeral(k, true));
-            simplify(result);
-            return result;
-        }
-    
         expr* mk_numeral(numeral const& k, bool is_int = true) { return m_arith.mk_numeral(k, is_int); }
 
         expr* mk_numeral(int k, bool is_int) { return mk_numeral(numeral(k),is_int); }
 
     private:
 
+        /**
+           \brief Compute least upper/greatest lower bounds for x.
+
+           Assume:
+           (not (= k 0))
+           (<= 0 (mod m k)) 
+           (< (mod m k) (abs k))
+           (= m (+ (* k (div m k)) (mod m k)))
+           i.e. 
+             k * (e div k) + (e mod k) = e
+
+           
+           When k is positive, least upper bound 
+           for x such that: k*x <= e is e div k
+
+           When k is negative, greatest lower bound 
+           for x such that k*x <= e is e div k
+
+           k * (e div k) + (e mod k) = e                   
+         */
+        expr_ref mk_idiv(expr* e, numeral k) {            
+            SASSERT(!k.is_zero());
+            arith_util& a = m_util.m_arith; 
+            if (k.is_one()) {
+                return expr_ref(e, m);
+            }
+            if (k.is_minus_one()) {
+                return expr_ref(a.mk_uminus(e), m);
+            }
+            SASSERT(a.is_int(e));
+            return expr_ref(a.mk_idiv(e, a.mk_numeral(k, true)), m);
+        }
+    
+
         void get_def(contains_app& contains_x, unsigned v, expr* fml, expr_ref& def) {
             app* x = contains_x.x();
             x_subst x_t(m_util);
                     // a*x + term <= 0
                     expr_ref term(bounds.exprs(is_strict, !is_lower)[i], m);
                     rational a = bounds.coeffs(is_strict, !is_lower)[i];
+
                     if (x_t.get_term()) {
-                        // a*(c*x' + s) + term <= 0
-                        // term <- a*s + term
-                        // a <- a*c
-                        term = m_util.mk_add(m_util.mk_mul(a,x_t.get_term()), term);
-                        a = a * x_t.get_coeff();
+                        // x := coeff * x' + s                        
+                        // solve instead for
+                        // a*coeff*x' + term + a*s <= 0
+                        TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + " 
+                              << mk_pp(x_t.get_term(), m) << "\n";);
+                        SASSERT(x_t.get_coeff().is_pos());
+                        term = m_util.mk_add(term, m_util.mk_mul(a, x_t.get_term()));
+                        a    = a * x_t.get_coeff();
                     }
+
+                    TRACE("qe", tout << a << "* " << mk_pp(x,m) << " + " << mk_pp(term, m) << " <= 0\n";);
                     SASSERT(a.is_int());
-                    if (is_lower) {
-                        //    a*x + t <= 0
-                        // <=
-                        //   x <= -t div a
-                        SASSERT(a.is_pos());
-                        term = m_util.mk_idiv(m_util.mk_uminus(term), a);
-                    }
-                    else {
-                        //   -a*x + t <= 0
-                        // <=>
-                        //    t <= a*x
-                        // <=
-                        //   ((div t a) + 1) <= x
-                        term = m_util.mk_idiv(term, abs(a));
-                        if (!(abs(a).is_one())) {
-                            term = m_util.mk_add(term, m_util.mk_one(x));
-                        }
-                    }
-                    terms.push_back(term);
                     SASSERT(is_lower == a.is_pos());                    
-                    TRACE("qe", tout << is_lower << " " << a << " " << mk_pp(term, m) << "\n";);
+
+                    //    a*x + t <= 0
+                    // <=
+                    //   x <= -t div a + 1
+                    
+                    term = m_util.mk_uminus(term);
+                    term = mk_idiv(term, a);
+                    terms.push_back(term);
+                    TRACE("qe", tout << "a: " << a << " term: " << mk_pp(term, m) << "\n";);
                 }
                 is_strict = true;
                 sz = bounds.size(is_strict, !is_lower);
                 }
                 
                 if (x_t.get_term()) {
-                    //
-                    //    x = x_t.get_coeff()*x' + x_t.get_term()
-                    // =>
-                    //    x' = (x - x_t.get_term()) div x_t.get_coeff()
-                    // 
-                    def = m_util.mk_idiv(m_util.mk_sub(def, x_t.get_term()), x_t.get_coeff());
+                    // x := coeff * x + s
+                    TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + " 
+                          << mk_pp(x_t.get_term(), m) << "\n";);
+                    def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term());
                 }
-
                 m_util.simplify(def);
                 return;
             }
             // assert v => (x <= t_i) 
             //
             SASSERT(v < bounds.size(is_strict, is_lower));
-            expr_ref t(bounds.exprs(is_strict, is_lower)[v], m);
+            def = bounds.exprs(is_strict, is_lower)[v];
             rational a = bounds.coeffs(is_strict, is_lower)[v];
+
+            if (x_t.get_term()) {
+                // x := coeff * x' + s                        
+                // solve instead for
+                // a*coeff*x' + term + a*s <= 0
+                TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + " 
+                      << mk_pp(x_t.get_term(), m) << "\n";);
+                SASSERT(x_t.get_coeff().is_pos());
+                def = m_util.mk_add(def, m_util.mk_mul(a, x_t.get_term()));
+                a    = a * x_t.get_coeff();
+            }
+
+            SASSERT(a.is_int());
+            SASSERT(is_lower != a.is_pos());                    
+
+            //    a*x + t <= 0
+            // <=
+            //   x <= -t div a 
             
-            t = x_t.mk_term(a, t);
-            a = x_t.mk_coeff(a);
+            def = m_util.mk_uminus(def);
+            def = mk_idiv(def, a);
 
-            def = t;
-            if (a.is_pos()) {
-                def = m_util.mk_uminus(def);
-            }
             if (x_t.get_term()) {
-                def = m_util.mk_idiv(m_util.mk_sub(def, x_t.get_term()), x_t.get_coeff());
-            }
-            if (!a.is_one()) {
-                def = m_util.mk_idiv(def, a);
+                // x := coeff * x + s
+                def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term());
             }
+
             m_util.simplify(def);
 
-            TRACE("qe", tout << "TBD: " << a << " " << mk_pp(t, m) << "\n";);
+
+            TRACE("qe", tout << "TBD: " << a << " " << mk_pp(def, m) << "\n";);
         }
 
         expr_ref mk_not(expr* e) {

src/muz_qe/qe_datatype_plugin.cpp

             SASSERT(m_datatype_util.is_datatype(s));
             TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
             if (m_datatype_util.is_recursive(s)) {
-                subst_rec(x, vl, fml);
+                subst_rec(x, vl, fml, def);
             }
             else {
-                subst_nonrec(x, vl, fml);
+                subst_nonrec(x, vl, fml, def);
             }
             if (def) {
                 *def = 0; // TBD
         
     private:
 
+        void add_def(expr* term, expr_ref* def) {
+            if (def) {
+                *def = term;
+            }
+        }
+
         //
         // replace x by C(y1,..,yn) where y1,..,yn are fresh variables.
         //
-        void subst_constructor(contains_app& x, func_decl* c, expr_ref& fml) {
+        void subst_constructor(contains_app& x, func_decl* c, expr_ref& fml, expr_ref* def) {
             subst_clos* sub = 0;
             
             if (m_subst_cache.find(x.x(), c, sub)) {
                 m_replace->apply_substitution(x.x(), sub->first, 0, fml);
+                add_def(sub->first, def);
                 for (unsigned i = 0; i < sub->second.size(); ++i) {
                     m_ctx.add_var(sub->second[i]);
                 }
             m_trail.push_back(c);
             m_trail.push_back(t);
 
+            add_def(t, def);
             m_replace->apply_substitution(x.x(), t, 0, fml);
             sub->first = t;
             m_subst_cache.insert(x.x(), c, sub);
             }
         }
 
-        void subst_rec(contains_app& contains_x, rational const& vl, expr_ref& fml) {
+        void subst_rec(contains_app& contains_x, rational const& vl, expr_ref& fml, expr_ref* def) {
             app* x = contains_x.x();
             sort* s = x->get_decl()->get_range();
             SASSERT(m_datatype_util.is_datatype(s));
                 app_ref fresh_x(m.mk_fresh_const("x", s), m);
                 m_ctx.add_var(fresh_x);
                 m_replace->apply_substitution(x, fresh_x, 0, fml);
+                add_def(fresh_x, def);
                 TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
                 return;
             }
 
             if (has_selector(contains_x, fml, c)) {
                 TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
-                subst_constructor(contains_x, c, fml); 
+                subst_constructor(contains_x, c, fml, def); 
                 return;
             }
 
             if (idx < eqs.num_eqs()) {
                 expr* t = eqs.eq(idx);
                 expr* c = eqs.eq_cond(idx);
+                add_def(t, def);
                 m_replace->apply_substitution(x, t, fml);
                 if (!m.is_true(c)) {
                     fml = m.mk_and(c, fml);
                 for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
                     m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
                 }
+                if (def) {
+                    NOT_IMPLEMENTED_YET();
+                    // you need to create a diagonal term
+                }
             }
             TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
         }
             m_ctx.add_constraint(true, is_c);
         }
 
-        virtual void subst_nonrec(contains_app& x, rational const& vl, expr_ref& fml) {
+        virtual void subst_nonrec(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
             sort* s = x.x()->get_decl()->get_range();
             SASSERT(m_datatype_util.is_datatype(s));
             SASSERT(!m_datatype_util.is_recursive(s));
                 SASSERT(vl.get_unsigned() < sz);
                 c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
             }
-            subst_constructor(x, c, fml);                
+            subst_constructor(x, c, fml, def);                
         }
 
 

src/test/dead/qe_defs.cpp

-#include "arith_decl_plugin.h"
-#include "qe.h"
-#include "ast_pp.h"
-#include "smtparser.h"
-#include "reg_decl_plugins.h"
-
-
-static void test_defs(ast_manager& m, expr* _fml) {
-    arith_util a(m);
-    app_ref x(m);
-    qe::def_vector defs(m);
-    expr_ref fml(_fml, m);
-    x = m.mk_const(symbol("x"), a.mk_int());
-    app* vars[1] = { x.get() };
-    front_end_params fparams;
-    qe::expr_quant_elim qelim(m, fparams);
-    lbool result = qelim.first_elim(1, vars, fml, defs);
-    std::cout << mk_pp(_fml, m) << "\n--->\n";
-    std::cout << mk_pp(fml, m)  << "\n";
-    for (unsigned i = 0; i < defs.size(); ++i) {
-        std::cout << defs.var(i)->get_name() << " " 
-                  << mk_pp(defs.def(i), m) << "\n";
-    }
-    std::cout << "\n";
-}
-
-static void test_defs_all(ast_manager& m, expr* _fml) {
-    arith_util a(m);
-    app_ref x(m);
-    expr_ref fml(_fml, m), fml0(_fml, m);
-    x = m.mk_const(symbol("x"), a.mk_int());
-    app* vars[1] = { x.get() };
-    front_end_params fparams;
-    qe::expr_quant_elim qelim(m, fparams);
-    lbool result = l_true;
-    while (result == l_true) {
-        fml = fml0;
-        qe::def_vector defs(m);
-        result = qelim.first_elim(1, vars, fml, defs);
-        std::cout << result << "\n";
-        std::cout << mk_pp(fml, m) << "\n";
-        for (unsigned i = 0; i < defs.size(); ++i) {
-            std::cout << defs.var(i)->get_name() << " " 
-                      << mk_pp(defs.def(i), m) << "\n";
-        }
-        fml0 = m.mk_and(fml0, m.mk_not(fml));
-    }
-}
-
-static void test_defs(char const* str) {
-    ast_manager m;
-    reg_decl_plugins(m);    
-    scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
-    parser->initialize_smtlib();
-    std::ostringstream buffer;
-    buffer << "(benchmark presburger :status unknown :logic AUFLIA "
-           << ":extrafuns ((x Int) (y Int) (z Int))\n"
-           << ":formula " << str << ")";
-    parser->parse_string(buffer.str().c_str());
-    smtlib::benchmark* b = parser->get_benchmark();
-    smtlib::theory::expr_iterator it  = b->begin_formulas();
-    smtlib::theory::expr_iterator end = b->end_formulas();
-    for (; it != end; ++it) {
-        test_defs(m, *it);
-    }
-}
-
-void tst_qe_defs() {
-    enable_trace("qe");
-    test_defs("(and (<= (* 2 x) y) (>= (* 3 x) z) (<= (* 4 x) (* 2 z)) (= (mod x 2) 0))");
-
-    return;
-    test_defs("(and (<= (* 2 x) y) (>= (* 3 x) z) (= (mod x 2) 0))");
-    test_defs("(and (<= (* 2 x) y) (= (mod x 2) 0))");
-    test_defs("(= (* 2 x) y)");
-    test_defs("(or (< x 0) (> x 1))");
-    test_defs("(or (< x y) (> x y))");
-    test_defs("(= x y)");
-    test_defs("(<= x y)");
-    test_defs("(>= x y)");
-    test_defs("(and (<= (+ x y) 0) (<= (+ x z) 0))");
-    test_defs("(and (<= (+ x y) 0) (<= (+ (* 2 x) z) 0))");
-    test_defs("(and (<= (+ (* 3 x) y) 0) (<= (+ (* 2 x) z) 0))");
-    test_defs("(and (>= x y) (>= x z))");
-    test_defs("(< x y)");
-    test_defs("(> x y)");
-}

src/test/quant_solve.cpp

 #include "expr_replacer.h"
 #include "smt_solver.h"
 #include "reg_decl_plugins.h"
+#include "smtparser.h"
+#include "expr_abstract.h"
+#include "model_smt2_pp.h"
 
-static void validate_quant_solution(ast_manager& m, app* x, expr* fml, expr* t, expr* new_fml) {
+static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) {
     // verify:
-    //    new_fml <=> fml[t/x]
+    //    new_fml => fml[t/x]
     scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
+    app_ref_vector xs(m);
     expr_substitution sub(m);
-    sub.insert(x, t);
+    for (unsigned i = 0; i < defs.size(); ++i) {
+        xs.push_back(m.mk_const(defs.var(i)));
+        sub.insert(xs.back(), defs.def(i));
+    }
     rep->set_substitution(&sub);
     expr_ref fml1(fml, m);
     (*rep)(fml1);
     expr_ref tmp(m);
-    tmp = m.mk_not(m.mk_iff(new_fml, fml1));
+    tmp = m.mk_not(m.mk_implies(guard, fml1));
+    front_end_params fp;
+    smt::solver solver(m, fp);
+    solver.assert_expr(tmp);
+    lbool res = solver.check();
+    //SASSERT(res == l_false);
+    if (res != l_false) {
+        std::cout << "Validation failed: " << res << "\n";
+        std::cout << mk_pp(tmp, m) << "\n";
+        model_ref model;
+        solver.get_model(model);
+        model_smt2_pp(std::cout, m, *model, 0);
+        fatal_error(0);
+    }
+}
+
+
+static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) {
+    return;
+    // quant_elim option got removed...
+    // verify:
+    //    fml <=> guard_1 \/ guard_2 \/ ... 
+    ast_manager& m = guards.get_manager();
+    expr_ref tmp(m), fml2(m);
+    tmp = m.mk_or(guards.size(), guards.c_ptr());
+    expr* _x = x;
+    std::cout << mk_pp(fml, m) << "\n";
+    expr_abstract(m, 0, 1, &_x, fml, fml2);
+    std::cout << mk_pp(fml2, m) << "\n";
+    symbol name(x->get_decl()->get_name());
+    sort* s = m.get_sort(x);
+    fml2 = m.mk_exists(1, &s, &name, fml2);
+    std::cout << mk_pp(fml2, m) << "\n";
+    tmp = m.mk_not(m.mk_iff(fml2, tmp));
+    std::cout << mk_pp(tmp, m) << "\n";
     front_end_params fp;
     smt::solver solver(m, fp);
     solver.assert_expr(tmp);
     lbool res = solver.check();
-    std::cout << res << "\n";
+    std::cout << "checked\n";
     SASSERT(res == l_false);
+    if (res != l_false) {
+        std::cout << res << "\n";
+        fatal_error(0);
+    }
 }
 
 static void test_quant_solver(ast_manager& m, app* x, expr* fml) {
     front_end_params params;
-    params.m_quant_elim = true;
     qe::expr_quant_elim qe(m, params);
-    expr_ref_vector terms(m);
-    expr_ref_vector fmls(m);
-    bool success = qe.solve_for_var(x, fml, terms, fmls);
+    qe::guarded_defs defs(m);
+    bool success = qe.solve_for_var(x, fml, defs);
     std::cout << "------------------------\n";
     std::cout << mk_pp(fml, m) << "\n";
-    if (success) {
-        for (unsigned i = 0; i < terms.size(); ++i) {
-            std::cout << mk_pp(x, m) << " = " << mk_pp(terms[i].get(), m) << "\n" << mk_pp(fmls[i].get(), m) << "\n";
-            validate_quant_solution(m, x, fml, terms[i].get(), fmls[i].get());
+    if (success) {        
+        defs.display(std::cout);
+        for (unsigned i = 0; i < defs.size(); ++i) {     
+            validate_quant_solution(m, fml, defs.guard(i), defs.defs(i));
         }
     }
     else {
     }
 }
 
-static void test_quant_solver_rec(ast_manager& m, unsigned num_vars, app* const* xs, expr* fml) {
-    if (num_vars == 0) {
-        return;
-    }
+
+static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) {
     front_end_params params;
-    params.m_quant_elim = true;
     qe::expr_quant_elim qe(m, params);
-    expr_ref_vector fmls(m), ors(m), terms(m);
-    app* x = xs[0];
-    bool success = qe.solve_for_var(x, fml, terms, fmls);
+    qe::guarded_defs defs(m);
+    bool success = qe.solve_for_vars(sz, xs, fml, defs);
     std::cout << "------------------------\n";
     std::cout << mk_pp(fml, m) << "\n";
-    if (success) {
-        for (unsigned i = 0; i < terms.size(); ++i) {
-            std::cout << mk_pp(x, m) << " = " << mk_pp(terms[i].get(), m) << "\n" << mk_pp(fmls[i].get(), m) << "\n";
-            validate_quant_solution(m, x, fml, terms[i].get(), fmls[i].get());
-            ors.reset();
-            if (m.is_or(fmls[i].get())) {
-                ors.append(to_app(fmls[i].get())->get_num_args(), to_app(fmls[i].get())->get_args());
-            }
-            else {
-                ors.push_back(fmls[i].get());
-            }
-            for (unsigned j = 0; j < ors.size(); ++j) {
-                test_quant_solver_rec(m, num_vars-1, xs+1, ors[j].get());
-            }
+    if (success) {        
+        defs.display(std::cout);
+        for (unsigned i = 0; i < defs.size(); ++i) {     
+            validate_quant_solution(m, fml, defs.guard(i), defs.defs(i));
         }
     }
     else {
 }
 
 
+static expr_ref parse_fml(ast_manager& m, char const* str) {
+    expr_ref result(m);
+    reg_decl_plugins(m);    
+    scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
+    parser->initialize_smtlib();
+    std::ostringstream buffer;
+    buffer << "(benchmark presburger :status unknown :logic AUFLIA "
+           << ":extrafuns ((x Int) (y Int) (z Int) (a Int) (b Int))\n"
+           << ":formula " << str << ")";
+    parser->parse_string(buffer.str().c_str());
+    smtlib::benchmark* b = parser->get_benchmark();
+    smtlib::theory::expr_iterator it  = b->begin_formulas();
+    smtlib::theory::expr_iterator end = b->end_formulas();
+    SASSERT(it != b->end_formulas());
+    result = *it;
+    return result;
+}
+
+static void test_quant_solver(ast_manager& m, app* x, char const* str) {
+    expr_ref fml = parse_fml(m, str);
+    test_quant_solver(m, x, fml);
+}
+
+static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str) {
+    expr_ref fml = parse_fml(m, str);
+    test_quant_solver(m, sz, xs, fml);
+}
+
+
 
 static void test_quant_solve1() {
     ast_manager m;
     arith_util ar(m);
-
     reg_decl_plugins(m);
     sort* i = ar.mk_int();
-    app_ref x(m.mk_const(symbol("x"),i), m);
-    app_ref y(m.mk_const(symbol("y"),i), m);
-    app_ref a(m.mk_const(symbol("a"),i), m);
-    app_ref b(m.mk_const(symbol("b"),i), m);
-    expr_ref n2(ar.mk_numeral(rational(2), true), m);
-    expr_ref n3(ar.mk_numeral(rational(3), true), m);
-    expr_ref n4(ar.mk_numeral(rational(4), true), m);
-    expr_ref n10(ar.mk_numeral(rational(10), true), m);
-    expr_ref n20(ar.mk_numeral(rational(20), true), m);
-    expr_ref x2(ar.mk_mul(n2, x), m);
-    expr_ref x3(ar.mk_mul(n3, x), m);
-    expr_ref fml1(m), fml2(m), fml3(m), fml4(m);
-    expr_ref fml(m), t1(m), t2(m);
-
-    fml1 = m.mk_eq(x, a);
-    fml2 = ar.mk_lt(x, a);
-    fml3 = ar.mk_gt(x, a);
-    fml4 = m.mk_and(ar.mk_lt(x, a), ar.mk_lt(x, b));
-    expr_ref fml5(m.mk_and(ar.mk_gt(x, a), ar.mk_lt(x, b)), m);
-    expr_ref fml6(ar.mk_le(x, a), m);
-    expr_ref fml7(ar.mk_ge(x, a), m);
-    expr_ref fml8(ar.mk_lt(ar.mk_mul(n2, x), a), m);
-    expr_ref fml9(m.mk_eq(ar.mk_mul(n2, x), a), m);
-
-    test_quant_solver(m, x.get(), fml1.get());
-    test_quant_solver(m, x.get(), fml2.get());
-    test_quant_solver(m, x.get(), fml3.get());
-    test_quant_solver(m, x.get(), fml4.get());
-    test_quant_solver(m, x.get(), fml5.get());
-    test_quant_solver(m, x.get(), fml6.get());
-    test_quant_solver(m, x.get(), fml7.get());
-    test_quant_solver(m, x.get(), fml8.get());
-    test_quant_solver(m, x.get(), fml9.get());
-
-    fml = ar.mk_lt(x2, a); test_quant_solver(m, x.get(), fml.get());
-    fml = ar.mk_gt(x2, a); test_quant_solver(m, x.get(), fml.get());
-    fml = ar.mk_le(x2, a); test_quant_solver(m, x.get(), fml.get());
-    fml = ar.mk_ge(x2, a); test_quant_solver(m, x.get(), fml.get());
-
-
-    fml = m.mk_and(ar.mk_lt(a, ar.mk_mul(n3,x)), ar.mk_lt(ar.mk_mul(n3,x), b));
-    test_quant_solver(m, x.get(), fml.get());
-
-    t1 = ar.mk_sub(ar.mk_mul(n2,y),b);
-    t2 = ar.mk_add(ar.mk_mul(n3,x),a);
-    fml1 = ar.mk_le(t1, t2);
-    t1 = ar.mk_sub(ar.mk_mul(n2,x),a);
-    t2 = ar.mk_add(ar.mk_mul(n4,y),b);
-    fml2 = ar.mk_le(t1,t2);
-    fml = m.mk_and(fml1, fml2);
-    app* xy[2] = { x.get(), y.get() };
-    test_quant_solver_rec(m, 2, xy, fml.get());
+    app_ref xr(m.mk_const(symbol("x"),i), m);
+    app_ref yr(m.mk_const(symbol("y"),i), m);
+    app* x = xr.get();
+    app* y = yr.get();
+    app* xy[2] = { x, y };
+
+
+    test_quant_solver(m, x, "(and (<= x y) (= (mod x 2) 0))");
+    test_quant_solver(m, x, "(and (<= (* 2 x) y) (= (mod x 2) 0))");
+    test_quant_solver(m, x, "(and (>= x y) (= (mod x 2) 0))");
+    test_quant_solver(m, x, "(and (>= (* 2 x) y) (= (mod x 2) 0))");
+    test_quant_solver(m, x, "(and (<= (* 2 x) y) (>= x z) (= (mod x 2) 0))");
+    test_quant_solver(m, x, "(and (<= (* 2 x) y) (>= (* 3 x) z) (= (mod x 2) 0))");
+
+    test_quant_solver(m, x, "(>= (* 2 x) a)");
+
+    test_quant_solver(m, x, "(<= (* 2 x) a)");
+    test_quant_solver(m, x, "(< (* 2 x) a)");
+    test_quant_solver(m, x, "(= (* 2 x) a)");
+    test_quant_solver(m, x, "(< (* 2 x) a)");
+    test_quant_solver(m, x, "(> (* 2 x) a)");
+
+
+    test_quant_solver(m, x, "(and (<= a x) (<= (* 2 x) b))");
+
+    test_quant_solver(m, x, "(and (<= a x) (<= x b))");
+    test_quant_solver(m, x, "(and (<= (* 2 a) x) (<= x b))");
+    test_quant_solver(m, x, "(and (<= (* 2 a) x) (<= (* 2 x) b))");
+    test_quant_solver(m, x, "(and (<= a x) (<= (* 3 x) b))");
+    test_quant_solver(m, x, "(and (<= (* 3 a) x) (<= x b))");
+    test_quant_solver(m, x, "(and (<= (* 3 a) x) (<= (* 3 x) b))");
+
+    test_quant_solver(m, x, "(and (< a (* 3 x)) (< (* 3 x) b))");    
+
+    test_quant_solver(m, x, "(< (* 3 x) a)");
+    test_quant_solver(m, x, "(= (* 3 x) a)");
+    test_quant_solver(m, x, "(< (* 3 x) a)");
+    test_quant_solver(m, x, "(> (* 3 x) a)");
+    test_quant_solver(m, x, "(<= (* 3 x) a)");
+    test_quant_solver(m, x, "(>= (* 3 x) a)");
+
+    test_quant_solver(m, x, "(<= (* 2 x) a)");
+    test_quant_solver(m, x, "(or (= (* 2 x) y) (= (+ (* 2 x) 1) y))");
+    test_quant_solver(m, x, "(= x a)");
+    test_quant_solver(m, x, "(< x a)");
+    test_quant_solver(m, x, "(> x a)");
+    test_quant_solver(m, x, "(and (> x a) (< x b))");
+    test_quant_solver(m, x, "(and (> x a) (< x b))");
+    test_quant_solver(m, x, "(<= x a)");
+    test_quant_solver(m, x, "(>= x a)");
+    test_quant_solver(m, x, "(and (<= (* 2 x) y) (= (mod x 2) 0))");
+    test_quant_solver(m, x, "(= (* 2 x) y)");
+    test_quant_solver(m, x, "(or (< x 0) (> x 1))");
+    test_quant_solver(m, x, "(or (< x y) (> x y))");
+    test_quant_solver(m, x, "(= x y)");
+    test_quant_solver(m, x, "(<= x y)");
+    test_quant_solver(m, x, "(>= x y)");
+    test_quant_solver(m, x, "(and (<= (+ x y) 0) (<= (+ x z) 0))");
+    test_quant_solver(m, x, "(and (<= (+ x y) 0) (<= (+ (* 2 x) z) 0))");
+    test_quant_solver(m, x, "(and (<= (+ (* 3 x) y) 0) (<= (+ (* 2 x) z) 0))");
+    test_quant_solver(m, x, "(and (>= x y) (>= x z))");
+    test_quant_solver(m, x, "(< x y)");
+    test_quant_solver(m, x, "(> x y)");
+
+    test_quant_solver(m, 2, xy, "(and (<= (- (* 2 y) b) (+ (* 3 x) a)) (<= (- (* 2 x) a) (+ (* 4 y) b)))");
+
 }