From 731cf9b88522f4e6ad2a91dd03be252d1c7de62b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 19 Mar 2021 15:37:05 -0700
Subject: [PATCH] ensure compilation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/CMakeLists.txt              |  1 +
 src/math/polysat/CMakeLists.txt |  7 +++
 src/math/polysat/polysat.cpp    | 94 +++++++++++++++++++++++++++++++++
 src/math/polysat/polysat.h      | 19 ++++---
 4 files changed, 113 insertions(+), 8 deletions(-)
 create mode 100644 src/math/polysat/CMakeLists.txt
 create mode 100644 src/math/polysat/polysat.cpp

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 75a12cdd9..404d5d521 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -37,6 +37,7 @@ endforeach()
 add_subdirectory(util)
 add_subdirectory(math/polynomial)
 add_subdirectory(math/dd)
+add_subdirectory(math/polysat)
 add_subdirectory(math/hilbert)
 add_subdirectory(math/simplex)
 add_subdirectory(math/automata)
diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
new file mode 100644
index 000000000..89382f290
--- /dev/null
+++ b/src/math/polysat/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(polysat
+  SOURCES
+    polysat.cpp
+  COMPONENT_DEPENDENCIES
+    util
+    dd
+)
diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp
new file mode 100644
index 000000000..ed8244ff6
--- /dev/null
+++ b/src/math/polysat/polysat.cpp
@@ -0,0 +1,94 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat
+
+Abstract:
+
+    Polynomial solver for modular arithmetic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+
+--*/
+
+#include "math/polysat/polysat.h"
+
+namespace polysat {
+
+    std::ostream& poly::display(std::ostream& out) const {
+        return out;
+    }
+
+    std::ostream& constraint::display(std::ostream& out) const {
+        return out;
+    }
+    
+    std::ostream& linear::display(std::ostream& out) const {
+        return out;
+    }
+
+    std::ostream& mono::display(std::ostream& out) const {
+        return out;
+    }
+
+    unsigned solver::poly2size(poly const& p) const {
+        return 0;
+    }
+
+    bool solver::is_viable(unsigned var, rational const& val) const {
+        return false;
+    }
+
+    /*
+        struct del_var;
+        struct del_constraint;
+        struct var_unassign;
+
+        void push();
+        void pop(unsigned n);
+
+        solver(trail_stack& s);
+        ~solver() {}
+
+        lbool check_sat();
+        
+        unsigned add_var(unsigned sz);
+
+        poly var(unsigned v);
+        poly mul(rational cons& r, poly const& p);
+        poly num(rational const& r, unsigned sz);
+        poly add(poly const& p, poly const& q);
+
+        vector<mono> poly2monos(poly const& p) const;        
+
+        void add_eq(poly const& p, unsigned dep);
+        void add_diseq(poly const& p, unsigned dep);
+        void add_ule(poly const& p, poly const& q, unsigned dep);
+        void add_sle(poly const& p, poly const& q, unsigned dep);
+        void assign(unsigned var, unsigned index, bool value, unsigned dep);        
+
+        bool  can_propagate();
+        lbool propagate();
+
+        bool can_decide();
+        void decide(rational & val, unsigned& var);
+        void assign(unsigned var, rational const& val);
+        
+        bool is_conflict();
+        unsigned resolve_conflict(unsigned_vector& deps);            
+        
+        bool can_learn();
+        void learn(constraint& c, unsigned_vector& deps); 
+        void learn(vector<constraint>& cs, unsigned_vector& deps); 
+
+        std::ostream& display(std::ostream& out) const;
+
+        */
+
+}
+
+
diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h
index 45d355377..e0f74fd33 100644
--- a/src/math/polysat/polysat.h
+++ b/src/math/polysat/polysat.h
@@ -18,12 +18,15 @@ Author:
 
 #include "util/dependency.h"
 #include "util/trail.h"
-#include "util/math/dd_pdd.h"
-#include "util/math/dd_bdd.h"
+#include "util/lbool.h"
+#include "math/dd/dd_pdd.h"
+#include "math/dd/dd_bdd.h"
 
 namespace polysat {
 
     class solver;
+    typedef dd::pdd pdd;
+    typedef dd::bdd bdd;
 
     class poly {
         solver&  s;
@@ -35,7 +38,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const;
     };
 
-    inline std::ostream& operator<<(std::ostream& out, poly const& p) { return p.display(p); }
+    inline std::ostream& operator<<(std::ostream& out, poly const& p) { return p.display(out); }
 
     enum ckind_t { eq_t, ule_t, sle_t };
 
@@ -72,10 +75,10 @@ namespace polysat {
     /**
      * monomial is a list of variables and coefficient.
      */
-    clas mono : public unsigned_vector {
+    class mono : public unsigned_vector {
         rational m_coeff;
     public:
-        linear(rational const& coeff): m_coeff(coeff) {}
+        mono(rational const& coeff): m_coeff(coeff) {}
         rational const& coeff() const { return m_coeff; }
         std::ostream& display(std::ostream& out) const;
     };
@@ -117,10 +120,10 @@ namespace polysat {
 
         // Per constraint state
         vector<u_dependency>     m_cdeps;   // each constraint has set of dependencies
-        vector<constraint>       m_constraints
+        vector<constraint>       m_constraints;
 
         // Per variable information
-        vector<dd::bdd>          m_viable;   // set of viable values.
+        vector<bdd>              m_viable;   // set of viable values.
         vector<u_dependency>     m_vdeps;    // dependencies for viable values
         vector<vector<poly>>     m_pdeps;    // dependencies in polynomial form
         vector<rational>         m_value;    // assigned value
@@ -176,7 +179,7 @@ namespace polysat {
          * Create polynomial terms
          */
         poly var(unsigned v);
-        poly mul(rational cons& r, poly const& p);
+        poly mul(rational const& r, poly const& p);
         poly num(rational const& r, unsigned sz);
         poly add(poly const& p, poly const& q);