Merge remote-tracking branch 'upstream/master'

src/api/python/z3/z3.py

@@ -6470,7 +6470,7 @@ class Solver(Z3PPObject):
             self.solver = solver
         Z3_solver_inc_ref(self.ctx.ref(), self.solver)
         if logFile is not None:
-            self.set("solver.smtlib2_log", logFile)
+            self.set("smtlib2_log", logFile)
 
     def __del__(self):
         if self.solver is not None and self.ctx.ref() is not None:

src/ast/rewriter/arith_rewriter.cpp

@@ -345,7 +345,7 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp
                 continue;
             eqs.push_back(m().mk_eq(arg, zero));
         }
-        result = m().mk_and(eqs);
+        result = m().mk_or(eqs);
         return BR_REWRITE2;
     }
 

src/ast/rewriter/seq_rewriter.cpp

@@ -2151,6 +2151,15 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
     return re_and(cond, re_with_empty);
 }
 
+expr_ref seq_rewriter::is_nullable_rec(expr* r) {
+    expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr), m());
+    if (!result) {
+        result = is_nullable(r);
+        m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, result);        
+    }
+    return result;
+}
+
 expr_ref seq_rewriter::is_nullable(expr* r) {
     SASSERT(m_util.is_re(r));
     expr* r1 = nullptr, *r2 = nullptr, *cond = nullptr;
@@ -2158,14 +2167,14 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
     expr_ref result(m());
     if (re().is_concat(r, r1, r2) ||
         re().is_intersection(r, r1, r2)) {
-        result = mk_and(m(), is_nullable(r1), is_nullable(r2));
+        result = mk_and(m(), is_nullable_rec(r1), is_nullable_rec(r2));
     }
     else if (re().is_union(r, r1, r2)) {
-        result = mk_or(m(), is_nullable(r1), is_nullable(r2));
+        result = mk_or(m(), is_nullable_rec(r1), is_nullable_rec(r2));
     }
     else if (re().is_diff(r, r1, r2)) {
-        result = mk_not(m(), is_nullable(r2));
+        result = mk_not(m(), is_nullable_rec(r2));
-        result = mk_and(m(), is_nullable(r1), result);
+        result = mk_and(m(), is_nullable_rec(r1), result);
     }
     else if (re().is_star(r) || 
         re().is_opt(r) ||
@@ -2184,10 +2193,10 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
         (re().is_loop(r, r1, lo) && lo > 0) ||
         (re().is_loop(r, r1, lo, hi) && lo > 0) ||
         (re().is_reverse(r, r1))) {
-        result = is_nullable(r1);
+        result = is_nullable_rec(r1);
     }
     else if (re().is_complement(r, r1)) {
-        result = mk_not(m(), is_nullable(r1));
+        result = mk_not(m(), is_nullable_rec(r1));
     }
     else if (re().is_to_re(r, r1)) {
         sort* seq_sort = nullptr;
@@ -2196,7 +2205,7 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
         result = m().mk_eq(emptystr, r1);
     }
     else if (m().is_ite(r, cond, r1, r2)) {
-        result = m().mk_ite(cond, is_nullable(r1), is_nullable(r2));
+        result = m().mk_ite(cond, is_nullable_rec(r1), is_nullable_rec(r2));
     }
     else {
         sort* seq_sort = nullptr;
@@ -4017,3 +4026,29 @@ bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs,
     }
     return true;
 } 
+
+seq_rewriter::op_cache::op_cache(ast_manager& m):
+    m(m),
+    m_trail(m)
+{}
+
+expr* seq_rewriter::op_cache::find(decl_kind op, expr* a, expr* b) {
+    op_entry e(op, a, b, nullptr);
+    m_table.find(e);
+    return e.r;
+}
+
+void seq_rewriter::op_cache::insert(decl_kind op, expr* a, expr* b, expr* r) {
+    cleanup();
+    if (a) m_trail.push_back(a);
+    if (b) m_trail.push_back(b);
+    if (r) m_trail.push_back(r);
+    m_table.insert(op_entry(op, a, b, r));
+}
+
+void seq_rewriter::op_cache::cleanup() {
+    if (m_table.size() >= m_max_cache_size) {
+        m_trail.reset();
+        m_table.reset();
+    }
+}

src/ast/rewriter/seq_rewriter.h

