mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Leonardo de Moura 2013-05-30 10:55:19 -07:00
commit b670f0bb69
50 changed files with 3280 additions and 195 deletions
Download patch file Download diff file Expand all files Collapse all files

106
src/api/c++/z3++.h
View file

@ -249,6 +249,8 @@ namespace z3 {
array & operator=(array const & s);
public:
array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
template<typename T2>
array(ast_vector_tpl<T2> const & v);
~array() { delete[] m_array; }
unsigned size() const { return m_size; }
T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
@ -939,49 +941,6 @@ namespace z3 {
inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
// Basic functions for creating quantified formulas.
// The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
inline expr forall(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
template<typename T> class cast_ast;
template<> class cast_ast<ast> {
@ -1043,6 +1002,67 @@ namespace z3 {
friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
};
template<typename T>
template<typename T2>
array<T>::array(ast_vector_tpl<T2> const & v) {
m_array = new T[v.size()];
m_size = v.size();
for (unsigned i = 0; i < m_size; i++) {
m_array[i] = v[i];
}
}
// Basic functions for creating quantified formulas.
// The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
inline expr forall(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr_vector const & xs, expr const & b) {
array<Z3_app> vars(xs);
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr_vector const & xs, expr const & b) {
array<Z3_app> vars(xs);
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
class func_entry : public object {
Z3_func_entry m_entry;
void init(Z3_func_entry e) {

15
src/api/dotnet/Context.cs
View file

@ -44,6 +44,21 @@ namespace Microsoft.Z3
/// <summary>
/// Constructor.
/// </summary>
/// <remarks>
/// The following parameters can be set:
/// - proof (Boolean) Enable proof generation
/// - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
/// - trace (Boolean) Tracing support for VCC
/// - trace_file_name (String) Trace out file for VCC traces
/// - timeout (unsigned) default timeout (in milliseconds) used for solvers
/// - well_sorted_check type checker
/// - auto_config use heuristics to automatically select solver and configure it
/// - model model generation for solvers, this parameter can be overwritten when creating a solver
/// - model_validate validate models produced by solvers
/// - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
/// Note that in previous versions of Z3, this constructor was also used to set global and module parameters.
/// For this purpose we should now use <see cref="Global.SetParameter"/>
/// </remarks>
public Context(Dictionary<string, string> settings)
: base()
{

15
src/api/java/Context.java
View file

@ -27,6 +27,21 @@ public class Context extends IDisposable
/**
* Constructor.
* <remarks>
* The following parameters can be set:
* - proof (Boolean) Enable proof generation
* - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
* - trace (Boolean) Tracing support for VCC
* - trace_file_name (String) Trace out file for VCC traces
* - timeout (unsigned) default timeout (in milliseconds) used for solvers
* - well_sorted_check type checker
* - auto_config use heuristics to automatically select solver and configure it
* - model model generation for solvers, this parameter can be overwritten when creating a solver
* - model_validate validate models produced by solvers
* - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
* Note that in previous versions of Z3, this constructor was also used to set global and
* module parameters. For this purpose we should now use <see cref="Global.setParameter"/>
* </remarks>
**/
public Context(Map<String, String> settings) throws Z3Exception
{

8
src/ast/pattern/database.smt2
View file

@ -119,13 +119,13 @@
:pattern (?select (?select (?asElems e) a) i))))
(assert (forall ((x Int) (f Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?fClosedTime f))) 0)
(or (<= (+ a0 (* (- 1) (?fClosedTime f))) 0)
(not (= (?isAllocated x a0) 1))
(= (?isAllocated (?select f x) a0) 1))
:pattern (?isAllocated (?select f x) a0))))
(assert (forall ((a Int) (e Int) (i Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?eClosedTime e))) 0)
(or (<= (+ a0 (* (- 1) (?eClosedTime e))) 0)
(not (= (?isAllocated a a0) 1))
(= (?isAllocated (?select (?select e a) i) a0) 1))
:pattern (?isAllocated (?select (?select e a) i) a0))))
@ -281,13 +281,13 @@
:pattern (IntsAllocated h (?StructGet_ s f)))))
(assert (forall ((x Int) (f Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?fClosedTime f))) 0)
(or (<= (+ a0 (* (- 1) (?fClosedTime f))) 0)
(not (?isAllocated_ x a0))
(?isAllocated_ (?select f x) a0))
:pattern (?isAllocated_ (?select f x) a0))))
(assert (forall ((a Int) (e Int) (i Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?eClosedTime e))) 0)
(or (<= (+ a0 (* (- 1) (?eClosedTime e))) 0)
(not (?isAllocated_ a a0))
(?isAllocated_ (?select (?select e a) i) a0))
:pattern (?isAllocated_ (?select (?select e a) i) a0))))

38
src/ast/rewriter/array_rewriter.cpp
View file

@ -25,6 +25,7 @@ void array_rewriter::updt_params(params_ref const & _p) {
array_rewriter_params p(_p);
m_sort_store = p.sort_store();
m_expand_select_store = p.expand_select_store();
m_expand_store_eq = p.expand_store_eq();
}
void array_rewriter::get_param_descrs(param_descrs & r) {
@ -365,3 +366,40 @@ br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & res
return BR_REWRITE3;
}
br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
if (!m_expand_store_eq) {
return BR_FAILED;
}
expr* lhs1 = lhs;
while (m_util.is_store(lhs1)) {
lhs1 = to_app(lhs1)->get_arg(0);
}
expr* rhs1 = rhs;
while (m_util.is_store(rhs1)) {
rhs1 = to_app(rhs1)->get_arg(0);
}
if (lhs1 != rhs1) {
return BR_FAILED;
}
ptr_buffer<expr> fmls, args;
expr* e;
expr_ref tmp1(m()), tmp2(m());
#define MK_EQ() \
while (m_util.is_store(e)) { \
args.push_back(lhs); \
args.append(to_app(e)->get_num_args()-2,to_app(e)->get_args()+1); \
mk_select(args.size(), args.c_ptr(), tmp1); \
args[0] = rhs; \
mk_select(args.size(), args.c_ptr(), tmp2); \
fmls.push_back(m().mk_eq(tmp1, tmp2)); \
e = to_app(e)->get_arg(0); \
args.reset(); \
} \
e = lhs;
MK_EQ();
e = rhs;
MK_EQ();
result = m().mk_and(fmls.size(), fmls.c_ptr());
return BR_REWRITE_FULL;
}

3
src/ast/rewriter/array_rewriter.h
View file

@ -31,12 +31,14 @@ class array_rewriter {
array_util m_util;
bool m_sort_store;
bool m_expand_select_store;
bool m_expand_store_eq;
template<bool CHECK_DISEQ>
lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
public:
array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {
updt_params(p);
}
ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); }
@ -60,6 +62,7 @@ public:
br_status mk_set_complement(expr * arg, expr_ref & result);
br_status mk_set_difference(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_set_subset(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
};
#endif

1
src/ast/rewriter/array_rewriter_params.pyg
View file

@ -2,4 +2,5 @@ def_module_params(module_name='rewriter',
class_name='array_rewriter_params',
export=True,
params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"),
("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"),
("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))

2
src/ast/rewriter/mk_simplified_app.cpp
View file

@ -62,6 +62,8 @@ struct mk_simplified_app::imp {
st = m_dt_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_f_rw.get_fid())
st = m_f_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_ar_rw.get_fid())
st = m_ar_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;

4
src/ast/rewriter/th_rewriter.cpp
View file

@ -169,7 +169,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
st = m_dt_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_f_rw.get_fid())
st = m_f_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_ar_rw.get_fid())
st = m_ar_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}

328
src/muz_qe/aig_exporter.cpp Executable file
View file

