From 6560fc0a2c85d8acb4289fc6d760b71877b36500 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <t-nclaud@microsoft.com>
Date: Thu, 16 May 2013 09:58:31 -0700
Subject: [PATCH] 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 | 2 +-
src/muz_qe/aig_exporter.cpp | 321 +++++++++++++++++++++++++++++++
src/muz_qe/aig_exporter.h | 66 +++++++
src/muz_qe/fixedpoint_params.pyg | 1 +
src/muz_qe/rel_context.cpp | 8 +
src/muz_qe/rel_context.h | 3 +-
6 files changed, 398 insertions(+), 3 deletions(-)
create mode 100755 src/muz_qe/aig_exporter.cpp
create mode 100755 src/muz_qe/aig_exporter.h
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 6ea794040..e6e7d5dc8 100644
--- a/scripts/mk_project.py
+++ b/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')
diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp
new file mode 100755
index 000000000..1b0dae1ba
--- /dev/null
+++ b/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;
+ }
+}
diff --git a/src/muz_qe/aig_exporter.h b/src/muz_qe/aig_exporter.h
new file mode 100755
index 000000000..f70945e7f
--- /dev/null
+++ b/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
diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg
index c516806a6..c2d33cb05 100644
--- a/src/muz_qe/fixedpoint_params.pyg
+++ b/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'),
))
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index b42adca79..7ad91ecb6 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/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); );
diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h
index 8e4c6f2de..7b4ee551c 100644
--- a/src/muz_qe/rel_context.h
+++ b/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;