@@ -114,9 +114,45 @@ public:
    \brief Cheap rewrite rules for seq constraints
 */
 class seq_rewriter {
+
+    class op_cache {
+        struct op_entry {
+            decl_kind k;
+            expr* a, *b, *r;
+            op_entry(decl_kind k, expr* a, expr* b, expr* r): k(k), a(a), b(b), r(r) {}
+            op_entry():k(0), a(nullptr), b(nullptr), r(nullptr) {}
+        };
+
+        struct hash_entry {
+            unsigned operator()(op_entry const& e) const { 
+                return mk_mix(e.k, e.a ? e.a->get_id() : 0, e.b ? e.b->get_id() : 0);
+            }
+        };
+
+        struct eq_entry {
+            bool operator()(op_entry const& a, op_entry const& b) const { 
+                return a.k == b.k && a.a == b.a && a.b == b.b;
+            }
+        };
+
+        typedef hashtable<op_entry, hash_entry, eq_entry> op_table;
+
+        ast_manager&    m;
+        unsigned        m_max_cache_size { 10000 };
+        expr_ref_vector m_trail;
+        op_table        m_table;
+        void cleanup();
+
+    public:
+        op_cache(ast_manager& m);
+        expr* find(decl_kind op, expr* a, expr* b);
+        void insert(decl_kind op, expr* a, expr* b, expr* r);
+    };
+
     seq_util       m_util;
     arith_util     m_autil;
     re2automaton   m_re2aut;
+    op_cache       m_op_cache;
     expr_ref_vector m_es, m_lhs, m_rhs;
     bool           m_coalesce_chars;    
 
@@ -127,6 +163,8 @@ class seq_rewriter {
         unknown_c
     };
 
+
+
     length_comparison compare_lengths(expr_ref_vector const& as, expr_ref_vector const& bs) {
         return compare_lengths(as.size(), as.c_ptr(), bs.size(), bs.c_ptr());
     }
@@ -231,7 +269,7 @@ class seq_rewriter {
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
+        m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
@@ -273,6 +311,7 @@ public:
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
 
     expr_ref is_nullable(expr* r);
+    expr_ref is_nullable_rec(expr* r);
 
     bool has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el);
 

src/ast/seq_decl_plugin.h

@@ -108,6 +108,7 @@ enum seq_op_kind {
     _OP_STRING_STRIDOF,
     _OP_REGEXP_EMPTY,
     _OP_REGEXP_FULL_CHAR,
+    _OP_RE_IS_NULLABLE,
     _OP_SEQ_SKOLEM,
     LAST_SEQ_OP
 };

src/math/lp/CMakeLists.txt

@@ -2,7 +2,6 @@ z3_add_component(lp
   SOURCES
     binary_heap_priority_queue.cpp
     binary_heap_upair_queue.cpp
-    lp_bound_propagator.cpp
     core_solver_pretty_printer.cpp
     dense_matrix.cpp
     eta_matrix.cpp

src/math/lp/bound_analyzer_on_row.h

@@ -24,14 +24,13 @@ Revision History:
 
 #include "util/vector.h"
 #include "math/lp/implied_bound.h"
-#include "math/lp/lp_bound_propagator.h"
 #include "math/lp/test_bound_analyzer.h"
 
 namespace lp {
-template <typename C> // C plays a role of a container
+template <typename C, typename B> // C plays a role of a container, B - lp_bound_propagator
 class bound_analyzer_on_row {
     const C&                           m_row;
-    lp_bound_propagator &              m_bp;
+    B &                                m_bp;
     unsigned                           m_row_or_term_index;
     int                                m_column_of_u; // index of an unlimited from above monoid
     // -1 means that such a value is not found, -2 means that at least two of such monoids were found
@@ -45,7 +44,7 @@ public :
         unsigned  bj, // basis column for the row
         const numeric_pair<mpq>& rs,
         unsigned row_or_term_index,
-        lp_bound_propagator & bp)
+        B & bp)
         :
         m_row(it),
         m_bp(bp),
@@ -55,11 +54,12 @@ public :
         m_rs(rs)
     {}
 
+    
     static void analyze_row(const C & row,
                             unsigned bj, // basis column for the row
                             const numeric_pair<mpq>& rs,
                             unsigned row_or_term_index,
-                            lp_bound_propagator & bp) {
+                            B & bp) {
         bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
         a.analyze();
         // TBD: a.analyze_eq();

src/math/lp/lar_solver.cpp

@@ -136,23 +136,6 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
 }
 
 
-void lar_solver::analyze_new_bounds_on_row(
-    unsigned row_index,
-    lp_bound_propagator & bp) {
-    lp_assert(!use_tableau());
-    unsigned j =  m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row
-
-    
-    bound_analyzer_on_row<indexed_vector<mpq>>::analyze_row(
-        m_mpq_lar_core_solver.get_pivot_row(),
-        j,
-        zero_of_type<numeric_pair<mpq>>(),
-        row_index,
-        bp
-                                                            );
-//    ra_pos.analyze();
-}
-
 bool lar_solver::row_has_a_big_num(unsigned i) const {
     for (const auto& c : A_r().m_rows[i]) {
         if (c.coeff().is_big())
@@ -161,23 +144,6 @@ bool lar_solver::row_has_a_big_num(unsigned i) const {
     return false;
 }
 
-void lar_solver::analyze_new_bounds_on_row_tableau(
-    unsigned row_index,
-    lp_bound_propagator & bp ) {
-
-    if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation
-        || row_has_a_big_num(row_index))
-        return;
-    lp_assert(use_tableau());
-
-    bound_analyzer_on_row<row_strip<mpq>>::analyze_row(A_r().m_rows[row_index],
-                                       null_ci,
-                                       zero_of_type<numeric_pair<mpq>>(),
-                                       row_index,
-                                       bp
-                                       );
-}
-
     
 void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) {
     // todo : create a map from term basic vars to the rows where they are used
@@ -191,16 +157,6 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) {
     }
 }
 
-void lar_solver::calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp) {
-    if (use_tableau()) {
-        analyze_new_bounds_on_row_tableau(i, bp);
-    } else {
-        m_mpq_lar_core_solver.calculate_pivot_row(i);
-        substitute_basis_var_in_terms_for_row(i);
-        analyze_new_bounds_on_row(i, bp);
-    }
-}
-
 unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const {
     if (!tv::is_term(j)) {
         unsigned ext_var_or_term = m_var_register.local_to_external(j);
@@ -214,64 +170,12 @@ unsigned lar_solver::map_term_index_to_column_index(unsigned j) const {
     return m_var_register.external_to_local(j);
 }
 
-void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset) {
-    lp_assert(false); // not implemented
-}
-
-
-void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) {
-    unsigned i = ib.m_row_or_term_index;
-    int bound_sign = ib.m_is_lower_bound? 1: -1;
-    int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
-    unsigned bound_j = ib.m_j;
-    if (tv::is_term(bound_j)) {
-        bound_j = m_var_register.external_to_local(bound_j);
-    }
-    for (auto const& r : A_r().m_rows[i]) {
-        unsigned j = r.var();
-        if (j == bound_j) continue;
-        mpq const& a = r.coeff();
-        int a_sign = is_pos(a)? 1: -1;
-        int sign = j_sign * a_sign;
-        const ul_pair & ul =  m_columns_to_ul_pairs[j];
-        auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
-        lp_assert(is_valid(witness));
-        bp.consume(a, witness);
-    }
-    // lp_assert(implied_bound_is_correctly_explained(ib, explanation));
-}
-
 // here i is just the term index
 bool lar_solver::term_is_used_as_row(unsigned i) const {
     SASSERT(i < m_terms.size());
     return m_var_register.external_is_used(tv::mask_term(i));
 }
 
-void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) {
-    for (unsigned i = 0; i < m_terms.size(); i++) {
-        if (term_is_used_as_row(i))
-            continue; // this term is used a left side of a constraint,
-        // it was processed as a touched row if needed
-        propagate_bounds_on_a_term(*m_terms[i], bp, i);
-    }
-}
-
-// goes over touched rows and tries to induce bounds
-void lar_solver::propagate_bounds_for_touched_rows(lp_bound_propagator & bp) {
-    if (!use_tableau())
-        return; // todo: consider to remove the restriction
-    
-    for (unsigned i : m_rows_with_changed_bounds) {
-        calculate_implied_bounds_for_row(i, bp);
-        if (settings().get_cancel_flag())
-            return;
-    }
-    m_rows_with_changed_bounds.clear();
-    if (!use_tableau()) {
-        propagate_bounds_on_terms(bp);
-    }
-}
-
 lp_status lar_solver::get_status() const { return m_status; }
 
 void lar_solver::set_status(lp_status s) { m_status = s; }

src/math/lp/lar_solver.h

@@ -41,8 +41,8 @@
 #include "math/lp/conversion_helper.h"
 #include "math/lp/int_solver.h"
 #include "math/lp/nra_solver.h"
-#include "math/lp/lp_bound_propagator.h"
 #include "math/lp/lp_types.h"
+#include "math/lp/lp_bound_propagator.h"
 
 namespace lp {
 
@@ -161,15 +161,53 @@ class lar_solver : public column_namer {
     bool use_lu() const;
     bool sizes_are_correct() const;
     bool implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const;
+    template <typename T>
     void analyze_new_bounds_on_row(
         unsigned row_index,
-        lp_bound_propagator & bp);
+        lp_bound_propagator<T>& bp) {
+        lp_assert(!use_tableau());
+        unsigned j =  m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row
+        bound_analyzer_on_row<indexed_vector<mpq>, lp_bound_propagator<T>>::analyze_row(
+            m_mpq_lar_core_solver.get_pivot_row(),
+            j,
+            zero_of_type<numeric_pair<mpq>>(),
+            row_index,
+            bp);
+    }
+
+    template <typename T>
     void analyze_new_bounds_on_row_tableau(
         unsigned row_index,
-        lp_bound_propagator & bp);
+        lp_bound_propagator<T> & bp ) {
+        
+        if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation
+            || row_has_a_big_num(row_index))
+            return;
+        lp_assert(use_tableau());
+        
+        bound_analyzer_on_row<row_strip<mpq>, lp_bound_propagator<T>>::analyze_row(A_r().m_rows[row_index],
+                                                                                   null_ci,
+                                                                                   zero_of_type<numeric_pair<mpq>>(),
+                                                                                   row_index,
+                                                                                   bp
+                                                                                   );
+    }
+
     void substitute_basis_var_in_terms_for_row(unsigned i);
-    void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp);    
+    template <typename T>
-    void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset);
+    void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator<T> & bp) {
+        if (use_tableau()) {
+            analyze_new_bounds_on_row_tableau(i, bp);
+        } else {
+            m_mpq_lar_core_solver.calculate_pivot_row(i);
+            substitute_basis_var_in_terms_for_row(i);
+            analyze_new_bounds_on_row(i, bp);
+        }
+    }
+    template <typename T>
+    void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator<T> & bp, unsigned term_offset) {
+        NOT_IMPLEMENTED_YET();
+    }
     static void clean_popped_elements(unsigned n, u_set& set);
     static void shrink_inf_set_after_pop(unsigned n, u_set & set);
     bool maximize_term_on_tableau(const lar_term & term,
@@ -282,12 +320,55 @@ public:
     void get_infeasibility_explanation(explanation &) const;
     inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; }
     inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
-    void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp);
+    template <typename T>
+    void explain_implied_bound(implied_bound & ib, lp_bound_propagator<T> & bp) {
+        unsigned i = ib.m_row_or_term_index;
+        int bound_sign = ib.m_is_lower_bound? 1: -1;
+        int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
+        unsigned bound_j = ib.m_j;
+        if (tv::is_term(bound_j)) {
+            bound_j = m_var_register.external_to_local(bound_j);
+        }
+        for (auto const& r : A_r().m_rows[i]) {
+            unsigned j = r.var();
+            if (j == bound_j) continue;
+            mpq const& a = r.coeff();
+            int a_sign = is_pos(a)? 1: -1;
+            int sign = j_sign * a_sign;
+            const ul_pair & ul =  m_columns_to_ul_pairs[j];
+            auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
+            lp_assert(is_valid(witness));
+            bp.consume(a, witness);
+        }
+    }
+    // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
     constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side);
     void activate(constraint_index ci);
     void random_update(unsigned sz, var_index const * vars);