@ -0,0 +1,328 @@
/*++
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;
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);
}
for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) {
predicates.insert(I->first);
}
// 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()));
}
}
void aig_exporter::mk_latch_vars(unsigned n) {
for (unsigned i = m_latch_vars.size(); i <= n; ++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()));
}
SASSERT(m_latch_vars.size() > n);
}
expr* aig_exporter::get_latch_var(unsigned i, const expr_ref_vector& vars) {
mk_latch_vars(i);
return vars.get(i);
}
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 = get_latch_var(i, vars);
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(get_latch_var(i, m_latch_varsp), 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;
if (is_uninterp_const(e))
return get_var(e);
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 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);
default:
UNREACHABLE();
}
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;
}
}

68
src/muz_qe/aig_exporter.h Executable file
View file

@ -0,0 +1,68 @@
/*++
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 mk_latch_vars(unsigned n);
expr* get_latch_var(unsigned i, const expr_ref_vector& vars);
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

15
src/muz_qe/clp_context.cpp
View file

@ -67,8 +67,10 @@ namespace datalog {
m_solver.reset();
m_goals.reset();
rm.mk_query(query, m_ctx.get_rules());
expr_ref head(m);
head = m_ctx.get_rules().last()->get_head();
m_ctx.apply_default_transformation();
func_decl *head_decl = m_ctx.get_rules().get_output_predicate();
expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
ground(head);
m_goals.push_back(to_app(head));
return search(20, 0);
@ -125,6 +127,10 @@ namespace datalog {
m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
}
static bool rule_sort_fn(const rule *r1, const rule *r2) {
return r1->get_uninterpreted_tail_size() < r2->get_uninterpreted_tail_size();
}
lbool search(unsigned depth, unsigned index) {
if (index == m_goals.size()) {
return l_true;
@ -135,7 +141,10 @@ namespace datalog {
IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";);
unsigned num_goals = m_goals.size();
app* head = m_goals[index].get();
rule_vector const& rules = m_ctx.get_rules().get_predicate_rules(head->get_decl());
rule_vector rules(m_ctx.get_rules().get_predicate_rules(head->get_decl()));
std::stable_sort(rules.begin(), rules.end(), rule_sort_fn);
lbool status = l_false;
for (unsigned i = 0; i < rules.size(); ++i) {
rule* r = rules[i];

14
src/muz_qe/dl_base.h
View file

@ -331,6 +331,10 @@ namespace datalog {
virtual mutator_fn * mk_filter_interpreted_fn(const base_object & t, app * condition)
{ return 0; }
virtual transformer_fn * mk_filter_interpreted_and_project_fn(const base_object & t,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols)
{ return 0; }
virtual transformer_fn * mk_select_equal_and_project_fn(const base_object & t,
const element & value, unsigned col) { return 0; }
@ -454,8 +458,8 @@ namespace datalog {
class convenient_join_fn : public join_fn {
signature m_result_sig;
protected:
const unsigned_vector m_cols1;
const unsigned_vector m_cols2;
unsigned_vector m_cols1;
unsigned_vector m_cols2;
convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt,
const unsigned * cols1, const unsigned * cols2)
@ -470,8 +474,8 @@ namespace datalog {
class convenient_join_project_fn : public join_fn {
signature m_result_sig;
protected:
const unsigned_vector m_cols1;
const unsigned_vector m_cols2;
unsigned_vector m_cols1;
unsigned_vector m_cols2;
//it is non-const because it needs to be modified in sparse_table version of the join_project operator
unsigned_vector m_removed_cols;
@ -498,7 +502,7 @@ namespace datalog {
class convenient_project_fn : public convenient_transformer_fn {
protected:
const unsigned_vector m_removed_cols;
unsigned_vector m_removed_cols;
convenient_project_fn(const signature & orig_sig, unsigned col_cnt, const unsigned * removed_cols)
: m_removed_cols(col_cnt, removed_cols) {

30
src/muz_qe/dl_bmc_engine.cpp
View file

@ -297,6 +297,7 @@ namespace datalog {
r->to_formula(fml);
r2 = r;
rm.substitute(r2, sub.size(), sub.c_ptr());
proof_ref p(m);
if (r0) {
VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get()));
expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true);
@ -306,7 +307,10 @@ namespace datalog {
r1->to_formula(concl);
scoped_proof _sp(m);
proof* p = r->get_proof();
p = r->get_proof();
if (!p) {
p = m.mk_asserted(fml);
}
proof* premises[2] = { pr, p };
positions.push_back(std::make_pair(0, 1));
@ -319,13 +323,17 @@ namespace datalog {
else {
r2->to_formula(concl);
scoped_proof _sp(m);
proof* p = r->get_proof();
p = r->get_proof();
if (!p) {
p = m.mk_asserted(fml);
}
if (sub.empty()) {
pr = p;
}
else {
substs.push_back(sub);
pr = m.mk_hyper_resolve(1, &p, concl, positions, substs);
proof* ps[1] = { p };
pr = m.mk_hyper_resolve(1, ps, concl, positions, substs);
}
r0 = r2;
}
@ -1211,6 +1219,15 @@ namespace datalog {
r->to_formula(fml);
r2 = r;
rm.substitute(r2, sub.size(), sub.c_ptr());
proof_ref p(m);
{
scoped_proof _sp(m);
p = r->get_proof();
if (!p) {
p = m.mk_asserted(fml);
}
}
if (r0) {
VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get()));
expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true);
@ -1218,9 +1235,8 @@ namespace datalog {
apply_subst(sub, sub2);
unifier.apply(*r0.get(), 0, *r2.get(), r1);
r1->to_formula(concl);
scoped_proof _sp(m);
proof* p = r->get_proof();
scoped_proof _sp(m);
proof* premises[2] = { pr, p };
positions.push_back(std::make_pair(0, 1));
@ -1233,13 +1249,13 @@ namespace datalog {
else {
r2->to_formula(concl);
scoped_proof _sp(m);
proof* p = r->get_proof();
if (sub.empty()) {
pr = p;
}
else {
substs.push_back(sub);
pr = m.mk_hyper_resolve(1, &p, concl, positions, substs);
proof * ps[1] = { p };
pr = m.mk_hyper_resolve(1, ps, concl, positions, substs);
}
r0 = r2;
}

81
src/muz_qe/dl_check_table.cpp
View file

@ -82,6 +82,34 @@ namespace datalog {
return alloc(join_fn, *this, t1, t2, col_cnt, cols1, cols2);
}
class check_table_plugin::join_project_fn : public table_join_fn {
scoped_ptr<table_join_fn> m_tocheck;
scoped_ptr<table_join_fn> m_checker;
public:
join_project_fn(check_table_plugin& p, const table_base & t1, const table_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2,
unsigned removed_col_cnt, const unsigned * removed_cols) {
m_tocheck = p.get_manager().mk_join_project_fn(tocheck(t1), tocheck(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols);
m_checker = p.get_manager().mk_join_project_fn(checker(t1), checker(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols);
}
virtual table_base* operator()(const table_base & t1, const table_base & t2) {
table_base* ttocheck = (*m_tocheck)(tocheck(t1), tocheck(t2));
table_base* tchecker = (*m_checker)(checker(t1), checker(t2));
check_table* result = alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
return result;
}
};
table_join_fn * check_table_plugin::mk_join_project_fn(const table_base & t1, const table_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
const unsigned * removed_cols) {
if (!check_kind(t1) || !check_kind(t2)) {
return 0;
}
return alloc(join_project_fn, *this, t1, t2, col_cnt, cols1, cols2, removed_col_cnt, removed_cols);
}
class check_table_plugin::union_fn : public table_union_fn {
scoped_ptr<table_union_fn> m_tocheck;
scoped_ptr<table_union_fn> m_checker;
@ -120,7 +148,6 @@ namespace datalog {
}
table_base* operator()(table_base const& src) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
table_base* tchecker = (*m_checker)(checker(src));
table_base* ttocheck = (*m_tocheck)(tocheck(src));
check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker);
@ -135,6 +162,31 @@ namespace datalog {
return alloc(project_fn, *this, t, col_cnt, removed_cols);
}
class check_table_plugin::select_equal_and_project_fn : public table_transformer_fn {
scoped_ptr<table_transformer_fn> m_checker;
scoped_ptr<table_transformer_fn> m_tocheck;
public:
select_equal_and_project_fn(check_table_plugin& p, const table_base & t, const table_element & value, unsigned col) {
m_checker = p.get_manager().mk_select_equal_and_project_fn(checker(t), value, col);
m_tocheck = p.get_manager().mk_select_equal_and_project_fn(tocheck(t), value, col);
}
table_base* operator()(table_base const& src) {
table_base* tchecker = (*m_checker)(checker(src));
table_base* ttocheck = (*m_tocheck)(tocheck(src));
check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker);
return result;
}
};
table_transformer_fn * check_table_plugin::mk_select_equal_and_project_fn(const table_base & t,
const table_element & value, unsigned col) {
if (!check_kind(t)) {
return 0;
}
return alloc(select_equal_and_project_fn, *this, t, value, col);
}
class check_table_plugin::rename_fn : public table_transformer_fn {
scoped_ptr<table_transformer_fn> m_checker;
scoped_ptr<table_transformer_fn> m_tocheck;
@ -233,6 +285,33 @@ namespace datalog {
return 0;
}
class check_table_plugin::filter_interpreted_and_project_fn : public table_transformer_fn {
scoped_ptr<table_transformer_fn> m_checker;
scoped_ptr<table_transformer_fn> m_tocheck;
public:
filter_interpreted_and_project_fn(check_table_plugin& p, const table_base & t, app * condition,
unsigned removed_col_cnt, const unsigned * removed_cols)
{
m_checker = p.get_manager().mk_filter_interpreted_and_project_fn(checker(t), condition, removed_col_cnt, removed_cols);
m_tocheck = p.get_manager().mk_filter_interpreted_and_project_fn(tocheck(t), condition, removed_col_cnt, removed_cols);
}
table_base* operator()(table_base const& src) {
table_base* tchecker = (*m_checker)(checker(src));
table_base* ttocheck = (*m_tocheck)(tocheck(src));
check_table* result = alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
return result;
}
};
table_transformer_fn * check_table_plugin::mk_filter_interpreted_and_project_fn(const table_base & t,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) {
if (check_kind(t)) {
return alloc(filter_interpreted_and_project_fn, *this, t, condition, removed_col_cnt, removed_cols);
}
return 0;
}
class check_table_plugin::filter_by_negation_fn : public table_intersection_filter_fn {
scoped_ptr<table_intersection_filter_fn> m_checker;
scoped_ptr<table_intersection_filter_fn> m_tocheck;

10
src/muz_qe/dl_check_table.h
View file

@ -35,13 +35,16 @@ namespace datalog {
unsigned m_count;
protected:
class join_fn;
class join_project_fn;
class union_fn;
class transformer_fn;
class rename_fn;
class project_fn;
class select_equal_and_project_fn;
class filter_equal_fn;
class filter_identical_fn;
class filter_interpreted_fn;
class filter_interpreted_and_project_fn;
class filter_by_negation_fn;
public:
@ -54,10 +57,15 @@ namespace datalog {
virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
virtual table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
const unsigned * removed_cols);
virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src,
const table_base * delta);
virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt,
const unsigned * removed_cols);
virtual table_transformer_fn * mk_select_equal_and_project_fn(const table_base & t,
const table_element & value, unsigned col);
virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len,
const unsigned * permutation_cycle);
virtual table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt,
@ -65,6 +73,8 @@ namespace datalog {
virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value,
unsigned col);
virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition);
virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols);
virtual table_intersection_filter_fn * mk_filter_by_negation_fn(
const table_base & t,
const table_base & negated_obj, unsigned joined_col_cnt,

128
src/muz_qe/dl_compiler.cpp
View file

@ -73,6 +73,18 @@ namespace datalog {
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
SASSERT(!removed_cols.empty());
relation_signature res_sig;
relation_signature::from_project(m_reg_signatures[src], removed_cols.size(),
removed_cols.c_ptr(), res_sig);
result = get_fresh_register(res_sig);
acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond,
removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
reg_idx & result, instruction_block & acc) {
relation_signature res_sig;
@ -499,8 +511,7 @@ namespace datalog {
expr * arg = a->get_arg(i);
if(is_app(arg)) {
app * c = to_app(arg); //argument is a constant
SASSERT(c->get_num_args()==0);
SASSERT(m_context.get_decl_util().is_numeral_ext(arg));
SASSERT(m.is_value(c));
reg_idx new_reg;
make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc);
if(single_res!=t_reg) {
@ -620,6 +631,116 @@ namespace datalog {
}
// enforce interpreted tail predicates
unsigned ft_len = r->get_tail_size(); // full tail
ptr_vector<expr> tail;
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
tail.push_back(r->get_tail(tail_index));
}
if (!tail.empty()) {
app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m);
ptr_vector<sort> filter_vars;
get_free_vars(filter_cond, filter_vars);
// create binding
expr_ref_vector binding(m);
binding.resize(filter_vars.size()+1);
for (unsigned v = 0; v < filter_vars.size(); ++v) {
if (!filter_vars[v])
continue;
int2ints::entry * entry = var_indexes.find_core(v);
unsigned src_col;
if (entry) {
src_col = entry->get_data().m_value.back();
} else {
// we have an unbound variable, so we add an unbound column for it
relation_sort unbound_sort = filter_vars[v];
reg_idx new_reg;
bool new_dealloc;
make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg;
src_col = single_res_expr.size();
single_res_expr.push_back(m.mk_var(v, unbound_sort));
entry = var_indexes.insert_if_not_there2(v, unsigned_vector());
entry->get_data().m_value.push_back(src_col);
}
relation_sort var_sort = m_reg_signatures[filtered_res][src_col];
binding[filter_vars.size()-v] = m.mk_var(src_col, var_sort);
}
// check if there are any columns to remove
unsigned_vector remove_columns;
{
unsigned_vector var_idx_to_remove;
ptr_vector<sort> vars;
get_free_vars(r->get_head(), vars);
for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end();
I != E; ++I) {
unsigned var_idx = I->m_key;
if (!vars.get(var_idx, 0)) {
unsigned_vector & cols = I->m_value;
for (unsigned i = 0; i < cols.size(); ++i) {
remove_columns.push_back(cols[i]);
}
var_idx_to_remove.push_back(var_idx);
}
}
for (unsigned i = 0; i < var_idx_to_remove.size(); ++i) {
var_indexes.remove(var_idx_to_remove[i]);
}
// update column idx for after projection state
if (!remove_columns.empty()) {
unsigned_vector offsets;
offsets.resize(single_res_expr.size(), 0);
for (unsigned i = 0; i < remove_columns.size(); ++i) {
for (unsigned col = remove_columns[i]; col < offsets.size(); ++col) {
++offsets[col];
}
}
for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end();
I != E; ++I) {
unsigned_vector & cols = I->m_value;
for (unsigned i = 0; i < cols.size(); ++i) {
cols[i] -= offsets[cols[i]];
}
}
}
}
expr_ref renamed(m);
m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr(), renamed);
app_ref app_renamed(to_app(renamed), m);
if (remove_columns.empty()) {
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
} else {
reg_idx new_reg;
std::sort(remove_columns.begin(), remove_columns.end());
make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, new_reg, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
filtered_res = new_reg;
}
dealloc = true;
}
#if 0
// this version is potentially better for non-symbolic tables,
// since it constraints each unbound column at a time (reducing the
// size of intermediate results).
unsigned ft_len=r->get_tail_size(); //full tail
for(unsigned tail_index=ut_len; tail_index<ft_len; tail_index++) {
app * t = r->get_tail(tail_index);
@ -687,6 +808,7 @@ namespace datalog {
acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
dealloc = true;
}
#endif
{
//put together the columns of head relation
@ -738,7 +860,7 @@ namespace datalog {
make_dealloc_non_void(new_head_reg, acc);
}
finish:
// finish:
m_instruction_observer.finish_rule();
}

2
src/muz_qe/dl_compiler.h
View file

@ -145,6 +145,8 @@ namespace datalog {
instruction_block & acc);
void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars,
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc);
void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc);
void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
reg_idx & result, instruction_block & acc);
/**

434
src/muz_qe/dl_hassel_common.cpp Executable file
View file

@ -0,0 +1,434 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_hassel_common.cpp
Abstract:
<abstract>
Revision History:
--*/
#include "dl_hassel_common.h"
#include "dl_context.h"
#include <vector>
namespace datalog {
static void formula_to_dnf_aux(app *and, unsigned idx, std::set<expr*>& conjexpr, std::set<expr*>& toplevel, ast_manager& m) {
if (idx == and->get_num_args()) {
std::vector<expr*> v(conjexpr.begin(), conjexpr.end());
toplevel.insert(m.mk_and((unsigned)v.size(), &v[0]));
return;
}
expr *e = and->get_arg(idx);
if (is_app(e) && to_app(e)->get_decl_kind() == OP_OR) {
app *or = to_app(e);
// quick subsumption test: if any of the elements of the OR is already ANDed, then we skip this OR
for (unsigned i = 0; i < or->get_num_args(); ++i) {
if (conjexpr.count(or->get_arg(i))) {
formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m);
return;
}
}
for (unsigned i = 0; i < or->get_num_args(); ++i) {
std::set<expr*> conjexpr2(conjexpr);
conjexpr2.insert(or->get_arg(i));
formula_to_dnf_aux(and, idx+1, conjexpr2, toplevel, m);
}
} else {
conjexpr.insert(e);
formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m);
}
}
expr_ref formula_to_dnf(expr_ref f) {
app *a = to_app(f);
SASSERT(a->get_decl_kind() == OP_AND);
std::set<expr*> toplevel, conjexpr;
formula_to_dnf_aux(a, 0, conjexpr, toplevel, f.m());
if (toplevel.size() > 1) {
std::vector<expr*> v(toplevel.begin(), toplevel.end());
return expr_ref(f.m().mk_or((unsigned)v.size(), &v[0]), f.m());
} else {
return expr_ref(*toplevel.begin(), f.m());
}
}
bool bit_vector::contains(const bit_vector & other) const {
unsigned n = num_words();
if (n == 0)
return true;
for (unsigned i = 0; i < n - 1; ++i) {
if ((m_data[i] & other.m_data[i]) != other.m_data[i])
return false;
}
unsigned bit_rest = m_num_bits % 32;
unsigned mask = (1 << bit_rest) - 1;
if (mask == 0) mask = UINT_MAX;
unsigned other_data = other.m_data[n-1] & mask;
return (m_data[n-1] & other_data) == other_data;
}
bool bit_vector::contains(const bit_vector & other, unsigned idx) const {
// TODO: optimize this to avoid copy
return slice(idx, other.size()).contains(other);
}
bool bit_vector::contains_consecutive_zeros() const {
unsigned n = num_words();
if (n == 0)
return false;
for (unsigned i = 0; i < n - 1; ++i) {
if ((((m_data[i] << 1) | m_data[i]) & 0xAAAAAAAA) != 0xAAAAAAAA)
return true;
}
unsigned bit_rest = m_num_bits % 32;
unsigned mask = (1 << bit_rest) - 1;
if (mask == 0) mask = UINT_MAX;
mask &= 0xAAAAAAAA;
return ((((m_data[n-1] << 1) | m_data[n-1]) & mask) != mask);
}
bit_vector bit_vector::slice(unsigned idx, unsigned length) const {
bit_vector Res(length);
// TODO: optimize w/ memcpy when possible
for (unsigned i = idx; i < idx + length; ++i) {
Res.push_back(get(i));
}
SASSERT(Res.size() == length);
return Res;
}
void bit_vector::append(const bit_vector & other) {
if (other.empty())
return;
if ((m_num_bits % 32) == 0) {
unsigned prev_num_bits = m_num_bits;
resize(m_num_bits + other.m_num_bits);
memcpy(&get_bit_word(prev_num_bits), other.m_data, other.num_words() * sizeof(unsigned));
return;
}
// TODO: optimize the other cases.
for (unsigned i = 0; i < other.m_num_bits; ++i) {
push_back(other.get(i));
}
}
uint64 bit_vector::to_number(unsigned idx, unsigned length) const {
SASSERT(length <= 64);
uint64 r = 0;
for (unsigned i = 0; i < length; ++i) {
r = (r << 1) | (uint64)get(idx+i);
}
return r;
}
bool bit_vector::operator<(bit_vector const & other) const {
SASSERT(m_num_bits == other.m_num_bits);
unsigned n = num_words();
if (n == 0)
return false;
for (unsigned i = 0; i < n - 1; ++i) {
if (m_data[i] > other.m_data[i])
return false;
if (m_data[i] < other.m_data[i])
return true;
}
unsigned bit_rest = m_num_bits % 32;
unsigned mask = (1 << bit_rest) - 1;
if (mask == 0) mask = UINT_MAX;
return (m_data[n-1] & mask) < (other.m_data[n-1] & mask);
}
table_information::table_information(table_plugin & p, const table_signature& sig) :
m_column_info(sig.size()+1),
m_bv_util(p.get_context().get_manager()),
m_decl_util(p.get_context().get_manager()) {
unsigned column = 0;
for (unsigned i = 0; i < sig.size(); ++i) {
unsigned num_bits = uint64_log2(sig[i]);
SASSERT(num_bits == 64 || (1ULL << num_bits) == sig[i]);
m_column_info[i] = column;
column += num_bits;
}
m_column_info[sig.size()] = column;
}
void table_information::expand_column_vector(unsigned_vector& v, const table_information *other) const {
unsigned_vector orig;
orig.swap(v);
for (unsigned i = 0; i < orig.size(); ++i) {
unsigned col, limit;
if (orig[i] < get_num_cols()) {
col = column_idx(orig[i]);
limit = col + column_num_bits(orig[i]);
} else {
unsigned idx = orig[i] - get_num_cols();
col = get_num_bits() + other->column_idx(idx);
limit = col + other->column_num_bits(idx);
}
for (; col < limit; ++col) {
v.push_back(col);
}
}
}
void table_information::display(std::ostream & out) const {
out << '<';
for (unsigned i = 0; i < get_num_cols(); ++i) {
if (i > 0)
out << ", ";
out << column_num_bits(i);
}
out << ">\n";
}
ternary_bitvector::ternary_bitvector(unsigned size, bool full) :
bit_vector() {
resize(size, full);
}
ternary_bitvector::ternary_bitvector(uint64 n, unsigned num_bits) :
bit_vector(2 * num_bits) {
append_number(n, num_bits);
}
ternary_bitvector::ternary_bitvector(const table_fact& f, const table_information& t) :
bit_vector(2 * t.get_num_bits()) {
for (unsigned i = 0; i < f.size(); ++i) {
SASSERT(t.column_idx(i) == size());
append_number(f[i], t.column_num_bits(i));
}
SASSERT(size() == t.get_num_bits());
}
void ternary_bitvector::fill1() {
memset(m_data, 0xFF, m_capacity * sizeof(unsigned));
}
unsigned ternary_bitvector::get(unsigned idx) const {
idx *= 2;
return (bit_vector::get(idx) << 1) | (unsigned)bit_vector::get(idx+1);
}
void ternary_bitvector::set(unsigned idx, unsigned val) {
SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x);
idx *= 2;
bit_vector::set(idx, (val >> 1) != 0);
bit_vector::set(idx+1, (val & 1) != 0);
}
void ternary_bitvector::push_back(unsigned val) {
SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x);
bit_vector::push_back((val >> 1) != 0);
bit_vector::push_back((val & 1) != 0);
}
void ternary_bitvector::append_number(uint64 n, unsigned num_bits) {
SASSERT(num_bits <= 64);
for (int bit = num_bits-1; bit >= 0; --bit) {
if (n & (1ULL << bit)) {
push_back(BIT_1);
} else {
push_back(BIT_0);
}
}
}
void ternary_bitvector::mk_idx_eq(unsigned idx, ternary_bitvector& val) {
for (unsigned i = 0; i < val.size(); ++i) {
set(idx+i, val.get(i));
}
}
ternary_bitvector ternary_bitvector::and(const ternary_bitvector& other) const{
ternary_bitvector result(*this);
result &= other;
return result;
}
void ternary_bitvector::neg(union_ternary_bitvector<ternary_bitvector>& result) const {
ternary_bitvector negated;
negated.resize(size());
for (unsigned i = 0; i < size(); ++i) {
switch (get(i)) {
case BIT_0:
negated.fill1();
negated.set(i, BIT_1);
break;
case BIT_1:
negated.fill1();
negated.set(i, BIT_0);
break;
default:
continue;
}
result.add_fact(negated);
}
}
static void join_fix_eqs(ternary_bitvector& TBV, unsigned idx, unsigned col2_offset,
const unsigned_vector& cols1, const unsigned_vector& cols2,
union_ternary_bitvector<ternary_bitvector>& result) {
if (idx == cols1.size()) {
result.add_fact(TBV);
return;
}
unsigned idx1 = cols1[idx];
unsigned idx2 = cols2[idx] + col2_offset;
unsigned v1 = TBV.get(idx1);
unsigned v2 = TBV.get(idx2);
if (v1 == BIT_x) {
if (v2 == BIT_x) {
// both x: duplicate row
ternary_bitvector TBV2(TBV);
TBV2.set(idx1, BIT_0);
TBV2.set(idx2, BIT_0);
join_fix_eqs(TBV2, idx+1, col2_offset, cols1, cols2, result);
TBV.set(idx1, BIT_1);
TBV.set(idx2, BIT_1);
} else {
TBV.set(idx1, v2);
}
} else if (v2 == BIT_x) {
TBV.set(idx2, v1);
} else if (v1 != v2) {
// columns don't match
return;
}
join_fix_eqs(TBV, idx+1, col2_offset, cols1, cols2, result);
}
void ternary_bitvector::join(const ternary_bitvector& other,
const unsigned_vector& cols1,
const unsigned_vector& cols2,
union_ternary_bitvector<ternary_bitvector>& result) const {
ternary_bitvector TBV(*this);
TBV.append(other);
join_fix_eqs(TBV, 0, size(), cols1, cols2, result);
}
bool ternary_bitvector::project(const unsigned_vector& delcols, ternary_bitvector& result) const {
unsigned *rm_cols = delcols.c_ptr();
for (unsigned i = 0; i < size(); ++i) {
if (*rm_cols == i) {
++rm_cols;
continue;
}
result.push_back(get(i));
}
return true;
}
static void copy_column(ternary_bitvector& CopyTo, const ternary_bitvector& CopyFrom,
unsigned col_dst, unsigned col_src, const table_information& src_table,
const table_information& dst_table) {
unsigned idx_dst = dst_table.column_idx(col_dst);
unsigned idx_src = src_table.column_idx(col_src);
unsigned num_bits = dst_table.column_num_bits(col_dst);
SASSERT(num_bits == src_table.column_num_bits(col_src));
for (unsigned i = 0; i < num_bits; ++i) {
CopyTo.set(idx_dst+i, CopyFrom.get(idx_src+i));
}
}
void ternary_bitvector::rename(const unsigned_vector& cyclecols,
const unsigned_vector& out_of_cycle_cols,
const table_information& src_table,
const table_information& dst_table,
ternary_bitvector& result) const {
result.resize(dst_table.get_num_bits());
for (unsigned i = 1; i < cyclecols.size(); ++i) {
copy_column(result, *this, cyclecols[i-1], cyclecols[i], src_table, dst_table);
}
copy_column(result, *this, cyclecols[cyclecols.size()-1], cyclecols[0], src_table, dst_table);
for (unsigned i = 0; i < out_of_cycle_cols.size(); ++i) {
unsigned col = out_of_cycle_cols[i];
copy_column(result, *this, col, col, src_table, dst_table);
}
}
unsigned ternary_bitvector::size_in_bytes() const {
return sizeof(*this) + m_capacity;
}
void ternary_bitvector::display(std::ostream & out) const {
for (unsigned i = 0; i < size(); ++i) {
switch (get(i)) {
case BIT_0:
out << '0';
break;
case BIT_1:
out << '1';
break;
case BIT_x:
out << 'x';
break;
default:
UNREACHABLE();
}
}
}
#if Z3DEBUG
void ternary_bitvector::expand(std::set<bit_vector> & BVs) const {
bit_vector BV(m_num_bits);
expand(BVs, BV, 0);
}
void ternary_bitvector::expand(std::set<bit_vector> & BVs, bit_vector &BV, unsigned idx) const {
if (idx == size()) {
BVs.insert(BV);
return;
}
switch (get(idx)) {
case BIT_0:
BV.push_back(false);
expand(BVs, BV, idx+1);
break;
case BIT_1:
BV.push_back(true);
expand(BVs, BV, idx+1);
break;
case BIT_x: { // x: duplicate
bit_vector BV2(BV);
BV.push_back(false);
BV2.push_back(true);
expand(BVs, BV, idx+1);
expand(BVs, BV2, idx+1);
}
break;
default:
UNREACHABLE();
}
}
#endif
}

