mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

Resolved merge conflict

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-04-05 20:31:45 +01:00
parent 932ba15261
commit 287c6f08e1
1 changed files with 79 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

149
src/tactic/sine_filter.cpp
View file

@ -35,25 +35,25 @@ 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) {}
tactic * translate(ast_manager & m) override { virtual tactic * translate(ast_manager & m) {
return alloc(sine_tactic, m, m_params); return alloc(sine_tactic, m, m_params);
} }
void updt_params(params_ref const & p) override { virtual void updt_params(params_ref const & p) {
} }
void collect_param_descrs(param_descrs & r) override { virtual void collect_param_descrs(param_descrs & r) {
} }
void operator()(goal_ref const & g, virtual void operator()(goal_ref const & g,
goal_ref_buffer & result, goal_ref_buffer & result,
model_converter_ref & mc, model_converter_ref & mc,
proof_converter_ref & pc, proof_converter_ref & pc,
expr_dependency_ref & core) override { expr_dependency_ref & core) {
mc = nullptr; pc = nullptr; core = nullptr; mc = 0; pc = 0; core = 0;
TRACE("sine", g->display(tout);); TRACE("sine", g->display(tout););
TRACE("sine", tout << g->size();); TRACE("sine", tout << g->size(););
@ -62,7 +62,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), nullptr, nullptr); 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);
@ -72,115 +72,120 @@ public:
filter_model_converter * fmc = alloc(filter_model_converter, m); filter_model_converter * fmc = alloc(filter_model_converter, m);
mc = fmc; mc = fmc;
} }
void cleanup() override { virtual void cleanup() {
} }
private: private:
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) && is_uninterp(curr)) {
app *a = to_app(curr); app *a = to_app(curr);
if (is_uninterp(a)) { func_decl *f = a->get_decl();
func_decl *f = a->get_decl(); consts.insert_if_not_there(f);
consts.insert_if_not_there(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",
for (obj_hashtable<func_decl>::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { tout << "size of consts is "; tout << consts.size(); tout << "\n";
TRACE("sine", tout << *constit; tout << "\n";); obj_hashtable<func_decl>::iterator it = consts.begin();
} obj_hashtable<func_decl>::iterator end = consts.end();
for (; it != end; it++)
tout << *it << "\n"; );
bool matched = false; bool matched = false;
for (unsigned i = 0; i < q->get_num_patterns(); i++) { for (unsigned i = 0; i < q->get_num_patterns(); i++) {
bool p_matched = true; bool p_matched = true;
ptr_vector<expr> stack; ptr_vector<expr> stack;
expr *curr; expr * curr;
// patterns are wrapped with "pattern" // patterns are wrapped with "pattern"
if (!m.is_pattern(q->get_pattern(i), stack)) { if (!m.is_pattern(q->get_pattern(i), stack))
continue; continue;
}
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 (!consts.contains(f)) { if (!consts.contains(f)) {
TRACE("sine", tout << mk_pp(f, m) << "\n";); TRACE("sine", tout << mk_pp(f, m) << "\n";);
p_matched = false; p_matched = false;
next_consts.push_back(f); next_consts.push_back(f);
break; break;
} }
for (unsigned j = 0; j < a->get_num_args(); j++) { for (unsigned j = 0; j < a->get_num_args(); j++)
stack.push_back(a->get_arg(j)); stack.push_back(a->get_arg(j));
}
} }
} }
if (p_matched) { if (p_matched) {
matched = true; matched = true;
break; 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 (unsigned i = 0; i < g->size(); i++) {
stack.push_back(work_item(g->form(i), g->form(i)));
}
t_work_item curr; t_work_item curr;
for (unsigned i = 0; i < g->size(); i++)
stack.push_back(work_item(g->form(i), g->form(i)));
while (!stack.empty()) { while (!stack.empty()) {
curr = stack.back(); curr = stack.back();
stack.pop_back(); stack.pop_back();
if (is_app(curr.first)) { if (is_app(curr.first) && is_uninterp(curr.first)) {
app *a = to_app(curr.first); app * a = to_app(curr.first);
if (is_uninterp(a)) { func_decl * f = a->get_decl();
func_decl *f = a->get_decl(); if (!consts.contains(f)) {
if (!consts.contains(f)) { consts.insert(f);
consts.insert(f); if (const2quantifier.contains(f)) {
if (const2quantifier.contains(f)) { obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin();
for (obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { obj_pair_hashtable<expr, expr>::iterator end = const2quantifier[f].end();
stack.push_back(*it); for (; it != end; it++)
} stack.push_back(*it);
const2quantifier.remove(f); 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);
} }
} }
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 (unsigned i = 0; i < a->get_num_args(); i++) { for (unsigned i = 0; i < a->get_num_args(); i++) {
stack.push_back(work_item(a->get_arg(i), curr.second)); stack.push_back(work_item(a->get_arg(i), curr.second));
} }
@ -214,28 +219,32 @@ private:
} }
} }
} }
// ok, now we just need to find the connected component of the last term // 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++) { obj_hashtable<func_decl>::iterator it = exp2const[visiting].begin();
for (obj_hashtable<expr>::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { obj_hashtable<func_decl>::iterator end = exp2const[visiting].end();
if (!visited.contains(*exprit)) { for (; it != end; it++) {
obj_hashtable<expr>::iterator exprit = const2exp[*it].begin();
obj_hashtable<expr>::iterator exprend = const2exp[*it].end();
for (; exprit != exprend; exprit++) {
if (!visited.contains(*exprit))
to_visit.push_back(*exprit); to_visit.push_back(*exprit);
}
} }
} }
} }
for (unsigned i = 0; i < g->size(); i++) { for (unsigned i = 0; i < g->size(); i++) {
if (visited.contains(g->form(i))) { if (visited.contains(g->form(i)))
new_exprs.push_back(g->form(i)); new_exprs.push_back(g->form(i));
}
} }
} }
}; };