-    void propagate_bounds_on_terms(lp_bound_propagator & bp);
+    template <typename T>
-    void propagate_bounds_for_touched_rows(lp_bound_propagator & bp);    
+    void propagate_bounds_on_terms(lp_bound_propagator<T> & bp) {
+        for (unsigned i = 0; i < m_terms.size(); i++) {
+            if (term_is_used_as_row(i))
+                continue; // this term is used a left side of a constraint,
+            // it was processed as a touched row if needed
+            propagate_bounds_on_a_term(*m_terms[i], bp, i);
+        }
+    }
+    template <typename T>
+    void propagate_bounds_for_touched_rows(lp_bound_propagator<T> & bp) {
+        if (!use_tableau())
+            return; // todo: consider to remove the restriction
+        
+        for (unsigned i : m_rows_with_changed_bounds) {
+            calculate_implied_bounds_for_row(i, bp);
+            if (settings().get_cancel_flag())
+                return;
+        }
+        m_rows_with_changed_bounds.clear();
+        if (!use_tableau()) {
+            propagate_bounds_on_terms(bp);
+        }
+    }
     bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
     inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
     bool external_is_used(unsigned) const;

src/math/lp/lp_bound_propagator.cpp

@@ -1,54 +0,0 @@
-/*
-  Copyright (c) 2017 Microsoft Corporation
-  Author: Lev Nachmanson
-*/
-#include "math/lp/lar_solver.h"
-namespace lp {
-lp_bound_propagator::lp_bound_propagator(lar_solver & ls):
-    m_lar_solver(ls) {}
-column_type lp_bound_propagator::get_column_type(unsigned j) const {
-    return m_lar_solver.get_column_type(j);
-}
-const impq & lp_bound_propagator::get_lower_bound(unsigned j) const {
-    return m_lar_solver.get_lower_bound(j);
-}
-const impq & lp_bound_propagator::get_upper_bound(unsigned j) const {
-    return m_lar_solver.get_upper_bound(j);
-}
-void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
-    j = m_lar_solver.adjust_column_index_to_term_index(j);    
-
-    lconstraint_kind kind = is_low? GE : LE;
-    if (strict)
-        kind = static_cast<lconstraint_kind>(kind / 2);
-    
-    if (!bound_is_interesting(j, kind, v))
-        return;
-     unsigned k; // index to ibounds
-     if (is_low) {
-         if (try_get_value(m_improved_lower_bounds, j, k)) {
-             auto & found_bound = m_ibounds[k];
-             if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) {
-                 found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
-                 TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout););
-             }
-         } else {
-             m_improved_lower_bounds[j] = m_ibounds.size();
-             m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
-             TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout););
-         }
-     } else { // the upper bound case
-         if (try_get_value(m_improved_upper_bounds, j, k)) {
-             auto & found_bound = m_ibounds[k];
-             if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) {
-                 found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
-                 TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout););
-             }
-         } else {
-             m_improved_upper_bounds[j] = m_ibounds.size();
-             m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
-             TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout););
-        }
-     }
-}
-}

src/math/lp/lp_bound_propagator.h

@@ -5,24 +5,65 @@
 #pragma once
 #include "math/lp/lp_settings.h"
 namespace lp {
-class lar_solver;
+template <typename T>
 class lp_bound_propagator {
     std::unordered_map<unsigned, unsigned> m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds
     std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
-    lar_solver & m_lar_solver;
+    T& m_imp;
 public:
     vector<implied_bound> m_ibounds;
-public:
+    lp_bound_propagator(T& imp): m_imp(imp) {}
-    lp_bound_propagator(lar_solver & ls);
+    column_type get_column_type(unsigned j) const {
-    column_type get_column_type(unsigned) const;
+        return m_imp.lp().get_column_type(j);
-    const impq & get_lower_bound(unsigned) const;
+    }
-    const impq & get_upper_bound(unsigned) const;
+    
-    void try_add_bound(mpq const & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict);
+    const impq & get_lower_bound(unsigned j) const {
-    void try_add_eq(lpvar x, lpvar y, unsigned row_or_term_index) {} // TBD
+        return m_imp.lp().get_lower_bound(j);
-    virtual bool bound_is_interesting(unsigned vi,
+    }
-                                      lp::lconstraint_kind kind,
+
-                                      const rational & bval) {return true;}
+    const impq & get_upper_bound(unsigned j) const {
-    unsigned number_of_found_bounds() const { return m_ibounds.size(); }
+        return m_imp.lp().get_upper_bound(j);
-    virtual void consume(mpq const& v, lp::constraint_index j) = 0;
+    }
+    
+    void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
+        j = m_imp.lp().adjust_column_index_to_term_index(j);    
+
+        lconstraint_kind kind = is_low? GE : LE;
+        if (strict)
+            kind = static_cast<lconstraint_kind>(kind / 2);
+    
+        if (!m_imp.bound_is_interesting(j, kind, v))
+            return;
+        unsigned k; // index to ibounds
+        if (is_low) {
+            if (try_get_value(m_improved_lower_bounds, j, k)) {
+                auto & found_bound = m_ibounds[k];
+                if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) {
+                    found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
+                    TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
+                }
+            } else {
+                m_improved_lower_bounds[j] = m_ibounds.size();
+                m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
+                TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
+            }
+        } else { // the upper bound case
+            if (try_get_value(m_improved_upper_bounds, j, k)) {
+                auto & found_bound = m_ibounds[k];
+                if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) {
+                    found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
+                    TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
+                }
+            } else {
+                m_improved_upper_bounds[j] = m_ibounds.size();
+                m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
+                TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
+            }
+        }
+    }
+
+    void consume(const mpq& a, constraint_index ci) {
+        m_imp.consume(a, ci);
+    }
 };
 }

src/math/lp/nra_solver.cpp

