Add internal support for integer and operator (#4668)

Towards merging iand branch to master. This adds internal support for an "integer AND" operator.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6850ef450c6282e805b3b7ea8064cbf8d1e8dddd..0774d60af4fc2508e346cd939ffac1fad54682ee 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1001,6 +1001,7 @@ install(FILES
           util/divisible.h
           util/gmp_util.h
           util/hash.h
+          util/iand.h
           util/integer_cln_imp.h
           util/integer_gmp_imp.h
           util/maybe.h

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 8e919db86b3be649ba54808d37c1b876d4b9bf95..8159b8ee06768603b89aa72eb29b66b9c51186d5 100644 (file)
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -81,6 +81,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
   ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
   ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java
+  ${CMAKE_CURRENT_BINARY_DIR}/IntAnd.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntToBitVector.java
   ${CMAKE_CURRENT_BINARY_DIR}/Integer.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntegerHashFunction.java

diff --git a/src/cvc4.i b/src/cvc4.i
index 4fc0b092a3297e31a05a703ca172ad75b77ecae3..9fc8ed60e6c3af53dc3cfa8e89394a0e73eb66d0 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -40,6 +40,7 @@ using namespace CVC4;
 #include "smt/command.h"
 #include "util/bitvector.h"
 #include "util/floatingpoint.h"
+#include "util/iand.h"
 #include "util/integer.h"
 #include "util/sexpr.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -206,6 +207,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/integer.i"
 %include "util/rational.i"
 %include "util/bitvector.i"
+%include "util/iand.i"
 %include "util/floatingpoint.i"
 
 // Tim: The remainder of util/.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index e50b79bbce89d4b75055cafffed0d6a6f2b923a7..188ef47e6f664512844c1a9afc643a0301f92909 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -25,6 +25,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 #include "theory/theory.h"
+#include "util/iand.h"
 
 namespace CVC4 {
 namespace theory {
@@ -101,8 +102,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::PLUS:
       return preRewritePlus(t);
     case kind::MULT:
-    case kind::NONLINEAR_MULT:
-      return preRewriteMult(t);  
+    case kind::NONLINEAR_MULT: return preRewriteMult(t);
+    case kind::IAND: return RewriteResponse(REWRITE_DONE, t);
     case kind::EXPONENTIAL:
     case kind::SINE:
     case kind::COSINE:
@@ -165,8 +166,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     case kind::PLUS:
       return postRewritePlus(t);
     case kind::MULT:
-    case kind::NONLINEAR_MULT:
-      return postRewriteMult(t);    
+    case kind::NONLINEAR_MULT: return postRewriteMult(t);
+    case kind::IAND: return postRewriteIAnd(t);
     case kind::EXPONENTIAL:
     case kind::SINE:
     case kind::COSINE:
@@ -371,6 +372,47 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   return RewriteResponse(REWRITE_DONE, res.getNode());
 }
 
+RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
+{
+  Assert(t.getKind() == kind::IAND);
+  NodeManager* nm = NodeManager::currentNM();
+  // if constant, we eliminate
+  if (t[0].isConst() && t[1].isConst())
+  {
+    size_t bsize = t.getOperator().getConst<IntAnd>().d_size;
+    Node iToBvop = nm->mkConst(IntToBitVector(bsize));
+    Node arg1 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[0]);
+    Node arg2 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[1]);
+    Node bvand = nm->mkNode(kind::BITVECTOR_AND, arg1, arg2);
+    Node ret = nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
+    return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+  }
+  else if (t[0] > t[1])
+  {
+    // ((_ iand k) x y) ---> ((_ iand k) y x) if x > y by node ordering
+    Node ret = nm->mkNode(kind::IAND, t.getOperator(), t[1], t[0]);
+    return RewriteResponse(REWRITE_AGAIN, ret);
+  }
+  else if (t[0] == t[1])
+  {
+    // ((_ iand k) x x) ---> x
+    return RewriteResponse(REWRITE_DONE, t[0]);
+  }
+  // simplifications involving constants
+  for (unsigned i = 0; i < 2; i++)
+  {
+    if (!t[i].isConst())
+    {
+      continue;
+    }
+    if (t[i].getConst<Rational>().sgn() == 0)
+    {
+      // ((_ iand k) 0 y) ---> 0
+      return RewriteResponse(REWRITE_DONE, t[i]);
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, t);
+}
 
 RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) {
   return RewriteResponse(REWRITE_DONE, t);

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 0563aa1de79d237799fc492b8191ba996d7152b2..1dc7565144157a3307bb0cefa863f017ae60122d 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -52,7 +52,9 @@ class ArithRewriter : public TheoryRewriter
 
   static RewriteResponse preRewriteMult(TNode t);
   static RewriteResponse postRewriteMult(TNode t);
-  
+
+  static RewriteResponse postRewriteIAnd(TNode t);
+
   static RewriteResponse preRewriteTranscendental(TNode t);
   static RewriteResponse postRewriteTranscendental(TNode t);
 

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 4c35e5d19d640d3d1519a4d10edc45c39218d8d6..858098b7085c942c5005acf0bad1757d95cb1aa4 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -47,6 +47,7 @@ ArithCongruenceManager::ArithCongruenceManager(
   d_ee.addFunctionKind(kind::NONLINEAR_MULT);
   d_ee.addFunctionKind(kind::EXPONENTIAL);
   d_ee.addFunctionKind(kind::SINE);
+  d_ee.addFunctionKind(kind::IAND);
 }
 
 ArithCongruenceManager::~ArithCongruenceManager() {}

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 409534050611656f0bbbcb42d10d50991e17ec90..e563d8f6669410dfb38947486f05f7c872e6d008 100644 (file)
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -133,4 +133,18 @@ nullaryoperator PI "pi"
 
 typerule PI ::CVC4::theory::arith::RealNullaryOperatorTypeRule
 
+# Integer AND, which is parameterized by a (positive) bitwidth k.
+# ((_ iand k) i1 i2) is equivalent to:
+# (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
+# for all integers i1, i2.
+constant IAND_OP \
+       ::CVC4::IntAnd \
+       "::CVC4::UnsignedHashFunction< ::CVC4::IntAnd >" \
+       "util/iand.h" \
+       "operator for integer AND; payload is an instance of the CVC4::IntAnd class"
+parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms"
+
+typerule IAND_OP ::CVC4::theory::arith::IAndOpTypeRule
+typerule IAND ::CVC4::theory::arith::IAndTypeRule
+
 endtheory

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c7b4b3625a2fd2ae46e616012359c6cdf1f9afc4..f964f1628589cdd9eded545c1fdfb66b920f1d6c 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -71,6 +71,12 @@ bool Variable::isLeafMember(Node n){
 
 VarList::VarList(Node n) : NodeWrapper(n) { Assert(isSorted(begin(), end())); }
 
+bool Variable::isIAndMember(Node n)
+{
+  return n.getKind() == kind::IAND && Polynomial::isMember(n[0])
+         && Polynomial::isMember(n[1]);
+}
+
 bool Variable::isDivMember(Node n){
   switch(n.getKind()){
   case kind::DIVISION:

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 3ab5d907a33b721ebbf9f7630ba6ee261a6ce799..484bdbf44ca7850d5cda6f7c55bc025ea6076977 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -239,6 +239,7 @@ public:
      case kind::INTS_DIVISION_TOTAL:
      case kind::INTS_MODULUS_TOTAL:
      case kind::DIVISION_TOTAL: return isDivMember(n);
+     case kind::IAND: return isIAndMember(n);
      case kind::EXPONENTIAL:
      case kind::SINE:
      case kind::COSINE:
@@ -264,6 +265,7 @@ public:
  }
 
   static bool isLeafMember(Node n);
+  static bool isIAndMember(Node n);
   static bool isDivMember(Node n);
   bool isDivLike() const{
     return isDivMember(getNode());

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 30b8ed01de76f6c03869e77de6f9d8e6f43493a5..8b4747927c4f6973ab5971ea76fd4f258701bee3 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -48,6 +48,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
     getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
     getExtTheory()->addFunctionKind(kind::SINE);
     getExtTheory()->addFunctionKind(kind::PI);
+    getExtTheory()->addFunctionKind(kind::IAND);
   }
 }
 

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 2d3d8a28be54281c6f86607b63b7490de5187688..77efcfff7257c6699b412d8540c7559570b43926 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -87,6 +87,49 @@ public:
   }
 };/* class RealNullaryOperatorTypeRule */
 
+class IAndOpTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (n.getKind() != kind::IAND_OP)
+    {
+      InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
+    }
+    TypeNode iType = nodeManager->integerType();
+    std::vector<TypeNode> argTypes;
+    argTypes.push_back(iType);
+    argTypes.push_back(iType);
+    return nodeManager->mkFunctionType(argTypes, iType);
+  }
+}; /* class IAndOpTypeRule */
+
+class IAndTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (n.getKind() != kind::IAND)
+    {
+      InternalError() << "IAND typerule invoked for IAND kind";
+    }
+    if (check)
+    {
+      TypeNode arg1 = n[0].getType(check);
+      TypeNode arg2 = n[1].getType(check);
+      if (!arg1.isInteger() || !arg2.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
+      }
+    }
+    return nodeManager->integerType();
+  }
+}; /* class BitVectorConversionTypeRule */
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index eba5fb8c9d7b959be049efb20fa1911a774b28c3..028288dbc432378fa2640ac0a938650f086ae4d3 100644 (file)
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -17,6 +17,7 @@ libcvc4_add_sources(
   floatingpoint.cpp
   gmp_util.h
   hash.h
+  iand.h
   index.cpp
   index.h
   maybe.h

diff --git a/src/util/iand.h b/src/util/iand.h
new file mode 100644 (file)
index 0000000..b5bc929
--- /dev/null
+++ b/src/util/iand.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file iand.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Anrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The integer AND operator.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__IAND_H
+#define CVC4__IAND_H
+
+#include <cstdint>
+#include <iosfwd>
+
+#include "base/exception.h"
+#include "util/integer.h"
+
+namespace CVC4 {
+
+struct CVC4_PUBLIC IntAnd
+{
+  unsigned d_size;
+  IntAnd(unsigned size) : d_size(size) {}
+  operator unsigned() const { return d_size; }
+}; /* struct IntAnd */
+
+/* -----------------------------------------------------------------------
+ ** Output stream
+ * ----------------------------------------------------------------------- */
+
+inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia)
+{
+  return os << "[" << ia.d_size << "]";
+}
+
+}  // namespace CVC4
+
+#endif /* CVC4__IAND_H */

diff --git a/src/util/iand.i b/src/util/iand.i
new file mode 100644 (file)
index 0000000..92c5a12
--- /dev/null
+++ b/src/util/iand.i
@@ -0,0 +1,9 @@
+%{
+#include "util/iand.h"
+%}
+
+%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const;
+
+%ignore CVC4::operator<<(std::ostream&, const IntAnd&);
+
+%include "util/iand.h"