mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

fix #3028

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-17 00:20:01 -10:00
parent 8428970a1f
commit 234b53b831
3 changed files with 7 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/macros/macro_manager.cpp
View file

@ -126,6 +126,7 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
m_decl2macro_dep.insert(f, dep); m_decl2macro_dep.insert(f, dep);
TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";); TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
SASSERT(false);
// Nothing's forbidden anymore; if something's bad, we detected it earlier. // Nothing's forbidden anymore; if something's bad, we detected it earlier.
// mark_forbidden(m->get_expr()); // mark_forbidden(m->get_expr());
@ -267,17 +268,19 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
func_decl * d = n->get_decl(); func_decl * d = n->get_decl();
TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";); TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
if (mm.m_decl2macro.find(d, q)) { if (mm.m_decl2macro.find(d, q)) {
TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
app * head = nullptr; app * head = nullptr;
expr * def = nullptr; expr * def = nullptr;
mm.get_head_def(q, d, head, def); mm.get_head_def(q, d, head, def);
unsigned num = n->get_num_args(); unsigned num = n->get_num_args();
SASSERT(head && def); SASSERT(head && def);
TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n" << mk_pp(head, m) << " " << mk_pp(def, m) << "\n";);
ptr_buffer<expr> subst_args; ptr_buffer<expr> subst_args;
subst_args.resize(num, 0); subst_args.resize(num, 0);
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
var * v = to_var(head->get_arg(i)); var * v = to_var(head->get_arg(i));
SASSERT(v->get_idx() < num); if (v->get_idx() >= num)
return false;
unsigned nidx = num - v->get_idx() - 1; unsigned nidx = num - v->get_idx() - 1;
SASSERT(subst_args[nidx] == 0); SASSERT(subst_args[nidx] == 0);
subst_args[nidx] = n->get_arg(i); subst_args[nidx] = n->get_arg(i);

1
src/ast/macros/macro_util.cpp
View file

@ -436,6 +436,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
See normalize_expr See normalize_expr
*/ */
void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const { void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";);
SASSERT(is_macro_head(head, head->get_num_args())); SASSERT(is_macro_head(head, head->get_num_args()));
SASSERT(!occurs(head->get_decl(), def)); SASSERT(!occurs(head->get_decl(), def));
normalize_expr(head, num_decls, def, interp); normalize_expr(head, num_decls, def, interp);

14
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -25,7 +25,6 @@ Revision History:
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
@ -35,7 +34,6 @@ class fix_dl_var_tactic : public tactic {
struct failed {}; struct failed {};
ast_manager & m; ast_manager & m;
arith_util & m_util; arith_util & m_util;
seq_util m_seq;
expr_fast_mark1 * m_visited; expr_fast_mark1 * m_visited;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
obj_map<app, unsigned> m_occs; obj_map<app, unsigned> m_occs;
@ -43,8 +41,7 @@ class fix_dl_var_tactic : public tactic {
is_target(arith_util & u): is_target(arith_util & u):
m(u.get_manager()), m(u.get_manager()),
m_util(u), m_util(u){
m_seq(m) {
} }
void throw_failed(expr * ctx1, expr * ctx2 = nullptr) { void throw_failed(expr * ctx1, expr * ctx2 = nullptr) {
@ -56,15 +53,6 @@ class fix_dl_var_tactic : public tactic {
sort * s = m.get_sort(n); sort * s = m.get_sort(n);
return s->get_family_id() == m_util.get_family_id(); return s->get_family_id() == m_util.get_family_id();
} }
// Return true if n is uninterpreted with respect to arithmetic.
// sequence theory is not disjoint from arithmetic
bool is_uninterp(expr * n) {
if (!is_app(n)) return false;
app* t = to_app(n);
family_id fid = t->get_family_id();
return fid != m_util.get_family_id() && fid != m_seq.get_family_id();
}
// Remark: we say an expression is nested, if it occurs inside the boolean structure of the formula. // Remark: we say an expression is nested, if it occurs inside the boolean structure of the formula.
// That is, the expression is not part of an unit clause comprising of a single inequality/equality. // That is, the expression is not part of an unit clause comprising of a single inequality/equality.