From 623cd5ded2bbc414faca3ca2295d62c935c026f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 13:00:43 -0700 Subject: [PATCH 1/6] fix naming for functions #1223 Signed-off-by: Nikolaj Bjorner --- src/api/api_model.cpp | 4 ++-- src/api/c++/z3++.h | 4 ++-- src/api/z3_api.h | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 66002baa0..540f014c6 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -337,9 +337,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) { + void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) { Z3_TRY; - LOG_Z3_add_func_entry(c, fi, args, value); + LOG_Z3_func_interp_add_entry(c, fi, args, value); //CHECK_NON_NULL(fi, void); //CHECK_NON_NULL(args, void); //CHECK_NON_NULL(value, void); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 2f67cb72a..6d8ff3b35 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1732,11 +1732,11 @@ namespace z3 { unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; } func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); } void add_entry(expr_vector const& args, expr& value) { - Z3_add_func_entry(ctx(), m_interp, args, value); + Z3_func_interp_add_entry(ctx(), m_interp, args, value); check_error(); } void set_else(expr& value) { - Z3_func_entry_set_else(ctx(), m_interp, value); + Z3_func_interp_set_else(ctx(), m_interp, value); check_error(); } }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 045417d38..bed70cb6c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4954,9 +4954,9 @@ extern "C" { If an two entries are added with the same arguments, only the second insertion survives and the first inserted entry is removed. - def_API('Z3_add_func_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST))) + def_API('Z3_func_interp_add_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST))) */ - void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value); + void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value); /** \brief Increment the reference counter of the given Z3_func_entry object. From 5db349f6fafc5b117dd49e11d7f2cd42531732af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 23:52:27 -0700 Subject: [PATCH 2/6] raise an exception if trying proof generation for the SAT solver. Stackoverflow question https://stackoverflow.com/questions/45885321/check-function-while-qf-fd-logic-is-set-throws-accessviolationexception Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 +++ src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) 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/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; } From 8542e4ae3df20070e9922b5e25e7381b6985ceb7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 00:05:53 -0700 Subject: [PATCH 3/6] add pre-processing simplificaiton of power to the legacy simplifier Fixes #1237 Signed-off-by: Nikolaj Bjorner --- .../simplifier/arith_simplifier_plugin.cpp | 21 ++++++++++++++++++- src/ast/simplifier/arith_simplifier_plugin.h | 1 + 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index bfe72b232..d604ba2ff 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -402,7 +402,7 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co 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: return false; + 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: @@ -412,6 +412,25 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co 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); diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h index 21ab8f6b4..4f3a6add0 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.h +++ b/src/ast/simplifier/arith_simplifier_plugin.h @@ -82,6 +82,7 @@ public: 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); From 974eaab01c752df9d61d53887709a5eb9a71ef1d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 01:38:23 -0700 Subject: [PATCH 4/6] complement regular expressions when used in negated membership constraints #1224 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 + src/math/automata/automaton.h | 59 +++++++++++------------ src/math/automata/symbolic_automata.h | 3 +- src/math/automata/symbolic_automata_def.h | 17 +++++-- src/smt/theory_seq.cpp | 20 +++++--- 5 files changed, 58 insertions(+), 42 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index f347a8e49..4f9a88490 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1726,6 +1726,7 @@ ast * ast_manager::register_node_core(ast * n) { } n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); + static unsigned s_counter = 0; TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); 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..35545e975 100644 --- a/src/math/automata/symbolic_automata.h +++ b/src/math/automata/symbolic_automata.h @@ -136,7 +136,8 @@ private: //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..aa8dd34fd 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,9 +296,19 @@ 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 - + + 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 and final otherwise - if (a.is_final_configuration(set) != flip_acceptance) { + unsigned_vector init_states; + a.get_epsilon_closure(a.init(), init_states); + bool found_final = false; + for (unsigned s : init_states) { + if (a.is_final_state(s)) { + found_final = true; + break; + } + } + if (found_final != flip_acceptance) { new_final_states.push_back(p_state_id); } @@ -342,6 +352,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/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c91882dad..a32a4833a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3391,15 +3391,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); } @@ -3408,17 +3415,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) { From 0ebb9172681e11b6ac0bcea6a4d69b021282a21a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 01:40:15 -0700 Subject: [PATCH 5/6] complement regular expressions when used in negated membership constraints #1224 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 2 -- src/math/automata/symbolic_automata.h | 4 ++-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4f9a88490..5c0abf6b8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1726,8 +1726,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(); - static unsigned s_counter = 0; - TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h index 35545e975..4831280af 100644 --- a/src/math/automata/symbolic_automata.h +++ b/src/math/automata/symbolic_automata.h @@ -130,13 +130,13 @@ 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 neg(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(); From feac705cb88bb00085e8c4313dbdc23befc7aa0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 13:47:19 -0700 Subject: [PATCH 6/6] include epsilon closure in initial state set, streamline final configuration computation #1224 Signed-off-by: Nikolaj Bjorner --- src/math/automata/symbolic_automata_def.h | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index aa8dd34fd..c89080d3d 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -298,21 +298,16 @@ symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_accepta unsigned p_state_id = 0; // next state identifier 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 and final otherwise + // 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); - bool found_final = false; + a.get_epsilon_closure(a.init(), init_states); for (unsigned s : init_states) { - if (a.is_final_state(s)) { - found_final = true; - break; - } + set.insert(s); } - if (found_final != flip_acceptance) { + 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);