mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fixed some bugs with quantifiers in rule bodies

Browse source
This commit is contained in:
Ken McMillan 2013-06-17 18:04:23 -07:00
parent a78564145b
commit 64acd9cac0
3 changed files with 38 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/duality/duality_rpfp.cpp
View file

@ -217,8 +217,12 @@ namespace Duality {
}
else if (t.is_quantifier())
{
std::vector<expr> pats;
t.get_patterns(pats);
for(unsigned i = 0; i < pats.size(); i++)
pats[i] = LocalizeRec(e,memo,pats[i]);
Term body = LocalizeRec(e,memo,t.body());
res = CloneQuantifier(t,body);
res = clone_quantifier(t, body, pats);
}
else res = t;
return res;
@ -1853,7 +1857,11 @@ namespace Duality {
}
else if (t.is_quantifier()){
int bound = t.get_quantifier_num_bound();
res = CloneQuantifier(t,SubstBoundRec(memo, subst, level + bound, t.body()));
std::vector<expr> pats;
t.get_patterns(pats);
for(unsigned i = 0; i < pats.size(); i++)
pats[i] = SubstBoundRec(memo, subst, level + bound, pats[i]);
res = clone_quantifier(t, SubstBoundRec(memo, subst, level + bound, t.body()), pats);
}
else if (t.is_var()) {
int idx = t.get_index_value();

24
src/duality/duality_wrapper.cpp
View file

@ -326,6 +326,26 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
}
expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns){
quantifier *thing = to_quantifier(q.raw());
bool is_forall = thing->is_forall();
unsigned num_patterns = patterns.size();
std::vector< ::expr *> _patterns(num_patterns);
for(unsigned i = 0; i < num_patterns; i++)
_patterns[i] = to_expr(patterns[i].raw());
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw())));
}
void expr::get_patterns(std::vector<expr> &pats) const {
quantifier *thing = to_quantifier(raw());
unsigned num_patterns = thing->get_num_patterns();
:: expr * const *it = thing->get_patterns();
pats.resize(num_patterns);
for(unsigned i = 0; i < num_patterns; i++)
pats[i] = expr(ctx(),it[i]);
}
func_decl context::fresh_func_decl(char const * prefix, const std::vector<sort> &domain, sort const & range){
std::vector < ::sort * > _domain(domain.size());
for(unsigned i = 0; i < domain.size(); i++)
@ -547,6 +567,10 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
a.show();
}
void show_ast(::ast *a, ast_manager &m) {
std::cout << mk_pp(a, m) << std::endl;
}
bool expr::is_label (bool &pos,std::vector<symbol> &names) const {
buffer< ::symbol> _names;
bool res = m().is_label(to_expr(raw()),pos,_names);

4
src/duality/duality_wrapper.h
View file

@ -556,11 +556,15 @@ namespace Duality {
friend expr clone_quantifier(const expr &, const expr &);
friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
friend std::ostream & operator<<(std::ostream & out, expr const & m){
m.ctx().print_expr(out,m);
return out;
}
void get_patterns(std::vector<expr> &pats) const ;
unsigned get_quantifier_num_bound() const {
return to_quantifier(raw())->get_num_decls();
}