From 9a061d8f4aa36c190858263e2cb91c8a3e3413e8 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Sun, 12 Mar 2023 15:59:44 +0100
Subject: [PATCH] find_op

---
 src/math/polysat/constraint_manager.cpp | 22 ++++++++++++++++++++--
 src/math/polysat/constraint_manager.h   |  6 +++++-
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index dc42ca96e..0afaf4cd9 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -417,6 +417,20 @@ namespace polysat {
         return -p - 1;
     }
 
+    signed_constraint constraint_manager::find_op(op_constraint::code op, pdd const& p, pdd const& q) const {
+        auto& m = p.manager();
+        unsigned sz = m.power_of_2();
+
+        op_constraint_args const args(op, p, q);
+        auto it = m_dedup.op_constraint_expr.find_iterator(args);
+        if (it == m_dedup.op_constraint_expr.end())
+            return {};
+        pdd r = m.mk_var(it->m_value);
+
+        op_constraint tmp(op, p, q, r);  // TODO: this still allocates op_constraint::m_vars
+        return { dedup_find(&tmp), true };
+    }
+
     pdd constraint_manager::mk_op_term(op_constraint::code op, pdd const& p, pdd const& q) {
         auto& m = p.manager();
         unsigned sz = m.power_of_2();
@@ -516,14 +530,18 @@ namespace polysat {
     pdd constraint_manager::bxnor(pdd const& p, pdd const& q) {
         return bnot(bxor(p, q));
     }
-    
+
     pdd constraint_manager::pseudo_inv(pdd const& p) {
         auto& m = p.manager();
         if (p.is_val())
             return m.mk_val(p.val().pseudo_inverse(m.power_of_2()));
         return mk_op_term(op_constraint::code::inv_op, p, m.zero());
     }
-    
+
+    signed_constraint constraint_manager::find_op_pseudo_inv(pdd const& p) const {
+        return find_op(op_constraint::code::inv_op, p, p.manager().zero());
+    }
+
     pdd constraint_manager::udiv(pdd const& p, pdd const& q) {
         return div_rem_op_constraint(p, q).first;
     }
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 5f78fec85..9c85f54df 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -107,7 +107,11 @@ namespace polysat {
 
         /** Find constraint p == 0; returns null if it doesn't exist yet */
         signed_constraint find_eq(pdd const& p) const;
-        signed_constraint find_ule(pdd const& a, pdd const& b) const;
+        /** Find constraint p <= q; returns null if it doesn't exist yet */
+        signed_constraint find_ule(pdd const& p, pdd const& q) const;
+        /** Find op_constraint; returns null if it doesn't exist yet */
+        signed_constraint find_op(op_constraint::code op, pdd const& p, pdd const& q) const;
+        signed_constraint find_op_pseudo_inv(pdd const& p) const;
 
         signed_constraint eq(pdd const& p);
         signed_constraint ule(pdd const& a, pdd const& b);