From 4f4cafbc988d60872ec1aa2c64d9a07767d42c6e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Dec 2024 18:17:07 -0800
Subject: [PATCH] start update with expr-inverter to handle PB

---
 src/ast/converters/expr_inverter.cpp | 80 ++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)

diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index 8bb316dfc..bba02b591 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -20,6 +20,7 @@ Author:
 #include "ast/ast_util.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
+#include "ast/pb_decl_plugin.h"
 #include "ast/converters/expr_inverter.h"
 
 class basic_expr_inverter : public iexpr_inverter {
@@ -743,6 +744,84 @@ public:
     }
 };
 
+#if 0
+class pb_expr_inverter : public iexpr_inverter {
+    pb_util pb;
+public:
+    pb_expr_inverter(ast_manager& m) : iexpr_inverter(m), pb(m) {}
+
+    family_id get_fid() const override { return pb.get_family_id(); }
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
+        rational k, c;
+        unsigned new_k = 0;
+        expr_ref_vector new_args(m), uncnstr_args(m);
+        vector<rational> coeffs;
+        switch (f->get_decl_kind()) {
+        case OP_AT_MOST_K:
+            // a' + b' + c  + d <= 3 -> r := c + d <= 1
+            // a' + b' + c  + d <= 1 -> r := c + d <= 1
+            // a' + b' + c' + d <= 2 -> r := fresh        
+            // a', b', c' := ~r
+            k = pb.get_k(f);
+            if (!k.is_unsigned())
+                return false;
+            for (unsigned i = 0; i < num; ++i)
+                if (uncnstr(args[i]))
+                    uncnstr_args.push_back(args[i]);
+                else
+                    new_args.push_back(args[i]);
+            if (uncnstr_args.empty())
+                return false;
+            if (new_args.size() <= k && uncnstr_args.size() > k) 
+                mk_fresh_uncnstr_var_for(f, r);         
+            else if (new_args.size() <= k) // k >= uncnstr_args.size()
+                r = pb.mk_at_most_k(new_args, k.get_unsigned() - uncnstr_args.size());            
+            else // |new_args| > k
+                r = pb.mk_at_most_k(new_args, k.get_unsigned());
+            if (m_mc) {
+                for (unsigned i = 0; i < uncnstr_args.size(); ++i)
+                    add_def(uncnstr_args.get(i), m.mk_not(r));
+            }
+            return true;
+        case OP_AT_LEAST_K:
+            k = pb.get_k(f);
+            if (!k.is_unsigned())
+                return false;
+            for (unsigned i = 0; i < num; ++i)
+                if (uncnstr(args[i]))
+                    uncnstr_args.push_back(args[i]);
+                else
+                    new_args.push_back(args[i]);
+            if (uncnstr_args.empty())
+                return false;
+            // cases k <= uncstr_args.size()
+            // k > uncstr_args.size()
+            return false;
+        case OP_PB_LE:
+            // 2*x + 3*y + z + 2*u <= k -> r
+            // r := z + 2u <= 
+            // 
+            k = pb.get_k(f);
+            for (unsigned i = 0; i < num; ++i)
+                if (uncnstr(args[i]))
+                    uncnstr_args.push_back(args[i]), c += pb.get_coeff(f, i);
+                else
+                    new_args.push_back(args[i]), coeffs.push_back(pb.get_coeff(f, i));
+            if (uncnstr_args.empty())
+                return false;
+            return false;
+        default:
+            return false;
+        }
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+         return false;
+    }
+};
+#endif
+
 
 class seq_expr_inverter : public iexpr_inverter {
     seq_util seq;
@@ -870,6 +949,7 @@ expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
     add(alloc(dt_expr_inverter, m));
     add(alloc(basic_expr_inverter, m, *this));
     add(alloc(seq_expr_inverter, m));
+    //add(alloc(pb_expr_inverter, m));
 }