mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-03 14:58:14 -07:00
parent c6722859c2 059bad909a
commit 5c8fa80c3f
8 changed files with 222 additions and 657 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

468
src/ast/simplifier/arith_simplifier_plugin.cpp
View file

@ -1,468 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
arith_simplifier_plugin.cpp
Abstract:
Simplifier for the arithmetic family.
Author:
Leonardo (leonardo) 2008-01-08
--*/
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
arith_simplifier_plugin::~arith_simplifier_plugin() {
}
arith_simplifier_plugin::arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p):
poly_simplifier_plugin(symbol("arith"), m, OP_ADD, OP_MUL, OP_UMINUS, OP_SUB, OP_NUM),
m_params(p),
m_util(m),
m_bsimp(b),
m_int_zero(m),
m_real_zero(m) {
m_int_zero = m_util.mk_numeral(rational(0), true);
m_real_zero = m_util.mk_numeral(rational(0), false);
}
/**
\brief Return true if the first monomial of t is negative.
*/
bool arith_simplifier_plugin::is_neg_poly(expr * t) const {
if (m_util.is_add(t)) {
t = to_app(t)->get_arg(0);
}
if (m_util.is_mul(t)) {
t = to_app(t)->get_arg(0);
rational r;
if (is_numeral(t, r))
return r.is_neg();
}
return false;
}
void arith_simplifier_plugin::get_monomial_gcd(expr_ref_vector& monomials, numeral& g) {
g = numeral::zero();
numeral n;
for (unsigned i = 0; !g.is_one() && i < monomials.size(); ++i) {
expr* e = monomials[i].get();
if (is_numeral(e, n)) {
g = gcd(abs(n), g);
}
else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {
g = gcd(abs(n), g);
}
else {
g = numeral::one();
return;
}
}
if (g.is_zero()) {
g = numeral::one();
}
}
void arith_simplifier_plugin::div_monomial(expr_ref_vector& monomials, numeral const& g) {
numeral n;
for (unsigned i = 0; i < monomials.size(); ++i) {
expr* e = monomials[i].get();
if (is_numeral(e, n)) {
SASSERT((n/g).is_int());
monomials[i] = mk_numeral(n/g);
}
else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {
SASSERT((n/g).is_int());
monomials[i] = mk_mul(n/g, to_app(e)->get_arg(1));
}
else {
UNREACHABLE();
}
}
}
void arith_simplifier_plugin::gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k) {
numeral g, n;
get_monomial_gcd(monomials, g);
g = gcd(abs(k), g);
if (g.is_one()) {
return;
}
SASSERT(g.is_pos());
k = k / g;
div_monomial(monomials, g);
}
template<arith_simplifier_plugin::op_kind Kind>
void arith_simplifier_plugin::mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(arg1);
bool is_int = m_curr_sort->get_decl_kind() == INT_SORT;
expr_ref_vector monomials(m_manager);
rational k;
TRACE("arith_eq_bug", tout << mk_ismt2_pp(arg1, m_manager) << "\n" << mk_ismt2_pp(arg2, m_manager) << "\n";);
process_sum_of_monomials(false, arg1, monomials, k);
process_sum_of_monomials(true, arg2, monomials, k);
k.neg();
if (is_int) {
numeral g;
get_monomial_gcd(monomials, g);
if (!g.is_one()) {
div_monomial(monomials, g);
switch(Kind) {
case LE:
//
// g*monmials' <= k
// <=>
// monomials' <= floor(k/g)
//
k = floor(k/g);
break;
case GE:
//
// g*monmials' >= k
// <=>
// monomials' >= ceil(k/g)
//
k = ceil(k/g);
break;
case EQ:
k = k/g;
if (!k.is_int()) {
result = m_manager.mk_false();
return;
}
break;
}
}
}
expr_ref lhs(m_manager);
mk_sum_of_monomials(monomials, lhs);
if (m_util.is_numeral(lhs)) {
SASSERT(lhs == mk_zero());
if (( Kind == LE && numeral::zero() <= k) ||
( Kind == GE && numeral::zero() >= k) ||
( Kind == EQ && numeral::zero() == k))
result = m_manager.mk_true();
else
result = m_manager.mk_false();
}
else {
if (is_neg_poly(lhs)) {
expr_ref neg_lhs(m_manager);
mk_uminus(lhs, neg_lhs);
lhs = neg_lhs;
k.neg();
expr * rhs = m_util.mk_numeral(k, is_int);
switch (Kind) {
case LE:
result = m_util.mk_ge(lhs, rhs);
break;
case GE:
result = m_util.mk_le(lhs, rhs);
break;
case EQ:
result = m_manager.mk_eq(lhs, rhs);
break;
}
}
else {
expr * rhs = m_util.mk_numeral(k, is_int);
switch (Kind) {
case LE:
result = m_util.mk_le(lhs, rhs);
break;
case GE:
result = m_util.mk_ge(lhs, rhs);
break;
case EQ:
result = m_manager.mk_eq(lhs, rhs);
break;
}
}
}
}
void arith_simplifier_plugin::mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result) {
mk_le_ge_eq_core<EQ>(arg1, arg2, result);
}
void arith_simplifier_plugin::mk_le(expr * arg1, expr * arg2, expr_ref & result) {
mk_le_ge_eq_core<LE>(arg1, arg2, result);
}
void arith_simplifier_plugin::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
mk_le_ge_eq_core<GE>(arg1, arg2, result);
}
void arith_simplifier_plugin::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
expr_ref tmp(m_manager);
mk_le(arg2, arg1, tmp);
m_bsimp.mk_not(tmp, result);
}
void arith_simplifier_plugin::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
expr_ref tmp(m_manager);
mk_le(arg1, arg2, tmp);
m_bsimp.mk_not(tmp, result);
}
void arith_simplifier_plugin::gcd_normalize(numeral & coeff, expr_ref& term) {
if (!abs(coeff).is_one()) {
set_curr_sort(term);
SASSERT(m_curr_sort->get_decl_kind() == INT_SORT);
expr_ref_vector monomials(m_manager);
rational k;
monomials.push_back(mk_numeral(numeral(coeff), true));
process_sum_of_monomials(false, term, monomials, k);
gcd_reduce_monomial(monomials, k);
numeral coeff1;
if (!is_numeral(monomials[0].get(), coeff1)) {
UNREACHABLE();
}
if (coeff1 == coeff) {
return;
}
monomials[0] = mk_numeral(k, true);
coeff = coeff1;
mk_sum_of_monomials(monomials, term);
}
}
void arith_simplifier_plugin::mk_div(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(arg1);
numeral v1, v2;
bool is_int;
if (m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
SASSERT(!is_int);
if (m_util.is_numeral(arg1, v1, is_int))
result = m_util.mk_numeral(v1/v2, false);
else {
numeral k(1);
k /= v2;
expr_ref inv_arg2(m_util.mk_numeral(k, false), m_manager);
mk_mul(inv_arg2, arg1, result);
}
}
else
result = m_util.mk_div(arg1, arg2);
}
void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(arg1);
numeral v1, v2;
bool is_int;
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero())
result = m_util.mk_numeral(div(v1, v2), is_int);
else
result = m_util.mk_idiv(arg1, arg2);
}
void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) {
SASSERT(m_util.is_int(e));
SASSERT(k.is_int() && k.is_pos());
numeral n;
bool is_int;
if (depth == 0) {
result = e;
}
else if (is_add(e) || is_mul(e)) {
expr_ref_vector args(m_manager);
expr_ref tmp(m_manager);
app* a = to_app(e);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
prop_mod_const(a->get_arg(i), depth - 1, k, tmp);
args.push_back(tmp);
}
reduce(a->get_decl(), args.size(), args.c_ptr(), result);
}
else if (m_util.is_numeral(e, n, is_int) && is_int) {
result = mk_numeral(mod(n, k), true);
}
else {
result = e;
}
}
void arith_simplifier_plugin::mk_mod(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(arg1);
numeral v1, v2;
bool is_int;
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
result = m_util.mk_numeral(mod(v1, v2), is_int);
}
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
result = m_util.mk_numeral(numeral(0), true);
}
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos()) {
expr_ref tmp(m_manager);
prop_mod_const(arg1, 5, v2, tmp);
result = m_util.mk_mod(tmp, arg2);
}
else {
result = m_util.mk_mod(arg1, arg2);
}
}
void arith_simplifier_plugin::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(arg1);
numeral v1, v2;
bool is_int;
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
numeral m = mod(v1, v2);
//
// rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
//
if (v2.is_neg()) {
m.neg();
}
result = m_util.mk_numeral(m, is_int);
}
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
result = m_util.mk_numeral(numeral(0), true);
}
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
expr_ref tmp(m_manager);
prop_mod_const(arg1, 5, v2, tmp);
result = m_util.mk_mod(tmp, arg2);
if (v2.is_neg()) {
result = m_util.mk_uminus(result);
}
}
else {
result = m_util.mk_rem(arg1, arg2);
}
}
void arith_simplifier_plugin::mk_to_real(expr * arg, expr_ref & result) {
numeral v;
if (m_util.is_numeral(arg, v))
result = m_util.mk_numeral(v, false);
else
result = m_util.mk_to_real(arg);
}
void arith_simplifier_plugin::mk_to_int(expr * arg, expr_ref & result) {
numeral v;
if (m_util.is_numeral(arg, v))
result = m_util.mk_numeral(floor(v), true);
else if (m_util.is_to_real(arg))
result = to_app(arg)->get_arg(0);
else
result = m_util.mk_to_int(arg);
}
void arith_simplifier_plugin::mk_is_int(expr * arg, expr_ref & result) {
numeral v;
if (m_util.is_numeral(arg, v))
result = v.is_int()?m_manager.mk_true():m_manager.mk_false();
else if (m_util.is_to_real(arg))
result = m_manager.mk_true();
else
result = m_util.mk_is_int(arg);
}
bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
SASSERT(f->get_family_id() == m_fid);
TRACE("arith_simplifier_plugin", tout << mk_pp(f, m_manager) << "\n";
for (unsigned i = 0; i < num_args; i++) tout << mk_pp(args[i], m_manager) << "\n";);
arith_op_kind k = static_cast<arith_op_kind>(f->get_decl_kind());
switch (k) {
case OP_NUM: return false;
case OP_LE: if (m_presimp) return false; SASSERT(num_args == 2); mk_le(args[0], args[1], result); break;
case OP_GE: if (m_presimp) return false; SASSERT(num_args == 2); mk_ge(args[0], args[1], result); break;
case OP_LT: if (m_presimp) return false; SASSERT(num_args == 2); mk_lt(args[0], args[1], result); break;
case OP_GT: if (m_presimp) return false; SASSERT(num_args == 2); mk_gt(args[0], args[1], result); break;
case OP_ADD: mk_add(num_args, args, result); break;
case OP_SUB: mk_sub(num_args, args, result); break;
case OP_UMINUS: SASSERT(num_args == 1); mk_uminus(args[0], result); break;
case OP_MUL:
mk_mul(num_args, args, result);
TRACE("arith_simplifier_plugin", tout << mk_pp(result, m_manager) << "\n";);
break;
case OP_DIV: SASSERT(num_args == 2); mk_div(args[0], args[1], result); break;
case OP_IDIV: SASSERT(num_args == 2); mk_idiv(args[0], args[1], result); break;
case OP_REM: SASSERT(num_args == 2); mk_rem(args[0], args[1], result); break;
case OP_MOD: SASSERT(num_args == 2); mk_mod(args[0], args[1], result); break;
case OP_TO_REAL: SASSERT(num_args == 1); mk_to_real(args[0], result); break;
case OP_TO_INT: SASSERT(num_args == 1); mk_to_int(args[0], result); break;
case OP_IS_INT: SASSERT(num_args == 1); mk_is_int(args[0], result); break;
case OP_POWER: SASSERT(num_args == 2); mk_power(args[0], args[1], result); break;
case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break;
case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
default:
return false;
}
TRACE("arith_simplifier_plugin", tout << mk_pp(result.get(), m_manager) << "\n";);
return true;
}
void arith_simplifier_plugin::mk_power(expr* x, expr* y, expr_ref& result) {
rational a, b;
if (is_numeral(y, b) && b.is_one()) {
result = x;
return;
}
if (is_numeral(x, a) && is_numeral(y, b) && b.is_unsigned()) {
if (b.is_zero() && !a.is_zero()) {
result = m_util.mk_numeral(rational(1), m_manager.get_sort(x));
return;
}
if (!b.is_zero()) {
result = m_util.mk_numeral(power(a, b.get_unsigned()), m_manager.get_sort(x));
return;
}
}
result = m_util.mk_power(x, y);
}
void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) {
expr_ref c(m_manager);
expr_ref m_arg(m_manager);
mk_uminus(arg, m_arg);
mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg)), c);
m_bsimp.mk_ite(c, arg, m_arg, result);
}
bool arith_simplifier_plugin::is_arith_term(expr * n) const {
return n->get_kind() == AST_APP && to_app(n)->get_family_id() == m_fid;
}
bool arith_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
TRACE("reduce_eq_bug", tout << mk_ismt2_pp(lhs, m_manager) << "\n" << mk_ismt2_pp(rhs, m_manager) << "\n";);
set_reduce_invoked();
if (m_presimp) {
return false;
}
if (m_params.m_arith_expand_eqs) {
expr_ref le(m_manager), ge(m_manager);
mk_le_ge_eq_core<LE>(lhs, rhs, le);
mk_le_ge_eq_core<GE>(lhs, rhs, ge);
m_bsimp.mk_and(le, ge, result);
return true;
}
if (m_params.m_arith_process_all_eqs || is_arith_term(lhs) || is_arith_term(rhs)) {
mk_arith_eq(lhs, rhs, result);
return true;
}
return false;
}

