add experimental Horn clause to AIG (AAG format) converter.

Clauses should be over booleans only (or bit-blasted with fixedpoint.bit_blast=true).
We will crash if that's not the case.
Only linear clauses supported for now

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>

scripts/mk_project.py

@@ -54,7 +54,7 @@ def init_project_def():
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
     # TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr.
-    add_lib('muz_qe', ['smt', 'sat', 'smt2parser'])
+    add_lib('muz_qe', ['smt', 'sat', 'smt2parser', 'aig_tactic'])
     add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz_qe'], 'tactic/smtlogics')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')

src/muz_qe/aig_exporter.cpp

@@ -0,0 +1,321 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    aig_exporter.cpp
+
+Abstract:
+
+    Export AIG files from horn clauses
+
+--*/
+
+#include "aig_exporter.h"
+#include "dl_context.h"
+#include <set>
+
+namespace datalog {
+
+    aig_exporter::aig_exporter(const rule_set& rules, context& ctx, const fact_vector *facts) :
+        m_rules(rules), m_facts(facts), m(ctx.get_manager()), m_rm(ctx.get_rule_manager()),
+        m_aigm(m), m_next_decl_id(1), m_next_aig_expr_id(2), m_num_and_gates(0),
+        m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m)
+    {
+        std::set<func_decl*> predicates;
+        unsigned num_variables = 0;
+        for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(),
+            E = m_rules.end_grouped_rules(); I != E; ++I) {
+            predicates.insert(I->m_key);
+            num_variables = std::max(num_variables, I->m_key->get_arity());
+        }
+
+        for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) {
+            predicates.insert(I->first);
+            num_variables = std::max(num_variables, I->first->get_arity());
+        }
+
+        // reserve pred id = 0 for initalization purposes
+        unsigned num_preds = (unsigned)predicates.size() + 1;
+
+        // poor's man round-up log2
+        unsigned preds_bitsize = log2(num_preds);
+        if ((1U << preds_bitsize) < num_preds)
+            ++preds_bitsize;
+        SASSERT((1U << preds_bitsize) >= num_preds);
+
+        for (unsigned i = 0; i < preds_bitsize; ++i) {
+            m_ruleid_var_set.push_back(m.mk_fresh_const("rule_id", m.mk_bool_sort()));
+            m_ruleid_varp_set.push_back(m.mk_fresh_const("rule_id_p", m.mk_bool_sort()));
+        }
+
+        for (unsigned i = 0; i < num_variables; ++i) {
+            m_latch_vars.push_back(m.mk_fresh_const("latch_var", m.mk_bool_sort()));
+            m_latch_varsp.push_back(m.mk_fresh_const("latch_varp", m.mk_bool_sort()));
+        }
+    }
+
+    void aig_exporter::assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs) {
+        unsigned id = 0;
+        if (decl && !m_decl_id_map.find(decl, id)) {
+            id = m_next_decl_id++;
+            SASSERT(id < (1U << vars.size()));
+            m_decl_id_map.insert(decl, id);
+        }
+
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            exprs.push_back((id & (1U << i)) ? vars[i] : m.mk_not(vars[i]));
+        }
+    }
+
+    void aig_exporter::collect_var_substs(substitution& subst, const app *h,
+        const expr_ref_vector& vars, expr_ref_vector& eqs) {
+        for (unsigned i = 0; i < h->get_num_args(); ++i) {
+            expr *arg = h->get_arg(i);
+            expr *latchvar = vars.get(i);
+
+            if (is_var(arg)) {
+                var *v = to_var(arg);
+                expr_offset othervar;
+                if (subst.find(v, 0, othervar)) {
+                    eqs.push_back(m.mk_eq(latchvar, othervar.get_expr()));
+                } else {
+                    subst.insert(v, 0, expr_offset(latchvar, 0));
+                }
+            } else {
+                eqs.push_back(m.mk_eq(latchvar, arg));
+            }
+        }
+    }
+
+    void aig_exporter::operator()(std::ostream& out) {
+        expr_ref_vector transition_function(m), output_preds(m);
+        var_ref_vector input_vars(m);
+
+        rule_counter& vc = m_rm.get_counter();
+        expr_ref_vector exprs(m);
+        substitution subst(m);
+
+        for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(),
+            E = m_rules.end_grouped_rules(); I != E; ++I) {
+            for (rule_vector::iterator II = I->get_value()->begin(),
+                EE = I->get_value()->end(); II != EE; ++II) {
+                rule *r = *II;
+                unsigned numqs = r->get_positive_tail_size();
+                if (numqs > 1) {
+                    std::cerr << "non-linear clauses not supported\n";
+                    exit(-1);
+                }
+
+                if (numqs != r->get_uninterpreted_tail_size()) {
+                    std::cerr << "negation of queries not supported\n";
+                    exit(-1);
+                }
+
+                exprs.reset();
+                assert_pred_id(numqs ? r->get_tail(0)->get_decl() : 0, m_ruleid_var_set, exprs);
+                assert_pred_id(r->get_head()->get_decl(), m_ruleid_varp_set, exprs);
+
+                subst.reset();
+                subst.reserve(1, vc.get_max_rule_var(*r)+1);
+                if (numqs)
+                    collect_var_substs(subst, r->get_tail(0), m_latch_vars, exprs);
+                collect_var_substs(subst, r->get_head(), m_latch_varsp, exprs);
+
+                for (unsigned i = numqs; i < r->get_tail_size(); ++i) {
+                    expr_ref e(m);
+                    subst.apply(r->get_tail(i), e);
+                    exprs.push_back(e);
+                }
+
+                transition_function.push_back(m.mk_and(exprs.size(), exprs.c_ptr()));
+            }
+        }
+
+        // collect table facts
+        if (m_facts) {
+            for (fact_vector::const_iterator I = m_facts->begin(), E = m_facts->end(); I != E; ++I) {
+                exprs.reset();
+                assert_pred_id(0, m_ruleid_var_set, exprs);
+                assert_pred_id(I->first, m_ruleid_varp_set, exprs);
+
+                for (unsigned i = 0; i < I->second.size(); ++i) {
+                    exprs.push_back(m.mk_eq(m_latch_varsp.get(i), I->second[i]));
+                }
+
+                transition_function.push_back(m.mk_and(exprs.size(), exprs.c_ptr()));
+            }
+        }
+
+        expr *tr = m.mk_or(transition_function.size(), transition_function.c_ptr());
+        aig_ref aig = m_aigm.mk_aig(tr);
+        expr_ref aig_expr(m);
+        m_aigm.to_formula(aig, aig_expr);
+
+#if 0
+        std::cout << mk_pp(tr, m) << "\n\n";
+        std::cout << mk_pp(aig_expr, m) << "\n\n";
+#endif
+
+        // make rule_id vars latches
+        for (unsigned i = 0; i < m_ruleid_var_set.size(); ++i) {
+            m_latch_vars.push_back(m_ruleid_var_set.get(i));
+            m_latch_varsp.push_back(m_ruleid_varp_set.get(i));
+        }
+
+        // create vars for latches
+        for (unsigned i = 0; i < m_latch_vars.size(); ++i) {
+            mk_var(m_latch_vars.get(i));
+            mk_input_var(m_latch_varsp.get(i));
+        }
+
+        unsigned tr_id = expr_to_aig(aig_expr);
+
+        // create latch next state variables: (ite tr varp var)
+        unsigned_vector latch_varp_ids;
+        for (unsigned i = 0; i < m_latch_vars.size(); ++i) {
+            unsigned in_val = mk_and(tr_id, get_var(m_latch_varsp.get(i)));
+            unsigned latch_val = mk_and(neg(tr_id), get_var(m_latch_vars.get(i)));
+            latch_varp_ids.push_back(mk_or(in_val, latch_val));
+        }
+        m_latch_varsp.reset();
+
+        // create output variable (true iff an output predicate is derivable)
+        unsigned output_id = 0;
+        {
+            expr_ref_vector output(m);
+            const func_decl_set& preds = m_rules.get_output_predicates();
+
+            for (func_decl_set::iterator I = preds.begin(), E = preds.end(); I != E; ++I) {
+                exprs.reset();
+                assert_pred_id(*I, m_ruleid_var_set, exprs);
+                output.push_back(m.mk_and(exprs.size(), exprs.c_ptr()));
+            }
+
+            expr *out = m.mk_or(output.size(), output.c_ptr());
+            aig = m_aigm.mk_aig(out);
+            m_aigm.to_formula(aig, aig_expr);
+            output_id = expr_to_aig(aig_expr);
+
+#if 0
+            std::cout << "output formula\n";
+            std::cout << mk_pp(out, m) << "\n\n";
+            std::cout << mk_pp(aig_expr, m) << "\n\n";
+#endif
+        }
+
+        // 1) print header
+        // aag var_index inputs latches outputs andgates
+        out << "aag " << (m_next_aig_expr_id-1)/2 << ' ' << m_input_vars.size()
+            << ' ' << m_latch_vars.size() << " 1 " << m_num_and_gates << '\n';
+
+        // 2) print inputs
+        for (unsigned i = 0; i < m_input_vars.size(); ++i) {
+            out << m_input_vars[i] << '\n';
+        }
+        
+        // 3) print latches
+        for (unsigned i = 0; i < m_latch_vars.size(); ++i) {
+            out << get_var(m_latch_vars.get(i)) << ' ' << latch_varp_ids[i] << '\n';
+        }
+
+        // 4) print outputs  (just one for now)
+        out << output_id << '\n';
+
+        // 5) print formula
+        out << m_buffer.str();
+    }
+
+    unsigned aig_exporter::expr_to_aig(const expr *e) {
+        unsigned id;
+        if (m_aig_expr_id_map.find(e, id))
+            return id;
+
+        switch (e->get_kind()) {
+        case AST_APP: {
+            const app *a = to_app(e);
+            switch (a->get_decl_kind()) {
+            case OP_OR:
+                SASSERT(a->get_num_args() > 0);
+                id = expr_to_aig(a->get_arg(0));
+                for (unsigned i = 1; i < a->get_num_args(); ++i) {
+                    id = mk_or(id, expr_to_aig(a->get_arg(i)));
+                }
+                m_aig_expr_id_map.insert(e, id);
+                return id;
+
+            case null_decl_kind:
+                return get_var(a);
+
+            case OP_NOT:
+                return neg(expr_to_aig(a->get_arg(0)));
+
+            case OP_FALSE:
+                return 0;
+
+            case OP_TRUE:
+                return 1;
+            }
+            break;}
+
+        case AST_VAR:
+            return get_var(e);
+        }
+        
+        UNREACHABLE();
+        return 0;
+    }
+
+    unsigned aig_exporter::neg(unsigned id) const {
+        return (id % 2) ? (id-1) : (id+1);
+    }
+
+    unsigned aig_exporter::mk_and(unsigned id1, unsigned id2) {
+        if (id1 > id2)
+            std::swap(id1, id2);
+
+        std::pair<unsigned,unsigned> key(id1, id2);
+        and_gates_map::const_iterator I = m_and_gates_map.find(key);
+        if (I != m_and_gates_map.end())
+            return I->second;
+
+        unsigned id = mk_expr_id();
+        m_buffer << id << ' ' << id1 << ' ' << id2 << '\n';
+        m_and_gates_map[key] = id;
+        ++m_num_and_gates;
+        return id;
+    }
+
+    unsigned aig_exporter::mk_or(unsigned id1, unsigned id2) {
+        return neg(mk_and(neg(id1), neg(id2)));
+    }
+
+    unsigned aig_exporter::get_var(const expr *e) {
+        unsigned id;
+        if (m_aig_expr_id_map.find(e, id))
+            return id;
+        return mk_input_var(e);
+    }
+
+    unsigned aig_exporter::mk_var(const expr *e) {
+        SASSERT(!m_aig_expr_id_map.contains(e));
+        unsigned id = mk_expr_id();
+        m_aig_expr_id_map.insert(e, id);
+        return id;
+    }
+    
+    unsigned aig_exporter::mk_input_var(const expr *e) {
+        SASSERT(!m_aig_expr_id_map.contains(e));
+        unsigned id = mk_expr_id();
+        m_input_vars.push_back(id);
+        if (e)
+            m_aig_expr_id_map.insert(e, id);
+        return id;
+    }
+
+    unsigned aig_exporter::mk_expr_id() {
+        unsigned id = m_next_aig_expr_id;
+        m_next_aig_expr_id += 2;
+        return id;
+    }
+}

src/muz_qe/aig_exporter.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    aig_exporter.h
+
+Abstract:
+
+    Export AIG files from horn clauses
+
+--*/
+
+#ifndef _AIG_EXPORTER_H_
+#define _AIG_EXPORTER_H_
+
+#include "aig.h"
+#include "dl_rule_set.h"
+#include "rel_context.h"
+#include <map>
+#include <sstream>
+
+namespace datalog {
+    class aig_exporter {
+    public:
+        aig_exporter(const rule_set& rules, context& ctx, const fact_vector *facts = 0);
+        void operator()(std::ostream& out);
+
+    private:
+        typedef obj_map<func_decl, unsigned> decl_id_map;
+        typedef obj_map<const expr, unsigned> aig_expr_id_map;
+        typedef std::map<std::pair<unsigned,unsigned>, unsigned> and_gates_map;
+
+        const rule_set&    m_rules;
+        const fact_vector *m_facts;
+        ast_manager&       m;
+        rule_manager&      m_rm;
+        aig_manager        m_aigm;
+        decl_id_map        m_decl_id_map;
+        unsigned           m_next_decl_id;
+        aig_expr_id_map    m_aig_expr_id_map;
+        unsigned           m_next_aig_expr_id;
+        and_gates_map      m_and_gates_map;
+        unsigned           m_num_and_gates;
+
+        expr_ref_vector m_latch_vars, m_latch_varsp;
+        expr_ref_vector m_ruleid_var_set, m_ruleid_varp_set;
+        unsigned_vector m_input_vars;
+
+        std::stringstream m_buffer;
+
+        void assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs);
+        void collect_var_substs(substitution& subst, const app *h,
+            const expr_ref_vector& vars, expr_ref_vector& eqs);
+        unsigned expr_to_aig(const expr *e);
+        unsigned neg(unsigned id) const;
+        unsigned mk_and(unsigned id1, unsigned id2);
+        unsigned mk_or(unsigned id1, unsigned id2);
+        unsigned get_var(const expr *e);
+        unsigned mk_var(const expr *e);
+        unsigned mk_input_var(const expr *e = 0);
+        unsigned mk_expr_id();
+    };
+}
+
+#endif

