add quasi macro detection

src/ast/simplifiers/eliminate_predicates.cpp

@@ -115,6 +115,8 @@ bool eliminate_predicates::can_be_macro_head(expr* _head, unsigned num_bound) {
         return false;
     if (f->is_associative())
         return false;
+    if (!is_uninterp(f))
+        return false;
     uint_set indices;
     for (expr* arg : *head) {
         if (!is_var(arg))
@@ -146,8 +148,14 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bou
         return false;
     if (f->is_associative())
         return false;
+    if (!is_uninterp(f))
+        return false;
     uint_set indices;
     for (expr* arg : *head) {
+        if (occurs(f, arg))
+            return false;
+        if (!is_macro_safe(arg))
+            return false;
         if (!is_var(arg))
             continue;
         unsigned idx = to_var(arg)->get_idx();
@@ -161,6 +169,49 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bou
 }
 
 
+//
+// (= (f x y (+ x y)) s), where x y are all bound variables.    
+// then replace (f x y z) by (if (= z (+ x y)) s (f' x y z))
+//
+
+void eliminate_predicates::insert_quasi_macro(app* head, expr* body, clause const& cl) {
+    expr_ref _body(body, m);
+    uint_set indices;
+    expr_ref_vector args(m), eqs(m);
+    var_ref new_var(m);
+    app_ref lhs(m), rhs(m);
+    func_decl_ref f1(m);
+    sort_ref_vector sorts(m);
+    svector<symbol> names;
+
+    unsigned num_decls = cl.m_bound.size();
+    func_decl* f = head->get_decl();
+    
+    for (expr* arg : *head) {
+        sorts.push_back(arg->get_sort());
+        names.push_back(symbol(std::string("x") + std::to_string(args.size())));
+        if (is_var(arg)) {
+            unsigned idx = to_var(arg)->get_idx();
+            if (!indices.contains(idx)) {
+                indices.insert(idx);
+                args.push_back(arg);
+                continue;
+            }
+        }
+        new_var = m.mk_var(eqs.size() + num_decls, arg->get_sort());
+        args.push_back(new_var);
+        eqs.push_back(m.mk_eq(arg, new_var));
+    }    
+    
+    // forall vars . f(args) = if eqs then body else f'(args)
+    f1 = m.mk_fresh_func_decl(f->get_name(), symbol::null, sorts.size(), sorts.data(), f->get_range());
+    lhs = m.mk_app(f, args);
+    rhs = m.mk_ite(mk_and(eqs), body, m.mk_app(f1, args));
+    insert_macro(lhs, rhs, cl.m_dep);
+}
+
+
+
 expr_ref eliminate_predicates::bind_free_variables_in_def(clause& cl, app* head, expr* def) {
     unsigned num_bound = cl.m_bound.size();
     if (head->get_num_args() == num_bound)
@@ -208,7 +259,7 @@ bool eliminate_predicates::try_find_binary_definition(func_decl* p, app_ref& hea
     };
 
     for (auto* cl : m_use_list.get(p, false)) {
-        if (cl->m_alive && cl->m_literals.size() == 2) {
+        if (cl->m_alive && cl->size() == 2) {
             auto const& [atom1, sign1] = cl->m_literals[0];
             auto const& [atom2, sign2] = cl->m_literals[1];
             add_def(*cl, atom1, sign1, atom2, sign2);
@@ -242,7 +293,7 @@ bool eliminate_predicates::try_find_binary_definition(func_decl* p, app_ref& hea
     };
 
     for (auto* cl : m_use_list.get(p, true)) {
-        if (cl->m_alive && cl->m_literals.size() == 2) {
+        if (cl->m_alive && cl->size() == 2) {
             if (is_def(0, 1, *cl))
                 return true;
             if (is_def(1, 0, *cl))
@@ -507,10 +558,45 @@ void eliminate_predicates::try_find_macro(clause& cl) {
     //
     
     //
-    // To review: quasi-macros
+    // quasi-macros
     // (= (f x y (+ x y)) s), where x y are all bound variables.    
-    // then replace (f x y z) by (if (= z (+ x y)) s (f' x y))
+    // then replace (f x y z) by (if (= z (+ x y)) s (f' x y z))
     //
+    auto can_be_qdef = [&](expr* _x, expr* y) {
+        if (!is_app(_x))
+            return false;
+        app* x = to_app(_x);
+        return 
+        can_be_quasi_macro_head(x, cl.m_bound.size()) && 
+        is_macro_safe(y) &&
+        !occurs(x->get_decl(), y);
+    };
+
+    if (cl.is_unit() && m.is_eq(cl.atom(0), x, y)) {
+        if (!cl.sign(0) && can_be_qdef(x, y)) {
+            insert_quasi_macro(to_app(x), y, cl);
+            return;
+        }
+        else if (!cl.sign(0) && can_be_qdef(y, x)) {
+            insert_quasi_macro(to_app(y), x, cl);        
+            return;
+        }
+        else if (cl.sign(0) && m.is_bool(y) && can_be_qdef(x, y)) {
+            insert_quasi_macro(to_app(x), m.mk_not(y), cl);
+            return;
+        }
+        else if (cl.sign(0) && m.is_bool(y) && can_be_qdef(y, x)) {
+            insert_quasi_macro(to_app(y), m.mk_not(x), cl);
+            return;
+        }
+    }
+    if (cl.is_unit()) {
+        expr* body = cl.sign(0) ? m.mk_false() : m.mk_true();
+        if (can_be_qdef(cl.atom(0), body)) {
+            insert_quasi_macro(to_app(x), body, cl);
+            return;            
+        }
+    }
 }
 
 
@@ -791,6 +877,11 @@ eliminate_predicates::clause* eliminate_predicates::init_clause(expr* f, expr_de
         bool sign = m.is_not(lit, lit);
         cl->m_literals.push_back({ expr_ref(lit, m), sign });
     }       
+
+    // extend macro detection to exploit bijective functions?
+    // f(+ x 1) = g(x) -> f(x) = g(- x 1)
+    // init_injective(*cl);
+    // init_surjective(*cl);
     return cl;
 }
 
@@ -811,6 +902,73 @@ void eliminate_predicates::init_clauses() {
     process_to_exclude(m_disable_elimination);
 }
 
+/**
+ * Ad hoc recognize surjectivity axioms
+ * - exists y . f(y) = x
+ */
+void eliminate_predicates::init_surjective(clause const& cl) {
+    if (!cl.is_unit())
+        return;
+    if (cl.sign(0))
+        return;
+    if (!is_exists(cl.atom(0)))
+        return;
+}
+
+/**
+ * Ad hoc recognize injectivity axioms
+ * - f(x) = f(y) => x = y
+ */
+void eliminate_predicates::init_injective(clause const& cl) {
+    if (cl.size() != 2)
+        return;
+    if (cl.m_bound.size() != 2)
+        return;
+    if (cl.sign(0) == cl.sign(1))
+        return;
+    expr* a = cl.atom(0), *b = cl.atom(1);
+    if (!cl.sign(0) && cl.sign(1))
+        std::swap(a, b);
+    expr* x, *y, *fx, *fy;
+    if (!m.is_eq(a, fx, fy))
+        return;
+    if (!m.is_eq(b, x, y))
+        return;
+    
+    auto is_fx = [&](expr* _fx, func_decl*& f, unsigned& idx) {
+        if (!is_app(_fx))
+            return false;
+        app* fx = to_app(_fx);
+        if (fx->get_num_args() != 1)
+            return false;
+        if (!is_var(fx->get_arg(0)))
+            return false;
+        f = fx->get_decl();
+        idx = to_var(fx->get_arg(0))->get_idx();
+        return true;
+    };
+    func_decl* f1, *f2;
+    unsigned idx1, idx2;
+    if (!is_fx(fx, f1, idx1))
+        return;
+    if (!is_fx(fy, f2, idx2))
+        return;
+    if (idx1 == idx2 || f1 != f2)
+        return;
+
+    auto check_var = [&](expr* x, unsigned& idx) {
+        if (!is_var(x))
+            return false;
+        idx = to_var(x)->get_idx();
+        return true;
+    };
+    if (!check_var(x, idx1) || !check_var(y, idx2))
+        return;
+    if (idx1 == idx2)
+        return;
+    m_is_injective.mark(f1, true);
+}
+
 /**
 * Convert clauses to m_fmls
 */
@@ -838,6 +996,8 @@ void eliminate_predicates::reset() {
     m_to_exclude.reset();
     m_disable_elimination.reset();
     m_is_macro.reset();
+    m_is_injective.reset();
+    m_is_surjective.reset();
     for (auto const& [k, v] : m_macros)
         dealloc(v);
     m_macros.reset();

src/ast/simplifiers/eliminate_predicates.h

@@ -55,6 +55,7 @@ public:
 
         std::ostream& display(std::ostream& out) const;
 
+        unsigned size() const { return m_literals.size(); }
         expr* atom(unsigned i) const { return m_literals[i].first; }
         bool sign(unsigned i) const { return m_literals[i].second; }
         bool is_unit() const { return m_literals.size() == 1; }
@@ -91,6 +92,7 @@ private:
     ast_mark              m_disable_elimination, m_predicate_decls, m_is_macro;
     ptr_vector<func_decl> m_predicates;
     ptr_vector<expr>      m_to_exclude;
+    ast_mark              m_is_injective, m_is_surjective;
     stats                 m_stats;
     use_list              m_use_list;
     der_rewriter          m_der;
@@ -101,6 +103,8 @@ private:
 
     clause* init_clause(unsigned i);
     clause* init_clause(expr* f, expr_dependency* d, unsigned i);
+    void init_injective(clause const& cl);
+    void init_surjective(clause const& cl);
     clause* resolve(func_decl* p, clause& pos, clause& neg);
     void add_use_list(clause& cl);
 
@@ -109,6 +113,7 @@ private:
     void insert_macro(app* head, expr* def, expr_dependency* dep);
     expr_ref bind_free_variables_in_def(clause& cl, app* head, expr* def);
     bool can_be_macro_head(expr* head, unsigned num_bound);
+    void insert_quasi_macro(app* head, expr* body, clause const& cl);
     bool can_be_quasi_macro_head(expr* head, unsigned num_bound);
     bool is_macro_safe(expr* e);
     void try_find_macro(clause& cl);

src/tactic/arith/degree_shift_tactic.h

@@ -28,7 +28,7 @@ Then, replace $x^n$ with a new fresh variable $y$.
 ```z3
 (declare-const x Real)
 (declare-const y Real)
-(assert (> (+ (* x x x 4) (* x x 3) 0)))
+(assert (> (+ (* x x x 4) (* x x 3)) 0))
 (assert (= (* x x) (* y y)))
 (apply degree-shift)
 ```