97
src/ast/simplifier/arith_simplifier_plugin.h
View file

@ -1,97 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
arith_simplifier_plugin.h
Abstract:
Simplifier for the arithmetic family.
Author:
Leonardo (leonardo) 2008-01-08
--*/
#ifndef ARITH_SIMPLIFIER_PLUGIN_H_
#define ARITH_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/poly_simplifier_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/simplifier/arith_simplifier_params.h"
/**
\brief Simplifier for the arith family.
*/
class arith_simplifier_plugin : public poly_simplifier_plugin {
public:
enum op_kind {
LE, GE, EQ
};
protected:
arith_simplifier_params & m_params;
arith_util m_util;
basic_simplifier_plugin & m_bsimp;
expr_ref m_int_zero;
expr_ref m_real_zero;
bool is_neg_poly(expr * t) const;
template<op_kind k>
void mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result);
void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result);
void gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k);
void div_monomial(expr_ref_vector& monomials, numeral const& g);
void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
public:
arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);
~arith_simplifier_plugin();
arith_util & get_arith_util() { return m_util; }
virtual numeral norm(const numeral & n) { return n; }
virtual bool is_numeral(expr * n, rational & val) const { bool f; return m_util.is_numeral(n, val, f); }
bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
virtual bool is_minus_one(expr * n) const { numeral tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
virtual expr * get_zero(sort * s) const { return m_util.is_int(s) ? m_int_zero.get() : m_real_zero.get(); }
virtual app * mk_numeral(numeral const & n) { return m_util.mk_numeral(n, m_curr_sort->get_decl_kind() == INT_SORT); }
app * mk_numeral(numeral const & n, bool is_int) { return m_util.mk_numeral(n, is_int); }
bool is_int_sort(sort const * s) const { return m_util.is_int(s); }
bool is_real_sort(sort const * s) const { return m_util.is_real(s); }
bool is_arith_sort(sort const * s) const { return is_int_sort(s) || is_real_sort(s); }
bool is_int(expr const * n) const { return m_util.is_int(n); }
bool is_le(expr const * n) const { return m_util.is_le(n); }
bool is_ge(expr const * n) const { return m_util.is_ge(n); }
virtual bool is_le_ge(expr * n) const { return is_le(n) || is_ge(n); }
void mk_le(expr * arg1, expr * arg2, expr_ref & result);
void mk_ge(expr * arg1, expr * arg2, expr_ref & result);
void mk_lt(expr * arg1, expr * arg2, expr_ref & result);
void mk_gt(expr * arg1, expr * arg2, expr_ref & result);
void mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result);
void mk_div(expr * arg1, expr * arg2, expr_ref & result);
void mk_idiv(expr * arg1, expr * arg2, expr_ref & result);
void mk_mod(expr * arg1, expr * arg2, expr_ref & result);
void mk_rem(expr * arg1, expr * arg2, expr_ref & result);
void mk_to_real(expr * arg, expr_ref & result);
void mk_to_int(expr * arg, expr_ref & result);
void mk_is_int(expr * arg, expr_ref & result);
void mk_power(expr* x, expr* y, expr_ref& result);
void mk_abs(expr * arg, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
bool is_arith_term(expr * n) const;
void gcd_normalize(numeral & coeff, expr_ref& term);
};
#endif /* ARITH_SIMPLIFIER_PLUGIN_H_ */

