new files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/func_decl_replace.cpp

@@ -0,0 +1,96 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    func_decl_replace.cpp
+
+Abstract:
+
+    Replace functions in expressions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-03-28
+
+Revision History:
+
+
+--*/
+
+
+#include "ast/rewriter/func_decl_replace.h"
+
+expr_ref func_decl_replace::operator()(expr* e) {
+    m_todo.push_back(e);
+    
+    while (!m_todo.empty()) {
+        expr* a = m_todo.back(), *b;
+        if (m_cache.contains(a)) {
+            m_todo.pop_back();
+        }
+        else if (is_var(a)) {
+            m_cache.insert(a, a);
+            m_todo.pop_back();
+        }
+        else if (is_app(a)) {
+            app* c = to_app(a);
+            unsigned n = c->get_num_args();
+            m_args.reset();            
+            bool arg_differs = false;
+            for (unsigned i = 0; i < n; ++i) {
+                expr* d = nullptr, *arg = c->get_arg(i);
+                if (m_cache.find(arg, d)) {
+                    m_args.push_back(d);
+                    arg_differs |= arg != d;
+                    SASSERT(m.get_sort(arg) == m.get_sort(d));
+                }
+                else {
+                    m_todo.push_back(arg);
+                }
+            }
+            if (m_args.size() == n) {
+                if (arg_differs) {
+                    b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
+                    m_refs.push_back(b);
+                    SASSERT(m.get_sort(a) == m.get_sort(b));
+                } else {
+                    b = a;
+                }
+                func_decl* f = nullptr;
+                if (m_subst.find(c->get_decl(), f)) {
+                    b = m.mk_app(f, m_args.size(), m_args.c_ptr());
+                    m_refs.push_back(b);
+                }
+                m_cache.insert(a, b);
+                m_todo.pop_back();
+            }
+        }
+        else {
+            quantifier* q = to_quantifier(a);
+            SASSERT(is_quantifier(a));
+            expr* body = q->get_expr(), *new_body;
+            if (m_cache.find(body, new_body)) {
+                if (new_body == body) {
+                    b = a;
+                }
+                else {
+                    b = m.update_quantifier(q, new_body);
+                    m_refs.push_back(b);
+                }
+                m_cache.insert(a, b);
+                m_todo.pop_back();
+            }
+            else {
+                m_todo.push_back(body);
+            }
+        }        
+    }
+    return expr_ref(cache.find(e), m);
+}
+
+void func_decl_replace::reset() {
+    m_cache.reset();
+    m_subst.reset();
+    m_refs.reset();
+}

src/ast/rewriter/func_decl_replace.h

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    func_decl_replace.h
+
+Abstract:
+
+    Replace functions in expressions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-03-28
+
+Revision History:
+
+
+--*/
+
+#ifndef FUNC_DECL_REPLACE_H_
+#define FUNC_DECL_REPLACE_H_
+
+#include "ast/ast.h"
+
+class func_decl_replace {
+    ast_manager& m;
+    obj_map<func_decl, func_decl*> m_subst;
+    obj_map<expr, expr*> m_cache;
+    ptr_vector<expr> m_todo, m_args;
+    expr_ref_vector m_refs;
+
+public:
+    func_decl_replace(ast_manager& m): m(m), m_refs(m) {}
+
+    void insert(func_decl* src, func_decl* dst) { m_subst.insert(src, dst); }
+
+    expr_ref operator()(expr* e);
+
+    void reset();
+
+    bool empty() const { return m_subst.empty(); }
+};
+
+#endif /* FUNC_DECL_REPLACE_H_ */

src/tactic/core/special_relations_tactic.cpp

@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    special_relations_tactic.cpp
+
+Abstract:
+
+    Detect special relations in an axiomatization, 
+    rewrite goal using special relations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-03-28
+
+Notes:
+
+--*/
+#include "tactic/core/special_relations.h"
+
+void special_relations_tactic::collect_feature(goal const& g, unsigned idx, 
+                                               obj_map<func_decl, sp_axioms>& goal_features) {
+    expr* f = g.form(idx);
+    func_decl_ref p(m);
+    if (is_transitivity(f, p)) {
+        insert(goal_features, p, idx, sr_transitive);
+    }
+}
+
+void specia_relations_tactic::insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* p, unsigned idx, sr_property p) {
+    
+}
+
+
+bool special_relations_tactic::is_transitivity(expr* fml, func_decl_ref& p) {
+    return false;
+}
+bool special_relations_tactic::is_anti_symmetry(expr* fml, func_decl_ref& p) {
+    return false;
+}
+bool special_relations_tactic::is_left_tree(expr* fml, func_decl_ref& p) {
+    return false;
+}
+bool special_relations_tactic::is_right_tree(expr* fml, func_decl_ref& p) {
+    return false;
+}
+bool special_relations_tactic::is_reflexivity(expr* fml, func_decl_ref& p) {
+    return false;
+}
+bool special_relations_tactic::is_total(expr* fml, func_decl_ref& p) {
+    return false;
+}
+bool special_relations_tactic::is_symmetric(expr* fml, func_decl_ref& p) {
+    return false;
+}
+
+    
+void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) {
+    tactic_report report("special_relations", g);
+    obj_map<func_decl, sp_axioms> goal_features;
+    unsigned size = g.size();
+    for (unsigned idx = 0; idx < size; idx++) {
+        collect_feature(g, idx, goal_features);
+    }
+    if (!goal_features.empty()) {
+        
+    }
+    g->inc_depth();
+    result.push_back(g.get());
+}
+    

src/tactic/core/special_relations_tactic.h

@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    special_relations_tactic.h
+
+Abstract:
+
+    Detect special relations in an axiomatization, 
+    rewrite goal using special relations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-03-28
+
+Notes:
+
+--*/
+#ifndef SPECIAL_RELATIONS_TACTIC_H_
+#define SPECIAL_RELATIONS_TACTIC_H_
+
+#include "tactic/tactic.h"
+#include "tactic/tactical.h"
+
+class special_relations_tactic : public tactic {
+    params_ref m_params;
+    
+    struct sp_axioms {
+        unsigned_vector m_goal_indices;
+        unsigned        m_sp_features;
+    };
+
+    void collect_feature(goal const& g, unsigned idx, obj_map<func_decl, sp_axioms>& goal_features);
+    void insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* p, unsigned idx, sr_property p);
+
+    bool is_transitivity(expr* fml, func_decl_ref& p);
+    bool is_anti_symmetry(expr* fml, func_decl_ref& p);
+    bool is_left_tree(expr* fml, func_decl_ref& p);
+    bool is_right_tree(expr* fml, func_decl_ref& p);
+    bool is_reflexivity(expr* fml, func_decl_ref& p);
+    bool is_total(expr* fml, func_decl_ref& p);
+    bool is_symmetric(expr* fml, func_decl_ref& p);
+
+public:
+
+    special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()) {}
+
+    ~special_relations_tactic() override {}
+
+    void updt_params(params_ref const & p) override { m_params = p; }
+    
+    void collect_param_descrs(param_descrs & r) override { }
+    
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
+    
+    void cleanup() override {}
+
+    tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); }
+
+};
+
+tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+  ADD_TACTIC("special_relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)")
+*/
+
+#endif