move into separate component

src/CMakeLists.txt

@@ -42,6 +42,7 @@ add_subdirectory(math/simplex)
 add_subdirectory(math/interval)
 add_subdirectory(math/bigfix)
 add_subdirectory(math/polysat)
+add_subdirectory(math/polysat/univariate)
 add_subdirectory(math/automata)
 add_subdirectory(math/realclosure)
 add_subdirectory(math/subpaving)

src/math/polysat/solver.h

@@ -35,7 +35,6 @@ Author:
 #include "math/polysat/trail.h"
 #include "math/polysat/viable.h"
 #include "math/polysat/log.h"
-#include "math/polysat/univariate_solver.h"
 
 
 

src/math/polysat/univariate/CMakeLists.txt

@@ -0,0 +1,4 @@
+z3_add_component(polysat_univariate_solver
+  SOURCES
+    univariate_solver.cpp
+)

src/math/polysat/univariate/univariate_solver.cpp

@@ -0,0 +1,90 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    polysat univariate solver
+
+Abstract:
+
+    Solve univariate constraints for polysat using bitblasting
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-03-10
+    Jakob Rath 2022-03-10
+
+--*/
+
+#include "math/polysat/univariate/univariate_solver.h"
+#include "solver/solver.h"
+#include "util/util.h"
+
+
+namespace polysat {
+
+    class univariate_bitblast_solver : public univariate_solver {
+        ast_manager m;
+        scoped_ptr<solver> s;
+
+    public:
+        univariate_bitblast_solver() {
+            NOT_IMPLEMENTED_YET();
+            // which concrete solver do we want here?
+            // need to set params to enable model and unsat core generation; and bit blasting?
+            s = mk_smt2_solver(m, params_ref::get_empty());
+        }
+
+        ~univariate_bitblast_solver() override = default;
+
+        void push() override {
+            s->push();
+        }
+
+        void pop(unsigned n) override {
+            s->pop(n);
+        }
+
+        void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
+            // s->assert_expr();
+            NOT_IMPLEMENTED_YET();
+        }
+
+        void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
+            NOT_IMPLEMENTED_YET();
+        }
+
+        void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
+            NOT_IMPLEMENTED_YET();
+        }
+
+        void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
+            NOT_IMPLEMENTED_YET();
+        }
+
+        lbool check() override {
+            // TODO: need to pass assumptions to get an unsat core?
+            return s->check_sat();
+        }
+
+        dep_vector unsat_core() override {
+            SASSERT(s->status() == l_false);
+            expr_ref_vector core(m);
+            s->get_unsat_core(core);
+            NOT_IMPLEMENTED_YET();
+            return {};
+        }
+
+        rational model() override {
+            SASSERT(s->status() == l_true);
+            model_ref model;
+            s->get_model(model);
+            NOT_IMPLEMENTED_YET();
+            return {};
+        }
+    };
+
+    scoped_ptr<univariate_solver> mk_univariate_bitblast_solver() {
+        return alloc(univariate_bitblast_solver);
+    }
+}

src/math/polysat/univariate/univariate_solver.h

@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2021 Microsoft Corporation
+Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
@@ -47,10 +47,6 @@ namespace polysat {
         // op constraints?
     };
 
-    class univariate_solver_factory {
-    public:
-        virtual ~univariate_solver_factory() = default;
-        virtual scoped_ptr<univariate_solver> create() = 0;
-    };
+    scoped_ptr<univariate_solver> mk_univariate_bitblast_solver();
 
 }

src/math/polysat/viable.h

@@ -23,7 +23,7 @@ Author:
 #include "math/polysat/types.h"
 #include "math/polysat/conflict.h"
 #include "math/polysat/constraint.h"
-#include "math/polysat/univariate_solver.h"
+#include "math/polysat/univariate/univariate_solver.h"
 
 namespace polysat {
 
@@ -33,7 +33,6 @@ namespace polysat {
         friend class test_fi;
 
         solver& s;
-        scoped_ptr<univariate_solver_factory> m_univariate_solver_factory;
         
         struct entry : public dll_base<entry>, public fi_record { 
             entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {}

src/sat/smt/bv_polysat.cpp

@@ -25,34 +25,9 @@ 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) {