Univariate solver interface

src/math/polysat/solver.h

@@ -35,6 +35,7 @@ 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_solver.h

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat abstract univariate solver
+
+Abstract:
+
+    Solver interface for univariate polynomials over modular arithmetic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-03-10
+    Jakob Rath 2022-03-10
+
+--*/
+#pragma once
+
+#include "util/lbool.h"
+#include "util/rational.h"
+#include "util/vector.h"
+#include "util/util.h"
+
+
+namespace polysat {
+
+    class univariate_solver {
+    public:
+        using dep_t = unsigned;
+        using dep_vector = svector<dep_t>;
+        using univariate = vector<rational>;
+
+        virtual ~univariate_solver();
+
+        virtual void push() = 0;
+        virtual void pop(unsigned n) = 0;
+
+        virtual lbool check() = 0;
+        virtual dep_vector unsat_core() = 0;
+        virtual rational model() = 0;
+
+        virtual void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
+        virtual void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
+        virtual void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
+        virtual void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
+        // op constraints?
+    };
+
+    class univariate_solver_factory {
+    public:
+        virtual ~univariate_solver_factory();
+        virtual scoped_ptr<univariate_solver> create() = 0;
+    };
+
+}

src/math/polysat/viable.h

@@ -23,6 +23,7 @@ Author:
 #include "math/polysat/types.h"
 #include "math/polysat/conflict.h"
 #include "math/polysat/constraint.h"
+#include "math/polysat/univariate_solver.h"
 
 namespace polysat {
 
@@ -32,6 +33,7 @@ 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()}) {}