From: makaimann <makaim@stanford.edu>
Date: Thu, 5 Dec 2019 02:59:44 +0000 (-0800)
Subject: Add mkOp for a single Kind (#3522)
X-Git-Tag: cvc5-1.0.0~3797
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2c68fa6fea5f98d6e5078961156d8c746bbd13c3;p=cvc5.git

Add mkOp for a single Kind (#3522)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 651ed60e4..7a3577e0d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -527,6 +527,30 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::LAST_KIND, LAST_KIND},
     };
 
+/* Set of kinds for indexed operators */
+const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
+    {CHAIN,
+     RECORD_UPDATE,
+     DIVISIBLE,
+     BITVECTOR_REPEAT,
+     BITVECTOR_ZERO_EXTEND,
+     BITVECTOR_SIGN_EXTEND,
+     BITVECTOR_ROTATE_LEFT,
+     BITVECTOR_ROTATE_RIGHT,
+     INT_TO_BITVECTOR,
+     FLOATINGPOINT_TO_UBV,
+     FLOATINGPOINT_TO_UBV_TOTAL,
+     FLOATINGPOINT_TO_SBV,
+     FLOATINGPOINT_TO_SBV_TOTAL,
+     TUPLE_UPDATE,
+     BITVECTOR_EXTRACT,
+     FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+     FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+     FLOATINGPOINT_TO_FP_REAL,
+     FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+     FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+     FLOATINGPOINT_TO_FP_GENERIC});
+
 namespace {
 
 bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
@@ -1025,7 +1049,11 @@ bool Op::isIndexedHelper() const { return !d_expr->isNull(); }
 /* Public methods                                                             */
 bool Op::operator==(const Op& t) const
 {
-  if (d_expr->isNull() || t.d_expr->isNull())
+  if (d_expr->isNull() && t.d_expr->isNull())
+  {
+    return (d_kind == t.d_kind);
+  }
+  else if (d_expr->isNull() || t.d_expr->isNull())
   {
     return false;
   }
@@ -3064,6 +3092,15 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
 /* Create operators                                                           */
 /* -------------------------------------------------------------------------- */
 
+Op Solver::mkOp(Kind kind) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
+      << "Expected a kind for a non-indexed operator.";
+  return Op(kind);
+  CVC4_API_SOLVER_TRY_CATCH_END
+}
+
 Op Solver::mkOp(Kind kind, Kind k) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 326a8fb70..8c9bdc10c 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1890,9 +1890,20 @@ class CVC4_PUBLIC Solver
                const std::vector<Term>& terms) const;
 
   /* .................................................................... */
-  /* Create Operator Terms                                                */
+  /* Create Operators                                                     */
   /* .................................................................... */
 
+  /**
+   * Create an operator for a builtin Kind
+   * The Kind may not be the Kind for an indexed operator
+   *   (e.g. BITVECTOR_EXTRACT)
+   * Note: in this case, the Op simply wraps the Kind.
+   * The Kind can be used in mkTerm directly without
+   *   creating an op first.
+   * @param kind the kind to wrap
+   */
+  Op mkOp(Kind kind) const;
+
   /**
    * Create operator of kind:
    *   - CHAIN
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h
index 3bf9b93c3..dcad8b649 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.h
@@ -66,6 +66,10 @@ void OpBlack::testOpFromKind()
   Op plus(PLUS);
   TS_ASSERT(!plus.isIndexed());
   TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkOp(PLUS));
+  TS_ASSERT_EQUALS(plus, d_solver.mkOp(PLUS));
+  TS_ASSERT_THROWS(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException&);
 }
 
 void OpBlack::testGetIndicesString()