Merge branch 'master' of https://github.com/z3prover/z3

src/api/api_goal.cpp

@@ -199,8 +199,8 @@ extern "C" {
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         if (!to_goal_ref(g)->is_cnf()) { 
-            warning_msg("goal is not in CNF. This will produce a propositional abstraction. "
+            SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
-                        "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
+            RETURN_Z3(nullptr);
         }
         to_goal_ref(g)->display_dimacs(buffer);
         // Hack for removing the trailing '\n'

src/api/z3_api.h

@@ -5525,6 +5525,11 @@ extern "C" {
 
     /**
        \brief Convert a goal into a DIMACS formatted string.
+       The goal must be in CNF. You can convert a goal to CNF
+       by applying the tseitin-cnf tactic. Bit-vectors are not automatically
+       converted to Booleans either, so the caller intends to 
+       preserve satisfiability, it should apply bit-blasting tactics.
+       Quantifiers and theory atoms will not be encoded.
 
        def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL)))
     */

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -89,6 +89,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
     expr_ref_vector                          m_out;
     obj_map<func_decl, expr*>                m_const2bits;
     expr_ref_vector                          m_bindings;
+    unsigned_vector                          m_shifts;
     func_decl_ref_vector                     m_keys;
     expr_ref_vector                          m_values;
     unsigned_vector                          m_keyval_lim;
@@ -579,9 +580,12 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             }
             SASSERT(new_bindings.size() == q->get_num_decls());
             i = q->get_num_decls();
+            unsigned shift = j;
+            if (!m_shifts.empty()) shift += m_shifts.back();
             while (i > 0) {
                 i--;
                 m_bindings.push_back(new_bindings[i]);
+                m_shifts.push_back(shift);
             }
         }
         return true;
@@ -589,9 +593,23 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
 
     bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
         if (m_blast_quant) {   
-            if (t->get_idx() >= m_bindings.size())
+            if (m_bindings.empty())
                 return false;
-            result = m_bindings.get(m_bindings.size() - t->get_idx() - 1);
+            unsigned shift = m_shifts.back();
+            if (t->get_idx() >= m_bindings.size()) {
+                if (shift == 0)
+                    return false;
+                result = m_manager.mk_var(t->get_idx() + shift, t->get_sort());
+            }
+            else {
+                unsigned offset = m_bindings.size() - t->get_idx() - 1; 
+                result = m_bindings.get(offset);
+                shift = shift - m_shifts[offset];
+                if (shift > 0) {
+                    var_shifter vs(m_manager);
+                    vs(result, shift, result);
+                }
+            }
             result_pr = nullptr;
             return true;
         }
@@ -641,6 +659,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
                                    old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
         result_pr = nullptr;
         m_bindings.shrink(old_sz);
+        m_shifts.shrink(old_sz);
         return true;
     }
 };

src/qe/qe_mbi.cpp

