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

src/api/api_numeral.cpp

@@ -68,8 +68,10 @@ extern "C" {
                 (' ' == *m) || ('\n' == *m) ||
                 ('.' == *m) || ('e' == *m) ||
                 ('E' == *m) ||
-                ('p' == *m && is_float) ||
+                (is_float &&
-                ('P' == *m && is_float))) {
+                    ('p' == *m) ||
+                    ('P' == *m) ||
+                    ('+' == *m)))) {
                 SET_ERROR_CODE(Z3_PARSER_ERROR);
                 return 0;
             }

src/api/python/z3.py

@@ -8099,10 +8099,6 @@ class FPRef(ExprRef):
     def __gt__(self, other):
         return fpGT(self, other, self.ctx)
 
-    def __ne__(self, other):
-        return fpNEQ(self, other, self.ctx)
-
-
     def __add__(self, other):
         """Create the Z3 expression `self + other`.
 
@@ -8824,7 +8820,7 @@ def _check_fp_args(a, b):
         _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression")
 
 def fpLT(a, b, ctx=None):
-    """Create the Z3 floating-point expression `other <= self`.
+    """Create the Z3 floating-point expression `other < self`.
 
     >>> x, y = FPs('x y', FPSort(8, 24))
     >>> fpLT(x, y)
@@ -8846,7 +8842,7 @@ def fpLEQ(a, b, ctx=None):
     return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
 
 def fpGT(a, b, ctx=None):
-    """Create the Z3 floating-point expression `other <= self`.
+    """Create the Z3 floating-point expression `other > self`.
 
     >>> x, y = FPs('x y', FPSort(8, 24))
     >>> fpGT(x, y)
@@ -8857,11 +8853,9 @@ def fpGT(a, b, ctx=None):
     return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
 
 def fpGEQ(a, b, ctx=None):
-    """Create the Z3 floating-point expression `other <= self`.
+    """Create the Z3 floating-point expression `other >= self`.
 
     >>> x, y = FPs('x y', FPSort(8, 24))
-    >>> x + y
-    x + y
     >>> fpGEQ(x, y)
     x >= y
     >>> (x >= y).sexpr()
@@ -8870,7 +8864,7 @@ def fpGEQ(a, b, ctx=None):
     return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
 
 def fpEQ(a, b, ctx=None):
-    """Create the Z3 floating-point expression `other <= self`.
+    """Create the Z3 floating-point expression `fpEQ(other, self)`.
 
     >>> x, y = FPs('x y', FPSort(8, 24))
     >>> fpEQ(x, y)
@@ -8881,7 +8875,7 @@ def fpEQ(a, b, ctx=None):
     return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
 
 def fpNEQ(a, b, ctx=None):
-    """Create the Z3 floating-point expression `other <= self`.
+    """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
 
     >>> x, y = FPs('x y', FPSort(8, 24))
     >>> fpNEQ(x, y)

src/math/automata/symbolic_automata.h

@@ -79,16 +79,18 @@ class symbolic_automata {
             return m_rep;
         }
 
-        void add(unsigned i) { m_set.insert(i); }
+        void insert(unsigned i) { m_set.insert(i); }
         bool contains(unsigned i) const { return m_set.contains(i); }        
         bool is_empty() const { return m_set.empty(); }
         unsigned size() const { return m_set.num_elems(); }
         void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; }        
         void clear() { m_set.reset(); m_rep_chosen = false; }
-        uint_set::iterator begin() { return m_set.begin(); }
+        uint_set::iterator begin() const { return m_set.begin(); }
-        uint_set::iterator end() { return m_set.end(); }
+        uint_set::iterator end() const { return m_set.end(); }
     };
 
+    void add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W);
+
 public:
     symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
     automaton_t* mk_determinstic(automaton_t& a);
@@ -96,6 +98,8 @@ public:
     automaton_t* remove_epsilons(automaton_t& a);
     automaton_t* mk_total(automaton_t& a);
     automaton_t* mk_minimize(automaton_t& a);
+    automaton_t* mk_minimize_total(automaton_t& a);
+    automaton_t* mk_difference(automaton_t& a, automaton_t& b);
     automaton_t* mk_product(automaton_t& a, automaton_t& b);
 };
 

src/math/automata/symbolic_automata_def.h

@@ -35,7 +35,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total
     moves_t mvs, new_mvs;
     for (unsigned i = 0; i < dead_state; ++i) {
         mvs.reset();
-        a.get_moves(i, mvs, true);
+        a.get_moves_from(i, mvs, true);
         refs_t vs(m);
         
         for (unsigned j = 0; j < mvs.size(); ++j) {
@@ -54,7 +54,8 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total
         return a.clone();
     }
     new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true()));
-    automaton_t::append_moves(0, a, new_mvs);
+
+    // TBD private: automaton_t::append_moves(0, a, new_mvs);
     
     return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs);        
 }
@@ -74,45 +75,69 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
     if (!fa) {
         return 0;
     }
-    
+    return mk_minimize_total(*fa.get());
-    block final_block(fa->final_states());
+}
-    block non_final_block(fa->non_final_states());
+
-    vector<block> blocks;
+
-    for (unsigned i = 0; i < fa->num_states(); ++i) {
+template<class T, class M>
-        if (fa->is_final_state(i)) {
+void symbolic_automata<T, M>::add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W) {
-            blocks.push_back(final_block);
+    block& p0 = pblocks[p0_index];
+    if (p1.size() < p0.size()) {
+        unsigned p1_index = pblocks.size();
+        pblocks.push_back(p1);
+        for (uint_set::iterator it = p1.begin(), end = p1.end(); it != end; ++it) {
+            p0.remove(*it);
+            blocks[*it] = p1_index;
+        }
+        if (W.contains(p0_index)) {
+            W.push_back(p1_index);
+        }
+        else if (p0.size() <= p1.size()) {
+            W.push_back(p0_index);
         }
         else {
-            blocks.push_back(non_final_block);
+            W.push_back(p1_index);
+        }
+    }                
+}
+
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize_total(automaton_t& a) {    
+    vector<block> pblocks;
+    unsigned_vector blocks;
+    unsigned_vector non_final;
+    for (unsigned i = 0; i < a.num_states(); ++i) {
+        if (!a.is_final_state(i)) {
+            non_final.push_back(i);
+            blocks.push_back(1);
+        }
+        else {
+            blocks.push_back(0);
         }
     }
-    vector<block> W;
+    pblocks.push_back(block(a.final_states()));      // 0 |-> final states
-    if (final_block.size() > non_final_block.size()) {
+    pblocks.push_back(block(non_final));             // 1 |-> non-final states
-        W.push_back(non_final_block);
+
-    }
+    unsigned_vector W;
-    else {
+    W.push_back(pblocks[0].size() > pblocks[1].size() ? 1 : 0);
-        W.push_back(final_block);
+        
-    }
-    
-#if 0
-    
     refs_t trail(m);
     u_map<T*> gamma;
     moves_t mvs;
     while (!W.empty()) {
-        block R(W.back());
+        block R(pblocks[W.back()]);
         W.pop_back();
-        block Rcopy(R);
         gamma.reset();
-        uint_set::iterator it = Rcopy.begin(), end = Rcopy.end();
+        uint_set::iterator it = R.begin(), end = R.end();
         for (; it != end; ++it) {
-            unsigned q = *it;
+            unsigned dst = *it;
             mvs.reset();
-            fa->get_moves_to(q, mvs);
+            a.get_moves_to(dst, mvs);
             for (unsigned i = 0; i < mvs.size(); ++i) {
                 unsigned src = mvs[i].src();
-                if (blocks[src].size() > 1) {
+                if (pblocks[src].size() > 1) {
-                    T* t = mvs[i]();
+                    T* t = mvs[i].t();
+                    T* t1;
                     if (gamma.find(src, t1)) {
                         t = m_ba.mk_or(t, t1);
                         trail.push_back(t);
@@ -121,17 +146,132 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
                 }
             }
         }
-        hashtable<block*> relevant;
+        uint_set relevant1;
-        u_map<T*>::iterator end = gamma.end();
+        typedef typename u_map<T*>::iterator gamma_iterator;
-        for (u_map<T*>::iterator it = gamma.begin(); it != end; ++it) {
+        gamma_iterator gend = gamma.end();
-            relevant.insert(blocks[it->m_key]);
+        for (gamma_iterator git = gamma.begin(); git != gend; ++git) {
+            unsigned p0A_index = blocks[git->m_key];
+            if (relevant1.contains(p0A_index)) {
+                continue;
+            }
+            relevant1.insert(p0A_index);
+            block& p0A = pblocks[p0A_index];
+            block p1;
+            for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
+                if (p0A.contains(it->m_key)) p1.insert(it->m_key);
+            }
+            
+            add_block(p1, p0A_index, blocks, pblocks, W);
+
+            bool iterate = true;
+            while (iterate) {
+                iterate = false;
+                uint_set relevant2;
+                for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
+                    unsigned p0B_index = blocks[it->m_key];
+                    if (pblocks[p0B_index].size() <= 1 || relevant2.contains(p0B_index)) {
+                        continue;
+                    }
+                    relevant2.insert(p0B_index);
+                    block const& p0B = pblocks[p0B_index];
+                    uint_set::iterator bi = p0B.begin(), be = p0B.end();
+
+                    block p1;
+                    p1.insert(*bi);
+                    bool split_found = false;
+                    ref_t psi(gamma[*bi], m); 
+                    ++bi;
+                    for (; bi != be; ++bi) {
+                        unsigned q = *bi;
+                        ref_t phi(gamma[q], m);
+                        if (split_found) {
+                            ref_t phi_and_psi(m_ba.mk_and(phi, psi), m);
+                            switch (m_ba.is_sat(phi_and_psi)) {
+                            case l_true:
+                                p1.insert(q);
+                                break;
+                            case l_undef:
+                                return 0;
+                            default:
+                                break;
+                            }                            
+                        }
+                        else {
+                            ref_t psi_min_phi(m_ba.mk_and(psi, m_ba.mk_not(phi)), m);
+                            lbool is_sat = m_ba.is_sat(psi_min_phi);
+                            if (is_sat == l_undef) {
+                                return 0;
+                            }
+                            if (is_sat == l_true) {
+                                psi = psi_min_phi;
+                                split_found = true;
+                                continue;
+                            }
+                            // psi is a subset of phi
+                            ref_t phi_min_psi(m_ba.mk_and(phi, m_ba.mk_not(psi)), m);
+                            is_sat = m_ba.is_sat(phi_min_psi);
+                            if (is_sat == l_undef) {
+                                return 0;
+                            }
+                            else if (is_sat == l_false) {
+                                p1.insert(q); // psi and phi are equivalent
+                            }
+                            else {
+                                p1.clear();
+                                p1.insert(q);
+                                psi = phi_min_psi;
+                                split_found = true;
+                            }
+                        }
+                    }
+                    if (p1.size() < p0B.size() && p0B.size() > 2) iterate = true;
+                    add_block(p1, p0B_index, blocks, pblocks, W);
+                }
+            }
         }
-        
     }
-#endif
+
-    
+    unsigned new_init = pblocks[blocks[a.init()]].get_representative();
-    return 0;
+
-        
+    // set moves
+    map<unsigned_pair, T*, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > conds;
+    svector<unsigned_pair> keys;
+    moves_t new_moves;
+
+    for (unsigned i = 0; i < a.num_states(); ++i) {
+        unsigned src = pblocks[blocks[i]].get_representative();
+        typename automaton_t::moves const& mvs = a.get_moves_from(i);
+        for (unsigned j = 0; j < mvs.size(); ++j) {
+            unsigned dst = pblocks[blocks[mvs[j].dst()]].get_representative();
+            unsigned_pair st(src, dst);
+            T* t = 0;
+            if (conds.find(st, t)) {
+                t = m_ba.mk_or(t, mvs[j].t());
+                trail.push_back(t);
+                conds.insert(st, t);
+            }
+            else {
+                conds.insert(st, mvs[j].t());
+                keys.push_back(st);
+            }
+        }
+    }    
+    for (unsigned i = 0; i < keys.size(); ++i) {
+        unsigned_pair st = keys[i];
+        new_moves.push_back(move_t(m, st.first, st.second, conds[st]));
+    }
+    // set final states.
+    unsigned_vector new_final;
+    uint_set new_final_set;
+    for (unsigned i = 0; i < a.final_states().size(); ++i) {
+        unsigned f = pblocks[blocks[a.final_states()[i]]].get_representative();
+        if (!new_final_set.contains(f)) {
+            new_final_set.insert(f);
+            new_final.push_back(f);
+        }
+    }
+
+    return alloc(automaton_t, m, new_init, new_final, new_moves);
 }
 
 template<class T, class M>
@@ -146,6 +286,9 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
     if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
         final.push_back(0);
     }
+    if (false) {
+        mk_minimize(a);
+    }
     unsigned n = 1;
     moves_t mvsA, mvsB;
     while (!todo.empty()) {

src/muz/rel/dl_base.h

@@ -435,11 +435,7 @@ namespace datalog {
             void destroy() {
                 SASSERT(this);
                 this->~base_ancestor();
-#if _DEBUG
-                memory::deallocate(__FILE__, __LINE__, this);
-#else
                 memory::deallocate(this);
-#endif
             }
         public:
             /**

src/tactic/bv/bv_bounds_tactic.cpp

@@ -22,7 +22,7 @@ Author:
 #include "ast_pp.h"
 #include <climits>
 
-static uint64_t uMaxInt(unsigned sz) {
+static uint64 uMaxInt(unsigned sz) {
     SASSERT(sz <= 64);
     return ULLONG_MAX >> (64u - sz);
 }
@@ -32,12 +32,12 @@ namespace {
 struct interval {
     // l < h: [l, h]
     // l > h: [0, h] U [l, UMAX_INT]
-    uint64_t l, h;
+    uint64 l, h;
     unsigned sz;
     bool tight;
 
     interval() {}
-    interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
+    interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
         // canonicalize full set
         if (is_wrapped() && l == h + 1) {
             this->l = 0;
@@ -164,7 +164,7 @@ struct undo_bound {
 class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     typedef obj_map<expr, interval> map;
     typedef obj_map<expr, bool> expr_set;
-    typedef obj_map<expr, expr_set*> expr_list_map;
+    typedef obj_map<expr, unsigned> expr_cnt;
 
     ast_manager&       m;
     params_ref         m_params;
@@ -172,10 +172,10 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     bv_util            m_bv;
     vector<undo_bound> m_scopes;
     map                m_bound;
-    expr_list_map      m_expr_vars;
+    svector<expr_set*> m_expr_vars;
-    expr_set           m_bound_exprs;
+    svector<expr_cnt*> m_bound_exprs;
 
-    bool is_number(expr *e, uint64_t& n, unsigned& sz) const {
+    bool is_number(expr *e, uint64& n, unsigned& sz) const {
         rational r;
         if (m_bv.is_numeral(e, r, sz) && sz <= 64) {
             n = r.get_uint64();
@@ -185,7 +185,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     }
 
     bool is_bound(expr *e, expr*& v, interval& b) const {
-        uint64_t n;
+        uint64 n;
         expr *lhs, *rhs;
         unsigned sz;
 
@@ -233,7 +233,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     }
 
     expr_set* get_expr_vars(expr* t) {
-        expr_set*& entry = m_expr_vars.insert_if_not_there2(t, 0)->get_data().m_value;
+        unsigned id = t->get_id();
+        m_expr_vars.reserve(id + 1);
+        expr_set*& entry = m_expr_vars[id];
         if (entry)
             return entry;
 
@@ -256,23 +258,33 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
         return set;
     }
 
-    bool expr_has_bounds(expr* t) {
+    expr_cnt* get_expr_bounds(expr* t) {
-        bool has_bounds = false;
+        unsigned id = t->get_id();
-        if (m_bound_exprs.find(t, has_bounds))
+        m_bound_exprs.reserve(id + 1);
-            return has_bounds;
+        expr_cnt*& entry = m_bound_exprs[id];
+        if (entry)
+            return entry;
+
+        expr_cnt* set = alloc(expr_cnt);
+        entry = set;
+
+        if (!is_app(t))
+            return set;
+
+        interval b;
+        expr* e;
+        if (is_bound(t, e, b)) {
+            set->insert_if_not_there2(e, 0)->get_data().m_value++;
+        }
 
         app* a = to_app(t);
-        if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) &&
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
-            (m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1)))) {
+            expr_cnt* set_arg = get_expr_bounds(a->get_arg(i));
-            has_bounds = true;
+            for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
+                set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value;
+            }
         }
-
+        return set;
-        for (unsigned i = 0; !has_bounds && i < a->get_num_args(); ++i) {
-            has_bounds = expr_has_bounds(a->get_arg(i));
-        }
-
-        m_bound_exprs.insert(t, has_bounds);
-        return has_bounds;
     }
 
 public:
@@ -289,8 +301,11 @@ public:
     }
 
     virtual ~bv_bounds_simplifier() {
-        for (expr_list_map::iterator I = m_expr_vars.begin(), E = m_expr_vars.end(); I != E; ++I) {
+        for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) {
-            dealloc(I->m_value);
+            dealloc(m_expr_vars[i]);
+        }
+        for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) {
+            dealloc(m_bound_exprs[i]);
         }
     }
 
@@ -393,7 +408,13 @@ public:
         if (is_bound(t, t1, b)) {
             return b.is_full() || m_bound.contains(t1);
         }
-        return expr_has_bounds(t);
+
+        expr_cnt* bounds = get_expr_bounds(t);
+        for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) {
+            if (I->m_value > 1 || m_bound.contains(I->m_key))
+                return true;
+        }
+        return false;
     }
 
     virtual void pop(unsigned num_scopes) {

src/util/memory_manager.cpp

@@ -198,7 +198,7 @@ void memory::display_i_max_usage(std::ostream & os) {
               << "\n";
 }
 
-#if _DEBUG
+#if Z3DEBUG
 void memory::deallocate(char const * file, int line, void * p) {
     deallocate(p);
     TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";););

src/util/memory_manager.h

@@ -60,7 +60,7 @@ public:
     static void deallocate(void* p);
     static ALLOC_ATTR void* allocate(size_t s);
     static ALLOC_ATTR void* reallocate(void *p, size_t s);
-#if _DEBUG
+#if Z3DEBUG
     static void deallocate(char const* file, int line, void* p);
     static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
 #endif

src/util/mpf.cpp

@@ -205,15 +205,23 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
     // We expect [i].[f]P[e], where P means that the exponent is interpreted as 2^e instead of 10^e.
 
     std::string v(value);
-    size_t e_pos = v.find('p');
-    if (e_pos == std::string::npos) e_pos = v.find('P');
 
     std::string f, e;
+    bool sgn = false;
 
+    if (v.substr(0, 1) == "-") {
+        sgn = true;
+        v = v.substr(1);
+    }
+    else if (v.substr(0, 1) == "+")
+        v = v.substr(1);
+
+    size_t e_pos = v.find('p');
+    if (e_pos == std::string::npos) e_pos = v.find('P');
     f = (e_pos != std::string::npos) ? v.substr(0, e_pos) : v;
     e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0";
 
-    TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;);
+    TRACE("mpf_dbg", tout << "sgn = " << sgn << " f = " << f << " e = " << e << std::endl;);
 
     scoped_mpq q(m_mpq_manager);
     m_mpq_manager.set(q, f.c_str());
@@ -222,6 +230,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
     m_mpz_manager.set(ex, e.c_str());
 
     set(o, ebits, sbits, rm, ex, q);
+    o.sign = sgn;
 
     TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;);
 }