build issues

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

src/math/lp/emonics.cpp

@@ -225,6 +225,7 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
         for (const monic& e : enum_sign_equiv_monics(m))
             c.insert(e.var());
         auto it = lists.find(m.rvars());
+        (void)it;
         
         CTRACE("nla_solver_mons",  it->second != c,
                tout << "m = " << m << "\n";

src/math/lp/lar_constraints.h

@@ -48,37 +48,50 @@ inline std::string lconstraint_kind_string(lconstraint_kind t) {
     return std::string(); // it is unreachable
 }
 
-struct lar_base_constraint {
+class lar_base_constraint {
     lconstraint_kind m_kind;
-    mpq m_right_side;
+    mpq              m_right_side;
+    bool             m_active;
+public:
+
     virtual vector<std::pair<mpq, var_index>> coeffs() const = 0;
-    lar_base_constraint() {}
+    lar_base_constraint(lconstraint_kind kind, const mpq& right_side) :m_kind(kind), m_right_side(right_side), m_active(false) {}
-    lar_base_constraint(lconstraint_kind kind, const mpq& right_side) :m_kind(kind), m_right_side(right_side) {}
+    virtual ~lar_base_constraint() {}
+
+    lconstraint_kind kind() const { return m_kind; }
+    mpq const& rhs() const { return m_right_side; }
+
+    void activate() { m_active = true; }
+    void deactivate() { m_active = false; }
+    bool is_active() const { return m_active; }
 
     virtual unsigned size() const = 0;
-    virtual ~lar_base_constraint(){}
     virtual mpq get_free_coeff_of_left_side() const { return zero_of_type<mpq>();}
 };
 
 class lar_var_constraint: public lar_base_constraint {
     unsigned m_j;
 public:
+    lar_var_constraint(unsigned j, lconstraint_kind kind, const mpq& right_side) : 
+        lar_base_constraint(kind, right_side), m_j(j) {}
+
     vector<std::pair<mpq, var_index>> coeffs() const override {
         vector<std::pair<mpq, var_index>> ret;
         ret.push_back(std::make_pair(one_of_type<mpq>(), m_j));
         return ret;
     }
     unsigned size() const override { return 1;}
-    lar_var_constraint(unsigned j, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_j(j) { }
 };
 
 
 class lar_term_constraint: public lar_base_constraint {
     const lar_term * m_term;
 public:
+    lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : 
+        lar_base_constraint(kind, right_side), m_term(t) {}
+
     vector<std::pair<mpq, var_index>> coeffs() const override { return m_term->coeffs_as_vector(); }
     unsigned size() const override { return m_term->size();}
-    lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { }
 };
 
 
@@ -87,6 +100,8 @@ class constraint_set {
     column_namer&                  m_namer;
     vector<lar_base_constraint*>   m_constraints;
     stacked_value<unsigned>        m_constraint_count;
+    unsigned_vector                m_active;
+    stacked_value<unsigned>        m_active_lim;
 
     constraint_index add(lar_base_constraint* c) {
         constraint_index ci = m_constraints.size();
@@ -135,6 +150,10 @@ public:
         m_constraint_count = m_constraints.size();
         m_constraint_count.push();
         m_region.push_scope();
+#if 0
+        m_active_lim = m_active.size();
+        m_active_lim.push();
+#endif
     }
 
     void pop(unsigned k) {
@@ -142,6 +161,13 @@ public:
         for (unsigned i = m_constraints.size(); i-- > m_constraint_count; )
             m_constraints[i]->~lar_base_constraint();        
         m_constraints.shrink(m_constraint_count);
+#if 0
+        m_active_lim.pop(k);
+        for (unsigned i = m_active.size(); i-- > m_active_lim; ) {
+            m_constraints[m_active[i]]->deactivate();
+        }
+        m_active.shrink(m_active_lim);
+#endif
         m_region.pop_scope(k);
     }
 
@@ -153,19 +179,78 @@ public:
         return add(new (m_region) lar_term_constraint(t, k, rhs));
     }
 
+#if 1
+    bool is_active(constraint_index ci) const { return true; }
+
+    void activate(constraint_index ci) {}
+
+#else
+    // future behavior uses activation bit.
+    bool is_active(constraint_index ci) const { return m_constraints[ci]->is_active(); }
+
+    void activate(constraint_index ci) { m_constraints[ci]->activate(); }
+#endif
+
     lar_base_constraint const& operator[](constraint_index ci) const { return *m_constraints[ci]; }    
 
-    // TBD: would like to make this opaque
-    // and expose just active constraints
-    // constraints need not be active.
     bool valid_index(constraint_index ci) const { return ci < m_constraints.size(); }
-    vector<lar_base_constraint*>::const_iterator begin() const { return m_constraints.begin(); }
+
-    vector<lar_base_constraint*>::const_iterator end() const { return m_constraints.end(); }
+    class active_constraints {
+        friend class constraint_set;
+        constraint_set const& cs;
+    public:
+        active_constraints(constraint_set const& cs): cs(cs) {}
+        class iterator {
+            friend class constraint_set;
+            constraint_set const& cs;
+            unsigned m_index;
+            iterator(constraint_set const& cs, unsigned idx): cs(cs), m_index(idx) { forward(); }
+            void next() { ++m_index; forward(); }
+            void forward() { for (; m_index < cs.m_constraints.size() && !cs.is_active(m_index); m_index++) ; }
+        public:
+            lar_base_constraint const& operator*() { return cs[m_index]; }
+            lar_base_constraint const* operator->() const { return &cs[m_index]; }
+            iterator& operator++() { next(); return *this; }
+            iterator operator++(int) { auto tmp = *this; next(); return tmp; }
+            bool operator==(iterator const& other) const { return m_index == other.m_index; }
+            bool operator!=(iterator const& other) const { return m_index != other.m_index; }
+        };
+        iterator begin() const { return iterator(cs, 0); }
+        iterator end() const { return iterator(cs, cs.m_constraints.size()); }
+    };
+
+    active_constraints active() const { return active_constraints(*this); }
+
+    class active_indices {
+        friend class constraint_set;
+        constraint_set const& cs;
+    public:
+        active_indices(constraint_set const& cs): cs(cs) {}
+        class iterator {
+            friend class constraint_set;
+            constraint_set const& cs;
+            unsigned m_index;
+            iterator(constraint_set const& cs, unsigned idx): cs(cs), m_index(idx) { forward(); }
+            void next() { ++m_index; forward(); }
+            void forward() { for (; m_index < cs.m_constraints.size() && !cs.is_active(m_index); m_index++) ; }
+        public:
+            constraint_index operator*() { return m_index; }
+            constraint_index const* operator->() const { return &m_index; }
+            iterator& operator++() { next(); return *this; }
+            iterator operator++(int) { auto tmp = *this; next(); return tmp; }
+            bool operator==(iterator const& other) const { return m_index == other.m_index; }
+            bool operator!=(iterator const& other) const { return m_index != other.m_index; }
+        };
+        iterator begin() const { return iterator(cs, 0); }
+        iterator end() const { return iterator(cs, cs.m_constraints.size()); }
+    };
+
+    active_indices indices() const { return active_indices(*this); }
         
     std::ostream& display(std::ostream& out) const {
         out << "number of constraints = " << m_constraints.size() << std::endl;
-        for (auto const* c : *this) {
+        for (auto const& c : active()) {
-            display(out, *c);
+            display(out, c);
         }
         return out;
     }
@@ -176,7 +261,7 @@ public:
 
     std::ostream& display(std::ostream& out, lar_base_constraint const& c) const {
         print_left_side_of_constraint(c, out);
-        return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl;
+        return out << " " << lconstraint_kind_string(c.kind()) << " " << c.rhs() << std::endl;
     }
 
     std::ostream& display_indices_only(std::ostream& out, constraint_index ci) const {
@@ -185,7 +270,7 @@ public:
 
     std::ostream& display_indices_only(std::ostream& out, lar_base_constraint const& c) const {
         print_left_side_of_constraint_indices_only(c, out);
-        return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl;
+        return out << " " << lconstraint_kind_string(c.kind()) << " " << c.rhs() << std::endl;
     }
 
     std::ostream& display(std::ostream& out, std::function<std::string (unsigned)> var_str, constraint_index ci) const {
@@ -194,7 +279,7 @@ public:
 
     std::ostream& display(std::ostream& out, std::function<std::string (unsigned)>& var_str, lar_base_constraint const& c) const {
         print_left_side_of_constraint(c, var_str, out); 
-        return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl;
+        return out << " " << lconstraint_kind_string(c.kind()) << " " << c.rhs() << std::endl;
     }
 
     

src/math/lp/lar_solver.cpp

@@ -100,13 +100,13 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
         mpq coeff = it.first;
         constraint_index con_ind = it.second;
         const auto & constr = m_constraints[con_ind];
-        lconstraint_kind kind = coeff.is_pos() ? constr.m_kind : flip_kind(constr.m_kind);
+        lconstraint_kind kind = coeff.is_pos() ? constr.kind() : flip_kind(constr.kind());
         register_in_map(coeff_map, constr, coeff);
         if (kind == GT || kind == LT)
             strict = true;
         if (kind == GE || kind == GT) n_of_G++;
         else if (kind == LE || kind == LT) n_of_L++;
-        rs_of_evidence += coeff*constr.m_right_side;
+        rs_of_evidence += coeff*constr.rhs();
     }
     lp_assert(n_of_G == 0 || n_of_L == 0);
     lconstraint_kind kind = n_of_G ? GE : (n_of_L ? LE : EQ);
@@ -981,30 +981,27 @@ bool lar_solver::all_constraints_hold() const {
     std::unordered_map<var_index, mpq> var_map;
     get_model_do_not_care_about_diff_vars(var_map);
     
-    unsigned i = 0;
+    for (auto const& c : m_constraints.active()) {
-    for (auto const* c : m_constraints) {
+        if (!constraint_holds(c, var_map)) {
-        if (!constraint_holds(*c, var_map)) {
             TRACE("lar_solver",
-                  tout << "i = " << i << "; ";
+                  m_constraints.display(tout, c) << "\n";
-                  m_constraints.display(tout, *c) << "\n";
+                  for (auto p : c.coeffs()) {
-                  for (auto p : c->coeffs()) {
                       m_mpq_lar_core_solver.m_r_solver.print_column_info(p.second, tout);
                   });
             return false;
         }
-        ++i;
     }
     return true;
 }
 
 bool lar_solver::constraint_holds(const lar_base_constraint & constr, std::unordered_map<var_index, mpq> & var_map) const {
     mpq left_side_val = get_left_side_val(constr, var_map);
-    switch (constr.m_kind) {
+    switch (constr.kind()) {
-    case LE: return left_side_val <= constr.m_right_side;
+    case LE: return left_side_val <= constr.rhs();
-    case LT: return left_side_val <  constr.m_right_side;
+    case LT: return left_side_val <  constr.rhs();
-    case GE: return left_side_val >= constr.m_right_side;
+    case GE: return left_side_val >= constr.rhs();
-    case GT: return left_side_val >  constr.m_right_side;
+    case GT: return left_side_val >  constr.rhs();
-    case EQ: return left_side_val == constr.m_right_side;
+    case EQ: return left_side_val == constr.rhs();
     default:
         lp_unreachable();
     }
@@ -1018,8 +1015,8 @@ bool lar_solver::the_relations_are_of_same_type(const vector<std::pair<mpq, unsi
         mpq coeff = it.first;
         constraint_index con_ind = it.second;
         lconstraint_kind kind = coeff.is_pos() ?
-            m_constraints[con_ind].m_kind :
+            m_constraints[con_ind].kind() :
-            flip_kind(m_constraints[con_ind].m_kind);
+            flip_kind(m_constraints[con_ind].kind());
         if (kind == GT || kind == LT)
             strict = true;
         if (kind == GE || kind == GT) 
@@ -1108,7 +1105,7 @@ mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const {
         mpq coeff = it.first;
         constraint_index con_ind = it.second;
         lp_assert(m_constraints.valid_index(con_ind));
-        ret += (m_constraints[con_ind].m_right_side - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff;
+        ret += (m_constraints[con_ind].rhs() - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff;
     }
     return ret;
 }
@@ -1802,6 +1799,7 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq &
 
 void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side,
                                               constraint_index constr_index) {
+    m_constraints.activate(constr_index);
     if (column_has_upper_bound(j))
         update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
     else 

src/math/lp/nex_creator.cpp

@@ -599,7 +599,6 @@ bool nex_creator::is_simplified(const nex& e) const {
     return true;
 }
 
-#ifdef Z3DEBUG
 unsigned nex_creator::find_sum_in_mul(const nex_mul* a) const {
     for (unsigned j = 0; j < a->size(); j++)
         if ((*a)[j].e()->is_sum())
@@ -673,5 +672,4 @@ bool nex_creator::equal(const nex* a, const nex* b) {
     TRACE("grobner_d", tout << "b = " << *b << ", canonized b = " << *cb << "\n";);
     return !(cn.gt(ca, cb) || cn.gt(cb, ca));
 }
-#endif
 

src/math/lp/nex_creator.h

@@ -293,12 +293,9 @@ public:
         return gt(a.e(), b.e());
     }
     void process_map_pair(nex*e, const rational& coeff, nex_sum & sum, std::unordered_set<nex const*>&);
-#ifdef Z3DEBUG
+    static bool equal(const nex*, const nex* );
-    static
-    bool equal(const nex*, const nex* );
     nex* canonize(const nex*);
     nex* canonize_mul(nex_mul*);
     unsigned find_sum_in_mul(const nex_mul* a) const;
-#endif
 };
 }

src/math/lp/nra_solver.cpp

@@ -92,11 +92,8 @@ typedef nla::variable_map_type variable_map_type;
             vector<nlsat::assumption, false> core;
 
             // add linear inequalities from lra_solver
-            unsigned i = 0;
+            for (lp::constraint_index ci : s.constraints().indices()) {
-            for (auto const* c : s.constraints()) {
+                add_constraint(ci);
-                (void)c;
-                add_constraint(i);
-                ++i;
             }
 
             // add polynomial definitions.
@@ -159,8 +156,8 @@ typedef nla::variable_map_type variable_map_type;
         void add_constraint(unsigned idx) {
             auto& c = s.constraints()[idx];
             auto& pm = m_nlsat->pm();
-            auto k = c.m_kind;
+            auto k = c.kind();
-            auto rhs = c.m_right_side;
+            auto rhs = c.rhs();
             auto lhs = c.coeffs();
             auto sz = lhs.size();
             svector<polynomial::var> vars;

src/sat/sat_lut_finder.cpp

@@ -234,7 +234,7 @@ namespace sat {
 
     uint64_t lut_finder::convert_combination(bool_var_vector& vars, bool_var& v) {
         SASSERT(lut_is_defined(vars.size()));
-        unsigned i = 0, j = 0;
+        unsigned i = 0;
         for (; i < vars.size(); ++i) {
             if (lut_is_defined(i, vars.size())) {
                 break;

src/smt/asserted_formulas.cpp

@@ -504,7 +504,6 @@ void asserted_formulas::propagate_values() {
     flush_cache();
 
     unsigned num_prop = 0;
-    unsigned num_iterations = 0;
     unsigned delta_prop = m_formulas.size();
     while (!inconsistent() && m_formulas.size()/20 < delta_prop) {
         m_expr2depth.reset();

src/smt/theory_lra.cpp

@@ -2032,11 +2032,11 @@ public:
         lp::lar_base_constraint const& c = lp().constraints()[ci];
         expr_ref fml(m);
         expr_ref_vector ts(m);
-        rational rhs = c.m_right_side;
+        rational rhs = c.rhs();
         for (auto cv : c.coeffs()) {
             ts.push_back(multerm(cv.first, var2expr(cv.second)));
         }
-        switch (c.m_kind) {
+        switch (c.kind()) {
         case lp::LE: fml = a.mk_le(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
         case lp::LT: fml = a.mk_lt(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
         case lp::GE: fml = a.mk_ge(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;

src/smt/theory_str.cpp

@@ -9690,7 +9690,7 @@ namespace smt {
 
             std::string s = std::to_string(val.get_int32());
             extra_deps.push_back(ctx.mk_eq_atom(fromInt, mk_int(val)));
-            return s.length();
+            return static_cast<unsigned>(s.length());
 
         } else if (u.str.is_at(ex)) {
             expr* substrBase = nullptr;
@@ -9886,8 +9886,7 @@ namespace smt {
 
     expr* theory_str::refine_function(expr* f) {
         //Can we learn something better?
-        ast_manager & m = get_manager();
+        TRACE("str", tout << "learning not " << mk_pp(f, get_manager()) << std::endl;);
-        TRACE("str", tout << "learning not " << mk_pp(f, m) << std::endl;);
         return f;
     }