rename polysat files to exclude namespace

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/polysat/CMakeLists.txt

@@ -1,13 +1,13 @@
 z3_add_component(polysat
   SOURCES
+    assignment.cpp
+    constraints.cpp
+    core.cpp
     fixed_bits.cpp
-    polysat_assignment.cpp
-    polysat_constraints.cpp
-    polysat_core.cpp
-    polysat_fi.cpp
-    polysat_ule.cpp
-    polysat_umul_ovfl.cpp
-    polysat_viable.cpp
+    forbidden_intervals.cpp
+    ule_constraint.cpp
+    umul_ovfl_constraint.cpp
+    viable.cpp
   COMPONENT_DEPENDENCIES
     util
     dd

src/sat/smt/polysat/assignment.cpp

@@ -13,8 +13,8 @@ Author:
 --*/
 
 #include <utility>
-#include "sat/smt/polysat/polysat_assignment.h"
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/assignment.h"
+#include "sat/smt/polysat/core.h"
 
 namespace polysat {
 

src/sat/smt/polysat/assignment.h

@@ -13,7 +13,7 @@ Author:
 --*/
 #pragma once
 #include "util/scoped_ptr_vector.h"
-#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/types.h"
 
 namespace polysat {
 

src/sat/smt/polysat/constraints.cpp

@@ -13,10 +13,10 @@ Author:
 --*/
 
 #include "util/log.h"
-#include "sat/smt/polysat/polysat_core.h"
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_ule.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/core.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/ule_constraint.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
 
 namespace polysat {
 

src/sat/smt/polysat/constraints.h

@@ -15,7 +15,7 @@ Author:
 
 #pragma once 
 #include "util/trail.h"
-#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/types.h"
 
 namespace polysat {
 

src/sat/smt/polysat/core.cpp

@@ -28,7 +28,7 @@ polysat::core
 
 --*/
 
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/core.h"
 
 namespace polysat {
 
@@ -335,4 +335,15 @@ namespace polysat {
         return s.trail();
     }
 
+    std::ostream& core::display(std::ostream& out) const {
+        if (m_constraint_index.empty() && m_vars.empty())
+            return out;
+        out << "polysat:\n";
+        for (auto const& [sc, d, value] : m_constraint_index) 
+            out << sc << " " << d << " := " << value << "\n";        
+        for (unsigned i = 0; i < m_vars.size(); ++i) 
+            out << "p" << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";
+        return out;
+    }
+
 }

src/sat/smt/polysat/core.h

@@ -21,10 +21,10 @@ Author:
 #include "util/dependency.h"
 #include "math/dd/dd_pdd.h"
 #include "sat/sat_extension.h"
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_viable.h"
-#include "sat/smt/polysat/polysat_assignment.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/viable.h"
+#include "sat/smt/polysat/assignment.h"
 
 namespace polysat {
 
@@ -136,7 +136,7 @@ namespace polysat {
         constraints& cs() { return m_constraints; }
         trail_stack& trail();
 
-        std::ostream& display(std::ostream& out) const { NOT_IMPLEMENTED_YET();  throw default_exception("nyi"); }
+        std::ostream& display(std::ostream& out) const;
     };
 
 }

src/sat/smt/polysat/fixed_bits.cpp

@@ -12,7 +12,7 @@ Author:
 --*/
 
 #include "sat/smt/polysat/fixed_bits.h"
-#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/ule_constraint.h"
 
 namespace polysat {
 

src/sat/smt/polysat/fixed_bits.h

@@ -11,8 +11,8 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/constraints.h"
 #include "util/vector.h"
 
 namespace polysat {

src/sat/smt/polysat/forbidden_intervals.cpp

@@ -13,11 +13,11 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
 
 --*/
-#include "sat/smt/polysat/polysat_fi.h"
-#include "sat/smt/polysat/polysat_interval.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
-#include "sat/smt/polysat/polysat_ule.h"
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/forbidden_intervals.h"
+#include "sat/smt/polysat/interval.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
+#include "sat/smt/polysat/ule_constraint.h"
+#include "sat/smt/polysat/core.h"
 
 namespace polysat {
 

src/sat/smt/polysat/forbidden_intervals.h

@@ -14,9 +14,9 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_interval.h"
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/interval.h"
+#include "sat/smt/polysat/constraints.h"
 
 namespace polysat {
 

src/sat/smt/polysat/interval.h

@@ -12,7 +12,7 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/types.h"
 #include <optional>
 
 namespace polysat {

src/sat/smt/polysat/ule_constraint.cpp

@@ -70,8 +70,8 @@ Useful lemmas:
 
 --*/
 
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/ule_constraint.h"
 
 #define LOG(_msg_) verbose_stream() << _msg_ << "\n"
 

src/sat/smt/polysat/ule_constraint.h

@@ -12,8 +12,8 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_assignment.h"
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/assignment.h"
+#include "sat/smt/polysat/constraints.h"
 
 
 namespace polysat {

src/sat/smt/polysat/umul_ovfl_constraint.cpp

@@ -10,9 +10,9 @@ Author:
     Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
 
 --*/
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_assignment.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/assignment.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
 
 
 namespace polysat {

src/sat/smt/polysat/umul_ovfl_constraint.h

@@ -11,7 +11,7 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/constraints.h"
 
 namespace polysat {
 

src/sat/smt/polysat/viable.cpp

@@ -18,9 +18,9 @@ Notes:
 
 #include "util/debug.h"
 #include "util/log.h"
-#include "sat/smt/polysat/polysat_viable.h"
-#include "sat/smt/polysat/polysat_core.h"
-#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/viable.h"
+#include "sat/smt/polysat/core.h"
+#include "sat/smt/polysat/ule_constraint.h"
 
 namespace polysat {
 

src/sat/smt/polysat/viable.h

@@ -21,8 +21,8 @@ Author:
 #include "util/map.h"
 #include "util/small_object_allocator.h"
 
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_fi.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/forbidden_intervals.h"
 
 namespace polysat {
 

src/sat/smt/polysat_solver.cpp

@@ -27,8 +27,8 @@ The result of polysat::core::check is one of:
 #include "ast/euf/euf_bv_plugin.h"
 #include "sat/smt/polysat_solver.h"
 #include "sat/smt/euf_solver.h"
-#include "sat/smt/polysat/polysat_ule.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/ule_constraint.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
 
 
 

src/sat/smt/polysat_solver.h

@@ -18,7 +18,7 @@ Author:
 
 #include "sat/smt/sat_th.h"
 #include "math/dd/dd_pdd.h"
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/core.h"
 #include "sat/smt/intblast_solver.h"
 
 namespace euf {