1079
src/muz_qe/dl_hassel_common.h Executable file
View file

File diff suppressed because it is too large Load diff

219
src/muz_qe/dl_hassel_diff_table.cpp Executable file
View file

@ -0,0 +1,219 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_hassel_diff_table.cpp
Abstract:
<abstract>
Revision History:
--*/
#include "ast_printer.h"
#include "dl_context.h"
#include "dl_util.h"
#include "dl_hassel_diff_table.h"
namespace datalog {
ternary_diff_bitvector::ternary_diff_bitvector(unsigned size, bool full) :
m_pos(size, full), m_neg(size) { }
ternary_diff_bitvector::ternary_diff_bitvector(uint64 n, unsigned num_bits) :
m_pos(n, num_bits), m_neg(num_bits) { }
ternary_diff_bitvector::ternary_diff_bitvector(const ternary_bitvector & tbv) :
m_pos(tbv), m_neg(tbv.size()) { }
bool ternary_diff_bitvector::contains(const ternary_diff_bitvector & other) const {
return m_pos.contains(other.m_pos) && other.m_neg.contains(m_neg);
}
bool ternary_diff_bitvector::is_empty() const {
if (m_pos.is_empty())
return true;
return m_neg.contains(m_pos);
}
ternary_diff_bitvector ternary_diff_bitvector::and(const ternary_diff_bitvector& other) const {
ternary_diff_bitvector result(m_pos.and(other.m_pos));
result.m_neg.swap(m_neg.or(other.m_neg));
return result;
}
void ternary_diff_bitvector::neg(union_ternary_bitvector<ternary_diff_bitvector>& result) const {
// not(A\B) <-> (T\A) U B
ternary_diff_bitvector negated(size(), true);
negated.m_neg.add_new_fact(m_pos);
result.add_fact(negated);
for (union_ternary_bitvector<ternary_bitvector>::const_iterator I = m_neg.begin(),
E = m_neg.end(); I != E; ++I) {
result.add_fact(*I);
}
}
void ternary_diff_bitvector::subtract(const union_ternary_bitvector<ternary_diff_bitvector>& other,
union_ternary_bitvector<ternary_diff_bitvector>& result) const {
ternary_diff_bitvector newfact(*this);
for (union_ternary_bitvector<ternary_diff_bitvector>::const_iterator I = other.begin(),
E = other.end(); I != E; ++I) {
if (!I->m_neg.empty()) {
NOT_IMPLEMENTED_YET();
}
newfact.m_neg.add_fact(I->m_pos);
}
if (!newfact.is_empty())
result.add_fact(newfact);
}
void ternary_diff_bitvector::join(const ternary_diff_bitvector& other,
const unsigned_vector& cols1,
const unsigned_vector& cols2,
union_ternary_bitvector<ternary_diff_bitvector>& result) const {
unsigned new_size = size() + other.size();
ternary_diff_bitvector res(new_size);
res.m_pos = m_pos;
res.m_pos.append(other.m_pos);
for (unsigned i = 0; i < cols1.size(); ++i) {
unsigned idx1 = cols1[i];
unsigned idx2 = size() + cols2[i];
unsigned v1 = res.m_pos.get(idx1);
unsigned v2 = res.m_pos.get(idx2);
if (v1 == BIT_x) {
if (v2 == BIT_x) {
// add to subtracted TBVs: 1xx0 and 0xx1
{
ternary_bitvector r(new_size, true);
r.set(idx1, BIT_0);
r.set(idx2, BIT_1);
res.m_neg.add_new_fact(r);
}
{
ternary_bitvector r(new_size, true);
r.set(idx1, BIT_1);
r.set(idx2, BIT_0);
res.m_neg.add_new_fact(r);
}
} else {
res.m_pos.set(idx1, v2);
}
} else if (v2 == BIT_x) {
res.m_pos.set(idx2, v1);
} else if (v1 != v2) {
// columns don't match
return;
}
}
// handle subtracted TBVs: 1010 -> 1010xxx
if (!m_neg.empty()) {
ternary_bitvector padding(other.size(), true);
for (union_ternary_bitvector<ternary_bitvector>::const_iterator I = m_neg.begin(),
E = m_neg.end(); I != E; ++I) {
ternary_bitvector BV(*I);
BV.append(padding);
res.m_neg.add_new_fact(BV);
}
}
if (!other.m_neg.empty()) {
ternary_bitvector padding(size(), true);
for (union_ternary_bitvector<ternary_bitvector>::const_iterator I = other.m_neg.begin(),
E = other.m_neg.end(); I != E; ++I) {
ternary_bitvector BV(padding);
BV.append(*I);
res.m_neg.add_new_fact(BV);
}
}
result.add_fact(res);
}
bool ternary_diff_bitvector::project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const {
m_pos.project(delcols, result.m_pos);
if (m_neg.empty())
return true;
ternary_bitvector newneg;
for (union_ternary_bitvector<ternary_bitvector>::const_iterator I = m_neg.begin(),
E = m_neg.end(); I != E; ++I) {
for (unsigned i = 0; i < delcols.size()-1; ++i) {
unsigned idx = delcols[i];
if (I->get(idx) != BIT_x && m_pos.get(idx) == BIT_x)
goto skip_row;
}
newneg.reset();
I->project(delcols, newneg);
result.m_neg.add_fact(newneg);
skip_row: ;
}
return !result.is_empty();
}
void ternary_diff_bitvector::rename(const unsigned_vector& cyclecols,
const unsigned_vector& out_of_cycle_cols,
const table_information& src_table,
const table_information& dst_table,
ternary_diff_bitvector& result) const {
m_pos.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_pos);
m_neg.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_neg);
}
unsigned ternary_diff_bitvector::get(unsigned idx) {
return m_pos.get(idx);
}
void ternary_diff_bitvector::set(unsigned idx, unsigned val) {
m_pos.set(idx, val);
}
void ternary_diff_bitvector::swap(ternary_diff_bitvector & other) {
m_pos.swap(other.m_pos);
m_neg.swap(other.m_neg);
}
void ternary_diff_bitvector::reset() {
m_pos.reset();
m_neg.reset();
}
void ternary_diff_bitvector::display(std::ostream & out) const {
m_pos.display(out);
if (!m_neg.empty()) {
out << " \\ ";
if (m_neg.num_disjs() > 1) out << '(';
m_neg.display(out);
if (m_neg.num_disjs() > 1) out << ')';
}
}
unsigned ternary_diff_bitvector::size_in_bytes() const {
return m_pos.size_in_bytes() + m_neg.num_bytes();
}
#if Z3DEBUG
void ternary_diff_bitvector::expand(std::set<bit_vector> & BVs) const {
m_pos.expand(BVs);
SASSERT(!BVs.empty());
std::set<bit_vector> NegBVs;
m_neg.expand(NegBVs);
BVs.erase(NegBVs.begin(), NegBVs.end());
}
#endif
hassel_diff_table_plugin::hassel_diff_table_plugin(relation_manager & manager)
: common_hassel_table_plugin(symbol("hassel_diff"), manager) {}
}

