From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 10 Jul 2020 20:51:25 +0000 (-0500)
Subject: Front end support for integer AND (#4717)
X-Git-Tag: cvc5-1.0.0~3133
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e9b3dfa40f0297bdb005f6c802443ebb3b8cad1;p=cvc5.git

Front end support for integer AND (#4717)
---

diff --git a/NEWS b/NEWS
index ee01b5212..b34d9b116 100644
--- a/NEWS
+++ b/NEWS
@@ -8,6 +8,8 @@ New Features:
   syntax for sequences used by Z3.
 * Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
   if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
+* Support for an integer operator `(_ iand n)` that returns the bitwise `and`
+  of two integers, seen as integers modulo n.
 
 Improvements:
 * New API: Added functions to retrieve the heap/nil term when using separation
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index a04b5cf85..ebafc3cc8 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -98,6 +98,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     /* Arithmetic ---------------------------------------------------------- */
     {PLUS, CVC4::Kind::PLUS},
     {MULT, CVC4::Kind::MULT},
+    {IAND, CVC4::Kind::IAND},
     {MINUS, CVC4::Kind::MINUS},
     {UMINUS, CVC4::Kind::UMINUS},
     {DIVISION, CVC4::Kind::DIVISION},
@@ -348,6 +349,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         /* Arithmetic ------------------------------------------------------ */
         {CVC4::Kind::PLUS, PLUS},
         {CVC4::Kind::MULT, MULT},
+        {CVC4::Kind::IAND, IAND},
         {CVC4::Kind::MINUS, MINUS},
         {CVC4::Kind::UMINUS, UMINUS},
         {CVC4::Kind::DIVISION, DIVISION},
@@ -593,6 +595,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
 const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
     {RECORD_UPDATE,
      DIVISIBLE,
+     IAND,
      BITVECTOR_REPEAT,
      BITVECTOR_ZERO_EXTEND,
      BITVECTOR_SIGN_EXTEND,
@@ -1262,6 +1265,7 @@ uint32_t Op::getIndices() const
       i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount;
       break;
     case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break;
+    case IAND: i = d_expr->getConst<IntAnd>().d_size; break;
     case FLOATINGPOINT_TO_UBV:
       i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size;
       break;
@@ -4019,6 +4023,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
                *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
                     .d_expr.get());
       break;
+    case IAND:
+      res = Op(this,
+               kind,
+               *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_expr.get());
+      break;
     case FLOATINGPOINT_TO_UBV:
       res = Op(
           this,
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index b3e88c98c..1f23d0e8d 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -319,6 +319,23 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   MULT,
+  /**
+   * Operator for Integer AND
+   * Parameter: 1
+   *   -[1]: Size of the bit-vector that determines the semantics of the IAND
+   * Create with:
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply integer conversion to bit-vector.
+   * Parameters: 2
+   *   -[1]: Op of kind IAND
+   *   -[2]: Integer term
+   *   -[3]: Integer term
+   * Create with:
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op, const std::vector<Term>& children)
+   */
+  IAND,
 #if 0
   /* Synonym for MULT.  */
   NONLINEAR_MULT,
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 46a2e2c59..ec2009cc3 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -639,6 +639,11 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
       defineVar("real.pi", d_solver->mkTerm(api::PI));
       addTranscendentalOperators();
     }
+    if (!strictModeEnabled())
+    {
+      // integer version of AND
+      addIndexedOperator(api::IAND, api::IAND, "iand");
+    }
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6077601bc..773c733d6 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -601,6 +601,10 @@ void Smt2Printer::toStream(std::ostream& out,
     parametricTypeChildren = true;
     out << smtKindString(k, d_variant) << " ";
     break;
+  case kind::IAND:
+    out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
+    stillNeedToPrintParams = false;
+    break;
 
   case kind::DIVISIBLE:
     out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
@@ -1031,6 +1035,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::PLUS: return "+";
   case kind::MULT:
   case kind::NONLINEAR_MULT: return "*";
+  case kind::IAND: return "iand";
   case kind::EXPONENTIAL: return "exp";
   case kind::SINE: return "sin";
   case kind::COSINE: return "cos";
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 00aa786ae..dd48b1fff 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1402,6 +1402,7 @@ set(regress_1_tests
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
+  regress1/nl/iand-native-1.smt2
   regress1/nl/issue3300-approx-sqrt-witness.smt2
   regress1/nl/issue3441.smt2
   regress1/nl/issue3617.smt2
diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress1/nl/iand-native-1.smt2
new file mode 100644
index 000000000..685922f88
--- /dev/null
+++ b/test/regress/regress1/nl/iand-native-1.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --iand-mode=value
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (and (<= 0 y) (< y 16)))
+(assert (> ((_ iand 4) x y) 0))
+
+(check-sat)