mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

reducing dependencies on simplifier

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-22 15:09:34 -07:00
parent a206362cef
commit e2b46257d6
18 changed files with 289 additions and 215 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/arith_decl_plugin.h
View file

@ -389,16 +389,16 @@ public:
app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }
app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); } app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); }
app * mk_add(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); } app * mk_add(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
app * mk_add(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); } app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
app * mk_add(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); } app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
app * mk_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); } app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
app * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); } app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
app * mk_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); } app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
app * mk_mul(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); } app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
app * mk_mul(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); } app * mk_mul(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
app * mk_uminus(expr * arg) { return m_manager.mk_app(m_afid, OP_UMINUS, arg); } app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); } app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); }
app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); } app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); }
app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); } app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); }

10
src/ast/bv_decl_plugin.cpp
View file

@ -784,6 +784,12 @@ bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_si
return true; return true;
} }
bool bv_recognizers::is_numeral(expr const * n, rational & val) const {
unsigned bv_size = 0;
return is_numeral(n, val, bv_size);
}
bool bv_recognizers::is_allone(expr const * e) const { bool bv_recognizers::is_allone(expr const * e) const {
rational r; rational r;
unsigned bv_size; unsigned bv_size;
@ -847,7 +853,7 @@ bv_util::bv_util(ast_manager & m):
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv"))); m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
} }
app * bv_util::mk_numeral(rational const & val, sort* s) { app * bv_util::mk_numeral(rational const & val, sort* s) const {
if (!is_bv_sort(s)) { if (!is_bv_sort(s)) {
return 0; return 0;
} }
@ -855,7 +861,7 @@ app * bv_util::mk_numeral(rational const & val, sort* s) {
return mk_numeral(val, bv_size); return mk_numeral(val, bv_size);
} }
app * bv_util::mk_numeral(rational const & val, unsigned bv_size) { app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
parameter p1(val); parameter p1(val);
parameter p[2] = { p1, parameter(static_cast<int>(bv_size)) }; parameter p[2] = { p1, parameter(static_cast<int>(bv_size)) };
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0); return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);

7
src/ast/bv_decl_plugin.h
View file

@ -293,6 +293,7 @@ public:
family_id get_fid() const { return m_afid; } family_id get_fid() const { return m_afid; }
family_id get_family_id() const { return get_fid(); } family_id get_family_id() const { return get_fid(); }
bool is_numeral(expr const * n, rational & val) const;
bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const; bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
bool is_numeral(expr const * n) const { return is_app_of(n, get_fid(), OP_BV_NUM); } bool is_numeral(expr const * n) const { return is_app_of(n, get_fid(), OP_BV_NUM); }
bool is_allone(expr const * e) const; bool is_allone(expr const * e) const;
@ -381,9 +382,9 @@ public:
ast_manager & get_manager() const { return m_manager; } ast_manager & get_manager() const { return m_manager; }
app * mk_numeral(rational const & val, sort* s); app * mk_numeral(rational const & val, sort* s) const;
app * mk_numeral(rational const & val, unsigned bv_size); app * mk_numeral(rational const & val, unsigned bv_size) const;
app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); } app * mk_numeral(uint64 u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui64()), bv_size); }
sort * mk_sort(unsigned bv_size); sort * mk_sort(unsigned bv_size);
unsigned get_bv_size(sort const * s) const { unsigned get_bv_size(sort const * s) const {

20
src/ast/macros/macro_finder.cpp
View file

@ -48,14 +48,12 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
return false; return false;
arith_simplifier_plugin * as = get_arith_simp();
arith_util & autil = as->get_arith_util();
expr * body = to_quantifier(n)->get_expr(); expr * body = to_quantifier(n)->get_expr();
unsigned num_decls = to_quantifier(n)->get_num_decls(); unsigned num_decls = to_quantifier(n)->get_num_decls();
if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body)) if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m_manager.is_eq(body))
return false; return false;
if (!as->is_add(to_app(body)->get_arg(0))) if (!m_autil.is_add(to_app(body)->get_arg(0)))
return false; return false;
app_ref head(m_manager); app_ref head(m_manager);
expr_ref def(m_manager); expr_ref def(m_manager);
@ -66,10 +64,10 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
if (!inv || m_manager.is_eq(body)) if (!inv || m_manager.is_eq(body))
new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def); new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
else if (as->is_le(body)) else if (m_autil.is_le(body))
new_body = autil.mk_ge(head, def); new_body = m_autil.mk_ge(head, def);
else else
new_body = autil.mk_le(head, def); new_body = m_autil.mk_le(head, def);
quantifier_ref new_q(m_manager); quantifier_ref new_q(m_manager);
new_q = m_manager.update_quantifier(to_quantifier(n), new_body); new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
@ -88,10 +86,9 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
app * k_app = m_manager.mk_app(k, head->get_num_args(), head->get_args()); app * k_app = m_manager.mk_app(k, head->get_num_args(), head->get_args());
expr_ref_buffer new_rhs_args(m_manager); expr_ref_buffer new_rhs_args(m_manager);
expr_ref new_rhs2(m_manager); expr_ref new_rhs2(m_autil.mk_add(def, k_app), m_manager);
as->mk_add(def, k_app, new_rhs2);
expr * body1 = m_manager.mk_eq(head, new_rhs2); expr * body1 = m_manager.mk_eq(head, new_rhs2);
expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, as->mk_numeral(rational(0))); expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
quantifier * q1 = m_manager.update_quantifier(new_q, body1); quantifier * q1 = m_manager.update_quantifier(new_q, body1);
expr * patterns[1] = { m_manager.mk_pattern(k_app) }; expr * patterns[1] = { m_manager.mk_pattern(k_app) };
quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2); quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2);
@ -158,7 +155,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
macro_finder::macro_finder(ast_manager & m, macro_manager & mm): macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
m_manager(m), m_manager(m),
m_macro_manager(mm), m_macro_manager(mm),
m_util(mm.get_util()) { m_util(mm.get_util()),
m_autil(m) {
} }
macro_finder::~macro_finder() { macro_finder::~macro_finder() {

3
src/ast/macros/macro_finder.h
View file

@ -20,7 +20,6 @@ Revision History:
#define MACRO_FINDER_H_ #define MACRO_FINDER_H_
#include "ast/macros/macro_manager.h" #include "ast/macros/macro_manager.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
bool is_macro_head(expr * n, unsigned num_decls); bool is_macro_head(expr * n, unsigned num_decls);
@ -37,7 +36,7 @@ class macro_finder {
ast_manager & m_manager; ast_manager & m_manager;
macro_manager & m_macro_manager; macro_manager & m_macro_manager;
macro_util & m_util; macro_util & m_util;
arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); } arith_util m_autil;
bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);

2
src/ast/macros/macro_manager.cpp
View file