87
src/muz_qe/dl_hassel_diff_table.h Executable file
View file

@ -0,0 +1,87 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_hassel_diff_table.h
Abstract:
<abstract>
Revision History:
--*/
#ifndef _DL_HASSEL_DIFF_TABLE_H_
#define _DL_HASSEL_DIFF_TABLE_H_
#include "dl_hassel_common.h"
namespace datalog {
class hassel_diff_table;
class ternary_diff_bitvector {
// pos \ (neg0 \/ ... \/ negn)
ternary_bitvector m_pos;
union_ternary_bitvector<ternary_bitvector> m_neg;
public:
ternary_diff_bitvector() : m_pos(), m_neg(0) {}
ternary_diff_bitvector(unsigned size) : m_pos(size), m_neg(size) {}
ternary_diff_bitvector(unsigned size, bool full);
ternary_diff_bitvector(uint64 n, unsigned num_bits);
ternary_diff_bitvector(const ternary_bitvector & tbv);
bool contains(const ternary_diff_bitvector & other) const;
bool is_empty() const;
ternary_diff_bitvector and(const ternary_diff_bitvector& other) const;
void neg(union_ternary_bitvector<ternary_diff_bitvector>& result) const;
static bool has_subtract() { return true; }
void subtract(const union_ternary_bitvector<ternary_diff_bitvector>& other,
union_ternary_bitvector<ternary_diff_bitvector>& result) const;
void join(const ternary_diff_bitvector& other, const unsigned_vector& cols1,
const unsigned_vector& cols2, union_ternary_bitvector<ternary_diff_bitvector>& result) const;
bool project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const;
void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols,
const table_information& src_table, const table_information& dst_table,
ternary_diff_bitvector& result) const;
unsigned get(unsigned idx);
void set(unsigned idx, unsigned val);
void swap(ternary_diff_bitvector & other);
void reset();
unsigned size() const { return m_pos.size(); }
void display(std::ostream & out) const;
unsigned size_in_bytes() const;
#if Z3DEBUG
void expand(std::set<bit_vector> & BVs) const;
#endif
};
typedef union_ternary_bitvector<ternary_diff_bitvector> union_ternary_diff_bitvector;
class hassel_diff_table : public common_hassel_table<union_ternary_diff_bitvector> {
public:
hassel_diff_table(table_plugin & p, const table_signature & sig) :
common_hassel_table(p, sig) {}
};
class hassel_diff_table_plugin : public common_hassel_table_plugin<hassel_diff_table> {
public:
hassel_diff_table_plugin(relation_manager & manager);
};
}
#endif

27
src/muz_qe/dl_hassel_table.cpp Normal file
View file

@ -0,0 +1,27 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_hassel_table.cpp
Abstract:
<abstract>
Revision History:
--*/
#include "ast_printer.h"
#include "dl_context.h"
#include "dl_util.h"
#include "dl_hassel_table.h"
namespace datalog {
hassel_table_plugin::hassel_table_plugin(relation_manager & manager)
: common_hassel_table_plugin(symbol("hassel"), manager) {}
}

39
src/muz_qe/dl_hassel_table.h Normal file
View file

@ -0,0 +1,39 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_hassel_table.h
Abstract:
<abstract>
Revision History:
--*/
#ifndef _DL_HASSEL_TABLE_H_
#define _DL_HASSEL_TABLE_H_
#include "dl_hassel_common.h"
namespace datalog {
class hassel_table;
typedef union_ternary_bitvector<ternary_bitvector> union_ternary_bitvectors;
class hassel_table : public common_hassel_table<union_ternary_bitvectors> {
public:
hassel_table(table_plugin & p, const table_signature & sig) :
common_hassel_table(p, sig) {}
};
class hassel_table_plugin : public common_hassel_table_plugin<hassel_table> {
public:
hassel_table_plugin(relation_manager & manager);
};
}
#endif

59
src/muz_qe/dl_instruction.cpp
View file

@ -526,6 +526,64 @@ namespace datalog {
return alloc(instr_filter_interpreted, reg, condition);
}
class instr_filter_interpreted_and_project : public instruction {
reg_idx m_src;
reg_idx m_res;
app_ref m_cond;
unsigned_vector m_cols;
public:
instr_filter_interpreted_and_project(reg_idx src, app_ref & condition,
unsigned col_cnt, const unsigned * removed_cols, reg_idx result)
: m_src(src), m_cond(condition), m_cols(col_cnt, removed_cols),
m_res(result) {}
virtual bool perform(execution_context & ctx) {
if (!ctx.reg(m_src)) {
ctx.make_empty(m_res);
return true;
}
relation_transformer_fn * fn;
relation_base & reg = *ctx.reg(m_src);
if (!find_fn(reg, fn)) {
fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr());
if (!fn) {
throw default_exception(
"trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s",
reg.get_plugin().get_name().bare_str());
}
store_fn(reg, fn);
}
ctx.set_reg(m_res, (*fn)(reg));
if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
ctx.make_empty(m_res);
}
return true;
}
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "filter_interpreted_and_project " << m_src << " into " << m_res;
out << " using " << mk_pp(m_cond, m_cond.get_manager());
out << " deleting columns ";
print_container(m_cols, out);
}
virtual void make_annotations(execution_context & ctx) {
std::stringstream s;
std::string a = "rel_src";
ctx.get_register_annotation(m_src, a);
s << "filter_interpreted_and_project " << mk_pp(m_cond, m_cond.get_manager());
ctx.set_register_annotation(m_res, s.str());
}
};
instruction * instruction::mk_filter_interpreted_and_project(reg_idx reg, app_ref & condition,
unsigned col_cnt, const unsigned * removed_cols, reg_idx result) {
return alloc(instr_filter_interpreted_and_project, reg, condition, col_cnt, removed_cols, result);
}
class instr_union : public instruction {
reg_idx m_src;
@ -592,6 +650,7 @@ namespace datalog {
}
}
SASSERT(r_src.get_signature().size() == r_tgt.get_signature().size());
TRACE("dl_verbose", r_tgt.display(tout <<"pre-union:"););
(*fn)(r_tgt, r_src, r_delta);

2
src/muz_qe/dl_instruction.h
View file

@ -260,6 +260,8 @@ namespace datalog {
static instruction * mk_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col);
static instruction * mk_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols);
static instruction * mk_filter_interpreted(reg_idx reg, app_ref & condition);
static instruction * mk_filter_interpreted_and_project(reg_idx src, app_ref & condition,
unsigned col_cnt, const unsigned * removed_cols, reg_idx result);
static instruction * mk_union(reg_idx src, reg_idx tgt, reg_idx delta);
static instruction * mk_widen(reg_idx src, reg_idx tgt, reg_idx delta);
static instruction * mk_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols,

