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:
Christoph M. Wintersteiger 2013-05-01 14:11:21 +01:00
commit 7053b7636b
90 changed files with 4876 additions and 907 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_ast.cpp
View file

@ -46,7 +46,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_int_symbol(c, i);
RESET_ERROR_CODE();
if (i < 0 || (unsigned)i >= (SIZE_MAX >> PTR_ALIGNMENT)) {
if (i < 0 || (size_t)i >= (SIZE_MAX >> PTR_ALIGNMENT)) {
SET_ERROR_CODE(Z3_IOB);
return 0;
}

2
src/ast/arith_decl_plugin.h
View file

@ -268,6 +268,8 @@ public:
bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); }
MATCH_UNARY(is_uminus);
MATCH_UNARY(is_to_real);
MATCH_UNARY(is_to_int);
MATCH_BINARY(is_sub);
MATCH_BINARY(is_add);
MATCH_BINARY(is_mul);

5
src/ast/ast_smt_pp.cpp
View file

@ -260,6 +260,7 @@ class smt_printer {
else {
m_out << sym << "[";
}
for (unsigned i = 0; i < num_params; ++i) {
parameter const& p = params[i];
if (p.is_ast()) {
@ -642,9 +643,7 @@ class smt_printer {
m_out << m_var_names[m_num_var_names - idx - 1];
}
else {
if (!m_is_smt2) {
m_out << "?" << idx;
}
m_out << "?" << idx;
}
}

59
src/ast/expr_abstract.cpp
View file

@ -20,52 +20,50 @@ Notes:
#include "expr_abstract.h"
#include "map.h"
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
ast_ref_vector pinned(m);
ptr_vector<expr> stack;
obj_map<expr, expr*> map;
void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
expr * curr = 0, *b = 0;
SASSERT(n->get_ref_count() > 0);
stack.push_back(n);
m_stack.push_back(n);
for (unsigned i = 0; i < num_bound; ++i) {
b = bound[i];
expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b));
pinned.push_back(v);
map.insert(b, v);
m_pinned.push_back(v);
m_map.insert(b, v);
}
while(!stack.empty()) {
curr = stack.back();
if (map.contains(curr)) {
stack.pop_back();
while(!m_stack.empty()) {
curr = m_stack.back();
if (m_map.contains(curr)) {
m_stack.pop_back();
continue;
}
switch(curr->get_kind()) {
case AST_VAR: {
map.insert(curr, curr);
stack.pop_back();
m_map.insert(curr, curr);
m_stack.pop_back();
break;
}
case AST_APP: {
app* a = to_app(curr);
bool all_visited = true;
ptr_vector<expr> args;
m_args.reset();
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (!map.find(a->get_arg(i), b)) {
stack.push_back(a->get_arg(i));
if (!m_map.find(a->get_arg(i), b)) {
m_stack.push_back(a->get_arg(i));
all_visited = false;
}
else {
args.push_back(b);
m_args.push_back(b);
}
}
if (all_visited) {
b = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
pinned.push_back(b);
map.insert(curr, b);
stack.pop_back();
b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
m_pinned.push_back(b);
m_map.insert(curr, b);
m_stack.pop_back();
}
break;
}
@ -81,17 +79,24 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons
}
expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1);
b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get());
pinned.push_back(b);
map.insert(curr, b);
stack.pop_back();
m_pinned.push_back(b);
m_map.insert(curr, b);
m_stack.pop_back();
break;
}
default:
UNREACHABLE();
}
}
if (!map.find(n, b)) {
UNREACHABLE();
}
VERIFY (m_map.find(n, b));
result = b;
m_pinned.reset();
m_map.reset();
m_stack.reset();
m_args.reset();
}
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
expr_abstractor abs(m);
abs(base, num_bound, bound, n, result);
}

11
src/ast/expr_abstract.h
View file

@ -21,6 +21,17 @@ Notes:
#include"ast.h"
class expr_abstractor {
ast_manager& m;
expr_ref_vector m_pinned;
ptr_vector<expr> m_stack, m_args;
obj_map<expr, expr*> m_map;
public:
expr_abstractor(ast_manager& m): m(m), m_pinned(m) {}
void operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
};
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
#endif

22
src/ast/rewriter/ast_counter.cpp
View file