@ -28,7 +28,7 @@ Revision History:
macro_manager::macro_manager(ast_manager & m, simplifier & s): macro_manager::macro_manager(ast_manager & m, simplifier & s):
m_manager(m), m_manager(m),
m_simplifier(s), m_simplifier(s),
m_util(m, s), m_util(m),
m_decls(m), m_decls(m),
m_macros(m), m_macros(m),
m_macro_prs(m), m_macro_prs(m),

85
src/ast/macros/macro_util.cpp
View file

@ -29,16 +29,17 @@ Revision History:
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bool_rewriter.h"
macro_util::macro_util(ast_manager & m, simplifier & s): macro_util::macro_util(ast_manager & m):
m_manager(m), m_manager(m),
m_bv(m), m_bv(m),
m_simplifier(s), m_arith(m),
m_arith_simp(0), m_arith_rw(m),
m_bv_simp(0), m_bv_rw(m),
m_forbidden_set(0), m_forbidden_set(0),
m_curr_clause(0) { m_curr_clause(0) {
} }
#if 0
arith_simplifier_plugin * macro_util::get_arith_simp() const { arith_simplifier_plugin * macro_util::get_arith_simp() const {
if (m_arith_simp == 0) { if (m_arith_simp == 0) {
const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith"))); const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
@ -54,7 +55,7 @@ bv_simplifier_plugin * macro_util::get_bv_simp() const {
SASSERT(m_bv_simp != 0); SASSERT(m_bv_simp != 0);
return m_bv_simp; return m_bv_simp;
} }
#endif
bool macro_util::is_bv(expr * n) const { bool macro_util::is_bv(expr * n) const {
return m_bv.is_bv(n); return m_bv.is_bv(n);
@ -65,32 +66,41 @@ bool macro_util::is_bv_sort(sort * s) const {
} }
bool macro_util::is_add(expr * n) const { bool macro_util::is_add(expr * n) const {
return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n); return m_arith.is_add(n) || m_bv.is_bv_add(n);
} }
bool macro_util::is_times_minus_one(expr * n, expr * & arg) const { bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg); return m_arith_rw.is_times_minus_one(n, arg) || m_bv_rw.is_times_minus_one(n, arg);
} }
bool macro_util::is_le(expr * n) const { bool macro_util::is_le(expr * n) const {
return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n); return m_arith.is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
} }
bool macro_util::is_le_ge(expr * n) const { bool macro_util::is_le_ge(expr * n) const {
return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n); return m_arith.is_ge(n) || m_arith.is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
} }
poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const { bool macro_util::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
if (is_bv_sort(s)) return m_arith_rw.is_var_plus_ground(n, inv, v, t) || m_bv_rw.is_var_plus_ground(n, inv, v, t);
return get_bv_simp(); }
else
return get_arith_simp(); bool macro_util::is_zero_safe(expr * n) const {
if (m_bv_rw.is_bv(n)) {
return m_bv.is_zero(n);
}
else {
return m_arith_rw.is_zero(n);
}
} }
app * macro_util::mk_zero(sort * s) const { app * macro_util::mk_zero(sort * s) const {
poly_simplifier_plugin * ps = get_poly_simp_for(s); if (m_bv.is_bv_sort(s)) {
ps->set_curr_sort(s); return m_bv.mk_numeral(rational(0), s);
return ps->mk_zero(); }
else {
return m_arith.mk_numeral(rational(0), s);
}
} }
void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const { void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
@ -98,7 +108,7 @@ void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
r = m_bv.mk_bv_sub(t1, t2); r = m_bv.mk_bv_sub(t1, t2);
} }
else { else {
get_arith_simp()->mk_sub(t1, t2, r); r = m_arith.mk_sub(t1, t2);
} }
} }
@ -107,18 +117,32 @@ void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
r = m_bv.mk_bv_add(t1, t2); r = m_bv.mk_bv_add(t1, t2);
} }
else { else {
get_arith_simp()->mk_add(t1, t2, r); r = m_arith.mk_add(t1, t2);
} }
} }
void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const { void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const {
if (num_args == 0) { switch (num_args) {
case 0:
r = mk_zero(s); r = mk_zero(s);
return; break;
case 1:
r = args[0];
break;
default:
if (m_bv.is_bv_sort(s)) {
r = args[0];
while (num_args >= 2) {
--num_args;
++args;
r = m_bv.mk_bv_add(r, args[0]);
}
}
else {
r = m_arith.mk_add(num_args, args);
}
break;
} }
poly_simplifier_plugin * ps = get_poly_simp_for(s);
ps->set_curr_sort(s);
ps->mk_add(num_args, args, r);
} }
/** /**
@ -241,13 +265,12 @@ bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) c
bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const { bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const {
// TODO: obsolete... we should move to collect_arith_macro_candidates // TODO: obsolete... we should move to collect_arith_macro_candidates
arith_simplifier_plugin * as = get_arith_simp(); if (!m_manager.is_eq(n) && !m_arith.is_le(n) && !m_arith.is_ge(n))
if (!m_manager.is_eq(n) && !as->is_le(n) && !as->is_ge(n))
return false; return false;
expr * lhs = to_app(n)->get_arg(0); expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1); expr * rhs = to_app(n)->get_arg(1);
if (!as->is_numeral(rhs)) if (!m_arith.is_numeral(rhs))
return false; return false;
inv = false; inv = false;
@ -272,7 +295,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
!poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) { !poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) {
h = arg; h = arg;
} }
else if (h == 0 && as->is_times_minus_one(arg, neg_arg) && else if (h == 0 && m_arith_rw.is_times_minus_one(arg, neg_arg) &&
is_macro_head(neg_arg, num_decls) && is_macro_head(neg_arg, num_decls) &&
!is_forbidden(to_app(neg_arg)->get_decl()) && !is_forbidden(to_app(neg_arg)->get_decl()) &&
!poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) { !poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) {
@ -287,11 +310,11 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
return false; return false;
head = to_app(h); head = to_app(h);
expr_ref tmp(m_manager); expr_ref tmp(m_manager);
as->mk_add(args.size(), args.c_ptr(), tmp); tmp = m_arith.mk_add(args.size(), args.c_ptr());
if (inv) if (inv)
as->mk_sub(tmp, rhs, def); def = m_arith.mk_sub(tmp, rhs);
else else
as->mk_sub(rhs, tmp, def); def = m_arith.mk_sub(rhs, tmp);
return true; return true;
} }

21
src/ast/macros/macro_util.h
View file

@ -22,12 +22,8 @@ Revision History:
#include "ast/ast.h" #include "ast/ast.h"
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
#include "ast/simplifier/simplifier.h" #include "ast/rewriter/arith_rewriter.h"
#include "ast/rewriter/bv_rewriter.h"
class poly_simplifier_plugin;
class arith_simplifier_plugin;
class bv_simplifier_plugin;
class basic_simplifier_plugin;
class macro_util { class macro_util {
public: public:
@ -63,9 +59,9 @@ public:
private: private:
ast_manager & m_manager; ast_manager & m_manager;
bv_util m_bv; bv_util m_bv;
simplifier & m_simplifier; arith_util m_arith;
arith_simplifier_plugin * m_arith_simp; arith_rewriter m_arith_rw;
bv_simplifier_plugin * m_bv_simp; bv_rewriter m_bv_rw;
obj_hashtable<func_decl> * m_forbidden_set; obj_hashtable<func_decl> * m_forbidden_set;
bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); } bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
@ -94,11 +90,9 @@ private:
public: public:
macro_util(ast_manager & m, simplifier & s); macro_util(ast_manager & m);
void set_forbidden_set(obj_hashtable<func_decl> * s) { m_forbidden_set = s; } void set_forbidden_set(obj_hashtable<func_decl> * s) { m_forbidden_set = s; }
arith_simplifier_plugin * get_arith_simp() const;
bv_simplifier_plugin * get_bv_simp() const;
bool is_macro_head(expr * n, unsigned num_decls) const; bool is_macro_head(expr * n, unsigned num_decls) const;
bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const; bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
@ -113,6 +107,8 @@ public:
return is_arith_macro(n, num_decls, head, def, inv); return is_arith_macro(n, num_decls, head, def, inv);
} }
bool is_zero_safe(expr * n) const;
bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t); bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def); bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
@ -137,7 +133,6 @@ public:
void mk_sub(expr * t1, expr * t2, expr_ref & r) const; void mk_sub(expr * t1, expr * t2, expr_ref & r) const;
void mk_add(expr * t1, expr * t2, expr_ref & r) const; void mk_add(expr * t1, expr * t2, expr_ref & r) const;
void mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const; void mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const;
poly_simplifier_plugin * get_poly_simp_for(sort * s) const;
}; };
#endif #endif

10
src/ast/macros/quasi_macros.cpp
View file

@ -22,10 +22,10 @@ Revision History:
#include "util/uint_set.h" #include "util/uint_set.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s) : quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
m_manager(m), m_manager(m),
m_macro_manager(mm), m_macro_manager(mm),
m_simplifier(s), m_rewriter(m),
m_new_vars(m), m_new_vars(m),
m_new_eqs(m), m_new_eqs(m),
m_new_qsorts(m) { m_new_qsorts(m) {
@ -299,8 +299,8 @@ void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const
proof_ref pr(m_manager), ps(m_manager); proof_ref pr(m_manager), ps(m_manager);
proof * p = m_manager.proofs_enabled() ? prs[i] : 0; proof * p = m_manager.proofs_enabled() ? prs[i] : 0;
m_macro_manager.expand_macros(exprs[i], p, r, pr); m_macro_manager.expand_macros(exprs[i], p, r, pr);
m_simplifier(r, rs, ps); m_rewriter(r);
new_exprs.push_back(rs); new_exprs.push_back(r);
new_prs.push_back(ps); new_prs.push_back(ps);
} }
} }

7
src/ast/macros/quasi_macros.h
View file

@ -21,8 +21,7 @@ Revision History:
#include<sstream> #include<sstream>
#include "ast/macros/macro_manager.h" #include "ast/macros/macro_manager.h"
#include "ast/simplifier/basic_simplifier_plugin.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/simplifier/simplifier.h"
/** /**
\brief Finds quasi macros and applies them. \brief Finds quasi macros and applies them.
@ -32,7 +31,7 @@ class quasi_macros {
ast_manager & m_manager; ast_manager & m_manager;
macro_manager & m_macro_manager; macro_manager & m_macro_manager;
simplifier & m_simplifier; th_rewriter m_rewriter;
occurrences_map m_occurrences; occurrences_map m_occurrences;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
@ -57,7 +56,7 @@ class quasi_macros {
void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
public: public:
quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s); quasi_macros(ast_manager & m, macro_manager & mm);
~quasi_macros(); ~quasi_macros();
/** /**

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

@ -35,7 +35,6 @@ protected:
bool is_numeral(expr * n) const { return m_util.is_numeral(n); } bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); } bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
bool is_zero(expr * n) const { return m_util.is_zero(n); }
bool is_minus_one(expr * n) const { return m_util.is_minus_one(n); } bool is_minus_one(expr * n) const { return m_util.is_minus_one(n); }
void normalize(numeral & c, sort * s) {} void normalize(numeral & c, sort * s) {}
app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); } app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); }
@ -45,6 +44,7 @@ protected:
decl_kind power_decl_kind() const { return OP_POWER; } decl_kind power_decl_kind() const { return OP_POWER; }
public: public:
arith_rewriter_core(ast_manager & m):m_util(m) {} arith_rewriter_core(ast_manager & m):m_util(m) {}
bool is_zero(expr * n) const { return m_util.is_zero(n); }
}; };
class arith_rewriter : public poly_rewriter<arith_rewriter_core> { class arith_rewriter : public poly_rewriter<arith_rewriter_core> {

4
src/ast/rewriter/poly_rewriter.h
View file

@ -39,7 +39,6 @@ protected:
bool is_numeral(expr * n) const { return Config::is_numeral(n); } bool is_numeral(expr * n) const { return Config::is_numeral(n); }
bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); } bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); }
bool is_zero(expr * n) const { return Config::is_zero(n); }
bool is_minus_one(expr * n) const { return Config::is_minus_one(n); } bool is_minus_one(expr * n) const { return Config::is_minus_one(n); }
void normalize(numeral & c) { Config::normalize(c, m_curr_sort); } void normalize(numeral & c) { Config::normalize(c, m_curr_sort); }
app * mk_numeral(numeral const & r) { return Config::mk_numeral(r, m_curr_sort); } app * mk_numeral(numeral const & r) { return Config::mk_numeral(r, m_curr_sort); }
@ -111,6 +110,9 @@ public:
bool is_mul(expr * n) const { return is_app_of(n, get_fid(), mul_decl_kind()); } bool is_mul(expr * n) const { return is_app_of(n, get_fid(), mul_decl_kind()); }
bool is_add(func_decl * f) const { return is_decl_of(f, get_fid(), add_decl_kind()); } bool is_add(func_decl * f) const { return is_decl_of(f, get_fid(), add_decl_kind()); }
bool is_mul(func_decl * f) const { return is_decl_of(f, get_fid(), mul_decl_kind()); } bool is_mul(func_decl * f) const { return is_decl_of(f, get_fid(), mul_decl_kind()); }
bool is_times_minus_one(expr * n, expr*& r) const;
bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args > 0); SASSERT(num_args > 0);

60
src/ast/rewriter/poly_rewriter_def.h
View file

@ -931,3 +931,63 @@ expr* poly_rewriter<Config>::merge_muls(expr* x, expr* y) {
m1[k] = mk_add_app(2, args); m1[k] = mk_add_app(2, args);
return mk_mul_app(k+1, m1.c_ptr()); return mk_mul_app(k+1, m1.c_ptr());
} }
template<typename Config>
bool poly_rewriter<Config>::is_times_minus_one(expr * n, expr* & r) const {
if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
r = to_app(n)->get_arg(1);
return true;
}
return false;
}
/**
\brief Return true if n is can be put into the form (+ v t) or (+ (- v) t)
\c inv = true will contain true if (- v) is found, and false otherwise.
*/
template<typename Config>
bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
if (!is_add(n) || is_ground(n))
return false;
ptr_buffer<expr> args;
v = 0;
expr * curr = to_app(n);
bool stop = false;
inv = false;
while (!stop) {
expr * arg;
expr * neg_arg;
if (is_add(curr)) {
arg = to_app(curr)->get_arg(0);
curr = to_app(curr)->get_arg(1);
}
else {
arg = curr;
stop = true;
}
if (is_ground(arg)) {
TRACE("model_checker_bug", tout << "pushing:\n" << mk_pp(arg, m()) << "\n";);
args.push_back(arg);
}
else if (is_var(arg)) {
if (v != 0)
return false; // already found variable
v = to_var(arg);
}
else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
if (v != 0)
return false; // already found variable
v = to_var(neg_arg);
inv = true;
}
else {
return false; // non ground term.
}
}
if (v == 0)
return false; // did not find variable
SASSERT(!args.empty());
mk_add(args.size(), args.c_ptr(), t);
return true;
}

