From 058c5771b99c06f40e6180986be534118cb00e64 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 22 Aug 2022 15:09:11 +0200
Subject: [PATCH] univariate solver: add_bit

---
 src/math/polysat/univariate/univariate_solver.cpp | 4 ++++
 src/math/polysat/univariate/univariate_solver.h   | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index c5beb5ab2..f17d4a735 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -144,6 +144,10 @@ namespace polysat {
             add(bv->mk_ule(mk_numeral(val), x), sign, dep);
         }
 
+        void add_bit(unsigned idx, bool sign, dep_t dep) override {
+            add(bv->mk_bit2bool(x, idx), sign, dep);
+        }
+
         lbool check() override {
             return s->check_sat();
         }
diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h
index 0a19081ed..65bc9c65a 100644
--- a/src/math/polysat/univariate/univariate_solver.h
+++ b/src/math/polysat/univariate/univariate_solver.h
@@ -63,8 +63,8 @@ namespace polysat {
         void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); }
         void add_ult_const(rational const& val, bool sign, dep_t dep) { add_uge_const(val, !sign, dep); }
 
-        // TODO: assert bit; use bv->mk_bit2bool(x, idx)
-        // virtual void add_bit(unsigned idx, bool sign, dep_t dep);
+        /// Assert i-th bit of x
+        virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0;
 
         virtual std::ostream& display(std::ostream& out) const = 0;
     };