23
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -141,13 +141,17 @@ namespace datalog {
func_decl_ref_vector const& new_funcs() const { return m_new_funcs; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
bool found = false;
for (unsigned j = 0; !found && j < num; ++j) {
found = m_util.is_mkbv(args[j]);
}
if (!found) {
if (num == 0) {
if (m_src->is_output_predicate(f))
m_dst->set_output_predicate(f);
return BR_FAILED;
}
for (unsigned i = 0; i < num; ++i) {
if (!m_util.is_mkbv(args[i]))
return BR_FAILED;
}
//
// f(mk_bv(args),...)
//
@ -260,7 +264,7 @@ namespace datalog {
m_rewriter.m_cfg.set_dst(result);
for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
rule * r = source.get_rule(i);
r->to_formula(fml);
r->to_formula(fml);
if (blast(r, fml)) {
proof_ref pr(m);
if (m_context.generate_proof_trace()) {
@ -275,6 +279,13 @@ namespace datalog {
result->add_rule(r);
}
}
// copy output predicates without any rule (bit-blasting not really needed)
const func_decl_set& decls = source.get_output_predicates();
for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) {
if (!source.contains(*I))
result->set_output_predicate(*I);
}
if (m_context.get_model_converter()) {
filter_model_converter* fmc = alloc(filter_model_converter, m);

83
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -37,6 +37,7 @@ Revision History:
#include"bool_rewriter.h"
#include"dl_mk_backwards.h"
#include"dl_mk_loop_counter.h"
#include "for_each_expr.h"
namespace datalog {
@ -47,7 +48,8 @@ namespace datalog {
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_inner_ctx(m, ctx.get_fparams()),
a(m) {
a(m),
m_pinned(m) {
params_ref params;
params.set_sym("default_relation", symbol("karr_relation"));
params.set_sym("engine", symbol("datalog"));
@ -201,29 +203,27 @@ namespace datalog {
return 0;
}
}
mk_loop_counter lc(m_ctx);
mk_backwards bwd(m_ctx);
scoped_ptr<rule_set> src_loop = lc(source);
TRACE("dl", src_loop->display(tout << "source loop\n"););
// run propagation forwards, then backwards
scoped_ptr<rule_set> src_annot = update_using_propagation(*src_loop, *src_loop);
TRACE("dl", src_annot->display(tout << "updated using propagation\n"););
get_invariants(*src_loop);
#if 0
// figure out whether to update same rules as used for saturation.
scoped_ptr<rule_set> rev_source = bwd(*src_annot);
src_annot = update_using_propagation(*src_annot, *rev_source);
#endif
scoped_ptr<rule_set> rev_source = bwd(*src_loop);
get_invariants(*rev_source);
scoped_ptr<rule_set> src_annot = update_rules(*src_loop);
rule_set* rules = lc.revert(*src_annot);
rules->inherit_predicates(source);
TRACE("dl", rules->display(tout););
m_pinned.reset();
m_fun2inv.reset();
return rules;
}
rule_set* mk_karr_invariants::update_using_propagation(rule_set const& src, rule_set const& srcref) {
void mk_karr_invariants::get_invariants(rule_set const& src) {
m_inner_ctx.reset();
rel_context& rctx = m_inner_ctx.get_rel_context();
ptr_vector<func_decl> heads;
@ -232,19 +232,41 @@ namespace datalog {
m_inner_ctx.register_predicate(*fit, false);
}
m_inner_ctx.ensure_opened();
m_inner_ctx.replace_rules(srcref);
m_inner_ctx.replace_rules(src);
m_inner_ctx.close();
rule_set::decl2rules::iterator dit = srcref.begin_grouped_rules();
rule_set::decl2rules::iterator dend = srcref.end_grouped_rules();
rule_set::decl2rules::iterator dit = src.begin_grouped_rules();
rule_set::decl2rules::iterator dend = src.end_grouped_rules();
for (; dit != dend; ++dit) {
heads.push_back(dit->m_key);
}
m_inner_ctx.rel_query(heads.size(), heads.c_ptr());
rule_set* dst = alloc(rule_set, m_ctx);
// retrieve invariants.
dit = src.begin_grouped_rules();
for (; dit != dend; ++dit) {
func_decl* p = dit->m_key;
relation_base* rb = rctx.try_get_relation(p);
if (rb) {
expr_ref fml(m);
rb->to_formula(fml);
if (m.is_true(fml)) {
continue;
}
expr* inv = 0;
if (m_fun2inv.find(p, inv)) {
fml = m.mk_and(inv, fml);
}
m_pinned.push_back(fml);
m_fun2inv.insert(p, fml);
}
}
}
rule_set* mk_karr_invariants::update_rules(rule_set const& src) {
scoped_ptr<rule_set> dst = alloc(rule_set, m_ctx);
rule_set::iterator it = src.begin(), end = src.end();
for (; it != end; ++it) {
update_body(rctx, *dst, **it);
update_body(*dst, **it);
}
if (m_ctx.get_model_converter()) {
add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m);
@ -252,10 +274,8 @@ namespace datalog {
rule_set::decl2rules::iterator gend = src.end_grouped_rules();
for (; git != gend; ++git) {
func_decl* p = git->m_key;
expr_ref fml(m);
relation_base* rb = rctx.try_get_relation(p);
if (rb) {
rb->to_formula(fml);
expr* fml = 0;
if (m_fun2inv.find(p, fml)) {
kmc->add(p, fml);
}
}
@ -263,10 +283,10 @@ namespace datalog {
}
dst->inherit_predicates(src);
return dst;
return dst.detach();
}
void mk_karr_invariants::update_body(rel_context& rctx, rule_set& rules, rule& r) {
void mk_karr_invariants::update_body(rule_set& rules, rule& r) {
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
app_ref_vector tail(m);
@ -275,17 +295,17 @@ namespace datalog {
tail.push_back(r.get_tail(i));
}
for (unsigned i = 0; i < utsz; ++i) {
func_decl* q = r.get_decl(i);
relation_base* rb = rctx.try_get_relation(r.get_decl(i));
if (rb) {
rb->to_formula(fml);
func_decl* q = r.get_decl(i);
expr* fml = 0;
if (m_fun2inv.find(q, fml)) {
expr_safe_replace rep(m);
for (unsigned j = 0; j < q->get_arity(); ++j) {
rep.insert(m.mk_var(j, q->get_domain(j)),
r.get_tail(i)->get_arg(j));
}
rep(fml);
tail.push_back(to_app(fml));
expr_ref tmp(fml, m);
rep(tmp);
tail.push_back(to_app(tmp));
}
}
rule* new_rule = &r;
@ -1029,16 +1049,17 @@ namespace datalog {
class karr_relation_plugin::filter_equal_fn : public relation_mutator_fn {
unsigned m_col;
rational m_value;
bool m_valid;
public:
filter_equal_fn(relation_manager & m, const relation_element & value, unsigned col)
: m_col(col) {
arith_util arith(m.get_context().get_manager());
VERIFY(arith.is_numeral(value, m_value));
m_valid = arith.is_numeral(value, m_value) && m_value.is_int();
}
virtual void operator()(relation_base & _r) {
karr_relation & r = get(_r);
if (m_value.is_int()) {
if (m_valid) {
r.get_ineqs();
vector<rational> row;
row.resize(r.get_signature().size());
@ -1054,7 +1075,7 @@ namespace datalog {
relation_mutator_fn * karr_relation_plugin::mk_filter_equal_fn(const relation_base & r,
const relation_element & value, unsigned col) {
if(check_kind(r)) {
if (check_kind(r)) {
return alloc(filter_equal_fn, get_manager(), value, col);
}
return 0;

16
src/muz_qe/dl_mk_karr_invariants.h
View file

@ -55,8 +55,13 @@ namespace datalog {
rule_manager& rm;
context m_inner_ctx;
arith_util a;
void update_body(rel_context& rctx, rule_set& result, rule& r);
rule_set* update_using_propagation(rule_set const& src, rule_set const& srcref);
obj_map<func_decl, expr*> m_fun2inv;
ast_ref_vector m_pinned;
void get_invariants(rule_set const& src);
void update_body(rule_set& result, rule& r);
rule_set* update_rules(rule_set const& src);
public:
mk_karr_invariants(context & ctx, unsigned priority);
@ -89,12 +94,7 @@ namespace datalog {
{}
virtual bool can_handle_signature(const relation_signature & sig) {
for (unsigned i = 0; i < sig.size(); ++i) {
if (a.is_int(sig[i])) {
return true;
}
}
return false;
return true;
}
static symbol get_name() { return symbol("karr_relation"); }

6
src/muz_qe/dl_mk_slice.cpp
View file

@ -710,6 +710,7 @@ namespace datalog {
void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) {
obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end();
ptr_vector<sort> domain;
bool has_output = false;
func_decl* f;
for (; it != end; ++it) {
domain.reset();
@ -731,8 +732,13 @@ namespace datalog {
}
else if (src.is_output_predicate(p)) {
dst.set_output_predicate(p);
has_output = true;
}
}
// disable slicing if the output predicates don't occur in rules.
if (!has_output) {
m_predicates.reset();
}
}
bool mk_slice::rule_updated(rule const& r) {

10
src/muz_qe/dl_product_relation.cpp
View file

@ -269,7 +269,7 @@ namespace datalog {
unsigned_vector r1_tables_indexes;
unsigned_vector r2_tables_indexes;
for (unsigned i = 0; i < num_rels1; ++i) {
if(is_tableish_relation(*r1[i])) {
if (is_tableish_relation(*r1[i])) {
r1_tables_indexes.push_back(i);
continue;
}
@ -291,7 +291,7 @@ namespace datalog {
if (!found) {
relation_plugin & r1_plugin = get_nonsieve_plugin(*r1[i]);
relation_base* rel2;
if(r1_plugin.can_handle_signature(r2_sig)) {
if (r1_plugin.can_handle_signature(r2_sig)) {
rel2 = r1_plugin.mk_full(p, r2_sig, r1_kind);
}
else {
@ -307,7 +307,7 @@ namespace datalog {
}
}
for (unsigned i = 0; i < num_rels2; ++i) {
if(is_tableish_relation(*r2[i])) {
if (is_tableish_relation(*r2[i])) {
r2_tables_indexes.push_back(i);
continue;
}
@ -315,7 +315,7 @@ namespace datalog {
relation_plugin & r2_plugin = get_nonsieve_plugin(*r2[i]);
family_id r2_kind = get_nonsieve_kind(*r2[i]);
relation_base* rel1;
if(r2_plugin.can_handle_signature(r1_sig)) {
if (r2_plugin.can_handle_signature(r1_sig)) {
rel1 = r2_plugin.mk_full(p, r1_sig, r2_kind);
}
else {
@ -331,7 +331,7 @@ namespace datalog {
}
}
if(!r1_tables_indexes.empty() && !r2_tables_indexes.empty()) {
if (!r1_tables_indexes.empty() && !r2_tables_indexes.empty()) {
//We may perhaps want to group the table relations by kinds so that tables of the same kind
//get joined...

46
src/muz_qe/dl_relation_manager.cpp
View file

@ -720,6 +720,13 @@ namespace datalog {
return t.get_plugin().mk_filter_interpreted_fn(t, condition);
}
relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t,
app * condition,
unsigned removed_col_cnt,
const unsigned * removed_cols) {
return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols);
}
class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn {
scoped_ptr<relation_mutator_fn> m_filter;
@ -1387,6 +1394,45 @@ namespace datalog {
}
class relation_manager::default_table_filter_interpreted_and_project_fn
: public table_transformer_fn {
scoped_ptr<table_mutator_fn> m_filter;
scoped_ptr<table_transformer_fn> m_project;
app_ref m_condition;
unsigned_vector m_removed_cols;
public:
default_table_filter_interpreted_and_project_fn(context & ctx, table_mutator_fn * filter,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols)
: m_filter(filter), m_condition(condition, ctx.get_manager()),
m_removed_cols(removed_col_cnt, removed_cols) {}
virtual table_base* operator()(const table_base & tb) {
table_base *t2 = tb.clone();
(*m_filter)(*t2);
if (!m_project) {
relation_manager & rmgr = t2->get_plugin().get_manager();
m_project = rmgr.mk_project_fn(*t2, m_removed_cols.size(), m_removed_cols.c_ptr());
if (!m_project) {
throw default_exception("projection does not exist");
}
}
return (*m_project)(*t2);
}
};
table_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const table_base & t,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) {
table_transformer_fn * res = t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols);
if (res)
return res;
table_mutator_fn * filter = mk_filter_interpreted_fn(t, condition);
SASSERT(filter);
res = alloc(default_table_filter_interpreted_and_project_fn, get_context(), filter, condition, removed_col_cnt, removed_cols);
return res;
}
table_intersection_filter_fn * relation_manager::mk_filter_by_intersection_fn(const table_base & t,
const table_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols) {
table_intersection_filter_fn * res = t.get_plugin().mk_filter_by_negation_fn(t, src, joined_col_cnt,

7
src/muz_qe/dl_relation_manager.h
View file

@ -55,6 +55,7 @@ namespace datalog {
class default_table_filter_equal_fn;
class default_table_filter_identical_fn;
class default_table_filter_interpreted_fn;
class default_table_filter_interpreted_and_project_fn;
class default_table_negation_filter_fn;
class default_table_filter_not_equal_fn;
class default_table_select_equal_and_project_fn;
@ -350,6 +351,9 @@ namespace datalog {
relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, app * condition,
unsigned removed_col_cnt, const unsigned * removed_cols);
/**
\brief Operations that returns all rows of \c t for which is column \c col equal to \c value
with the column \c col removed.
@ -522,6 +526,9 @@ namespace datalog {
table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition);
table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition,
unsigned removed_col_cnt, const unsigned * removed_cols);
/**
\brief Operations that returns all rows of \c t for which is column \c col equal to \c value
with the column \c col removed.

5
src/muz_qe/dl_sieve_relation.cpp
View file

@ -158,7 +158,7 @@ namespace datalog {
inner_sig_singleton.push_back(s[i]);
inner_columns[i] = inner.can_handle_signature(inner_sig_singleton);
}
#if Z3DEBUG
#if Z3DEBUG
//we assume that if a relation plugin can handle two sets of columns separetely,
//it can also handle them in one relation
relation_signature inner_sig;
@ -246,7 +246,8 @@ namespace datalog {
relation_base * sieve_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {
relation_signature empty_sig;
relation_base * inner = get_manager().mk_full_relation(empty_sig, p, null_family_id);
relation_plugin& plugin = get_manager().get_appropriate_plugin(s);
relation_base * inner = plugin.mk_full(p, empty_sig, null_family_id);
svector<bool> inner_cols;
inner_cols.resize(s.size(), false);
return mk_from_inner(s, inner_cols, inner);

15
src/muz_qe/dl_table_relation.cpp
View file

@ -354,6 +354,21 @@ namespace datalog {
return alloc(tr_mutator_fn, tfun);
}
relation_transformer_fn * table_relation_plugin::mk_filter_interpreted_and_project_fn(const relation_base & t,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) {
if (!t.from_table())
return 0;
const table_relation & tr = static_cast<const table_relation &>(t);
table_transformer_fn * tfun = get_manager().mk_filter_interpreted_and_project_fn(tr.get_table(),
condition, removed_col_cnt, removed_cols);
SASSERT(tfun);
relation_signature sig;
relation_signature::from_project(t.get_signature(), removed_col_cnt, removed_cols, sig);
return alloc(tr_transformer_fn, sig, tfun);
}
class table_relation_plugin::tr_intersection_filter_fn : public relation_intersection_filter_fn {
scoped_ptr<table_intersection_filter_fn> m_tfun;
public:

2
src/muz_qe/dl_table_relation.h
View file

@ -71,6 +71,8 @@ namespace datalog {
virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value,
unsigned col);
virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t,
app * condition, unsigned removed_col_cnt, const unsigned * removed_cols);
virtual relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t,
const relation_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols);
virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t,

1
src/muz_qe/fixedpoint_params.pyg
View file

@ -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'),
))

25
src/muz_qe/horn_tactic.cpp
View file

@ -124,6 +124,15 @@ class horn_tactic : public tactic {
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
bool is_implication(expr* f) {
expr* e1;
while (is_forall(f)) {
f = to_quantifier(f)->get_expr();
}
while (m.is_implies(f, e1, f)) ;
return is_predicate(f);
}
formula_kind get_formula_kind(expr_ref& f) {
expr_ref tmp(f);
normalize(tmp);
@ -149,7 +158,10 @@ class horn_tactic : public tactic {
}
}
if (head) {
// f = m.mk_implies(f, head);
if (!is_implication(f)) {
f = m.mk_and(body.size(), body.c_ptr());
f = m.mk_implies(f, head);
}
return IS_RULE;
}
else {
@ -200,6 +212,7 @@ class horn_tactic : public tactic {
break;
default:
msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
TRACE("horn", tout << msg.str(););
throw tactic_exception(msg.str().c_str());
}
}
@ -230,7 +243,15 @@ class horn_tactic : public tactic {
model_converter_ref & mc,
proof_converter_ref & pc) {
lbool is_reachable = m_ctx.query(q);
lbool is_reachable = l_undef;
try {
is_reachable = m_ctx.query(q);
}
catch (default_exception& ex) {
IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
throw ex;
}
g->inc_depth();
bool produce_models = g->models_enabled();

6
src/muz_qe/pdr_dl_interface.cpp
View file

@ -133,6 +133,12 @@ lbool dl_interface::query(expr * query) {
--num_unfolds;
}
}
if (m_ctx.get_rules().get_output_predicates().empty()) {
m_context->set_unsat();
return l_false;
}
query_pred = m_ctx.get_rules().get_output_predicate();
IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););

20
src/muz_qe/rel_context.cpp
View file

@ -18,6 +18,9 @@ Revision History:
Extracted from dl_context
--*/
#define Z3_HASSEL_TABLE
#include"rel_context.h"
#include"dl_context.h"
#include"dl_compiler.h"
@ -30,8 +33,13 @@ Revision History:
#include"dl_mk_karr_invariants.h"
#include"dl_finite_product_relation.h"
#include"dl_sparse_table.h"
#ifdef Z3_HASSEL_TABLE
# include"dl_hassel_table.h"
# include"dl_hassel_diff_table.h"
#endif
#include"dl_table.h"
#include"dl_table_relation.h"
#include"aig_exporter.h"
namespace datalog {
@ -86,6 +94,10 @@ namespace datalog {
get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
#ifdef Z3_HASSEL_TABLE
get_rmanager().register_plugin(alloc(hassel_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(hassel_diff_table_plugin, get_rmanager()));
#endif
// register plugins for builtin relations
@ -127,6 +139,14 @@ 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);
std::ofstream strm(filename, std::ios_base::binary);
aig(strm);
exit(0);
}
compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
TRACE("dl", m_code.display(*this, tout); );

3
src/muz_qe/rel_context.h
View file

@ -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;

81
src/smt/diff_logic.h
View file

@ -24,6 +24,7 @@ Revision History:
#include"statistics.h"
#include"trace.h"
#include"warning.h"
#include"uint_set.h"
typedef int dl_var;
@ -306,14 +307,6 @@ private:
return true;
}
// Update the assignment of variable v, that is,
// m_assignment[v] += inc
// This method also stores the old value of v in the assignment stack.
void acc_assignment(dl_var v, const numeral & inc) {
TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
m_assignment_stack.push_back(assignment_trail(v, m_assignment[v]));
m_assignment[v] += inc;
}
// Restore the assignment using the information in m_assignment_stack.
// This method is called when make_feasible fails.
@ -827,6 +820,16 @@ public:
}
}
// Update the assignment of variable v, that is,
// m_assignment[v] += inc
// This method also stores the old value of v in the assignment stack.
void acc_assignment(dl_var v, const numeral & inc) {
TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
m_assignment_stack.push_back(assignment_trail(v, m_assignment[v]));
m_assignment[v] += inc;
}
struct every_var_proc {
bool operator()(dl_var v) const {
return true;
@ -837,6 +840,36 @@ public:
display_core(out, every_var_proc());
}
void display_agl(std::ostream & out) const {
uint_set vars;
typename edges::const_iterator it = m_edges.begin();
typename edges::const_iterator end = m_edges.end();
for (; it != end; ++it) {
edge const& e = *it;
if (e.is_enabled()) {
vars.insert(e.get_source());
vars.insert(e.get_target());
}
}
out << "digraph "" {\n";
unsigned n = m_assignment.size();
for (unsigned v = 0; v < n; v++) {
if (vars.contains(v)) {
out << "\"" << v << "\" [label=\"" << v << ":" << m_assignment[v] << "\"]\n";
}
}
it = m_edges.begin();
for (; it != end; ++it) {
edge const& e = *it;
if (e.is_enabled()) {
out << "\"" << e.get_source() << "\"->\"" << e.get_target() << "\"[label=\"" << e.get_weight() << "\"]\n";
}
}
out << "}\n";
}
template<typename FilterAssignmentProc>
void display_core(std::ostream & out, FilterAssignmentProc p) const {
display_edges(out);
@ -1000,6 +1033,38 @@ public:
}
}
void compute_zero_succ(dl_var v, int_vector& succ) {
unsigned n = m_assignment.size();
m_dfs_time.reset();
m_dfs_time.resize(n, -1);
m_dfs_time[v] = 0;
succ.push_back(v);
numeral gamma;
for (unsigned i = 0; i < succ.size(); ++i) {
v = succ[i];
edge_id_vector & edges = m_out_edges[v];
typename edge_id_vector::iterator it = edges.begin();
typename edge_id_vector::iterator end = edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
edge & e = m_edges[e_id];
if (!e.is_enabled()) {
continue;
}
SASSERT(e.get_source() == v);
set_gamma(e, gamma);
if (gamma.is_zero()) {
dl_var target = e.get_target();
if (m_dfs_time[target] == -1) {
succ.push_back(target);
m_dfs_time[target] = 0;
}
}
}
}
}
numeral get_assignment(dl_var v) const {
return m_assignment[v];
}

19
src/smt/theory_utvpi.h
View file

@ -65,7 +65,7 @@ namespace smt {
class parent_trail;
struct GExt : public Ext {
typedef literal explanation;
typedef std::pair<literal,unsigned> explanation;
};
class atom {
@ -113,15 +113,18 @@ namespace smt {
// a negative cycle.
class nc_functor {
literal_vector m_antecedents;
unsigned_vector m_coeffs;
theory_utvpi& m_super;
public:
nc_functor(theory_utvpi& s) : m_super(s) {}
void reset() { m_antecedents.reset(); }
void reset() { m_antecedents.reset(); m_coeffs.reset(); }
literal_vector const& get_lits() const { return m_antecedents; }
unsigned_vector const& get_coeffs() const { return m_coeffs; }
void operator()(literal const & ex) {
if (ex != null_literal) {
m_antecedents.push_back(ex);
void operator()(std::pair<literal,unsigned> const & ex) {
if (ex.first != null_literal) {
m_antecedents.push_back(ex.first);
m_coeffs.push_back(ex.second);
}
}
@ -259,7 +262,11 @@ namespace smt {
private:
rational mk_value(theory_var v);
rational mk_value(theory_var v, bool is_int);
bool is_parity_ok(unsigned v) const;
void enforce_parity();
void validate_model();

180
src/smt/theory_utvpi_def.h
View file

@ -33,7 +33,17 @@ Revision History:
3. Solve for x^+ and x^-
4. Check parity condition for integers (see Lahiri and Musuvathi 05)
5. extract model for M(x) := (M(x^+)- M(x^-))/2
This checks if x^+ and x^- are in the same component but of different
parities.
5. Enforce parity on variables. This checks if x^+ and x^- have different
parities. If they have different parities, the assignment to one
of the variables is decremented (choose the variable that is not tightly
constrained with 0).
The process that adjusts parities converges: Suppose we break a parity
of a different variable y while fixing x's parity. A cyclic breaking/fixing
of parities implies there is a strongly connected component between x, y
and the two polarities of the variables. This contradicts the test in 4.
6. extract model for M(x) := (M(x^+)- M(x^-))/2
--*/
@ -197,6 +207,15 @@ namespace smt {
inc_conflicts();
literal_vector const& lits = m_nc_functor.get_lits();
context & ctx = get_context();
IF_VERBOSE(2,
verbose_stream() << "conflict:\n";
for (unsigned i = 0; i < lits.size(); ++i) {
ast_manager& m = get_manager();
expr_ref e(m);
ctx.literal2expr(lits[i], e);
verbose_stream() << mk_pp(e, m) << "\n";
}
verbose_stream() << "\n";);
TRACE("utvpi",
tout << "conflict: ";
for (unsigned i = 0; i < lits.size(); ++i) {
@ -213,7 +232,9 @@ namespace smt {
vector<parameter> params;
if (get_manager().proofs_enabled()) {
params.push_back(parameter(symbol("farkas")));
params.resize(lits.size()+1, parameter(rational(1)));
for (unsigned i = 0; i < m_nc_functor.get_coeffs().size(); ++i) {
params.push_back(parameter(rational(m_nc_functor.get_coeffs()[i])));
}
}
ctx.set_conflict(
@ -386,7 +407,6 @@ namespace smt {
template<typename Ext>
final_check_status theory_utvpi<Ext>::final_check_eh() {
SASSERT(is_consistent());
TRACE("utvpi", display(tout););
if (can_propagate()) {
propagate();
return FC_CONTINUE;
@ -413,7 +433,7 @@ namespace smt {
unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) {
enode* e = get_enode(i);
if (a.is_int(e->get_owner())) {
if (!a.is_int(e->get_owner())) {
continue;
}
th_var v1 = to_var(i);
@ -500,7 +520,7 @@ namespace smt {
template<typename Ext>
theory_var theory_utvpi<Ext>::mk_term(app* n) {
TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";);
TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";);
context& ctx = get_context();
bool cl = m_test.linearize(n);
@ -508,7 +528,7 @@ namespace smt {
found_non_utvpi_expr(n);
return null_theory_var;
}
coeffs coeffs;
rational w;
mk_coeffs(m_test.get_linearization(), coeffs, w);
@ -620,28 +640,28 @@ namespace smt {
edge_id id = m_graph.get_num_edges();
th_var w1 = to_var(v1), w2 = to_var(v2);
if (terms.size() == 1 && pos1) {
m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l);
m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l);
m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2));
m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2));
}
else if (terms.size() == 1 && !pos1) {
m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l);
m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l);
m_graph.add_edge(pos(w1), neg(w1), -weight-weight, std::make_pair(l,2));
m_graph.add_edge(pos(w1), neg(w1), -weight-weight, std::make_pair(l,2));
}
else if (pos1 && pos2) {
m_graph.add_edge(neg(w2), pos(w1), -weight, l);
m_graph.add_edge(neg(w1), pos(w2), -weight, l);
m_graph.add_edge(neg(w2), pos(w1), -weight, std::make_pair(l,1));
m_graph.add_edge(neg(w1), pos(w2), -weight, std::make_pair(l,1));
}
else if (pos1 && !pos2) {
m_graph.add_edge(pos(w2), pos(w1), -weight, l);
m_graph.add_edge(neg(w1), neg(w2), -weight, l);
m_graph.add_edge(pos(w2), pos(w1), -weight, std::make_pair(l,1));
m_graph.add_edge(neg(w1), neg(w2), -weight, std::make_pair(l,1));
}
else if (!pos1 && pos2) {
m_graph.add_edge(neg(w2), neg(w1), -weight, l);
m_graph.add_edge(pos(w1), pos(w2), -weight, l);
m_graph.add_edge(neg(w2), neg(w1), -weight, std::make_pair(l,1));
m_graph.add_edge(pos(w1), pos(w2), -weight, std::make_pair(l,1));
}
else {
m_graph.add_edge(pos(w1), neg(w2), -weight, l);
m_graph.add_edge(pos(w2), neg(w1), -weight, l);
m_graph.add_edge(pos(w1), neg(w2), -weight, std::make_pair(l,1));
m_graph.add_edge(pos(w2), neg(w1), -weight, std::make_pair(l,1));
}
return id;
}
@ -656,12 +676,98 @@ namespace smt {
return m_graph.is_feasible();
}
template<typename Ext>
bool theory_utvpi<Ext>::is_parity_ok(unsigned i) const {
th_var v1 = to_var(i);
th_var v2 = neg(v1);
rational r1 = m_graph.get_assignment(v1).get_rational();
rational r2 = m_graph.get_assignment(v2).get_rational();
return r1.is_even() == r2.is_even();
}
/**
\brief adjust values for variables in the difference graph
such that for variables of integer sort it is
the case that x^+ - x^- is even.
The informal justification for the procedure enforce_parity is that
the graph does not contain a strongly connected component where
x^+ and x+- are connected. They can be independently changed.
Since we would like variables representing 0 (zero) map to 0,
we selectively update the subgraph that can be updated without
changing the value of zero (which should be 0).
*/
template<typename Ext>
void theory_utvpi<Ext>::enforce_parity() {
unsigned_vector todo;
unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) {
enode* e = get_enode(i);
if (a.is_int(e->get_owner()) && !is_parity_ok(i)) {
todo.push_back(i);
}
}
if (todo.empty()) {
return;
}
while (!todo.empty()) {
unsigned i = todo.back();
todo.pop_back();
if (is_parity_ok(i)) {
continue;
}
th_var v1 = to_var(i);
th_var v2 = neg(v1);
TRACE("utvpi", tout << "disparity: " << v1 << "\n";);
int_vector zero_v;
m_graph.compute_zero_succ(v1, zero_v);
bool found0 = false;
for (unsigned j = 0; !found0 && j < zero_v.size(); ++j) {
found0 =
(to_var(m_zero_int) == zero_v[j]) ||
(neg(to_var(m_zero_int)) == zero_v[j]);
}
// variables that are tightly connected
// to 0 should not have their values changed.
if (found0) {
zero_v.reset();
m_graph.compute_zero_succ(v2, zero_v);
}
TRACE("utvpi",
for (unsigned j = 0; j < zero_v.size(); ++j) {
tout << "decrement: " << zero_v[j] << "\n";
});
for (unsigned j = 0; j < zero_v.size(); ++j) {
int v = zero_v[j];
m_graph.acc_assignment(v, numeral(-1));
th_var k = from_var(v);
if (!is_parity_ok(k)) {
TRACE("utvpi", tout << "new disparity: " << k << "\n";);
todo.push_back(k);
}
}
}
SASSERT(m_graph.is_feasible());
DEBUG_CODE(
for (unsigned i = 0; i < sz; ++i) {
enode* e = get_enode(i);
if (a.is_int(e->get_owner()) && !is_parity_ok(i)) {
IF_VERBOSE(0, verbose_stream() << "disparities not fixed\n";);
UNREACHABLE();
}
});
}
// models:
template<typename Ext>
void theory_utvpi<Ext>::init_model(model_generator & m) {
m_factory = alloc(arith_factory, get_manager());
m.register_factory(m_factory);
// TBD: enforce strong or tight coherence?
enforce_parity();
compute_delta();
DEBUG_CODE(validate_model(););
}
@ -677,7 +783,8 @@ namespace smt {
}
bool ok = true;
expr* e = ctx.bool_var2expr(b);
switch(ctx.get_assignment(b)) {
lbool assign = ctx.get_assignment(b);
switch(assign) {
case l_true:
ok = eval(e);
break;
@ -687,7 +794,23 @@ namespace smt {
default:
break;
}
CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";);
CTRACE("utvpi", !ok,
tout << "validation failed:\n";
tout << "Assignment: " << assign << "\n";
m_atoms[i].display(*this, tout);
tout << "\n";
display(tout);
m_graph.display_agl(tout);
);
if (!ok) {
std::cout << "validation failed:\n";
std::cout << "Assignment: " << assign << "\n";
m_atoms[i].display(*this, std::cout);
std::cout << "\n";
display(std::cout);
m_graph.display_agl(std::cout);
}
// CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";);
SASSERT(ok);
}
@ -740,7 +863,7 @@ namespace smt {
return eval_num(e1);
}
if (is_uninterp_const(e)) {
return mk_value(mk_var(e));
return mk_value(mk_var(e), a.is_int(e));
}
TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";);
UNREACHABLE();
@ -749,23 +872,28 @@ namespace smt {
template<typename Ext>
rational theory_utvpi<Ext>::mk_value(th_var v) {
rational theory_utvpi<Ext>::mk_value(th_var v, bool is_int) {
SASSERT(v != null_theory_var);
numeral val1 = m_graph.get_assignment(to_var(v));
numeral val2 = m_graph.get_assignment(neg(to_var(v)));
numeral val = val1 - val2;
rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational());
num = num/rational(2);
num = floor(num);
SASSERT(!is_int || num.is_int());
TRACE("utvpi",
expr* n = get_enode(v)->get_owner();
tout << mk_pp(n, get_manager()) << " |-> (" << val1 << " - " << val2 << ")/2 = " << num << "\n";);
return num;
}
template<typename Ext>
model_value_proc * theory_utvpi<Ext>::mk_value(enode * n, model_generator & mg) {
theory_var v = n->get_th_var(get_id());
rational num = mk_value(v);
bool is_int = a.is_int(n->get_owner());
rational num = mk_value(v, is_int);
TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner())));
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int));
}
/**

6
src/tactic/aig/aig.cpp
View file

@ -869,11 +869,7 @@ struct aig_manager::imp {
void mk_ite(aig * n) {
aig_lit c, t, e;
#ifdef Z3DEBUG
bool ok =
#endif
m.is_ite(n, c, t, e);
SASSERT(ok);
VERIFY(m.is_ite(n, c, t, e));
if (c.is_inverted()) {
c.invert();
std::swap(t, e);

1
src/tactic/aig/aig.h
View file

@ -70,7 +70,6 @@ public:
void max_sharing(aig_ref & r);
void to_formula(aig_ref const & r, expr_ref & result);
void to_formula(aig_ref const & r, goal & result);
void to_cnf(aig_ref const & r, goal & result);
void display(std::ostream & out, aig_ref const & r) const;
void display_smt2(std::ostream & out, aig_ref const & r) const;
unsigned get_num_aigs() const;

45
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -30,7 +30,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
expr_ref_vector m_out;
fpa2bv_converter & m_conv;
sort_ref_vector m_bindings;
expr_ref_vector m_mappings;
expr_ref_vector m_mappings;
unsigned long long m_max_memory;
unsigned m_max_steps;
@ -166,9 +167,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
bool pre_visit(expr * t)
{
TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
TRACE("fpa2bv", tout << "pre_visit [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
sort_ref_vector new_bindings(m_manager);
for (unsigned i = 0 ; i < q->get_num_decls(); i++)
new_bindings.push_back(q->get_decl_sort(i));
@ -199,17 +202,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
name_buffer.reset();
name_buffer << n << ".exp";
name_buffer << n << ".bv";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(ebits));
name_buffer.reset();
name_buffer << n << ".sig";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits-1));
name_buffer.reset();
name_buffer << n << ".sgn";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(1));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
}
else {
new_decl_sorts.push_back(s);
@ -231,20 +226,26 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
return false;
unsigned inx = m_bindings.size() - t->get_idx() - 1;
if (m_mappings[inx] == 0)
expr_ref new_exp(m());
sort * s = t->get_sort();
if (m_conv.is_float(s))
{
unsigned shift = 0;
for (unsigned i = m_bindings.size() - 1; i > inx; i--)
if (m_conv.is_float(m_bindings[i].get())) shift += 2;
expr_ref new_var(m());
if (m_conv.is_float(t->get_sort()))
m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var);
else
new_var = m().mk_var(t->get_idx() + shift, t->get_sort());
m_mappings[inx] = new_var;
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
m_conv.mk_triple(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
m_conv.bu().mk_extract(ebits-1, 0, new_var),
new_exp);
}
else
new_exp = m().mk_var(t->get_idx(), s);
m_mappings[inx] = new_exp;
result = m_mappings[inx].get();
result_pr = 0;
TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);

7
src/util/bit_vector.h
View file

@ -28,6 +28,7 @@ COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
#define BV_DEFAULT_CAPACITY 2
class bit_vector {
protected:
unsigned m_num_bits;
unsigned m_capacity; //!< in words
unsigned * m_data;
@ -64,6 +65,12 @@ public:
m_data(0) {
}
bit_vector(unsigned reserve_num_bits) :
m_num_bits(0),
m_capacity(num_words(reserve_num_bits)),
m_data(alloc_svect(unsigned, m_capacity)) {
}
bit_vector(bit_vector const & source):
m_num_bits(source.m_num_bits),
m_capacity(source.m_capacity),