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

src/muz_qe/dl_context.cpp

@@ -544,14 +544,16 @@ namespace datalog {
     unsigned context::get_num_levels(func_decl* pred) {
         switch(get_engine()) {
         case DATALOG_ENGINE:
-            throw default_exception("get_num_levels is unsupported for datalog engine");
+            throw default_exception("get_num_levels is not supported for datalog engine");
         case PDR_ENGINE:
         case QPDR_ENGINE:
             ensure_pdr();
             return m_pdr->get_num_levels(pred);
         case BMC_ENGINE:
         case QBMC_ENGINE:
-            throw default_exception("get_num_levels is unsupported for bmc");
+            throw default_exception("get_num_levels is not supported for bmc");
+        case TAB_ENGINE:
+            throw default_exception("get_num_levels is not supported for tab");
         default:
             throw default_exception("unknown engine");
         } 
@@ -560,14 +562,16 @@ namespace datalog {
     expr_ref context::get_cover_delta(int level, func_decl* pred) {
         switch(get_engine()) {
         case DATALOG_ENGINE:
-            throw default_exception("operation is unsupported for datalog engine");
+            throw default_exception("operation is not supported for datalog engine");
         case PDR_ENGINE:
         case QPDR_ENGINE:
             ensure_pdr();
             return m_pdr->get_cover_delta(level, pred);
         case BMC_ENGINE:
         case QBMC_ENGINE:
-            throw default_exception("operation is unsupported for BMC engine");
+            throw default_exception("operation is not supported for BMC engine");
+        case TAB_ENGINE:
+            throw default_exception("operation is not supported for TAB engine");
         default:
             throw default_exception("unknown engine");
         } 
@@ -576,7 +580,7 @@ namespace datalog {
     void context::add_cover(int level, func_decl* pred, expr* property) {
         switch(get_engine()) {
         case DATALOG_ENGINE:
-            throw default_exception("operation is unsupported for datalog engine");
+            throw default_exception("operation is not supported for datalog engine");
         case PDR_ENGINE:
         case QPDR_ENGINE:
             ensure_pdr();
@@ -584,7 +588,9 @@ namespace datalog {
             break;
         case BMC_ENGINE:
         case QBMC_ENGINE:
-            throw default_exception("operation is unsupported for BMC engine");
+            throw default_exception("operation is not supported for BMC engine");
+        case TAB_ENGINE:
+            throw default_exception("operation is not supported for TAB engine");
         default:
             throw default_exception("unknown engine");
         } 
@@ -720,7 +726,11 @@ namespace datalog {
         case QBMC_ENGINE:
             check_existential_tail(r);
             check_positive_predicates(r);
-            break;            
+            break;         
+        case TAB_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            break;
         default:
             UNREACHABLE();
             break;
@@ -921,6 +931,7 @@ namespace datalog {
         if (m_pdr.get()) m_pdr->cancel();
         if (m_bmc.get()) m_bmc->cancel();
         if (m_rel.get()) m_rel->cancel();
+        if (m_tab.get()) m_tab->cancel();
     }
 
     void context::cleanup() {
@@ -928,6 +939,7 @@ namespace datalog {
         if (m_pdr.get()) m_pdr->cleanup();
         if (m_bmc.get()) m_bmc->cleanup();
         if (m_rel.get()) m_rel->cleanup();
+        if (m_tab.get()) m_tab->cleanup();
     }
 
     class context::engine_type_proc {
@@ -974,6 +986,9 @@ namespace datalog {
         else if (e == symbol("qbmc")) {
             m_engine = QBMC_ENGINE;
         }
+        else if (e == symbol("tab")) {
+            m_engine = TAB_ENGINE;
+        }
 
         if (m_engine == LAST_ENGINE) {
             expr_fast_mark1 mark;
@@ -1008,6 +1023,8 @@ namespace datalog {
         case BMC_ENGINE:
         case QBMC_ENGINE:
             return bmc_query(query);
+        case TAB_ENGINE:
+            return tab_query(query);
         default:
             UNREACHABLE();
             return rel_query(query);
@@ -1064,6 +1081,17 @@ namespace datalog {
         return m_bmc->query(query);
     }
 
+    void context::ensure_tab() {
+        if (!m_tab.get()) {
+            m_tab = alloc(tab, *this);
+        }
+    }
+
+    lbool context::tab_query(expr* query) {
+        ensure_tab();
+        return m_tab->query(query);
+    }
+
     void context::ensure_rel() {
         if (!m_rel.get()) {
             m_rel = alloc(rel_context, *this);
@@ -1100,6 +1128,10 @@ namespace datalog {
             ensure_rel();
             m_last_answer = m_rel->get_last_answer();
             return m_last_answer.get();
+        case TAB_ENGINE:
+            ensure_tab();
+            m_last_answer = m_tab->get_answer();
+            return m_last_answer.get();
         default:
             UNREACHABLE();
         }
@@ -1120,6 +1152,10 @@ namespace datalog {
             ensure_bmc();
             m_bmc->display_certificate(out);
             return true;
+        case TAB_ENGINE:
+            ensure_tab();
+            m_tab->display_certificate(out);
+            return true;
         default: 
             return false;
         }        
@@ -1151,6 +1187,11 @@ namespace datalog {
                 m_bmc->collect_statistics(st);
             }
             break;
+        case TAB_ENGINE:
+            if (m_tab) {
+                m_tab->collect_statistics(st);
+            }
+            break;
         default: 
             break;
         }

src/muz_qe/dl_context.h

@@ -35,6 +35,7 @@ Revision History:
 #include"dl_rule_set.h"
 #include"pdr_dl_interface.h"
 #include"dl_bmc_engine.h"
+#include"tab_context.h"
 #include"rel_context.h"
 #include"lbool.h"
 #include"statistics.h"
@@ -100,6 +101,7 @@ namespace datalog {
         scoped_ptr<pdr::dl_interface>   m_pdr;
         scoped_ptr<bmc>                 m_bmc;
         scoped_ptr<rel_context>         m_rel;
+        scoped_ptr<tab>                 m_tab;
 
         bool               m_closed;
         bool               m_saturation_was_run;
@@ -434,6 +436,8 @@ namespace datalog {
 
         void ensure_bmc();
 
+        void ensure_tab();
+
         void ensure_rel();
 
         void new_query();
@@ -444,6 +448,8 @@ namespace datalog {
 
         lbool bmc_query(expr* query);
 
+        lbool tab_query(expr* query);
+
         void check_quantifier_free(rule_ref& r);        
         void check_uninterpreted_free(rule_ref& r);
         void check_existential_tail(rule_ref& r);

src/muz_qe/dl_util.h

@@ -52,6 +52,7 @@ namespace datalog {
         QPDR_ENGINE,
         BMC_ENGINE,
         QBMC_ENGINE,
+        TAB_ENGINE,
         LAST_ENGINE
     };
 

src/muz_qe/pdr_farkas_learner.cpp

@@ -860,38 +860,5 @@ namespace pdr {
     }
 
 
-    void farkas_learner::test(char const* filename)  {
-#if 0
-        // [Leo]: disabled because it uses an external component: SMT 1.0 parser
-        if (!filename) {
-            test();
-            return;
-        }
-        ast_manager m;
-        reg_decl_plugins(m);  
-        scoped_ptr<smtlib::parser> p = smtlib::parser::create(m);
-        p->initialize_smtlib();
-
-        if (!p->parse_file(filename)) {
-            warning_msg("Failed to parse file %s\n", filename);
-            return;
-        }
-        expr_ref A(m), B(m);
-
-        smtlib::theory::expr_iterator it = p->get_benchmark()->begin_axioms();
-        smtlib::theory::expr_iterator end = p->get_benchmark()->end_axioms();
-        A = m.mk_and(static_cast<unsigned>(end-it), it);
-
-        it = p->get_benchmark()->begin_formulas();
-        end = p->get_benchmark()->end_formulas();
-        B = m.mk_and(static_cast<unsigned>(end-it), it);
-
-        smt_params params;
-        pdr::farkas_learner fl(params, m);
-        expr_ref_vector lemmas(m);
-        bool res = fl.get_lemma_guesses(A, B, lemmas);        
-        std::cout << "lemmas: " << pp_cube(lemmas, m) << "\n";
-#endif
-    }
 };
 

src/muz_qe/pdr_farkas_learner.h

@@ -99,8 +99,6 @@ public:
 
     void collect_statistics(statistics& st) const;
 
-    static void test(char const* filename);
-
 };
 
 

src/muz_qe/tab_context.cpp

@@ -30,7 +30,9 @@ namespace datalog {
         rule_ref_vector& m_rules;
         rule_ref&        m_rule;
         
-        restore_rule(rule_ref_vector& rules, rule_ref& rule): m_rules(rules), m_rule(rule) {
+        restore_rule(rule_ref_vector& rules, rule_ref& rule): 
+            m_rules(rules),
+            m_rule(rule) {
             m_rules.push_back(m_rule);
         }
         
@@ -40,28 +42,51 @@ namespace datalog {
         }
     };
 
+    enum tab_instruction {
+        SELECT_RULE,
+        SELECT_PREDICATE,
+        BACKTRACK,
+        NEXT_RULE,
+        SATISFIABLE,
+        UNSATISFIABLE,
+        CANCEL
+    };
+
+    std::ostream& operator<<(std::ostream& out, tab_instruction i) {
+        switch(i) {
+        case SELECT_RULE: return out << "select-rule";
+        case SELECT_PREDICATE: return out << "select-predicate";
+        case BACKTRACK: return out << "backtrack";
+        case NEXT_RULE: return out << "next-rule";
+        case SATISFIABLE: return out << "sat";
+        case UNSATISFIABLE: return out << "unsat";
+        case CANCEL: return out << "cancel";
+        }
+        return out << "unmatched instruction";
+    }
+
     class tab::imp {
-        enum instruction {
+        struct stats {
-            SELECT_RULE,
+            stats() { reset(); }
-            SELECT_PREDICATE,
+            void reset() { memset(this, 0, sizeof(*this)); }
-            BACKTRACK,
+            unsigned m_num_unfold;
-            NEXT_RULE,
+            unsigned m_num_no_unfold;
-            SATISFIABLE,
+            unsigned m_num_subsume;
-            UNSATISFIABLE,
-            CANCEL
         };
+
         context&           m_ctx;
         ast_manager&       m;
         rule_manager&      rm;
         rule_unifier       m_unifier;
         rule_set           m_rules;
         trail_stack<imp>   m_trail;
-        instruction        m_instruction;
+        tab_instruction    m_instruction;
         rule_ref           m_query;
         rule_ref_vector    m_query_trail;
         unsigned           m_predicate_index;
         unsigned           m_rule_index;
         volatile bool      m_cancel;
+        stats              m_stats;
     public:
         imp(context& ctx):
             m_ctx(ctx), 
@@ -99,10 +124,12 @@ namespace datalog {
             m_query_trail.reset();
         }
         void reset_statistics() {
-            // TBD
+            m_stats.reset();
         }
         void collect_statistics(statistics& st) const {
-            // TBD
+            st.update("tab.num_unfold", m_stats.m_num_unfold);
+            st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold);
+            st.update("tab.num_subsume", m_stats.m_num_subsume);
         }
         void display_certificate(std::ostream& out) const {
             // TBD
@@ -111,12 +138,13 @@ namespace datalog {
             // TBD
             return expr_ref(0, m);
         }
-private:
+    private:
     
         void select_predicate() {
             unsigned num_predicates = m_query->get_uninterpreted_tail_size();
             if (num_predicates == 0) {
                 m_instruction = UNSATISFIABLE;
+                IF_VERBOSE(1, m_query->display(m_ctx, verbose_stream()); );
             }
             else {
                 m_instruction = SELECT_RULE;
@@ -125,37 +153,47 @@ private:
             }
         }
         
-    void apply_rule(rule const& r) {
+        void apply_rule(rule const& r) {
+            m_rule_index++;
             bool can_unify = m_unifier.unify_rules(*m_query, m_predicate_index, r);
             if (can_unify) {
+                m_stats.m_num_unfold++;
+                m_trail.push_scope();
+                m_trail.push(value_trail<imp,unsigned>(m_rule_index));
+                m_trail.push(value_trail<imp,unsigned>(m_predicate_index));
                 rule_ref new_query(rm);
                 m_unifier.apply(*m_query, m_predicate_index, r, new_query);
                 m_trail.push(restore_rule<imp>(m_query_trail, m_query));
                 m_query = new_query;
                 TRACE("dl", m_query->display(m_ctx, tout););
+                if (l_false == query_is_sat()) {
+                    m_instruction = BACKTRACK;
+                }
+                else if (l_true == query_is_subsumed()) {
+                    NOT_IMPLEMENTED_YET();
+                }
+                else {
+                    m_instruction = SELECT_PREDICATE;
+                }
             }
             else {
-                m_instruction = NEXT_RULE;
+                m_stats.m_num_no_unfold++;
+                m_instruction = SELECT_RULE;
             }
         }
 
         void select_rule() {
             func_decl* p = m_query->get_decl(m_predicate_index);
             rule_vector const& rules = m_rules.get_predicate_rules(p);
-            if (rules.size() >= m_rule_index) {
+            if (rules.size() <= m_rule_index) {
                 m_instruction = BACKTRACK;
             }
             else {
-                rule* r = rules[m_rule_index];
+                apply_rule(*rules[m_rule_index]);
-                m_trail.push_scope();
-                m_rule_index++;
-                m_trail.push(value_trail<imp,unsigned>(m_rule_index));
-                m_trail.push(value_trail<imp,unsigned>(m_predicate_index));
-                apply_rule(*r);
             }
         }
 
-    void backtrack() {
+        void backtrack() {
             if (m_trail.get_num_scopes() == 0) {
                 m_instruction = SATISFIABLE;
             }
@@ -174,8 +212,9 @@ private:
         lbool run() {
             m_instruction = SELECT_PREDICATE;
             while (true) {
+                IF_VERBOSE(1, verbose_stream() << "run " << m_instruction << "\n";);                
                 if (m_cancel) {
-                    m_cancel = false;
+                    cleanup();
                     return l_undef;
                 }
                 switch(m_instruction) {
@@ -192,15 +231,25 @@ private:
                     next_rule();
                     break;
                 case SATISFIABLE: 
-                    return l_true;
-                case UNSATISFIABLE:
                     return l_false;
+                case UNSATISFIABLE:
+                    return l_true;
                 case CANCEL:
                     m_cancel = false;
                     return l_undef;
                 }
             }
-        }       
+        }    
+
+        lbool query_is_sat() {
+            expr_ref_vector fmls(m);
+
+            return l_undef;
+        }
+
+        lbool query_is_subsumed() {
+            return l_undef;
+        }
 
     };