From 01c81405af41873aca19867a8de0f80204bb88fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 22 Jun 2021 20:58:32 -0700
Subject: [PATCH] remove var-constraint alltogether

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/CMakeLists.txt     |  1 -
 src/math/polysat/constraint.cpp     |  1 -
 src/math/polysat/solver.h           |  1 -
 src/math/polysat/var_constraint.cpp | 48 -----------------------------
 src/math/polysat/var_constraint.h   | 48 -----------------------------
 5 files changed, 99 deletions(-)
 delete mode 100644 src/math/polysat/var_constraint.cpp
 delete mode 100644 src/math/polysat/var_constraint.h

diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index 09dd6f084..56e2eb57e 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -11,7 +11,6 @@ z3_add_component(polysat
     search_state.cpp
     solver.cpp
     ule_constraint.cpp
-    var_constraint.cpp
     viable.cpp
   COMPONENT_DEPENDENCIES
     util
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 7c5f4642e..86b421f68 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -16,7 +16,6 @@ Author:
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
-#include "math/polysat/var_constraint.h"
 #include "math/polysat/eq_constraint.h"
 #include "math/polysat/ule_constraint.h"
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index e2aa0b1ca..fffda2277 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -22,7 +22,6 @@ Author:
 #include "math/polysat/boolean.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/eq_constraint.h"
-#include "math/polysat/var_constraint.h"
 #include "math/polysat/ule_constraint.h"
 #include "math/polysat/justification.h"
 #include "math/polysat/linear_solver.h"
diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp
deleted file mode 100644
index ceac907af..000000000
--- a/src/math/polysat/var_constraint.cpp
+++ /dev/null
@@ -1,48 +0,0 @@
-/*++
-Copyright (c) 2021 Microsoft Corporation
-
-Module Name:
-
-    polysat var_constraint
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
-
---*/
-
-#if 0
-#include "math/polysat/var_constraint.h"
-#include "math/polysat/solver.h"
-
-namespace polysat {
-
-    std::ostream& var_constraint::display(std::ostream& out) const {
-        out << "v" << m_var << ": " << m_viable << "\n";
-        return display_extra(out);
-    }
-
-    constraint_ref var_constraint::resolve(solver& s, pvar v) {
-        UNREACHABLE();
-        return nullptr;
-    }
-
-    bool var_constraint::is_always_false() {
-        return false;
-    }
-
-    bool var_constraint::is_currently_false(solver& s) {
-        return s.m_vble.is_false(m_var);
-    }
-
-    bool var_constraint::is_currently_true(solver& s) {
-        return !is_currently_false(s);
-    }
-
-    void var_constraint::narrow(solver& s) {
-        s.m_vble.intersect_viable(m_var, m_viable);
-    }
-
-}
-#endif
diff --git a/src/math/polysat/var_constraint.h b/src/math/polysat/var_constraint.h
deleted file mode 100644
index 2594e7d3e..000000000
--- a/src/math/polysat/var_constraint.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*++
-Copyright (c) 2021 Microsoft Corporation
-
-Module Name:
-
-    polysat var_constraint
-
-Abstract:
-
-    Var constraints restrict viable values.
-
-    The main way var-constraints interact with the solver is to 
-    narrow m_viable during initialization. 
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
-
---*/
-
-
-#if 0
-// to remove
-#pragma once
-#include "math/dd/dd_bdd.h"
-#include "math/polysat/constraint.h"
-
-
-namespace polysat {
-
-    class var_constraint : public constraint {
-        pvar        m_var;
-        bdd         m_viable;
-    public:
-        var_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pvar v, bdd const & b, p_dependency_ref const& dep):
-            constraint(m, lvl, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
-        ~var_constraint() override {}
-        std::ostream& display(std::ostream& out) const override;
-        constraint_ref resolve(solver& s, pvar v) override;
-        void narrow(solver& s) override;
-        bool is_always_false() override;
-        bool is_currently_false(solver& s) override;
-        bool is_currently_true(solver& s) override;
-    };
-}
-
-#endif