mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
fixup std-order / inv-order
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
66bb310966
commit
969511ac00
|
@ -30,7 +30,7 @@ class contains_vars::imp {
|
|||
|
||||
void visit(expr * n, unsigned delta, bool & visited) {
|
||||
expr_delta_pair e(n, delta);
|
||||
if (!m_cache.contains(e)) {
|
||||
if (!is_ground(n) && !m_cache.contains(e)) {
|
||||
m_todo.push_back(e);
|
||||
visited = false;
|
||||
}
|
||||
|
@ -74,6 +74,7 @@ public:
|
|||
m_todo.push_back(expr_delta_pair(n, begin));
|
||||
while (!m_todo.empty()) {
|
||||
expr_delta_pair e = m_todo.back();
|
||||
|
||||
if (visit_children(e.m_node, e.m_delta)) {
|
||||
m_cache.insert(e);
|
||||
m_todo.pop_back();
|
||||
|
|
|
@ -59,7 +59,7 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
|
|||
new_args.push_back(arg);
|
||||
else {
|
||||
unsigned idx = to_var(arg)->get_idx();
|
||||
new_args.push_back(m_std_order ? args[idx] : args[num_args - idx - 1]);
|
||||
new_args.push_back(m_std_order ? args[num_args - idx - 1] : args[idx]);
|
||||
}
|
||||
}
|
||||
result = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.data());
|
||||
|
|
|
@ -116,6 +116,7 @@ namespace smt2 {
|
|||
symbol m_match;
|
||||
symbol m_case;
|
||||
symbol m_underscore;
|
||||
contains_vars m_has_free_vars;
|
||||
|
||||
typedef std::pair<symbol, expr*> named_expr;
|
||||
named_expr m_last_named_expr;
|
||||
|
@ -1031,7 +1032,7 @@ namespace smt2 {
|
|||
|
||||
void name_expr(expr * n, symbol const & s) {
|
||||
TRACE("name_expr", tout << "naming: " << s << " ->\n" << mk_pp(n, m()) << "\n";);
|
||||
if (!is_ground(n) && has_free_vars(n))
|
||||
if (!is_ground(n) && m_has_free_vars(n))
|
||||
throw parser_exception("invalid named expression, expression contains free variables");
|
||||
m_ctx.insert(s, 0, nullptr, n);
|
||||
m_last_named_expr.first = s;
|
||||
|
|
Loading…
Reference in a new issue