102
src/cmd_context/cmd_context.cpp
View file

@ -229,6 +229,28 @@ func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const *
return find(num_args, sorts.c_ptr(), range); return find(num_args, sorts.c_ptr(), range);
} }
unsigned func_decls::get_num_entries() const {
if (!more_than_one())
return 1;
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
return fs->size();
}
func_decl * func_decls::get_entry(unsigned inx) {
if (!more_than_one()) {
SASSERT(inx == 0);
return first();
}
else {
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
auto b = fs->begin();
for (unsigned i = 0; i < inx; i++)
b++;
return *b;
}
}
void macro_decls::finalize(ast_manager& m) { void macro_decls::finalize(ast_manager& m) {
for (auto v : *m_decls) m.dec_ref(v.m_body); for (auto v : *m_decls) m.dec_ref(v.m_body);
dealloc(m_decls); dealloc(m_decls);
@ -288,13 +310,13 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
} }
else { else {
VERIFY(decls.insert(m(), arity, domain, t)); VERIFY(decls.insert(m(), arity, domain, t));
} }
} }
void cmd_context::erase_macro(symbol const& s) { void cmd_context::erase_macro(symbol const& s) {
macro_decls decls; macro_decls decls;
VERIFY(m_macros.find(s, decls)); VERIFY(m_macros.find(s, decls));
decls.erase_last(m()); decls.erase_last(m());
} }
bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const { bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const {
@ -864,11 +886,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
} }
// //
// disable warning given the current way they are used // disable warning given the current way they are used
// (Z3 will here silently assume and not check the definitions to be well founded, // (Z3 will here silently assume and not check the definitions to be well founded,
// and please use HSF for everything else). // and please use HSF for everything else).
// //
if (false && !ids.empty() && !m_rec_fun_declared) { if (false && !ids.empty() && !m_rec_fun_declared) {
warning_msg("recursive function definitions are assumed well-founded"); warning_msg("recursive function definitions are assumed well-founded");
m_rec_fun_declared = true; m_rec_fun_declared = true;
} }
@ -947,7 +969,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
return f; return f;
} }
if (contains_macro(s, arity, domain)) if (contains_macro(s, arity, domain))
throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
if (num_indices > 0) if (num_indices > 0)
@ -1298,7 +1320,7 @@ void cmd_context::push(unsigned n) {
push(); push();
} }
void cmd_context::restore_func_decls(unsigned old_sz) { void cmd_context::restore_func_decls(unsigned old_sz) {
SASSERT(old_sz <= m_func_decls_stack.size()); SASSERT(old_sz <= m_func_decls_stack.size());
svector<sf_pair>::iterator it = m_func_decls_stack.begin() + old_sz; svector<sf_pair>::iterator it = m_func_decls_stack.begin() + old_sz;
svector<sf_pair>::iterator end = m_func_decls_stack.end(); svector<sf_pair>::iterator end = m_func_decls_stack.end();
@ -1400,7 +1422,7 @@ void cmd_context::pop(unsigned n) {
restore_assertions(s.m_assertions_lim); restore_assertions(s.m_assertions_lim);
restore_psort_inst(s.m_psort_inst_stack_lim); restore_psort_inst(s.m_psort_inst_stack_lim);
m_scopes.shrink(new_lvl); m_scopes.shrink(new_lvl);
} }
void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) { void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) {
@ -1470,6 +1492,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
} }
display_sat_result(r); display_sat_result(r);
if (r == l_true) { if (r == l_true) {
complete_model();
validate_model(); validate_model();
} }
validate_check_sat_result(r); validate_check_sat_result(r);
@ -1528,7 +1551,7 @@ void cmd_context::reset_assertions() {
if (m_solver) m_solver->push(); if (m_solver) m_solver->push();
} }
} }
void cmd_context::display_model(model_ref& mdl) { void cmd_context::display_model(model_ref& mdl) {
if (mdl) { if (mdl) {
@ -1612,6 +1635,65 @@ struct contains_array_op_proc {
void operator()(quantifier * n) {} void operator()(quantifier * n) {}
}; };
/**
\brief Complete the model if necessary.
*/
void cmd_context::complete_model() {
if (!is_model_available() ||
gparams::get_value("model.completion") != "true")
return;
model_ref md;
get_check_sat_result()->get_model(md);
SASSERT(md.get() != 0);
params_ref p;
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
p.set_uint("sort_store", true);
p.set_bool("completion", true);
model_evaluator evaluator(*(md.get()), p);
evaluator.set_expand_array_equalities(false);
scoped_rlimit _rlimit(m().limit(), 0);
cancel_eh<reslimit> eh(m().limit());
expr_ref r(m());
scoped_ctrl_c ctrlc(eh);
for (auto kd : m_psort_decls) {
symbol const & k = kd.m_key;
psort_decl * v = kd.m_value;
if (v->is_user_decl()) {
SASSERT(!v->has_var_params());
IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
ptr_vector<sort> param_sorts(v->get_num_params(), m().mk_bool_sort());
sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.c_ptr());
if (!md->has_uninterpreted_sort(srt)) {
expr * singleton = m().get_some_value(srt);
md->register_usort(srt, 1, &singleton);
}
}
}
for (auto kd : m_func_decls) {
symbol const & k = kd.m_key;
func_decls & v = kd.m_value;
IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
for (unsigned i = 0; i < v.get_num_entries(); i++) {
func_decl * f = v.get_entry(i);
if (!md->has_interpretation(f)) {
sort * range = f->get_range();
expr * some_val = m().get_some_value(range);
if (f->get_arity() > 0) {
func_interp * fi = alloc(func_interp, m(), f->get_arity());
fi->set_else(some_val);
md->register_decl(f, fi);
}
else
md->register_decl(f, some_val);
}
}
}
}
/** /**
\brief Check if the current model satisfies the quantifier free formulas. \brief Check if the current model satisfies the quantifier free formulas.
*/ */
@ -1891,7 +1973,7 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
} }
if (m_owner.m_scopes.size() > 0) { if (m_owner.m_scopes.size() > 0) {
m_owner.m_psort_inst_stack.push_back(pd); m_owner.m_psort_inst_stack.push_back(pd);
} }
} }

