From 3a34995b036a8dbf15dad8b346449f36996ee48b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 12 Jan 2022 13:47:05 +0100
Subject: [PATCH] Add eval_and

---
 src/math/polysat/op_constraint.cpp | 14 ++++++++++++++
 src/math/polysat/op_constraint.h   |  1 +
 2 files changed, 15 insertions(+)

diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 31f20cc71..3f98018c8 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -51,6 +51,8 @@ namespace polysat {
         switch (m_op) {
         case code::lshr_op:
             return eval_lshr(p, q, r);
+        case code::and_op:
+            return eval_and(p, q, r);
         default:
             return l_undef;
         }
@@ -287,4 +289,16 @@ namespace polysat {
             }
         }
     }
+
+    lbool op_constraint::eval_and(pdd const& p, pdd const& q, pdd const& r) const {
+        auto& m = p.manager();
+
+        if ((p.is_zero() || q.is_zero()) && r.is_zero())
+            return l_true;
+
+        if (p.is_val() && q.is_val() && r.is_val())
+            return r.val() == bitwise_and(p.val(), q.val()) ? l_true : l_false;
+
+        return l_undef;
+    }
 }
diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h
index a12434fcd..45e73e9c7 100644
--- a/src/math/polysat/op_constraint.h
+++ b/src/math/polysat/op_constraint.h
@@ -44,6 +44,7 @@ namespace polysat {
         lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r) const;
 
         void narrow_and(solver& s);
+        lbool eval_and(pdd const& p, pdd const& q, pdd const& r) const;
 
     public:        
         ~op_constraint() override {}