@@ -346,9 +346,49 @@ namespace qe {
             func_decl_ref_vector no_shared(m);
             tg1.set_vars(no_shared, false);
             tg1.add_lits(lits);
+            arith_util a(m);
+            expr_ref_vector foreign = tg1.shared_occurrences(a.get_family_id());
+            obj_hashtable<expr> _foreign;
+            for (expr* e : foreign) _foreign.insert(e);
+            vector<expr_ref_vector> partition = tg1.get_partition(*mdl);
             expr_ref_vector diseq = tg1.get_ackerman_disequalities();
             lits.append(diseq);
-            TRACE("qe", tout << "diseq: " << diseq << "\n";);
+            TRACE("qe", tout << "diseq: " << diseq << "\n";
+                  tout << "foreign: " << foreign << "\n";
+                  for (auto const& v : partition) {
+                      tout << "partition: {";
+                      bool first = true;
+                      for (expr* e : v) {
+                          if (first) first = false; else tout << ", ";
+                          tout << expr_ref(e, m);
+                      }
+                      tout << "}\n";
+                  }
+                  );
+            vector<expr_ref_vector> refined_partition;
+            for (auto & p : partition) {
+                unsigned j = 0; 
+                for (expr* e : p) {
+                    if (_foreign.contains(e) || 
+                        (is_app(e) && m_shared.contains(to_app(e)->get_decl()))) {
+                        p[j++] = e;
+                    }
+                }
+                p.shrink(j);
+                if (!p.empty()) refined_partition.push_back(p);
+            }
+            TRACE("qe",
+                  for (auto const& v : refined_partition) {
+                      tout << "partition: {";
+                      bool first = true;
+                      for (expr* e : v) {
+                          if (first) first = false; else tout << ", ";
+                          tout << expr_ref(e, m);
+                      }
+                      tout << "}\n";
+                  });
+
+            
             
             arith_project_plugin ap(m);
             ap.set_check_purified(false);

src/qe/qe_term_graph.cpp

@@ -99,7 +99,7 @@ namespace qe {
             m_mark(false),
             m_mark2(false),
             m_interpreted(false) {
-            if (!is_app()) return;
+            if (!is_app(m_expr)) return;
             for (expr* e : *to_app(m_expr)) {
                 term* t = app2term[e->get_id()];
                 t->get_root().m_parents.push_back(this);
@@ -151,7 +151,7 @@ namespace qe {
 
         unsigned get_id() const { return m_expr->get_id();}
 
-        unsigned get_decl_id() const { return is_app() ? get_app()->get_decl()->get_id() : m_expr->get_id(); }
+        unsigned get_decl_id() const { return is_app(m_expr) ? to_app(m_expr)->get_decl()->get_id() : m_expr->get_id(); }
 
         bool is_marked() const {return m_mark;}
         void set_mark(bool v){m_mark = v;}
@@ -159,12 +159,10 @@ namespace qe {
         void set_mark2(bool v){m_mark2 = v;}      // NSB: where is this used?
 
         bool is_interpreted() const {return m_interpreted;}
-        bool is_theory() const { return !is_app() || get_app()->get_family_id() != null_family_id; }
+        bool is_theory() const { return !is_app(m_expr) || to_app(m_expr)->get_family_id() != null_family_id; }
         void mark_as_interpreted() {m_interpreted=true;}
         expr* get_expr() const {return m_expr;}
-        bool is_app() const {return ::is_app(m_expr);}
+        unsigned get_num_args() const { return is_app(m_expr) ? to_app(m_expr)->get_num_args() : 0; }
-        app *get_app() const {return is_app() ? to_app(m_expr) : nullptr;}
-        unsigned get_num_args() const { return is_app() ? get_app()->get_num_args() : 0; }
 
         term &get_root() const {return *m_root;}
         bool is_root() const {return m_root == this;}
@@ -226,7 +224,7 @@ namespace qe {
     }
 
     bool term_graph::is_variable_proc::operator()(const term &t) const {
-        return (*this)(t.get_app());
+        return (*this)(t.get_expr());
     }
 
     void term_graph::is_variable_proc::set_decls(const func_decl_ref_vector &decls, bool exclude) {
@@ -444,7 +442,7 @@ namespace qe {
             return expr_ref(res, m);
         }
 
-        res = mk_app_core (r.get_app());
+        res = mk_app_core (r.get_expr());
         m_term2app.insert(r.get_id(), res);
         return expr_ref(res, m);
 
@@ -463,7 +461,7 @@ namespace qe {
         SASSERT(t.is_root());
         expr_ref rep(mk_app(t), m);
         for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
-            expr* mem = mk_app_core(it->get_app());
+            expr* mem = mk_app_core(it->get_expr());
             out.push_back (m.mk_eq (rep, mem));
         }
     }
@@ -472,9 +470,9 @@ namespace qe {
         mk_equalities(t, out);
 
         for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) {
-            expr* a1 = mk_app_core (it->get_app());
+            expr* a1 = mk_app_core (it->get_expr());
             for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) {
-                expr* a2 =  mk_app_core(it2->get_app());
+                expr* a2 =  mk_app_core(it2->get_expr());
                 out.push_back (m.mk_eq (a1, a2));
             }
         }
@@ -1000,6 +998,47 @@ namespace qe {
             reset();
             return res;
         }
+
+        vector<expr_ref_vector> get_partition(model& mdl) {
+            vector<expr_ref_vector> result;
+            expr_ref_vector pinned(m);
+            obj_map<expr, unsigned> pid;
+            model::scoped_model_completion _smc(mdl, true);
+            for (term *t : m_tg.m_terms) {
+                expr* a = t->get_expr();
+                if (!is_app(a)) continue;
+                if (m.is_bool(a)) continue;
+                expr_ref val = mdl(a);
+                unsigned p = 0;
+                // NB. works for simple domains Integers, Rationals, 
+                // but not for algebraic numerals.
+                if (!pid.find(val, p)) {
+                    p = pid.size();
+                    pid.insert(val, p);
+                    pinned.push_back(val);
+                    result.push_back(expr_ref_vector(m));
+                }
+                result[p].push_back(a);
+            }            
+            return result;
+        }
+
+        expr_ref_vector shared_occurrences(family_id fid) {
+            expr_ref_vector result(m);
+            for (term *t : m_tg.m_terms) {
+                expr* e = t->get_expr();
+                if (m.get_sort(e)->get_family_id() != fid) continue;
+                for (term * p : term::parents(t->get_root())) {
+                    expr* pe = p->get_expr();
+                    if (!is_app(pe)) continue;
+                    if (to_app(pe)->get_family_id() == fid) continue;
+                    if (to_app(pe)->get_family_id() == m.get_basic_family_id()) continue;
+                    result.push_back(e);
+                    break;
+                }                
+            }
+            return result;
+        }
     };
 
     void term_graph::set_vars(func_decl_ref_vector const& decls, bool exclude) {
@@ -1033,5 +1072,14 @@ namespace qe {
         return p.get_ackerman_disequalities();
     }
 
+    vector<expr_ref_vector> term_graph::get_partition(model& mdl) {
+        term_graph::projector p(*this);
+        return p.get_partition(mdl);
+    }
+
+    expr_ref_vector term_graph::shared_occurrences(family_id fid) {
+        term_graph::projector p(*this);
+        return p.shared_occurrences(fid);        
+    }
 
 }

src/qe/qe_term_graph.h

@@ -122,6 +122,19 @@ namespace qe {
          */
         expr_ref_vector get_ackerman_disequalities();
 
+        /**
+         * Produce a model-based partition.
+         */
+        vector<expr_ref_vector> get_partition(model& mdl);
+
+        /**
+         * Extract shared occurrences of terms whose sort are 
+         * fid, but appear in a context that is not fid.
+         * for example f(x + y) produces the shared occurrence
+         * x + y when f is uninterpreted and x + y has sort Int or Real.
+         */
+        expr_ref_vector shared_occurrences(family_id fid);
+
     };
 
 }

src/sat/sat_solver.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 
+
 #include <cmath>
 #include "sat/sat_solver.h"
 #include "sat/sat_integrity_checker.h"
@@ -298,6 +299,9 @@ namespace sat {
         if (!c.is_learned()) {
             m_stats.m_non_learned_generation++;
         } 
+        if (c.frozen()) {
+            --m_num_frozen;
+        }
         if (m_config.m_drat && !m_drat.is_cleaned(c)) {
             m_drat.del(c);
         }
@@ -481,9 +485,10 @@ namespace sat {
         }
         unsigned some_idx = c.size() >> 1;
         literal block_lit = c[some_idx];
-        DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
+        VERIFY(!c.frozen());
-        DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
+        DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
-        VERIFY(c[0] != c[1]);
+        DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
+        SASSERT(c[0] != c[1]);
         m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
         m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
         return reinit;
@@ -2139,7 +2144,6 @@ namespace sat {
                 else {
                     c.inc_inact_rounds();
                     if (c.inact_rounds() > m_config.m_gc_k) {
-                        m_num_frozen--;
                         del_clause(c);
                         m_stats.m_gc_clause++;
                         deleted++;

src/sat/sat_solver.h

@@ -682,10 +682,10 @@ namespace sat {
         bool m_deleted;
     public:
         scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
-            s.detach_clause(c);
+            if (!c.frozen()) s.detach_clause(c);
         }            
         ~scoped_detach() {
-            if (!m_deleted) s.attach_clause(c);
+            if (!m_deleted && !c.frozen()) s.attach_clause(c);
         }
         
         void del_clause() {

src/smt/theory_lra.cpp

@@ -1168,7 +1168,9 @@ public:
         if (m_variable_values.count(vi) > 0)
             return m_variable_values[vi];
         
-        SASSERT (m_solver->is_term(vi));
+        if(!m_solver->is_term(vi))
+            return rational::zero();
+        
         m_todo_terms.push_back(std::make_pair(vi, rational::one()));
         rational result(0);
         while (!m_todo_terms.empty()) {

src/tactic/goal.cpp

@@ -733,7 +733,9 @@ bool goal::is_cnf() const {
 bool goal::is_literal(expr* f) const {
     m_manager.is_not(f, f);
     if (!is_app(f)) return false;
-    if (to_app(f)->get_family_id() == m_manager.get_basic_family_id() &&
+    if (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) {
-        !m_manager.is_false(f) && !m_manager.is_true(f)) return false;
+        for (expr* arg : *to_app(f)) 
+            if (m_manager.is_bool(arg)) return false;
+    }
     return true;
 }

src/util/lp/lar_solver.cpp

@@ -1507,11 +1507,6 @@ bool lar_solver::column_is_fixed(unsigned j) const {
     return m_mpq_lar_core_solver.column_is_fixed(j);
 }
 
-    
-bool lar_solver::ext_var_is_int(var_index ext_var) const {
-    return m_var_register.external_is_int(ext_var);
-}
-
 // below is the initialization functionality of lar_solver
 
 bool lar_solver::strategy_is_undecided() const {

src/util/lp/lar_solver.h

@@ -155,8 +155,6 @@ public:
 
     bool var_is_int(var_index v) const;
 
-    bool ext_var_is_int(var_index ext_var) const;
-    
     void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int);
 
     void add_new_var_to_core_fields_for_doubles(bool register_in_basis);

src/util/lp/var_register.h

@@ -19,19 +19,19 @@ Revision History:
 #pragma once
 namespace lp  {
 class ext_var_info {
-    unsigned m_internal_j; // the internal index
+    unsigned m_external_j; // the internal index
     bool m_is_integer;
 public:
     ext_var_info() {}
     ext_var_info(unsigned j): ext_var_info(j, true) {}
-    ext_var_info(unsigned j , bool is_int) : m_internal_j(j), m_is_integer(is_int) {}
+    ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {}
-    unsigned internal_j() const { return m_internal_j;}
+    unsigned external_j() const { return m_external_j;}
     bool is_integer() const {return m_is_integer;}
 };
 
 class var_register {
-    svector<unsigned> m_local_to_external;
+    svector<ext_var_info> m_local_to_external;
-    std::unordered_map<unsigned, ext_var_info> m_external_to_local;
+    std::unordered_map<unsigned, unsigned> m_external_to_local;
 public:
     unsigned add_var(unsigned user_var) {
         return add_var(user_var, true);
@@ -39,19 +39,23 @@ public:
     unsigned add_var(unsigned user_var, bool is_int) {
         auto t = m_external_to_local.find(user_var);
         if (t != m_external_to_local.end()) {
-            return t->second.internal_j();
+            return t->second;
         }
 
-        unsigned j = size();
+        m_local_to_external.push_back(ext_var_info(user_var, is_int));
-        m_external_to_local[user_var] = ext_var_info(j, is_int);
+        return m_external_to_local[user_var] = size() - 1;
-        m_local_to_external.push_back(user_var);
-        return j;
     }
 
-    const svector<unsigned> & vars() const { return m_local_to_external; }
+    svector<unsigned> vars() const {
+        svector<unsigned> ret;
+        for (const auto& p : m_local_to_external) {
+            ret.push_back(p.external_j());
+        }
+        return ret;
+    }
     
     unsigned local_to_external(unsigned local_var) const {
-        return m_local_to_external[local_var];
+        return m_local_to_external[local_var].external_j();
     }
     unsigned size() const {
         return m_local_to_external.size();
@@ -64,13 +68,7 @@ public:
     unsigned external_to_local(unsigned j) const {
         auto it = m_external_to_local.find(j);
         lp_assert(it != m_external_to_local.end());
-        return it->second.internal_j();
+        return it->second;
-    }
-
-    bool external_is_int(unsigned j) const {
-        auto it = m_external_to_local.find(j);
-        lp_assert(it != m_external_to_local.end());
-        return it->second.is_integer();
     }
 
     bool external_is_used(unsigned ext_j) const {
@@ -82,7 +80,7 @@ public:
         auto it = m_external_to_local.find(ext_j);
         if ( it == m_external_to_local.end())
             return false;
-        local_j = it->second.internal_j();
+        local_j = it->second;
         return true;
     }
 
@@ -90,19 +88,19 @@ public:
         auto it = m_external_to_local.find(ext_j);
         if ( it == m_external_to_local.end())
             return false;
-        local_j = it->second.internal_j();
+        local_j = it->second;
-        is_int = it->second.is_integer();
+        is_int = m_local_to_external[local_j].is_integer();
         return true;
     }
 
     
     bool local_is_int(unsigned j) const {
-        return external_is_int(m_local_to_external[j]);
+        return m_local_to_external[j].is_integer();
     }
 
     void shrink(unsigned shrunk_size) {
         for (unsigned j = size(); j-- > shrunk_size;) {
-            m_external_to_local.erase(m_local_to_external[j]);
+            m_external_to_local.erase(m_local_to_external[j].external_j());
         }
         m_local_to_external.resize(shrunk_size);
     }