47
src/cmd_context/cmd_context.h
View file

@ -8,7 +8,7 @@ Module Name:
Abstract: Abstract:
Ultra-light command context. Ultra-light command context.
It provides a generic command pluging infrastructure. It provides a generic command pluging infrastructure.
A command context also provides names (aka symbols) to Z3 objects. A command context also provides names (aka symbols) to Z3 objects.
These names are used to reference Z3 objects in commands. These names are used to reference Z3 objects in commands.
Author: Author:
@ -58,6 +58,8 @@ public:
func_decl * first() const; func_decl * first() const;
func_decl * find(unsigned arity, sort * const * domain, sort * range) const; func_decl * find(unsigned arity, sort * const * domain, sort * range) const;
func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const; func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const;
unsigned get_num_entries() const;
func_decl * get_entry(unsigned inx);
}; };
struct macro_decl { struct macro_decl {
@ -66,18 +68,18 @@ struct macro_decl {
macro_decl(unsigned arity, sort *const* domain, expr* body): macro_decl(unsigned arity, sort *const* domain, expr* body):
m_domain(arity, domain), m_body(body) {} m_domain(arity, domain), m_body(body) {}
void dec_ref(ast_manager& m) { m.dec_ref(m_body); } void dec_ref(ast_manager& m) { m.dec_ref(m_body); }
}; };
class macro_decls { class macro_decls {
vector<macro_decl>* m_decls; vector<macro_decl>* m_decls;
public: public:
macro_decls() { m_decls = 0; } macro_decls() { m_decls = 0; }
void finalize(ast_manager& m); void finalize(ast_manager& m);
bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body); bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body);
expr* find(unsigned arity, sort *const* domain) const; expr* find(unsigned arity, sort *const* domain) const;
void erase_last(ast_manager& m); void erase_last(ast_manager& m);
vector<macro_decl>::iterator begin() const { return m_decls->begin(); } vector<macro_decl>::iterator begin() const { return m_decls->begin(); }
vector<macro_decl>::iterator end() const { return m_decls->end(); } vector<macro_decl>::iterator end() const { return m_decls->end(); }
@ -158,11 +160,11 @@ public:
enum status { enum status {
UNSAT, SAT, UNKNOWN UNSAT, SAT, UNKNOWN
}; };
enum check_sat_state { enum check_sat_state {
css_unsat, css_sat, css_unknown, css_clear css_unsat, css_sat, css_unknown, css_clear
}; };
typedef std::pair<unsigned, expr*> macro; typedef std::pair<unsigned, expr*> macro;
struct scoped_watch { struct scoped_watch {
@ -188,7 +190,7 @@ protected:
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_processing_pareto; // used when re-entering check-sat for pareto front. bool m_processing_pareto; // used when re-entering check-sat for pareto front.
bool m_exit_on_error; bool m_exit_on_error;
static std::ostringstream g_error_stream; static std::ostringstream g_error_stream;
ast_manager * m_manager; ast_manager * m_manager;
@ -200,7 +202,7 @@ protected:
check_logic m_check_logic; check_logic m_check_logic;
stream_ref m_regular; stream_ref m_regular;
stream_ref m_diagnostic; stream_ref m_diagnostic;
dictionary<cmd*> m_cmds; dictionary<cmd*> m_cmds;
dictionary<builtin_decl> m_builtin_decls; dictionary<builtin_decl> m_builtin_decls;
scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
dictionary<object_ref*> m_object_refs; // anything that can be named. dictionary<object_ref*> m_object_refs; // anything that can be named.
@ -217,7 +219,7 @@ protected:
svector<symbol> m_macros_stack; svector<symbol> m_macros_stack;
ptr_vector<pdecl> m_psort_inst_stack; ptr_vector<pdecl> m_psort_inst_stack;
// //
ptr_vector<pdecl> m_aux_pdecls; ptr_vector<pdecl> m_aux_pdecls;
ptr_vector<expr> m_assertions; ptr_vector<expr> m_assertions;
std::vector<std::string> m_assertion_strings; std::vector<std::string> m_assertion_strings;
@ -236,7 +238,7 @@ protected:
svector<scope> m_scopes; svector<scope> m_scopes;
scoped_ptr<solver_factory> m_solver_factory; scoped_ptr<solver_factory> m_solver_factory;
scoped_ptr<solver_factory> m_interpolating_solver_factory; scoped_ptr<solver_factory> m_interpolating_solver_factory;
ref<solver> m_solver; ref<solver> m_solver;
ref<check_sat_result> m_check_sat_result; ref<check_sat_result> m_check_sat_result;
ref<opt_wrapper> m_opt; ref<opt_wrapper> m_opt;
@ -296,7 +298,7 @@ protected:
bool contains_macro(symbol const& s) const; bool contains_macro(symbol const& s) const;
bool contains_macro(symbol const& s, func_decl* f) const; bool contains_macro(symbol const& s, func_decl* f) const;
bool contains_macro(symbol const& s, unsigned arity, sort *const* domain) const; bool contains_macro(symbol const& s, unsigned arity, sort *const* domain) const;
void insert_macro(symbol const& s, unsigned arity, sort*const* domain, expr* t); void insert_macro(symbol const& s, unsigned arity, sort*const* domain, expr* t);
void erase_macro(symbol const& s); void erase_macro(symbol const& s);
bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const; bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const;
@ -304,7 +306,7 @@ protected:
public: public:
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
~cmd_context(); ~cmd_context();
void set_cancel(bool f); void set_cancel(bool f);
context_params & params() { return m_params; } context_params & params() { return m_params; }
solver_factory &get_solver_factory() { return *m_solver_factory; } solver_factory &get_solver_factory() { return *m_solver_factory; }
@ -354,39 +356,40 @@ public:
virtual ast_manager & get_ast_manager() { return m(); } virtual ast_manager & get_ast_manager() { return m(); }
pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; } pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; } sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
void set_solver_factory(solver_factory * s); void set_solver_factory(solver_factory * s);
void set_interpolating_solver_factory(solver_factory * s); void set_interpolating_solver_factory(solver_factory * s);
void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; } void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); } check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
check_sat_state cs_state() const; check_sat_state cs_state() const;
void complete_model();
void validate_model(); void validate_model();
void display_model(model_ref& mdl); void display_model(model_ref& mdl);
void register_plugin(symbol const & name, decl_plugin * p, bool install_names); void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
bool is_func_decl(symbol const & s) const; bool is_func_decl(symbol const & s) const;
bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); } bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); }
void insert(cmd * c); void insert(cmd * c);
void insert(symbol const & s, func_decl * f); void insert(symbol const & s, func_decl * f);
void insert(func_decl * f) { insert(f->get_name(), f); } void insert(func_decl * f) { insert(f->get_name(), f); }
void insert(symbol const & s, psort_decl * p); void insert(symbol const & s, psort_decl * p);
void insert(psort_decl * p) { insert(p->get_name(), p); } void insert(psort_decl * p) { insert(p->get_name(), p); }
void insert(symbol const & s, unsigned arity, sort *const* domain, expr * t); void insert(symbol const & s, unsigned arity, sort *const* domain, expr * t);
void insert(symbol const & s, object_ref *); void insert(symbol const & s, object_ref *);
void insert(tactic_cmd * c) { tactic_manager::insert(c); } void insert(tactic_cmd * c) { tactic_manager::insert(c); }
void insert(probe_info * p) { tactic_manager::insert(p); } void insert(probe_info * p) { tactic_manager::insert(p); }
void insert_user_tactic(symbol const & s, sexpr * d); void insert_user_tactic(symbol const & s, sexpr * d);
void insert_aux_pdecl(pdecl * p); void insert_aux_pdecl(pdecl * p);
void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e); void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
func_decl * find_func_decl(symbol const & s) const; func_decl * find_func_decl(symbol const & s) const;
func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
unsigned arity, sort * const * domain, sort * range) const; unsigned arity, sort * const * domain, sort * range) const;
psort_decl * find_psort_decl(symbol const & s) const; psort_decl * find_psort_decl(symbol const & s) const;
cmd * find_cmd(symbol const & s) const; cmd * find_cmd(symbol const & s) const;
sexpr * find_user_tactic(symbol const & s) const; sexpr * find_user_tactic(symbol const & s) const;
object_ref * find_object_ref(symbol const & s) const; object_ref * find_object_ref(symbol const & s) const;
void mk_const(symbol const & s, expr_ref & result) const; void mk_const(symbol const & s, expr_ref & result) const;
void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range,
expr_ref & r) const; expr_ref & r) const;
void erase_cmd(symbol const & s); void erase_cmd(symbol const & s);
void erase_func_decl(symbol const & s); void erase_func_decl(symbol const & s);
@ -401,7 +404,7 @@ public:
void reset_object_refs(); void reset_object_refs();
void reset_user_tactics(); void reset_user_tactics();
void set_regular_stream(char const * name) { m_regular.set(name); } void set_regular_stream(char const * name) { m_regular.set(name); }
void set_diagnostic_stream(char const * name); void set_diagnostic_stream(char const * name);
virtual std::ostream & regular_stream() { return *m_regular; } virtual std::ostream & regular_stream() { return *m_regular; }
virtual std::ostream & diagnostic_stream() { return *m_diagnostic; } virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }
char const * get_regular_stream_name() const { return m_regular.name(); } char const * get_regular_stream_name() const { return m_regular.name(); }
@ -429,7 +432,7 @@ public:
// display the result produced by a check-sat or check-sat-using commands in the regular stream // display the result produced by a check-sat or check-sat-using commands in the regular stream
void display_sat_result(lbool r); void display_sat_result(lbool r);
// check if result produced by check-sat or check-sat-using matches the known status // check if result produced by check-sat or check-sat-using matches the known status
void validate_check_sat_result(lbool r); void validate_check_sat_result(lbool r);
unsigned num_scopes() const { return m_scopes.size(); } unsigned num_scopes() const { return m_scopes.size(); }
dictionary<macro_decls> const & get_macros() const { return m_macros; } dictionary<macro_decls> const & get_macros() const { return m_macros; }

