working on tab Horn solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/substitution/matcher.cpp

@@ -49,6 +49,10 @@ bool matcher::operator()(expr * e1, expr * e2, substitution & s) {
 
         if (is_var(p.second))
             return false;
+        if (!is_app(p.first))
+            return false;
+        if (!is_app(p.second))
+            return false;
 
         app * n1 = to_app(p.first);
         app * n2 = to_app(p.second);

src/ast/substitution/matcher.h

@@ -32,7 +32,7 @@ class matcher {
 
     ast_manager &         m_manager;
     substitution *        m_subst;
-    cache                 m_cache;
+    // cache                 m_cache;
     svector<expr_pair>    m_todo;
 
     void reset();

src/muz_qe/dl_mk_interp_tail_simplifier.cpp

@@ -518,7 +518,7 @@ namespace datalog {
 
         if (m.is_false(itail.get())) {
             //the tail member is never true, so we may delete the rule
-            TRACE("dl", r->display(m_context, tout << "rule in infeasible\n"););
+            TRACE("dl", r->display(m_context, tout << "rule is infeasible\n"););
             return false;
         }
         if (!m.is_true(itail.get())) {

src/muz_qe/tab_context.cpp

@@ -22,6 +22,8 @@ Revision History:
 #include "dl_rule_set.h"
 #include "dl_context.h"
 #include "dl_mk_rule_inliner.h"
+#include "smt_kernel.h"
+#include "matcher.h"
 
 namespace datalog {
 
@@ -42,6 +44,129 @@ namespace datalog {
         }
     };
 
+    // subsumption index structure.
+    class tab_index {
+        ast_manager&   m;
+        rule_manager&  rm;
+        context&       m_ctx;
+        app_ref_vector m_preds;
+        expr_ref       m_precond;
+        rule_ref_vector    m_rules;
+        svector<unsigned>  m_num_vars;
+        unsigned       m_index;
+        matcher        m_matcher;
+        substitution   m_subst;
+        
+    public:
+        tab_index(ast_manager& m, rule_manager& rm, context& ctx): 
+            m(m),
+            rm(rm),
+            m_ctx(ctx),
+            m_preds(m),
+            m_precond(m),
+            m_rules(rm),
+            m_matcher(m),
+            m_subst(m) {}
+
+        void insert(rule* r) {
+            m_rules.push_back(r);
+            m_num_vars.push_back(1+rm.get_var_counter().get_max_var(*r));
+        }
+        
+        void setup(rule const& r) {
+            m_preds.reset();
+            m_index = 0;
+            expr_ref_vector fmls(m);
+            expr_ref_vector vars(m);
+            expr_ref fml(m);
+            ptr_vector<sort> sorts;
+            r.get_vars(sorts);
+            unsigned utsz = r.get_uninterpreted_tail_size();
+            unsigned tsz  = r.get_tail_size();
+            var_subst vs(m, false);
+            for (unsigned i = 0; i < sorts.size(); ++i) {
+                if (!sorts[i]) {
+                    sorts[i] = m.mk_bool_sort();
+                }
+                vars.push_back(m.mk_const(symbol(i), sorts[i]));
+            }
+            for (unsigned i = 0; i < utsz; ++i) {
+                fml = r.get_tail(i);
+                vs(fml, vars.size(), vars.c_ptr(), fml);
+                m_preds.push_back(to_app(fml));
+            }
+            for (unsigned i = utsz; i < tsz; ++i) {
+                fml = r.get_tail(i);
+                vs(fml, vars.size(), vars.c_ptr(), fml);
+                fmls.push_back(fml);
+            }            
+            m_precond = m.mk_and(fmls.size(), fmls.c_ptr());            
+            IF_VERBOSE(1, r.display(m_ctx, verbose_stream() << "setup-match\n"););
+        }
+
+        // extract pre_cond => post_cond validation obligation from match.
+        bool next_match(expr_ref& pre_cond, expr_ref& post_cond) {            
+            for (; m_index < m_rules.size(); ++m_index) {
+                if (try_match(pre_cond, post_cond)) {
+                    return true;
+                }
+            }
+            return false;            
+        }
+    private:
+        //
+        // check that each predicate in r is matched by some predicate in premise.
+        // for now: skip multiple matches within the same rule (incomplete).
+        //
+        bool try_match(expr_ref& pre_cond, expr_ref& post_cond) {
+            rule const& r = *m_rules[m_index];
+            unsigned num_vars = m_num_vars[m_index];
+            m_subst.reset();
+            m_subst.reserve(2, num_vars);
+            unsigned deltas[2] = {0, 0};
+            expr_ref_vector fmls(m);
+            expr_ref q(m);
+            unsigned utsz = r.get_uninterpreted_tail_size();
+            unsigned tsz = r.get_tail_size();
+            
+            IF_VERBOSE(1, r.display(m_ctx, verbose_stream() << "try-match\n"););
+
+            for (unsigned i = 0; i < utsz; ++i) {
+                m_subst.push_scope();
+                if (!try_match(r.get_tail(i))) {
+                    return false;
+                }
+            }
+            for (unsigned i = utsz; i < tsz; ++i) {
+                app* p = r.get_tail(i);
+                m_subst.apply(2, deltas, expr_offset(p, 0), q);
+                fmls.push_back(q);
+            }
+
+            pre_cond = m_precond;
+            post_cond = m.mk_and(fmls.size(), fmls.c_ptr());
+            IF_VERBOSE(1, verbose_stream() << "match: " << mk_pp(post_cond, m) << "\n";);
+            // TBD: 
+            // - existential closure of post_cond
+            // - eliminate variables from post_cond
+            return true;
+        }
+
+        bool try_match(expr* q) {
+            for (unsigned i = 0; i < m_preds.size(); ++i) {
+                if (m_matcher(q, m_preds[i].get(), m_subst)) {
+                    return true;
+                }
+                else {
+                    // undo effect of failed match attempt.
+                    m_subst.pop_scope();
+                    m_subst.push_scope();
+                }
+            }
+            return false;
+        }
+    };
+
     enum tab_instruction {
         SELECT_RULE,
         SELECT_PREDICATE,
@@ -54,13 +179,13 @@ namespace datalog {
 
     std::ostream& operator<<(std::ostream& out, tab_instruction i) {
         switch(i) {
-        case SELECT_RULE: return out << "select-rule";
+        case SELECT_RULE:      return out << "select-rule";
         case SELECT_PREDICATE: return out << "select-predicate";
-        case BACKTRACK: return out << "backtrack";
+        case BACKTRACK:        return out << "backtrack";
-        case NEXT_RULE: return out << "next-rule";
+        case NEXT_RULE:        return out << "next-rule";
-        case SATISFIABLE: return out << "sat";
+        case SATISFIABLE:      return out << "sat";
-        case UNSATISFIABLE: return out << "unsat";
+        case UNSATISFIABLE:    return out << "unsat";
-        case CANCEL: return out << "cancel";
+        case CANCEL:           return out << "cancel";
         }
         return out << "unmatched instruction";
     }
@@ -77,6 +202,9 @@ namespace datalog {
         context&           m_ctx;
         ast_manager&       m;
         rule_manager&      rm;
+        tab_index          m_subsumption_index;
+        smt_params         m_fparams;
+        smt::kernel        m_solver;
         rule_unifier       m_unifier;
         rule_set           m_rules;
         trail_stack<imp>   m_trail;
@@ -92,6 +220,8 @@ namespace datalog {
             m_ctx(ctx), 
             m(ctx.get_manager()),
             rm(ctx.get_rule_manager()),
+            m_subsumption_index(m, rm, ctx),
+            m_solver(m, m_fparams),
             m_unifier(ctx),
             m_rules(ctx),
             m_trail(*this),
@@ -101,7 +231,11 @@ namespace datalog {
             m_predicate_index(0),
             m_rule_index(0),
             m_cancel(false)
-        {}
+        {
+            // m_fparams.m_relevancy_lvl = 0;
+            m_fparams.m_mbqi = false;
+            m_fparams.m_soft_timeout = 1000;
+        }
 
         ~imp() {}        
 
@@ -148,13 +282,15 @@ namespace datalog {
             }
             else {
                 m_instruction = SELECT_RULE;
-                m_predicate_index = 0; // TBD replace by better selection function.
+                m_predicate_index = 0; // TBD replace by better selection function.                
                 m_rule_index = 0;
+                IF_VERBOSE(1, verbose_stream() << mk_pp(m_query->get_tail(m_predicate_index), m) << "\n";);
             }
         }
         
         void apply_rule(rule const& r) {
             m_rule_index++;
+            IF_VERBOSE(1, r.display(m_ctx, verbose_stream()););
             bool can_unify = m_unifier.unify_rules(*m_query, m_predicate_index, r);
             if (can_unify) {
                 m_stats.m_num_unfold++;
@@ -162,18 +298,24 @@ namespace datalog {
                 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);
+                bool is_feasible = m_unifier.apply(*m_query, m_predicate_index, r, new_query);
-                m_trail.push(restore_rule<imp>(m_query_trail, m_query));
+                if (is_feasible) {
-                m_query = new_query;
+                    TRACE("dl", m_query->display(m_ctx, tout););
-                TRACE("dl", m_query->display(m_ctx, tout););
+                    if (l_false == query_is_sat(*new_query.get())) {
-                if (l_false == query_is_sat()) {
+                        m_instruction = BACKTRACK;
-                    m_instruction = BACKTRACK;
+                    }
-                }
+                    else if (l_true == query_is_subsumed(*new_query.get())) {
-                else if (l_true == query_is_subsumed()) {
+                        m_instruction = BACKTRACK;
-                    NOT_IMPLEMENTED_YET();
+                    }
+                    else {
+                        m_subsumption_index.insert(m_query.get());
+                        m_trail.push(restore_rule<imp>(m_query_trail, m_query));
+                        m_query = new_query;
+                        m_instruction = SELECT_PREDICATE;
+                    }
                 }
                 else {
-                    m_instruction = SELECT_PREDICATE;
+                    m_instruction = BACKTRACK;
                 }
             }
             else {
@@ -212,7 +354,7 @@ namespace datalog {
         lbool run() {
             m_instruction = SELECT_PREDICATE;
             while (true) {
-                IF_VERBOSE(1, verbose_stream() << "run " << m_instruction << "\n";);                
+                IF_VERBOSE(1, verbose_stream() << "run " << m_trail.get_num_scopes() << " " << m_instruction << "\n";);                
                 if (m_cancel) {
                     cleanup();
                     return l_undef;
@@ -241,16 +383,55 @@ namespace datalog {
             }
         }    
 
-        lbool query_is_sat() {
+        lbool query_is_sat(rule const& query) {
             expr_ref_vector fmls(m);
+            expr_ref fml(m);
+            unsigned utsz = query.get_uninterpreted_tail_size();
+            unsigned tsz = query.get_tail_size();
+            for (unsigned i = utsz; i < tsz; ++i) {
+                fmls.push_back(query.get_tail(i));
+            }
+            ptr_vector<sort> sorts;
+            svector<symbol> names;
+            query.get_vars(sorts);
+            sorts.reverse();
+            for (unsigned i = 0; i < sorts.size(); ++i) {
+                if (!sorts[i]) {
+                    sorts[i] = m.mk_bool_sort();
+                }
+                names.push_back(symbol(i));
+            }
+            fml = m.mk_and(fmls.size(), fmls.c_ptr());
+            fml = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml);
+            m_solver.push();
+            m_solver.assert_expr(fml);
+            lbool is_sat = m_solver.check();            
+            m_solver.pop(1);
 
-            return l_undef;
+            TRACE("dl", tout << is_sat << ":\n" << mk_pp(fml, m) << "\n";);
+            
+            return is_sat;
         }
 
-        lbool query_is_subsumed() {
+        lbool query_is_subsumed(rule const& query) {
-            return l_undef;
+            lbool is_subsumed = l_false;
+            m_subsumption_index.setup(query);
+            expr_ref precond(m), postcond(m);
+            while (m_subsumption_index.next_match(precond, postcond)) {
+                if (is_ground(postcond)) {
+                    postcond = m.mk_not(postcond);
+                    m_solver.push();
+                    m_solver.assert_expr(precond);
+                    m_solver.assert_expr(postcond);
+                    lbool is_sat = m_solver.check();
+                    m_solver.pop(1);
+                    if (is_sat == l_false) {
+                        return l_true;
+                    }
+                }
+            }
+            return is_subsumed;
         }
-
     };
 
     tab::tab(context& ctx):

src/test/matcher.cpp

@@ -19,6 +19,8 @@ Revision History:
 #ifdef _WINDOWS
 #include"matcher.h"
 #include"ast_pp.h"
+#include "reg_decl_plugins.h"
+
 
 void tst_match(ast_manager & m, app * t, app * i) {
     substitution s(m);
@@ -72,6 +74,7 @@ void tst_match(ast_manager & m, app * t, app * i) {
 
 void tst1() {
     ast_manager m;
+    reg_decl_plugins(m);
     sort_ref s(          m.mk_sort(symbol("S")),    m);
     func_decl_ref g(     m.mk_func_decl(symbol("g"), s, s), m);
     func_decl_ref h(     m.mk_func_decl(symbol("h"), s, s), m);