2
src/smt/asserted_formulas.cpp
View file

@ -410,7 +410,7 @@ void asserted_formulas::apply_quasi_macros() {
TRACE("before_quasi_macros", display(tout);); TRACE("before_quasi_macros", display(tout););
expr_ref_vector new_exprs(m); expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m); proof_ref_vector new_prs(m);
quasi_macros proc(m, m_macro_manager, m_simplifier); quasi_macros proc(m, m_macro_manager);
while (proc(m_asserted_formulas.size() - m_asserted_qhead, while (proc(m_asserted_formulas.size() - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead,

246
src/smt/smt_model_finder.cpp
View file

@ -23,8 +23,6 @@ Revision History:
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h" #include "ast/array_decl_plugin.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/normal_forms/pull_quant.h" #include "ast/normal_forms/pull_quant.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
@ -392,9 +390,9 @@ namespace smt {
The idea is to create node objects based on the information produced by the quantifier_analyzer. The idea is to create node objects based on the information produced by the quantifier_analyzer.
*/ */
class auf_solver : public evaluator { class auf_solver : public evaluator {
ast_manager & m_manager; ast_manager & m;
arith_simplifier_plugin * m_asimp; arith_util m_arith;
bv_simplifier_plugin * m_bvsimp; bv_util m_bv;
ptr_vector<node> m_nodes; ptr_vector<node> m_nodes;
unsigned m_next_node_id; unsigned m_next_node_id;
key2node m_uvars; key2node m_uvars;
@ -466,16 +464,16 @@ namespace smt {
} }
public: public:
auf_solver(ast_manager & m, simplifier & s): auf_solver(ast_manager & m):
m_manager(m), m(m),
m_arith(m),
m_bv(m),
m_next_node_id(0), m_next_node_id(0),
m_context(0), m_context(0),
m_ks(m), m_ks(m),
m_model(0), m_model(0),
m_eval_cache_range(m), m_eval_cache_range(m),
m_new_constraints(0) { m_new_constraints(0) {
m_asimp = static_cast<arith_simplifier_plugin*>(s.get_plugin(m.mk_family_id("arith")));
m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.mk_family_id("bv")));
} }
virtual ~auf_solver() { virtual ~auf_solver() {
@ -488,12 +486,8 @@ namespace smt {
m_context = ctx; m_context = ctx;
} }
ast_manager & get_manager() const { return m_manager; } ast_manager & get_manager() const { return m; }
arith_simplifier_plugin * get_arith_simp() const { return m_asimp; }
bv_simplifier_plugin * get_bv_simp() const { return m_bvsimp; }
void reset() { void reset() {
flush_nodes(); flush_nodes();
m_nodes.reset(); m_nodes.reset();
@ -538,7 +532,7 @@ namespace smt {
void mk_instantiation_sets() { void mk_instantiation_sets() {
for (node* curr : m_nodes) { for (node* curr : m_nodes) {
if (curr->is_root()) { if (curr->is_root()) {
curr->mk_instantiation_set(m_manager); curr->mk_instantiation_set(m);
} }
} }
} }
@ -554,7 +548,7 @@ namespace smt {
for (auto const& kv : elems) { for (auto const& kv : elems) {
expr * n = kv.m_key; expr * n = kv.m_key;
expr * n_val = eval(n, true); expr * n_val = eval(n, true);
if (!n_val || !m_manager.is_value(n_val)) if (!n_val || !m.is_value(n_val))
to_delete.push_back(n); to_delete.push_back(n);
} }
for (expr* e : to_delete) { for (expr* e : to_delete) {
@ -568,7 +562,7 @@ namespace smt {
display_key2node(out, m_uvars); display_key2node(out, m_uvars);
display_A_f_is(out); display_A_f_is(out);
for (node* n : m_nodes) { for (node* n : m_nodes) {
n->display(out, m_manager); n->display(out, m);
} }
} }
@ -577,14 +571,14 @@ namespace smt {
if (m_eval_cache[model_completion].find(n, r)) { if (m_eval_cache[model_completion].find(n, r)) {
return r; return r;
} }
expr_ref tmp(m_manager); expr_ref tmp(m);
if (!m_model->eval(n, tmp, model_completion)) { if (!m_model->eval(n, tmp, model_completion)) {
r = 0; r = 0;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";); TRACE("model_finder", tout << "eval\n" << mk_pp(n, m) << "\n-----> null\n";);
} }
else { else {
r = tmp; r = tmp;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";); TRACE("model_finder", tout << "eval\n" << mk_pp(n, m) << "\n----->\n" << mk_pp(r, m) << "\n";);
} }
m_eval_cache[model_completion].insert(n, r); m_eval_cache[model_completion].insert(n, r);
m_eval_cache_range.push_back(r); m_eval_cache_range.push_back(r);
@ -636,7 +630,7 @@ namespace smt {
SASSERT(t_val != 0); SASSERT(t_val != 0);
bool found = false; bool found = false;
for (expr* v : ex_vals) { for (expr* v : ex_vals) {
if (!m_manager.are_distinct(t_val, v)) { if (!m.are_distinct(t_val, v)) {
found = true; found = true;
break; break;
} }
@ -652,7 +646,7 @@ namespace smt {
bool is_infinite(sort * s) const { bool is_infinite(sort * s) const {
// we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers. // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
return return
!m_manager.is_uninterp(s) && !m.is_uninterp(s) &&
s->is_infinite(); s->is_infinite();
} }
@ -665,7 +659,7 @@ namespace smt {
app * r = 0; app * r = 0;
if (m_sort2k.find(s, r)) if (m_sort2k.find(s, r))
return r; return r;
r = m_manager.mk_fresh_const("k", s); r = m.mk_fresh_const("k", s);
m_model->register_aux_decl(r->get_decl()); m_model->register_aux_decl(r->get_decl());
m_sort2k.insert(s, r); m_sort2k.insert(s, r);
m_ks.push_back(r); m_ks.push_back(r);
@ -680,7 +674,7 @@ namespace smt {
Remark: this method uses get_fresh_value, so it may fail. Remark: this method uses get_fresh_value, so it may fail.
*/ */
expr * get_k_interp(app * k) { expr * get_k_interp(app * k) {
sort * s = m_manager.get_sort(k); sort * s = m.get_sort(k);
SASSERT(is_infinite(s)); SASSERT(is_infinite(s));
func_decl * k_decl = k->get_decl(); func_decl * k_decl = k->get_decl();
expr * r = m_model->get_const_interp(k_decl); expr * r = m_model->get_const_interp(k_decl);
@ -691,7 +685,7 @@ namespace smt {
return 0; return 0;
m_model->register_decl(k_decl, r); m_model->register_decl(k_decl, r);
SASSERT(m_model->get_const_interp(k_decl) == r); SASSERT(m_model->get_const_interp(k_decl) == r);
TRACE("model_finder", tout << mk_pp(r, m_manager) << "\n";); TRACE("model_finder", tout << mk_pp(r, m) << "\n";);
return r; return r;
} }
@ -701,18 +695,18 @@ namespace smt {
It invokes get_k_interp that may fail. It invokes get_k_interp that may fail.
*/ */
bool assert_k_diseq_exceptions(app * k, ptr_vector<expr> const & exceptions) { bool assert_k_diseq_exceptions(app * k, ptr_vector<expr> const & exceptions) {
TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m_manager) << "\nexceptions:\n"; TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m) << "\nexceptions:\n";
for (expr * e : exceptions) tout << mk_pp(e, m_manager) << "\n";); for (expr * e : exceptions) tout << mk_pp(e, m) << "\n";);
expr * k_interp = get_k_interp(k); expr * k_interp = get_k_interp(k);
if (k_interp == 0) if (k_interp == 0)
return false; return false;
for (expr * ex : exceptions) { for (expr * ex : exceptions) {
expr * ex_val = eval(ex, true); expr * ex_val = eval(ex, true);
if (!m_manager.are_distinct(k_interp, ex_val)) { if (!m.are_distinct(k_interp, ex_val)) {
SASSERT(m_new_constraints); SASSERT(m_new_constraints);
// This constraint cannot be asserted into m_context during model construction. // This constraint cannot be asserted into m_context during model construction.
// We must save it, and assert it during a restart. // We must save it, and assert it during a restart.
m_new_constraints->push_back(m_manager.mk_not(m_manager.mk_eq(k, ex))); m_new_constraints->push_back(m.mk_not(m.mk_eq(k, ex)));
} }
} }
return true; return true;
@ -735,7 +729,7 @@ namespace smt {
return; return;
} }
sort * s = n->get_sort(); sort * s = n->get_sort();
TRACE("model_finder", tout << "trying to create k for " << mk_pp(s, m_manager) << ", is_infinite: " << is_infinite(s) << "\n";); TRACE("model_finder", tout << "trying to create k for " << mk_pp(s, m) << ", is_infinite: " << is_infinite(s) << "\n";);
if (is_infinite(s)) { if (is_infinite(s)) {
app * k = get_k_for(s); app * k = get_k_for(s);
if (assert_k_diseq_exceptions(k, exceptions)) { if (assert_k_diseq_exceptions(k, exceptions)) {
@ -758,28 +752,33 @@ namespace smt {
void add_mono_exceptions(node * n) { void add_mono_exceptions(node * n) {
SASSERT(n->is_mono_proj()); SASSERT(n->is_mono_proj());
sort * s = n->get_sort(); sort * s = n->get_sort();
arith_simplifier_plugin * as = get_arith_simp(); arith_rewriter arw(m);
bv_simplifier_plugin * bs = get_bv_simp(); bv_rewriter brw(m);
bool is_int = as->is_int_sort(s);
bool is_bv = bs->is_bv_sort(s);
if (!is_int && !is_bv)
return;
poly_simplifier_plugin * ps = as;
if (is_bv)
ps = bs;
ps->set_curr_sort(s);
expr_ref one(m_manager);
one = ps->mk_one();
ptr_vector<expr> const & exceptions = n->get_exceptions(); ptr_vector<expr> const & exceptions = n->get_exceptions();
for (expr * e : exceptions) { if (m_arith.is_int(s)) {
expr_ref e_plus_1(m_manager); expr_ref one(m_arith.mk_int(1), m);
expr_ref e_minus_1(m_manager); for (expr * e : exceptions) {
TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m_manager) << "\none:\n" << mk_ismt2_pp(one, m_manager) << "\n";); expr_ref e_plus_1(m_arith.mk_add(e, one), m);
ps->mk_add(e, one, e_plus_1); expr_ref e_minus_1(m_arith.mk_sub(e, one), m);
ps->mk_sub(e, one, e_minus_1); TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";);
// Note: exceptions come from quantifiers bodies. So, they have generation 0. // Note: exceptions come from quantifiers bodies. So, they have generation 0.
n->insert(e_plus_1, 0); n->insert(e_plus_1, 0);
n->insert(e_minus_1, 0); n->insert(e_minus_1, 0);
}
}
else if (m_bv.is_bv_sort(s)) {
expr_ref one(m_bv.mk_numeral(rational(1), s), m);
for (expr * e : exceptions) {
expr_ref e_plus_1(m_bv.mk_bv_add(e, one), m);
expr_ref e_minus_1(m_bv.mk_bv_sub(e, one), m);
TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";);
// Note: exceptions come from quantifiers bodies. So, they have generation 0.
n->insert(e_plus_1, 0);
n->insert(e_minus_1, 0);
}
}
else {
return;
} }
} }
@ -797,16 +796,17 @@ namespace smt {
} }
TRACE("model_finder_bug", tout << "values for the instantiation_set of @" << n->get_id() << "\n"; TRACE("model_finder_bug", tout << "values for the instantiation_set of @" << n->get_id() << "\n";
for (expr * v : values) { for (expr * v : values) {
tout << mk_pp(v, m_manager) << "\n"; tout << mk_pp(v, m) << "\n";
}); });
} }
template<class T>
struct numeral_lt { struct numeral_lt {
poly_simplifier_plugin * m_p; T& m_util;
numeral_lt(poly_simplifier_plugin * p):m_p(p) {} numeral_lt(T& a): m_util(a) {}
bool operator()(expr * e1, expr * e2) { bool operator()(expr* e1, expr* e2) {
rational v1, v2; rational v1, v2;
if (m_p->is_numeral(e1, v1) && m_p->is_numeral(e2, v2)) { if (m_util.is_numeral(e1, v1) && m_util.is_numeral(e2, v1)) {
return v1 < v2; return v1 < v2;
} }
else { else {
@ -815,15 +815,16 @@ namespace smt {
} }
}; };
struct signed_bv_lt { struct signed_bv_lt {
bv_simplifier_plugin * m_bs; bv_util& m_bv;
unsigned m_bv_size; unsigned m_bv_size;
signed_bv_lt(bv_simplifier_plugin * bs, unsigned sz):m_bs(bs), m_bv_size(sz) {} signed_bv_lt(bv_util& bv, unsigned sz):m_bv(bv), m_bv_size(sz) {}
bool operator()(expr * e1, expr * e2) { bool operator()(expr * e1, expr * e2) {
rational v1, v2; rational v1, v2;
if (m_bs->is_numeral(e1, v1) && m_bs->is_numeral(e2, v2)) { if (m_bv.is_numeral(e1, v1) && m_bv.is_numeral(e2, v2)) {
v1 = m_bs->norm(v1, m_bv_size, true); v1 = m_bv.norm(v1, m_bv_size, true);
v2 = m_bs->norm(v2, m_bv_size, true); v2 = m_bv.norm(v2, m_bv_size, true);
return v1 < v2; return v1 < v2;
} }
else { else {
@ -834,15 +835,14 @@ namespace smt {
void sort_values(node * n, ptr_buffer<expr> & values) { void sort_values(node * n, ptr_buffer<expr> & values) {
sort * s = n->get_sort(); sort * s = n->get_sort();
if (get_arith_simp()->is_arith_sort(s)) { if (m_arith.is_int(s) || m_arith.is_real(s)) {
std::sort(values.begin(), values.end(), numeral_lt(get_arith_simp())); std::sort(values.begin(), values.end(), numeral_lt<arith_util>(m_arith));
} }
else if (!n->is_signed_proj()) { else if (!n->is_signed_proj()) {
std::sort(values.begin(), values.end(), numeral_lt(get_bv_simp())); std::sort(values.begin(), values.end(), numeral_lt<bv_util>(m_bv));
} }
else { else {
bv_simplifier_plugin * bs = get_bv_simp(); std::sort(values.begin(), values.end(), signed_bv_lt(m_bv, m_bv.get_bv_size(s)));
std::sort(values.begin(), values.end(), signed_bv_lt(bs, bs->get_bv_size(s)));
} }
} }
@ -853,27 +853,25 @@ namespace smt {
if (values.empty()) return; if (values.empty()) return;
sort_values(n, values); sort_values(n, values);
sort * s = n->get_sort(); sort * s = n->get_sort();
arith_simplifier_plugin * as = get_arith_simp(); bool is_arith = m_arith.is_int(s) || m_arith.is_real(s);
bv_simplifier_plugin * bs = get_bv_simp();
bool is_arith = as->is_arith_sort(s);
bool is_signed = n->is_signed_proj(); bool is_signed = n->is_signed_proj();
unsigned sz = values.size(); unsigned sz = values.size();
SASSERT(sz > 0); SASSERT(sz > 0);
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s); func_decl * p = m.mk_fresh_func_decl(1, &s, s);
expr * pi = values[sz - 1]; expr * pi = values[sz - 1];
expr_ref var(m_manager); expr_ref var(m);
var = m_manager.mk_var(0, s); var = m.mk_var(0, s);
for (unsigned i = sz - 1; i >= 1; i--) { for (unsigned i = sz - 1; i >= 1; i--) {
expr_ref c(m_manager); expr_ref c(m);
if (is_arith) if (is_arith)
as->mk_lt(var, values[i], c); c = m_arith.mk_lt(var, values[i]);
else if (!is_signed) else if (!is_signed)
bs->mk_ult(var, values[i], c); c = m.mk_not(m_bv.mk_ule(values[i], var));
else else
bs->mk_slt(var, values[i], c); c = m.mk_not(m_bv.mk_sle(values[i], var));
pi = m_manager.mk_ite(c, values[i-1], pi); pi = m.mk_ite(c, values[i-1], pi);
} }
func_interp * rpi = alloc(func_interp, m_manager, 1); func_interp * rpi = alloc(func_interp, m, 1);
rpi->set_else(pi); rpi->set_else(pi);
m_model->register_aux_decl(p, rpi); m_model->register_aux_decl(p, rpi);
n->set_proj(p); n->set_proj(p);
@ -884,8 +882,8 @@ namespace smt {
ptr_buffer<expr> values; ptr_buffer<expr> values;
get_instantiation_set_values(n, values); get_instantiation_set_values(n, values);
sort * s = n->get_sort(); sort * s = n->get_sort();
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s); func_decl * p = m.mk_fresh_func_decl(1, &s, s);
func_interp * pi = alloc(func_interp, m_manager, 1); func_interp * pi = alloc(func_interp, m, 1);
m_model->register_aux_decl(p, pi); m_model->register_aux_decl(p, pi);
if (n->get_else()) { if (n->get_else()) {
expr * else_val = eval(n->get_else(), true); expr * else_val = eval(n->get_else(), true);
@ -916,7 +914,7 @@ namespace smt {
if (!r.contains(f)) { if (!r.contains(f)) {
func_interp * fi = m_model->get_func_interp(f); func_interp * fi = m_model->get_func_interp(f);
if (fi == 0) { if (fi == 0) {
fi = alloc(func_interp, m_manager, f->get_arity()); fi = alloc(func_interp, m, f->get_arity());
m_model->register_decl(f, fi); m_model->register_decl(f, fi);
SASSERT(fi->is_partial()); SASSERT(fi->is_partial());
} }
@ -938,7 +936,7 @@ namespace smt {
for (node * n : m_root_nodes) { for (node * n : m_root_nodes) {
SASSERT(n->is_root()); SASSERT(n->is_root());
sort * s = n->get_sort(); sort * s = n->get_sort();
if (m_manager.is_uninterp(s) && if (m.is_uninterp(s) &&
// Making all uninterpreted sorts finite. // Making all uninterpreted sorts finite.
// n->must_avoid_itself() && // n->must_avoid_itself() &&
!m_model->is_finite(s)) { !m_model->is_finite(s)) {
@ -962,7 +960,7 @@ namespace smt {
// If these module values "leak" inside the logical context, they may affect satisfiability. // If these module values "leak" inside the logical context, they may affect satisfiability.
// //
sort * ns = n->get_sort(); sort * ns = n->get_sort();
if (m_manager.is_fully_interp(ns)) { if (m.is_fully_interp(ns)) {
n->insert(m_model->get_some_value(ns), 0); n->insert(m_model->get_some_value(ns), 0);
} }
else { else {
@ -973,18 +971,18 @@ namespace smt {
sort2elems.insert(n->get_sort(), elems.begin()->m_key); sort2elems.insert(n->get_sort(), elems.begin()->m_key);
} }
} }
expr_ref_vector trail(m_manager); expr_ref_vector trail(m);
for (unsigned i = 0; i < need_fresh.size(); ++i) { for (unsigned i = 0; i < need_fresh.size(); ++i) {
expr * e; expr * e;
node* n = need_fresh[i]; node* n = need_fresh[i];
sort* s = n->get_sort(); sort* s = n->get_sort();
if (!sort2elems.find(s, e)) { if (!sort2elems.find(s, e)) {
e = m_manager.mk_fresh_const("elem", s); e = m.mk_fresh_const("elem", s);
trail.push_back(e); trail.push_back(e);
sort2elems.insert(s, e); sort2elems.insert(s, e);
} }
n->insert(e, 0); n->insert(e, 0);
TRACE("model_finder", tout << "fresh constant: " << mk_pp(e, m_manager) << "\n";); TRACE("model_finder", tout << "fresh constant: " << mk_pp(e, m) << "\n";);
} }
} }
@ -1037,13 +1035,13 @@ namespace smt {
if (fi->is_constant()) if (fi->is_constant())
continue; // there is no point in using the projection for fi, since fi is the constant function. continue; // there is no point in using the projection for fi, since fi is the constant function.
expr_ref_vector args(m_manager); expr_ref_vector args(m);
bool has_proj = false; bool has_proj = false;
for (unsigned i = 0; i < arity; i++) { for (unsigned i = 0; i < arity; i++) {
var * v = m_manager.mk_var(i, f->get_domain(i)); var * v = m.mk_var(i, f->get_domain(i));
func_decl * pi = get_f_i_proj(f, i); func_decl * pi = get_f_i_proj(f, i);
if (pi != 0) { if (pi != 0) {
args.push_back(m_manager.mk_app(pi, v)); args.push_back(m.mk_app(pi, v));
has_proj = true; has_proj = true;
} }
else { else {
@ -1052,11 +1050,11 @@ namespace smt {
} }
if (has_proj) { if (has_proj) {
// f_aux will be assigned to the old interpretation of f. // f_aux will be assigned to the old interpretation of f.
func_decl * f_aux = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range()); func_decl * f_aux = m.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range());
func_interp * new_fi = alloc(func_interp, m_manager, arity); func_interp * new_fi = alloc(func_interp, m, arity);
new_fi->set_else(m_manager.mk_app(f_aux, args.size(), args.c_ptr())); new_fi->set_else(m.mk_app(f_aux, args.size(), args.c_ptr()));
TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" << TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" <<
mk_pp(new_fi->get_else(), m_manager) << "\n";); mk_pp(new_fi->get_else(), m) << "\n";);
m_model->reregister_decl(f, new_fi, f_aux); m_model->reregister_decl(f, new_fi, f_aux);
} }
} }
@ -1256,21 +1254,21 @@ namespace smt {
if (A_f_i == S_j) { if (A_f_i == S_j) {
// there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset // there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset
// hope for the best... // hope for the best...
arith_simplifier_plugin * as = s.get_arith_simp();
bv_simplifier_plugin * bs = s.get_bv_simp();
node * S_j = s.get_uvar(q, m_var_j); node * S_j = s.get_uvar(q, m_var_j);
enode_vector::const_iterator it = ctx->begin_enodes_of(m_f); enode_vector::const_iterator it = ctx->begin_enodes_of(m_f);
enode_vector::const_iterator end = ctx->end_enodes_of(m_f); enode_vector::const_iterator end = ctx->end_enodes_of(m_f);
for (; it != end; it++) { for (; it != end; it++) {
enode * n = *it; enode * n = *it;
if (ctx->is_relevant(n)) { if (ctx->is_relevant(n)) {
arith_util arith(ctx->get_manager());
bv_util bv(ctx->get_manager());
enode * e_arg = n->get_arg(m_arg_i); enode * e_arg = n->get_arg(m_arg_i);
expr * arg = e_arg->get_owner(); expr * arg = e_arg->get_owner();
expr_ref arg_minus_k(ctx->get_manager()); expr_ref arg_minus_k(ctx->get_manager());
if (bs->is_bv(arg)) if (bv.is_bv(arg))
bs->mk_sub(arg, m_offset, arg_minus_k); arg_minus_k = bv.mk_bv_sub(arg, m_offset);
else else
as->mk_sub(arg, m_offset, arg_minus_k); arg_minus_k = arith.mk_sub(arg, m_offset);
S_j->insert(arg_minus_k, e_arg->get_generation()); S_j->insert(arg_minus_k, e_arg->get_generation());
} }
} }
@ -1290,20 +1288,20 @@ namespace smt {
template<bool PLUS> template<bool PLUS>
void copy_instances(node * from, node * to, auf_solver & s) { void copy_instances(node * from, node * to, auf_solver & s) {
arith_simplifier_plugin * as = s.get_arith_simp();
bv_simplifier_plugin * bs = s.get_bv_simp();
poly_simplifier_plugin * ps = as;
if (bs->is_bv_sort(from->get_sort()))
ps = bs;
instantiation_set const * from_s = from->get_instantiation_set(); instantiation_set const * from_s = from->get_instantiation_set();
obj_map<expr, unsigned> const & elems_s = from_s->get_elems(); obj_map<expr, unsigned> const & elems_s = from_s->get_elems();
arith_util arith(m_offset.get_manager());
bv_util bv(m_offset.get_manager());
bool is_bv = bv.is_bv_sort(from->get_sort());
for (auto const& kv : elems_s) { for (auto const& kv : elems_s) {
expr * n = kv.m_key; expr * n = kv.m_key;
expr_ref n_k(m_offset.get_manager()); expr_ref n_k(m_offset.get_manager());
if (PLUS) if (PLUS)
ps->mk_add(n, m_offset, n_k); n_k = is_bv ? bv.mk_bv_add(n, m_offset) : arith.mk_add(n, m_offset);
else else
ps->mk_sub(n, m_offset, n_k); n_k = is_bv ? bv.mk_bv_sub(n, m_offset) : arith.mk_sub(n, m_offset);
to->insert(n_k, kv.m_value); to->insert(n_k, kv.m_value);
} }
} }
@ -1897,11 +1895,8 @@ namespace smt {
m_info->insert_qinfo(qi); m_info->insert_qinfo(qi);
} }
arith_simplifier_plugin * get_arith_simp() const { return m_mutil.get_arith_simp(); } bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
bv_simplifier_plugin * get_bv_simp() const { return m_mutil.get_bv_simp(); } return m_mutil.is_var_plus_ground(n, inv, v, t);
bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) const {
return get_arith_simp()->is_var_plus_ground(n, inv, v, t) || get_bv_simp()->is_var_plus_ground(n, inv, v, t);
} }
bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) { bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) {
@ -1917,10 +1912,7 @@ namespace smt {
} }
bool is_zero(expr * n) const { bool is_zero(expr * n) const {
if (get_bv_simp()->is_bv(n)) return m_mutil.is_zero_safe(n);
return get_bv_simp()->is_zero_safe(n);
else
return get_arith_simp()->is_zero_safe(n);
} }
bool is_times_minus_one(expr * n, expr * & arg) const { bool is_times_minus_one(expr * n, expr * & arg) const {
@ -1951,7 +1943,7 @@ namespace smt {
m_mutil.mk_add(t1, t2, r); m_mutil.mk_add(t1, t2, r);
} }
bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) const { bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) {
inv = false; // true if invert the sign inv = false; // true if invert the sign
TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";); TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";);
if (is_var(lhs) && is_ground(rhs)) { if (is_var(lhs) && is_ground(rhs)) {
@ -1986,12 +1978,12 @@ namespace smt {
return false; return false;
} }
bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const { bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) {
bool inv; bool inv;
return is_var_and_ground(lhs, rhs, v, t, inv); return is_var_and_ground(lhs, rhs, v, t, inv);
} }
bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const { bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) {
if (!is_app(n)) if (!is_app(n))
return false; return false;
if (m_manager.is_eq(n)) if (m_manager.is_eq(n))
@ -1999,7 +1991,7 @@ namespace smt {
return false; return false;
} }
bool is_var_minus_var(expr * n, var * & v1, var * & v2) const { bool is_var_minus_var(expr * n, var * & v1, var * & v2) {
if (!is_add(n)) if (!is_add(n))
return false; return false;
expr * arg1 = to_app(n)->get_arg(0); expr * arg1 = to_app(n)->get_arg(0);
@ -2018,7 +2010,7 @@ namespace smt {
return true; return true;
} }
bool is_var_and_var(expr * lhs, expr * rhs, var * & v1, var * & v2) const { bool is_var_and_var(expr * lhs, expr * rhs, var * & v1, var * & v2) {
if (is_var(lhs) && is_var(rhs)) { if (is_var(lhs) && is_var(rhs)) {
v1 = to_var(lhs); v1 = to_var(lhs);
v2 = to_var(rhs); v2 = to_var(rhs);
@ -2029,11 +2021,11 @@ namespace smt {
(is_var_minus_var(rhs, v1, v2) && is_zero(lhs)); (is_var_minus_var(rhs, v1, v2) && is_zero(lhs));
} }
bool is_x_eq_y_atom(expr * n, var * & v1, var * & v2) const { bool is_x_eq_y_atom(expr * n, var * & v1, var * & v2) {
return m_manager.is_eq(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2); return m_manager.is_eq(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2);
} }
bool is_x_gle_y_atom(expr * n, var * & v1, var * & v2) const { bool is_x_gle_y_atom(expr * n, var * & v1, var * & v2) {
return is_le_ge(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2); return is_le_ge(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2);
} }
@ -2379,10 +2371,10 @@ namespace smt {
public: public:
quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s): quantifier_analyzer(model_finder& mf, ast_manager & m):
m_mf(mf), m_mf(mf),
m_manager(m), m_manager(m),
m_mutil(m, s), m_mutil(m),
m_array_util(m), m_array_util(m),
m_arith_util(m), m_arith_util(m),
m_bv_util(m), m_bv_util(m),
@ -3152,11 +3144,11 @@ namespace smt {
// //
// ----------------------------------- // -----------------------------------
model_finder::model_finder(ast_manager & m, simplifier & s): model_finder::model_finder(ast_manager & m):
m_manager(m), m_manager(m),
m_context(0), m_context(0),
m_analyzer(alloc(quantifier_analyzer, *this, m, s)), m_analyzer(alloc(quantifier_analyzer, *this, m)),
m_auf_solver(alloc(auf_solver, m, s)), m_auf_solver(alloc(auf_solver, m)),
m_dependencies(m), m_dependencies(m),
m_sm_solver(alloc(simple_macro_solver, m, m_q2info)), m_sm_solver(alloc(simple_macro_solver, m, m_q2info)),
m_hint_solver(alloc(hint_solver, m, m_q2info)), m_hint_solver(alloc(hint_solver, m, m_q2info)),

3
src/smt/smt_model_finder.h
View file

@ -48,7 +48,6 @@ Revision History:
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/func_decl_dependencies.h" #include "ast/func_decl_dependencies.h"
#include "ast/simplifier/simplifier.h"
#include "smt/proto_model/proto_model.h" #include "smt/proto_model/proto_model.h"
#include "util/cooperate.h" #include "util/cooperate.h"
#include "tactic/tactic_exception.h" #include "tactic/tactic_exception.h"
@ -107,7 +106,7 @@ namespace smt {
public: public:
model_finder(ast_manager & m, simplifier & s); model_finder(ast_manager & m);
~model_finder(); ~model_finder();
void set_context(context * ctx); void set_context(context * ctx);

2
src/smt/smt_quantifier.cpp
View file

@ -434,7 +434,7 @@ namespace smt {
m_mam = mk_mam(*m_context); m_mam = mk_mam(*m_context);
m_lazy_mam = mk_mam(*m_context); m_lazy_mam = mk_mam(*m_context);
m_model_finder = alloc(model_finder, m, m_context->get_simplifier()); m_model_finder = alloc(model_finder, m);
m_model_checker = alloc(model_checker, m, *m_fparams, *(m_model_finder.get())); m_model_checker = alloc(model_checker, m, *m_fparams, *(m_model_finder.get()));
m_model_finder->set_context(m_context); m_model_finder->set_context(m_context);

2
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -63,7 +63,7 @@ class quasi_macros_tactic : public tactic {
simp.register_plugin(bvsimp); simp.register_plugin(bvsimp);
macro_manager mm(m_manager, simp); macro_manager mm(m_manager, simp);
quasi_macros qm(m_manager, mm, simp); quasi_macros qm(m_manager, mm);
bool more = true; bool more = true;
expr_ref_vector forms(m_manager), new_forms(m_manager); expr_ref_vector forms(m_manager), new_forms(m_manager);