src/muz_qe/fixedpoint_params.pyg

@@ -62,6 +62,7 @@ def_module_params('fixedpoint',
                           ('print_statistics',  BOOL, False, 'print statistics'),
 			  ('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'),
 	                  ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),
+                          ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
                           ))
 
 

src/muz_qe/rel_context.cpp

@@ -32,6 +32,7 @@ Revision History:
 #include"dl_sparse_table.h"
 #include"dl_table.h"
 #include"dl_table_relation.h"
+#include"aig_exporter.h"
 
 namespace datalog {
 
@@ -127,6 +128,13 @@ namespace datalog {
             }
             TRACE("dl", m_context.display(tout););
 
+            if (m_context.get_params().dump_aig().size()) {
+                const char *filename = static_cast<const char*>(m_context.get_params().dump_aig().c_ptr());
+                aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts);
+                aig(std::ofstream(filename, std::ios_base::binary));
+                exit(0);
+            }
+
             compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
 
             TRACE("dl", m_code.display(*this, tout); );

src/muz_qe/rel_context.h

@@ -28,10 +28,9 @@ Revision History:
 namespace datalog {
 
     class context;
+    typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
 
     class rel_context {
-        typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
-
         context&           m_context;
         ast_manager&       m;
         relation_manager   m_rmanager;