@ -93,7 +93,9 @@ void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; i++) {
m_sorts.reset();
::get_free_vars(pred->get_arg(i), m_sorts);
m_todo.reset();
m_mark.reset();
::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts);
for (unsigned j = 0; j < m_sorts.size(); ++j) {
if (m_sorts[j]) {
update(j, coef);
@ -108,24 +110,27 @@ unsigned var_counter::get_max_var(bool& has_var) {
unsigned max_var = 0;
while (!m_todo.empty()) {
expr* e = m_todo.back();
unsigned scope = m_scopes.back();
m_todo.pop_back();
m_scopes.pop_back();
if (m_visited.is_marked(e)) {
continue;
}
m_visited.mark(e, true);
switch(e->get_kind()) {
case AST_QUANTIFIER: {
var_counter aux_counter;
quantifier* q = to_quantifier(e);
m_todo.push_back(q->get_expr());
m_scopes.push_back(scope + q->get_num_decls());
bool has_var1 = false;
unsigned max_v = aux_counter.get_max_var(has_var1);
if (max_v > max_var + q->get_num_decls()) {
max_var = max_v - q->get_num_decls();
has_var = true;
}
break;
}
case AST_VAR: {
if (to_var(e)->get_idx() >= scope + max_var) {
if (to_var(e)->get_idx() >= max_var) {
has_var = true;
max_var = to_var(e)->get_idx() - scope;
max_var = to_var(e)->get_idx();
}
break;
}
@ -133,7 +138,6 @@ unsigned var_counter::get_max_var(bool& has_var) {
app* a = to_app(e);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
m_todo.push_back(a->get_arg(i));
m_scopes.push_back(scope);
}
break;
}
@ -150,14 +154,12 @@ unsigned var_counter::get_max_var(bool& has_var) {
unsigned var_counter::get_max_var(expr* e) {
bool has_var = false;
m_todo.push_back(e);
m_scopes.push_back(0);
return get_max_var(has_var);
}
unsigned var_counter::get_next_var(expr* e) {
bool has_var = false;
m_todo.push_back(e);
m_scopes.push_back(0);
unsigned mv = get_max_var(has_var);
if (has_var) mv++;
return mv;

2
src/ast/rewriter/ast_counter.h
View file

@ -38,6 +38,7 @@ public:
counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
void reset() { m_data.reset(); }
iterator begin() const { return m_data.begin(); }
iterator end() const { return m_data.end(); }
void update(unsigned el, int delta);
@ -71,6 +72,7 @@ protected:
ptr_vector<sort> m_sorts;
expr_fast_mark1 m_visited;
ptr_vector<expr> m_todo;
ast_mark m_mark;
unsigned_vector m_scopes;
unsigned get_max_var(bool & has_var);
public:

51
src/ast/rewriter/var_subst.cpp
View file

@ -17,7 +17,6 @@ Notes:
--*/
#include"var_subst.h"
#include"used_vars.h"
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"ast_smt2_pp.h"
@ -40,7 +39,7 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp
tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
}
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
SASSERT(is_well_sorted(m, q));
if (is_ground(q->get_expr())) {
// ignore patterns if the body is a ground formula.
@ -51,17 +50,17 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
result = q;
return;
}
used_vars used;
used.process(q->get_expr());
m_used.reset();
m_used.process(q->get_expr());
unsigned num_patterns = q->get_num_patterns();
for (unsigned i = 0; i < num_patterns; i++)
used.process(q->get_pattern(i));
m_used.process(q->get_pattern(i));
unsigned num_no_patterns = q->get_num_no_patterns();
for (unsigned i = 0; i < num_no_patterns; i++)
used.process(q->get_no_pattern(i));
m_used.process(q->get_no_pattern(i));
unsigned num_decls = q->get_num_decls();
if (used.uses_all_vars(num_decls)) {
if (m_used.uses_all_vars(num_decls)) {
q->set_no_unused_vars();
result = q;
return;
@ -70,7 +69,7 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
ptr_buffer<sort> used_decl_sorts;
buffer<symbol> used_decl_names;
for (unsigned i = 0; i < num_decls; ++i) {
if (used.contains(num_decls - i - 1)) {
if (m_used.contains(num_decls - i - 1)) {
used_decl_sorts.push_back(q->get_decl_sort(i));
used_decl_names.push_back(q->get_decl_name(i));
}
@ -79,10 +78,10 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
unsigned num_removed = 0;
expr_ref_buffer var_mapping(m);
int next_idx = 0;
unsigned sz = used.get_max_found_var_idx_plus_1();
unsigned sz = m_used.get_max_found_var_idx_plus_1();
for (unsigned i = 0; i < num_decls; ++i) {
sort * s = used.contains(i);
sort * s = m_used.contains(i);
if (s) {
var_mapping.push_back(m.mk_var(next_idx, s));
next_idx++;
@ -95,7 +94,7 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
// (VAR 0) is in the first position of var_mapping.
for (unsigned i = num_decls; i < sz; i++) {
sort * s = used.contains(i);
sort * s = m_used.contains(i);
if (s)
var_mapping.push_back(m.mk_var(i - num_removed, s));
else
@ -110,9 +109,8 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
std::reverse(var_mapping.c_ptr(), var_mapping.c_ptr() + var_mapping.size());
expr_ref new_expr(m);
var_subst subst(m);
subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
m_subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
if (num_removed == num_decls) {
result = new_expr;
@ -124,11 +122,11 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
expr_ref_buffer new_no_patterns(m);
for (unsigned i = 0; i < num_patterns; i++) {
subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
new_patterns.push_back(tmp);
}
for (unsigned i = 0; i < num_no_patterns; i++) {
subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
new_no_patterns.push_back(tmp);
}
@ -145,7 +143,12 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
num_no_patterns,
new_no_patterns.c_ptr());
to_quantifier(result)->set_no_unused_vars();
SASSERT(is_well_sorted(m, result));
SASSERT(is_well_sorted(m, result));
}
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
unused_vars_eliminator el(m);
el(q, result);
}
void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref & result) {
@ -161,9 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
}
static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sorts) {
ast_mark mark;
ptr_vector<expr> todo;
static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
@ -175,7 +176,9 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sor
switch(e->get_kind()) {
case AST_QUANTIFIER: {
quantifier* q = to_quantifier(e);
get_free_vars_offset(q->get_expr(), offset+q->get_num_decls(), sorts);
ast_mark mark1;
ptr_vector<expr> todo1;
get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
break;
}
case AST_VAR: {
@ -207,5 +210,11 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sor
void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
get_free_vars_offset(e, 0, sorts);
ast_mark mark;
ptr_vector<expr> todo;
get_free_vars_offset(mark, todo, 0, e, sorts);
}
void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
get_free_vars_offset(mark, todo, 0, e, sorts);
}

12
src/ast/rewriter/var_subst.h
View file

@ -20,6 +20,7 @@ Notes:
#define _VAR_SUBST_H_
#include"rewriter.h"
#include"used_vars.h"
/**
\brief Alias for var_shifter class.
@ -53,6 +54,15 @@ public:
/**
\brief Eliminate the unused variables from \c q. Store the result in \c r.
*/
class unused_vars_eliminator {
ast_manager& m;
var_subst m_subst;
used_vars m_used;
public:
unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {}
void operator()(quantifier* q, expr_ref& r);
};
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r);
/**
@ -73,6 +83,8 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
*/
void get_free_vars(expr* e, ptr_vector<sort>& sorts);
void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts);
#endif

226
src/muz_qe/clp_context.cpp Normal file
View file

@ -0,0 +1,226 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
clp_context.cpp
Abstract:
Bounded CLP (symbolic simulation using Z3) context.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
--*/
#include "clp_context.h"
#include "dl_context.h"
#include "unifier.h"
#include "var_subst.h"
#include "substitution.h"
namespace datalog {
class clp::imp {
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
unsigned m_num_unfold;
unsigned m_num_no_unfold;
unsigned m_num_subsumed;
};
context& m_ctx;
ast_manager& m;
rule_manager& rm;
smt_params m_fparams;
smt::kernel m_solver;
var_subst m_var_subst;
expr_ref_vector m_ground;
app_ref_vector m_goals;
volatile bool m_cancel;
stats m_stats;
public:
imp(context& ctx):
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_solver(m, m_fparams), // TBD: can be replaced by efficient BV solver.
m_var_subst(m, false),
m_ground(m),
m_goals(m),
m_cancel(false)
{
// m_fparams.m_relevancy_lvl = 0;
m_fparams.m_mbqi = false;
m_fparams.m_soft_timeout = 1000;
}
~imp() {}
lbool query(expr* query) {
m_ctx.ensure_opened();
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();
ground(head);
m_goals.push_back(to_app(head));
return search(20, 0);
}
void cancel() {
m_cancel = true;
m_solver.cancel();
}
void cleanup() {
m_cancel = false;
m_goals.reset();
m_solver.reset_cancel();
}
void reset_statistics() {
m_stats.reset();
}
void collect_statistics(statistics& st) const {
//st.update("tab.num_unfold", m_stats.m_num_unfold);
//st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold);
//st.update("tab.num_subsumed", m_stats.m_num_subsumed);
}
void display_certificate(std::ostream& out) const {
expr_ref ans = get_answer();
out << mk_pp(ans, m) << "\n";
}
expr_ref get_answer() const {
return expr_ref(m.mk_true(), m);
}
private:
void reset_ground() {
m_ground.reset();
}
void ground(expr_ref& e) {
ptr_vector<sort> sorts;
get_free_vars(e, sorts);
if (m_ground.size() < sorts.size()) {
m_ground.resize(sorts.size());
}
for (unsigned i = 0; i < sorts.size(); ++i) {
if (sorts[i] && !m_ground[i].get()) {
m_ground[i] = m.mk_fresh_const("c",sorts[i]);
}
}
m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
}
lbool search(unsigned depth, unsigned index) {
if (index == m_goals.size()) {
return l_true;
}
if (depth == 0) {
return l_undef;
}
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());
lbool status = l_false;
for (unsigned i = 0; i < rules.size(); ++i) {
rule* r = rules[i];
m_solver.push();
reset_ground();
expr_ref tmp(m);
tmp = r->get_head();
IF_VERBOSE(2, verbose_stream() << index << " " << mk_pp(tmp, m) << "\n";);
ground(tmp);
for (unsigned j = 0; j < head->get_num_args(); ++j) {
expr_ref eq(m);
eq = m.mk_eq(head->get_arg(j), to_app(tmp)->get_arg(j));
m_solver.assert_expr(eq);
}
for (unsigned j = r->get_uninterpreted_tail_size(); j < r->get_tail_size(); ++j) {
tmp = r->get_tail(j);
ground(tmp);
m_solver.assert_expr(tmp);
}
lbool is_sat = m_solver.check();
switch (is_sat) {
case l_false:
break;
case l_true:
if (depth == 1 && (index+1 > m_goals.size() || r->get_uninterpreted_tail_size() > 0)) {
status = l_undef;
break;
}
for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) {
tmp = r->get_tail(j);
ground(tmp);
m_goals.push_back(to_app(tmp));
}
switch(search(depth-1, index+1)) {
case l_undef:
status = l_undef;
// fallthrough
case l_false:
m_goals.resize(num_goals);
break;
case l_true:
return l_true;
}
break;
case l_undef:
status = l_undef;
throw default_exception("undef");
}
m_solver.pop(1);
}
return status;
}
proof_ref get_proof() const {
return proof_ref(0, m);
}
};
clp::clp(context& ctx):
m_imp(alloc(imp, ctx)) {
}
clp::~clp() {
dealloc(m_imp);
}
lbool clp::query(expr* query) {
return m_imp->query(query);
}
void clp::cancel() {
m_imp->cancel();
}
void clp::cleanup() {
m_imp->cleanup();
}
void clp::reset_statistics() {
m_imp->reset_statistics();
}
void clp::collect_statistics(statistics& st) const {
m_imp->collect_statistics(st);
}
void clp::display_certificate(std::ostream& out) const {
m_imp->display_certificate(out);
}
expr_ref clp::get_answer() {
return m_imp->get_answer();
}
};

45
src/muz_qe/clp_context.h Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
clp_context.h
Abstract:
Bounded CLP (symbolic simulation using Z3) context.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
--*/
#ifndef _CLP_CONTEXT_H_
#define _CLP_CONTEXT_H_
#include "ast.h"
#include "lbool.h"
#include "statistics.h"
namespace datalog {
class context;
class clp {
class imp;
imp* m_imp;
public:
clp(context& ctx);
~clp();
lbool query(expr* query);
void cancel();
void cleanup();
void reset_statistics();
void collect_statistics(statistics& st) const;
void display_certificate(std::ostream& out) const;
expr_ref get_answer();
};
};
#endif

11
src/muz_qe/dl_base.h
View file

@ -656,6 +656,7 @@ namespace datalog {
typedef sort * relation_sort;
typedef ptr_vector<sort> relation_signature_base0;
typedef ptr_hash<sort> relation_sort_hash;
typedef app * relation_element;
typedef app_ref relation_element_ref;
@ -739,8 +740,8 @@ namespace datalog {
struct hash {
unsigned operator()(relation_signature const& s) const {
relation_sort const* sorts = s.c_ptr();
return string_hash(reinterpret_cast<char const*>(sorts), sizeof(*sorts)*s.size(), 12); }
return obj_vector_hash<relation_signature>(s);
}
};
struct eq {
@ -816,9 +817,11 @@ namespace datalog {
typedef uint64 table_sort;
typedef svector<table_sort> table_signature_base0;
typedef uint64_hash table_sort_hash;
typedef uint64 table_element;
typedef svector<table_element> table_fact;
typedef uint64_hash table_element_hash;
struct table_traits {
typedef table_plugin plugin;
@ -881,8 +884,8 @@ namespace datalog {
public:
struct hash {
unsigned operator()(table_signature const& s) const {
table_sort const* sorts = s.c_ptr();
return string_hash(reinterpret_cast<char const*>(sorts), sizeof(*sorts)*s.size(), 12); }
return svector_hash<table_sort_hash>()(s);
}
};
struct eq {

1
src/muz_qe/dl_bmc_engine.cpp
View file

@ -1004,7 +1004,6 @@ namespace datalog {
symbol is_name(_name.str().c_str());
std::stringstream _name2;
_name2 << "get_succ#" << i;
symbol acc_name(_name2.str().c_str());
ptr_vector<accessor_decl> accs;
type_ref tr(0);
accs.push_back(mk_accessor_decl(name, tr));

9
src/muz_qe/dl_check_table.h
View file

@ -89,15 +89,6 @@ namespace datalog {
class check_table : public table_base {
friend class check_table_plugin;
friend class check_table_plugin::join_fn;
friend class check_table_plugin::union_fn;
friend class check_table_plugin::transformer_fn;
friend class check_table_plugin::rename_fn;
friend class check_table_plugin::project_fn;
friend class check_table_plugin::filter_equal_fn;
friend class check_table_plugin::filter_identical_fn;
friend class check_table_plugin::filter_interpreted_fn;
friend class check_table_plugin::filter_by_negation_fn;
table_base* m_checker;
table_base* m_tocheck;

113
src/muz_qe/dl_compiler.cpp
View file

@ -36,7 +36,7 @@ namespace datalog {
}
void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
pred2idx::entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
if(e->get_data().m_value!=UINT_MAX) {
//predicate is already loaded
return;
@ -421,6 +421,7 @@ namespace datalog {
void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs,
reg_idx delta_reg, bool use_widening, instruction_block & acc) {
ast_manager & m = m_context.get_manager();
m_instruction_observer.start_rule(r);
const app * h = r->get_head();
@ -433,7 +434,7 @@ namespace datalog {
SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin
reg_idx single_res;
ptr_vector<expr> single_res_expr;
expr_ref_vector single_res_expr(m);
//used to save on filter_identical instructions where the check is already done
//by the join operation
@ -536,7 +537,7 @@ namespace datalog {
unsigned srlen=single_res_expr.size();
SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size()));
for(unsigned i=0; i<srlen; i++) {
expr * exp = single_res_expr[i];
expr * exp = single_res_expr[i].get();
if(is_app(exp)) {
SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
relation_element value = to_app(exp);
@ -618,14 +619,13 @@ namespace datalog {
dealloc = true;
}
//enforce interpreted tail predicates
// enforce interpreted tail predicates
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);
var_idx_set t_vars;
ast_manager & m = m_context.get_manager();
collect_vars(m, t, t_vars);
ptr_vector<sort> t_vars;
::get_free_vars(t, t_vars);
if(t_vars.empty()) {
expr_ref simplified(m);
m_context.get_rewriter()(t, simplified);
@ -639,40 +639,23 @@ namespace datalog {
}
//determine binding size
unsigned max_var=0;
var_idx_set::iterator vit = t_vars.begin();
var_idx_set::iterator vend = t_vars.end();
for(; vit!=vend; ++vit) {
unsigned v = *vit;
if(v>max_var) { max_var = v; }
while (!t_vars.back()) {
t_vars.pop_back();
}
unsigned max_var = t_vars.size();
//create binding
expr_ref_vector binding(m);
binding.resize(max_var+1);
vit = t_vars.begin();
for(; vit!=vend; ++vit) {
unsigned v = *vit;
for(unsigned v = 0; v < t_vars.size(); ++v) {
if (!t_vars[v]) {
continue;
}
int2ints::entry * e = var_indexes.find_core(v);
if(!e) {
//we have an unbound variable, so we add an unbound column for it
relation_sort unbound_sort = 0;
for(unsigned hindex = 0; hindex<head_len; hindex++) {
expr * harg = h->get_arg(hindex);
if(!is_var(harg) || to_var(harg)->get_idx()!=v) {
continue;
}
unbound_sort = to_var(harg)->get_sort();
}
if(!unbound_sort) {
// the variable in the interpreted tail is neither bound in the
// uninterpreted tail nor present in the head
std::stringstream sstm;
sstm << "rule with unbound variable #" << v << " in interpreted tail: ";
r->display(m_context, sstm);
throw default_exception(sstm.str());
}
relation_sort unbound_sort = t_vars[v];
reg_idx new_reg;
TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
@ -759,7 +742,7 @@ namespace datalog {
m_instruction_observer.finish_rule();
}
void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr,
void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr,
bool & dealloc, instruction_block & acc) {
uint_set pos_vars;
u_map<expr*> neg_vars;
@ -782,7 +765,7 @@ namespace datalog {
}
// populate positive variables:
for (unsigned i = 0; i < single_res_expr.size(); ++i) {
expr* e = single_res_expr[i];
expr* e = single_res_expr[i].get();
if (is_var(e)) {
pos_vars.insert(to_var(e)->get_idx());
}
@ -849,19 +832,19 @@ namespace datalog {
typedef rule_dependencies::item_set item_set; //set of T
rule_dependencies & m_deps;
rule_set const& m_rules;
context& m_context;
item_set & m_removed;
svector<T> m_stack;
ast_mark m_stack_content;
ast_mark m_visited;
void traverse(T v) {
SASSERT(!m_visited.is_marked(v));
if (m_removed.contains(v)) {
SASSERT(!m_stack_content.is_marked(v));
if(m_visited.is_marked(v) || m_removed.contains(v)) {
return;
}
m_stack.push_back(v);
m_stack_content.mark(v, true);
m_visited.mark(v, true);
const item_set & deps = m_deps.get_deps(v);
@ -869,49 +852,22 @@ namespace datalog {
item_set::iterator end = deps.end();
for(; it!=end; ++it) {
T d = *it;
if (m_visited.is_marked(d)) {
if(m_stack_content.is_marked(d)) {
//TODO: find the best vertex to remove in the cycle
remove_from_stack();
continue;
m_removed.insert(v);
break;
}
traverse(d);
}
SASSERT(m_stack.back()==v);
m_stack.pop_back();
m_visited.mark(v, false);
}
void remove_from_stack() {
for (unsigned i = 0; i < m_stack.size(); ++i) {
func_decl* p = m_stack[i];
if (m_context.has_facts(p)) {
m_removed.insert(p);
return;
}
rule_vector const& rules = m_rules.get_predicate_rules(p);
unsigned stratum = m_rules.get_predicate_strat(p);
for (unsigned j = 0; j < rules.size(); ++j) {
rule const& r = *rules[j];
bool ok = true;
for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
}
if (ok) {
m_removed.insert(p);
return;
}
}
}
// nothing was found.
m_removed.insert(m_stack.back());
m_stack_content.mark(v, false);
}
public:
cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed)
: m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }
cycle_breaker(rule_dependencies & deps, item_set & removed)
: m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); }
void operator()() {
rule_dependencies::iterator it = m_deps.begin();
@ -933,7 +889,7 @@ namespace datalog {
rule_dependencies deps(m_rule_set.get_dependencies());
deps.restrict(preds);
cycle_breaker(deps, m_rule_set, m_context, global_deltas)();
cycle_breaker(deps, global_deltas)();
VERIFY( deps.sort_deps(ordered_preds) );
//the predicates that were removed to get acyclic induced subgraph are put last
@ -1069,12 +1025,17 @@ namespace datalog {
}
func_decl_vector preds_vector;
func_decl_set global_deltas;
func_decl_set global_deltas_dummy;
detect_chains(head_preds, preds_vector, global_deltas);
detect_chains(head_preds, preds_vector, global_deltas_dummy);
/*
FIXME: right now we use all preds as global deltas for correctness purposes
func_decl_set local_deltas(head_preds);
set_difference(local_deltas, global_deltas);
*/
func_decl_set local_deltas;
func_decl_set global_deltas(head_preds);
pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop
get_fresh_registers(global_deltas, d_global_src);

4
src/muz_qe/dl_compiler.h
View file

@ -41,7 +41,7 @@ namespace datalog {
typedef hashtable<unsigned, u_hash, u_eq> int_set;
typedef u_map<unsigned> int2int;
typedef u_map<unsigned_vector> int2ints;
typedef map<func_decl *, reg_idx, ptr_hash<func_decl>,ptr_eq<func_decl> > pred2idx;
typedef obj_map<func_decl, reg_idx> pred2idx;
typedef unsigned_vector var_vector;
typedef ptr_vector<func_decl> func_decl_vector;
@ -177,7 +177,7 @@ namespace datalog {
void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result,
instruction_block & acc);
void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr,
void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr,
bool & dealloc, instruction_block& acc);
void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc);

85
src/muz_qe/dl_context.cpp
View file

@ -41,7 +41,6 @@ Revision History:
#include"for_each_expr.h"
#include"ast_smt_pp.h"
#include"ast_smt2_pp.h"
#include"expr_functors.h"
#include"dl_mk_partial_equiv.h"
#include"dl_mk_bit_blast.h"
#include"dl_mk_array_blast.h"
@ -49,7 +48,6 @@ Revision History:
#include"dl_mk_quantifier_abstraction.h"
#include"dl_mk_quantifier_instantiation.h"
#include"datatype_decl_plugin.h"
#include"expr_abstract.h"
namespace datalog {
@ -226,6 +224,10 @@ namespace datalog {
m_rewriter(m),
m_var_subst(m),
m_rule_manager(*this),
m_elim_unused_vars(m),
m_abstractor(m),
m_contains_p(*this),
m_check_pred(m_contains_p, m),
m_transf(*this),
m_trail(*this),
m_pinned(m),
@ -301,18 +303,19 @@ namespace datalog {
expr_ref context::bind_variables(expr* fml, bool is_forall) {
expr_ref result(m);
app_ref_vector const & vars = m_vars;
rule_manager& rm = get_rule_manager();
if (vars.empty()) {
result = fml;
}
else {
ptr_vector<sort> sorts;
expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
get_free_vars(result, sorts);
m_names.reset();
m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
rm.collect_vars(result);
ptr_vector<sort>& sorts = rm.get_var_sorts();
if (sorts.empty()) {
result = fml;
}
else {
svector<symbol> names;
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
if (i < vars.size()) {
@ -323,16 +326,16 @@ namespace datalog {
}
}
if (i < vars.size()) {
names.push_back(vars[i]->get_decl()->get_name());
m_names.push_back(vars[i]->get_decl()->get_name());
}
else {
names.push_back(symbol(i));
m_names.push_back(symbol(i));
}
}
quantifier_ref q(m);
sorts.reverse();
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
elim_unused_vars(m, q, result);
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result);
m_elim_unused_vars(q, result);
}
}
return result;
@ -544,6 +547,8 @@ namespace datalog {
throw default_exception("get_num_levels is not supported for bmc");
case TAB_ENGINE:
throw default_exception("get_num_levels is not supported for tab");
case CLP_ENGINE:
throw default_exception("get_num_levels is not supported for clp");
default:
throw default_exception("unknown engine");
}
@ -562,6 +567,8 @@ namespace datalog {
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
@ -581,6 +588,8 @@ namespace datalog {
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
@ -607,28 +616,16 @@ namespace datalog {
}
}
class context::contains_pred : public i_expr_pred {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
virtual ~contains_pred() {}
virtual bool operator()(expr* e) {
return ctx.is_predicate(e);
}
};
void context::check_existential_tail(rule_ref& r) {
unsigned ut_size = r->get_uninterpreted_tail_size();
unsigned t_size = r->get_tail_size();
contains_pred contains_p(*this);
check_pred check_pred(contains_p, get_manager());
TRACE("dl", r->display_smt2(get_manager(), tout); tout << "\n";);
for (unsigned i = ut_size; i < t_size; ++i) {
app* t = r->get_tail(i);
TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";);
if (check_pred(t)) {
if (m_check_pred(t)) {
std::ostringstream out;
out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate";
throw default_exception(out.str());
@ -720,6 +717,10 @@ namespace datalog {
check_existential_tail(r);
check_positive_predicates(r);
break;
case CLP_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
default:
UNREACHABLE();
break;
@ -813,9 +814,8 @@ namespace datalog {
void context::transform_rules() {
m_transf.reset();
if (get_params().filter_rules()) {
m_transf.register_plugin(alloc(mk_filter_rules, *this));
}
m_transf.register_plugin(alloc(mk_coi_filter, *this));
m_transf.register_plugin(alloc(mk_filter_rules, *this));
m_transf.register_plugin(alloc(mk_simple_joins, *this));
if (unbound_compressor()) {
m_transf.register_plugin(alloc(mk_unbound_compressor, *this));
@ -823,7 +823,14 @@ namespace datalog {
if (similarity_compressor()) {
m_transf.register_plugin(alloc(mk_similarity_compressor, *this));
}
m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
m_transf.register_plugin(alloc(mk_partial_equivalence_transformer, *this));
m_transf.register_plugin(alloc(mk_rule_inliner, *this));
m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this));
if (get_params().bit_blast()) {
m_transf.register_plugin(alloc(mk_bit_blast, *this, 22000));
m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this, 21000));
}
transform_rules(m_transf);
}
@ -988,6 +995,9 @@ namespace datalog {
else if (e == symbol("tab")) {
m_engine = TAB_ENGINE;
}
else if (e == symbol("clp")) {
m_engine = CLP_ENGINE;
}
if (m_engine == LAST_ENGINE) {
expr_fast_mark1 mark;
@ -1023,6 +1033,8 @@ namespace datalog {
return bmc_query(query);
case TAB_ENGINE:
return tab_query(query);
case CLP_ENGINE:
return clp_query(query);
default:
UNREACHABLE();
return rel_query(query);
@ -1087,11 +1099,22 @@ namespace datalog {
}
}
void context::ensure_clp() {
if (!m_clp.get()) {
m_clp = alloc(clp, *this);
}
}
lbool context::tab_query(expr* query) {
ensure_tab();
return m_tab->query(query);
}
lbool context::clp_query(expr* query) {
ensure_clp();
return m_clp->query(query);
}
void context::ensure_rel() {
if (!m_rel.get()) {
m_rel = alloc(rel_context, *this);
@ -1132,6 +1155,10 @@ namespace datalog {
ensure_tab();
m_last_answer = m_tab->get_answer();
return m_last_answer.get();
case CLP_ENGINE:
ensure_clp();
m_last_answer = m_clp->get_answer();
return m_last_answer.get();
default:
UNREACHABLE();
}
@ -1157,6 +1184,10 @@ namespace datalog {
ensure_tab();
m_tab->display_certificate(out);
return true;
case CLP_ENGINE:
ensure_clp();
m_clp->display_certificate(out);
return true;
default:
return false;
}

25
src/muz_qe/dl_context.h
View file

@ -45,6 +45,9 @@ Revision History:
#include"model2expr.h"
#include"smt_params.h"
#include"dl_rule_transformer.h"
#include"expr_abstract.h"
#include"expr_functors.h"
#include"clp_context.h"
namespace datalog {
@ -76,6 +79,18 @@ namespace datalog {
typedef obj_map<const func_decl, svector<symbol> > pred2syms;
typedef obj_map<const sort, sort_domain*> sort_domain_map;
class contains_pred : public i_expr_pred {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
virtual ~contains_pred() {}
virtual bool operator()(expr* e) {
return ctx.is_predicate(e);
}
};
ast_manager & m;
smt_params & m_fparams;
params_ref m_params_ref;
@ -84,10 +99,15 @@ namespace datalog {
th_rewriter m_rewriter;
var_subst m_var_subst;
rule_manager m_rule_manager;
unused_vars_eliminator m_elim_unused_vars;
expr_abstractor m_abstractor;
contains_pred m_contains_p;
check_pred m_check_pred;
rule_transformer m_transf;
trail_stack<context> m_trail;
ast_ref_vector m_pinned;
app_ref_vector m_vars;
svector<symbol> m_names;
sort_domain_map m_sorts;
func_decl_set m_preds;
sym2decl m_preds_by_name;
@ -104,6 +124,7 @@ namespace datalog {
scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
scoped_ptr<tab> m_tab;
scoped_ptr<clp> m_clp;
bool m_closed;
bool m_saturation_was_run;
@ -457,6 +478,8 @@ namespace datalog {
void ensure_tab();
void ensure_clp();
void ensure_rel();
void new_query();
@ -469,6 +492,8 @@ namespace datalog {
lbool tab_query(expr* query);
lbool clp_query(expr* query);
void check_quantifier_free(rule_ref& r);
void check_uninterpreted_free(rule_ref& r);
void check_existential_tail(rule_ref& r);

4
src/muz_qe/dl_finite_product_relation.cpp
View file

@ -1291,8 +1291,8 @@ namespace datalog {
m_renaming_for_inner_rel(m_manager) {
relation_manager & rmgr = r.get_manager();
idx_set cond_columns;
collect_vars(m_manager, m_cond, cond_columns);
rule_manager& rm = r.get_context().get_rule_manager();
idx_set& cond_columns = rm.collect_vars(m_cond);
unsigned sig_sz = r.get_signature().size();
for(unsigned i=0; i<sig_sz; i++) {

2
src/muz_qe/dl_finite_product_relation.h
View file

@ -47,7 +47,7 @@ namespace datalog {
}
struct hash {
unsigned operator()(const rel_spec & o) const {
return o.m_inner_kind^int_vector_hash(o.m_table_cols);
return o.m_inner_kind^svector_hash<bool_hash>()(o.m_table_cols);
}
};
};

16
src/muz_qe/dl_instruction.cpp
View file

@ -359,21 +359,7 @@ namespace datalog {
r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
try {
ctx.set_reg(m_res, (*fn)(r1, r2));
}
catch(...)
{
std::string annotation;
unsigned sz;
ctx.get_register_annotation(m_rel1, annotation);
sz = ctx.reg(m_rel1)?ctx.reg(m_rel1)->get_size_estimate_rows():0;
std::cout << m_rel1 << "\t" << sz << "\t" << annotation << "\n";
ctx.get_register_annotation(m_rel2, annotation);
sz = ctx.reg(m_rel2)?ctx.reg(m_rel2)->get_size_estimate_rows():0;
std::cout << m_rel2 << "\t" << sz << "\t" << annotation << "\n";
throw;
}
ctx.set_reg(m_res, (*fn)(r1, r2));
TRACE("dl",
ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);

7
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -145,7 +145,6 @@ namespace datalog {
expr_ref_vector conjs(m), new_conjs(m);
expr_ref tmp(m);
expr_safe_replace sub(m);
uint_set lhs_vars, rhs_vars;
bool change = false;
bool inserted = false;
@ -161,10 +160,8 @@ namespace datalog {
if (is_store_def(e, x, y)) {
// enforce topological order consistency:
uint_set lhs;
collect_vars(m, x, lhs_vars);
collect_vars(m, y, rhs_vars);
lhs = lhs_vars;
uint_set lhs = rm.collect_vars(x);
uint_set rhs_vars = rm.collect_vars(y);
lhs &= rhs_vars;
if (!lhs.empty()) {
TRACE("dl", tout << "unusable equality " << mk_pp(e, m) << "\n";);

78
src/muz_qe/dl_mk_backwards.cpp Normal file
View file

@ -0,0 +1,78 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_backwards.cpp
Abstract:
Create Horn clauses for backwards flow.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-17
Revision History:
--*/
#include"dl_mk_backwards.h"
#include"dl_context.h"
namespace datalog {
mk_backwards::mk_backwards(context & ctx, unsigned priority):
plugin(priority),
m(ctx.get_manager()),
m_ctx(ctx) {
}
mk_backwards::~mk_backwards() { }
rule_set * mk_backwards::operator()(rule_set const & source) {
context& ctx = source.get_context();
rule_manager& rm = source.get_rule_manager();
rule_set * result = alloc(rule_set, ctx);
unsigned sz = source.get_num_rules();
rule_ref new_rule(rm);
app_ref_vector tail(m);
app_ref head(m);
svector<bool> neg;
app_ref query(m);
query = m.mk_fresh_const("Q", m.mk_bool_sort());
result->set_output_predicate(query->get_decl());
m_ctx.register_predicate(query->get_decl(), false);
for (unsigned i = 0; i < sz; ++i) {
tail.reset();
neg.reset();
rule & r = *source.get_rule(i);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
if (!source.is_output_predicate(r.get_decl())) {
tail.push_back(r.get_head());
neg.push_back(false);
}
for (unsigned j = utsz; j < tsz; ++j) {
tail.push_back(r.get_tail(j));
neg.push_back(false);
}
for (unsigned j = 0; j <= utsz; ++j) {
if (j == utsz && j > 0) {
break;
}
if (j == utsz) {
head = query;
}
else {
head = r.get_tail(j);
}
new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
result->add_rule(new_rule);
}
}
TRACE("dl", result->display(tout););
return result;
}
};

38
src/muz_qe/dl_mk_backwards.h Normal file
View file

@ -0,0 +1,38 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_backwards.h
Abstract:
Create Horn clauses for backwards flow.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-17
Revision History:
--*/
#ifndef _DL_MK_BACKWARDS_H_
#define _DL_MK_BACKWARDS_H_
#include"dl_rule_transformer.h"
namespace datalog {
class mk_backwards : public rule_transformer::plugin {
ast_manager& m;
context& m_ctx;
public:
mk_backwards(context & ctx, unsigned priority = 33000);
~mk_backwards();
rule_set * operator()(rule_set const & source);
};
};
#endif /* _DL_MK_BACKWARDS_H_ */

31
src/muz_qe/dl_mk_filter_rules.cpp
View file

@ -27,9 +27,10 @@ namespace datalog {
mk_filter_rules::mk_filter_rules(context & ctx):
plugin(2000),
m_context(ctx),
m_manager(ctx.get_manager()),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_result(0),
m_pinned(m_manager) {
m_pinned(m) {
}
mk_filter_rules::~mk_filter_rules() {
@ -52,14 +53,14 @@ namespace datalog {
*/
bool mk_filter_rules::is_candidate(app * pred) {
if (!m_context.is_predicate(pred)) {
TRACE("mk_filter_rules", tout << mk_pp(pred, m_manager) << "\nis not a candidate because it is interpreted.\n";);
TRACE("mk_filter_rules", tout << mk_pp(pred, m) << "\nis not a candidate because it is interpreted.\n";);
return false;
}
var_idx_set used_vars;
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; i++) {
expr * arg = pred->get_arg(i);
if (m_manager.is_value(arg))
if (m.is_value(arg))
return true;
SASSERT(is_var(arg));
unsigned vidx = to_var(arg)->get_idx();
@ -74,10 +75,10 @@ namespace datalog {
\brief Create a "filter" (if it doesn't exist already) for the given predicate.
*/
func_decl * mk_filter_rules::mk_filter_decl(app * pred, var_idx_set const & non_local_vars) {
sort_ref_buffer filter_domain(m_manager);
sort_ref_buffer filter_domain(m);
filter_key * key = alloc(filter_key, m_manager);
mk_new_rule_tail(m_manager, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
filter_key * key = alloc(filter_key, m);
mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
func_decl * filter_decl = 0;
if (!m_tail2filter.find(key, filter_decl)) {
filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"),
@ -85,8 +86,8 @@ namespace datalog {
m_pinned.push_back(filter_decl);
m_tail2filter.insert(key, filter_decl);
app_ref filter_head(m_manager);
filter_head = m_manager.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
app_ref filter_head(m);
filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
app * filter_tail = key->new_pred;
rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0);
filter_rule->set_accounting_parent_object(m_context, m_current);
@ -104,16 +105,15 @@ namespace datalog {
void mk_filter_rules::process(rule * r) {
m_current = r;
app * new_head = r->get_head();
app_ref_vector new_tail(m_manager);
app_ref_vector new_tail(m);
svector<bool> new_is_negated;
unsigned sz = r->get_tail_size();
bool rule_modified = false;
for (unsigned i = 0; i < sz; i++) {
app * tail = r->get_tail(i);
if (is_candidate(tail)) {
TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m_manager) << "\n";);
var_idx_set non_local_vars;
collect_non_local_vars(m_manager, r, tail, non_local_vars);
TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m) << "\n";);
var_idx_set non_local_vars = rm.collect_rule_vars_ex(r, tail);
func_decl * filter_decl = mk_filter_decl(tail, non_local_vars);
ptr_buffer<expr> new_args;
var_idx_set used_vars;
@ -129,7 +129,7 @@ namespace datalog {
}
}
SASSERT(new_args.size() == filter_decl->get_arity());
new_tail.push_back(m_manager.mk_app(filter_decl, new_args.size(), new_args.c_ptr()));
new_tail.push_back(m.mk_app(filter_decl, new_args.size(), new_args.c_ptr()));
rule_modified = true;
}
else {
@ -152,9 +152,6 @@ namespace datalog {
}
rule_set * mk_filter_rules::operator()(rule_set const & source) {
if (!m_context.get_params().filter_rules()) {
return 0;
}
m_tail2filter.reset();
m_result = alloc(rule_set, m_context);
m_modified = false;

11
src/muz_qe/dl_mk_filter_rules.h
View file

@ -45,17 +45,22 @@ namespace datalog {
filter_key(ast_manager & m) : new_pred(m), filter_args(m) {}
unsigned hash() const {
return new_pred->hash() ^ int_vector_hash(filter_args);
unsigned r = new_pred->hash();
for (unsigned i = 0; i < filter_args.size(); ++i) {
r ^= filter_args[i]->hash();
}
return r;
}
bool operator==(const filter_key & o) const {
return o.new_pred==new_pred && vectors_equal(o.filter_args, filter_args);
}
};
typedef map<filter_key*, func_decl*, obj_ptr_hash<filter_key>, deref_eq<filter_key> > filter_cache;
typedef obj_map<filter_key, func_decl*> filter_cache;
context & m_context;
ast_manager & m_manager;
ast_manager & m;
rule_manager & rm;
filter_cache m_tail2filter;
rule_set * m_result;
rule * m_current;

98
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -67,24 +67,23 @@ namespace datalog {
void mk_interp_tail_simplifier::rule_substitution::get_result(rule_ref & res) {
SASSERT(m_rule);
app_ref new_head(m);
apply(m_rule->get_head(), new_head);
apply(m_rule->get_head(), m_head);
app_ref_vector tail(m);
svector<bool> tail_neg;
m_tail.reset();
m_neg.reset();
unsigned tail_len = m_rule->get_tail_size();
for (unsigned i=0; i<tail_len; i++) {
app_ref new_tail_el(m);
apply(m_rule->get_tail(i), new_tail_el);
tail.push_back(new_tail_el);
tail_neg.push_back(m_rule->is_neg_tail(i));
m_tail.push_back(new_tail_el);
m_neg.push_back(m_rule->is_neg_tail(i));
}
mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg);
SASSERT(tail.size() == tail_neg.size());
res = m_context.get_rule_manager().mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
SASSERT(m_tail.size() == m_neg.size());
res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr());
res->set_accounting_parent_object(m_context, m_rule);
res->norm_vars(res.get_manager());
}
@ -362,14 +361,37 @@ namespace datalog {
}
};
class mk_interp_tail_simplifier::normalizer_rw : public rewriter_tpl<normalizer_cfg> {
public:
normalizer_rw(ast_manager& m, normalizer_cfg& cfg): rewriter_tpl<normalizer_cfg>(m, false, cfg) {}
};
mk_interp_tail_simplifier::mk_interp_tail_simplifier(context & ctx, unsigned priority)
: plugin(priority),
m(ctx.get_manager()),
m_context(ctx),
m_simp(ctx.get_rewriter()),
a(m),
m_rule_subst(ctx),
m_tail(m),
m_itail_members(m),
m_conj(m) {
m_cfg = alloc(normalizer_cfg, m);
m_rw = alloc(normalizer_rw, m, *m_cfg);
}
mk_interp_tail_simplifier::~mk_interp_tail_simplifier() {
dealloc(m_rw);
dealloc(m_cfg);
}
void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res)
{
expr_ref simp1_res(m);
m_simp(a, simp1_res);
normalizer_cfg r_cfg(m);
rewriter_tpl<normalizer_cfg> rwr(m, false, r_cfg);
expr_ref dl_form_e(m);
rwr(simp1_res.get(), res);
(*m_rw)(simp1_res.get(), res);
/*if (simp1_res.get()!=res.get()) {
std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
@ -385,15 +407,15 @@ namespace datalog {
return false;
}
ptr_vector<expr> todo;
m_todo.reset();
m_leqs.reset();
for (unsigned i = u_len; i < len; i++) {
todo.push_back(r->get_tail(i));
m_todo.push_back(r->get_tail(i));
SASSERT(!r->is_neg_tail(i));
}
m_rule_subst.reset(r);
obj_hashtable<expr> leqs;
expr_ref_vector trail(m);
expr_ref tmp1(m), tmp2(m);
bool found_something = false;
@ -401,10 +423,10 @@ namespace datalog {
#define TRY_UNIFY(_x,_y) if (m_rule_subst.unify(_x,_y)) { found_something = true; }
#define IS_FLEX(_x) (is_var(_x) || m.is_value(_x))
while (!todo.empty()) {
while (!m_todo.empty()) {
expr * arg1, *arg2;
expr * t0 = todo.back();
todo.pop_back();
expr * t0 = m_todo.back();
m_todo.pop_back();
expr* t = t0;
bool neg = m.is_not(t, t);
if (is_var(t)) {
@ -412,7 +434,7 @@ namespace datalog {
}
else if (!neg && m.is_and(t)) {
app* a = to_app(t);
todo.append(a->get_num_args(), a->get_args());
m_todo.append(a->get_num_args(), a->get_args());
}
else if (!neg && m.is_eq(t, arg1, arg2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
TRY_UNIFY(arg1, arg2);
@ -440,12 +462,12 @@ namespace datalog {
else if (!neg && (a.is_le(t, arg1, arg2) || a.is_ge(t, arg2, arg1))) {
tmp1 = a.mk_sub(arg1, arg2);
tmp2 = a.mk_sub(arg2, arg1);
if (false && leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
if (false && m_leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
TRY_UNIFY(arg1, arg2);
}
else {
trail.push_back(tmp1);
leqs.insert(tmp1);
m_leqs.insert(tmp1);
}
}
}
@ -485,12 +507,12 @@ namespace datalog {
}
app_ref head(r->get_head(), m);
app_ref_vector tail(m);
svector<bool> tail_neg;
m_tail.reset();
m_tail_neg.reset();
for (unsigned i=0; i<u_len; i++) {
tail.push_back(r->get_tail(i));
tail_neg.push_back(r->is_neg_tail(i));
m_tail.push_back(r->get_tail(i));
m_tail_neg.push_back(r->is_neg_tail(i));
}
bool modified = false;
@ -502,12 +524,12 @@ namespace datalog {
SASSERT(!r->is_neg_tail(u_len));
}
else {
expr_ref_vector itail_members(m);
m_itail_members.reset();
for (unsigned i=u_len; i<len; i++) {
itail_members.push_back(r->get_tail(i));
m_itail_members.push_back(r->get_tail(i));
SASSERT(!r->is_neg_tail(i));
}
itail = m.mk_and(itail_members.size(), itail_members.c_ptr());
itail = m.mk_and(m_itail_members.size(), m_itail_members.c_ptr());
modified = true;
}
@ -523,21 +545,21 @@ namespace datalog {
SASSERT(m.is_bool(simp_res));
if (modified) {
expr_ref_vector conjs(m);
flatten_and(simp_res, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
m_conj.reset();
flatten_and(simp_res, m_conj);
for (unsigned i = 0; i < m_conj.size(); ++i) {
expr* e = m_conj[i].get();
if (is_app(e)) {
tail.push_back(to_app(e));
m_tail.push_back(to_app(e));
}
else {
tail.push_back(m.mk_eq(e, m.mk_true()));
m_tail.push_back(m.mk_eq(e, m.mk_true()));
}
tail_neg.push_back(false);
m_tail_neg.push_back(false);
}
SASSERT(tail.size() == tail_neg.size());
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
SASSERT(m_tail.size() == m_tail_neg.size());
res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr());
res->set_accounting_parent_object(m_context, r);
}
else {

33
src/muz_qe/dl_mk_interp_tail_simplifier.h
View file

@ -34,15 +34,17 @@ namespace datalog {
{
ast_manager& m;
context& m_context;
substitution m_subst;
unifier m_unif;
rule * m_rule;
substitution m_subst;
unifier m_unif;
app_ref m_head;
app_ref_vector m_tail;
svector<bool> m_neg;
rule * m_rule;
void apply(app * a, app_ref& res);
public:
rule_substitution(context & ctx)
: m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_rule(0) {}
: m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_head(m), m_tail(m), m_rule(0) {}
/**
Reset substitution and get it ready for working with rule r.
@ -61,13 +63,23 @@ namespace datalog {
}
};
class normalizer_cfg;
class normalizer_rw;
ast_manager & m;
context & m_context;
th_rewriter & m_simp;
arith_util a;
rule_substitution m_rule_subst;
ptr_vector<expr> m_todo;
obj_hashtable<expr> m_leqs;
app_ref_vector m_tail;
expr_ref_vector m_itail_members;
expr_ref_vector m_conj;
svector<bool> m_tail_neg;
normalizer_cfg* m_cfg;
normalizer_rw* m_rw;
class normalizer_cfg;
void simplify_expr(app * a, expr_ref& res);
@ -77,13 +89,8 @@ namespace datalog {
/** Return true if something was modified */
bool transform_rules(const rule_set & orig, rule_set & tgt);
public:
mk_interp_tail_simplifier(context & ctx, unsigned priority=40000)
: plugin(priority),
m(ctx.get_manager()),
m_context(ctx),
m_simp(ctx.get_rewriter()),
a(m),
m_rule_subst(ctx) {}
mk_interp_tail_simplifier(context & ctx, unsigned priority=40000);
virtual ~mk_interp_tail_simplifier();
/**If rule should be retained, assign transformed version to res and return true;
if rule can be deleted, return false.

47
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -35,6 +35,8 @@ Revision History:
#include"dl_mk_karr_invariants.h"
#include"expr_safe_replace.h"
#include"bool_rewriter.h"
#include"dl_mk_backwards.h"
#include"dl_mk_loop_counter.h"
namespace datalog {
@ -199,6 +201,29 @@ 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"););
#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
rule_set* rules = lc.revert(*src_annot);
rules->inherit_predicates(source);
TRACE("dl", rules->display(tout););
return rules;
}
rule_set* mk_karr_invariants::update_using_propagation(rule_set const& src, rule_set const& srcref) {
m_inner_ctx.reset();
rel_context& rctx = m_inner_ctx.get_rel_context();
ptr_vector<func_decl> heads;
@ -207,24 +232,24 @@ namespace datalog {
m_inner_ctx.register_predicate(*fit, false);
}
m_inner_ctx.ensure_opened();
m_inner_ctx.replace_rules(source);
m_inner_ctx.replace_rules(srcref);
m_inner_ctx.close();
rule_set::decl2rules::iterator dit = source.begin_grouped_rules();
rule_set::decl2rules::iterator dend = source.end_grouped_rules();
rule_set::decl2rules::iterator dit = srcref.begin_grouped_rules();
rule_set::decl2rules::iterator dend = srcref.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* rules = alloc(rule_set, m_ctx);
it = source.begin();
rule_set* dst = alloc(rule_set, m_ctx);
rule_set::iterator it = src.begin(), end = src.end();
for (; it != end; ++it) {
update_body(rctx, *rules, **it);
update_body(rctx, *dst, **it);
}
if (m_ctx.get_model_converter()) {
add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m);
rule_set::decl2rules::iterator git = source.begin_grouped_rules();
rule_set::decl2rules::iterator gend = source.end_grouped_rules();
rule_set::decl2rules::iterator git = src.begin_grouped_rules();
rule_set::decl2rules::iterator gend = src.end_grouped_rules();
for (; git != gend; ++git) {
func_decl* p = git->m_key;
expr_ref fml(m);
@ -236,9 +261,9 @@ namespace datalog {
}
m_ctx.add_model_converter(kmc);
}
TRACE("dl", rules->display(tout););
rules->inherit_predicates(source);
return rules;
dst->inherit_predicates(src);
return dst;
}
void mk_karr_invariants::update_body(rel_context& rctx, rule_set& rules, rule& r) {

2
src/muz_qe/dl_mk_karr_invariants.h
View file

@ -56,7 +56,7 @@ namespace datalog {
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);
public:
mk_karr_invariants(context & ctx, unsigned priority);

60
src/muz_qe/dl_mk_loop_counter.cpp
View file

@ -32,7 +32,7 @@ namespace datalog {
mk_loop_counter::~mk_loop_counter() { }
app_ref mk_loop_counter::add_arg(app* fn, unsigned idx) {
app_ref mk_loop_counter::add_arg(rule_set const& src, rule_set& dst, app* fn, unsigned idx) {
expr_ref_vector args(m);
func_decl* new_fn, *old_fn = fn->get_decl();
args.append(fn->get_num_args(), fn->get_args());
@ -46,17 +46,29 @@ namespace datalog {
m_old2new.insert(old_fn, new_fn);
m_new2old.insert(new_fn, old_fn);
m_refs.push_back(new_fn);
m_ctx.register_predicate(new_fn, false);
if (src.is_output_predicate(old_fn)) {
dst.set_output_predicate(new_fn);
}
}
return app_ref(m.mk_app(new_fn, args.size(), args.c_ptr()), m);
}
app_ref mk_loop_counter::del_arg(app* fn) {
expr_ref_vector args(m);
func_decl* old_fn, *new_fn = fn->get_decl();
SASSERT(fn->get_num_args() > 0);
args.append(fn->get_num_args()-1, fn->get_args());
VERIFY (m_new2old.find(new_fn, old_fn));
return app_ref(m.mk_app(old_fn, args.size(), args.c_ptr()), m);
}
rule_set * mk_loop_counter::operator()(rule_set const & source) {
m_refs.reset();
m_old2new.reset();
m_new2old.reset();
context& ctx = source.get_context();
rule_manager& rm = source.get_rule_manager();
rule_set * result = alloc(rule_set, ctx);
rule_set * result = alloc(rule_set, m_ctx);
unsigned sz = source.get_num_rules();
rule_ref new_rule(rm);
app_ref_vector tail(m);
@ -71,16 +83,14 @@ namespace datalog {
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < utsz; ++j, ++cnt) {
tail.push_back(add_arg(r.get_tail(j), cnt));
tail.push_back(add_arg(source, *result, r.get_tail(j), cnt));
neg.push_back(r.is_neg_tail(j));
m_ctx.register_predicate(tail.back()->get_decl(), false);
}
for (unsigned j = utsz; j < tsz; ++j) {
tail.push_back(r.get_tail(j));
neg.push_back(false);
}
head = add_arg(r.get_head(), cnt);
m_ctx.register_predicate(head->get_decl(), false);
head = add_arg(source, *result, r.get_head(), cnt);
// set the loop counter to be an increment of the previous
bool found = false;
unsigned last = head->get_num_args()-1;
@ -108,9 +118,41 @@ namespace datalog {
// model converter: remove references to extra argument.
// proof converter: remove references to extra argument as well.
result->inherit_predicates(source);
return result;
}
rule_set * mk_loop_counter::revert(rule_set const & source) {
context& ctx = source.get_context();
rule_manager& rm = source.get_rule_manager();
rule_set * result = alloc(rule_set, ctx);
unsigned sz = source.get_num_rules();
rule_ref new_rule(rm);
app_ref_vector tail(m);
app_ref head(m);
svector<bool> neg;
for (unsigned i = 0; i < sz; ++i) {
tail.reset();
neg.reset();
rule & r = *source.get_rule(i);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < utsz; ++j) {
tail.push_back(del_arg(r.get_tail(j)));
neg.push_back(r.is_neg_tail(j));
}
for (unsigned j = utsz; j < tsz; ++j) {
tail.push_back(r.get_tail(j));
neg.push_back(false);
}
head = del_arg(r.get_head());
new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
result->add_rule(new_rule);
}
// model converter: ...
// proof converter: ...
return result;
}
};

5
src/muz_qe/dl_mk_loop_counter.h
View file

@ -32,7 +32,8 @@ namespace datalog {
obj_map<func_decl, func_decl*> m_new2old;
obj_map<func_decl, func_decl*> m_old2new;
app_ref add_arg(app* fn, unsigned idx);
app_ref add_arg(rule_set const& src, rule_set& dst, app* fn, unsigned idx);
app_ref del_arg(app* fn);
public:
mk_loop_counter(context & ctx, unsigned priority = 33000);
~mk_loop_counter();
@ -40,6 +41,8 @@ namespace datalog {
rule_set * operator()(rule_set const & source);
func_decl* get_old(func_decl* f) const { return m_new2old.find(f); }
rule_set * revert(rule_set const& source);
};
};

3
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -28,6 +28,7 @@ namespace datalog {
plugin(10000, true),
m_context(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_pinned(m),
m_goal(goal, m) {
}
@ -259,7 +260,7 @@ namespace datalog {
}
new_tail.push_back(curr);
negations.push_back(r->is_neg_tail(curr_index));
collect_vars(m, curr, bound_vars);
bound_vars |= rm.collect_vars(curr);
}

8
src/muz_qe/dl_mk_magic_sets.h
View file

@ -47,6 +47,11 @@ namespace datalog {
AD_BOUND
};
struct a_flag_hash {
typedef a_flag data;
unsigned operator()(a_flag x) const { return x; }
};
struct adornment : public svector<a_flag> {
void populate(app * lit, const var_idx_set & bound_vars);
@ -71,7 +76,7 @@ namespace datalog {
return m_pred==o.m_pred && m_adornment==o.m_adornment;
}
unsigned hash() const {
return m_pred->hash()^int_vector_hash(m_adornment);
return m_pred->hash()^svector_hash<a_flag_hash>()(m_adornment);
}
};
@ -90,6 +95,7 @@ namespace datalog {
context & m_context;
ast_manager & m;
rule_manager& rm;
ast_ref_vector m_pinned;
/**
\brief Predicates from the original set that appear in a head of a rule

30
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -505,9 +505,6 @@ namespace datalog {
unsigned head_arity = head_pred->get_arity();
//var_idx_set head_vars;
//var_idx_set same_strat_vars;
//collect_vars(m, r->get_head(), head_vars);
unsigned pt_len = r->get_positive_tail_size();
for (unsigned ti=0; ti<pt_len; ++ti) {
@ -518,7 +515,6 @@ namespace datalog {
SASSERT(pred_strat<=head_strat);
if (pred_strat==head_strat) {
//collect_vars(m, r->get_head(), same_strat_vars);
if (pred->get_arity()>head_arity
|| (pred->get_arity()==head_arity && pred->get_id()>=head_pred->get_id()) ) {
return false;
@ -709,8 +705,7 @@ namespace datalog {
#define PRT(_x_) ((_x_)?"T":"F")
bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
bool done_something = false;
unsigned sz = rules->get_num_rules();
@ -731,7 +726,7 @@ namespace datalog {
svector<bool>& can_expand = m_head_visitor.can_expand();
for (unsigned i = 0; i < sz; ++i) {
add_rule(source, acc[i].get(), i);
add_rule(*rules, acc[i].get(), i);
}
// initialize substitution.
@ -808,7 +803,7 @@ namespace datalog {
TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
del_rule(r, i);
add_rule(source, rl_res.get(), i);
add_rule(*rules, rl_res.get(), i);
r = rl_res;
@ -828,13 +823,15 @@ namespace datalog {
}
}
if (done_something) {
rules = alloc(rule_set, m_context);
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
for (unsigned i = 0; i < sz; ++i) {
if (valid.get(i)) {
rules->add_rule(acc[i].get());
res->add_rule(acc[i].get());
}
}
TRACE("dl", rules->display(tout););
res->inherit_predicates(*rules);
TRACE("dl", res->display(tout););
rules = res.detach();
}
return done_something;
}
@ -871,11 +868,17 @@ namespace datalog {
// try eager inlining
if (do_eager_inlining(res)) {
something_done = true;
}
}
TRACE("dl", res->display(tout << "after eager inlining\n"););
}
if (something_done) {
res->inherit_predicates(source);
}
else {
res = alloc(rule_set, source);
}
if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
if (m_context.get_params().inline_linear() && inline_linear(res)) {
something_done = true;
}
@ -883,7 +886,6 @@ namespace datalog {
res = 0;
}
else {
res->inherit_predicates(source);
m_context.add_model_converter(hsmc.get());
}

2
src/muz_qe/dl_mk_rule_inliner.h
View file

@ -172,7 +172,7 @@ namespace datalog {
/**
Inline predicates that are known to not be join-points.
*/
bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
bool inline_linear(scoped_ptr<rule_set>& rules);
void add_rule(rule_set const& rule_set, rule* r, unsigned i);
void del_rule(rule* r, unsigned i);

10
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -29,6 +29,7 @@ namespace datalog {
m_manager(ctx.get_manager()),
m_threshold_count(ctx.similarity_compressor_threshold()),
m_result_rules(ctx.get_rule_manager()),
m_modified(false),
m_pinned(m_manager) {
SASSERT(m_threshold_count>1);
}
@ -55,6 +56,9 @@ namespace datalog {
return (a>b) ? 1 : ( (a==b) ? 0 : -1);
}
template<typename T>
static int aux_compare(T* a, T* b);
static int compare_var_args(app* t1, app* t2) {
SASSERT(t1->get_num_args()==t2->get_num_args());
int res;
@ -88,7 +92,7 @@ namespace datalog {
if ((skip_countdown--) == 0) {
continue;
}
res = aux_compare(t1->get_arg(i), t2->get_arg(i));
res = aux_compare(t1->get_arg(i)->get_id(), t2->get_arg(i)->get_id());
if (res!=0) { return res; }
}
return 0;
@ -113,7 +117,7 @@ namespace datalog {
for (int i=-1; i<pos_tail_sz; i++) {
app * t1 = get_by_tail_index(r1, i);
app * t2 = get_by_tail_index(r2, i);
res = aux_compare(t1->get_decl(), t2->get_decl());
res = aux_compare(t1->get_decl()->get_id(), t2->get_decl()->get_id());
if (res!=0) { return res; }
res = compare_var_args(t1, t2);
if (res!=0) { return res; }
@ -121,7 +125,7 @@ namespace datalog {
unsigned tail_sz = r1->get_tail_size();
for (unsigned i=pos_tail_sz; i<tail_sz; i++) {
res = aux_compare(r1->get_tail(i), r2->get_tail(i));
res = aux_compare(r1->get_tail(i)->get_id(), r2->get_tail(i)->get_id());
if (res!=0) { return res; }
}

27
src/muz_qe/dl_mk_simple_joins.cpp
View file

@ -29,7 +29,8 @@ namespace datalog {
mk_simple_joins::mk_simple_joins(context & ctx):
plugin(1000),
m_context(ctx) {
m_context(ctx),
rm(ctx.get_rule_manager()) {
}
class join_planner {
@ -120,6 +121,7 @@ namespace datalog {
context & m_context;
ast_manager & m;
rule_manager & rm;
var_subst & m_var_subst;
rule_set & m_rs_aux_copy; //reference to a rule_set that will allow to ask for stratum levels
@ -130,10 +132,13 @@ namespace datalog {
ptr_hashtable<rule, ptr_hash<rule>, ptr_eq<rule> > m_modified_rules;
ast_ref_vector m_pinned;
mutable ptr_vector<sort> m_vars;
public:
join_planner(context & ctx, rule_set & rs_aux_copy)
: m_context(ctx), m(ctx.get_manager()), m_var_subst(ctx.get_var_subst()),
: m_context(ctx), m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_var_subst(ctx.get_var_subst()),
m_rs_aux_copy(rs_aux_copy),
m_introduced_rules(ctx.get_rule_manager()),
m_pinned(ctx.get_manager())
@ -175,9 +180,7 @@ namespace datalog {
unsigned max_var_idx = 0;
{
var_idx_set orig_var_set;
collect_vars(m, t1, orig_var_set);
collect_vars(m, t2, orig_var_set);
var_idx_set& orig_var_set = rm.collect_vars(t1, t2);
var_idx_set::iterator ovit = orig_var_set.begin();
var_idx_set::iterator ovend = orig_var_set.end();
for(; ovit!=ovend; ++ovit) {
@ -323,14 +326,13 @@ namespace datalog {
}
for(unsigned i=0; i<pos_tail_size; i++) {
app * t1 = r->get_tail(i);
var_idx_set t1_vars;
collect_vars(m, t1, t1_vars);
var_idx_set t1_vars = rm.collect_vars(t1);
counter.count_vars(m, t1, -1); //temporarily remove t1 variables from counter
for(unsigned j=i+1; j<pos_tail_size; j++) {
app * t2 = r->get_tail(j);
counter.count_vars(m, t2, -1); //temporarily remove t2 variables from counter
var_idx_set scope_vars(t1_vars);
collect_vars(m, t2, scope_vars);
var_idx_set scope_vars = rm.collect_vars(t2);
scope_vars |= t1_vars;
var_idx_set non_local_vars;
counter.collect_positive(non_local_vars);
counter.count_vars(m, t2, 1); //restore t2 variables in counter
@ -472,8 +474,7 @@ namespace datalog {
while(!added_tails.empty()) {
app * a_tail = added_tails.back(); //added tail
var_idx_set a_tail_vars;
collect_vars(m, a_tail, a_tail_vars);
var_idx_set a_tail_vars = rm.collect_vars(a_tail);
counter.count_vars(m, a_tail, -1); //temporarily remove a_tail variables from counter
for(unsigned i=0; i<len; i++) {
@ -484,8 +485,8 @@ namespace datalog {
}
counter.count_vars(m, o_tail, -1); //temporarily remove o_tail variables from counter
var_idx_set scope_vars(a_tail_vars);
collect_vars(m, o_tail, scope_vars);
var_idx_set scope_vars = rm.collect_vars(o_tail);
scope_vars |= a_tail_vars;
var_idx_set non_local_vars;
counter.collect_positive(non_local_vars);
counter.count_vars(m, o_tail, 1); //restore o_tail variables in counter

3
src/muz_qe/dl_mk_simple_joins.h
View file

@ -49,7 +49,8 @@ namespace datalog {
We say that a rule containing C_i's is a rule with a "big tail".
*/
class mk_simple_joins : public rule_transformer::plugin {
context & m_context;
context & m_context;
rule_manager & rm;
public:
mk_simple_joins(context & ctx);

3
src/muz_qe/dl_mk_slice.cpp
View file

@ -725,6 +725,9 @@ namespace datalog {
m_mc->add_predicate(p, f);
}
}
else if (src.is_output_predicate(p)) {
dst.set_output_predicate(p);
}
}
}

6
src/muz_qe/dl_mk_subsumption_checker.cpp
View file

@ -241,6 +241,7 @@ namespace datalog {
tgt.add_rule(new_rule);
subs_index.add(new_rule);
}
tgt.inherit_predicates(orig);
TRACE("dl",
tout << "original set size: "<<orig.get_num_rules()<<"\n"
<< "reduced set size: "<<tgt.get_num_rules()<<"\n"; );
@ -338,7 +339,7 @@ namespace datalog {
rule_set * res = alloc(rule_set, m_context);
bool modified = transform_rules(source, *res);
if(!m_have_new_total_rule && !modified) {
if (!m_have_new_total_rule && !modified) {
dealloc(res);
return 0;
}
@ -347,7 +348,7 @@ namespace datalog {
//During the construction of the new set we may discover new total relations
//(by quantifier elimination on the uninterpreted tails).
SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
while(m_have_new_total_rule) {
while (m_have_new_total_rule) {
m_have_new_total_rule = false;
rule_set * old = res;
@ -355,7 +356,6 @@ namespace datalog {
transform_rules(*old, *res);
dealloc(old);
}
res->inherit_predicates(source);
return res;
}

28
src/muz_qe/dl_mk_unbound_compressor.cpp
View file

@ -27,7 +27,8 @@ namespace datalog {
plugin(500),
m_context(ctx),
m(ctx.get_manager()),
m_rules(ctx.get_rule_manager()),
rm(ctx.get_rule_manager()),
m_rules(rm),
m_pinned(m) {
}
@ -47,10 +48,7 @@ namespace datalog {
}
unsigned var_idx = to_var(head_arg)->get_idx();
var_idx_set tail_vars;
collect_tail_vars(m, r, tail_vars);
return tail_vars.contains(var_idx);
return rm.collect_tail_vars(r).contains(var_idx);
}
void mk_unbound_compressor::add_task(func_decl * pred, unsigned arg_index) {
@ -83,8 +81,7 @@ namespace datalog {
void mk_unbound_compressor::detect_tasks(rule_set const& source, unsigned rule_index) {
rule * r = m_rules.get(rule_index);
var_idx_set tail_vars;
collect_tail_vars(m, r, tail_vars);
var_idx_set& tail_vars = rm.collect_tail_vars(r);
app * head = r->get_head();
func_decl * head_pred = head->get_decl();
@ -94,9 +91,9 @@ namespace datalog {
}
unsigned n = head_pred->get_arity();
var_counter head_var_counter;
head_var_counter.count_vars(m, head, 1);
rm.get_counter().reset();
rm.get_counter().count_vars(m, head, 1);
for (unsigned i=0; i<n; i++) {
expr * arg = head->get_arg(i);
@ -107,7 +104,7 @@ namespace datalog {
if (!tail_vars.contains(var_idx)) {
//unbound
unsigned occurence_cnt = head_var_counter.get(var_idx);
unsigned occurence_cnt = rm.get_counter().get(var_idx);
SASSERT(occurence_cnt>0);
if (occurence_cnt == 1) {
TRACE("dl", r->display(m_context, tout << "Compress: "););
@ -121,15 +118,14 @@ namespace datalog {
void mk_unbound_compressor::try_compress(rule_set const& source, unsigned rule_index) {
start:
rule * r = m_rules.get(rule_index);
var_idx_set tail_vars;
collect_tail_vars(m, r, tail_vars);
var_idx_set& tail_vars = rm.collect_tail_vars(r);
app * head = r->get_head();
func_decl * head_pred = head->get_decl();
unsigned head_arity = head_pred->get_arity();
var_counter head_var_counter;
head_var_counter.count_vars(m, head);
rm.get_counter().reset();
rm.get_counter().count_vars(m, head);
unsigned arg_index;
for (arg_index = 0; arg_index < head_arity; arg_index++) {
@ -140,7 +136,7 @@ namespace datalog {
unsigned var_idx = to_var(arg)->get_idx();
if (!tail_vars.contains(var_idx)) {
//unbound
unsigned occurence_cnt = head_var_counter.get(var_idx);
unsigned occurence_cnt = rm.get_counter().get(var_idx);
SASSERT(occurence_cnt>0);
if ( occurence_cnt==1 && m_in_progress.contains(c_info(head_pred, arg_index)) ) {
//we have found what to compress

1
src/muz_qe/dl_mk_unbound_compressor.h
View file

@ -52,6 +52,7 @@ namespace datalog {
context & m_context;
ast_manager & m;
rule_manager & rm;
rule_ref_vector m_rules;
bool m_modified;
todo_stack m_todo;

6
src/muz_qe/dl_product_relation.h
View file

@ -40,8 +40,12 @@ namespace datalog {
class filter_equal_fn;
class filter_identical_fn;
class filter_interpreted_fn;
struct fid_hash {
typedef family_id data;
unsigned operator()(data x) const { return static_cast<unsigned>(x); }
};
rel_spec_store<rel_spec> m_spec_store;
rel_spec_store<rel_spec, svector_hash<fid_hash> > m_spec_store;
family_id get_relation_kind(const product_relation & r);

1
src/muz_qe/dl_relation_manager.cpp
View file

@ -740,7 +740,6 @@ namespace datalog {
relation_transformer_fn * relation_manager::mk_select_equal_and_project_fn(const relation_base & t,
const relation_element & value, unsigned col) {
relation_transformer_fn * res = t.get_plugin().mk_select_equal_and_project_fn(t, value, col);
TRACE("dl", tout << t.get_plugin().get_name() << " " << value << " " << col << "\n";);
if(!res) {
relation_mutator_fn * selector = mk_filter_equal_fn(t, value, col);
if(selector) {

2
src/muz_qe/dl_relation_manager.h
View file

@ -605,7 +605,7 @@ namespace datalog {
/**
This is a helper class for relation_plugins whose relations can be of various kinds.
*/
template<class Spec, class Hash=int_vector_hash_proc<Spec>, class Eq=vector_eq_proc<Spec> >
template<class Spec, class Hash, class Eq=vector_eq_proc<Spec> >
class rel_spec_store {
typedef relation_signature::hash r_hash;
typedef relation_signature::eq r_eq;

179
src/muz_qe/dl_rule.cpp
View file

@ -40,15 +40,20 @@ Revision History:
#include"quant_hoist.h"
#include"expr_replacer.h"
#include"bool_rewriter.h"
#include"qe_lite.h"
#include"expr_safe_replace.h"
#include"hnf.h"
namespace datalog {
rule_manager::rule_manager(context& ctx)
: m(ctx.get_manager()),
m_ctx(ctx) {}
m_ctx(ctx),
m_body(m),
m_head(m),
m_args(m),
m_hnf(m),
m_qe(m),
m_cfg(m),
m_rwr(m, false, m_cfg) {}
void rule_manager::inc_ref(rule * r) {
if (r) {
@ -67,29 +72,23 @@ namespace datalog {
}
}
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg() {}
rule_manager::remove_label_cfg::~remove_label_cfg() {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (is_decl_of(f, m_label_fid, OP_LABEL)) {
SASSERT(num == 1);
result = args[0];
return BR_DONE;
}
return BR_FAILED;
br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (is_decl_of(f, m_label_fid, OP_LABEL)) {
SASSERT(num == 1);
result = args[0];
return BR_DONE;
}
};
return BR_FAILED;
}
void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
expr_ref tmp(m);
remove_label_cfg r_cfg(m);
rewriter_tpl<remove_label_cfg> rwr(m, false, r_cfg);
rwr(fml, tmp);
m_rwr(fml, tmp);
if (pr && fml != tmp) {
pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
@ -97,6 +96,67 @@ namespace datalog {
fml = tmp;
}
var_idx_set& rule_manager::collect_vars(expr* e) {
return collect_vars(e, 0);
}
var_idx_set& rule_manager::collect_vars(expr* e1, expr* e2) {
reset_collect_vars();
if (e1) accumulate_vars(e1);
if (e2) accumulate_vars(e2);
return finalize_collect_vars();
}
void rule_manager::reset_collect_vars() {
m_vars.reset();
m_var_idx.reset();
m_todo.reset();
m_mark.reset();
}
var_idx_set& rule_manager::finalize_collect_vars() {
unsigned sz = m_vars.size();
for (unsigned i=0; i<sz; ++i) {
if (m_vars[i]) m_var_idx.insert(i);
}
return m_var_idx;
}
var_idx_set& rule_manager::collect_tail_vars(rule * r) {
reset_collect_vars();
unsigned n = r->get_tail_size();
for (unsigned i=0;i<n;i++) {
accumulate_vars(r->get_tail(i));
}
return finalize_collect_vars();
}
var_idx_set& rule_manager::collect_rule_vars_ex(rule * r, app* t) {
reset_collect_vars();
unsigned n = r->get_tail_size();
accumulate_vars(r->get_head());
for (unsigned i=0;i<n;i++) {
if (r->get_tail(i) != t) {
accumulate_vars(r->get_tail(i));
}
}
return finalize_collect_vars();
}
var_idx_set& rule_manager::collect_rule_vars(rule * r) {
reset_collect_vars();
unsigned n = r->get_tail_size();
accumulate_vars(r->get_head());
for (unsigned i=0;i<n;i++) {
accumulate_vars(r->get_tail(i));
}
return finalize_collect_vars();
}
void rule_manager::accumulate_vars(expr* e) {
::get_free_vars(m_mark, m_todo, e, m_vars);
}
void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
@ -125,13 +185,13 @@ namespace datalog {
}
void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) {
hnf h(m);
expr_ref_vector fmls(m);
proof_ref_vector prs(m);
h.set_name(name);
h(fml, p, fmls, prs);
for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) {
m_ctx.register_predicate(h.get_fresh_predicates()[i], false);
m_hnf.reset();
m_hnf.set_name(name);
m_hnf(fml, p, fmls, prs);
for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) {
m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false);
}
for (unsigned i = 0; i < fmls.size(); ++i) {
mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name);
@ -140,24 +200,23 @@ namespace datalog {
void rule_manager::mk_horn_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
app_ref_vector body(m);
app_ref head(m);
svector<bool> is_negated;
unsigned index = extract_horn(fml, body, head);
hoist_compound_predicates(index, head, body);
m_body.reset();
m_neg.reset();
unsigned index = extract_horn(fml, m_body, m_head);
hoist_compound_predicates(index, m_head, m_body);
TRACE("dl_rule",
tout << mk_pp(head, m) << " :- ";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << " ";
tout << mk_pp(m_head, m) << " :- ";
for (unsigned i = 0; i < m_body.size(); ++i) {
tout << mk_pp(m_body[i].get(), m) << " ";
}
tout << "\n";);
mk_negations(body, is_negated);
check_valid_rule(head, body.size(), body.c_ptr());
mk_negations(m_body, m_neg);
check_valid_rule(m_head, m_body.size(), m_body.c_ptr());
rule_ref r(*this);
r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name);
r = mk(m_head.get(), m_body.size(), m_body.c_ptr(), m_neg.c_ptr(), name);
expr_ref fml1(m);
if (p) {
@ -326,28 +385,28 @@ namespace datalog {
fml = m.mk_not(fml);
return;
}
expr_ref_vector args(m);
if (!m_ctx.is_predicate(fml)) {
return;
}
m_args.reset();
for (unsigned i = 0; i < fml->get_num_args(); ++i) {
e = fml->get_arg(i);
if (!is_app(e)) {
args.push_back(e);
m_args.push_back(e);
continue;
}
app* b = to_app(e);
if (m.is_value(b)) {
args.push_back(e);
m_args.push_back(e);
}
else {
var* v = m.mk_var(num_bound++, m.get_sort(b));
args.push_back(v);
m_args.push_back(v);
body.push_back(m.mk_eq(v, b));
}
}
fml = m.mk_app(fml->get_decl(), args.size(), args.c_ptr());
fml = m.mk_app(fml->get_decl(), m_args.size(), m_args.c_ptr());
TRACE("dl_rule", tout << mk_pp(fml.get(), m) << "\n";);
}
@ -511,29 +570,22 @@ namespace datalog {
void rule_manager::reduce_unbound_vars(rule_ref& r) {
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned t_len = r->get_tail_size();
ptr_vector<sort> vars;
uint_set index_set;
qe_lite qe(m);
expr_ref_vector conjs(m);
if (ut_len == t_len) {
return;
}
get_free_vars(r->get_head(), vars);
reset_collect_vars();
accumulate_vars(r->get_head());
for (unsigned i = 0; i < ut_len; ++i) {
get_free_vars(r->get_tail(i), vars);
accumulate_vars(r->get_tail(i));
}
var_idx_set& index_set = finalize_collect_vars();
for (unsigned i = ut_len; i < t_len; ++i) {
conjs.push_back(r->get_tail(i));
}
for (unsigned i = 0; i < vars.size(); ++i) {
if (vars[i]) {
index_set.insert(i);
}
}
qe(index_set, false, conjs);
m_qe(index_set, false, conjs);
bool change = conjs.size() != t_len - ut_len;
for (unsigned i = 0; !change && i < conjs.size(); ++i) {
change = r->get_tail(ut_len+i) != conjs[i].get();
@ -570,15 +622,14 @@ namespace datalog {
return;
}
ptr_vector<sort> free_rule_vars;
var_counter vctr;
app_ref_vector tail(m);
svector<bool> tail_neg;
app_ref head(r->get_head(), m);
get_free_vars(r, free_rule_vars);
collect_rule_vars(r);
vctr.count_vars(m, head);
ptr_vector<sort>& free_rule_vars = m_vars;
for (unsigned i = 0; i < ut_len; i++) {
app * t = r->get_tail(i);
@ -906,7 +957,7 @@ namespace datalog {
}
void rule::norm_vars(rule_manager & rm) {
used_vars used;
used_vars& used = rm.reset_used();
get_used_vars(used);
unsigned first_unsused = used.get_max_found_var_idx_plus_1();
@ -1004,16 +1055,14 @@ namespace datalog {
}
svector<symbol> names;
used_symbols<> us;
us(fml);
sorts.reverse();
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
}
us(fml);
sorts.reverse();
for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
func_decl_ref f(m);
@ -1067,6 +1116,8 @@ namespace datalog {
}
};
template class rewriter_tpl<datalog::rule_manager::remove_label_cfg>;

49
src/muz_qe/dl_rule.h
View file

@ -27,6 +27,9 @@ Revision History:
#include"proof_converter.h"
#include"model_converter.h"
#include"ast_counter.h"
#include"rewriter.h"
#include"hnf.h"
#include"qe_lite.h"
namespace datalog {
@ -47,9 +50,33 @@ namespace datalog {
*/
class rule_manager
{
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg();
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr);
};
ast_manager& m;
context& m_ctx;
rule_counter m_counter;
used_vars m_used;
ptr_vector<sort> m_vars;
var_idx_set m_var_idx;
ptr_vector<expr> m_todo;
ast_mark m_mark;
app_ref_vector m_body;
app_ref m_head;
expr_ref_vector m_args;
svector<bool> m_neg;
hnf m_hnf;
qe_lite m_qe;
remove_label_cfg m_cfg;
rewriter_tpl<remove_label_cfg> m_rwr;
// only the context can create a rule_manager
friend class context;
@ -90,6 +117,10 @@ namespace datalog {
*/
void reduce_unbound_vars(rule_ref& r);
void reset_collect_vars();
var_idx_set& finalize_collect_vars();
public:
ast_manager& get_manager() const { return m; }
@ -98,6 +129,24 @@ namespace datalog {
void dec_ref(rule * r);
used_vars& reset_used() { m_used.reset(); return m_used; }
var_idx_set& collect_vars(expr * pred);
var_idx_set& collect_vars(expr * e1, expr* e2);
var_idx_set& collect_rule_vars(rule * r);
var_idx_set& collect_rule_vars_ex(rule * r, app* t);
var_idx_set& collect_tail_vars(rule * r);
void accumulate_vars(expr* pred);
ptr_vector<sort>& get_var_sorts() { return m_vars; }
var_idx_set& get_var_idx() { return m_var_idx; }
/**
\brief Create a Datalog rule from a Horn formula.
The formula is of the form (forall (...) (forall (...) (=> (and ...) head)))

7
src/muz_qe/dl_rule_set.cpp
View file

@ -409,9 +409,10 @@ namespace datalog {
}
void rule_set::reopen() {
SASSERT(is_closed());
m_stratifier = 0;
m_deps.reset();
if (is_closed()) {
m_stratifier = 0;
m_deps.reset();
}
}
/**

3
src/muz_qe/dl_sieve_relation.cpp
View file

@ -567,8 +567,7 @@ namespace datalog {
const relation_signature sig = r.get_signature();
unsigned sz = sig.size();
var_idx_set cond_vars;
collect_vars(m, condition, cond_vars);
var_idx_set& cond_vars = get_context().get_rule_manager().collect_vars(condition);
expr_ref_vector subst_vect(m);
subst_vect.resize(sz);
unsigned subst_ofs = sz-1;

2
src/muz_qe/dl_sieve_relation.h
View file

@ -52,7 +52,7 @@ namespace datalog {
struct hash {
unsigned operator()(const rel_spec & s) const {
return int_vector_hash(s.m_inner_cols)^s.m_inner_kind;
return svector_hash<bool_hash>()(s.m_inner_cols)^s.m_inner_kind;
}
};
};

2
src/muz_qe/dl_sparse_table.h
View file

@ -359,7 +359,7 @@ namespace datalog {
typedef svector<unsigned> key_spec; //sequence of columns in a key
typedef svector<table_element> key_value; //values of key columns
typedef map<key_spec, key_indexer*, int_vector_hash_proc<key_spec>,
typedef map<key_spec, key_indexer*, svector_hash_proc<unsigned_hash>,
vector_eq_proc<key_spec> > key_index_map;
static const store_offset NO_RESERVE = UINT_MAX;

2
src/muz_qe/dl_table.h
View file

@ -73,7 +73,7 @@ namespace datalog {
class our_iterator_core;
typedef hashtable<table_fact, int_vector_hash_proc<table_fact>,
typedef hashtable<table_fact, svector_hash_proc<table_element_hash>,
vector_eq_proc<table_fact> > storage;
storage m_data;

50
src/muz_qe/dl_util.cpp
View file

@ -158,36 +158,7 @@ namespace datalog {
::get_free_vars(trm, vars);
return var_idx < vars.size() && vars[var_idx] != 0;
}
void collect_vars(ast_manager & m, expr * e, var_idx_set & result) {
ptr_vector<sort> vars;
::get_free_vars(e, vars);
unsigned sz = vars.size();
for(unsigned i=0; i<sz; ++i) {
if(vars[i]) { result.insert(i); }
}
}
void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result) {
unsigned n = r->get_tail_size();
for(unsigned i=0;i<n;i++) {
collect_vars(m, r->get_tail(i), result);
}
}
void get_free_tail_vars(rule * r, ptr_vector<sort>& sorts) {
unsigned n = r->get_tail_size();
for(unsigned i=0;i<n;i++) {
get_free_vars(r->get_tail(i), sorts);
}
}
void get_free_vars(rule * r, ptr_vector<sort>& sorts) {
get_free_vars(r->get_head(), sorts);
get_free_tail_vars(r, sorts);
}
unsigned count_variable_arguments(app * pred)
{
SASSERT(is_uninterp(pred));
@ -202,26 +173,6 @@ namespace datalog {
return res;
}
void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result) {
collect_vars(m, r->get_head(), result);
unsigned sz = r->get_tail_size();
for (unsigned i = 0; i < sz; i++) {
app * curr = r->get_tail(i);
if (curr != t)
collect_vars(m, curr, result);
}
}
void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result) {
collect_vars(m, r->get_head(), result);
unsigned sz = r->get_tail_size();
for (unsigned i = 0; i < sz; i++) {
app * curr = r->get_tail(i);
if (curr != t_1 && curr != t_2)
collect_vars(m, curr, result);
}
}
void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var,
sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) {
expr_ref_buffer new_args(m);
@ -404,6 +355,7 @@ namespace datalog {
void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
reset();
count_vars(m, r->get_head(), 1);
unsigned n = r->get_tail_size();
for (unsigned i = 0; i < n; i++) {

52
src/muz_qe/dl_util.h
View file

@ -54,6 +54,7 @@ namespace datalog {
BMC_ENGINE,
QBMC_ENGINE,
TAB_ENGINE,
CLP_ENGINE,
LAST_ENGINE
};
@ -81,33 +82,13 @@ namespace datalog {
void flatten_or(expr* fml, expr_ref_vector& result);
bool contains_var(expr * trm, unsigned var_idx);
/**
\brief Collect the variables in \c pred.
\pre \c pred must be a valid head or tail.
*/
void collect_vars(ast_manager & m, expr * pred, var_idx_set & result);
void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result);
void get_free_vars(rule * r, ptr_vector<sort>& sorts);
/**
\brief Return number of arguments of \c pred that are variables
*/
unsigned count_variable_arguments(app * pred);
/**
\brief Store in \c result the set of variables used by \c r when ignoring the tail \c t.
*/
void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result);
/**
\brief Store in \c result the set of variables used by \c r when ignoring the tail elements \c t_1 and \c t_2.
*/
void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result);
template<typename T>
void copy_nonvariables(app * src, T& tgt)
@ -207,7 +188,9 @@ namespace datalog {
static unsigned expr_cont_get_size(app * a) { return a->get_num_args(); }
static expr * expr_cont_get(app * a, unsigned i) { return a->get_arg(i); }
static unsigned expr_cont_get_size(const ptr_vector<expr> & v) { return v.size(); }
static unsigned expr_cont_get_size(const expr_ref_vector & v) { return v.size(); }
static expr * expr_cont_get(const ptr_vector<expr> & v, unsigned i) { return v[i]; }
static expr * expr_cont_get(const expr_ref_vector & v, unsigned i) { return v[i]; }
public:
variable_intersection(ast_manager & m) : m_consts(m) {}
@ -585,17 +568,31 @@ namespace datalog {
}
template<class T>
unsigned int_vector_hash(const T & cont) {
return string_hash(reinterpret_cast<const char *>(cont.c_ptr()),
cont.size()*sizeof(typename T::data), 0);
struct default_obj_chash {
unsigned operator()(T const& cont, unsigned i) const {
return cont[i]->hash();
}
};
template<class T>
unsigned obj_vector_hash(const T & cont) {
return get_composite_hash(cont, cont.size(),default_kind_hash_proc<T>(), default_obj_chash<T>());
}
template<class T>
struct int_vector_hash_proc {
struct obj_vector_hash_proc {
unsigned operator()(const T & cont) const {
return int_vector_hash(cont);
return obj_vector_hash(cont);
}
};
template<class T>
struct svector_hash_proc {
unsigned operator()(const svector<typename T::data> & cont) const {
return svector_hash<T>()(cont);
}
};
template<class T>
struct vector_eq_proc {
bool operator()(const T & c1, const T & c2) const { return vectors_equal(c1, c2); }
@ -763,11 +760,6 @@ namespace datalog {
//
// -----------------------------------
struct uint64_hash {
typedef uint64 data;
unsigned operator()(uint64 x) const { return hash_ull(x); }
};
template<class T>
void universal_delete(T* ptr) {
dealloc(ptr);

2
src/muz_qe/fixedpoint_params.pyg
View file

@ -13,7 +13,6 @@ def_module_params('fixedpoint',
('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"),
('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"),
('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),
('filter_rules', BOOL, True, "(DATALOG) apply filter compression on rules"),
('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"),
('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"),
('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"),
@ -61,6 +60,7 @@ def_module_params('fixedpoint',
('print_answer', BOOL, False, 'print answer instance(s) to query'),
('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
('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'),
))

34
src/muz_qe/hnf.cpp
View file

@ -71,6 +71,9 @@ class hnf::imp {
obj_map<expr, app*> m_memoize_disj;
obj_map<expr, proof*> m_memoize_proof;
func_decl_ref_vector m_fresh_predicates;
expr_ref_vector m_body;
proof_ref_vector m_defs;
public:
imp(ast_manager & m):
@ -82,7 +85,9 @@ public:
m_refs(m),
m_name("P"),
m_qh(m),
m_fresh_predicates(m) {
m_fresh_predicates(m),
m_body(m),
m_defs(m) {
}
void operator()(expr * n,
@ -181,14 +186,15 @@ private:
void mk_horn(expr_ref& fml, proof_ref& premise) {
SASSERT(!premise || fml == m.get_fact(premise));
expr* e1, *e2;
expr_ref_vector body(m);
proof_ref_vector defs(m);
expr_ref fml0(m), fml1(m), fml2(m), head(m);
proof_ref p(m);
fml0 = fml;
m_names.reset();
m_sorts.reset();
m_body.reset();
m_defs.reset();
m_qh.pull_quantifier(true, fml0, &m_sorts, &m_names);
if (premise){
fml1 = bind_variables(fml0);
@ -199,12 +205,12 @@ private:
}
head = fml0;
while (m.is_implies(head, e1, e2)) {
body.push_back(e1);
m_body.push_back(e1);
head = e2;
}
datalog::flatten_and(body);
datalog::flatten_and(m_body);
if (premise) {
p = m.mk_rewrite(fml0, mk_implies(body, head));
p = m.mk_rewrite(fml0, mk_implies(m_body, head));
}
//
@ -214,8 +220,8 @@ private:
// A -> C
// B -> C
//
if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
app* _or = to_app(body[0].get());
if (m_body.size() == 1 && m.is_or(m_body[0].get()) && contains_predicate(m_body[0].get())) {
app* _or = to_app(m_body[0].get());
unsigned sz = _or->get_num_args();
expr* const* args = _or->get_args();
for (unsigned i = 0; i < sz; ++i) {
@ -224,7 +230,7 @@ private:
}
if (premise) {
expr_ref f1 = bind_variables(mk_implies(body, head));
expr_ref f1 = bind_variables(mk_implies(m_body, head));
expr* f2 = m.mk_and(sz, m_todo.c_ptr()+m_todo.size()-sz);
proof_ref p2(m), p3(m);
p2 = m.mk_def_axiom(m.mk_iff(f1, f2));
@ -240,13 +246,13 @@ private:
}
eliminate_disjunctions(body, defs);
p = mk_congruence(p, body, head, defs);
eliminate_disjunctions(m_body, m_defs);
p = mk_congruence(p, m_body, head, m_defs);
eliminate_quantifier_body(body, defs);
p = mk_congruence(p, body, head, defs);
eliminate_quantifier_body(m_body, m_defs);
p = mk_congruence(p, m_body, head, m_defs);
fml2 = mk_implies(body, head);
fml2 = mk_implies(m_body, head);
fml = bind_variables(fml2);

17
src/muz_qe/horn_subsume_model_converter.cpp
View file

@ -28,10 +28,8 @@ Revision History:
#include "well_sorted.h"
void horn_subsume_model_converter::insert(app* head, expr* body) {
func_decl_ref pred(m);
expr_ref body_res(m);
VERIFY(mk_horn(head, body, pred, body_res));
insert(pred.get(), body_res.get());
m_delay_head.push_back(head);
m_delay_body.push_back(body);
}
void horn_subsume_model_converter::insert(app* head, unsigned sz, expr* const* body) {
@ -148,6 +146,7 @@ bool horn_subsume_model_converter::mk_horn(
}
void horn_subsume_model_converter::add_default_proc::operator()(app* n) {
//
// predicates that have not been assigned values
// in the Horn model are assumed false.
@ -174,6 +173,16 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
void horn_subsume_model_converter::operator()(model_ref& mr) {
func_decl_ref pred(m);
expr_ref body_res(m);
for (unsigned i = 0; i < m_delay_head.size(); ++i) {
VERIFY(mk_horn(m_delay_head[i].get(), m_delay_body[i].get(), pred, body_res));
insert(pred.get(), body_res.get());
}
m_delay_head.reset();
m_delay_body.reset();
TRACE("mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
for (unsigned i = m_funcs.size(); i > 0; ) {
--i;

6
src/muz_qe/horn_subsume_model_converter.h
View file

@ -43,6 +43,8 @@ class horn_subsume_model_converter : public model_converter {
func_decl_ref_vector m_funcs;
expr_ref_vector m_bodies;
th_rewriter m_rewrite;
app_ref_vector m_delay_head;
expr_ref_vector m_delay_body;
void add_default_false_interpretation(expr* e, model_ref& md);
@ -56,7 +58,9 @@ class horn_subsume_model_converter : public model_converter {
public:
horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m), m_rewrite(m) {}
horn_subsume_model_converter(ast_manager& m):
m(m), m_funcs(m), m_bodies(m), m_rewrite(m),
m_delay_head(m), m_delay_body(m) {}
bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body);

16
src/muz_qe/horn_tactic.cpp
View file

@ -125,12 +125,13 @@ class horn_tactic : public tactic {
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
formula_kind get_formula_kind(expr_ref& f) {
normalize(f);
expr_ref tmp(f);
normalize(tmp);
ast_mark mark;
expr_ref_vector args(m), body(m);
expr_ref head(m);
expr* a = 0, *a1 = 0;
datalog::flatten_or(f, args);
datalog::flatten_or(tmp, args);
for (unsigned i = 0; i < args.size(); ++i) {
a = args[i].get();
check_predicate(mark, a);
@ -147,12 +148,12 @@ class horn_tactic : public tactic {
body.push_back(m.mk_not(a));
}
}
f = m.mk_and(body.size(), body.c_ptr());
if (head) {
f = m.mk_implies(f, head);
// f = m.mk_implies(f, head);
return IS_RULE;
}
else {
f = m.mk_and(body.size(), body.c_ptr());
return IS_QUERY;
}
}
@ -171,7 +172,7 @@ class horn_tactic : public tactic {
tactic_report report("horn", *g);
bool produce_proofs = g->proofs_enabled();
if (produce_proofs) {
if (produce_proofs) {
if (!m_ctx.get_params().generate_proof_trace()) {
params_ref params = m_ctx.get_params().p;
params.set_bool("generate_proof_trace", true);
@ -239,10 +240,13 @@ class horn_tactic : public tactic {
switch (is_reachable) {
case l_true: {
// goal is unsat
g->assert_expr(m.mk_false());
if (produce_proofs) {
proof_ref proof = m_ctx.get_proof();
pc = proof2proof_converter(m, proof);
g->assert_expr(m.mk_false(), proof, 0);
}
else {
g->assert_expr(m.mk_false());
}
break;
}

29
src/muz_qe/pdr_context.cpp
View file

@ -43,6 +43,7 @@ Notes:
#include "ast_ll_pp.h"
#include "proof_checker.h"
#include "smt_value_sort.h"
#include "proof_utils.h"
namespace pdr {
@ -275,7 +276,7 @@ namespace pdr {
src.pop_back();
}
else if (is_invariant(tgt_level, curr, false, assumes_level)) {
add_property(curr, assumes_level?tgt_level:infty_level);
TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);
src[i] = src.back();
@ -596,7 +597,7 @@ namespace pdr {
expr_ref fml = pm.mk_and(conj);
th_rewriter rw(m);
rw(fml);
if (ctx.is_dl()) {
if (ctx.is_dl() || ctx.is_utvpi()) {
hoist_non_bool_if(fml);
}
TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
@ -1225,6 +1226,7 @@ namespace pdr {
m_search(m_params.bfs_model_search()),
m_last_result(l_undef),
m_inductive_lvl(0),
m_expanded_lvl(0),
m_cancel(false)
{
}
@ -1357,9 +1359,10 @@ namespace pdr {
bool m_is_bool_arith;
bool m_has_arith;
bool m_is_dl;
bool m_is_utvpi;
public:
classifier_proc(ast_manager& m, datalog::rule_set& rules):
m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false) {
m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false), m_is_utvpi(false) {
classify(rules);
}
void operator()(expr* e) {
@ -1405,6 +1408,7 @@ namespace pdr {
bool is_dl() const { return m_is_dl; }
bool is_utvpi() const { return m_is_utvpi; }
private:
@ -1425,6 +1429,7 @@ namespace pdr {
mark.reset();
m_is_dl = false;
m_is_utvpi = false;
if (m_has_arith) {
ptr_vector<expr> forms;
for (it = rules.begin(); it != end; ++it) {
@ -1436,6 +1441,7 @@ namespace pdr {
}
}
m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr());
m_is_utvpi = m_is_dl || is_utvpi_logic(m, forms.size(), forms.c_ptr());
}
}
@ -1555,7 +1561,12 @@ namespace pdr {
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
m_fparams.m_arith_eager_eq_axioms = false;
if (classify.is_dl()) {
if (classify.is_utvpi() && m_params.use_utvpi()) {
IF_VERBOSE(1, verbose_stream() << "UTVPI\n";);
m_fparams.m_arith_mode = AS_UTVPI;
m_fparams.m_arith_expand_eqs = true;
}
else if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
}
@ -1680,6 +1691,9 @@ namespace pdr {
proof = m_search.get_proof_trace(*this);
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
apply(m, m_pc.get(), proof);
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
// proof_utils::push_instantiations_up(proof);
// TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
return proof;
}
@ -1711,6 +1725,7 @@ namespace pdr {
bool reachable;
while (true) {
checkpoint();
m_expanded_lvl = lvl;
reachable = check_reachability(lvl);
if (reachable) {
throw model_exception();
@ -1769,6 +1784,10 @@ namespace pdr {
void context::expand_node(model_node& n) {
SASSERT(n.is_open());
expr_ref_vector cube(m);
if (n.level() < m_expanded_lvl) {
m_expanded_lvl = n.level();
}
if (n.pt().is_reachable(n.state())) {
TRACE("pdr", tout << "reachable\n";);
@ -1835,7 +1854,7 @@ namespace pdr {
if (m_params.simplify_formulas_pre()) {
simplify_formulas();
}
for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) {
checkpoint();
bool all_propagated = true;
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();

3
src/muz_qe/pdr_context.h
View file

@ -303,6 +303,7 @@ namespace pdr {
mutable model_search m_search;
lbool m_last_result;
unsigned m_inductive_lvl;
unsigned m_expanded_lvl;
ptr_vector<core_generalizer> m_core_generalizers;
stats m_stats;
volatile bool m_cancel;
@ -366,7 +367,7 @@ namespace pdr {
expr_ref get_answer();
bool is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; }
bool is_utvpi() const { return m_fparams.m_arith_mode == AS_UTVPI; }
void collect_statistics(statistics& st) const;
void reset_statistics();

3
src/muz_qe/pdr_farkas_learner.cpp
View file

@ -216,6 +216,9 @@ namespace pdr {
}
res = m.mk_not(res);
th_rewriter rw(m);
params_ref params;
params.set_bool("gcd_rounding", true);
rw.updt_params(params);
proof_ref pr(m);
expr_ref tmp(m);
rw(res, tmp, pr);

44
src/muz_qe/pdr_prop_solver.cpp
View file

@ -383,26 +383,32 @@ namespace pdr {
fl.get_lemmas(pr, bs, lemmas);
safe.elim_proxies(lemmas);
fl.simplify_lemmas(lemmas); // redundant?
if (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
!is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) {
IF_VERBOSE(1,
verbose_stream() << "not diff\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
});
extract_subset_core(safe);
return;
bool outside_of_logic =
(m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
!is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) ||
(m_fparams.m_arith_mode == AS_UTVPI &&
!is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr()));
if (outside_of_logic) {
IF_VERBOSE(2,
verbose_stream() << "not diff\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
});
extract_subset_core(safe);
}
else {
IF_VERBOSE(2,
verbose_stream() << "Lemmas\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
});
m_core->reset();
m_core->append(lemmas);
}
IF_VERBOSE(2,
verbose_stream() << "Lemmas\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
});
m_core->reset();
m_core->append(lemmas);
}
lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) {

36
src/muz_qe/pdr_util.cpp
View file

@ -1081,6 +1081,7 @@ namespace pdr {
arith_util a;
bv_util bv;
bool m_is_dl;
bool m_test_for_utvpi;
bool is_numeric(expr* e) const {
if (a.is_numeral(e)) {
@ -1115,6 +1116,16 @@ namespace pdr {
}
return false;
}
if (m_test_for_utvpi) {
if (a.is_mul(e, e1, e2)) {
if (is_minus_one(e1)) {
return is_offset(e2);
}
if (is_minus_one(e2)) {
return is_offset(e1);
}
}
}
return !is_arith_expr(e);
}
@ -1140,6 +1151,9 @@ namespace pdr {
if (!a.is_add(lhs, arg1, arg2))
return false;
// x
if (m_test_for_utvpi) {
return is_offset(arg1) && is_offset(arg2);
}
if (is_arith_expr(arg1))
std::swap(arg1, arg2);
if (is_arith_expr(arg1))
@ -1209,8 +1223,10 @@ namespace pdr {
}
public:
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {}
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
void test_for_utvpi() { m_test_for_utvpi = true; }
void operator()(expr* e) {
if (!m_is_dl) {
return;
@ -1232,7 +1248,11 @@ namespace pdr {
}
if (!m_is_dl) {
IF_VERBOSE(1, verbose_stream() << "non-diff: " << mk_pp(e, m) << "\n";);
char const* msg = "non-diff: ";
if (m_test_for_utvpi) {
msg = "non-utvpi: ";
}
IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";);
}
}
@ -1248,6 +1268,16 @@ namespace pdr {
return test.is_dl();
}
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
test_diff_logic test(m);
test.test_for_utvpi();
expr_fast_mark1 mark;
for (unsigned i = 0; i < num_fmls; ++i) {
quick_for_each_expr(test, mark, fmls[i]);
}
return test.is_dl();
}
}
template class rewriter_tpl<pdr::ite_hoister_cfg>;

2
src/muz_qe/pdr_util.h
View file

@ -151,6 +151,8 @@ namespace pdr {
bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
}
#endif

91
src/muz_qe/proof_utils.cpp
View file

@ -1,6 +1,7 @@
#include "dl_util.h"
#include "proof_utils.h"
#include "ast_smt2_pp.h"
#include "var_subst.h"
class reduce_hypotheses {
typedef obj_hashtable<expr> expr_set;
@ -517,3 +518,93 @@ void proof_utils::permute_unit_resolution(proof_ref& pr) {
obj_map<proof,proof*> cache;
::permute_unit_resolution(refs, cache, pr);
}
class push_instantiations_up_cl {
ast_manager& m;
public:
push_instantiations_up_cl(ast_manager& m): m(m) {}
void operator()(proof_ref& p) {
expr_ref_vector s0(m);
p = push(p, s0);
}
private:
proof* push(proof* p, expr_ref_vector const& sub) {
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned> > positions;
vector<expr_ref_vector> substs;
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
for (unsigned i = 0; i < premises.size(); ++i) {
compose(substs[i], sub);
premises[i] = push(premises[i].get(), substs[i]);
substs[i].reset();
}
instantiate(sub, conclusion);
return
m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion,
positions,
substs);
}
if (sub.empty()) {
return p;
}
if (m.is_modus_ponens(p)) {
SASSERT(m.get_num_parents(p) == 2);
proof* p0 = m.get_parent(p, 0);
proof* p1 = m.get_parent(p, 1);
if (m.get_fact(p0) == m.get_fact(p)) {
return push(p0, sub);
}
expr* e1, *e2;
if (m.is_rewrite(p1, e1, e2) &&
is_quantifier(e1) && is_quantifier(e2) &&
to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
expr_ref r1(e1,m), r2(e2,m);
instantiate(sub, r1);
instantiate(sub, r2);
p1 = m.mk_rewrite(r1, r2);
return m.mk_modus_ponens(push(p0, sub), p1);
}
}
premises.push_back(p);
substs.push_back(sub);
conclusion = m.get_fact(p);
instantiate(sub, conclusion);
return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
}
void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
for (unsigned i = 0; i < sub.size(); ++i) {
expr_ref e(m);
var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
sub[i] = e;
}
}
void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
if (sub.empty()) {
return;
}
if (!is_forall(fml)) {
return;
}
quantifier* q = to_quantifier(fml);
if (q->get_num_decls() != sub.size()) {
TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
tout << mk_pp(q, m) << "\n";
tout << sub.size() << "\n";);
return;
}
var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
}
};
void proof_utils::push_instantiations_up(proof_ref& pr) {
push_instantiations_up_cl push(pr.get_manager());
push(pr);
}

6
src/muz_qe/proof_utils.h
View file

@ -36,6 +36,12 @@ public:
*/
static void permute_unit_resolution(proof_ref& pr);
/**
\brief Push instantiations created in hyper-resolutions up to leaves.
This produces a "ground" proof where leaves are annotated by instantiations.
*/
static void push_instantiations_up(proof_ref& pr);
};
#endif

8
src/muz_qe/qe_lite.cpp
View file

@ -2525,15 +2525,15 @@ public:
m_params(p) {
m_imp = alloc(imp, m, p);
}
virtual tactic * translate(ast_manager & m) {
return alloc(qe_lite_tactic, m, m_params);
}
virtual ~qe_lite_tactic() {
dealloc(m_imp);
}
virtual tactic * translate(ast_manager & m) {
return alloc(qe_lite_tactic, m, m_params);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
// m_imp->updt_params(p);

13
src/muz_qe/rel_context.cpp
View file

@ -40,7 +40,9 @@ namespace datalog {
rule_set m_rules;
decl_set m_preds;
bool m_was_closed;
public:
scoped_query(context& ctx):
m_ctx(ctx),
m_rules(ctx.get_rules()),
@ -51,6 +53,7 @@ namespace datalog {
ctx.reopen();
}
}
~scoped_query() {
m_ctx.reopen();
m_ctx.restrict_predicates(m_preds);
@ -179,9 +182,7 @@ namespace datalog {
scoped_query.reset();
}
m_context.record_transformed_rules();
TRACE("dl", m_ectx.report_big_relations(100, tout););
m_code.process_all_costs();
m_code.make_annotations(m_ectx);
TRACE("dl", display_profile(tout););
return result;
}
@ -236,7 +237,6 @@ namespace datalog {
query_pred = rm.mk_query(query, m_context.get_rules());
}
catch (default_exception& exn) {
m_context.close();
m_context.set_status(INPUT_ERROR);
throw exn;
}
@ -480,7 +480,10 @@ namespace datalog {
get_rmanager().display(out);
}
void rel_context::display_profile(std::ostream& out) const {
void rel_context::display_profile(std::ostream& out) {
m_code.make_annotations(m_ectx);
m_code.process_all_costs();
out << "\n--------------\n";
out << "Instructions\n";
m_code.display(*this, out);

2
src/muz_qe/rel_context.h
View file

@ -105,7 +105,7 @@ namespace datalog {
void display_output_facts(rule_set const& rules, std::ostream & out) const;
void display_facts(std::ostream & out) const;
void display_profile(std::ostream& out) const;
void display_profile(std::ostream& out);
lbool saturate();

2
src/parsers/smt2/smt2parser.cpp
View file

@ -1159,7 +1159,7 @@ namespace smt2 {
m_num_expr_frames++;
unsigned num_vars = parse_sorted_vars();
if (num_vars == 0)
throw parser_exception("invalied quantifier, list of sorted variables is empty");
throw parser_exception("invalid quantifier, list of sorted variables is empty");
}
symbol parse_indexed_identifier_core() {

33
src/smt/diff_logic.h
View file

@ -118,7 +118,7 @@ const edge_id null_edge_id = -1;
template<typename Ext>
class dl_graph {
struct statistics {
struct stats {
unsigned m_propagation_cost;
unsigned m_implied_literal_cost;
unsigned m_num_implied_literals;
@ -131,16 +131,16 @@ class dl_graph {
m_num_helpful_implied_literals = 0;
m_num_relax = 0;
}
statistics() { reset(); }
void display(std::ostream& out) const {
out << "num. prop. steps. " << m_propagation_cost << "\n";
out << "num. impl. steps. " << m_implied_literal_cost << "\n";
out << "num. impl. lits. " << m_num_implied_literals << "\n";
out << "num. impl. conf lits. " << m_num_helpful_implied_literals << "\n";
out << "num. bound relax. " << m_num_relax << "\n";
stats() { reset(); }
void collect_statistics(::statistics& st) const {
st.update("dl prop steps", m_propagation_cost);
st.update("dl impl steps", m_implied_literal_cost);
st.update("dl impl lits", m_num_implied_literals);
st.update("dl impl conf lits", m_num_helpful_implied_literals);
st.update("dl bound relax", m_num_relax);
}
};
statistics m_stats;
stats m_stats;
typedef typename Ext::numeral numeral;
typedef typename Ext::explanation explanation;
typedef vector<numeral> assignment;
@ -264,7 +264,6 @@ class dl_graph {
m_assignment[e.get_target()] - m_assignment[e.get_source()] <= e.get_weight();
}
public:
// An assignment is feasible if all edges are feasible.
bool is_feasible() const {
@ -472,8 +471,9 @@ public:
m_bw(m_mark) {
}
void display_statistics(std::ostream& out) const {
m_stats.display(out);
void collect_statistics(::statistics& st) const {
m_stats.collect_statistics(st);
}
// Create/Initialize a variable with the given id.
@ -655,10 +655,8 @@ public:
throw default_exception("edges are not inconsistent");
}
#if 1
// experimental feature:
// allow theory to introduce shortcut lemmas.
prune_edges(edges, f);
#endif
for (unsigned i = 0; i < edges.size(); ++i) {
edge const& e = m_edges[edges[i]];
@ -752,7 +750,6 @@ public:
f.new_edge(src, dst, idx2-idx1+1, edges.begin()+idx1);
}
// Create a new scope.
// That is, save the number of edges in the graph.
void push() {
@ -1643,7 +1640,3 @@ public:
#endif /* _DIFF_LOGIC_H_ */
#if 0
#endif

4
src/smt/params/theory_arith_params.h
View file

@ -26,7 +26,9 @@ enum arith_solver_id {
AS_NO_ARITH,
AS_DIFF_LOGIC,
AS_ARITH,
AS_DENSE_DIFF_LOGIC
AS_DENSE_DIFF_LOGIC,
AS_UTVPI,
AS_HORN
};
enum bound_prop_mode {

14
src/smt/smt_setup.cpp
View file

@ -22,6 +22,8 @@ Revision History:
#include"theory_arith.h"
#include"theory_dense_diff_logic.h"
#include"theory_diff_logic.h"
#include"theory_horn_ineq.h"
#include"theory_utvpi.h"
#include"theory_array.h"
#include"theory_array_full.h"
#include"theory_bv.h"
@ -723,6 +725,18 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
}
break;
case AS_HORN:
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_ihi, m_manager));
else
m_context.register_plugin(alloc(smt::theory_rhi, m_manager));
break;
case AS_UTVPI:
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));
else
m_context.register_plugin(alloc(smt::theory_rutvpi, m_manager));
break;
default:
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));

133
src/smt/theory_diff_logic.h
View file

@ -46,7 +46,6 @@ namespace smt {
unsigned m_num_conflicts;
unsigned m_num_assertions;
unsigned m_num_th2core_eqs;
unsigned m_num_th2core_prop;
unsigned m_num_core2th_eqs;
unsigned m_num_core2th_diseqs;
@ -59,109 +58,30 @@ namespace smt {
}
};
class dl_conflict : public simple_justification {
public:
dl_conflict(region & r, unsigned nls, literal const * lits): simple_justification(r, nls, lits) { }
virtual proof * mk_proof(conflict_resolution & cr) {
NOT_IMPLEMENTED_YET();
return 0;
}
};
template<typename Ext>
class theory_diff_logic : public theory, private Ext {
typedef typename Ext::numeral numeral;
class implied_eq_justification : public justification {
theory_diff_logic & m_theory;
theory_var m_v1;
theory_var m_v2;
unsigned m_timestamp;
public:
implied_eq_justification(theory_diff_logic & theory, theory_var v1, theory_var v2, unsigned ts):
m_theory(theory),
m_v1(v1),
m_v2(v2),
m_timestamp(ts) {
}
virtual void get_antecedents(conflict_resolution & cr) {
m_theory.get_eq_antecedents(m_v1, m_v2, m_timestamp, cr);
}
virtual proof * mk_proof(conflict_resolution & cr) { NOT_IMPLEMENTED_YET(); return 0; }
};
class implied_bound_justification : public justification {
theory_diff_logic& m_theory;
edge_id m_subsumed_edge;
edge_id m_bridge_edge;
public:
implied_bound_justification(theory_diff_logic & theory, edge_id se, edge_id be):
m_theory(theory),
m_subsumed_edge(se),
m_bridge_edge(be) {
}
virtual void get_antecedents(conflict_resolution & cr) {
m_theory.get_implied_bound_antecedents(m_bridge_edge, m_subsumed_edge, cr);
}
virtual proof * mk_proof(conflict_resolution & cr) { NOT_IMPLEMENTED_YET(); return 0; }
};
enum atom_kind {
LE_ATOM,
EQ_ATOM
};
class atom {
protected:
atom_kind m_kind;
bool_var m_bvar;
bool m_true;
int m_pos;
int m_neg;
public:
atom(atom_kind k, bool_var bv) : m_kind(k), m_bvar(bv), m_true(false) {}
virtual ~atom() {}
atom_kind kind() const { return m_kind; }
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_true; }
void assign_eh(bool is_true) { m_true = is_true; }
virtual std::ostream& display(theory_diff_logic const& th, std::ostream& out) const;
};
class le_atom : public atom {
int m_pos;
int m_neg;
public:
le_atom(bool_var bv, int pos, int neg):
atom(LE_ATOM, bv),
atom(bool_var bv, int pos, int neg):
m_bvar(bv), m_true(false),
m_pos(pos),
m_neg(neg) {
}
virtual ~le_atom() {}
~atom() {}
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_true; }
void assign_eh(bool is_true) { m_true = is_true; }
int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
int get_pos() const { return m_pos; }
int get_neg() const { return m_neg; }
virtual std::ostream& display(theory_diff_logic const& th, std::ostream& out) const;
};
class eq_atom : public atom {
app_ref m_le;
app_ref m_ge;
public:
eq_atom(bool_var bv, app_ref& le, app_ref& ge):
atom(EQ_ATOM, bv),
m_le(le),
m_ge(ge)
{}
virtual ~eq_atom() {}
virtual std::ostream& display(theory_diff_logic const& th, std::ostream& out) const;
app* get_le() const { return m_le.get(); }
app* get_ge() const { return m_ge.get(); }
std::ostream& display(theory_diff_logic const& th, std::ostream& out) const;
};
typedef ptr_vector<atom> atoms;
@ -239,19 +159,7 @@ namespace smt {
unsigned m_asserted_qhead_old;
};
class theory_diff_logic_del_eh : public clause_del_eh {
theory_diff_logic& m_super;
public:
theory_diff_logic_del_eh(theory_diff_logic& s) : m_super(s) {}
virtual ~theory_diff_logic_del_eh() {}
virtual void operator()(ast_manager&, clause* cls) {
TRACE("dl_activity", tout << "deleting " << cls << "\n";);
m_super.del_clause_eh(cls);
dealloc(this);
}
};
smt_params & m_params;
smt_params & m_params;
arith_util m_util;
arith_eq_adapter m_arith_eq_adapter;
theory_diff_logic_statistics m_stats;
@ -259,8 +167,6 @@ namespace smt {
theory_var m_zero_int; // cache the variable representing the zero variable.
theory_var m_zero_real; // cache the variable representing the zero variable.
int_vector m_scc_id; // Cheap equality propagation
bool m_modified_since_eq_prop; // true if new constraints were asserted
// since last eq propagation.
eq_prop_info_set m_eq_prop_info_set; // set of existing equality prop infos
ptr_vector<eq_prop_info> m_eq_prop_infos;
@ -289,20 +195,14 @@ namespace smt {
virtual theory_var mk_var(enode* n);
virtual theory_var mk_var(app* n);
void mark_as_modified_since_eq_prop();
void unmark_as_modified_since_eq_prop();
bool propagate_cheap_equalities();
void compute_delta();
void found_non_diff_logic_expr(expr * n);
bool is_interpreted(app* n) const;
void del_clause_eh(clause* cls);
bool is_interpreted(app* n) const {
return get_family_id() == n->get_family_id();
}
public:
theory_diff_logic(ast_manager& m, smt_params & params):
@ -312,7 +212,6 @@ namespace smt {
m_arith_eq_adapter(*this, params, m_util),
m_zero_int(null_theory_var),
m_zero_real(null_theory_var),
m_modified_since_eq_prop(false),
m_asserted_qhead(0),
m_num_core_conflicts(0),
m_num_propagation_calls(0),
@ -323,7 +222,7 @@ namespace smt {
m_nc_functor(*this) {
}
~theory_diff_logic() {
virtual ~theory_diff_logic() {
reset_eh();
}
@ -360,7 +259,7 @@ namespace smt {
m_arith_eq_adapter.restart_eh();
}
virtual void relevant_eh(app* e);
virtual void relevant_eh(app* e) {}
virtual void init_search_eh() {
m_arith_eq_adapter.init_search_eh();

206
src/smt/theory_diff_logic_def.h
View file

@ -31,34 +31,15 @@ Revision History:
using namespace smt;
template<typename Ext>
std::ostream& theory_diff_logic<Ext>::atom::display(theory_diff_logic const& th, std::ostream& out) const {
std::ostream& theory_diff_logic<Ext>::atom::display(theory_diff_logic const& th, std::ostream& out) const {
context& ctx = th.get_context();
lbool asgn = ctx.get_assignment(m_bvar);
//SASSERT(asgn == l_undef || ((asgn == l_true) == m_true));
bool sign = (l_undef == asgn) || m_true;
return out << literal(m_bvar, sign)
<< " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " ";
}
template<typename Ext>
std::ostream& theory_diff_logic<Ext>::eq_atom::display(theory_diff_logic const& th, std::ostream& out) const {
atom::display(th, out);
lbool asgn = th.get_context().get_assignment(this->m_bvar);
if (l_undef == asgn) {
out << "unassigned\n";
}
else {
out << mk_pp(m_le.get(), m_le.get_manager()) << " "
<< mk_pp(m_ge.get(), m_ge.get_manager()) << "\n";
}
return out;
}
template<typename Ext>
std::ostream& theory_diff_logic<Ext>::le_atom::display(theory_diff_logic const& th, std::ostream& out) const {
atom::display(th, out);
lbool asgn = th.get_context().get_assignment(this->m_bvar);
if (l_undef == asgn) {
out << "unassigned\n";
}
@ -94,7 +75,6 @@ void theory_diff_logic<Ext>::init(context * ctx) {
e = ctx->mk_enode(zero, false, false, true);
SASSERT(!is_attached_to_var(e));
m_zero_real = mk_var(e);
}
@ -277,7 +257,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
k -= this->m_epsilon;
}
edge_id neg = m_graph.add_edge(target, source, k, ~l);
le_atom * a = alloc(le_atom, bv, pos, neg);
atom * a = alloc(atom, bv, pos, neg);
m_atoms.push_back(a);
m_bool_var2atom.insert(bv, a);
@ -318,7 +298,7 @@ template<typename Ext>
void theory_diff_logic<Ext>::assign_eh(bool_var v, bool is_true) {
m_stats.m_num_assertions++;
atom * a = 0;
m_bool_var2atom.find(v, a);
VERIFY (m_bool_var2atom.find(v, a));
SASSERT(a);
SASSERT(get_context().get_assignment(v) != l_undef);
SASSERT((get_context().get_assignment(v) == l_true) == is_true);
@ -330,10 +310,11 @@ void theory_diff_logic<Ext>::assign_eh(bool_var v, bool is_true) {
template<typename Ext>
void theory_diff_logic<Ext>::collect_statistics(::statistics & st) const {
st.update("dl conflicts", m_stats.m_num_conflicts);
st.update("dl propagations", m_stats.m_num_th2core_prop);
st.update("dl asserts", m_stats.m_num_assertions);
st.update("core->dl eqs", m_stats.m_num_core2th_eqs);
st.update("core->dl diseqs", m_stats.m_num_core2th_diseqs);
m_arith_eq_adapter.collect_statistics(st);
m_graph.collect_statistics(st);
}
template<typename Ext>
@ -374,15 +355,6 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
// either will already be zero (as we don't do mixed constraints).
m_graph.set_to_zero(m_zero_int, m_zero_real);
SASSERT(is_consistent());
#if 0
TBD:
if (propagate_cheap_equalities()) {
return FC_CONTINUE;
}
#endif
if (m_non_diff_logic_exprs) {
return FC_GIVEUP;
}
@ -506,61 +478,14 @@ bool theory_diff_logic<Ext>::propagate_atom(atom* a) {
if (ctx.inconsistent()) {
return false;
}
switch(a->kind()) {
case LE_ATOM: {
int edge_id = dynamic_cast<le_atom*>(a)->get_asserted_edge();
if (!m_graph.enable_edge(edge_id)) {
set_neg_cycle_conflict();
return false;
}
#if 0
if (m_params.m_arith_bound_prop != BP_NONE) {
svector<int> subsumed;
m_graph.find_subsumed1(edge_id, subsumed);
for (unsigned i = 0; i < subsumed.size(); ++i) {
int subsumed_edge_id = subsumed[i];
literal l = m_graph.get_explanation(subsumed_edge_id);
context & ctx = get_context();
region& r = ctx.get_region();
++m_stats.m_num_th2core_prop;
ctx.assign(l, new (r) implied_bound_justification(*this, subsumed_edge_id, edge_id));
}
}
#endif
break;
}
case EQ_ATOM:
if (!a->is_true()) {
SASSERT(ctx.get_assignment(a->get_bool_var()) == l_false);
// eq_atom * ea = dynamic_cast<eq_atom*>(a);
}
break;
int edge_id = a->get_asserted_edge();
if (!m_graph.enable_edge(edge_id)) {
set_neg_cycle_conflict();
return false;
}
return true;
}
template<typename Ext>
void theory_diff_logic<Ext>::mark_as_modified_since_eq_prop() {
if (!m_modified_since_eq_prop) {
get_context().push_trail(value_trail<context, bool>(m_modified_since_eq_prop));
m_modified_since_eq_prop = true;
}
}
template<typename Ext>
void theory_diff_logic<Ext>::unmark_as_modified_since_eq_prop() {
get_context().push_trail(value_trail<context, bool>(m_modified_since_eq_prop));
m_modified_since_eq_prop = false;
}
template<typename Ext>
void theory_diff_logic<Ext>::del_clause_eh(clause* cls) {
}
template<typename Ext>
void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {
@ -609,7 +534,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
atom* a = 0;
m_bool_var2atom.find(bv, a);
SASSERT(a);
edge_id e_id = static_cast<le_atom*>(a)->get_pos();
edge_id e_id = a->get_pos();
literal_vector lits;
for (unsigned i = 0; i < num_edges; ++i) {
@ -633,11 +558,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
lits.size(), lits.c_ptr(),
params.size(), params.c_ptr());
}
clause_del_eh* del_eh = alloc(theory_diff_logic_del_eh, *this);
clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, del_eh);
if (!cls) {
dealloc(del_eh);
}
clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
if (dump_lemmas()) {
char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA";
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
@ -677,7 +598,6 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
literal_vector const& lits = m_nc_functor.get_lits();
context & ctx = get_context();
TRACE("arith_conflict",
//display(tout);
tout << "conflict: ";
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.display_literal_info(tout, lits[i]);
@ -802,7 +722,6 @@ theory_var theory_diff_logic<Ext>::mk_num(app* n, rational const& r) {
template<typename Ext>
theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
mark_as_modified_since_eq_prop();
theory_var v = theory::mk_var(n);
TRACE("diff_logic_vars", tout << "mk_var: " << v << "\n";);
m_graph.init_var(v);
@ -810,10 +729,6 @@ theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
return v;
}
template<typename Ext>
bool theory_diff_logic<Ext>::is_interpreted(app* n) const {
return n->get_family_id() == get_family_id();
}
template<typename Ext>
theory_var theory_diff_logic<Ext>::mk_var(app* n) {
@ -854,7 +769,6 @@ void theory_diff_logic<Ext>::reset_eh() {
m_asserted_atoms .reset();
m_stats .reset();
m_scopes .reset();
m_modified_since_eq_prop = false;
m_asserted_qhead = 0;
m_num_core_conflicts = 0;
m_num_propagation_calls = 0;
@ -865,70 +779,6 @@ void theory_diff_logic<Ext>::reset_eh() {
}
template<typename Ext>
bool theory_diff_logic<Ext>::propagate_cheap_equalities() {
bool result = false;
TRACE("dl_new_eq", get_context().display(tout););
context& ctx = get_context();
region& reg = ctx.get_region();
SASSERT(m_eq_prop_info_set.empty());
SASSERT(m_eq_prop_infos.empty());
if (m_modified_since_eq_prop) {
m_graph.compute_zero_edge_scc(m_scc_id);
int n = get_num_vars();
for (theory_var v = 0; v < n; v++) {
rational delta_r;
theory_var x_v = expand(true, v, delta_r);
numeral delta(delta_r);
int scc_id = m_scc_id[x_v];
if (scc_id != -1) {
delta += m_graph.get_assignment(x_v);
TRACE("eq_scc", tout << v << " " << x_v << " " << scc_id << " " << delta << "\n";);
eq_prop_info info(scc_id, delta);
typename eq_prop_info_set::entry * entry = m_eq_prop_info_set.find_core(&info);
if (entry == 0) {
eq_prop_info * new_info = alloc(eq_prop_info, scc_id, delta, v);
m_eq_prop_info_set.insert(new_info);
m_eq_prop_infos.push_back(new_info);
}
else {
// new equality found
theory_var r = entry->get_data()->get_root();
enode * n1 = get_enode(v);
enode * n2 = get_enode(r);
if (n1->get_root() != n2->get_root()) {
// r may be an alias (i.e., it is not realy in the graph). So, I should expand it.
// nsb: ??
rational r_delta;
theory_var x_r = expand(true, r, r_delta);
justification* j = new (reg) implied_eq_justification(*this, x_v, x_r, m_graph.get_timestamp());
(void)j;
m_stats.m_num_th2core_eqs++;
// TBD: get equality into core.
NOT_IMPLEMENTED_YET();
// new_eq_eh(x_v, x_r, *j);
result = true;
}
}
}
}
m_eq_prop_info_set.reset();
std::for_each(m_eq_prop_infos.begin(), m_eq_prop_infos.end(), delete_proc<eq_prop_info>());
m_eq_prop_infos.reset();
unmark_as_modified_since_eq_prop();
}
TRACE("dl_new_eq", get_context().display(tout););
SASSERT(!m_modified_since_eq_prop);
return result;
}
template<typename Ext>
void theory_diff_logic<Ext>::compute_delta() {
m_delta = rational(1);
@ -1001,30 +851,9 @@ bool theory_diff_logic<Ext>::is_consistent() const {
lbool asgn = ctx.get_assignment(bv);
if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) {
SASSERT((asgn == l_true) == a->is_true());
switch(a->kind()) {
case LE_ATOM: {
le_atom* le = dynamic_cast<le_atom*>(a);
int edge_id = le->get_asserted_edge();
SASSERT(m_graph.is_enabled(edge_id));
SASSERT(m_graph.is_feasible(edge_id));
break;
}
case EQ_ATOM: {
eq_atom* ea = dynamic_cast<eq_atom*>(a);
bool_var bv1 = ctx.get_bool_var(ea->get_le());
bool_var bv2 = ctx.get_bool_var(ea->get_ge());
lbool val1 = ctx.get_assignment(bv1);
lbool val2 = ctx.get_assignment(bv2);
if (asgn == l_true) {
SASSERT(val1 == l_true);
SASSERT(val2 == l_true);
}
else {
SASSERT(val1 == l_false || val2 == l_false);
}
break;
}
}
int edge_id = a->get_asserted_edge();
SASSERT(m_graph.is_enabled(edge_id));
SASSERT(m_graph.is_feasible(edge_id));
}
}
return m_graph.is_feasible();
@ -1087,7 +916,6 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
// assign the corresponding equality literal.
//
mark_as_modified_since_eq_prop();
app_ref eq(m), s2(m), t2(m);
app* s1 = get_enode(s)->get_owner();
@ -1142,10 +970,6 @@ void theory_diff_logic<Ext>::new_diseq_eh(theory_var v1, theory_var v2) {
}
template<typename Ext>
void theory_diff_logic<Ext>::relevant_eh(app* e) {
}
struct imp_functor {
conflict_resolution & m_cr;

236
src/smt/theory_horn_ineq.cpp Normal file
View file

@ -0,0 +1,236 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_horn_ineq.h
Author:
Nikolaj Bjorner (nbjorner) 2013-04-18
Revision History:
The implementaton is derived from theory_diff_logic.
--*/
#include "theory_horn_ineq.h"
#include "theory_horn_ineq_def.h"
namespace smt {
template class theory_horn_ineq<ihi_ext>;
template class theory_horn_ineq<rhi_ext>;
// similar to test_diff_logic:
horn_ineq_tester::horn_ineq_tester(ast_manager& m): m(m), a(m) {}
bool horn_ineq_tester::operator()(expr* e) {
m_todo.reset();
m_pols.reset();
pos_mark.reset();
neg_mark.reset();
m_todo.push_back(e);
m_pols.push_back(l_true);
while (!m_todo.empty()) {
expr* e = m_todo.back();
lbool p = m_pols.back();
m_todo.pop_back();
m_pols.pop_back();
switch (p) {
case l_true:
if (pos_mark.is_marked(e)) {
continue;
}
pos_mark.mark(e, true);
break;
case l_false:
if (neg_mark.is_marked(e)) {
continue;
}
neg_mark.mark(e, true);
break;
case l_undef:
if (pos_mark.is_marked(e) && neg_mark.is_marked(e)) {
continue;
}
pos_mark.mark(e, true);
neg_mark.mark(e, true);
break;
}
if (!test_expr(p, e)) {
return false;
}
}
return true;
}
vector<std::pair<expr*,rational> > const& horn_ineq_tester::get_linearization() const {
return m_terms;
}
bool horn_ineq_tester::test_expr(lbool p, expr* e) {
expr* e1, *e2, *e3;
if (is_var(e)) {
return true;
}
if (!is_app(e)) {
return false;
}
app* ap = to_app(e);
if (m.is_and(ap) || m.is_or(ap)) {
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
m_todo.push_back(ap->get_arg(i));
m_pols.push_back(p);
}
}
else if (m.is_not(e, e1)) {
m_todo.push_back(e);
m_pols.push_back(~p);
}
else if (m.is_ite(e, e1, e2, e3)) {
m_todo.push_back(e1);
m_pols.push_back(l_undef);
m_todo.push_back(e2);
m_pols.push_back(p);
m_todo.push_back(e3);
m_pols.push_back(p);
}
else if (m.is_iff(e, e1, e2)) {
m_todo.push_back(e1);
m_pols.push_back(l_undef);
m_todo.push_back(e2);
m_pols.push_back(l_undef);
m_todo.push_back(e2);
}
else if (m.is_implies(e, e1, e2)) {
m_todo.push_back(e1);
m_pols.push_back(~p);
m_todo.push_back(e2);
m_pols.push_back(p);
}
else if (m.is_eq(e, e1, e2)) {
return linearize(e1, e2) == diff;
}
else if (m.is_true(e) || m.is_false(e)) {
// no-op
}
else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) ||
a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) {
if (p == l_false) {
std::swap(e2, e1);
}
classify_t cl = linearize(e1, e2);
switch(p) {
case l_undef:
return cl == diff;
case l_true:
case l_false:
return cl == horn || cl == diff;
}
}
else if (!is_uninterp_const(e)) {
return false;
}
return true;
}
bool horn_ineq_tester::operator()(unsigned num_fmls, expr* const* fmls) {
for (unsigned i = 0; i < num_fmls; ++i) {
if (!(*this)(fmls[i])) {
return false;
}
}
return true;
}
horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e) {
m_terms.reset();
m_terms.push_back(std::make_pair(e, rational(1)));
return linearize();
}
horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e1, expr* e2) {
m_terms.reset();
m_terms.push_back(std::make_pair(e1, rational(1)));
m_terms.push_back(std::make_pair(e2, rational(-1)));
return linearize();
}
horn_ineq_tester::classify_t horn_ineq_tester::linearize() {
m_weight.reset();
m_coeff_map.reset();
while (!m_terms.empty()) {
expr* e1, *e2;
rational num;
rational mul = m_terms.back().second;
expr* e = m_terms.back().first;
m_terms.pop_back();
if (a.is_add(e)) {
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul));
}
}
else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) {
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_sub(e, e1, e2)) {
m_terms.push_back(std::make_pair(e1, mul));
m_terms.push_back(std::make_pair(e2, -mul));
}
else if (a.is_uminus(e, e1)) {
m_terms.push_back(std::make_pair(e1, -mul));
}
else if (a.is_numeral(e, num)) {
m_weight += num*mul;
}
else if (a.is_to_real(e, e1)) {
m_terms.push_back(std::make_pair(e1, mul));
}
else if (!is_uninterp_const(e)) {
return non_horn;
}
else {
m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
}
}
unsigned num_negative = 0;
unsigned num_positive = 0;
bool is_unit_pos = true, is_unit_neg = true;
obj_map<expr, rational>::iterator it = m_coeff_map.begin();
obj_map<expr, rational>::iterator end = m_coeff_map.end();
for (; it != end; ++it) {
rational r = it->m_value;
if (r.is_zero()) {
continue;
}
m_terms.push_back(std::make_pair(it->m_key, r));
if (r.is_pos()) {
is_unit_pos = is_unit_pos && r.is_one();
num_positive++;
}
else {
is_unit_neg = is_unit_neg && r.is_minus_one();
num_negative++;
}
}
if (num_negative <= 1 && is_unit_pos && is_unit_neg && num_positive <= 1) {
return diff;
}
if (num_positive <= 1 && is_unit_pos) {
return horn;
}
if (num_negative <= 1 && is_unit_neg) {
return co_horn;
}
return non_horn;
}
}

329
src/smt/theory_horn_ineq.h Normal file
View file

@ -0,0 +1,329 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_horn_ineq.h
Abstract:
A*x <= weight + D*x, coefficients to A and D are non-negative,
D is a diagonal matrix.
Coefficients to weight may have both signs.
Label variables by weight.
Select inequality that is not satisfied.
Set delta(LHS) := 0
Set delta(RHS(x)) := weight(x) - b
Propagate weight increment through inequalities.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-18
Revision History:
The implementaton is derived from theory_diff_logic.
--*/
#ifndef _THEORY_HORN_INEQ_H_
#define _THEORY_HORN_INEQ_H_
#include"rational.h"
#include"inf_rational.h"
#include"inf_int_rational.h"
#include"inf_eps_rational.h"
#include"smt_theory.h"
#include"arith_decl_plugin.h"
#include"smt_justification.h"
#include"map.h"
#include"smt_params.h"
#include"arith_eq_adapter.h"
#include"smt_model_generator.h"
#include"numeral_factory.h"
#include"smt_clause.h"
namespace smt {
class horn_ineq_tester {
ast_manager& m;
arith_util a;
ptr_vector<expr> m_todo;
svector<lbool> m_pols;
ast_mark pos_mark, neg_mark;
obj_map<expr, rational> m_coeff_map;
rational m_weight;
vector<std::pair<expr*, rational> > m_terms;
public:
enum classify_t {
co_horn,
horn,
diff,
non_horn
};
horn_ineq_tester(ast_manager& m);
// test if formula is in the Horn inequality fragment:
bool operator()(expr* fml);
bool operator()(unsigned num_fmls, expr* const* fmls);
// linearize inequality/equality
classify_t linearize(expr* e);
classify_t linearize(expr* e1, expr* e2);
// retrieve linearization
vector<std::pair<expr*,rational> > const& get_linearization() const;
rational const& get_weight() const { return m_weight; }
private:
bool test_expr(lbool p, expr* e);
classify_t linearize();
};
template<typename Ext>
class theory_horn_ineq : public theory, private Ext {
typedef typename Ext::numeral numeral;
typedef typename Ext::inf_numeral inf_numeral;
typedef literal explanation;
typedef theory_var th_var;
typedef svector<th_var> th_var_vector;
typedef unsigned clause_id;
typedef vector<std::pair<th_var, rational> > coeffs;
static const clause_id null_clause_id = UINT_MAX;
class clause;
class graph;
class assignment_trail;
class parent_trail;
class atom {
protected:
bool_var m_bvar;
bool m_true;
int m_pos;
int m_neg;
public:
atom(bool_var bv, int pos, int neg) :
m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {}
virtual ~atom() {}
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_true; }
void assign_eh(bool is_true) { m_true = is_true; }
int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
int get_pos() const { return m_pos; }
int get_neg() const { return m_neg; }
std::ostream& display(theory_horn_ineq const& th, std::ostream& out) const;
};
typedef svector<atom> atoms;
struct scope {
unsigned m_atoms_lim;
unsigned m_asserted_atoms_lim;
unsigned m_asserted_qhead_old;
};
struct stats {
unsigned m_num_conflicts;
unsigned m_num_assertions;
unsigned m_num_core2th_eqs;
unsigned m_num_core2th_diseqs;
void reset() {
memset(this, 0, sizeof(*this));
}
stats() {
reset();
}
};
stats m_stats;
smt_params m_params;
arith_util a;
arith_eq_adapter m_arith_eq_adapter;
th_var m_zero_int; // cache the variable representing the zero variable.
th_var m_zero_real; // cache the variable representing the zero variable.
graph* m_graph;
atoms m_atoms;
unsigned_vector m_asserted_atoms; // set of asserted atoms
unsigned m_asserted_qhead;
u_map<unsigned> m_bool_var2atom;
svector<scope> m_scopes;
double m_agility;
bool m_lia;
bool m_lra;
bool m_non_horn_ineq_exprs;
horn_ineq_tester m_test;
arith_factory * m_factory;
rational m_delta;
rational m_lambda;
// Set a conflict due to a negative cycle.
void set_neg_cycle_conflict();
// Create a new theory variable.
virtual th_var mk_var(enode* n);
virtual th_var mk_var(expr* n);
void compute_delta();
void found_non_horn_ineq_expr(expr * n);
bool is_interpreted(app* n) const {
return n->get_family_id() == get_family_id();
}
public:
theory_horn_ineq(ast_manager& m);
virtual ~theory_horn_ineq();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_horn_ineq, get_manager()); }
virtual char const * get_name() const { return "horn-inequality-logic"; }
/**
\brief See comment in theory::mk_eq_atom
*/
virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); }
virtual void init(context * ctx);
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual void internalize_eq_eh(app * atom, bool_var v);
virtual void assign_eh(bool_var v, bool is_true);
virtual void new_eq_eh(th_var v1, th_var v2) {
m_arith_eq_adapter.new_eq_eh(v1, v2);
}
virtual bool use_diseqs() const { return true; }
virtual void new_diseq_eh(th_var v1, th_var v2) {
m_arith_eq_adapter.new_diseq_eh(v1, v2);
}
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void restart_eh() {
m_arith_eq_adapter.restart_eh();
}
virtual void relevant_eh(app* e) {}
virtual void init_search_eh() {
m_arith_eq_adapter.init_search_eh();
}
virtual final_check_status final_check_eh();
virtual bool is_shared(th_var v) const {
return false;
}
virtual bool can_propagate() {
SASSERT(m_asserted_qhead <= m_asserted_atoms.size());
return m_asserted_qhead != m_asserted_atoms.size();
}
virtual void propagate();
virtual justification * why_is_diseq(th_var v1, th_var v2) {
UNREACHABLE();
return 0;
}
virtual void reset_eh();
virtual void init_model(model_generator & m);
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const {
return true;
}
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
private:
virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_eqs++;
new_eq_or_diseq(true, v1, v2, j);
}
virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_diseqs++;
new_eq_or_diseq(false, v1, v2, j);
}
void negate(coeffs& coeffs, rational& weight);
numeral mk_weight(bool is_real, bool is_strict, rational const& w) const;
void mk_coeffs(vector<std::pair<expr*,rational> >const& terms, coeffs& coeffs, rational& w);
void del_atoms(unsigned old_size);
void propagate_core();
bool propagate_atom(atom const& a);
th_var mk_term(app* n);
th_var mk_num(app* n, rational const& r);
bool is_consistent() const;
th_var expand(bool pos, th_var v, rational & k);
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
void inc_conflicts();
};
struct rhi_ext {
typedef inf_rational inf_numeral;
typedef inf_eps_rational<inf_rational> numeral;
numeral m_epsilon;
numeral m_minus_infty;
rhi_ext() : m_epsilon(inf_rational(rational(), true)), m_minus_infty(rational(-1),inf_rational()) {}
};
struct ihi_ext {
typedef rational inf_numeral;
typedef inf_eps_rational<rational> numeral;
numeral m_epsilon;
numeral m_minus_infty;
ihi_ext() : m_epsilon(rational(1)), m_minus_infty(rational(-1),rational(0)) {}
};
typedef theory_horn_ineq<rhi_ext> theory_rhi;
typedef theory_horn_ineq<ihi_ext> theory_ihi;
};
#endif /* _THEORY_HORN_INEQ_H_ */

1164
src/smt/theory_horn_ineq_def.h Normal file
View file

File diff suppressed because it is too large Load diff

160
src/smt/theory_utvpi.cpp Normal file
View file

@ -0,0 +1,160 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_utvpi.h
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
The implementaton is derived from theory_diff_logic.
--*/
#include "theory_utvpi.h"
#include "theory_utvpi_def.h"
namespace smt {
template class theory_utvpi<idl_ext>;
template class theory_utvpi<rdl_ext>;
// similar to test_diff_logic:
utvpi_tester::utvpi_tester(ast_manager& m): m(m), a(m) {}
bool utvpi_tester::operator()(expr* e) {
m_todo.reset();
m_mark.reset();
m_todo.push_back(e);
expr* e1, *e2;
while (!m_todo.empty()) {
expr* e = m_todo.back();
m_todo.pop_back();
if (!m_mark.is_marked(e)) {
m_mark.mark(e, true);
if (is_var(e)) {
continue;
}
if (!is_app(e)) {
return false;
}
app* ap = to_app(e);
if (m.is_eq(ap, e1, e2)) {
if (!linearize(e1, e2)) {
return false;
}
}
else if (ap->get_family_id() == m.get_basic_family_id()) {
continue;
}
else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) ||
a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) {
if (!linearize(e1, e2)) {
return false;
}
}
else if (is_uninterp_const(e)) {
continue;
}
else {
return false;
}
}
}
return true;
}
vector<std::pair<expr*, rational> > const& utvpi_tester::get_linearization() const {
SASSERT(m_terms.size() <= 2);
return m_terms;
}
bool utvpi_tester::operator()(unsigned num_fmls, expr* const* fmls) {
for (unsigned i = 0; i < num_fmls; ++i) {
if (!(*this)(fmls[i])) {
return false;
}
}
return true;
}
bool utvpi_tester::linearize(expr* e) {
m_terms.reset();
m_terms.push_back(std::make_pair(e, rational(1)));
return linearize();
}
bool utvpi_tester::linearize(expr* e1, expr* e2) {
m_terms.reset();
m_terms.push_back(std::make_pair(e1, rational(1)));
m_terms.push_back(std::make_pair(e2, rational(-1)));
return linearize();
}
bool utvpi_tester::linearize() {
m_weight.reset();
m_coeff_map.reset();
while (!m_terms.empty()) {
expr* e1, *e2;
rational num;
rational mul = m_terms.back().second;
expr* e = m_terms.back().first;
m_terms.pop_back();
if (a.is_add(e)) {
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul));
}
}
else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) {
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_sub(e, e1, e2)) {
m_terms.push_back(std::make_pair(e1, mul));
m_terms.push_back(std::make_pair(e2, -mul));
}
else if (a.is_uminus(e, e1)) {
m_terms.push_back(std::make_pair(e1, -mul));
}
else if (a.is_numeral(e, num)) {
m_weight += num*mul;
}
else if (a.is_to_real(e, e1)) {
m_terms.push_back(std::make_pair(e1, mul));
}
else if (!is_uninterp_const(e)) {
return false;
}
else {
m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
}
}
obj_map<expr, rational>::iterator it = m_coeff_map.begin();
obj_map<expr, rational>::iterator end = m_coeff_map.end();
for (; it != end; ++it) {
rational r = it->m_value;
if (r.is_zero()) {
continue;
}
m_terms.push_back(std::make_pair(it->m_key, r));
if (m_terms.size() > 2) {
return false;
}
if (!r.is_one() && !r.is_minus_one()) {
return false;
}
}
return true;
}
}

336
src/smt/theory_utvpi.h Normal file
View file

@ -0,0 +1,336 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_utvpi.h
Abstract:
use Bellman Ford traversal algorithm for UTVPI.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
The implementaton is derived from theory_diff_logic.
--*/
#ifndef _THEORY_UTVPI_H_
#define _THEORY_UTVPI_H_
#include"theory_diff_logic.h"
namespace smt {
class utvpi_tester {
ast_manager& m;
arith_util a;
ptr_vector<expr> m_todo;
ast_mark m_mark;
obj_map<expr, rational> m_coeff_map;
rational m_weight;
vector<std::pair<expr*, rational> > m_terms;
public:
utvpi_tester(ast_manager& m);
// test if formula is in the Horn inequality fragment:
bool operator()(expr* fml);
bool operator()(unsigned num_fmls, expr* const* fmls);
// linearize inequality/equality
bool linearize(expr* e);
bool linearize(expr* e1, expr* e2);
// retrieve linearization
vector<std::pair<expr*, rational> > const& get_linearization() const;
rational const& get_weight() const { return m_weight; }
private:
bool linearize();
};
template<typename Ext>
class theory_utvpi : public theory, private Ext {
typedef typename Ext::numeral numeral;
typedef theory_var th_var;
typedef svector<th_var> th_var_vector;
typedef vector<std::pair<th_var, rational> > coeffs;
class assignment_trail;
class parent_trail;
struct GExt : public Ext {
typedef literal explanation;
};
class atom {
protected:
bool_var m_bvar;
bool m_true;
int m_pos;
int m_neg;
public:
atom(bool_var bv, int pos, int neg) :
m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {}
virtual ~atom() {}
bool_var get_bool_var() const { return m_bvar; }
void assign_eh(bool is_true) { m_true = is_true; }
int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
int get_pos() const { return m_pos; }
int get_neg() const { return m_neg; }
std::ostream& display(theory_utvpi const& th, std::ostream& out) const;
};
typedef svector<atom> atoms;
struct scope {
unsigned m_atoms_lim;
unsigned m_asserted_atoms_lim;
unsigned m_asserted_qhead_old;
};
struct stats {
unsigned m_num_conflicts;
unsigned m_num_assertions;
unsigned m_num_core2th_eqs;
unsigned m_num_core2th_diseqs;
void reset() {
memset(this, 0, sizeof(*this));
}
stats() {
reset();
}
};
// Functor used to collect the proofs for a conflict due to
// a negative cycle.
class nc_functor {
literal_vector m_antecedents;
theory_utvpi& m_super;
public:
nc_functor(theory_utvpi& s) : m_super(s) {}
void reset() { m_antecedents.reset(); }
literal_vector const& get_lits() const { return m_antecedents; }
void operator()(literal const & ex) {
if (ex != null_literal) {
m_antecedents.push_back(ex);
}
}
void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {
m_super.new_edge(src, dst, num_edges, edges);
}
};
stats m_stats;
smt_params m_params;
arith_util a;
arith_eq_adapter m_arith_eq_adapter;
th_var m_zero_int; // cache the variable representing the zero variable.
th_var m_zero_real; // cache the variable representing the zero variable.
dl_graph<GExt> m_graph;
nc_functor m_nc_functor;
atoms m_atoms;
unsigned_vector m_asserted_atoms; // set of asserted atoms
unsigned m_asserted_qhead;
u_map<unsigned> m_bool_var2atom;
svector<scope> m_scopes;
double m_agility;
bool m_lia;
bool m_lra;
bool m_non_utvpi_exprs;
utvpi_tester m_test;
arith_factory * m_factory;
rational m_delta;
// Set a conflict due to a negative cycle.
void set_conflict();
void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {}
// Create a new theory variable.
virtual th_var mk_var(enode* n);
virtual th_var mk_var(expr* n);
void compute_delta();
void found_non_utvpi_expr(expr * n);
bool is_interpreted(app* n) const {
return n->get_family_id() == get_family_id();
}
public:
theory_utvpi(ast_manager& m);
virtual ~theory_utvpi();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, get_manager()); }
virtual char const * get_name() const { return "utvpi-logic"; }
/**
\brief See comment in theory::mk_eq_atom
*/
virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); }
virtual void init(context * ctx);
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual void internalize_eq_eh(app * atom, bool_var v);
virtual void assign_eh(bool_var v, bool is_true);
virtual void new_eq_eh(th_var v1, th_var v2) {
m_stats.m_num_core2th_eqs++;
m_arith_eq_adapter.new_eq_eh(v1, v2);
}
virtual bool use_diseqs() const { return true; }
virtual void new_diseq_eh(th_var v1, th_var v2) {
m_arith_eq_adapter.new_diseq_eh(v1, v2);
}
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void restart_eh() {
m_arith_eq_adapter.restart_eh();
}
virtual void relevant_eh(app* e) {}
virtual void init_search_eh() {
m_arith_eq_adapter.init_search_eh();
}
virtual final_check_status final_check_eh();
virtual bool is_shared(th_var v) const {
return false;
}
virtual bool can_propagate() {
SASSERT(m_asserted_qhead <= m_asserted_atoms.size());
return m_asserted_qhead != m_asserted_atoms.size();
}
virtual void propagate();
virtual justification * why_is_diseq(th_var v1, th_var v2) {
UNREACHABLE();
return 0;
}
virtual void reset_eh();
virtual void init_model(model_generator & m);
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const {
return true;
}
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
private:
rational mk_value(theory_var v);
void validate_model();
bool eval(expr* e);
rational eval_num(expr* e);
bool check_z_consistency();
virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_eqs++;
new_eq_or_diseq(true, v1, v2, j);
}
virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_diseqs++;
new_eq_or_diseq(false, v1, v2, j);
}
void negate(coeffs& coeffs, rational& weight);
numeral mk_weight(bool is_real, bool is_strict, rational const& w) const;
void mk_coeffs(vector<std::pair<expr*,rational> >const& terms, coeffs& coeffs, rational& w);
void del_atoms(unsigned old_size);
bool propagate_atom(atom const& a);
th_var mk_term(app* n);
th_var mk_num(app* n, rational const& r);
bool is_consistent() const;
th_var expand(bool pos, th_var v, rational & k);
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
void inc_conflicts();
edge_id add_ineq(vector<std::pair<th_var, rational> > const& terms, numeral const& weight, literal l);
bool enable_edge(edge_id id);
th_var to_var(th_var v) const {
return 2*v;
}
th_var from_var(th_var v) const {
return v/2;
}
th_var pos(th_var v) const {
return v & 0xFFFFFFFE;
}
th_var neg(th_var v) const {
return v | 0x1;
}
};
typedef theory_utvpi<rdl_ext> theory_rutvpi;
typedef theory_utvpi<idl_ext> theory_iutvpi;
};
#endif /* _THEORY_UTVPI_H_ */

814
src/smt/theory_utvpi_def.h Normal file
View file

@ -0,0 +1,814 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_utvpi_def.h
Abstract:
Implementation of UTVPI solver.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
1. introduce x^+ and x^-, such that 2*x := x^+ - x^-
2. rewrite constraints as follows:
x - y <= k => x^+ - y^+ <= k
y^- - x^- <= k
x <= k => x^+ - x^- <= 2k
x + y <= k => x^+ - y^- <= k
y^+ - x^- <= k
- x - y <= k => x^- - y^+ <= k
y^- - x^+ <= k
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
--*/
#ifndef _THEORY_UTVPI_DEF_H_
#define _THEORY_UTVPI_DEF_H_
#include "theory_utvpi.h"
#include "heap.h"
#include "ast_pp.h"
#include "smt_context.h"
namespace smt {
template<typename Ext>
theory_utvpi<Ext>::theory_utvpi(ast_manager& m):
theory(m.mk_family_id("arith")),
a(m),
m_arith_eq_adapter(*this, m_params, a),
m_zero_int(null_theory_var),
m_zero_real(null_theory_var),
m_asserted_qhead(0),
m_nc_functor(*this),
m_agility(0.5),
m_lia(false),
m_lra(false),
m_non_utvpi_exprs(false),
m_test(m),
m_factory(0) {
}
template<typename Ext>
theory_utvpi<Ext>::~theory_utvpi() {
reset_eh();
}
template<typename Ext>
std::ostream& theory_utvpi<Ext>::atom::display(theory_utvpi const& th, std::ostream& out) const {
context& ctx = th.get_context();
lbool asgn = ctx.get_assignment(m_bvar);
bool sign = (l_undef == l_false);
return out << literal(m_bvar, sign) << " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " ";
if (l_undef == asgn) {
out << "unassigned\n";
}
else {
th.m_graph.display_edge(out, get_asserted_edge());
}
return out;
}
template<typename Ext>
theory_var theory_utvpi<Ext>::mk_var(enode* n) {
th_var v = theory::mk_var(n);
TRACE("utvpi", tout << v << " " << mk_pp(n->get_owner(), get_manager()) << "\n";);
m_graph.init_var(to_var(v));
m_graph.init_var(neg(to_var(v)));
get_context().attach_th_var(n, this, v);
return v;
}
template<typename Ext>
theory_var theory_utvpi<Ext>::mk_var(expr* n) {
context & ctx = get_context();
enode* e = 0;
th_var v = null_theory_var;
m_lia |= a.is_int(n);
m_lra |= a.is_real(n);
if (!is_app(n)) {
return v;
}
if (ctx.e_internalized(n)) {
e = ctx.get_enode(n);
v = e->get_th_var(get_id());
}
else {
ctx.internalize(n, false);
e = ctx.get_enode(n);
}
if (v == null_theory_var) {
v = mk_var(e);
}
if (is_interpreted(to_app(n))) {
found_non_utvpi_expr(n);
}
return v;
}
template<typename Ext>
void theory_utvpi<Ext>::reset_eh() {
m_graph .reset();
m_zero_int = null_theory_var;
m_zero_real = null_theory_var;
m_atoms .reset();
m_asserted_atoms .reset();
m_stats .reset();
m_scopes .reset();
m_asserted_qhead = 0;
m_agility = 0.5;
m_lia = false;
m_lra = false;
m_non_utvpi_exprs = false;
theory::reset_eh();
}
template<typename Ext>
void theory_utvpi<Ext>::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) {
rational k;
th_var s = expand(true, v1, k);
th_var t = expand(false, v2, k);
context& ctx = get_context();
ast_manager& m = get_manager();
if (s == t) {
if (is_eq != k.is_zero()) {
// conflict 0 /= k;
inc_conflicts();
ctx.set_conflict(&eq_just);
}
}
else {
//
// Create equality ast, internalize_atom
// assign the corresponding equality literal.
//
app_ref eq(m), s2(m), t2(m);
app* s1 = get_enode(s)->get_owner();
app* t1 = get_enode(t)->get_owner();
s2 = a.mk_sub(t1, s1);
t2 = a.mk_numeral(k, m.get_sort(s2.get()));
// t1 - s1 = k
eq = m.mk_eq(s2.get(), t2.get());
TRACE("utvpi",
tout << v1 << " .. " << v2 << "\n";
tout << mk_pp(eq.get(), m) <<"\n";);
if (!internalize_atom(eq.get(), false)) {
UNREACHABLE();
}
literal l(ctx.get_literal(eq.get()));
if (!is_eq) {
l = ~l;
}
ctx.assign(l, b_justification(&eq_just), false);
}
}
template<typename Ext>
void theory_utvpi<Ext>::inc_conflicts() {
m_stats.m_num_conflicts++;
if (m_params.m_arith_adaptive) {
double g = m_params.m_arith_adaptive_propagation_threshold;
m_agility = m_agility*g + 1 - g;
}
}
template<typename Ext>
void theory_utvpi<Ext>::set_conflict() {
inc_conflicts();
literal_vector const& lits = m_nc_functor.get_lits();
context & ctx = get_context();
TRACE("utvpi",
tout << "conflict: ";
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.display_literal_info(tout, lits[i]);
}
tout << "\n";
);
if (m_params.m_arith_dump_lemmas) {
char const * logic = m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA";
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
}
vector<parameter> params;
if (get_manager().proofs_enabled()) {
params.push_back(parameter(symbol("farkas")));
params.resize(lits.size()+1, parameter(rational(1)));
}
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
get_id(), ctx.get_region(),
lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr())));
m_nc_functor.reset();
}
template<typename Ext>
void theory_utvpi<Ext>::found_non_utvpi_expr(expr* n) {
if (!m_non_utvpi_exprs) {
std::stringstream msg;
msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n";
TRACE("utvpi", tout << msg.str(););
warning_msg(msg.str().c_str());
get_context().push_trail(value_trail<context, bool>(m_non_utvpi_exprs));
m_non_utvpi_exprs = true;
}
}
template<typename Ext>
void theory_utvpi<Ext>::init(context* ctx) {
theory::init(ctx);
m_zero_int = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true));
m_zero_real = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), false), false, false, true));
}
/**
\brief Create negated literal.
The negation of: E <= 0
-E + epsilon <= 0
or
-E + 1 <= 0
*/
template<typename Ext>
void theory_utvpi<Ext>::negate(coeffs& coeffs, rational& weight) {
for (unsigned i = 0; i < coeffs.size(); ++i) {
coeffs[i].second.neg();
}
weight.neg();
}
template<typename Ext>
typename theory_utvpi<Ext>::numeral theory_utvpi<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const {
if (is_strict) {
return numeral(w) + (is_real?Ext::m_epsilon:numeral(1));
}
else {
return numeral(w);
}
}
template<typename Ext>
void theory_utvpi<Ext>::mk_coeffs(vector<std::pair<expr*,rational> > const& terms, coeffs& coeffs, rational& w) {
coeffs.reset();
w = m_test.get_weight();
for (unsigned i = 0; i < terms.size(); ++i) {
coeffs.push_back(std::make_pair(mk_var(terms[i].first), terms[i].second));
}
}
template<typename Ext>
void theory_utvpi<Ext>::internalize_eq_eh(app * atom, bool_var v) {
context & ctx = get_context();
app * lhs = to_app(atom->get_arg(0));
app * rhs = to_app(atom->get_arg(1));
if (a.is_numeral(rhs)) {
std::swap(rhs, lhs);
}
if (!a.is_numeral(rhs)) {
return;
}
if (a.is_add(lhs) || a.is_sub(lhs)) {
// force axioms for (= (+ x y) k)
// this is necessary because (+ x y) is not expressible as a utvpi term.
m_arith_eq_adapter.mk_axioms(ctx.get_enode(lhs), ctx.get_enode(rhs));
}
}
template<typename Ext>
bool theory_utvpi<Ext>::internalize_atom(app * n, bool) {
context & ctx = get_context();
if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) {
found_non_utvpi_expr(n);
return false;
}
SASSERT(!ctx.b_internalized(n));
expr* e1 = n->get_arg(0), *e2 = n->get_arg(1);
if (a.is_ge(n) || a.is_gt(n)) {
std::swap(e1, e2);
}
bool is_strict = a.is_gt(n) || a.is_lt(n);
bool cl = m_test.linearize(e1, e2);
if (!cl) {
found_non_utvpi_expr(n);
return false;
}
rational w;
coeffs coeffs;
mk_coeffs(m_test.get_linearization(), coeffs, w);
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
literal l(bv);
numeral w1 = mk_weight(a.is_real(e1), is_strict, w);
edge_id pos = add_ineq(coeffs, w1, l);
negate(coeffs, w);
numeral w2 = mk_weight(a.is_real(e1), !is_strict, w);
edge_id neg = add_ineq(coeffs, w2, ~l);
m_bool_var2atom.insert(bv, m_atoms.size());
m_atoms.push_back(atom(bv, pos, neg));
TRACE("utvpi",
tout << mk_pp(n, get_manager()) << "\n";
m_graph.display_edge(tout << "pos: ", pos);
m_graph.display_edge(tout << "neg: ", neg);
);
return true;
}
template<typename Ext>
bool theory_utvpi<Ext>::internalize_term(app * term) {
bool result = null_theory_var != mk_term(term);
CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
return result;
}
template<typename Ext>
void theory_utvpi<Ext>::assign_eh(bool_var v, bool is_true) {
m_stats.m_num_assertions++;
unsigned idx = m_bool_var2atom.find(v);
SASSERT(get_context().get_assignment(v) != l_undef);
SASSERT((get_context().get_assignment(v) == l_true) == is_true);
m_atoms[idx].assign_eh(is_true);
m_asserted_atoms.push_back(idx);
}
template<typename Ext>
void theory_utvpi<Ext>::push_scope_eh() {
theory::push_scope_eh();
m_graph.push();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_atoms_lim = m_atoms.size();
s.m_asserted_atoms_lim = m_asserted_atoms.size();
s.m_asserted_qhead_old = m_asserted_qhead;
}
template<typename Ext>
void theory_utvpi<Ext>::pop_scope_eh(unsigned num_scopes) {
unsigned lvl = m_scopes.size();
SASSERT(num_scopes <= lvl);
unsigned new_lvl = lvl - num_scopes;
scope & s = m_scopes[new_lvl];
del_atoms(s.m_atoms_lim);
m_asserted_atoms.shrink(s.m_asserted_atoms_lim);
m_asserted_qhead = s.m_asserted_qhead_old;
m_scopes.shrink(new_lvl);
m_graph.pop(num_scopes);
theory::pop_scope_eh(num_scopes);
}
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;
}
else if (!check_z_consistency()) {
return FC_CONTINUE;
}
else if (m_non_utvpi_exprs) {
return FC_GIVEUP;
}
else {
m_graph.set_to_zero(to_var(m_zero_int), to_var(m_zero_real));
m_graph.set_to_zero(neg(to_var(m_zero_int)), neg(to_var(m_zero_real)));
m_graph.set_to_zero(to_var(m_zero_int), neg(to_var(m_zero_int)));
return FC_DONE;
}
}
template<typename Ext>
bool theory_utvpi<Ext>::check_z_consistency() {
int_vector scc_id;
m_graph.compute_zero_edge_scc(scc_id);
unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) {
enode* e = get_enode(i);
if (a.is_int(e->get_owner())) {
continue;
}
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();
SASSERT(r1.is_int());
SASSERT(r2.is_int());
if (r1.is_even() == r2.is_even()) {
continue;
}
if (scc_id[v1] != scc_id[v2]) {
continue;
}
if (scc_id[v1] == -1) {
continue;
}
// they are in the same SCC and have different parities => contradiction.
m_nc_functor.reset();
VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, UINT_MAX, m_nc_functor));
VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, UINT_MAX, m_nc_functor));
IF_VERBOSE(1, verbose_stream() << "parity conflict " << mk_pp(e->get_owner(), get_manager()) << "\n";);
set_conflict();
return false;
}
return true;
}
template<typename Ext>
void theory_utvpi<Ext>::display(std::ostream& out) const {
for (unsigned i = 0; i < m_atoms.size(); ++i) {
m_atoms[i].display(*this, out); out << "\n";
}
m_graph.display(out);
}
template<typename Ext>
void theory_utvpi<Ext>::collect_statistics(::statistics& st) const {
st.update("utvpi conflicts", m_stats.m_num_conflicts);
st.update("utvpi asserts", m_stats.m_num_assertions);
st.update("core->utvpi eqs", m_stats.m_num_core2th_eqs);
st.update("core->utvpi diseqs", m_stats.m_num_core2th_diseqs);
m_arith_eq_adapter.collect_statistics(st);
m_graph.collect_statistics(st);
}
template<typename Ext>
void theory_utvpi<Ext>::del_atoms(unsigned old_size) {
typename atoms::iterator begin = m_atoms.begin() + old_size;
typename atoms::iterator it = m_atoms.end();
while (it != begin) {
--it;
m_bool_var2atom.erase(it->get_bool_var());
}
m_atoms.shrink(old_size);
}
template<typename Ext>
void theory_utvpi<Ext>::propagate() {
bool consistent = true;
while (consistent && can_propagate()) {
unsigned idx = m_asserted_atoms[m_asserted_qhead];
m_asserted_qhead++;
consistent = propagate_atom(m_atoms[idx]);
}
}
template<typename Ext>
bool theory_utvpi<Ext>::propagate_atom(atom const& a) {
context& ctx = get_context();
TRACE("utvpi", a.display(*this, tout); tout << "\n";);
if (ctx.inconsistent()) {
return false;
}
int edge_id = a.get_asserted_edge();
if (!enable_edge(edge_id)) {
m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor);
set_conflict();
return false;
}
return true;
}
template<typename Ext>
theory_var theory_utvpi<Ext>::mk_term(app* n) {
TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";);
context& ctx = get_context();
bool cl = m_test.linearize(n);
if (!cl) {
found_non_utvpi_expr(n);
return null_theory_var;
}
coeffs coeffs;
rational w;
mk_coeffs(m_test.get_linearization(), coeffs, w);
if (coeffs.empty()) {
return mk_num(n, w);
}
if (coeffs.size() == 1 && coeffs[0].second.is_one()) {
return coeffs[0].first;
}
if (coeffs.size() == 2) {
// do not create an alias.
return null_theory_var;
}
for (unsigned i = 0; i < n->get_num_args(); ++i) {
mk_term(to_app(n->get_arg(i)));
}
th_var target = mk_var(ctx.mk_enode(n, false, false, true));
coeffs.push_back(std::make_pair(target, rational(-1)));
VERIFY(enable_edge(add_ineq(coeffs, numeral(w), null_literal)));
negate(coeffs, w);
VERIFY(enable_edge(add_ineq(coeffs, numeral(w), null_literal)));
return target;
}
template<typename Ext>
theory_var theory_utvpi<Ext>::mk_num(app* n, rational const& r) {
theory_var v = null_theory_var;
context& ctx = get_context();
if (r.is_zero()) {
v = a.is_int(n)?m_zero_int:m_zero_real;
}
else if (ctx.e_internalized(n)) {
enode* e = ctx.get_enode(n);
v = e->get_th_var(get_id());
SASSERT(v != null_theory_var);
}
else {
v = mk_var(ctx.mk_enode(n, false, false, true));
// v = k: v <= k k <= v
coeffs coeffs;
coeffs.push_back(std::make_pair(v, rational(-1)));
VERIFY(enable_edge(add_ineq(coeffs, numeral(r), null_literal)));
coeffs.back().second.neg();
VERIFY(enable_edge(add_ineq(coeffs, numeral(-r), null_literal)));
}
return v;
}
template<typename Ext>
theory_var theory_utvpi<Ext>::expand(bool pos, th_var v, rational & k) {
context& ctx = get_context();
enode* e = get_enode(v);
expr* x, *y;
rational r;
for (;;) {
app* n = e->get_owner();
if (a.is_add(n, x, y)) {
if (a.is_numeral(x, r)) {
e = ctx.get_enode(y);
}
else if (a.is_numeral(y, r)) {
e = ctx.get_enode(x);
}
v = e->get_th_var(get_id());
SASSERT(v != null_theory_var);
if (v == null_theory_var) {
break;
}
if (pos) {
k += r;
}
else {
k -= r;
}
}
else {
break;
}
}
return v;
}
// m_graph(source, target, weight, ex);
// target - source <= weight
template<typename Ext>
edge_id theory_utvpi<Ext>::add_ineq(vector<std::pair<th_var, rational> > const& terms, numeral const& weight, literal l) {
SASSERT(terms.size() <= 2);
SASSERT(terms.size() < 1 || terms[0].second.is_one() || terms[0].second.is_minus_one());
SASSERT(terms.size() < 2 || terms[1].second.is_one() || terms[1].second.is_minus_one());
th_var v1 = null_theory_var, v2 = null_theory_var;
bool pos1 = true, pos2 = true;
if (terms.size() >= 1) {
v1 = terms[0].first;
pos1 = terms[0].second.is_one();
SASSERT(v1 != null_theory_var);
SASSERT(pos1 || terms[0].second.is_minus_one());
}
if (terms.size() >= 2) {
v2 = terms[1].first;
pos2 = terms[1].second.is_one();
SASSERT(v1 != null_theory_var);
SASSERT(pos2 || terms[1].second.is_minus_one());
}
// TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";);
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);
}
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);
}
else if (pos1 && pos2) {
m_graph.add_edge(neg(w2), pos(w1), -weight, l);
m_graph.add_edge(neg(w1), pos(w2), -weight, l);
}
else if (pos1 && !pos2) {
m_graph.add_edge(pos(w2), pos(w1), -weight, l);
m_graph.add_edge(neg(w1), neg(w2), -weight, l);
}
else if (!pos1 && pos2) {
m_graph.add_edge(neg(w2), neg(w1), -weight, l);
m_graph.add_edge(pos(w1), pos(w2), -weight, l);
}
else {
m_graph.add_edge(pos(w1), neg(w2), -weight, l);
m_graph.add_edge(pos(w2), neg(w1), -weight, l);
}
return id;
}
template<typename Ext>
bool theory_utvpi<Ext>::enable_edge(edge_id id) {
return (id == null_edge_id) || (m_graph.enable_edge(id) && m_graph.enable_edge(id+1));
}
template<typename Ext>
bool theory_utvpi<Ext>::is_consistent() const {
return m_graph.is_feasible();
}
// 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?
compute_delta();
DEBUG_CODE(validate_model(););
}
template<typename Ext>
void theory_utvpi<Ext>::validate_model() {
context& ctx = get_context();
unsigned sz = m_atoms.size();
for (unsigned i = 0; i < sz; ++i) {
bool_var b = m_atoms[i].get_bool_var();
if (!ctx.is_relevant(b)) {
continue;
}
bool ok = true;
expr* e = ctx.bool_var2expr(b);
switch(ctx.get_assignment(b)) {
case l_true:
ok = eval(e);
break;
case l_false:
ok = !eval(e);
break;
default:
break;
}
CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";);
// CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";);
SASSERT(ok);
}
}
template<typename Ext>
bool theory_utvpi<Ext>::eval(expr* e) {
expr* e1, *e2;
if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1)) {
return eval_num(e1) <= eval_num(e2);
}
if (a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) {
return eval_num(e1) < eval_num(e2);
}
if (get_manager().is_eq(e, e1, e2)) {
return eval_num(e1) == eval_num(e2);
}
TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";);
return false;
}
template<typename Ext>
rational theory_utvpi<Ext>::eval_num(expr* e) {
rational r;
expr* e1, *e2;
if (a.is_numeral(e, r)) {
return r;
}
if (a.is_sub(e, e1, e2)) {
return eval_num(e1) - eval_num(e2);
}
if (a.is_add(e)) {
r.reset();
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
r += eval_num(to_app(e)->get_arg(i));
}
return r;
}
if (a.is_mul(e)) {
r = rational(1);
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
r *= eval_num(to_app(e)->get_arg(i));
}
return r;
}
if (a.is_uminus(e, e1)) {
return -eval_num(e1);
}
if (a.is_to_real(e, e1)) {
return eval_num(e1);
}
if (is_uninterp_const(e)) {
return mk_value(mk_var(e));
}
TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";);
UNREACHABLE();
return rational(0);
}
template<typename Ext>
rational theory_utvpi<Ext>::mk_value(th_var v) {
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);
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);
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())));
}
/**
\brief Compute numeral values for the infinitesimals to satisfy the inequalities.
*/
template<typename Ext>
void theory_utvpi<Ext>::compute_delta() {
m_delta = rational(1);
unsigned sz = m_graph.get_num_edges();
for (unsigned i = 0; i < sz; ++i) {
if (!m_graph.is_enabled(i)) {
continue;
}
numeral w = m_graph.get_weight(i);
numeral tgt = m_graph.get_assignment(m_graph.get_target(i));
numeral src = m_graph.get_assignment(m_graph.get_source(i));
numeral b = tgt - src - w;
SASSERT(b.is_nonpos());
rational eps_r = b.get_infinitesimal();
// Given: b <= 0
// suppose that 0 < b.eps
// then we have 0 > b.num
// then delta must ensure:
// 0 >= b.num + delta*b.eps
// <=>
// -b.num/b.eps >= delta
if (eps_r.is_pos()) {
rational num_r = -b.get_rational();
SASSERT(num_r.is_pos());
rational new_delta = num_r/eps_r;
if (new_delta < m_delta) {
m_delta = new_delta;
}
}
}
}
};
#endif

6
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -371,6 +371,12 @@ struct ctx_simplify_tactic::imp {
if (!modified) {
r = t;
}
else if (new_new_args.empty()) {
r = OR?m.mk_false():m.mk_true();
}
else if (new_new_args.size() == 1) {
r = new_new_args[0];
}
else {
std::reverse(new_new_args.c_ptr(), new_new_args.c_ptr() + new_new_args.size());
m_mk_app(t->get_decl(), new_new_args.size(), new_new_args.c_ptr(), r);

1
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -94,7 +94,6 @@ public:
smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {}
virtual ~smt_strategic_solver_factory() {}
virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) {
symbol l;
if (m_logic != symbol::null)

6
src/util/hash.h
View file

@ -20,6 +20,7 @@ Revision History:
#define _HASH_H_
#include<algorithm>
#include"util.h"
#ifndef __fallthrough
#define __fallthrough
@ -142,6 +143,11 @@ struct size_t_hash {
unsigned operator()(size_t x) const { return static_cast<unsigned>(x); }
};
struct uint64_hash {
typedef uint64 data;
unsigned operator()(uint64 x) const { return static_cast<unsigned>(x); }
};
struct bool_hash {
typedef bool data;
unsigned operator()(bool x) const { return static_cast<unsigned>(x); }

409
src/util/inf_eps_rational.h Normal file
View file

@ -0,0 +1,409 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
inf_eps_rational.h
Abstract:
Rational numbers with infinity and epsilon.
Author:
Nikolaj Bjorner (nbjorner) 2013-4-23.
Revision History:
--*/
#ifndef _INF_EPS_RATIONAL_H_
#define _INF_EPS_RATIONAL_H_
#include<stdlib.h>
#include<string>
#include"debug.h"
#include"vector.h"
#include"rational.h"
template<typename Numeral>
class inf_eps_rational {
rational m_infty;
Numeral m_r;
public:
unsigned hash() const {
return m_infty.hash() ^ m_r.hash();
}
struct hash_proc { unsigned operator()(inf_eps_rational const& r) const { return r.hash(); } };
struct eq_proc { bool operator()(inf_eps_rational const& r1, inf_eps_rational const& r2) const { return r1 == r2; } };
void swap(inf_eps_rational & n) {
m_infty.swap(n.m_infty);
m_r.swap(n.m_r);
}
std::string to_string() const {
if (m_infty.is_zero()) {
return m_r.to_string();
}
std::string si;
if (m_infty.is_one()) {
si = "oo";
}
else if (m_infty.is_minus_one()) {
si = "-oo";
}
else {
si = m_infty.to_string() += "*oo";
}
if (m_r.is_zero()) {
return si;
}
std::string s = "(";
s += si;
s += " + ";
s += m_r.to_string();
s += ")";
return s;
}
inf_eps_rational():
m_infty(),
m_r()
{}
inf_eps_rational(const inf_eps_rational & r):
m_infty(r.m_infty),
m_r(r.m_r)
{}
explicit inf_eps_rational(int n):
m_infty(),
m_r(n)
{}
explicit inf_eps_rational(Numeral const& r):
m_infty(),
m_r(r)
{}
explicit inf_eps_rational(rational const& i, Numeral const& r):
m_infty(i),
m_r(r) {
}
~inf_eps_rational() {}
/**
\brief Set inf_eps_rational to 0.
*/
void reset() {
m_infty.reset();
m_r.reset();
}
bool is_int() const {
return m_infty.is_zero() && m_r.is_int();
}
bool is_int64() const {
return m_infty.is_zero() && m_r.is_int64();
}
bool is_uint64() const {
return m_infty.is_zero() && m_r.is_uint64();
}
bool is_rational() const { return m_infty.is_zero() && m_r.is_rational(); }
int64 get_int64() const {
SASSERT(is_int64());
return m_r.get_int64();
}
uint64 get_uint64() const {
SASSERT(is_uint64());
return m_r.get_uint64();
}
rational const& get_rational() const {
return m_r.get_rational();
}
rational const& get_infinitesimal() const {
return m_r.get_infinitesimal();
}
rational const& get_infinity() const {
return m_infty;
}
inf_eps_rational & operator=(const inf_eps_rational & r) {
m_infty = r.m_infty;
m_r = r.m_r;
return *this;
}
inf_eps_rational & operator=(const rational & r) {
m_infty.reset();
m_r = r;
return *this;
}
inf_eps_rational & operator+=(const inf_eps_rational & r) {
m_infty += r.m_infty;
m_r += r.m_r;
return *this;
}
inf_eps_rational & operator-=(const inf_eps_rational & r) {
m_infty -= r.m_infty;
m_r -= r.m_r;
return *this;
}
inf_eps_rational & operator+=(const rational & r) {
m_r += r;
return *this;
}
inf_eps_rational & operator-=(const rational & r) {
m_r -= r;
return *this;
}
inf_eps_rational & operator*=(const rational & r1) {
m_infty *= r1;
m_r *= r1;
return *this;
}
inf_eps_rational & operator/=(const rational & r) {
m_infty /= r;
m_r /= r;
return *this;
}
inf_eps_rational & operator++() {
++m_r;
return *this;
}
const inf_eps_rational operator++(int) { inf_eps_rational tmp(*this); ++(*this); return tmp; }
inf_eps_rational & operator--() {
--m_r;
return *this;
}
const inf_eps_rational operator--(int) { inf_eps_rational tmp(*this); --(*this); return tmp; }
friend inline bool operator==(const inf_eps_rational & r1, const inf_eps_rational & r2) {
return r1.m_infty == r2.m_infty && r1.m_r == r2.m_r;
}
friend inline bool operator==(const rational & r1, const inf_eps_rational & r2) {
return r1 == r2.m_infty && r2.m_r.is_zero();
}
friend inline bool operator==(const inf_eps_rational & r1, const rational & r2) {
return r1.m_infty == r2 && r1.m_r.is_zero();
}
friend inline bool operator<(const inf_eps_rational & r1, const inf_eps_rational & r2) {
return
(r1.m_infty < r2.m_infty) ||
(r1.m_infty == r2.m_infty && r1.m_r < r2.m_r);
}
friend inline bool operator<(const rational & r1, const inf_eps_rational & r2) {
return
r2.m_infty.is_pos() ||
(r2.m_infty.is_zero() && r1 < r2.m_r);
}
friend inline bool operator<(const inf_eps_rational & r1, const rational & r2) {
return
r1.m_infty.is_neg() ||
(r1.m_infty.is_zero() && r1.m_r < r2);
}
void neg() {
m_infty.neg();
m_r.neg();
}
bool is_zero() const {
return m_infty.is_zero() && m_r.is_zero();
}
bool is_one() const {
return m_infty.is_zero() && m_r.is_one();
}
bool is_minus_one() const {
return m_infty.is_zero() && m_r.is_minus_one();
}
bool is_neg() const {
return
m_infty.is_neg() ||
(m_infty.is_zero() && m_r.is_neg());
}
bool is_pos() const {
return
m_infty.is_pos() ||
(m_infty.is_zero() && m_r.is_pos());
}
bool is_nonneg() const {
return
m_infty.is_pos() ||
(m_infty.is_zero() && m_r.is_nonneg());
}
bool is_nonpos() const {
return
m_infty.is_neg() ||
(m_infty.is_zero() && m_r.is_nonpos());
}
friend inline rational floor(const inf_eps_rational & r) {
SASSERT(r.m_infty.is_zero());
return floor(r.m_r);
}
friend inline rational ceil(const inf_eps_rational & r) {
SASSERT(r.m_infty.is_zero());
return ceil(r.m_r);
}
// Perform: this += c * k
void addmul(const rational & c, const inf_eps_rational & k) {
m_infty.addmul(c, k.m_infty);
m_r.addmul(c, k.m_r);
}
// Perform: this += c * k
void submul(const rational & c, const inf_eps_rational & k) {
m_infty.submul(c, k.m_infty);
m_r.submul(c, k.m_r);
}
};
template<typename N>
inline bool operator!=(const inf_eps_rational<N> & r1, const inf_eps_rational<N> & r2) {
return !operator==(r1, r2);
}
template<typename N>
inline bool operator!=(const rational & r1, const inf_eps_rational<N> & r2) {
return !operator==(r1, r2);
}
template<typename N>
inline bool operator!=(const inf_eps_rational<N> & r1, const rational & r2) {
return !operator==(r1, r2);
}
template<typename N>
inline bool operator>(const inf_eps_rational<N> & r1, const inf_eps_rational<N> & r2) {
return operator<(r2, r1);
}
template<typename N>
inline bool operator>(const inf_eps_rational<N> & r1, const rational & r2) {
return operator<(r2, r1);
}
template<typename N>
inline bool operator>(const rational & r1, const inf_eps_rational<N> & r2) {
return operator<(r2, r1);
}
template<typename N>
inline bool operator<=(const inf_eps_rational<N> & r1, const inf_eps_rational<N> & r2) {
return !operator>(r1, r2);
}
template<typename N>
inline bool operator<=(const rational & r1, const inf_eps_rational<N> & r2) {
return !operator>(r1, r2);
}
template<typename N>
inline bool operator<=(const inf_eps_rational<N> & r1, const rational & r2) {
return !operator>(r1, r2);
}
template<typename N>
inline bool operator>=(const inf_eps_rational<N> & r1, const inf_eps_rational<N> & r2) {
return !operator<(r1, r2);
}
template<typename N>
inline bool operator>=(const rational & r1, const inf_eps_rational<N> & r2) {
return !operator<(r1, r2);
}
template<typename N>
inline bool operator>=(const inf_eps_rational<N> & r1, const rational & r2) {
return !operator<(r1, r2);
}
template<typename N>
inline inf_eps_rational<N> operator+(const inf_eps_rational<N> & r1, const inf_eps_rational<N> & r2) {
return inf_eps_rational<N>(r1) += r2;
}
template<typename N>
inline inf_eps_rational<N> operator-(const inf_eps_rational<N> & r1, const inf_eps_rational<N> & r2) {
return inf_eps_rational<N>(r1) -= r2;
}
template<typename N>
inline inf_eps_rational<N> operator-(const inf_eps_rational<N> & r) {
inf_eps_rational<N> result(r);
result.neg();
return result;
}
template<typename N>
inline inf_eps_rational<N> operator*(const rational & r1, const inf_eps_rational<N> & r2) {
inf_eps_rational<N> result(r2);
result *= r1;
return result;
}
template<typename N>
inline inf_eps_rational<N> operator*(const inf_eps_rational<N> & r1, const rational & r2) {
return r2 * r1;
}
template<typename N>
inline inf_eps_rational<N> operator/(const inf_eps_rational<N> & r1, const rational & r2) {
inf_eps_rational<N> result(r1);
result /= r2;
return result;
}
template<typename N>
inline std::ostream & operator<<(std::ostream & target, const inf_eps_rational<N> & r) {
target << r.to_string();
return target;
}
template<typename N>
inline inf_eps_rational<N> abs(const inf_eps_rational<N> & r) {
inf_eps_rational<N> result(r);
if (result.is_neg()) {
result.neg();
}
return result;
}
#endif /* _INF_EPS_RATIONAL_H_ */

5
src/util/inf_rational.h
View file

@ -223,6 +223,7 @@ class inf_rational {
}
friend inline inf_rational operator*(const rational & r1, const inf_rational & r2);
friend inline inf_rational operator*(const inf_rational & r1, const rational & r2);
friend inline inf_rational operator/(const inf_rational & r1, const rational & r2);
inf_rational & operator++() {
@ -426,6 +427,10 @@ inline inf_rational operator*(const rational & r1, const inf_rational & r2) {
return result;
}
inline inf_rational operator*(const inf_rational & r1, const rational & r2) {
return r2 * r1;
}
inline inf_rational operator/(const inf_rational & r1, const rational & r2) {
inf_rational result(r1);
result.m_first /= r2;

3
src/util/memory_manager.cpp
View file

@ -231,9 +231,8 @@ void * memory::allocate(size_t s) {
return 0;
s = s + sizeof(size_t); // we allocate an extra field!
void * r = malloc(s);
if (r == 0) {
if (r == 0)
throw_out_of_memory();
}
*(static_cast<size_t*>(r)) = s;
g_memory_thread_alloc_size += s;
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {

17
src/util/vector.h
View file

@ -432,24 +432,29 @@ typedef svector<unsigned> unsigned_vector;
typedef svector<char> char_vector;
typedef svector<double> double_vector;
template<typename Hash>
struct vector_hash {
template<typename Hash, typename Vec>
struct vector_hash_tpl {
Hash m_hash;
typedef vector<typename Hash::data> data;
typedef Vec data;
unsigned operator()(data const& v, unsigned idx) const { return m_hash(v[idx]); }
vector_hash(Hash const& h = Hash()):m_hash(h) {}
vector_hash_tpl(Hash const& h = Hash()):m_hash(h) {}
unsigned operator()(data const& v) const {
if (v.empty()) {
return 778;
}
return get_composite_hash<data, default_kind_hash_proc<data>, vector_hash>(v, v.size());
return get_composite_hash<data, default_kind_hash_proc<data>, vector_hash_tpl>(v, v.size());
}
};
template<typename Hash>
struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> > {};
template<typename Hash>
struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
#endif /* _VECTOR_H_ */