mirror of
https://github.com/Z3Prover/z3
synced 2025-06-29 01:18:45 +00:00
reindent
This commit is contained in:
Doug Woos
parent
c0bb6dd2be
commit
89ba99918e
1 changed files with 151 additions and 151 deletions
|
|
@ -3,15 +3,15 @@ Copyright (c) 2016 Microsoft Corporation
|
||||||
|
|
||||||
Module Name:
|
Module Name:
|
||||||
|
|
||||||
sine_filter.cpp
|
sine_filter.cpp
|
||||||
|
|
||||||
Abstract:
|
Abstract:
|
||||||
|
|
||||||
Tactic that performs Sine Qua Non premise selection
|
Tactic that performs Sine Qua Non premise selection
|
||||||
|
|
||||||
Author:
|
Author:
|
||||||
|
|
||||||
Doug Woos
|
Doug Woos
|
||||||
|
|
||||||
Revision History:
|
Revision History:
|
||||||
--*/
|
--*/
|
||||||
|
|
@ -35,7 +35,7 @@ class sine_tactic : public tactic {
|
||||||
public:
|
public:
|
||||||
|
|
||||||
sine_tactic(ast_manager& m, params_ref const& p):
|
sine_tactic(ast_manager& m, params_ref const& p):
|
||||||
m(m), m_params(p) {}
|
m(m), m_params(p) {}
|
||||||
|
|
||||||
virtual tactic * translate(ast_manager & m) {
|
virtual tactic * translate(ast_manager & m) {
|
||||||
return alloc(sine_tactic, m, m_params);
|
return alloc(sine_tactic, m, m_params);
|
||||||
|
|
@ -61,7 +61,7 @@ public:
|
||||||
TRACE("sine", tout << new_forms.size(););
|
TRACE("sine", tout << new_forms.size(););
|
||||||
g->reset();
|
g->reset();
|
||||||
for (unsigned i = 0; i < new_forms.size(); i++) {
|
for (unsigned i = 0; i < new_forms.size(); i++) {
|
||||||
g->assert_expr(new_forms.get(i), 0, 0);
|
g->assert_expr(new_forms.get(i), 0, 0);
|
||||||
}
|
}
|
||||||
g->inc_depth();
|
g->inc_depth();
|
||||||
g->updt_prec(goal::OVER);
|
g->updt_prec(goal::OVER);
|
||||||
|
|
@ -77,169 +77,169 @@ public:
|
||||||
|
|
||||||
private:
|
private:
|
||||||
|
|
||||||
// is this a user-defined symbol name?
|
// is this a user-defined symbol name?
|
||||||
bool is_name(func_decl * f) {
|
bool is_name(func_decl * f) {
|
||||||
return f->get_family_id() < 0;
|
return f->get_family_id() < 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
typedef std::pair<expr*,expr*> t_work_item;
|
typedef std::pair<expr*,expr*> t_work_item;
|
||||||
|
|
||||||
t_work_item work_item(expr *e, expr *root) {
|
t_work_item work_item(expr *e, expr *root) {
|
||||||
return std::pair<expr*, expr*>(e, root);
|
return std::pair<expr*, expr*>(e, root);
|
||||||
}
|
}
|
||||||
|
|
||||||
void find_constants(expr *e, obj_hashtable<func_decl> &consts) {
|
void find_constants(expr *e, obj_hashtable<func_decl> &consts) {
|
||||||
ptr_vector<expr> stack;
|
ptr_vector<expr> stack;
|
||||||
stack.push_back(e);
|
stack.push_back(e);
|
||||||
expr *curr;
|
expr *curr;
|
||||||
while (!stack.empty()) {
|
while (!stack.empty()) {
|
||||||
curr = stack.back();
|
curr = stack.back();
|
||||||
stack.pop_back();
|
stack.pop_back();
|
||||||
if (is_app(curr)) {
|
if (is_app(curr)) {
|
||||||
app *a = to_app(curr);
|
app *a = to_app(curr);
|
||||||
func_decl *f = a->get_decl();
|
func_decl *f = a->get_decl();
|
||||||
if (is_name(f) && !consts.contains(f)) {
|
if (is_name(f) && !consts.contains(f)) {
|
||||||
consts.insert(f);
|
consts.insert(f);
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
bool quantifier_matches(quantifier *q,
|
bool quantifier_matches(quantifier *q,
|
||||||
obj_hashtable<func_decl> const & consts,
|
obj_hashtable<func_decl> const & consts,
|
||||||
ptr_vector<func_decl> & next_consts) {
|
ptr_vector<func_decl> & next_consts) {
|
||||||
TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";);
|
TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";);
|
||||||
for (obj_hashtable<func_decl>::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) {
|
for (obj_hashtable<func_decl>::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) {
|
||||||
TRACE("sine", tout << *constit; tout << "\n";);
|
TRACE("sine", tout << *constit; tout << "\n";);
|
||||||
}
|
|
||||||
bool matched = false;
|
|
||||||
for (int i = 0; i < q->get_num_patterns(); i++) {
|
|
||||||
bool p_matched = true;
|
|
||||||
vector<expr *> stack;
|
|
||||||
expr *curr;
|
|
||||||
// patterns are wrapped with "pattern"
|
|
||||||
stack.push_back(to_app(q->get_pattern(i))->get_arg(0));
|
|
||||||
while (!stack.empty()) {
|
|
||||||
curr = stack.back();
|
|
||||||
stack.pop_back();
|
|
||||||
if (is_app(curr)) {
|
|
||||||
app *a = to_app(curr);
|
|
||||||
func_decl *f = a->get_decl();
|
|
||||||
if (!consts.contains(f)) {
|
|
||||||
TRACE("sine", tout << f; tout << "\n";);
|
|
||||||
p_matched = false;
|
|
||||||
next_consts.push_back(f);
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
for (int j = 0; j < a->get_num_args(); j++) {
|
|
||||||
stack.push_back(a->get_arg(j));
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
bool matched = false;
|
||||||
if (p_matched) {
|
for (int i = 0; i < q->get_num_patterns(); i++) {
|
||||||
matched = true;
|
bool p_matched = true;
|
||||||
break;
|
vector<expr *> stack;
|
||||||
}
|
expr *curr;
|
||||||
|
// patterns are wrapped with "pattern"
|
||||||
|
stack.push_back(to_app(q->get_pattern(i))->get_arg(0));
|
||||||
|
while (!stack.empty()) {
|
||||||
|
curr = stack.back();
|
||||||
|
stack.pop_back();
|
||||||
|
if (is_app(curr)) {
|
||||||
|
app *a = to_app(curr);
|
||||||
|
func_decl *f = a->get_decl();
|
||||||
|
if (!consts.contains(f)) {
|
||||||
|
TRACE("sine", tout << f; tout << "\n";);
|
||||||
|
p_matched = false;
|
||||||
|
next_consts.push_back(f);
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
for (int j = 0; j < a->get_num_args(); j++) {
|
||||||
|
stack.push_back(a->get_arg(j));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (p_matched) {
|
||||||
|
matched = true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return matched;
|
||||||
}
|
}
|
||||||
return matched;
|
|
||||||
}
|
|
||||||
|
|
||||||
void filter_expressions(goal_ref const & g, ptr_vector<expr> & new_exprs) {
|
void filter_expressions(goal_ref const & g, ptr_vector<expr> & new_exprs) {
|
||||||
obj_map<func_decl, obj_hashtable<expr> > const2exp;
|
obj_map<func_decl, obj_hashtable<expr> > const2exp;
|
||||||
obj_map<expr, obj_hashtable<func_decl> > exp2const;
|
obj_map<expr, obj_hashtable<func_decl> > exp2const;
|
||||||
obj_map<func_decl, obj_pair_hashtable<expr, expr> > const2quantifier;
|
obj_map<func_decl, obj_pair_hashtable<expr, expr> > const2quantifier;
|
||||||
obj_hashtable<func_decl> consts;
|
obj_hashtable<func_decl> consts;
|
||||||
vector<t_work_item> stack;
|
vector<t_work_item> stack;
|
||||||
for (int i = 0; i < g->size(); i++) {
|
for (int i = 0; i < g->size(); i++) {
|
||||||
stack.push_back(work_item(g->form(i), g->form(i)));
|
stack.push_back(work_item(g->form(i), g->form(i)));
|
||||||
}
|
|
||||||
t_work_item curr;
|
|
||||||
while (!stack.empty()) {
|
|
||||||
curr = stack.back();
|
|
||||||
stack.pop_back();
|
|
||||||
if (is_app(curr.first)) {
|
|
||||||
app *a = to_app(curr.first);
|
|
||||||
func_decl *f = a->get_decl();
|
|
||||||
if (is_name(f)) {
|
|
||||||
if (!consts.contains(f)) {
|
|
||||||
consts.insert(f);
|
|
||||||
if (const2quantifier.contains(f)) {
|
|
||||||
for (obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) {
|
|
||||||
stack.push_back(*it);
|
|
||||||
}
|
|
||||||
const2quantifier.remove(f);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (!const2exp.contains(f)) {
|
|
||||||
const2exp.insert(f, obj_hashtable<expr>());
|
|
||||||
}
|
|
||||||
if (!const2exp[f].contains(curr.second)) {
|
|
||||||
const2exp[f].insert(curr.second);
|
|
||||||
}
|
|
||||||
if (!exp2const.contains(curr.second)) {
|
|
||||||
exp2const.insert(curr.second, obj_hashtable<func_decl>());
|
|
||||||
}
|
|
||||||
if (!exp2const[curr.second].contains(f)) {
|
|
||||||
exp2const[curr.second].insert(f);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
for (int i = 0; i < a->get_num_args(); i++) {
|
t_work_item curr;
|
||||||
stack.push_back(work_item(a->get_arg(i), curr.second));
|
while (!stack.empty()) {
|
||||||
}
|
curr = stack.back();
|
||||||
}
|
stack.pop_back();
|
||||||
else if (is_quantifier(curr.first)) {
|
if (is_app(curr.first)) {
|
||||||
quantifier *q = to_quantifier(curr.first);
|
app *a = to_app(curr.first);
|
||||||
if (q->is_forall()) {
|
func_decl *f = a->get_decl();
|
||||||
if (q->has_patterns()) {
|
if (is_name(f)) {
|
||||||
ptr_vector<func_decl> next_consts;
|
if (!consts.contains(f)) {
|
||||||
if (quantifier_matches(q, consts, next_consts)) {
|
consts.insert(f);
|
||||||
stack.push_back(work_item(q->get_expr(), curr.second));
|
if (const2quantifier.contains(f)) {
|
||||||
}
|
for (obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) {
|
||||||
else {
|
stack.push_back(*it);
|
||||||
for (unsigned i = 0; i < next_consts.size(); i++) {
|
}
|
||||||
func_decl *c = next_consts.get(i);
|
const2quantifier.remove(f);
|
||||||
if (!const2quantifier.contains(c)) {
|
}
|
||||||
const2quantifier.insert(c, obj_pair_hashtable<expr, expr>());
|
}
|
||||||
|
if (!const2exp.contains(f)) {
|
||||||
|
const2exp.insert(f, obj_hashtable<expr>());
|
||||||
|
}
|
||||||
|
if (!const2exp[f].contains(curr.second)) {
|
||||||
|
const2exp[f].insert(curr.second);
|
||||||
|
}
|
||||||
|
if (!exp2const.contains(curr.second)) {
|
||||||
|
exp2const.insert(curr.second, obj_hashtable<func_decl>());
|
||||||
|
}
|
||||||
|
if (!exp2const[curr.second].contains(f)) {
|
||||||
|
exp2const[curr.second].insert(f);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
if (!const2quantifier[c].contains(curr)) {
|
for (int i = 0; i < a->get_num_args(); i++) {
|
||||||
const2quantifier[c].insert(curr);
|
stack.push_back(work_item(a->get_arg(i), curr.second));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else if (is_quantifier(curr.first)) {
|
||||||
|
quantifier *q = to_quantifier(curr.first);
|
||||||
|
if (q->is_forall()) {
|
||||||
|
if (q->has_patterns()) {
|
||||||
|
ptr_vector<func_decl> next_consts;
|
||||||
|
if (quantifier_matches(q, consts, next_consts)) {
|
||||||
|
stack.push_back(work_item(q->get_expr(), curr.second));
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
for (unsigned i = 0; i < next_consts.size(); i++) {
|
||||||
|
func_decl *c = next_consts.get(i);
|
||||||
|
if (!const2quantifier.contains(c)) {
|
||||||
|
const2quantifier.insert(c, obj_pair_hashtable<expr, expr>());
|
||||||
|
}
|
||||||
|
if (!const2quantifier[c].contains(curr)) {
|
||||||
|
const2quantifier[c].insert(curr);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
stack.push_back(work_item(q->get_expr(), curr.second));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else if (q->is_exists()) {
|
||||||
|
stack.push_back(work_item(q->get_expr(), curr.second));
|
||||||
}
|
}
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
else {
|
|
||||||
stack.push_back(work_item(q->get_expr(), curr.second));
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
else if (q->is_exists()) {
|
// ok, now we just need to find the connected component of the last term
|
||||||
stack.push_back(work_item(q->get_expr(), curr.second));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
// ok, now we just need to find the connected component of the last term
|
|
||||||
|
|
||||||
obj_hashtable<expr> visited;
|
obj_hashtable<expr> visited;
|
||||||
ptr_vector<expr> to_visit;
|
ptr_vector<expr> to_visit;
|
||||||
to_visit.push_back(g->form(g->size() - 1));
|
to_visit.push_back(g->form(g->size() - 1));
|
||||||
expr *visiting;
|
expr *visiting;
|
||||||
while (!to_visit.empty()) {
|
while (!to_visit.empty()) {
|
||||||
visiting = to_visit.back();
|
visiting = to_visit.back();
|
||||||
to_visit.pop_back();
|
to_visit.pop_back();
|
||||||
visited.insert(visiting);
|
visited.insert(visiting);
|
||||||
for (obj_hashtable<func_decl>::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) {
|
for (obj_hashtable<func_decl>::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) {
|
||||||
for (obj_hashtable<expr>::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) {
|
for (obj_hashtable<expr>::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) {
|
||||||
if (!visited.contains(*exprit)) {
|
if (!visited.contains(*exprit)) {
|
||||||
to_visit.push_back(*exprit);
|
to_visit.push_back(*exprit);
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
for (int i = 0; i < g->size(); i++) {
|
||||||
|
if (visited.contains(g->form(i))) {
|
||||||
|
new_exprs.push_back(g->form(i));
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
|
||||||
}
|
}
|
||||||
for (int i = 0; i < g->size(); i++) {
|
|
||||||
if (visited.contains(g->form(i))) {
|
|
||||||
new_exprs.push_back(g->form(i));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
};
|
||||||
|
|
||||||
tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) {
|
tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) {
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue