mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master'

Browse source
This commit is contained in:
calebstanford-msr 2020-06-04 20:56:12 -04:00
commit 460068eade
29 changed files with 74 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/ast.cpp
View file

@ -3064,13 +3064,7 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<exp
}
bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
if (is_rewrite(e)) {
VERIFY (is_eq(to_app(e)->get_arg(0), r1, r2));
return true;
}
else {
return false;
}
return is_rewrite(e) && is_eq(to_app(e)->get_arg(0), r1, r2);
}
proof * ast_manager::mk_def_axiom(expr * ax) {
@ -3081,9 +3075,7 @@ proof * ast_manager::mk_def_axiom(expr * ax) {
proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs) {
SASSERT(num_proofs >= 2);
for (unsigned i = 0; i < num_proofs; i++) {
SASSERT(has_fact(proofs[i]));
}
DEBUG_CODE(for (unsigned i = 0; i < num_proofs; i++) SASSERT(has_fact(proofs[i])););
ptr_buffer<expr> args;
expr * fact;
expr * f1 = get_fact(proofs[0]);

1
src/ast/rewriter/rewriter_def.h
View file

@ -802,6 +802,7 @@ void rewriter_tpl<Config>::operator()(expr * t, expr_ref & result, proof_ref & r
if (!frame_stack().empty() || m_cache != m_cache_stack[0]) {
frame_stack().reset();
result_stack().reset();
result_pr_stack().reset();
m_scopes.reset();
reset_cache();
}

18
src/cmd_context/cmd_context.cpp
View file

@ -473,7 +473,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_status(UNKNOWN),
m_numeral_as_real(false),
m_ignore_check(false),
m_processing_pareto(false),
m_exit_on_error(false),
m_manager(m),
m_own_manager(m == nullptr),
@ -1261,7 +1260,6 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
}
void cmd_context::reset(bool finalize) {
m_processing_pareto = false;
m_logic = symbol::null;
m_check_sat_result = nullptr;
m_numeral_as_real = false;
@ -1307,7 +1305,6 @@ void cmd_context::reset(bool finalize) {
void cmd_context::assert_expr(expr * t) {
scoped_rlimit no_limit(m().limit(), 0);
m_processing_pareto = false;
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
m_check_sat_result = nullptr;
@ -1320,7 +1317,6 @@ void cmd_context::assert_expr(expr * t) {
}
void cmd_context::assert_expr(symbol const & name, expr * t) {
m_processing_pareto = false;
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
if (!produce_unsat_cores() || name == symbol::null) {
@ -1440,7 +1436,6 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
}
void cmd_context::restore_assertions(unsigned old_sz) {
m_processing_pareto = false;
if (!has_manager()) {
// restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
SASSERT(old_sz == m_assertions.size());
@ -1460,7 +1455,6 @@ void cmd_context::restore_assertions(unsigned old_sz) {
void cmd_context::pop(unsigned n) {
m_check_sat_result = nullptr;
m_processing_pareto = false;
if (n == 0)
return;
unsigned lvl = m_scopes.size();
@ -1507,7 +1501,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
scoped_rlimit _rlimit(m().limit(), rlimit);
expr_ref_vector asms(m());
asms.append(num_assumptions, assumptions);
if (!m_processing_pareto) {
if (!get_opt()->is_pareto()) {
expr_ref_vector assertions(m());
unsigned sz = m_assertions.size();
for (unsigned i = 0; i < sz; ++i) {
@ -1523,9 +1517,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
}
try {
r = get_opt()->optimize(asms);
if (r == l_true && get_opt()->is_pareto()) {
m_processing_pareto = true;
}
}
catch (z3_error & ex) {
throw ex;
@ -1533,9 +1524,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
catch (z3_exception & ex) {
throw cmd_exception(ex.msg());
}
if (m_processing_pareto && r != l_true) {
m_processing_pareto = false;
}
get_opt()->set_status(r);
}
else if (m_solver) {
@ -1575,10 +1563,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
validate_model();
}
validate_check_sat_result(r);
if (was_opt && r != l_false && !m_processing_pareto) {
// get_opt()->display_assignment(regular_stream());
}
model_ref md;
if (r == l_true && m_params.m_dump_models && is_model_available(md)) {
display_model(md);

1
src/cmd_context/cmd_context.h
View file

@ -192,7 +192,6 @@ protected:
status m_status;
bool m_numeral_as_real;
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_exit_on_error;
static std::ostringstream g_error_stream;

2
src/math/grobner/pdd_solver.cpp
View file

@ -362,7 +362,7 @@ namespace dd {
}
bool solver::canceled() {
return m_limit.get_cancel_flag();
return m_limit.is_canceled();
}
bool solver::done() {

2
src/math/lp/nra_solver.cpp
View file

@ -78,7 +78,7 @@ struct solver::imp {
r = m_nlsat->check();
}
catch (z3_exception&) {
if (m_limit.get_cancel_flag()) {
if (m_limit.is_canceled()) {
r = l_undef;
}
else {

34
src/muz/base/dl_context.cpp
View file

@ -21,15 +21,15 @@ Revision History:
#include<limits>
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "muz/base/dl_context.h"
#include "ast/for_each_expr.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/scoped_proof.h"
#include "muz/base/fp_params.hpp"
#include "ast/ast_pp_util.h"
#include "ast/ast_util.h"
#include "muz/base/dl_context.h"
#include "muz/base/fp_params.hpp"
namespace datalog {
@ -354,10 +354,9 @@ namespace datalog {
void context::restrict_predicates(func_decl_set const& preds) {
m_preds.reset();
func_decl_set::iterator it = preds.begin(), end = preds.end();
for (; it != end; ++it) {
TRACE("dl", tout << mk_pp(*it, m) << "\n";);
m_preds.insert(*it);
for (func_decl* p : preds) {
TRACE("dl", tout << mk_pp(p, m) << "\n";);
m_preds.insert(p);
}
}
@ -742,13 +741,7 @@ namespace datalog {
}
expr_ref context::get_background_assertion() {
expr_ref result(m);
switch (m_background.size()) {
case 0: result = m.mk_true(); break;
case 1: result = m_background[0].get(); break;
default: result = m.mk_and(m_background.size(), m_background.c_ptr()); break;
}
return result;
return mk_and(m_background);
}
void context::assert_expr(expr* e) {
@ -967,18 +960,17 @@ namespace datalog {
rule_ref_vector rv (rm);
get_rules_along_trace (rv);
expr_ref fml (m);
rule_ref_vector::iterator it = rv.begin (), end = rv.end ();
for (; it != end; it++) {
m_rule_manager.to_formula (**it, fml);
for (auto* r : rv) {
m_rule_manager.to_formula (*r, fml);
rules.push_back (fml);
// The concatenated names are already stored last-first, so do not need to be reversed here
const symbol& rule_name = (*it)->name();
const symbol& rule_name = r->name();
names.push_back (rule_name);
TRACE ("dl",
if (rule_name == symbol::null) {
tout << "Encountered unnamed rule: ";
(*it)->display(*this, tout);
r->display(*this, tout);
tout << "\n";
});
}
@ -1070,9 +1062,7 @@ namespace datalog {
--i;
}
}
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
rule* r = *it;
for (rule* r : m_rule_set) {
rm.to_formula(*r, fml);
func_decl* h = r->get_decl();
if (m_rule_set.is_output_predicate(h)) {

2
src/muz/spacer/spacer_util.cpp
View file

@ -383,7 +383,7 @@ namespace {
expr_ref res(m), v(m);
v = m_model(e);
// the literal must have a value
SASSERT(m.is_true(v) || m.is_false(v));
SASSERT(m.limit().is_canceled() || m.is_true(v) || m.is_false(v));
res = m.is_false(v) ? m.mk_not(e) : e;

1
src/muz/transforms/dl_mk_subsumption_checker.cpp
View file

@ -350,7 +350,6 @@ namespace datalog {
return nullptr;
}
//During the construction of the new set we may discover new total relations
//(by quantifier elimination on the uninterpreted tails).
SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);

6
src/nlsat/nlsat_solver.cpp
View file

@ -1759,7 +1759,7 @@ namespace nlsat {
if (assigned_value(antecedent) == l_undef) {
checkpoint();
// antecedent must be false in the current arith interpretation
SASSERT(value(antecedent) == l_false || m_rlimit.get_cancel_flag());
SASSERT(value(antecedent) == l_false || m_rlimit.is_canceled());
if (!is_marked(b)) {
SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage
TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";);
@ -1837,10 +1837,10 @@ namespace nlsat {
for (unsigned i = 0; i < sz; i++) {
literal l = m_lazy_clause[i];
if (l.var() != b) {
SASSERT(value(l) == l_false || m_rlimit.get_cancel_flag());
SASSERT(value(l) == l_false || m_rlimit.is_canceled());
}
else {
SASSERT(value(l) == l_true || m_rlimit.get_cancel_flag());
SASSERT(value(l) == l_true || m_rlimit.is_canceled());
SASSERT(!l.sign() || m_bvalues[b] == l_false);
SASSERT(l.sign() || m_bvalues[b] == l_true);
}

2
src/opt/maxlex.cpp
View file

@ -161,7 +161,7 @@ namespace opt {
case l_true:
if (!update_assignment())
return l_undef;
SASSERT(soft.value == l_true || m.limit().get_cancel_flag());
SASSERT(soft.value == l_true || m.limit().is_canceled());
break;
case l_false:
soft.set_value(l_false);

2
src/opt/maxres.cpp
View file

@ -216,7 +216,7 @@ public:
tout << *m_model << "assumptions: ";
for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " ";
tout << "\n";);
SASSERT(m_model->is_true(m_asms));
SASSERT(m_model->is_true(m_asms) || m.limit().is_canceled());
found_optimum();
return l_true;
case l_false:

5
src/qe/qe_arith.cpp
View file

@ -65,7 +65,7 @@ namespace qe {
DEBUG_CODE(expr_ref val(m);
eval(lit, val);
CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
SASSERT(m.limit().get_cancel_flag() || !m.is_false(val)););
SASSERT(m.limit().is_canceled() || !m.is_false(val)););
if (!m.inc())
return false;
@ -345,6 +345,9 @@ namespace qe {
if (is_arith(v) && !tids.contains(v)) {
rational r;
expr_ref val = eval(v);
if (!m.inc())
return vector<def>();
VERIFY(a.is_numeral(val, r));
TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
tids.insert(v, mbo.add_var(r, a.is_int(v)));

4
src/qe/qsat.cpp
View file

@ -647,8 +647,10 @@ namespace qe {
switch (res) {
case l_true:
s.get_model(m_model);
if (!m_model)
return l_undef;
SASSERT(validate_defs("check_sat"));
SASSERT(validate_assumptions(*m_model.get(), asms));
SASSERT(!m_model.get() || validate_assumptions(*m_model.get(), asms));
SASSERT(validate_model(asms));
TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
if (m_level == 0) {

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -963,6 +963,8 @@ private:
for (expr * f : m_fmls) {
expr_ref tmp(m);
eval(f, tmp);
if (m.limit().is_canceled())
return;
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
model_smt2_pp(tout, m, *(mdl.get()), 0););

4
src/smt/asserted_formulas.cpp
View file

@ -182,13 +182,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
void asserted_formulas::push_scope() {
reduce();
commit();
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().get_cancel_flag());
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
m_scoped_substitution.push();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_formulas_lim = m_formulas.size();
SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().get_cancel_flag());
SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().is_canceled());
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push();
m_elim_term_ite.push();

16
src/smt/smt_context.cpp
View file

@ -554,7 +554,7 @@ namespace smt {
catch (...) {
// Restore trail size since procedure was interrupted in the middle.
// If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().get_cancel_flag() << "\n";);
TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().is_canceled() << "\n";);
m_trail_stack.shrink(old_trail_size);
throw;
}
@ -2845,12 +2845,13 @@ namespace smt {
}
}
void context::push() {
TRACE("unit_subsumption_bug", display(tout << "context::push()\n"););
void context::push() {
pop_to_base_lvl();
setup_context(false);
bool was_consistent = !inconsistent();
internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
if (!m.inc())
throw default_exception("push canceled");
scoped_suspend_rlimit _suspend_cancel(m.limit());
propagate();
if (was_consistent && inconsistent() && !m_asserted_formulas.inconsistent()) {
@ -3084,6 +3085,7 @@ namespace smt {
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
reduce_assertions();
if (get_cancel_flag()) return;
if (!m_asserted_formulas.inconsistent()) {
unsigned sz = m_asserted_formulas.get_num_formulas();
unsigned qhead = m_asserted_formulas.get_qhead();
@ -4483,9 +4485,9 @@ namespace smt {
return false;
}
void context::get_model(model_ref & m) {
if (inconsistent())
m = nullptr;
void context::get_model(model_ref & mdl) {
if (inconsistent() || !m.inc())
mdl = nullptr;
else {
mk_proto_model();
if (!m_model && m_proto_model) {
@ -4497,7 +4499,7 @@ namespace smt {
// no op
}
}
m = m_model.get();
mdl = m_model.get();
}
}

2
src/smt/smt_context_inv.cpp
View file

@ -264,7 +264,7 @@ namespace smt {
bool context::check_th_diseq_propagation() const {
TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
int num = get_num_bool_vars();
if (inconsistent() || get_manager().limit().get_cancel_flag()) {
if (inconsistent() || get_manager().limit().is_canceled()) {
return true;
}
for (bool_var v = 0; v < num; v++) {

2
src/smt/tactic/smt_tactic.cpp
View file

@ -231,6 +231,8 @@ public:
mc = concat(fmc.get(), mc.get());
in->add(mc.get());
}
if (m_ctx->canceled())
throw tactic_exception(Z3_CANCELED_MSG);
return;
}
case l_false: {

4
src/smt/theory_arith_inv.h
View file

@ -191,7 +191,7 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::satisfy_bounds() const {
if (get_manager().limit().get_cancel_flag())
if (get_manager().limit().is_canceled())
return true;
int num = get_num_vars();
for (theory_var v = 0; v < num; v++) {
@ -217,7 +217,7 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::valid_assignment() const {
if (get_manager().limit().get_cancel_flag())
if (get_manager().limit().is_canceled())
return true;
if (valid_row_assignment() &&
satisfy_bounds() &&

2
src/smt/theory_bv.cpp
View file

@ -1811,7 +1811,7 @@ namespace smt {
}
bool theory_bv::check_invariant() {
if (m.limit().get_cancel_flag())
if (m.limit().is_canceled())
return true;
if (ctx.inconsistent())
return true;

2
src/smt/theory_lra.cpp
View file

@ -3441,7 +3441,7 @@ public:
else {
rational r = get_value(v);
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}

7
src/smt/theory_seq.cpp
View file

@ -507,8 +507,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
m_fixed.contains(e)) {
return false;
}
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_fixed, e));
m_fixed.insert(e);
@ -520,8 +518,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
}
else if (!is_zero) {
unsigned _lo = lo.get_unsigned();
expr_ref_vector elems(m);
expr_ref_vector elems(m);
for (unsigned j = 0; j < _lo; ++j) {
m_sk.decompose(seq, head, tail);
elems.push_back(head);
@ -2304,7 +2301,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
k.assert_expr(f);
}
lbool r = k.check();
if (r != l_false && !m.limit().get_cancel_flag()) {
if (r != l_false && !m.limit().is_canceled()) {
model_ref mdl;
k.get_model(mdl);
IF_VERBOSE(0,

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

@ -204,15 +204,15 @@ private:
return true;
case OP_BMUL:
model = rational::one();
return true;
case OP_BSDIV:
case OP_BSDIV0:
case OP_BSDIV_I:
case OP_BUDIV:
case OP_BUDIV0:
case OP_BUDIV_I:
model = rational::one();
return true;
default:
return false;
}

4
src/tactic/tactic.cpp
View file

@ -190,6 +190,10 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
(*mc)(labels);
model_converter2model(m, mc.get(), md);
}
if (!m.inc()) {
reason_unknown = "canceled";
return l_undef;
}
if (!md) {
// create empty model.
md = alloc(model, m);

6
src/util/rlimit.cpp
View file

@ -44,14 +44,12 @@ uint64_t reslimit::count() const {
bool reslimit::inc() {
++m_count;
bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
return r;
return not_canceled();
}
bool reslimit::inc(unsigned offset) {
m_count += offset;
bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
return r;
return not_canceled();
}
void reslimit::push(unsigned delta_limit) {

3
src/util/rlimit.h
View file

@ -50,7 +50,8 @@ public:
uint64_t count() const;
bool suspended() const { return m_suspend; }
bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; }
inline bool not_canceled() const { return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; }
inline bool is_canceled() const { return !not_canceled(); }
char const* get_cancel_msg() const;
void cancel();
void reset_cancel();