77
src/cmd_context/pdecl.cpp
View file

@ -25,11 +25,11 @@ class psort_inst_cache {
sort * m_const; sort * m_const;
obj_map<sort, void *> m_map; // if m_num_params == 1 value is a sort, otherwise it is a reference to another inst_cache obj_map<sort, void *> m_map; // if m_num_params == 1 value is a sort, otherwise it is a reference to another inst_cache
public: public:
psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) { psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) {
} }
~psort_inst_cache() { SASSERT(m_map.empty()); SASSERT(m_const == 0); } ~psort_inst_cache() { SASSERT(m_map.empty()); SASSERT(m_const == 0); }
void finalize(pdecl_manager & m) { void finalize(pdecl_manager & m) {
if (m_num_params == 0) { if (m_num_params == 0) {
SASSERT(m_map.empty()); SASSERT(m_map.empty());
@ -83,7 +83,7 @@ public:
curr = static_cast<psort_inst_cache*>(next); curr = static_cast<psort_inst_cache*>(next);
} }
} }
sort * find(sort * const * s) const { sort * find(sort * const * s) const {
if (m_num_params == 0) if (m_num_params == 0)
return m_const; return m_const;
@ -136,8 +136,8 @@ class psort_sort : public psort {
friend class pdecl_manager; friend class pdecl_manager;
sort * m_sort; sort * m_sort;
psort_sort(unsigned id, pdecl_manager & m, sort * s):psort(id, 0), m_sort(s) { m.m().inc_ref(m_sort); } psort_sort(unsigned id, pdecl_manager & m, sort * s):psort(id, 0), m_sort(s) { m.m().inc_ref(m_sort); }
virtual void finalize(pdecl_manager & m) { virtual void finalize(pdecl_manager & m) {
m.m().dec_ref(m_sort); m.m().dec_ref(m_sort);
psort::finalize(m); psort::finalize(m);
} }
virtual bool check_num_params(pdecl * other) const { return true; } virtual bool check_num_params(pdecl * other) const { return true; }
@ -150,7 +150,7 @@ public:
virtual char const * hcons_kind() const { return "psort_sort"; } virtual char const * hcons_kind() const { return "psort_sort"; }
virtual unsigned hcons_hash() const { return m_sort->get_id(); } virtual unsigned hcons_hash() const { return m_sort->get_id(); }
virtual bool hcons_eq(psort const * other) const { virtual bool hcons_eq(psort const * other) const {
if (other->hcons_kind() != hcons_kind()) if (other->hcons_kind() != hcons_kind())
return false; return false;
return m_sort == static_cast<psort_sort const *>(other)->m_sort; return m_sort == static_cast<psort_sort const *>(other)->m_sort;
} }
@ -170,10 +170,10 @@ public:
virtual char const * hcons_kind() const { return "psort_var"; } virtual char const * hcons_kind() const { return "psort_var"; }
virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); } virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); }
virtual bool hcons_eq(psort const * other) const { virtual bool hcons_eq(psort const * other) const {
if (other->hcons_kind() != hcons_kind()) if (other->hcons_kind() != hcons_kind())
return false; return false;
return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx; return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx;
} }
virtual void display(std::ostream & out) const { virtual void display(std::ostream & out) const {
out << "s_" << m_idx; out << "s_" << m_idx;
} }
@ -195,7 +195,7 @@ class psort_app : public psort {
DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); }); DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
} }
virtual void finalize(pdecl_manager & m) { virtual void finalize(pdecl_manager & m) {
m.lazy_dec_ref(m_decl); m.lazy_dec_ref(m_decl);
m.lazy_dec_ref(m_args.size(), m_args.c_ptr()); m.lazy_dec_ref(m_args.size(), m_args.c_ptr());
psort::finalize(m); psort::finalize(m);
@ -206,14 +206,14 @@ class psort_app : public psort {
struct khasher { struct khasher {
unsigned operator()(psort_app const * d) const { return d->m_decl->hash(); } unsigned operator()(psort_app const * d) const { return d->m_decl->hash(); }
}; };
struct chasher { struct chasher {
unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); } unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); }
}; };
virtual sort * instantiate(pdecl_manager & m, sort * const * s) { virtual sort * instantiate(pdecl_manager & m, sort * const * s) {
sort * r = find(s); sort * r = find(s);
if (r) if (r)
return r; return r;
sort_ref_buffer args_i(m.m()); sort_ref_buffer args_i(m.m());
unsigned sz = m_args.size(); unsigned sz = m_args.size();
@ -229,11 +229,11 @@ class psort_app : public psort {
public: public:
virtual ~psort_app() {} virtual ~psort_app() {}
virtual char const * hcons_kind() const { return "psort_app"; } virtual char const * hcons_kind() const { return "psort_app"; }
virtual unsigned hcons_hash() const { virtual unsigned hcons_hash() const {
return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size()); return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size());
} }
virtual bool hcons_eq(psort const * other) const { virtual bool hcons_eq(psort const * other) const {
if (other->hcons_kind() != hcons_kind()) if (other->hcons_kind() != hcons_kind())
return false; return false;
if (get_num_params() != other->get_num_params()) if (get_num_params() != other->get_num_params())
return false; return false;
@ -266,6 +266,7 @@ public:
psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n): psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n):
pdecl(id, num_params), pdecl(id, num_params),
m_psort_kind(PSORT_BASE),
m_name(n), m_name(n),
m_inst_cache(0) { m_inst_cache(0) {
} }
@ -293,7 +294,7 @@ sort * psort_decl::find(sort * const * s) {
#if 0 #if 0
psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n): psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n):
psort_decl(id, num_params, m, n) { psort_decl(id, num_params, m, n) {
} }
void psort_dt_decl::finalize(pdecl_manager& m) { void psort_dt_decl::finalize(pdecl_manager& m) {
@ -312,9 +313,10 @@ void psort_dt_decl::display(std::ostream & out) const {
#endif #endif
psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p): psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p) :
psort_decl(id, num_params, m, n), psort_decl(id, num_params, m, n),
m_def(p) { m_def(p) {
m_psort_kind = PSORT_USER;
m.inc_ref(p); m.inc_ref(p);
SASSERT(p == 0 || num_params == p->get_num_params()); SASSERT(p == 0 || num_params == p->get_num_params());
} }
@ -367,6 +369,7 @@ psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol co
psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n), psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n),
m_fid(fid), m_fid(fid),
m_kind(k) { m_kind(k) {
m_psort_kind = PSORT_BUILTIN;
} }
sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
@ -415,16 +418,16 @@ void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) cons
paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r): paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r):
pdecl(id, num_params), pdecl(id, num_params),
m_name(n), m_name(n),
m_type(r) { m_type(r) {
if (m_type.kind() == PTR_PSORT) { if (m_type.kind() == PTR_PSORT) {
m.inc_ref(r.get_psort()); m.inc_ref(r.get_psort());
} }
} }
void paccessor_decl::finalize(pdecl_manager & m) { void paccessor_decl::finalize(pdecl_manager & m) {
if (m_type.kind() == PTR_PSORT) { if (m_type.kind() == PTR_PSORT) {
m.lazy_dec_ref(m_type.get_psort()); m.lazy_dec_ref(m_type.get_psort());
} }
} }
@ -437,7 +440,7 @@ bool paccessor_decl::has_missing_refs(symbol & missing) const {
} }
bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) { bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n"; TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n";
if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";); if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";);
if (m_type.kind() != PTR_MISSING_REF) if (m_type.kind() != PTR_MISSING_REF)
return true; return true;
@ -468,7 +471,7 @@ void paccessor_decl::display(std::ostream & out, pdatatype_decl const * const *
out << ")"; out << ")";
} }
pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m,
symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors): symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors):
pdecl(id, num_params), pdecl(id, num_params),
m_name(n), m_name(n),
@ -514,7 +517,7 @@ void pconstructor_decl::display(std::ostream & out, pdatatype_decl const * const
out << ")"; out << ")";
} }
pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m,
symbol const & n, unsigned num_constructors, pconstructor_decl * const * constructors): symbol const & n, unsigned num_constructors, pconstructor_decl * const * constructors):
psort_decl(id, num_params, m, n), psort_decl(id, num_params, m, n),
m_constructors(num_constructors, constructors), m_constructors(num_constructors, constructors),
@ -620,7 +623,7 @@ void pdatatype_decl::display(std::ostream & out) const {
out << ")"; out << ")";
} }
pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m,
unsigned num_datatypes, pdatatype_decl * const * dts): unsigned num_datatypes, pdatatype_decl * const * dts):
pdecl(id, num_params), pdecl(id, num_params),
m_datatypes(num_datatypes, dts) { m_datatypes(num_datatypes, dts) {
@ -685,22 +688,22 @@ struct pdecl_manager::sort_info {
struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
ptr_vector<sort> m_args; ptr_vector<sort> m_args;
app_sort_info(pdecl_manager & m, psort_decl * d, unsigned n, sort * const * s): app_sort_info(pdecl_manager & m, psort_decl * d, unsigned n, sort * const * s):
sort_info(m, d), sort_info(m, d),
m_args(n, s) { m_args(n, s) {
m.m().inc_array_ref(n, s); m.m().inc_array_ref(n, s);
} }
virtual ~app_sort_info() {} virtual ~app_sort_info() {}
virtual unsigned obj_size() const { return sizeof(app_sort_info); } virtual unsigned obj_size() const { return sizeof(app_sort_info); }
virtual void finalize(pdecl_manager & m) { virtual void finalize(pdecl_manager & m) {
sort_info::finalize(m); sort_info::finalize(m);
m.m().dec_array_ref(m_args.size(), m_args.c_ptr()); m.m().dec_array_ref(m_args.size(), m_args.c_ptr());
} }
virtual void display(std::ostream & out, pdecl_manager const & m) const { virtual void display(std::ostream & out, pdecl_manager const & m) const {
if (m_args.empty()) { if (m_args.empty()) {
out << m_decl->get_name(); out << m_decl->get_name();
@ -714,7 +717,7 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
out << ")"; out << ")";
} }
} }
virtual format * pp(pdecl_manager const & m) const { virtual format * pp(pdecl_manager const & m) const {
if (m_args.empty()) { if (m_args.empty()) {
return mk_string(m.m(), m_decl->get_name().str().c_str()); return mk_string(m.m(), m_decl->get_name().str().c_str());
@ -726,7 +729,7 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str()); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str());
} }
} }
}; };
struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
svector<unsigned> m_indices; svector<unsigned> m_indices;
@ -752,7 +755,7 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
out << ")"; out << ")";
} }
} }
virtual format * pp(pdecl_manager const & m) const { virtual format * pp(pdecl_manager const & m) const {
if (m_indices.empty()) { if (m_indices.empty()) {
return mk_string(m.m(), m_decl->get_name().str().c_str()); return mk_string(m.m(), m_decl->get_name().str().c_str());
@ -772,7 +775,7 @@ void pdecl_manager::init_list() {
psort * v = mk_psort_var(1, 0); psort * v = mk_psort_var(1, 0);
ptype T(v); ptype T(v);
ptype ListT(0); ptype ListT(0);
paccessor_decl * as[2] = { mk_paccessor_decl(1, symbol("head"), T), paccessor_decl * as[2] = { mk_paccessor_decl(1, symbol("head"), T),
mk_paccessor_decl(1, symbol("tail"), ListT) }; mk_paccessor_decl(1, symbol("tail"), ListT) };
pconstructor_decl * cs[2] = { mk_pconstructor_decl(1, symbol("nil"), symbol("is-nil"), 0, 0), pconstructor_decl * cs[2] = { mk_pconstructor_decl(1, symbol("nil"), symbol("is-nil"), 0, 0),
mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) }; mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) };
@ -822,8 +825,8 @@ psort * pdecl_manager::mk_psort_var(unsigned num_params, unsigned vidx) {
paccessor_decl * pdecl_manager::mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p) { paccessor_decl * pdecl_manager::mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p) {
return new (a().allocate(sizeof(paccessor_decl))) paccessor_decl(m_id_gen.mk(), num_params, *this, s, p); return new (a().allocate(sizeof(paccessor_decl))) paccessor_decl(m_id_gen.mk(), num_params, *this, s, p);
} }
pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params, pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params,
symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as) { symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as) {
return new (a().allocate(sizeof(pconstructor_decl))) pconstructor_decl(m_id_gen.mk(), num_params, *this, return new (a().allocate(sizeof(pconstructor_decl))) pconstructor_decl(m_id_gen.mk(), num_params, *this,
s, r, num, as); s, r, num, as);
@ -872,9 +875,9 @@ sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args)
void pdecl_manager::del_decl_core(pdecl * p) { void pdecl_manager::del_decl_core(pdecl * p) {
TRACE("pdecl_manager", TRACE("pdecl_manager",
tout << "del_decl_core:\n"; tout << "del_decl_core:\n";
if (p->is_psort()) static_cast<psort*>(p)->display(tout); if (p->is_psort()) static_cast<psort*>(p)->display(tout);
else static_cast<psort_decl*>(p)->display(tout); else static_cast<psort_decl*>(p)->display(tout);
tout << "\n";); tout << "\n";);
size_t sz = p->obj_size(); size_t sz = p->obj_size();
@ -892,7 +895,7 @@ void pdecl_manager::del_decl(pdecl * p) {
else else
m_table.erase(_p); m_table.erase(_p);
} }
del_decl_core(p); del_decl_core(p);
} }
void pdecl_manager::del_decls() { void pdecl_manager::del_decls() {

13
src/cmd_context/pdecl.h
View file

@ -86,10 +86,13 @@ typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> psort_table;
#define PSORT_DECL_VAR_PARAMS UINT_MAX #define PSORT_DECL_VAR_PARAMS UINT_MAX
typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN } psort_decl_kind;
class psort_decl : public pdecl { class psort_decl : public pdecl {
protected: protected:
friend class pdecl_manager; friend class pdecl_manager;
symbol m_name; symbol m_name;
psort_decl_kind m_psort_kind;
psort_inst_cache * m_inst_cache; psort_inst_cache * m_inst_cache;
void cache(pdecl_manager & m, sort * const * s, sort * r); void cache(pdecl_manager & m, sort * const * s, sort * r);
sort * find(sort * const * s); sort * find(sort * const * s);
@ -105,6 +108,8 @@ public:
bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; } bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; }
symbol const & get_name() const { return m_name; } symbol const & get_name() const { return m_name; }
virtual void reset_cache(pdecl_manager& m); virtual void reset_cache(pdecl_manager& m);
bool is_user_decl() const { return m_psort_kind == PSORT_USER; }
bool is_builtin_decl() const { return m_psort_kind == PSORT_BUILTIN; }
}; };
class psort_user_decl : public psort_decl { class psort_user_decl : public psort_decl {
@ -195,7 +200,7 @@ class pconstructor_decl : public pdecl {
symbol m_name; symbol m_name;
symbol m_recogniser_name; symbol m_recogniser_name;
ptr_vector<paccessor_decl> m_accessors; ptr_vector<paccessor_decl> m_accessors;
pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m,
symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors); symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors);
virtual void finalize(pdecl_manager & m); virtual void finalize(pdecl_manager & m);
virtual size_t obj_size() const { return sizeof(pconstructor_decl); } virtual size_t obj_size() const { return sizeof(pconstructor_decl); }
@ -215,7 +220,7 @@ class pdatatype_decl : public psort_decl {
friend class pdatatypes_decl; friend class pdatatypes_decl;
ptr_vector<pconstructor_decl> m_constructors; ptr_vector<pconstructor_decl> m_constructors;
pdatatypes_decl * m_parent; pdatatypes_decl * m_parent;
pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n,
unsigned num_constructors, pconstructor_decl * const * constructors); unsigned num_constructors, pconstructor_decl * const * constructors);
virtual void finalize(pdecl_manager & m); virtual void finalize(pdecl_manager & m);
virtual size_t obj_size() const { return sizeof(pdatatype_decl); } virtual size_t obj_size() const { return sizeof(pdatatype_decl); }
@ -268,7 +273,7 @@ class pdecl_manager {
struct indexed_sort_info; struct indexed_sort_info;
obj_map<sort, sort_info *> m_sort2info; // for pretty printing sorts obj_map<sort, sort_info *> m_sort2info; // for pretty printing sorts
void init_list(); void init_list();
void del_decl_core(pdecl * p); void del_decl_core(pdecl * p);
void del_decl(pdecl * p); void del_decl(pdecl * p);
@ -282,7 +287,7 @@ public:
small_object_allocator & a() const { return m_allocator; } small_object_allocator & a() const { return m_allocator; }
family_id get_datatype_fid() const { return m_datatype_fid; } family_id get_datatype_fid() const { return m_datatype_fid; }
void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; } void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; }
psort * mk_psort_cnst(sort * s); psort * mk_psort_cnst(sort * s);
psort * mk_psort_var(unsigned num_params, unsigned vidx); psort * mk_psort_var(unsigned num_params, unsigned vidx);
psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args); psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args);
psort * mk_psort_app(psort_decl * d); psort * mk_psort_app(psort_decl * d);

