one must answer the call of the master of compilers #2258

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

src/ast/seq_decl_plugin.cpp

@@ -906,12 +906,18 @@ bool seq_decl_plugin::is_value(app* e) const {
             m_manager->is_value(e->get_arg(0))) {
             return true;
         }
-        if (is_app_of(e, m_family_id, OP_SEQ_CONCAT) &&
+        if (is_app_of(e, m_family_id, OP_SEQ_CONCAT)) {
-            e->get_num_args() == 2 && 
+            bool first = true;
-            is_app(e->get_arg(0)) &&
+            for (expr* arg : *e) {
-            is_app(e->get_arg(1)) &&
+                if (first) {
-            is_value(to_app(e->get_arg(0)))) {
+                    first = false;
-            e = to_app(e->get_arg(1));
+                }
+                else if (is_app(arg) && !is_value(to_app(arg))) {
+                    return false;
+                }
+            }
+            if (!is_app(e->get_arg(0))) return false;            
+            e = to_app(e->get_arg(0));
             continue;
         }
         return false;

src/qe/qe_lite.cpp

@@ -69,6 +69,7 @@ namespace eq {
         ast_manager &   m;
         arith_util      a;
         datatype_util   dt;
+        bv_util         bv;
         is_variable_proc* m_is_variable;
         beta_reducer    m_subst;
         expr_ref_vector m_subst_map;
@@ -84,6 +85,37 @@ namespace eq {
         th_rewriter      m_rewriter;
         params_ref       m_params;
 
+        bool is_sub_extract(unsigned idx, expr* t) {
+            bool has_ground = false;            
+            if (bv.is_concat(t)) {
+                unsigned lo, hi;
+                ptr_buffer<expr> args;
+                args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
+                for (unsigned i = 0; i < args.size(); ++i) {
+                    expr* arg = args[i];
+                    if (is_ground(arg)) {
+                        has_ground = true;
+                        continue;
+                    }
+                    if (bv.is_extract(arg, lo, hi, arg)) {
+                        if (is_var(arg) && to_var(arg)->get_idx() == idx) 
+                            continue;
+                    }
+                    if (bv.is_concat(arg)) {
+                        args.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
+                        continue;
+                    }
+                    return false;
+                }
+                return has_ground;
+            }
+            return false;
+        }
+
+        bool strict_occurs_var(unsigned idx, expr* t) {
+            return occurs_var(idx, t) && !is_sub_extract(idx, t);
+        }
+
         void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
             order.reset();
 
@@ -92,7 +124,7 @@ namespace eq {
             for (unsigned i = 0; i < definitions.size(); i++) {
                 var * v  = vars[i];
                 expr * t = definitions[i];
-                if (t == nullptr || has_quantifiers(t) || occurs_var(v->get_idx(), t))
+                if (t == nullptr || has_quantifiers(t) || strict_occurs_var(v->get_idx(), t))
                     definitions[i] = nullptr;
                 else
                     found = true; // found at least one candidate
@@ -112,6 +144,10 @@ namespace eq {
             for (unsigned i = 0; i < definitions.size(); i++) {
                 if (definitions[i] == nullptr)
                     continue;
+                if (is_sub_extract(vars[i]->get_idx(), definitions[i])) {
+                    order.push_back(i);
+                    continue;
+                }
                 var * v = vars[i];
                 SASSERT(v->get_idx() == i);
                 SASSERT(todo.empty());
@@ -255,6 +291,7 @@ namespace eq {
 
         bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
             expr* lhs = nullptr, *rhs = nullptr;
+            TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
 
             // (= 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)) {
@@ -270,6 +307,7 @@ namespace eq {
                 if (res != e && m.is_eq(res, lhs, rhs) && is_variable(lhs)) {
                     vs.push_back(to_var(lhs));
                     ts.push_back(rhs);
+                    TRACE("qe_lite", tout << res << "\n";);
                     return true;
                 }
             }
@@ -314,7 +352,8 @@ namespace eq {
                 expr_ref r(m);
                 if (is_ground(cur)) r = cur; else m_subst(cur, r);
                 unsigned inx = sz - idx - 1;
-                CTRACE("topo_sort", m_subst_map.get(inx) != nullptr,
+                TRACE("qe_lite", tout << idx << " |-> " << r << "\n";);
+                CTRACE("top_sort", m_subst_map.get(inx) != nullptr,
                        tout << "inx is " << inx << "\n"
                        << "idx is " << idx << "\n"
                        << "sz is " << sz << "\n"
@@ -368,6 +407,7 @@ namespace eq {
                 break;
             }
             expr_ref new_e = m_subst(t, m_subst_map.size(), m_subst_map.c_ptr());
+            TRACE("qe_lite", tout << new_e << "\n";);
 
             // don't forget to update the quantifier patterns
             expr_ref_buffer  new_patterns(m);
@@ -657,6 +697,7 @@ namespace eq {
             m(m),
             a(m),
             dt(m),
+            bv(m),
             m_is_variable(nullptr),
             m_subst(m),
             m_subst_map(m),
@@ -671,6 +712,7 @@ namespace eq {
             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));            
+            m_solvers.register_plugin(qe::mk_bv_solve_plugin(m, proc));            
         }
 
         void operator()(quantifier * q, expr_ref & r, proof_ref & pr) {

src/qe/qe_solve_plugin.cpp

@@ -19,6 +19,7 @@ Revision History:
 --*/
 
 #include "ast/arith_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
@@ -359,10 +360,46 @@ namespace qe {
     };
 
     class bv_solve_plugin : public solve_plugin {
+        bv_util m_bv;
+        bool solve_eq(expr*& lhs, expr*& rhs) {
+            unsigned lo, hi;
+            expr* e = nullptr;
+            if (m_bv.is_extract(lhs, lo, hi, e) && is_variable(e)) {
+                lhs = e;
+                unsigned sz = m_bv.get_bv_size(e);
+                if (lo > 0 && hi + 1 < sz) {
+                    expr* args[3] = { m_bv.mk_extract(sz-1, hi + 1, e), rhs, m_bv.mk_extract(lo - 1, 0, e)};
+                    rhs = m_bv.mk_concat(3, args);
+                }
+                else if (lo == 0 && hi + 1 < sz) {
+                    expr* args[2] = { m_bv.mk_extract(sz-1, hi + 1, e), rhs };
+                    rhs = m_bv.mk_concat(2, args);
+                }
+                else if (lo > 0 && hi + 1 == sz) {
+                    expr* args[3] = { rhs, m_bv.mk_extract(lo - 1, 0, e) };
+                    rhs = m_bv.mk_concat(2, args);                    
+                }
+                else {
+                    return false;
+                }
+                return true;
+            }
+            return false;
+        }
     public:
-        bv_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("bv"), is_var) {}
+        bv_solve_plugin(ast_manager& m, is_variable_proc& is_var): 
+            solve_plugin(m, m.get_family_id("bv"), is_var), m_bv(m) {}
         expr_ref solve(expr *atom, bool is_pos) override {
             expr_ref res(atom, m);
+            expr* lhs = nullptr, *rhs = nullptr;
+            if (is_pos && m.is_eq(atom, lhs, rhs) && solve_eq(lhs, rhs)) {
+                res = m.mk_eq(lhs, rhs);
+                return res;
+            }
+            if (is_pos && m.is_eq(atom, lhs, rhs) && solve_eq(rhs, lhs)) {
+                res = m.mk_eq(rhs, lhs);
+                return res;
+            }
             return is_pos ? res : mk_not(res);
         }
     };
@@ -388,11 +425,11 @@ 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);
     }
 
+#if 0
     solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var) {
         return alloc(array_solve_plugin, m, is_var);
     }

src/qe/qe_solve_plugin.h

@@ -48,7 +48,7 @@ namespace qe {
 
     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);
 }