mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

refactor occurrence utility for common use (to be used in ctx_simplifier) per Nuno's suggestion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-09 15:53:02 -08:00
parent 9743c188da
commit 03a0a6f6a1
3 changed files with 138 additions and 82 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

97
src/tactic/core/collect_occs.cpp Normal file
View file

@ -0,0 +1,97 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
collect_cccs.cpp
Abstract:
Collect variables by occurrences.
Author:
Leonardo (leonardo) 2011-10-22
Notes:
--*/
#include "ast.h"
#include "goal.h"
#include "hashtable.h"
#include "collect_occs.h"
bool collect_occs::visit(expr * t) {
if (m_visited.is_marked(t)) {
if (is_uninterp_const(t))
m_more_than_once.mark(t);
return true;
}
m_visited.mark(t);
if (is_uninterp_const(t)) {
m_vars.push_back(to_app(t));
return true;
}
if (is_var(t))
return true;
if (is_app(t) && to_app(t)->get_num_args() == 0)
return true;
m_stack.push_back(frame(t, 0));
return false;
}
void collect_occs::process(expr * t) {
SASSERT(m_stack.empty());
if (visit(t))
return;
SASSERT(!m_stack.empty());
unsigned num;
expr * child;
while (!m_stack.empty()) {
start:
frame & fr = m_stack.back();
expr * t = fr.first;
switch (t->get_kind()) {
case AST_APP:
num = to_app(t)->get_num_args();
while (fr.second < num) {
child = to_app(t)->get_arg(fr.second);
fr.second++;
if (!visit(child))
goto start;
}
m_stack.pop_back();
break;
case AST_QUANTIFIER:
// don't need to visit patterns
child = to_quantifier(t)->get_expr();
fr.second++;
if (!visit(child))
goto start;
m_stack.pop_back();
break;
default:
UNREACHABLE();
}
}
}
void collect_occs::operator()(goal const & g, obj_hashtable<expr> & r) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
expr * t = g.form(i);
process(t);
}
ptr_vector<app>::const_iterator it = m_vars.begin();
ptr_vector<app>::const_iterator end = m_vars.end();
for (; it != end; ++it) {
if (m_more_than_once.is_marked(*it))
continue;
r.insert(*it);
}
m_visited.reset();
m_more_than_once.reset();
}

38
src/tactic/core/collect_occs.h Normal file
View file

@ -0,0 +1,38 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
collect_cccs.h
Abstract:
Collect variables by occurrences.
Author:
Leonardo (leonardo) 2011-10-22
Notes:
--*/
#ifndef COLLECT_OCCS_H_
#define COLLECT_OCCS_H_
class collect_occs {
expr_fast_mark1 m_visited;
expr_fast_mark2 m_more_than_once;
typedef std::pair<expr *, unsigned> frame;
svector<frame> m_stack;
ptr_vector<app> m_vars;
bool visit(expr * t);
void process(expr * t);
public:
void operator()(goal const & g, obj_hashtable<expr> & r);
};
#endif

85
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"collect_occs.h"
#include"cooperate.h"
#include"ast_smt2_pp.h"
#include"ast_ll_pp.h"
@ -32,86 +33,6 @@ class elim_uncnstr_tactic : public tactic {
struct imp {
// unconstrained vars collector
struct collect {
expr_fast_mark1 m_visited;
expr_fast_mark2 m_more_than_once;
typedef std::pair<expr *, unsigned> frame;
svector<frame> m_stack;
ptr_vector<app> m_vars;
bool visit(expr * t) {
if (m_visited.is_marked(t)) {
if (is_uninterp_const(t))
m_more_than_once.mark(t);
return true;
}
m_visited.mark(t);
if (is_uninterp_const(t)) {
m_vars.push_back(to_app(t));
return true;
}
if (is_var(t))
return true;
if (is_app(t) && to_app(t)->get_num_args() == 0)
return true;
m_stack.push_back(frame(t, 0));
return false;
}
void process(expr * t) {
SASSERT(m_stack.empty());
if (visit(t))
return;
SASSERT(!m_stack.empty());
unsigned num;
expr * child;
while (!m_stack.empty()) {
start:
frame & fr = m_stack.back();
expr * t = fr.first;
switch (t->get_kind()) {
case AST_APP:
num = to_app(t)->get_num_args();
while (fr.second < num) {
child = to_app(t)->get_arg(fr.second);
fr.second++;
if (!visit(child))
goto start;
}
m_stack.pop_back();
break;
case AST_QUANTIFIER:
// don't need to visit patterns
child = to_quantifier(t)->get_expr();
fr.second++;
if (!visit(child))
goto start;
m_stack.pop_back();
break;
default:
UNREACHABLE();
}
}
}
void operator()(goal const & g, obj_hashtable<expr> & r) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
expr * t = g.form(i);
process(t);
}
ptr_vector<app>::const_iterator it = m_vars.begin();
ptr_vector<app>::const_iterator end = m_vars.end();
for (; it != end; ++it) {
if (m_more_than_once.is_marked(*it))
continue;
r.insert(*it);
}
m_visited.reset();
m_more_than_once.reset();
}
};
typedef extension_model_converter mc;
@ -910,7 +831,7 @@ class elim_uncnstr_tactic : public tactic {
TRACE("elim_uncnstr_bug", g->display(tout););
tactic_report report("elim-uncnstr-vars", *g);
m_vars.reset();
collect p;
collect_occs p;
p(*g, m_vars);
if (m_vars.empty()) {
result.push_back(g.get());
@ -977,7 +898,7 @@ class elim_uncnstr_tactic : public tactic {
m_rw->reset(); // reset cache
m_vars.reset();
{
collect p;
collect_occs p;
p(*g, m_vars);
}
if (m_vars.empty())