initial test for polynormalization

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

src/muz_qe/dl_mk_coi_filter.cpp

@@ -16,6 +16,9 @@ Author:
 
 Revision History:
 
+    Andrey Rybalchenko (rybal) 2013-8-8
+    Added bottom_up pruning.
+
 --*/
 
 
@@ -32,12 +35,97 @@ namespace datalog {
     //
     // -----------------------------------
 
-
-    rule_set * mk_coi_filter::operator()(rule_set const & source)
-    {
+    rule_set * mk_coi_filter::operator()(rule_set const & source) {
         if (source.empty()) {
             return 0;
         }
+        scoped_ptr<rule_set> result = top_down(source);
+        return bottom_up(result?*result:source);
+    }
+
+    rule_set * mk_coi_filter::bottom_up(rule_set const & source) {
+        decl_set all, reached;
+        ptr_vector<func_decl> todo;
+        rule_set::decl2rules body2rules;
+        // initialization for reachability
+        for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
+            rule * r = *it;
+            all.insert(r->get_decl());
+            if (r->get_uninterpreted_tail_size() == 0) {
+                if (!reached.contains(r->get_decl())) {
+                    reached.insert(r->get_decl());
+                    todo.insert(r->get_decl());
+                }
+            } 
+            else {
+                for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
+                    func_decl * d = r->get_tail(i)->get_decl();
+                    all.insert(d);
+                    rule_set::decl2rules::obj_map_entry * e = body2rules.insert_if_not_there2(d, 0);
+                    if (!e->get_data().m_value) {
+                        e->get_data().m_value = alloc(ptr_vector<rule>);
+                    }
+                    e->get_data().m_value->push_back(r);
+                }
+            }
+        }
+        // reachability computation
+        while (!todo.empty()) {
+            func_decl * d = todo.back();
+            todo.pop_back();
+            ptr_vector<rule> * rules; 
+            if (!body2rules.find(d, rules)) continue;
+            for (ptr_vector<rule>::iterator it = rules->begin(); it != rules->end(); ++it) {
+                rule * r = *it;
+                if (reached.contains(r->get_decl())) continue;
+                bool contained = true;
+                for (unsigned i = 0; contained && i < r->get_uninterpreted_tail_size(); ++i) {
+                    contained = reached.contains(r->get_tail(i)->get_decl());
+                }
+                if (!contained) continue;
+                reached.insert(r->get_decl());
+                todo.insert(r->get_decl());
+            }
+        }
+
+        // eliminate each rule when some body predicate is not reached
+        scoped_ptr<rule_set> res = alloc(rule_set, m_context);
+        res->inherit_predicates(source);
+        for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
+            rule * r = *it;
+
+            bool contained = true;
+            for (unsigned i = 0; contained && i < r->get_uninterpreted_tail_size(); ++i) {
+                contained = reached.contains(r->get_tail(i)->get_decl());
+            }
+            if (contained) {
+                res->add_rule(r);
+            }
+        }
+
+        if (res->get_num_rules() == source.get_num_rules()) {
+            return 0;
+        } 
+        res->close();
+
+        // set to false each unreached predicate 
+        if (m_context.get_model_converter()) {
+            extension_model_converter* mc0 = alloc(extension_model_converter, m);
+            for (decl_set::iterator it = all.begin(); it != all.end(); ++it) {
+                if (!reached.contains(*it)) {
+                    mc0->insert(*it, m.mk_false());
+                }
+            }   
+            m_context.add_model_converter(mc0);
+        }
+        // clean up body2rules range resources
+        for (rule_set::decl2rules::iterator it = body2rules.begin(); it != body2rules.end(); ++it) {
+            dealloc(it->m_value);
+        }
+        return res.detach();
+    }
+
+    rule_set * mk_coi_filter::top_down(rule_set const & source) {
 
         decl_set interesting_preds;
         decl_set pruned_preds;
@@ -60,7 +148,7 @@ namespace datalog {
 
             const rule_dependencies::item_set& cdeps = deps.get_deps(curr);
             rule_dependencies::item_set::iterator dend = cdeps.end();
-            for (rule_dependencies::item_set::iterator it = cdeps.begin(); it!=dend; ++it) {
+            for (rule_dependencies::item_set::iterator it = cdeps.begin(); it != dend; ++it) {
                 func_decl * dep_pred = *it;
                 if (!interesting_preds.contains(dep_pred)) {
                     interesting_preds.insert(dep_pred);
@@ -73,7 +161,7 @@ namespace datalog {
         res->inherit_predicates(source);
 
         rule_set::iterator rend = source.end();
-        for (rule_set::iterator rit = source.begin(); rit!=rend; ++rit) {
+        for (rule_set::iterator rit = source.begin(); rit != rend; ++rit) {
             rule * r = *rit;
             func_decl * pred = r->get_decl();
             if (interesting_preds.contains(pred)) {

src/muz_qe/dl_mk_coi_filter.h

@@ -32,6 +32,10 @@ namespace datalog {
 
         ast_manager & m;
         context & m_context;
+
+        rule_set * bottom_up(rule_set const & source);
+        rule_set * top_down(rule_set const & source);
+
     public:
         mk_coi_filter(context & ctx, unsigned priority=45000)
             : plugin(priority),

src/test/dl_context.cpp

@@ -60,7 +60,7 @@ void dl_context_saturate_file(params_ref & params, const char * f) {
     }
     dealloc(parser);
     std::cerr << "Saturating...\n";
-    ctx.get_rel_context().saturate();
+    ctx.get_rel_context()->saturate();
     std::cerr << "Done\n";
 }
 

src/test/dl_product_relation.cpp

@@ -22,7 +22,7 @@ namespace datalog {
     void test_functional_columns(smt_params fparams, params_ref& params) {
         ast_manager m;
         context ctx(m, fparams);
-        rel_context& rctx = ctx.get_rel_context();
+        rel_context& rctx = *ctx.get_rel_context();
         ctx.updt_params(params);
         relation_manager & rmgr(rctx.get_rmanager());
 
@@ -127,7 +127,7 @@ namespace datalog {
         context ctx(m, fparams);
         ctx.updt_params(params);
         dl_decl_util dl_util(m);
-        relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
+        relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
 
         relation_plugin & rel_plugin = *rmgr.get_relation_plugin(params.get_sym("default_relation", symbol("sparse")));
         SASSERT(&rel_plugin);

src/test/dl_query.cpp

@@ -58,7 +58,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
         TRUSTME( p->parse_file(problem_file) );
         dealloc(p);
     }
-    relation_manager & rel_mgr_q = ctx_b.get_rel_context().get_rmanager();
+    relation_manager & rel_mgr_q = ctx_b.get_rel_context()->get_rmanager();
 
     decl_set out_preds = ctx_b.get_rules().get_output_predicates();
     decl_set::iterator it = out_preds.begin();
@@ -69,10 +69,10 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
         func_decl * pred_q = ctx_q.try_get_predicate_decl(symbol(pred_b->get_name().bare_str()));
         SASSERT(pred_q);
 
-        relation_base & rel_b = ctx_b.get_rel_context().get_relation(pred_b);
+        relation_base & rel_b = ctx_b.get_rel_context()->get_relation(pred_b);
 
         relation_signature sig_b = rel_b.get_signature();
-        relation_signature sig_q = ctx_q.get_rel_context().get_relation(pred_q).get_signature();
+        relation_signature sig_q = ctx_q.get_rel_context()->get_relation(pred_q).get_signature();
         SASSERT(sig_b.size()==sig_q.size());
 
         std::cerr << "Queries on random facts...\n";
@@ -211,7 +211,7 @@ void tst_dl_query() {
         TRUSTME( p->parse_file(problem_file) );
         dealloc(p);
     }
-    ctx_base.get_rel_context().saturate();
+    ctx_base.get_rel_context()->saturate();
 
     for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) {
         params.set_uint("initial_restart_timeout", use_restarts ? 100 : 0);

src/test/dl_relation.cpp

@@ -12,7 +12,7 @@ namespace datalog {
         ast_manager ast_m;
         context ctx(ast_m, params);    
         arith_util autil(ast_m);
-        relation_manager & m = ctx.get_rel_context().get_rmanager();
+        relation_manager & m = ctx.get_rel_context()->get_rmanager();
         m.register_plugin(alloc(interval_relation_plugin, m));
         interval_relation_plugin& ip = dynamic_cast<interval_relation_plugin&>(*m.get_relation_plugin(symbol("interval_relation")));
         SASSERT(&ip);
@@ -115,7 +115,7 @@ namespace datalog {
         ast_manager ast_m;
         context ctx(ast_m, params);    
         arith_util autil(ast_m);
-        relation_manager & m = ctx.get_rel_context().get_rmanager();
+        relation_manager & m = ctx.get_rel_context()->get_rmanager();
         m.register_plugin(alloc(bound_relation_plugin, m));
         bound_relation_plugin& br = dynamic_cast<bound_relation_plugin&>(*m.get_relation_plugin(symbol("bound_relation")));
         SASSERT(&br);

src/test/dl_table.cpp

@@ -19,7 +19,7 @@ static void test_table(mk_table_fn mk_table) {
     smt_params params;
     ast_manager ast_m;
     datalog::context ctx(ast_m, params);    
-    datalog::relation_manager & m = ctx.get_rel_context().get_rmanager();
+    datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager();
 
     m.register_plugin(alloc(datalog::bitvector_table_plugin, m));
 

src/test/main.cpp

@@ -213,6 +213,7 @@ int main(int argc, char ** argv) {
     TST(dl_query);
     TST(quant_solve);
     TST(rcf);
+    TST(polynorm);
 }
 
 void initialize_mam() {}

src/test/polynorm.cpp

@@ -0,0 +1,119 @@
+#include "th_rewriter.h"
+#include "smt2parser.h"
+#include "arith_decl_plugin.h"
+#include "reg_decl_plugins.h"
+#include "ast_pp.h"
+
+
+static expr_ref parse_fml(ast_manager& m, char const* str) {
+    expr_ref result(m);
+    cmd_context ctx(false, &m);
+    ctx.set_ignore_check(true);
+    std::ostringstream buffer;
+    buffer << "(declare-const x Int)\n"
+           << "(declare-const y Int)\n"
+           << "(declare-const z Int)\n"
+           << "(declare-const a Int)\n"
+           << "(declare-const b Int)\n"
+           << "(assert " << str << ")\n";
+    std::istringstream is(buffer.str());
+    VERIFY(parse_smt2_commands(ctx, is));
+    SASSERT(ctx.begin_assertions() != ctx.end_assertions());
+    result = *ctx.begin_assertions();
+    return result;
+}
+
+static char const* example1 = "(= (+ (- (* x x) (* 2 y)) y) 0)";
+static char const* example2 = "(= (+ 4 3 (- (* x x) (* 2 y)) y) 0)";
+
+
+// ast
+///  sort : ast
+///  func_decl : ast
+///  expr : ast
+///    app : expr
+///    quantifier : expr
+///    var : expr
+/// 
+
+static expr_ref mk_mul(arith_util& arith, unsigned num_args, expr* const* args) {
+    ast_manager& m = arith.get_manager();
+    expr_ref result(m);
+    switch (num_args) {
+    case 0: 
+        UNREACHABLE();
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        result = arith.mk_mul(num_args, args);
+        break;
+    }
+    return result;
+}
+
+static void nf(expr_ref& term) {
+    ast_manager& m = term.get_manager();
+    expr *e1, *e2;
+
+    th_rewriter rw(m);
+    arith_util arith(m);
+
+    VERIFY(m.is_eq(term, e1, e2));
+    term = e1;
+    
+    rw(term);
+
+    std::cout << mk_pp(term, m) << "\n";
+    std::cout << arith.is_add(term) << "\n";
+    
+    expr_ref_vector factors(m);
+    vector<rational> coefficients;
+    rational coefficient(0);
+
+    if (arith.is_add(term)) {
+        factors.append(to_app(term)->get_num_args(), to_app(term)->get_args());
+    }
+    else {
+        factors.push_back(term);
+    }
+    for (unsigned i = 0; i < factors.size(); ++i) {
+        expr* f = factors[i].get();
+        rational r;
+        if (arith.is_mul(f) && arith.is_numeral(to_app(f)->get_arg(0), r)) {
+            coefficients.push_back(r);            
+            factors[i] = mk_mul(arith, to_app(f)->get_num_args()-1, to_app(f)->get_args()+1);
+        }
+        else if (arith.is_numeral(f, r)) {
+            factors[i] = factors.back();
+            factors.pop_back();
+            SASSERT(coefficient.is_zero());
+            SASSERT(!r.is_zero());
+            coefficient = r;
+            --i; // repeat examining 'i'
+        }
+        else {
+            coefficients.push_back(rational(1));
+        }
+    }
+
+    std::cout << coefficient << "\n";
+    for (unsigned i = 0; i < factors.size(); ++i) {
+        std::cout << mk_pp(factors[i].get(), m) << " * " << coefficients[i] << "\n";
+    }
+}
+
+void tst_polynorm() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    expr_ref fml(m);
+
+    fml = parse_fml(m, example2);
+
+    std::cout << mk_pp(fml, m) << "\n";
+
+    nf(fml);
+
+    
+}