@@ -52,6 +52,7 @@ struct solver::imp {
     */
     lbool check() {        
         SASSERT(need_check());
+        m_zero = nullptr;
         m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
         m_zero = alloc(scoped_anum, am());
         m_term_set.clear();

src/qe/qsat.cpp

@@ -563,7 +563,11 @@ namespace qe {
                 m_solver->collect_statistics(st);
         }
         void reset_statistics() {
-            init();
+            clear();
+        }
+        void collect_statistics(statistics& st) {
+            if (m_solver)
+                m_solver->collect_statistics(st);
         }
         
         void clear() {
@@ -736,6 +740,7 @@ namespace qe {
             m_ex.init();                
         }    
 
+        
         /**
            \brief create a quantifier prefix formula.
         */
@@ -1334,8 +1339,8 @@ namespace qe {
         
         void collect_statistics(statistics & st) const override {
             st.copy(m_st);
-            m_fa.s().collect_statistics(st);
+            m_fa.collect_statistics(st);
-            m_ex.s().collect_statistics(st);        
+            m_ex.collect_statistics(st);        
             m_pred_abs.collect_statistics(st);
             st.update("qsat num rounds", m_stats.m_num_rounds); 
             m_pred_abs.collect_statistics(st);
@@ -1348,7 +1353,7 @@ namespace qe {
         }
         
         void cleanup() override {
-            reset();
+            clear();
         }
         
         void set_logic(symbol const & l) override {

src/smt/seq_eq_solver.cpp

@@ -775,6 +775,10 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
     for (unsigned i = 0; i < ls.size(); ++i) {
         if (eq_unit(ls[i], rs.back())) {
             bool same = true;
+            if (i == 0) {
+                m_overlap_lhs.insert(pair, true);
+                return true;
+            }
             // ls = rs' ++ y && rs = x ++ rs', diff = |x|
             if (rs.size() > i) {
                 unsigned diff = rs.size() - (i + 1);
@@ -817,6 +821,10 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
         unsigned diff = ls.size()-1-i;
         if (eq_unit(ls[diff], rs[0])) {
             bool same = true;
+            if (i == 0) {
+                m_overlap_rhs.insert(pair, true);
+                return true;
+            }
             // ls = x ++ rs' && rs = rs' ++ y, diff = |x|
             if (rs.size() > i) {
                 for (unsigned j = 1; same && j <= i; ++j) {
@@ -973,19 +981,21 @@ bool theory_seq::branch_quat_variable(eq const& e) {
 
     bool cond = false;
 
-    // xs and ys cannot align
-    if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys))
-        cond = true;
     // xs = ys and xs and ys cannot align except the case xs = ys
-    else if (xs == ys) {
+    if (xs == ys) {
         expr_ref_vector xs1(m), xs2(m);
         xs1.reset();
         xs1.append(xs.size()-1, xs.c_ptr()+1);
         xs2.reset();
         xs2.append(xs.size()-1, xs.c_ptr());
-        if (!can_align_from_lhs(xs2, ys) && !can_align_from_rhs(xs1, ys))
+        if (xs1.empty() || xs2.empty())
+            cond = true;
+        else if (!can_align_from_lhs(xs2, ys) && !can_align_from_rhs(xs1, ys))
             cond = true;
     }
+    // xs and ys cannot align
+    else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys))
+        cond = true;
 
     if (cond) {
         literal_vector lits;

src/smt/smt_case_split_queue.cpp

@@ -1252,12 +1252,12 @@ namespace {
 namespace smt {
     case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) {
         if (ctx.relevancy_lvl() < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
-                p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
+                                        p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
             warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5");
             p.m_case_split_strategy = CS_ACTIVITY;
         }
         if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
-                p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
+                                p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
             warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5");
             p.m_case_split_strategy = CS_ACTIVITY;
         }

src/smt/smt_context.cpp

@@ -47,7 +47,7 @@ namespace smt {
         m_fparams(p),
         m_params(_p),
         m_setup(*this, p),
-        m_relevancy_lvl(p.m_relevancy_lvl),
+        m_relevancy_lvl(m_fparams.m_relevancy_lvl),
         m_asserted_formulas(m, p, _p),
         m_rewriter(m),
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),

src/smt/smt_context.h

@@ -741,7 +741,12 @@ namespace smt {
 
         bool should_internalize_rec(expr* e) const;
 
-        void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
+        void top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & sorted_exprs);
+
+        void internalize_rec(expr * n, bool gate_ctx);
+
+        void internalize_deep(expr * n);
+        void internalize_deep(expr* const* n, unsigned num_exprs);
 
         void assert_default(expr * n, proof * pr);
 
@@ -868,6 +873,7 @@ namespace smt {
         void ensure_internalized(expr* e);
 
         void internalize(expr * n, bool gate_ctx);
+        void internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx);
 
         void internalize(expr * n, bool gate_ctx, unsigned generation);
 
@@ -906,10 +912,6 @@ namespace smt {
 
     public:
 
-        void internalize_rec(expr * n, bool gate_ctx);
-
-        void internalize_deep(expr * n);
-
         // helper function for trail
         void undo_th_case_split(literal l);
 

src/smt/smt_internalizer.cpp

@@ -152,11 +152,9 @@ namespace smt {
         return visited;
     }
 
-    void context::top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs) {
+    void context::top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & sorted_exprs) {
-        ts_todo.reset();
         tcolors.reset();
         fcolors.reset();
-        ts_todo.push_back(expr_bool_pair(n, true));
         while (!ts_todo.empty()) {
             expr_bool_pair & p = ts_todo.back();
             expr * curr        = p.first;
@@ -166,12 +164,14 @@ namespace smt {
                 set_color(tcolors, fcolors, curr, gate_ctx, Grey);
                 ts_visit_children(curr, gate_ctx, ts_todo);
                 break;
-            case Grey:
+            case Grey: {
                 SASSERT(ts_visit_children(curr, gate_ctx, ts_todo));
                 set_color(tcolors, fcolors, curr, gate_ctx, Black);
-                if (n != curr && !m.is_not(curr))
+                auto end = exprs + num_exprs;
+                if (std::find(exprs, end, curr) == end && !m.is_not(curr) && should_internalize_rec(curr))
                     sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx));
                 break;
+            }
             case Black:
                 ts_todo.pop_back();
                 break;
@@ -190,22 +190,32 @@ namespace smt {
             to_app(e)->get_family_id() == m.get_basic_family_id();
     }
 
-    void context::internalize_deep(expr* n) {
+    void context::internalize_deep(expr* const* exprs, unsigned num_exprs) {
-        if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) {
+        ts_todo.reset();
-            // if the expression is deep, then execute topological sort to avoid
+        for (unsigned i = 0; i < num_exprs; ++i) {
-            // stack overflow.
+            expr * n = exprs[i];
-            // a caveat is that theory internalizers do rely on recursive descent so
+            if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) {
-            // internalization over these follows top-down
+                // if the expression is deep, then execute topological sort to avoid
-            TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m););
+                // stack overflow.
-            svector<expr_bool_pair> sorted_exprs;
+                // a caveat is that theory internalizers do rely on recursive descent so
-            top_sort_expr(n, sorted_exprs);
+                // internalization over these follows top-down
-            TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
+                TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m););
-            for (auto & kv : sorted_exprs) {
+                ts_todo.push_back(expr_bool_pair(n, true));
-                expr* e = kv.first;
-                if (should_internalize_rec(e)) 
-                    internalize_rec(e, kv.second);
             }
         }
+
+        svector<expr_bool_pair> sorted_exprs;
+        top_sort_expr(exprs, num_exprs, sorted_exprs);
+        TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
+        for (auto & kv : sorted_exprs) {
+            expr* e = kv.first;
+            SASSERT(should_internalize_rec(e));
+            internalize_rec(e, kv.second);
+        }
+    }
+    void context::internalize_deep(expr* n) {
+        expr * v[1] = { n };
+        internalize_deep(v, 1);
     }
  
     /**
@@ -343,6 +353,13 @@ namespace smt {
         internalize_rec(n, gate_ctx);
     }
 
+    void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
+        internalize_deep(exprs, num_exprs);
+        for (unsigned i = 0; i < num_exprs; ++i) {
+            internalize_rec(exprs[i], gate_ctx);
+        }
+    }
+
     void context::internalize_rec(expr * n, bool gate_ctx) {
         TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";);
         TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m) << "\n";);

src/smt/theory_array_full.cpp

@@ -398,7 +398,7 @@ namespace smt {
         if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){
             return;
         }
-        if (!ctx.e_internalized(n)) ctx.internalize(n, false);;
+        ctx.ensure_internalized(n);
         enode* node = ctx.get_enode(n);
         if (is_select(n)) {
             enode * arg = ctx.get_enode(n->get_arg(0));

src/smt/theory_bv.cpp

@@ -52,10 +52,15 @@ namespace smt {
         literal_vector & bits = m_bits[v];
         TRACE("bv", tout << "v" << v << "\n";);
         bits.reset();
+        m_bits_expr.reset();
+
         for (unsigned i = 0; i < bv_size; i++) {
-            app * bit  = mk_bit2bool(owner, i);
+            m_bits_expr.push_back(mk_bit2bool(owner, i));
-            ctx.internalize(bit, true);
+        }
-            bool_var b = ctx.get_bool_var(bit);
+        ctx.internalize(m_bits_expr.c_ptr(), bv_size, true);
+
+        for (unsigned i = 0; i < bv_size; i++) {
+            bool_var b = ctx.get_bool_var(m_bits_expr[i]);
             bits.push_back(literal(b));
             if (is_relevant && !ctx.is_relevant(b)) {
                 ctx.mark_as_relevant(b);
@@ -142,9 +147,7 @@ namespace smt {
     }
 
     void theory_bv::process_args(app * n) {
-        for (expr* arg : *n) {
+        ctx.internalize(n->get_args(), n->get_num_args(), false);
-            ctx.internalize(arg, false);
-        }
     }
 
     enode * theory_bv::mk_enode(app * n) {
@@ -189,7 +192,7 @@ namespace smt {
         for (literal lit : bits) {
             expr_ref l(get_manager());
             ctx.literal2expr(lit, l);
-            r.push_back(l);
+            r.push_back(std::move(l));
         }
     }
 
@@ -312,13 +315,13 @@ namespace smt {
         unsigned sz             = bits.size();
         SASSERT(get_bv_size(n) == sz);
         m_bits[v].reset();
+
+        ctx.internalize(bits.c_ptr(), sz, true);
+
         for (unsigned i = 0; i < sz; i++) {
             expr * bit          = bits.get(i);
-            expr_ref s_bit(m);
+            literal l           = ctx.get_literal(bit);
-            simplify_bit(bit, s_bit);
+            TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(bit, m) << "\n";);
-            ctx.internalize(s_bit, true);
-            literal l           = ctx.get_literal(s_bit.get());
-            TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(s_bit, m) << "\n";);
             add_bit(v, l);
         }
         find_wpos(v);
@@ -740,28 +743,6 @@ namespace smt {
         TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \
     }
 
-
-#define MK_BINARY_COND(NAME, BLAST_OP)                                                  \
-    void theory_bv::NAME(app * n) {                                                     \
-        SASSERT(!ctx.e_internalized(n));                                      \
-        SASSERT(n->get_num_args() == 2);                                                \
-        process_args(n);                                                                \
-        enode * e       = mk_enode(n);                                                  \
-        expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);                            \
-        expr_ref        cond(m), s_cond(m);                                             \
-        get_arg_bits(e, 0, arg1_bits);                                                  \
-        get_arg_bits(e, 1, arg2_bits);                                                  \
-        SASSERT(arg1_bits.size() == arg2_bits.size());                                  \
-        m_bb.BLAST_OP(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, cond); \
-        init_bits(e, bits);                                                             \
-        simplify_bit(cond, s_cond);                                     \
-        ctx.internalize(s_cond, true);                                  \
-        literal l(ctx.get_literal(s_cond));                             \
-        ctx.mark_as_relevant(l);                                        \
-        ctx.mk_th_axiom(get_id(), 1, &l);                               \
-        TRACE("bv", tout << mk_pp(cond, m) << "\n"; tout << l << "\n";); \
-    }
-
     void theory_bv::internalize_sub(app *n) {
         SASSERT(!ctx.e_internalized(n));                      
         SASSERT(n->get_num_args() == 2);                                                
@@ -983,9 +964,7 @@ namespace smt {
     }
 
     bool theory_bv::internalize_carry(app * n, bool gate_ctx) {
-        ctx.internalize(n->get_arg(0), true);
+        ctx.internalize(n->get_args(), 3, true);
-        ctx.internalize(n->get_arg(1), true);
-        ctx.internalize(n->get_arg(2), true);
         bool is_new_var = false;
         bool_var v;
         if (!ctx.b_internalized(n)) {
@@ -1016,9 +995,7 @@ namespace smt {
     }
 
     bool theory_bv::internalize_xor3(app * n, bool gate_ctx) {
-        ctx.internalize(n->get_arg(0), true);
+        ctx.internalize(n->get_args(), 3, true);
-        ctx.internalize(n->get_arg(1), true);
-        ctx.internalize(n->get_arg(2), true);
         bool is_new_var = false;
         bool_var v;
         if (!ctx.b_internalized(n)) {
@@ -1183,7 +1160,7 @@ namespace smt {
             ctx.internalize(diff, true);
             literal arg = ctx.get_literal(diff);
             lits.push_back(arg);
-            exprs.push_back(diff);
+            exprs.push_back(std::move(diff));
         }
         m_stats.m_num_diseq_dynamic++;
         if (m.has_trace_stream()) {
@@ -1447,7 +1424,9 @@ namespace smt {
         m_find(*this),
         m_approximates_large_bvs(false) {
         memset(m_eq_activity, 0, sizeof(m_eq_activity));
+#if WATCH_DISEQ
         memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
+#endif
     }
 
     theory_bv::~theory_bv() {

src/smt/theory_bv.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef THEORY_BV_H_
+#pragma once
-#define THEORY_BV_H_
 
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
 #include "util/trail.h"
@@ -112,6 +111,7 @@ namespace smt {
         th_trail_stack           m_trail_stack;
         th_union_find            m_find;
         vector<literal_vector>   m_bits;     // per var, the bits of a given variable.
+        ptr_vector<expr>         m_bits_expr;
         svector<unsigned>        m_wpos;     // per var, watch position for fixed variable detection. 
         vector<zero_one_bits>    m_zero_one_bits; // per var, see comment in the struct zero_one_bit
         bool_var2atom            m_bool_var2atom;
@@ -124,11 +124,11 @@ namespace smt {
         value2var                m_fixed_var_table;
         
         unsigned char            m_eq_activity[256];
-        unsigned char            m_diseq_activity[256];
+        //unsigned char            m_diseq_activity[256];
         svector<std::pair<theory_var, theory_var>> m_replay_diseq;
-        vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
+        //vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
-        svector<bool_var> m_diseq_watch_trail;
+        //svector<bool_var> m_diseq_watch_trail;
-        unsigned_vector   m_diseq_watch_lim;
+        //unsigned_vector   m_diseq_watch_lim;
 
         literal_vector           m_tmp_literals;
         svector<var_pos>         m_prop_queue;
@@ -278,6 +278,3 @@ namespace smt {
         bool check_zero_one_bits(theory_var v);
     };
 };
-
-#endif /* THEORY_BV_H_ */
-

src/smt/theory_fpa.cpp

@@ -415,9 +415,7 @@ namespace smt {
         if (ctx.b_internalized(atom))
             return true;
 
-        unsigned num_args = atom->get_num_args();
+        ctx.internalize(atom->get_args(), atom->get_num_args(), false);
-        for (unsigned i = 0; i < num_args; i++)
-            ctx.internalize(atom->get_arg(i), false);
 
         literal l(ctx.mk_bool_var(atom));
         ctx.set_var_theory(l.var(), get_id());
@@ -436,9 +434,7 @@ namespace smt {
         SASSERT(term->get_family_id() == get_family_id());
         SASSERT(!ctx.e_internalized(term));
 
-        unsigned num_args = term->get_num_args();
+        ctx.internalize(term->get_args(), term->get_num_args(), false);
-        for (unsigned i = 0; i < num_args; i++)
-            ctx.internalize(term->get_arg(i), false);
 
         enode * e = ctx.mk_enode(term, false, false, true);
 
@@ -476,7 +472,7 @@ namespace smt {
         SASSERT(m_fpa_util.is_float(n->get_owner()) || m_fpa_util.is_rm(n->get_owner()));
         SASSERT(n->get_owner()->get_decl()->get_range() == s);
 
-        app_ref owner(n->get_owner(), m);
+        app * owner = n->get_owner();
 
         if (!is_attached_to_var(n)) {
             attach_new_th_var(n);
@@ -697,9 +693,7 @@ namespace smt {
     }
 
     enode* theory_fpa::ensure_enode(expr* e) {
-        if (!ctx.e_internalized(e)) {
+        ctx.ensure_internalized(e);
-            ctx.internalize(e, false);
-        }
         enode* n = ctx.get_enode(e);
         ctx.mark_as_relevant(n);
         return n;

src/smt/theory_lra.cpp

@@ -328,9 +328,6 @@ class theory_lra::imp {
     enode* get_enode(expr* e) const { return ctx().get_enode(e); }
     expr*  get_owner(theory_var v) const { return get_enode(v)->get_owner(); }        
 
-    lp::lar_solver& lp(){ return *m_solver.get(); }
-    const lp::lar_solver& lp() const { return *m_solver.get(); }
-    
     void init_solver() {
         if (m_solver) return;
 
@@ -969,6 +966,9 @@ public:
         std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc<internalize_state>());
     }
 
+    lp::lar_solver& lp(){ return *m_solver.get(); }
+    const lp::lar_solver& lp() const { return *m_solver.get(); }    
+ 
     void init() {
         if (m_solver) return;
 
@@ -2311,10 +2311,34 @@ public:
     //     }
     // }
 
+    bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval)  {
+        theory_var v = lp().local_to_external(vi);
+        if (v == null_theory_var) {
+            return false;
+        }
+        if (m_bounds.size() <= static_cast<unsigned>(v) || m_unassigned_bounds[v] == 0) {
+            return false;
+        }
+        for (lp_api::bound* b : m_bounds[v]) {
+            if (ctx().get_assignment(b->get_bv()) == l_undef &&
+                null_literal != is_bound_implied(kind, bval, *b)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    void consume(rational const& v, lp::constraint_index j) {
+        set_evidence(j, m_core, m_eqs);
+        m_explanation.add_pair(j, v);
+    }
+
+    
     void propagate_bounds_with_lp_solver() {
         if (!should_propagate()) 
             return;
-        local_bound_propagator bp(*this);
+        
+        lp::lp_bound_propagator<imp>  bp(*this);
 
         lp().propagate_bounds_for_touched_rows(bp);
 
@@ -2348,22 +2372,6 @@ public:
         }
         return false;
     }
-
-    struct local_bound_propagator: public lp::lp_bound_propagator {
-        imp & m_imp;
-        local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {}
-
-        bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const rational & v) override {
-            return m_imp.bound_is_interesting(j, kind, v);
-        }
-
-        void consume(rational const& v, lp::constraint_index j) override {
-            m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs);
-            m_imp.m_explanation.add_pair(j, v);
-        }
-    };
-
-        
     void propagate_lp_solver_bound(lp::implied_bound& be) {
         lpvar vi = be.m_j;
         theory_var v = lp().local_to_external(vi);
@@ -2396,7 +2404,7 @@ public:
                 first = false;
                 reset_evidence();
                 m_explanation.clear();
-                local_bound_propagator bp(*this);
+                lp::lp_bound_propagator<imp> bp(*this);
                 lp().explain_implied_bound(be, bp);
             }
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
@@ -2419,6 +2427,27 @@ public:
         }
     }
 
+    void add_eq(lpvar u, lpvar v, lp::explanation const& e) {
+        if (ctx().inconsistent())
+            return;
+        theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
+        theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
+        enode* n1 = get_enode(uv);
+        enode* n2 = get_enode(vv);
+        if (n1->get_root() == n2->get_root())
+            return;
+        reset_evidence();
+        for (auto const& ev : e) 
+            set_evidence(ev.ci(), m_core, m_eqs);
+        justification* js = ctx().mk_justification(
+            ext_theory_eq_propagation_justification(
+                get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), n1, n2));
+        
+        std::function<expr*(void)> fn = [&]() { return m.mk_eq(n1->get_owner(), n2->get_owner()); };
+        scoped_trace_stream _sts(th, fn);
+        ctx().assign_eq(n1, n2, eq_justification(js));        
+    }
+
     literal_vector m_core2;
 
     void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {
@@ -3364,7 +3393,7 @@ public:
         if (t.is_term()) {
 
             m_todo_terms.push_back(std::make_pair(t, rational::one()));
-
+            TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";);
             TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n";
                   lp().print_term(lp().get_term(t), tout) << "\n";);
 
@@ -3402,7 +3431,7 @@ public:
     model_value_proc * mk_value(enode * n, model_generator & mg) {
         theory_var v = n->get_th_var(get_id());
         expr* o = n->get_owner();
-        if (use_nra_model()) {
+        if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
             anum const& an = nl_value(v, *m_a1);
             if (a.is_int(o) && !m_nla->am().is_int(an)) {
                 return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o)));
@@ -3999,7 +4028,9 @@ theory_var theory_lra::add_objective(app* term) {
 expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
     return m_imp->mk_ge(fm, v, val);
 }
-
-
-
 }
+template  class lp::lp_bound_propagator<smt::theory_lra::imp>;
+template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);
+template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&);
+template void lp::lar_solver::calculate_implied_bounds_for_row<smt::theory_lra::imp>(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>&);
+template void lp::lar_solver::propagate_bounds_on_terms<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);

src/smt/theory_lra.h

@@ -24,7 +24,9 @@ Revision History:
 
 namespace smt {
     class theory_lra : public theory, public theory_opt {
+    public:
         class imp;
+    private:
         imp* m_imp;
 
     public:

src/smt/theory_str_mc.cpp

@@ -725,7 +725,10 @@ namespace smt {
             v.init(&get_context());
             rational pos_value;
             bool pos_exists = v.get_value(pos, pos_value);
-            ENSURE(pos_exists);
+            if (!pos_exists) {
+                cex = m.mk_or(m_autil.mk_ge(pos, mk_int(0)), m_autil.mk_le(pos, mk_int(0)));
+                return false;
+            }
             TRACE("str_fl", tout << "reduce str.at: base=" << mk_pp(base, m) << ", pos=" << pos_value.to_string() << std::endl;);
             if (pos_value.is_neg() || pos_value >= rational(base_chars.size())) {
                 // return the empty string

src/test/lp/lp.cpp

@@ -313,11 +313,6 @@ void test_cn() {
 namespace lp {
 unsigned seed = 1;
 
-class my_bound_propagator : public lp_bound_propagator {
-public:
-    my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls) {}
-    void consume(mpq const& v, lp::constraint_index j) override {}
-};
 
 random_gen g_rand;
 static unsigned my_random() {