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

src/muz_qe/dl_base.cpp

@@ -325,9 +325,20 @@ namespace datalog {
         return res;
     }
 
+    /**
+       \brief Default method for complementation.
+
+       It assumes that the compiler creates only tables with
+       at most one column (0 or 1 columns).       
+       Complementation of tables with more than one columns
+       is transformed into a cross product of complements and/or
+       difference. 
+
+     */
     table_base * table_base::complement(func_decl* p, const table_element * func_columns) const {
         const table_signature & sig = get_signature();
         SASSERT(sig.functional_columns()==0 || func_columns!=0);
+        SASSERT(sig.first_functional() <= 1);
 
         table_base * res = get_plugin().mk_empty(sig);
 
@@ -342,9 +353,7 @@ namespace datalog {
             return res;
         }
 
-        if(sig.first_functional()!=1) { //now we support only tables with one non-functional column
+        VERIFY(sig.first_functional() == 1);
-            NOT_IMPLEMENTED_YET();
-        }
 
         uint64 upper_bound = get_signature()[0];
         bool empty_table = empty();
@@ -363,44 +372,6 @@ namespace datalog {
             }
         }
         return res;
-#if 0
-        svector<unsigned> var_arg_indexes(arity);
-        var_arg_indexes.fill(0);
-
-        svector<unsigned> var_arg_domain_sizes = s;
-
-        unsigned var_cnt=var_arg_indexes.size();
-        table_fact fact;
-        fact.resize(arity);
-        fact.fill(0);
-        unsigned depth=arity;
-
-        while(true) {
-            if(depth==arity) {
-                SASSERT(!res->contains_fact(fact));
-                if(empty_table || !contains_fact(fact)) {
-                    res->add_fact(fact);
-                }
-                depth--;
-            }
-            else if(fact[depth]==s[depth]-1) {
-                val_indexes[depth]=0;
-                if(depth==0) {
-                    break;
-                }
-                depth--;
-            }
-            else {
-                SASSERT(val_indexes[depth]<var_arg_domain_sizes[depth]);
-                unsigned arg_idx = var_arg_indexes[depth];
-                unsigned val_idx = val_indexes[depth]++;
-                head_args[arg_idx]=ctx.get_arith().mk_numeral(rational(val_idx), true);
-                depth++;
-            }
-        }
-
-        return res;
-#endif
     }
     
     void table_base::display(std::ostream & out) const {
@@ -468,6 +439,7 @@ namespace datalog {
         expr_ref_vector disjs(m);
         expr_ref_vector conjs(m);
         dl_decl_util util(m);
+        bool_rewriter brw(m);
         table_fact fact;
         iterator it = begin();
         iterator iend = end();
@@ -478,13 +450,10 @@ namespace datalog {
             for (unsigned i = 0; i < fact.size(); ++i) {
                 conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i])));
             }
-            switch(conjs.size()) {
+            brw.mk_and(conjs.size(), conjs.c_ptr(), fml);
-            case 0: disjs.push_back(m.mk_true()); break;
+            disjs.push_back(fml);
-            case 1: disjs.push_back(conjs[0].get()); break;
-            default: disjs.push_back(m.mk_and(conjs.size(), conjs.c_ptr())); break;
         }
-        }
+        brw.mk_or(disjs.size(), disjs.c_ptr(), fml);        
-        bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), fml);        
     }
 
 }

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -325,7 +325,6 @@ namespace datalog {
         TRACE("dl", m_hb.display(tout););
         SASSERT(is_sat == l_true);
         unsigned basis_size = m_hb.get_basis_size();
-        bool first_initial = true;
         for (unsigned i = 0; i < basis_size; ++i) {
             bool is_initial;
             vector<rational> soln;
@@ -378,7 +377,6 @@ namespace datalog {
     }
 
     void mk_karr_invariants::update_body(rule_set& rules, rule& r){
-        func_decl* p = r.get_decl();        
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz  = r.get_tail_size();
         app_ref_vector tail(m);

src/muz_qe/dl_relation_manager.cpp

@@ -245,7 +245,6 @@ namespace datalog {
         relation_plugin * res = try_get_appropriate_plugin(s);
         if (!res) {
             throw default_exception("no suitable plugin found for given relation signature");
-            throw 0;
         }
         return *res;
     }

src/muz_qe/horn_tactic.cpp

@@ -169,7 +169,6 @@ class horn_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("horn", *g);
-            bool produce_models = g->models_enabled();
             bool produce_proofs = g->proofs_enabled();
 
             if (produce_proofs) {

src/muz_qe/rel_context.cpp

@@ -31,9 +31,6 @@ Revision History:
 #include"dl_sparse_table.h"
 #include"dl_table.h"
 #include"dl_table_relation.h"
-#ifndef _EXTERNAL_RELEASE
-#include"dl_skip_table.h"
-#endif
 
 namespace datalog {
    
@@ -44,14 +41,14 @@ namespace datalog {
           m_answer(m), 
           m_cancel(false), 
           m_last_result_relation(0) {
+
+        // register plugins for builtin tables
+
         get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
         get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
         get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
         get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
 
-#ifndef _EXTERNAL_RELEASE
-        get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
-#endif
 
         // register plugins for builtin relations