fill out qe_solve_plugin functionality

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

src/ast/datatype_decl_plugin.h

@@ -358,8 +358,10 @@ namespace datatype {
         bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
         bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
         bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
+        bool is_constructor(expr* e) const { return is_app(e) && is_constructor(to_app(e)); }
         bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);} 
         bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);} 
+        bool is_is(expr * e) const { return is_app(e) && is_is(to_app(e)); }
         bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
         bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
         bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }

src/qe/qe_lite.cpp

@@ -36,6 +36,7 @@ Revision History:
 #include "ast/datatype_decl_plugin.h"
 
 #include "qe/qe_vartest.h"
+#include "qe/qe_solve_plugin.h"
 
 namespace eq {
 
@@ -72,6 +73,7 @@ namespace eq {
         beta_reducer    m_subst;
         expr_ref_vector m_subst_map;
         expr_ref_vector m_new_exprs;
+        plugin_manager<qe::solve_plugin> m_solvers;
 
         ptr_vector<expr> m_map;
         int_vector       m_pos2var;
@@ -221,97 +223,6 @@ namespace eq {
             }
         }
 
-        bool is_invertible_const(bool is_int, expr* x, rational& a_val) {
-            expr* y;
-            if (a.is_uminus(x, y) && is_invertible_const(is_int, y, a_val)) {
-                a_val.neg();
-                return true;
-            }
-            else if (a.is_numeral(x, a_val) && !a_val.is_zero()) {
-                if (!is_int || a_val.is_one() || a_val.is_minus_one()) {
-                    return true;
-                }
-            }
-            return false;
-        }
-
-        bool is_invertible_mul(bool is_int, expr*& arg, rational& a_val) {
-            if (is_variable(arg)) {
-                a_val = rational(1);
-                return true;
-            }
-            expr* x, *y;
-            if (a.is_mul(arg, x, y)) {
-                if (is_variable(x) && is_invertible_const(is_int, y, a_val)) {
-                    arg = x;
-                    return true;
-                }
-                if (is_variable(y) && is_invertible_const(is_int, x, a_val)) {
-                    arg = y;
-                    return true;
-                }
-            }
-            return false;
-        }
-
-        typedef std::pair<bool,expr*> signed_expr;
-
-        expr_ref solve_arith(bool is_int, rational const& r, bool sign, svector<signed_expr> const& exprs) {
-            expr_ref_vector result(m);
-            for (unsigned i = 0; i < exprs.size(); ++i) {
-                bool sign2 = exprs[i].first;
-                expr* e    = exprs[i].second;
-                rational r2(r);
-                if (sign == sign2) {
-                    r2.neg();
-                }
-                if (!r2.is_one()) {
-                    result.push_back(a.mk_mul(a.mk_numeral(r2, is_int), e));
-                }
-                else {
-                    result.push_back(e);
-                }
-            }
-            return expr_ref(a.mk_add(result.size(), result.c_ptr()), m);
-        }
-
-        bool solve_arith(expr* lhs, expr* rhs, ptr_vector<var>& vs, expr_ref_vector& ts) {
-            if (!a.is_int(lhs) && !a.is_real(rhs)) {
-                return false;
-            }
-            rational a_val;
-            bool is_int = a.is_int(lhs);
-            svector<signed_expr> todo, done;
-            todo.push_back(std::make_pair(true,  lhs));
-            todo.push_back(std::make_pair(false, rhs));
-            while (!todo.empty()) {
-                expr* e = todo.back().second;
-                bool sign = todo.back().first;
-                todo.pop_back();
-                if (a.is_add(e)) {
-                    for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
-                        todo.push_back(std::make_pair(sign, to_app(e)->get_arg(i)));
-                    }
-                }
-                else if (is_invertible_mul(is_int, e, a_val)) {
-                    done.append(todo);
-                    vs.push_back(to_var(e));
-                    a_val = rational(1)/a_val;
-                    ts.push_back(solve_arith(is_int, a_val, sign, done));
-                    TRACE("qe_lite", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << mk_pp(ts.back(), m) << "\n";);
-                    return true;
-                }
-                else {
-                    done.push_back(std::make_pair(sign, e));
-                }
-            }
-            return false;
-        }
-
-        bool arith_solve(expr * lhs, expr * rhs, expr * eq, ptr_vector<var>& vs, expr_ref_vector& ts) {
-            return solve_arith(lhs, rhs, vs, ts);
-        }
-
         bool trivial_solve(expr* lhs, expr* rhs, expr* eq, ptr_vector<var>& vs, expr_ref_vector& ts) {
             if (!is_variable(lhs)) {
                 std::swap(lhs, rhs);
@@ -343,65 +254,25 @@ namespace eq {
         */
 
         bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
-            expr* lhs, *rhs;
+            expr* lhs = nullptr, *rhs = nullptr;
-            var* v;
 
             // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases
+            if (m.is_eq(e, lhs, rhs) && trivial_solve(lhs, rhs, e, vs, ts)) {
+                return true;
+            }
+            family_id fid = get_sort(e)->get_family_id();
             if (m.is_eq(e, lhs, rhs)) {
-                // (iff (not VAR) t) (iff t (not VAR)) cases
+                fid = get_sort(lhs)->get_family_id();
-                if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) {
+            }
-                    if (!is_neg_var(m, lhs, v)) {
+            qe::solve_plugin* p = m_solvers.get_plugin(fid);
-                        std::swap(lhs, rhs);
+            if (p) {
-                    }
+                expr_ref res = (*p)(e);
-                    if (!is_neg_var(m, lhs, v)) {
+                if (res != e && m.is_eq(res, lhs, rhs) && is_variable(lhs)) {
-                        return false;
+                    vs.push_back(to_var(lhs));
-                    }
+                    ts.push_back(rhs);
-                    vs.push_back(v);
-                    ts.push_back(m.mk_not(rhs));
-                    TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
                     return true;
                 }
-                if (trivial_solve(lhs, rhs, e, vs, ts)) {
-                    return true;
-                }
-                if (arith_solve(lhs, rhs, e, vs, ts)) {
-                    return true;
-                }
-                return false;
             }
-
-            // (ite cond (= VAR t) (= VAR t2)) case
-            expr* cond, *e2, *e3;
-            if (m.is_ite(e, cond, e2, e3)) {
-                if (is_var_eq(e2, vs, ts)) {
-                    expr_ref_vector ts2(m);
-                    ptr_vector<var> vs2;
-                    if (is_var_eq(e3, vs2, ts2) && same_vars(vs, vs2)) {
-                        for (unsigned i = 0; i < vs.size(); ++i) {
-                            ts[i] = m.mk_ite(cond, ts[i].get(), ts2[i].get());
-                        }
-                        return true;
-                    }
-                }
-                return false;
-            }
-
-            // VAR = true case
-            if (is_variable(e)) {
-                ts.push_back(m.mk_true());
-                vs.push_back(to_var(e));
-                TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
-                return true;
-            }
-
-            // VAR = false case
-            if (is_neg_var(m, e, v)) {
-                ts.push_back(m.mk_false());
-                vs.push_back(v);
-                TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
-                return true;
-            }
-
             return false;
         }
 
@@ -785,9 +656,15 @@ namespace eq {
             m_new_exprs(m),
             m_new_args(m),
             m_rewriter(m),
-            m_params(p) {}
+            m_params(p) {
+        }
 
-        void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
+        void set_is_variable_proc(is_variable_proc& proc) { 
+            m_is_variable = &proc;
+            m_solvers.reset();
+            m_solvers.register_plugin(qe::mk_arith_solve_plugin(m, proc));            
+            m_solvers.register_plugin(qe::mk_basic_solve_plugin(m, proc));            
+        }
 
         void operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
             TRACE("qe_lite", tout << mk_pp(q, m) << "\n";);

src/qe/qe_solve_plugin.cpp

@@ -19,6 +19,7 @@ Revision History:
 --*/
 
 #include "ast/arith_decl_plugin.h"
+#include "ast/datatype_decl_plugin.h"
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "qe/qe_solve_plugin.h"
@@ -65,7 +66,7 @@ namespace qe {
         /**
          * \brief return true if lhs = rhs can be solved as v = t, where v is a variable.
          */
-        bool solve_arith(expr* lhs, expr* rhs, expr_ref& v, expr_ref& t) {
+        bool solve(expr* lhs, expr* rhs, expr_ref& v, expr_ref& t) {
             if (!a.is_int(lhs) && !a.is_real(rhs)) {
                 return false;
             }
@@ -83,6 +84,16 @@ namespace qe {
                         todo.push_back(std::make_pair(sign, e));
                     }
                 }
+                else if (a.is_sub(e)) {
+                    app* sub = to_app(e);
+                    todo.push_back(std::make_pair(sign, sub->get_arg(0)));
+                    for (unsigned i = 1; i < sub->get_num_args(); ++i) {
+                        todo.push_back(std::make_pair(!sign, sub->get_arg(i)));
+                    }
+                }
+                else if (a.is_uminus(e)) {
+                    todo.push_back(std::make_pair(!sign, to_app(e)->get_arg(0)));
+                }
                 else if (is_invertible_mul(is_int, e, a_val)) {
                     done.append(todo);
                     v = e;
@@ -98,7 +109,7 @@ namespace qe {
             return false;
         }
 
-        // can we solve for a variable by ...
+        // is x a constant and can we safely divide by x to solve for a variable?
         bool is_invertible_const(bool is_int, expr* x, rational& a_val) {
             expr* y;
             if (a.is_uminus(x, y) && is_invertible_const(is_int, y, a_val)) {
@@ -113,6 +124,8 @@ namespace qe {
             return false;
         }
 
+        // is arg of the form a_val * v, where a_val 
+        // is a constant that we can safely divide by.
         bool is_invertible_mul(bool is_int, expr*& arg, rational& a_val) {
             if (is_variable(arg)) {
                 a_val = rational(1);
@@ -133,10 +146,11 @@ namespace qe {
         }
         
 
-        expr_ref mk_eq_core (expr *_e1, expr *_e2) {
+        expr_ref mk_eq_core (expr *e1, expr *e2) {            
-            expr *e1, *e2;
+            expr_ref v(m), t(m);
-            e1 = _e1;
+            if (solve(e1, e2, v, t)) {
-            e2 = _e2;
+                return expr_ref(m.mk_eq(v, t), m);
+            }
 
             if (a.is_zero(e1)) {
                 std::swap(e1, e2);
@@ -257,6 +271,90 @@ namespace qe {
         }
     };
 
+    class basic_solve_plugin : public solve_plugin {
+    public:
+        basic_solve_plugin(ast_manager& m, is_variable_proc& is_var): 
+            solve_plugin(m, m.get_basic_family_id(), is_var) {}
+
+        expr_ref solve(expr *atom, bool is_pos) override {
+            expr_ref res(atom, m);
+            expr* lhs = nullptr, *rhs = nullptr, *n = nullptr;
+            if (m.is_eq(atom, lhs, rhs)) {
+                if (m.is_not(lhs, n) && is_variable(n)) {
+                    res = m.mk_eq(n, mk_not(m, rhs));
+                }
+                else if (m.is_not(rhs, n) && is_variable(n)) {
+                    res = m.mk_eq(n, mk_not(m, lhs));
+                }
+                else if (is_variable(rhs) && !is_variable(lhs)) {
+                    res = m.mk_eq(rhs, lhs);
+                } 
+            }
+            // (ite cond (= VAR t) (= VAR t2)) case
+            expr* cond = nullptr, *th = nullptr, *el = nullptr;
+            if (m.is_ite(atom, cond, th, el)) {
+                expr_ref r1 = solve(th, true);
+                expr_ref r2 = solve(el, true);
+                expr* v1 = nullptr, *t1 = nullptr, *v2 = nullptr, *t2 = nullptr;
+                if (m.is_eq(r1, v1, t1) && m.is_eq(r2, v2, t2) && v1 == v2) { 
+                    res = m.mk_eq(v1, m.mk_ite(cond, t1, t2));
+                }
+            }
+
+            if (is_variable(atom) && m.is_bool(atom)) {
+                res = m.mk_eq(atom, m.mk_bool_val(is_pos));
+                return res;
+            }
+
+            return is_pos ? res : mk_not(res);
+        }
+    };
+
+    class dt_solve_plugin : public solve_plugin {
+        datatype_util dt;
+    public:
+        dt_solve_plugin(ast_manager& m, is_variable_proc& is_var): 
+            solve_plugin(m, m.get_family_id("datatype"), is_var), 
+            dt(m) {}
+
+        expr_ref solve(expr *atom, bool is_pos) override {
+            expr_ref res(atom, m);
+            expr* lhs = nullptr, *rhs = nullptr;
+            if (m.is_eq(atom, lhs, rhs)) {
+                if (dt.is_constructor(rhs)) {
+                    std::swap(lhs, rhs);
+                }
+                if (dt.is_constructor(lhs) && dt.is_constructor(rhs)) {
+                    app* l = to_app(lhs), *r = to_app(rhs);
+                    if (l->get_decl() == r->get_decl()) {
+                        expr_ref_vector eqs(m);
+                        for (unsigned i = 0, sz = l->get_num_args(); i < sz; ++i) {
+                            eqs.push_back(m.mk_eq(l->get_arg(i), r->get_arg(i)));
+                        }
+                        res = mk_and(eqs);
+                    }
+                    else {
+                        res = m.mk_false();
+                    }
+                }
+                else if (dt.is_constructor(lhs)) {
+                    app* l = to_app(lhs);
+                    func_decl* d = l->get_decl();
+                    expr_ref_vector conjs(m);
+                    conjs.push_back(dt.mk_is(d, rhs));
+                    ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d);
+                    for (unsigned i = 0; i < acc.size(); ++i) {
+                        conjs.push_back(m.mk_eq(l->get_arg(i), m.mk_app(acc[i], rhs)));
+                    }
+                    res = mk_and(conjs);
+                }
+            }
+            // TBD: can also solve for is_nil(x) by x = nil
+            // 
+            return is_pos ? res : mk_not(res);
+        }
+    };
+    
     class bv_solve_plugin : public solve_plugin {
     public:
         bv_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("bv"), is_var) {}
@@ -266,15 +364,6 @@ namespace qe {
         }
     };
 
-    class dt_solve_plugin : public solve_plugin {
-    public:
-        dt_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("dt"), is_var) {}
-        expr_ref solve(expr *atom, bool is_pos) override {
-            expr_ref res(atom, m);
-            return is_pos ? res : mk_not(res);
-        }
-    };
-    
     class array_solve_plugin : public solve_plugin {
     public:
         array_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("array"), is_var) {}
@@ -284,6 +373,9 @@ namespace qe {
         }
     };
 
+    solve_plugin* mk_basic_solve_plugin(ast_manager& m, is_variable_proc& is_var) {
+        return alloc(basic_solve_plugin, m, is_var);
+    }
 
     solve_plugin* mk_arith_solve_plugin(ast_manager& m, is_variable_proc& is_var) {
         return alloc(arith_solve_plugin, m, is_var);
@@ -293,6 +385,7 @@ namespace qe {
         return alloc(dt_solve_plugin, m, is_var);
     }
 
+#if 0
     solve_plugin* mk_bv_solve_plugin(ast_manager& m, is_variable_proc& is_var) {
         return alloc(bv_solve_plugin, m, is_var);
     }
@@ -300,4 +393,6 @@ namespace qe {
     solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var) {
         return alloc(array_solve_plugin, m, is_var);
     }
+#endif
+
 }

src/qe/qe_solve_plugin.h

@@ -42,11 +42,13 @@ namespace qe {
         expr_ref operator() (expr *lit);
     };
 
+    solve_plugin* mk_basic_solve_plugin(ast_manager& m, is_variable_proc& is_var);
+
     solve_plugin* mk_arith_solve_plugin(ast_manager& m, is_variable_proc& is_var);
 
     solve_plugin* mk_dt_solve_plugin(ast_manager& m, is_variable_proc& is_var);
 
-    solve_plugin* mk_bv_solve_plugin(ast_manager& m, is_variable_proc& is_var);
+    // solve_plugin* mk_bv_solve_plugin(ast_manager& m, is_variable_proc& is_var);
 
-    solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var);
+    // solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var);
 }

src/util/plugin_manager.h

@@ -27,7 +27,12 @@ class plugin_manager {
     ptr_vector<Plugin>   m_plugins;
 public:
     ~plugin_manager() {
+        reset();
+    }
+
+    void reset() {
         std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<Plugin>());
+        release();
     }
 
     /**