Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/ast/ast.cpp

@@ -2755,7 +2755,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
         app const * cls   = to_app(f1);
         unsigned num_args = cls->get_num_args();
 #ifdef Z3DEBUG
-        vector<bool> found;
+        svector<bool> found;
 #endif
         for (unsigned i = 0; i < num_args; i++) {
             expr * lit = cls->get_arg(i);

src/ast/dl_decl_plugin.cpp

@@ -660,9 +660,9 @@ namespace datalog {
         return 0;
     }
 
-    bool dl_decl_util::is_numeral(expr* e, uint64& v) const {
+    bool dl_decl_util::is_numeral(const expr* e, uint64& v) const {
         if (is_numeral(e)) {
-            app* c = to_app(e);
+            const app* c = to_app(e);
             SASSERT(c->get_decl()->get_num_parameters() == 2);
             parameter const& p = c->get_decl()->get_parameter(0);
             SASSERT(p.is_rational());

src/ast/dl_decl_plugin.h

@@ -169,11 +169,11 @@ namespace datalog {
 
         app* mk_le(expr* a, expr* b);
 
-        bool is_lt(expr* a) { return is_app_of(a, m_fid, OP_DL_LT); }
+        bool is_lt(const expr* a) const { return is_app_of(a, m_fid, OP_DL_LT); }
 
-        bool is_numeral(expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); }
+        bool is_numeral(const expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); }
 
-        bool is_numeral(expr* e, uint64& v) const;
+        bool is_numeral(const expr* e, uint64& v) const;
 
         //
         // Utilities for extracting constants 

src/muz_qe/dl_compiler.cpp

@@ -803,17 +803,15 @@ namespace datalog {
         context& m_context;
         item_set & m_removed;
         svector<T> m_stack;
-        ast_mark m_stack_content;
         ast_mark m_visited;
 
         void traverse(T v) {
-            SASSERT(!m_stack_content.is_marked(v));
+            SASSERT(!m_visited.is_marked(v));
-            if(m_visited.is_marked(v) || m_removed.contains(v)) {
+            if (m_removed.contains(v)) {
                 return;
             }
 
             m_stack.push_back(v);
-            m_stack_content.mark(v, true);
             m_visited.mark(v, true);
 
             const item_set & deps = m_deps.get_deps(v);
@@ -821,33 +819,34 @@ namespace datalog {
             item_set::iterator end = deps.end();
             for(; it!=end; ++it) {
                 T d = *it;
-                if(m_stack_content.is_marked(d)) {
+                if (m_visited.is_marked(d)) {
                     //TODO: find the best vertex to remove in the cycle
                     remove_from_stack();
-                    break;
+                    continue;
                 }
                 traverse(d);
             }
             SASSERT(m_stack.back()==v);
 
             m_stack.pop_back();
-            m_stack_content.mark(v, false);
+            m_visited.mark(v, false);
         }
 
         void remove_from_stack() {
             for (unsigned i = 0; i < m_stack.size(); ++i) {
                 func_decl* p = m_stack[i];
-                rule_vector const& rules = m_rules.get_predicate_rules(p);
-                unsigned stratum = m_rules.get_predicate_strat(p);
                 if (m_context.has_facts(p)) {
                     m_removed.insert(p);
                     return;
                 }
+
+                rule_vector const& rules = m_rules.get_predicate_rules(p);
+                unsigned stratum = m_rules.get_predicate_strat(p);
                 for (unsigned j = 0; j < rules.size(); ++j) {
                     rule const& r = *rules[j];
                     bool ok = true;
                     for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
-                        ok &= m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
+                        ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
                     }
                     if (ok) {
                         m_removed.insert(p);
@@ -858,8 +857,8 @@ namespace datalog {
 
             // nothing was found.
             m_removed.insert(m_stack.back());
-
         }
+
     public:
         cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed) 
             : m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }

src/muz_qe/dl_sparse_table.cpp

@@ -1022,19 +1022,16 @@ namespace datalog {
 
 
     class sparse_table_plugin::rename_fn : public convenient_table_rename_fn {
-        const unsigned m_cycle_len;
-        const unsigned m_col_cnt;
         unsigned_vector m_out_of_cycle;
     public:
         rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) 
-            : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle), 
+            : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) {
-            m_cycle_len(permutation_cycle_len), m_col_cnt(orig_sig.size()) {
                 SASSERT(permutation_cycle_len>=2);
                 idx_set cycle_cols;
-                for (unsigned i=0; i<m_cycle_len; i++) {
+                for (unsigned i=0; i < permutation_cycle_len; ++i) {
                     cycle_cols.insert(permutation_cycle[i]);
                 }
-                for (unsigned i=0; i<m_col_cnt; i++) {
+                for (unsigned i=0; i < orig_sig.size(); ++i) {
                     if (!cycle_cols.contains(i)) {
                         m_out_of_cycle.push_back(i);
                     }
@@ -1045,10 +1042,10 @@ namespace datalog {
             const sparse_table::column_layout & src_layout, 
             const sparse_table::column_layout & tgt_layout) {
 
-                for (unsigned i=1; i<m_cycle_len; i++) {
+                for (unsigned i=1; i < m_cycle.size(); ++i) {
                     tgt_layout.set(tgt, m_cycle[i-1], src_layout.get(src, m_cycle[i]));
                 }
-                tgt_layout.set(tgt, m_cycle[m_cycle_len-1], src_layout.get(src, m_cycle[0]));
+                tgt_layout.set(tgt, m_cycle[m_cycle.size()-1], src_layout.get(src, m_cycle[0]));
 
                 unsigned_vector::const_iterator it = m_out_of_cycle.begin();
                 unsigned_vector::const_iterator end = m_out_of_cycle.end();

src/muz_qe/pdr_prop_solver.cpp

@@ -145,7 +145,8 @@ namespace pdr {
                     rational two(2);
                     for (unsigned j = 0; j < bv_size; ++j) {
                         parameter p(j);
-                        expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
+                        //expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
+                        expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c));
                         if ((r % two).is_zero()) {
                             e = m.mk_not(e);
                         }

src/shell/datalog_frontend.cpp

@@ -43,17 +43,7 @@ static datalog::context * g_ctx = 0;
 static datalog::rule_set * g_orig_rules;
 static datalog::instruction_block * g_code;
 static datalog::execution_context * g_ectx;
-static smt_params * g_params;
 
-datalog_params::datalog_params():
-    m_default_table("sparse"),
-    m_default_table_checked(false)
-{}
-
-// void datalog_params::register_params(ini_params& p) {
-//    p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)");
-//    p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker");
-// }
 
 static void display_statistics(
     std::ostream& out,
@@ -61,7 +51,6 @@ static void display_statistics(
     datalog::rule_set& orig_rules,
     datalog::instruction_block& code,
     datalog::execution_context& ex_ctx,
-    smt_params& params,
     bool verbose
     ) 
 {
@@ -109,7 +98,7 @@ static void display_statistics(
 
 static void display_statistics() {
     if (g_ctx) {
-        display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, *g_params, true);
+        display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, true);
     }
 }
 
@@ -127,7 +116,6 @@ static void on_ctrl_c(int) {
 
 unsigned read_datalog(char const * file) {
     IF_VERBOSE(1, verbose_stream() << "Z3 Datalog Engine\n";);
-    datalog_params dl_params;
     smt_params     s_params;
     ast_manager m;
     g_overall_time.start();
@@ -135,8 +123,6 @@ unsigned read_datalog(char const * file) {
     signal(SIGINT, on_ctrl_c);
     params_ref params;
     params.set_sym("engine", symbol("datalog"));
-    params.set_sym("default_table", dl_params.m_default_table);
-    params.set_bool("default_table_checked", dl_params.m_default_table_checked);
 
     datalog::context ctx(m, s_params, params);
     datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
@@ -186,7 +172,6 @@ unsigned read_datalog(char const * file) {
     g_orig_rules = &original_rules;
     g_code = &rules_code;
     g_ectx = &ex_ctx;
-    g_params = &s_params;
 
     try {    
         g_piece_timer.reset();
@@ -254,7 +239,6 @@ unsigned read_datalog(char const * file) {
             original_rules, 
             rules_code,
             ex_ctx,
-            s_params,
             false);
 
     }
@@ -266,7 +250,6 @@ unsigned read_datalog(char const * file) {
             original_rules, 
             rules_code,
             ex_ctx,
-            s_params,
             true);
         return ERR_MEMOUT;
     }

src/shell/datalog_frontend.h

@@ -19,11 +19,6 @@ Revision History:
 #ifndef _DATALOG_FRONTEND_H_
 #define _DATALOG_FRONTEND_H_
 
-struct datalog_params {
-    symbol m_default_table;
-    bool   m_default_table_checked;
-    datalog_params();
-};
 
 unsigned read_datalog(char const * file);
 

src/shell/main.cpp

@@ -27,8 +27,8 @@ Revision History:
 #include"z3_log_frontend.h"
 #include"warning.h"
 #include"version.h"
-#include"datalog_frontend.h"
 #include"dimacs_frontend.h"
+#include"datalog_frontend.h"
 #include"timeout.h"
 #include"z3_exception.h"
 #include"error_codes.h"

src/util/bit_vector.cpp

@@ -208,8 +208,8 @@ void bit_vector::display(std::ostream & out) const {
 
 void fr_bit_vector::reset() {
     unsigned sz = size();
-    vector<unsigned>::const_iterator it  = m_one_idxs.begin();
+    unsigned_vector::const_iterator it  = m_one_idxs.begin();
-    vector<unsigned>::const_iterator end = m_one_idxs.end();
+    unsigned_vector::const_iterator end = m_one_idxs.end();
     for (; it != end; ++it) {
         unsigned idx = *it;
         if (idx < sz)
@@ -217,5 +217,3 @@ void fr_bit_vector::reset() {
     }
     m_one_idxs.reset();
 }
-
-

src/util/bit_vector.h

@@ -204,7 +204,7 @@ inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {
    This class should be used if the reset is frequently called.
 */
 class fr_bit_vector : private bit_vector {
-    svector<unsigned> m_one_idxs;
+    unsigned_vector m_one_idxs;
 public:
     void reset();
 

src/util/mpff.h

@@ -107,7 +107,7 @@ class mpff_manager {
     
     unsigned          m_precision;      //!< Number of words in the significand. Must be an even number.
     unsigned          m_precision_bits; //!< Number of bits in the significand.  Must be 32*m_precision.
-    vector<unsigned>  m_significands;   //!< Array containing all significands.
+    unsigned_vector   m_significands;   //!< Array containing all significands.
     unsigned          m_capacity;       //!< Number of significands that can be stored in m_significands.
     bool              m_to_plus_inf;    //!< If True, then round to plus infinity, otherwise to minus infinity
     id_gen            m_id_gen;