72
src/math/automata/automaton.h
View file

@ -25,6 +25,7 @@ Revision History:
#include "util/util.h" #include "util/util.h"
#include "util/vector.h" #include "util/vector.h"
#include "util/uint_set.h" #include "util/uint_set.h"
#include "util/trace.h"
template<class T> template<class T>
class default_value_manager { class default_value_manager {
@ -383,12 +384,12 @@ public:
else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) { else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
moves const& mvs = m_delta[dst]; moves const& mvs = m_delta[dst];
moves mvs1; moves mvs1;
for (unsigned k = 0; k < mvs.size(); ++k) { for (move const& mv : mvs) {
mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t())); mvs1.push_back(move(m, src, mv.dst(), mv.t()));
} }
for (unsigned k = 0; k < mvs1.size(); ++k) { for (move const& mv : mvs1) {
remove(dst, mvs1[k].dst(), mvs1[k].t()); remove(dst, mv.dst(), mv.t());
add(mvs1[k]); add(mv);
} }
} }
// //
@ -401,13 +402,13 @@ public:
unsigned_vector src0s; unsigned_vector src0s;
moves const& mvs = m_delta_inv[dst]; moves const& mvs = m_delta_inv[dst];
moves mvs1; moves mvs1;
for (unsigned k = 0; k < mvs.size(); ++k) { for (move const& mv1 : mvs) {
SASSERT(mvs[k].is_epsilon()); SASSERT(mv1.is_epsilon());
mvs1.push_back(move(m, mvs[k].src(), dst1, t)); mvs1.push_back(move(m, mv1.src(), dst1, t));
} }
for (unsigned k = 0; k < mvs1.size(); ++k) { for (move const& mv1 : mvs1) {
remove(mvs1[k].src(), dst, 0); remove(mv1.src(), dst, 0);
add(mvs1[k]); add(mv1);
} }
remove(dst, dst1, t); remove(dst, dst1, t);
--j; --j;
@ -419,12 +420,12 @@ public:
else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) { else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
moves const& mvs = m_delta_inv[src]; moves const& mvs = m_delta_inv[src];
moves mvs1; moves mvs1;
for (unsigned k = 0; k < mvs.size(); ++k) { for (move const& mv : mvs) {
mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t())); mvs1.push_back(move(m, mv.src(), dst, mv.t()));
} }
for (unsigned k = 0; k < mvs1.size(); ++k) { for (move const& mv : mvs1) {
remove(mvs1[k].src(), src, mvs1[k].t()); remove(mv.src(), src, mv.t());
add(mvs1[k]); add(mv);
} }
} }
else { else {
@ -447,6 +448,7 @@ public:
break; break;
} }
} }
sinkify_dead_states();
} }
bool is_sequence(unsigned& length) const { bool is_sequence(unsigned& length) const {
@ -564,6 +566,40 @@ public:
} }
private: private:
void sinkify_dead_states() {
uint_set dead_states;
for (unsigned i = 0; i < m_delta.size(); ++i) {
if (!m_final_states.contains(i)) {
dead_states.insert(i);
}
}
bool change = true;
unsigned_vector to_remove;
while (change) {
change = false;
to_remove.reset();
for (unsigned s : dead_states) {
moves const& mvs = m_delta[s];
for (move const& mv : mvs) {
if (!dead_states.contains(mv.dst())) {
to_remove.push_back(s);
break;
}
}
}
change = !to_remove.empty();
for (unsigned s : to_remove) {
dead_states.remove(s);
}
to_remove.reset();
}
TRACE("seq", tout << "remove: " << dead_states << "\n";);
for (unsigned s : dead_states) {
CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";);
m_delta[s].reset();
}
}
void remove_dead_states() { void remove_dead_states() {
unsigned_vector remap; unsigned_vector remap;
for (unsigned i = 0; i < m_delta.size(); ++i) { for (unsigned i = 0; i < m_delta.size(); ++i) {
@ -669,8 +705,8 @@ private:
} }
static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) { static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
for (unsigned i = 0; i < a.m_final_states.size(); ++i) { for (unsigned s : a.m_final_states) {
final.push_back(a.m_final_states[i]+offset); final.push_back(s+offset);
} }
} }

3
src/model/model_params.pyg
View file

@ -1,8 +1,9 @@
def_module_params('model', def_module_params('model',
export=True, export=True,
params=(('partial', BOOL, False, 'enable/disable partial function interpretations'), params=(('partial', BOOL, False, 'enable/disable partial function interpretations'),
('v1', BOOL, False, 'use Z3 version 1.x pretty printer'), ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'), ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('completion', BOOL, False, 'enable/disable model completion'),
)) ))