From 9a933e29e3d0af982b5cf742eac95145c3fbafb1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 Dec 2023 18:00:43 -0800
Subject: [PATCH] include nyis

---
 src/sat/smt/polysat/core.cpp          | 11 ++++++-----
 src/sat/smt/polysat/op_constraint.cpp |  9 +++++++++
 src/sat/smt/polysat/op_constraint.h   |  1 +
 3 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index ac3870635..de2fedb5a 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -69,10 +69,11 @@ namespace polysat {
         void undo() override {            
             auto& [sc, lit, val] = c.m_constraint_index.back();
             auto& vars = sc.vars();
+            IF_VERBOSE(10, 
             verbose_stream() << "undo add watch " << sc << " ";
             if (vars.size() > 0) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[0]] << ") ";
             if (vars.size() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") ";
-            verbose_stream() << "\n";
+            verbose_stream() << "\n");
             SASSERT(vars.size() <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1);
             SASSERT(vars.size() <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
             if (vars.size() > 0)
@@ -141,10 +142,10 @@ namespace polysat {
             add_watch(idx, vars[0]);
         if (vars.size() > 1)
             add_watch(idx, vars[1]);
-        verbose_stream() << "add watch " << sc << " " << vars << "  ";
-        if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
-        if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
-        verbose_stream() << "\n";
+        IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << "  ";
+                    if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
+                    if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
+                    verbose_stream() << "\n");
         s.trail().push(mk_add_watch(*this));
         return idx;
     }
diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp
index 234ddea04..c971fe1cd 100644
--- a/src/sat/smt/polysat/op_constraint.cpp
+++ b/src/sat/smt/polysat/op_constraint.cpp
@@ -42,6 +42,7 @@ namespace polysat {
             break;
         case code::inv_op:
             SASSERT(q.is_zero());
+            break;
         default:
             break;
         }
@@ -192,6 +193,9 @@ namespace polysat {
         case code::lshr_op:
             propagate_lshr(c, dep);
             break;
+        case code::ashr_op:
+            propagate_ashr(c, dep);
+            break;
         case code::shl_op:
             propagate_shl(c, dep);
             break;
@@ -202,6 +206,7 @@ namespace polysat {
             propagate_inv(c, dep);
             break;
         default:
+            verbose_stream() << "not implemented yet: " << *this << "\n";
             NOT_IMPLEMENTED_YET();
             break;
         }
@@ -311,6 +316,10 @@ namespace polysat {
         }
     }   
 
+    void op_constraint::propagate_ashr(core& s, dependency const& dep) {
+
+    }
+
 
     /**
      * Enforce axioms for constraint: r == p << q
diff --git a/src/sat/smt/polysat/op_constraint.h b/src/sat/smt/polysat/op_constraint.h
index d7b6be392..1aec1c486 100644
--- a/src/sat/smt/polysat/op_constraint.h
+++ b/src/sat/smt/polysat/op_constraint.h
@@ -57,6 +57,7 @@ namespace polysat {
         static lbool eval_inv(pdd const& p, pdd const& r);
 
         void propagate_lshr(core& s, dependency const& dep);
+        void propagate_ashr(core& s, dependency const& dep);
         void propagate_shl(core& s, dependency const& dep);
         void propagate_and(core& s, dependency const& dep);
         void propagate_inv(core& s, dependency const& dep);