From d4a28d4553544c0637d58f7e932e2a65bd42f77b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 10 Mar 2022 11:13:06 +0100
Subject: [PATCH] implementation stub

---
 src/math/polysat/univariate_solver.h |  4 ++--
 src/sat/smt/bv_polysat.cpp           | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/univariate_solver.h b/src/math/polysat/univariate_solver.h
index 3d47c46f4..87d1fe94f 100644
--- a/src/math/polysat/univariate_solver.h
+++ b/src/math/polysat/univariate_solver.h
@@ -31,7 +31,7 @@ namespace polysat {
         using dep_vector = svector<dep_t>;
         using univariate = vector<rational>;
 
-        virtual ~univariate_solver();
+        virtual ~univariate_solver() = default;
 
         virtual void push() = 0;
         virtual void pop(unsigned n) = 0;
@@ -49,7 +49,7 @@ namespace polysat {
 
     class univariate_solver_factory {
     public:
-        virtual ~univariate_solver_factory();
+        virtual ~univariate_solver_factory() = default;
         virtual scoped_ptr<univariate_solver> create() = 0;
     };
 
diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp
index 7d05d97ab..405d4e55c 100644
--- a/src/sat/smt/bv_polysat.cpp
+++ b/src/sat/smt/bv_polysat.cpp
@@ -25,9 +25,34 @@ Notes:
 #include "sat/smt/bv_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "math/polysat/solver.h"
+#include "math/polysat/univariate_solver.h"
 
 namespace bv {
 
+    class univariate_bitblast_solver : public polysat::univariate_solver {
+    public:
+        univariate_bitblast_solver() {};
+        ~univariate_bitblast_solver() override = default;
+        void push() override {}
+        void pop(unsigned n) override {}
+        lbool check() override { return l_undef; }
+        dep_vector unsat_core() override { return {}; }
+        rational model() override { return {}; }
+        void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {}
+        void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {}
+        void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {}
+        void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {}
+    };
+
+    class univariate_bitblast_factory : public polysat::univariate_solver_factory {
+    public:
+        ~univariate_bitblast_factory() override = default;
+        scoped_ptr<polysat::univariate_solver> create() override {
+            return alloc(univariate_bitblast_solver);
+        }
+    };
+
+
     typedef polysat::pdd pdd;
 
     void solver::internalize_polysat(app* a) {