mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 14:13:23 +00:00
Anti-unification of two ground expressions
This commit is contained in:
Arie Gurfinkel
parent
aa8dac2583
commit
af57db0413
2 changed files with 80 additions and 190 deletions
|
|
@ -103,190 +103,73 @@ struct var_abs_rewriter : public default_rewriter_cfg {
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
/*
|
|
||||||
* construct m_g, which is a generalization of t, where every constant
|
|
||||||
* is replaced by a variable for any variable in m_g, remember the
|
|
||||||
* substitution to get back t and save it in m_substitutions
|
|
||||||
*/
|
|
||||||
anti_unifier::anti_unifier(expr* t, ast_manager& man) : m(man), m_pinned(m), m_g(m)
|
|
||||||
{
|
|
||||||
m_pinned.push_back(t);
|
|
||||||
|
|
||||||
obj_map<expr, expr*> substitution;
|
anti_unifier::anti_unifier(ast_manager &manager) : m(manager), m_pinned(m) {}
|
||||||
|
|
||||||
var_abs_rewriter var_abs_cfg(m, substitution);
|
void anti_unifier::reset() {
|
||||||
rewriter_tpl<var_abs_rewriter> var_abs_rw (m, false, var_abs_cfg);
|
m_subs.reset();
|
||||||
var_abs_rw (t, m_g);
|
m_cache.reset();
|
||||||
|
m_todo.reset();
|
||||||
m_substitutions.push_back(substitution); //TODO: refactor into vector, remove k
|
m_pinned.reset();
|
||||||
}
|
}
|
||||||
|
|
||||||
/* traverses m_g and t in parallel. if they only differ in constants
|
void anti_unifier::operator()(expr *e1, expr *e2, expr_ref &res,
|
||||||
* (i.e. m_g contains a variable, where t contains a constant), then
|
substitution &s1, substitution &s2) {
|
||||||
* add the substitutions, which need to be applied to m_g to get t, to
|
|
||||||
* m_substitutions.
|
|
||||||
*/
|
|
||||||
bool anti_unifier::add_term(expr* t) {
|
|
||||||
m_pinned.push_back(t);
|
|
||||||
|
|
||||||
ptr_vector<expr> todo;
|
reset();
|
||||||
ptr_vector<expr> todo2;
|
if (e1 == e2) {res = e1; s1.reset(); s2.reset(); return;}
|
||||||
todo.push_back(m_g);
|
|
||||||
todo2.push_back(t);
|
|
||||||
|
|
||||||
ast_mark visited;
|
m_todo.push_back(expr_pair(e1, e2));
|
||||||
|
while (!m_todo.empty()) {
|
||||||
|
const expr_pair &p = m_todo.back();
|
||||||
|
SASSERT(is_app(p.first));
|
||||||
|
SASSERT(is_app(p.second));
|
||||||
|
|
||||||
arith_util util(m);
|
app * n1 = to_app(p.first);
|
||||||
|
app * n2 = to_app(p.second);
|
||||||
|
|
||||||
obj_map<expr, expr*> substitution;
|
unsigned num_arg1 = n1->get_num_args();
|
||||||
|
unsigned num_arg2 = n2->get_num_args();
|
||||||
while (!todo.empty()) {
|
if (n1->get_decl() != n2->get_decl() || num_arg1 != num_arg2) {
|
||||||
expr* current = todo.back();
|
expr_ref v(m);
|
||||||
todo.pop_back();
|
v = m.mk_var(m_subs.size(), get_sort(n1));
|
||||||
expr* current2 = todo2.back();
|
m_pinned.push_back(v);
|
||||||
todo2.pop_back();
|
m_subs.push_back(expr_pair(n1, n2));
|
||||||
|
m_cache.insert(n1, n2, v);
|
||||||
if (!visited.is_marked(current)) {
|
|
||||||
visited.mark(current, true);
|
|
||||||
|
|
||||||
if (is_var(current)) {
|
|
||||||
// TODO: for now we don't allow variables in the terms we want to antiunify
|
|
||||||
SASSERT(m_substitutions[0].contains(current));
|
|
||||||
if (util.is_numeral(current2)) {
|
|
||||||
substitution.insert(current, current2);
|
|
||||||
}
|
|
||||||
else {return false;}
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
SASSERT(is_app(current));
|
|
||||||
|
|
||||||
if (is_app(current2) &&
|
|
||||||
to_app(current)->get_decl() == to_app(current2)->get_decl() &&
|
|
||||||
to_app(current)->get_num_args() == to_app(current2)->get_num_args()) {
|
|
||||||
// TODO: what to do for numerals here? E.g. if we
|
|
||||||
// have 1 and 2, do they have the same decl or are
|
|
||||||
// the decls already different?
|
|
||||||
SASSERT (!util.is_numeral(current) || current == current2);
|
|
||||||
for (unsigned i = 0, num_args = to_app(current)->get_num_args();
|
|
||||||
i < num_args; ++i) {
|
|
||||||
todo.push_back(to_app(current)->get_arg(i));
|
|
||||||
todo2.push_back(to_app(current2)->get_arg(i));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// we now know that the terms can be anti-unified, so add the cached substitution
|
|
||||||
m_substitutions.push_back(substitution);
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
/*
|
|
||||||
* returns m_g, where additionally any variable, which has only equal
|
|
||||||
* substitutions, is substituted with that substitution
|
|
||||||
*/
|
|
||||||
void anti_unifier::finalize() {
|
|
||||||
ptr_vector<expr> todo;
|
|
||||||
todo.push_back(m_g);
|
|
||||||
|
|
||||||
ast_mark visited;
|
|
||||||
|
|
||||||
obj_map<expr, expr*> generalization;
|
|
||||||
|
|
||||||
arith_util util(m);
|
|
||||||
|
|
||||||
// post-order traversel which ignores constants and handles them
|
|
||||||
// directly when the enclosing term of the constant is handled
|
|
||||||
while (!todo.empty()) {
|
|
||||||
expr* current = todo.back();
|
|
||||||
SASSERT(is_app(current));
|
|
||||||
|
|
||||||
// if we haven't already visited current
|
|
||||||
if (!visited.is_marked(current)) {
|
|
||||||
bool existsUnvisitedParent = false;
|
|
||||||
|
|
||||||
for (unsigned i = 0, sz = to_app(current)->get_num_args(); i < sz; ++i) {
|
|
||||||
expr* argument = to_app(current)->get_arg(i);
|
|
||||||
|
|
||||||
if (!is_var(argument)) {
|
|
||||||
SASSERT(is_app(argument));
|
|
||||||
// if we haven't visited the current parent yet
|
|
||||||
if(!visited.is_marked(argument)) {
|
|
||||||
// add it to the stack
|
|
||||||
todo.push_back(argument);
|
|
||||||
existsUnvisitedParent = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// if we already visited all parents, we can visit current too
|
|
||||||
if (!existsUnvisitedParent) {
|
|
||||||
visited.mark(current, true);
|
|
||||||
todo.pop_back();
|
|
||||||
|
|
||||||
ptr_buffer<expr> arg_list;
|
|
||||||
for (unsigned i = 0, num_args = to_app(current)->get_num_args();
|
|
||||||
i < num_args; ++i) {
|
|
||||||
expr* argument = to_app(current)->get_arg(i);
|
|
||||||
|
|
||||||
if (is_var(argument)) {
|
|
||||||
// compute whether there are different
|
|
||||||
// substitutions for argument
|
|
||||||
bool containsDifferentSubstitutions = false;
|
|
||||||
|
|
||||||
for (unsigned i=0, sz = m_substitutions.size(); i+1 < sz; ++i) {
|
|
||||||
SASSERT(m_substitutions[i].contains(argument));
|
|
||||||
SASSERT(m_substitutions[i+1].contains(argument));
|
|
||||||
|
|
||||||
// TODO: how to check equality?
|
|
||||||
if (m_substitutions[i][argument] !=
|
|
||||||
m_substitutions[i+1][argument])
|
|
||||||
{
|
|
||||||
containsDifferentSubstitutions = true;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// if yes, use the variable
|
|
||||||
if (containsDifferentSubstitutions) {
|
|
||||||
arg_list.push_back(argument);
|
|
||||||
}
|
|
||||||
// otherwise use the concrete value instead
|
|
||||||
// and remove the substitutions
|
|
||||||
else
|
|
||||||
{
|
|
||||||
arg_list.push_back(m_substitutions[0][argument]);
|
|
||||||
|
|
||||||
for (unsigned i=0, sz = m_substitutions.size(); i < sz; ++i) {
|
|
||||||
SASSERT(m_substitutions[i].contains(argument));
|
|
||||||
m_substitutions[i].remove(argument);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
SASSERT(generalization.contains(argument));
|
|
||||||
arg_list.push_back(generalization[argument]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
SASSERT(to_app(current)->get_num_args() == arg_list.size());
|
|
||||||
expr_ref application(m.mk_app(to_app(current)->get_decl(),
|
|
||||||
to_app(current)->get_num_args(),
|
|
||||||
arg_list.c_ptr()), m);
|
|
||||||
m_pinned.push_back(application);
|
|
||||||
generalization.insert(current, application);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
todo.pop_back();
|
expr *tmp;
|
||||||
|
unsigned todo_sz = m_todo.size();
|
||||||
|
ptr_buffer<expr> kids;
|
||||||
|
for (unsigned i = 0; i < num_arg1; ++i) {
|
||||||
|
expr *arg1 = n1->get_arg(i);
|
||||||
|
expr *arg2 = n2->get_arg(i);
|
||||||
|
if (arg1 == arg2) {kids.push_back(arg1);}
|
||||||
|
else if (m_cache.find(arg1, arg2, tmp)) {kids.push_back(tmp);}
|
||||||
|
else {m_todo.push_back(expr_pair(arg1, arg2));}
|
||||||
|
}
|
||||||
|
if (m_todo.size() > todo_sz) {continue;}
|
||||||
|
|
||||||
|
expr_ref u(m);
|
||||||
|
u = m.mk_app(n1->get_decl(), kids.size(), kids.c_ptr());
|
||||||
|
m_pinned.push_back(u);
|
||||||
|
m_cache.insert(n1, n2, u);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
m_g = generalization[m_g];
|
expr *r;
|
||||||
|
VERIFY(m_cache.find(e1, e2, r));
|
||||||
|
res = r;
|
||||||
|
|
||||||
|
// create substitutions
|
||||||
|
s1.reserve(2, m_subs.size());
|
||||||
|
s2.reserve(2, m_subs.size());
|
||||||
|
|
||||||
|
for (unsigned i = 0, sz = m_subs.size(); i < sz; ++i) {
|
||||||
|
expr_pair p = m_subs.get(i);
|
||||||
|
s1.insert(i, 0, expr_offset(p.first, 1));
|
||||||
|
s2.insert(i, 0, expr_offset(p.second, 1));
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -319,6 +202,8 @@ public:
|
||||||
*/
|
*/
|
||||||
bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
|
bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
|
||||||
expr_ref& result) {
|
expr_ref& result) {
|
||||||
|
NOT_IMPLEMENTED_YET();
|
||||||
|
#if 0
|
||||||
arith_util util(m);
|
arith_util util(m);
|
||||||
|
|
||||||
SASSERT(au.get_num_substitutions() > 0);
|
SASSERT(au.get_num_substitutions() > 0);
|
||||||
|
|
@ -412,6 +297,7 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
|
||||||
result = expr_ref(m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), body),m);
|
result = expr_ref(m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), body),m);
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
bool naive_convex_closure::get_range(vector<unsigned int>& v,
|
bool naive_convex_closure::get_range(vector<unsigned int>& v,
|
||||||
|
|
|
||||||
|
|
@ -22,32 +22,36 @@ Revision History:
|
||||||
#define _SPACER_ANTIUNIFY_H_
|
#define _SPACER_ANTIUNIFY_H_
|
||||||
|
|
||||||
#include "ast/ast.h"
|
#include "ast/ast.h"
|
||||||
|
#include "ast/substitution/substitution.h"
|
||||||
|
#include "util/obj_pair_hashtable.h"
|
||||||
namespace spacer {
|
namespace spacer {
|
||||||
|
/**
|
||||||
|
\brief Anti-unifier for ground expressions
|
||||||
|
*/
|
||||||
class anti_unifier
|
class anti_unifier
|
||||||
{
|
{
|
||||||
public:
|
typedef std::pair<expr *, expr *> expr_pair;
|
||||||
anti_unifier(expr* t, ast_manager& m);
|
typedef pair_hash<obj_ptr_hash<expr>, obj_ptr_hash<expr> > expr_pair_hash;
|
||||||
~anti_unifier() {}
|
typedef obj_pair_map<expr, expr, expr*> cache_ty;
|
||||||
|
|
||||||
bool add_term(expr* t);
|
ast_manager &m;
|
||||||
void finalize();
|
|
||||||
|
|
||||||
expr* get_generalization() {return m_g;}
|
|
||||||
unsigned get_num_substitutions() {return m_substitutions.size();}
|
|
||||||
obj_map<expr, expr*> get_substitution(unsigned index){
|
|
||||||
SASSERT(index < m_substitutions.size());
|
|
||||||
return m_substitutions[index];
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
ast_manager& m;
|
|
||||||
// tracking all created expressions
|
|
||||||
expr_ref_vector m_pinned;
|
expr_ref_vector m_pinned;
|
||||||
|
|
||||||
expr_ref m_g;
|
svector<expr_pair> m_todo;
|
||||||
|
cache_ty m_cache;
|
||||||
|
svector<expr_pair> m_subs;
|
||||||
|
|
||||||
vector<obj_map<expr, expr*>> m_substitutions;
|
public:
|
||||||
|
anti_unifier(ast_manager& m);
|
||||||
|
|
||||||
|
void reset();
|
||||||
|
|
||||||
|
/**
|
||||||
|
\brief Computes anti-unifier of two ground expressions. Returns
|
||||||
|
the anti-unifier and the corresponding substitutions
|
||||||
|
*/
|
||||||
|
void operator() (expr *e1, expr *e2, expr_ref &res,
|
||||||
|
substitution &s1, substitution &s2);
|
||||||
};
|
};
|
||||||
|
|
||||||
class naive_convex_closure
|
class naive_convex_closure
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue