mirror of
https://github.com/Z3Prover/z3
synced 2025-08-19 17:50:23 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3 into csp
This commit is contained in:
Nikolaj Bjorner
commit
ccca063e54
254 changed files with 1194 additions and 1753 deletions
|
|
@ -123,7 +123,7 @@ inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.
|
|||
|
||||
/**
|
||||
Return a if arg = (not a)
|
||||
Retur (not arg) otherwise
|
||||
Return (not arg) otherwise
|
||||
*/
|
||||
expr * mk_not(ast_manager & m, expr * arg);
|
||||
|
||||
|
|
|
|||
|
|
@ -231,7 +231,7 @@ namespace datatype {
|
|||
}
|
||||
return s;
|
||||
}
|
||||
catch (invalid_datatype) {
|
||||
catch (const invalid_datatype &) {
|
||||
m_manager->raise_exception("invalid datatype");
|
||||
return nullptr;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ bool has_skolem_functions(expr * n) {
|
|||
try {
|
||||
for_each_expr(p, n);
|
||||
}
|
||||
catch (has_skolem_functions_ns::found) {
|
||||
catch (const has_skolem_functions_ns::found &) {
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c,
|
|||
m_bindings(m)
|
||||
{
|
||||
updt_params(p);
|
||||
// We need to make sure that the mananger has the BV plugin loaded.
|
||||
// We need to make sure that the manager has the BV plugin loaded.
|
||||
symbol s_bv("bv");
|
||||
if (!m_manager.has_plugin(s_bv))
|
||||
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ public:
|
|||
void reset();
|
||||
|
||||
/**
|
||||
\brief Create a dependecy set.
|
||||
\brief Create a dependency set.
|
||||
This set should be populated using #collect_func_decls.
|
||||
After populating the set, it must be used as an argument for the #insert method.
|
||||
|
||||
|
|
|
|||
|
|
@ -263,7 +263,7 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
|
|||
m_occurrences.reset();
|
||||
|
||||
|
||||
// Find out how many non-ground appearences for each uninterpreted function there are
|
||||
// Find out how many non-ground appearances for each uninterpreted function there are
|
||||
for (unsigned i = 0 ; i < n ; i++)
|
||||
find_occurrences(exprs[i]);
|
||||
|
||||
|
|
@ -301,7 +301,7 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
|
|||
m_occurrences.reset();
|
||||
|
||||
|
||||
// Find out how many non-ground appearences for each uninterpreted function there are
|
||||
// Find out how many non-ground appearances for each uninterpreted function there are
|
||||
for ( unsigned i = 0 ; i < n ; i++ )
|
||||
find_occurrences(exprs[i].get_fml());
|
||||
|
||||
|
|
|
|||
|
|
@ -258,7 +258,6 @@ struct nnf::imp {
|
|||
// configuration ----------------
|
||||
nnf_mode m_mode;
|
||||
bool m_ignore_labels;
|
||||
bool m_skolemize;
|
||||
// ------------------------------
|
||||
|
||||
name_exprs * m_name_nested_formulas;
|
||||
|
|
@ -312,7 +311,6 @@ struct nnf::imp {
|
|||
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";);
|
||||
|
||||
m_ignore_labels = p.ignore_labels();
|
||||
m_skolemize = p.skolemize();
|
||||
m_max_memory = megabytes_to_bytes(p.max_memory());
|
||||
m_skolemizer.set_sk_hack(p.sk_hack());
|
||||
}
|
||||
|
|
@ -759,7 +757,7 @@ struct nnf::imp {
|
|||
if (!visit(q->get_expr(), fr.m_pol, true))
|
||||
return false;
|
||||
}
|
||||
else if (is_forall(q) == fr.m_pol || !m_skolemize) {
|
||||
else if (is_forall(q) == fr.m_pol) {
|
||||
if (!visit(q->get_expr(), fr.m_pol, true))
|
||||
return false;
|
||||
}
|
||||
|
|
@ -788,7 +786,7 @@ struct nnf::imp {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
else if (is_forall(q) == fr.m_pol || !m_skolemize) {
|
||||
else if (is_forall(q) == fr.m_pol) {
|
||||
expr * new_expr = m_result_stack.back();
|
||||
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : nullptr;
|
||||
|
||||
|
|
|
|||
|
|
@ -5,5 +5,4 @@ def_module_params('nnf',
|
|||
('sk_hack', BOOL, False, 'hack for VCC'),
|
||||
('mode', SYMBOL, 'skolem',
|
||||
'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full'),
|
||||
('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled'),
|
||||
('skolemize', BOOL, True, 'skolemize (existential force) quantifiers')))
|
||||
('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled')))
|
||||
|
|
|
|||
|
|
@ -24,11 +24,11 @@ Notes:
|
|||
struct pull_quant::imp {
|
||||
|
||||
struct rw_cfg : public default_rewriter_cfg {
|
||||
ast_manager & m_manager;
|
||||
ast_manager & m;
|
||||
shift_vars m_shift;
|
||||
|
||||
rw_cfg(ast_manager & m):
|
||||
m_manager(m),
|
||||
m(m),
|
||||
m_shift(m) {
|
||||
}
|
||||
|
||||
|
|
@ -43,14 +43,14 @@ struct pull_quant::imp {
|
|||
// Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...)))
|
||||
// So, when pulling a quantifier over a NOT, it becomes an exists.
|
||||
|
||||
if (m_manager.is_not(d)) {
|
||||
if (m.is_not(d)) {
|
||||
SASSERT(num_children == 1);
|
||||
expr * child = children[0];
|
||||
if (is_quantifier(child)) {
|
||||
quantifier * q = to_quantifier(child);
|
||||
expr * body = q->get_expr();
|
||||
quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k;
|
||||
result = m_manager.update_quantifier(q, k, m_manager.mk_not(body));
|
||||
result = m.update_quantifier(q, k, m.mk_not(body));
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
|
|
@ -86,7 +86,7 @@ struct pull_quant::imp {
|
|||
var_sorts.push_back(nested_q->get_decl_sort(j));
|
||||
symbol s = nested_q->get_decl_name(j);
|
||||
if (std::find(var_names.begin(), var_names.end(), s) != var_names.end())
|
||||
var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? nullptr : s.bare_str()));
|
||||
var_names.push_back(m.mk_fresh_var_name(s.is_numerical() ? nullptr : s.bare_str()));
|
||||
else
|
||||
var_names.push_back(s);
|
||||
}
|
||||
|
|
@ -96,8 +96,8 @@ struct pull_quant::imp {
|
|||
if (!var_sorts.empty()) {
|
||||
SASSERT(found_quantifier);
|
||||
// adjust the variable ids in formulas in new_children
|
||||
expr_ref_buffer new_adjusted_children(m_manager);
|
||||
expr_ref adjusted_child(m_manager);
|
||||
expr_ref_buffer new_adjusted_children(m);
|
||||
expr_ref adjusted_child(m);
|
||||
unsigned num_decls = var_sorts.size();
|
||||
unsigned shift_amount = 0;
|
||||
TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";);
|
||||
|
|
@ -108,7 +108,7 @@ struct pull_quant::imp {
|
|||
// child will be in the scope of num_decls bound variables.
|
||||
m_shift(child, num_decls, adjusted_child);
|
||||
TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" <<
|
||||
mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
|
||||
mk_pp(child, m) << "\n---->\n" << mk_pp(adjusted_child, m) << "\n";);
|
||||
}
|
||||
else {
|
||||
quantifier * nested_q = to_quantifier(child);
|
||||
|
|
@ -130,8 +130,8 @@ struct pull_quant::imp {
|
|||
shift_amount, // shift2 (shift by this amount if var idx < bound)
|
||||
adjusted_child);
|
||||
TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount <<
|
||||
" shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) <<
|
||||
"\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
|
||||
" shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m) <<
|
||||
"\n---->\n" << mk_pp(adjusted_child, m) << "\n";);
|
||||
shift_amount += nested_q->get_num_decls();
|
||||
}
|
||||
new_adjusted_children.push_back(adjusted_child);
|
||||
|
|
@ -150,11 +150,11 @@ struct pull_quant::imp {
|
|||
// 3) MBQI
|
||||
std::reverse(var_sorts.begin(), var_sorts.end());
|
||||
std::reverse(var_names.begin(), var_names.end());
|
||||
result = m_manager.mk_quantifier(forall_children ? forall_k : exists_k,
|
||||
result = m.mk_quantifier(forall_children ? forall_k : exists_k,
|
||||
var_sorts.size(),
|
||||
var_sorts.c_ptr(),
|
||||
var_names.c_ptr(),
|
||||
m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()),
|
||||
m.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()),
|
||||
w,
|
||||
qid);
|
||||
return true;
|
||||
|
|
@ -167,7 +167,7 @@ struct pull_quant::imp {
|
|||
|
||||
void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) {
|
||||
if (!pull_quant1_core(d, num_children, children, result)) {
|
||||
result = m_manager.mk_app(d, num_children, children);
|
||||
result = m.mk_app(d, num_children, children);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -185,7 +185,7 @@ struct pull_quant::imp {
|
|||
var_names.append(nested_q->get_num_decls(), const_cast<symbol*>(nested_q->get_decl_names()));
|
||||
// Remark: patterns are ignored.
|
||||
// See comment in reduce1_app
|
||||
result = m_manager.mk_forall(var_sorts.size(),
|
||||
result = m.mk_forall(var_sorts.size(),
|
||||
var_sorts.c_ptr(),
|
||||
var_names.c_ptr(),
|
||||
nested_q->get_expr(),
|
||||
|
|
@ -201,7 +201,7 @@ struct pull_quant::imp {
|
|||
}
|
||||
else {
|
||||
SASSERT(!is_quantifier(new_expr));
|
||||
result = m_manager.update_quantifier(q, new_expr);
|
||||
result = m.update_quantifier(q, new_expr);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -218,36 +218,36 @@ struct pull_quant::imp {
|
|||
void pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
|
||||
pr = nullptr;
|
||||
if (is_app(n)) {
|
||||
expr_ref_buffer new_args(m_manager);
|
||||
expr_ref new_arg(m_manager);
|
||||
expr_ref_buffer new_args(m);
|
||||
expr_ref new_arg(m);
|
||||
ptr_buffer<proof> proofs;
|
||||
for (expr * arg : *to_app(n)) {
|
||||
pull_quant1(arg , new_arg);
|
||||
new_args.push_back(new_arg);
|
||||
if (new_arg != arg)
|
||||
proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
|
||||
proofs.push_back(m.mk_pull_quant(arg, to_quantifier(new_arg)));
|
||||
}
|
||||
pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
|
||||
if (m_manager.proofs_enabled()) {
|
||||
app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
proof * p1 = proofs.empty() ? nullptr : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
|
||||
proof * p2 = r1 == r ? nullptr : m_manager.mk_pull_quant(r1, to_quantifier(r));
|
||||
pr = m_manager.mk_transitivity(p1, p2);
|
||||
if (m.proofs_enabled()) {
|
||||
app * r1 = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
proof * p1 = proofs.empty() ? nullptr : m.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
|
||||
proof * p2 = r1 == r ? nullptr : m.mk_pull_quant(r1, to_quantifier(r));
|
||||
pr = m.mk_transitivity(p1, p2);
|
||||
}
|
||||
}
|
||||
else if (is_quantifier(n)) {
|
||||
expr_ref new_expr(m_manager);
|
||||
expr_ref new_expr(m);
|
||||
pull_quant1(to_quantifier(n)->get_expr(), new_expr);
|
||||
pull_quant1(to_quantifier(n), new_expr, r);
|
||||
if (m_manager.proofs_enabled()) {
|
||||
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
|
||||
if (m.proofs_enabled()) {
|
||||
quantifier * q1 = m.update_quantifier(to_quantifier(n), new_expr);
|
||||
proof * p1 = nullptr;
|
||||
if (n != q1) {
|
||||
proof * p0 = m_manager.mk_pull_quant(n, to_quantifier(new_expr));
|
||||
p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
|
||||
proof * p0 = m.mk_pull_quant(n, to_quantifier(new_expr));
|
||||
p1 = m.mk_quant_intro(to_quantifier(n), q1, p0);
|
||||
}
|
||||
proof * p2 = q1 == r ? nullptr : m_manager.mk_pull_quant(q1, to_quantifier(r));
|
||||
pr = m_manager.mk_transitivity(p1, p2);
|
||||
proof * p2 = q1 == r ? nullptr : m.mk_pull_quant(q1, to_quantifier(r));
|
||||
pr = m.mk_transitivity(p1, p2);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
@ -256,14 +256,14 @@ struct pull_quant::imp {
|
|||
}
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
if (!m_manager.is_or(f) && !m_manager.is_and(f) && !m_manager.is_not(f))
|
||||
if (!m.is_or(f) && !m.is_and(f) && !m.is_not(f))
|
||||
return BR_FAILED;
|
||||
|
||||
if (!pull_quant1_core(f, num, args, result))
|
||||
return BR_FAILED;
|
||||
|
||||
if (m_manager.proofs_enabled()) {
|
||||
result_pr = m_manager.mk_pull_quant(m_manager.mk_app(f, num, args),
|
||||
if (m.proofs_enabled()) {
|
||||
result_pr = m.mk_pull_quant(m.mk_app(f, num, args),
|
||||
to_quantifier(result.get()));
|
||||
}
|
||||
return BR_DONE;
|
||||
|
|
@ -277,8 +277,11 @@ struct pull_quant::imp {
|
|||
proof_ref & result_pr) {
|
||||
|
||||
if (is_exists(old_q)) {
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
result = m.mk_not(new_body);
|
||||
result = m.mk_not(m.update_quantifier(old_q, exists_k, result));
|
||||
if (m.proofs_enabled())
|
||||
m.mk_rewrite(old_q, result);
|
||||
return true;
|
||||
}
|
||||
if (is_lambda(old_q)) {
|
||||
return false;
|
||||
|
|
@ -288,8 +291,8 @@ struct pull_quant::imp {
|
|||
return false;
|
||||
|
||||
pull_quant1_core(old_q, new_body, result);
|
||||
if (m_manager.proofs_enabled())
|
||||
result_pr = m_manager.mk_pull_quant(old_q, to_quantifier(result.get()));
|
||||
if (m.proofs_enabled())
|
||||
result_pr = m.mk_pull_quant(old_q, to_quantifier(result.get()));
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ bool occurs(expr * n1, expr * n2) {
|
|||
try {
|
||||
quick_for_each_expr(p, n2);
|
||||
}
|
||||
catch (occurs_namespace::found) {
|
||||
catch (const occurs_namespace::found &) {
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
|
@ -69,7 +69,7 @@ bool occurs(func_decl * d, expr * n) {
|
|||
try {
|
||||
quick_for_each_expr(p, n);
|
||||
}
|
||||
catch (occurs_namespace::found) {
|
||||
catch (const occurs_namespace::found &) {
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
|
|
|||
|
|
@ -687,7 +687,7 @@ bool pattern_inference_cfg::reduce_quantifier(
|
|||
mk_patterns(result2->get_num_decls(), result2->get_expr(), 0, nullptr, new_patterns);
|
||||
if (!new_patterns.empty()) {
|
||||
if (m_params.m_pi_warnings) {
|
||||
warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
|
||||
warning_msg("pulled nested quantifier to be able to find an usable pattern (quantifier id: %s)", q->get_qid().str().c_str());
|
||||
}
|
||||
new_q = m.update_quantifier(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr());
|
||||
if (m.proofs_enabled()) {
|
||||
|
|
|
|||
|
|
@ -111,7 +111,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
|
|||
numeral val, val1;
|
||||
unsigned bv_sz1;
|
||||
|
||||
if (0) {
|
||||
if (false) {
|
||||
if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) {
|
||||
return record(to_app(lhs), val, val, negated, nis);
|
||||
}
|
||||
|
|
@ -125,7 +125,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
|
|||
return record(to_app(lhs), numeral::zero(), val, negated, nis);
|
||||
}
|
||||
|
||||
if (1) {
|
||||
if (true) {
|
||||
numeral rhs_val;
|
||||
unsigned rhs_sz;
|
||||
if (m_m.is_eq(e, lhs, rhs)
|
||||
|
|
@ -343,7 +343,7 @@ bool bv_bounds::add_constraint(expr* e) {
|
|||
numeral val, val1;
|
||||
unsigned bv_sz1;
|
||||
|
||||
if (0) {
|
||||
if (false) {
|
||||
if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) {
|
||||
return add_bound_unsigned(to_app(lhs), val, val, negated);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2679,7 +2679,7 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu
|
|||
}
|
||||
|
||||
const unsigned sz = m_util.get_bv_size(rhs);
|
||||
if (sz == 1) { // detect (lhs = N) ? C : D, where N, C, D are 1 bit numberals
|
||||
if (sz == 1) { // detect (lhs = N) ? C : D, where N, C, D are 1 bit numerals
|
||||
numeral rhs_n, e_n, t_n;
|
||||
unsigned rhs_sz, e_sz, t_sz;
|
||||
if (is_numeral(rhs, rhs_n, rhs_sz)
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ br_status datatype_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & resul
|
|||
// (= (+ c5 a5) b5) <<< NOT SIMPLIFIED WITH RESPECT TO ARITHMETIC
|
||||
// (= (cons a6 nil) (cons b6 nil))) <<< NOT SIMPLIFIED WITH RESPECT TO DATATYPE theory
|
||||
//
|
||||
// Note that asserted_formulas::reduce() applied the simplier many times.
|
||||
// Note that asserted_formulas::reduce() applied the simplifier many times.
|
||||
// After the first simplification step we had:
|
||||
// (= a1 b1)
|
||||
// (= (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))
|
||||
|
|
|
|||
|
|
@ -108,7 +108,7 @@ Revision History:
|
|||
apply var_subst using m_map to this child, and store the result in a new children array
|
||||
Create a new OR (new body of the quantifier) using the new children
|
||||
Then, we create a new quantifier using this new body, and use the function elim_unused_vars to
|
||||
eliminate the ununsed variables.
|
||||
eliminate the unused variables.
|
||||
|
||||
Remark: let us implement the new version inside the class der.
|
||||
Use #if 0 ... #endif to comment the old version.
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
|
|||
\brief Variation of push_app_ite that applies the transformation on nonground terms only.
|
||||
|
||||
\remark This functor uses the app::is_ground method. This method is not
|
||||
completly precise, for instance, any term containing a quantifier is marked as non ground.
|
||||
completely precise, for instance, any term containing a quantifier is marked as non ground.
|
||||
*/
|
||||
class ng_push_app_ite_cfg : public push_app_ite_cfg {
|
||||
protected:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue