diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 029e2d90c..c1ff04ada 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 55c5436e4..1ab54d0b5 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -37,23 +37,6 @@ macro_util::macro_util(ast_manager & m): m_curr_clause(0) { } -#if 0 -arith_simplifier_plugin * macro_util::get_arith_simp() const { - if (m_arith_simp == 0) { - const_cast(this)->m_arith_simp = static_cast(m_simplifier.get_plugin(m_manager.mk_family_id("arith"))); - } - SASSERT(m_arith_simp != 0); - return m_arith_simp; -} - -bv_simplifier_plugin * macro_util::get_bv_simp() const { - if (m_bv_simp == 0) { - const_cast(this)->m_bv_simp = static_cast(m_simplifier.get_plugin(m_manager.mk_family_id("bv"))); - } - SASSERT(m_bv_simp != 0); - return m_bv_simp; -} -#endif bool macro_util::is_bv(expr * n) const { return m_bv.is_bv(n); diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp new file mode 100644 index 000000000..d604ba2ff --- /dev/null +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -0,0 +1,468 @@ +/*++ +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 +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(arg1, arg2, result); +} + +void arith_simplifier_plugin::mk_le(expr * arg1, expr * arg2, expr_ref & result) { + mk_le_ge_eq_core(arg1, arg2, result); +} + +void arith_simplifier_plugin::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { + mk_le_ge_eq_core(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(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(lhs, rhs, le); + mk_le_ge_eq_core(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; +} + + + diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h new file mode 100644 index 000000000..4f3a6add0 --- /dev/null +++ b/src/ast/simplifier/arith_simplifier_plugin.h @@ -0,0 +1,97 @@ +/*++ +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 + 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_ */ diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index cf4dcbfc6..2f55d5cc2 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -107,11 +107,10 @@ public: m_init = init; m_delta.push_back(moves()); m_delta_inv.push_back(moves()); - for (unsigned i = 0; i < final.size(); ++i) { - add_to_final_states(final[i]); + for (unsigned f : final) { + add_to_final_states(f); } - for (unsigned i = 0; i < mvs.size(); ++i) { - move const& mv = mvs[i]; + for (move const& mv : mvs) { unsigned n = std::max(mv.src(), mv.dst()); if (n >= m_delta.size()) { m_delta.resize(n+1, moves()); @@ -280,8 +279,8 @@ public: } else { init = a.num_states(); - for (unsigned i = 0; i < a.m_final_states.size(); ++i) { - mvs.push_back(move(m, init, a.m_final_states[i])); + for (unsigned st : a.m_final_states) { + mvs.push_back(move(m, init, st)); } } return alloc(automaton, m, init, final, mvs); @@ -471,18 +470,17 @@ public: moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; } bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); } bool is_final_state(unsigned s) const { return m_final_set.contains(s); } - bool is_final_configuration(uint_set s) const { - for (uint_set::iterator it = s.begin(), end = s.end(); it != end; ++it) { - if (is_final_state(*it)) - return true; - } - return false; - } + bool is_final_configuration(uint_set s) const { + for (unsigned i : s) { + if (is_final_state(i)) + return true; + } + return false; + } bool is_epsilon_free() const { - for (unsigned i = 0; i < m_delta.size(); ++i) { - moves const& mvs = m_delta[i]; - for (unsigned j = 0; j < mvs.size(); ++j) { - if (!mvs[j].t()) return false; + for (moves const& mvs : m_delta) { + for (move const & m : mvs) { + if (!m.t()) return false; } } return true; @@ -490,8 +488,8 @@ public: bool all_epsilon_in(unsigned s) { moves const& mvs = m_delta_inv[s]; - for (unsigned j = 0; j < mvs.size(); ++j) { - if (mvs[j].t()) return false; + for (move const& m : mvs) { + if (m.t()) return false; } return true; } @@ -504,15 +502,15 @@ public: bool is_loop_state(unsigned s) const { moves mvs; get_moves_from(s, mvs); - for (unsigned i = 0; i < mvs.size(); ++i) { - if (s == mvs[i].dst()) return true; + for (move const& m : mvs) { + if (s == m.dst()) return true; } return false; } unsigned move_count() const { unsigned result = 0; - for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {} + for (moves const& mvs : m_delta) result += mvs.size(); return result; } void get_epsilon_closure(unsigned state, unsigned_vector& states) { @@ -524,13 +522,13 @@ public: void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const { get_moves(state, m_delta, mvs, epsilon_closure); } - void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const { - for (uint_set::iterator it = states.begin(), end = states.end(); it != end; ++it) { - moves curr; - get_moves(*it, m_delta, curr, epsilon_closure); - mvs.append(curr); - } - } + void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const { + for (unsigned i : states) { + moves curr; + get_moves(i, m_delta, curr, epsilon_closure); + mvs.append(curr); + } + } void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) { get_moves(state, m_delta_inv, mvs, epsilon_closure); } @@ -543,8 +541,7 @@ public: out << "\n"; for (unsigned i = 0; i < m_delta.size(); ++i) { moves const& mvs = m_delta[i]; - for (unsigned j = 0; j < mvs.size(); ++j) { - move const& mv = mvs[j]; + for (move const& mv : mvs) { out << i << " -> " << mv.dst() << " "; if (mv.t()) { out << "if "; diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h index 4a8e7a74d..4831280af 100644 --- a/src/math/automata/symbolic_automata.h +++ b/src/math/automata/symbolic_automata.h @@ -130,13 +130,14 @@ private: else { //true case curr_bv.push_back(true); - ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m); + ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m); generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos); curr_bv.pop_back(); //false case curr_bv.push_back(false); - ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m); + ref_t neg(m_ba.mk_not(constraints[i]), m); + ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m); generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg); curr_bv.pop_back(); } diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index c1ee53214..c89080d3d 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -288,7 +288,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_acceptance) { vector, ref_t> > min_terms; vector predicates; - + map s2id; // set of states to unique id vector id2s; // unique id to set of b-states uint_set set; @@ -296,13 +296,18 @@ symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_accepta moves_t new_mvs; // moves in the resulting automaton unsigned_vector new_final_states; // new final states unsigned p_state_id = 0; // next state identifier - - // adds non-final states of a to final if flipping and and final otherwise + + TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";); + // adds non-final states of a to final if flipping and final otherwise + unsigned_vector init_states; + a.get_epsilon_closure(a.init(), init_states); + for (unsigned s : init_states) { + set.insert(s); + } if (a.is_final_configuration(set) != flip_acceptance) { new_final_states.push_back(p_state_id); } - set.insert(a.init()); // Initial state as aset s2id.insert(set, p_state_id++); // the index to the initial state is 0 id2s.push_back(set); @@ -342,6 +347,7 @@ symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_accepta bool is_new = !s2id.contains(set); if (is_new) { + TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";); if (a.is_final_configuration(set) != flip_acceptance) { new_final_states.push_back(p_state_id); } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 521aa5e71..21f9f1e8a 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -388,6 +388,9 @@ private: m_subgoals.reset(); init_preprocess(); SASSERT(g->models_enabled()); + if (g->proofs_enabled()) { + throw default_exception("generation of proof objects is not supported in this mode"); + } SASSERT(!g->proofs_enabled()); TRACE("sat", g->display(tout);); try { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 8d6d70a79..461e9e8ee 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3392,15 +3392,22 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { return; } - eautomaton* a = get_automaton(e2); + expr_ref e3(e2, m); + context& ctx = get_context(); + literal lit = ctx.get_literal(n); + if (!is_true) { + e3 = m_util.re.mk_complement(e2); + is_true = true; + lit.neg(); + } + eautomaton* a = get_automaton(e3); if (!a) return; - context& ctx = get_context(); expr_ref len(m_util.str.mk_length(e1), m); for (unsigned i = 0; i < a->num_states(); ++i) { - literal acc = mk_accept(e1, len, e2, i); - literal rej = mk_reject(e1, len, e2, i); + literal acc = mk_accept(e1, len, e3, i); + literal rej = mk_reject(e1, len, e3, i); add_axiom(a->is_final_state(i)?acc:~acc); add_axiom(a->is_final_state(i)?~rej:rej); } @@ -3409,17 +3416,16 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { unsigned_vector states; a->get_epsilon_closure(a->init(), states); literal_vector lits; - literal lit = ctx.get_literal(n); if (is_true) { lits.push_back(~lit); } for (unsigned i = 0; i < states.size(); ++i) { if (is_true) { - lits.push_back(mk_accept(e1, zero, e2, states[i])); + lits.push_back(mk_accept(e1, zero, e3, states[i])); } else { literal nlit = ~lit; - propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e2, states[i])); + propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e3, states[i])); } } if (is_true) { diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 0ad9e5f19..3e77b7abc 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); - else if (logic == "QF_FD" || logic == "SAT") + else if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled()) return mk_solver2tactic(mk_fd_solver(m, p)); //else if (logic=="QF_UFNRA") // return mk_qfufnra_tactic(m, p); @@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const } static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { - if (logic == "QF_FD" || logic == "SAT") + if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled()) return mk_fd_solver(m, p); return 0; }