From 9d571cb1156e5ed6a6ba8a261b365e7fb5f92914 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 3 Apr 2020 18:53:41 -0700
Subject: [PATCH] New C++ API: Remove Op::getSort(). (#4208)

---
 src/api/cvc4cpp.cpp      |  6 ----
 src/api/cvc4cpp.h        |  5 ----
 src/api/python/cvc4.pxi  |  5 ----
 src/parser/smt2/Smt2.g   | 65 +---------------------------------------
 test/unit/api/op_black.h | 10 -------
 5 files changed, 1 insertion(+), 90 deletions(-)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 2e6e70d6b..ba42c4a93 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1141,12 +1141,6 @@ Kind Op::getKind() const
   return d_kind;
 }
 
-Sort Op::getSort() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return Sort(d_expr->getType());
-}
-
 bool Op::isNull() const { return isNullHelper(); }
 
 bool Op::isIndexed() const { return isIndexedHelper(); }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index edff95a2f..a2683e773 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -678,11 +678,6 @@ class CVC4_PUBLIC Op
    */
   Kind getKind() const;
 
-  /**
-   * @return the sort of this operator
-   */
-  Sort getSort() const;
-
   /**
    * @return true if this operator is a null term
    */
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 60bd89cbd..1489b34a6 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -191,11 +191,6 @@ cdef class Op:
     def getKind(self):
         return kind(<int> self.cop.getKind())
 
-    def getSort(self):
-        cdef Sort sort = Sort()
-        sort.csort = self.cop.getSort()
-        return sort
-
     def isNull(self):
         return self.cop.isNull()
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1d0fb71cb..35227e7ce 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2138,70 +2138,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
   : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
   {
     attr = AntlrInput::tokenText($KEYWORD);
-    if(attr == ":rewrite-rule") {
-      if(hasValue) {
-        std::stringstream ss;
-        ss << "warning: Attribute " << attr
-           << " does not take a value (ignoring)";
-        PARSER_STATE->warning(ss.str());
-      }
-      // do nothing
-    }
-    else if (attr==":axiom" || attr==":conjecture" || attr==":fun-def")
-    {
-      if(hasValue) {
-        std::stringstream ss;
-        ss << "warning: Attribute " << attr
-           << " does not take a value (ignoring)";
-        PARSER_STATE->warning(ss.str());
-      }
-      api::Term avar;
-      bool success = true;
-      std::string attr_name = attr;
-      attr_name.erase( attr_name.begin() );
-      if( attr==":fun-def" ){
-        if( expr.getKind()!=api::EQUAL || expr[0].getKind()!=api::APPLY_UF ){
-          success = false;
-        }else{
-          api::Sort t = expr[0].getOp().getSort();
-          for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
-            if( expr[0][i].getKind() != api::VARIABLE ||
-                expr[0][i].getSort() != t.getFunctionDomainSorts()[i] ){
-              success = false;
-              break;
-            }else{
-              for( unsigned j=0; j<i; j++ ){
-                if( expr[0][j]==expr[0][i] ){
-                  success = false;
-                  break;
-                }
-              }
-            }
-          }
-        }
-        if( !success ){
-          std::stringstream ss;
-          ss << "warning: Function definition should be an equality whose LHS "
-             << "is an uninterpreted function applied to unique variables.";
-          PARSER_STATE->warning(ss.str());
-        }else{
-          avar = expr[0];
-        }
-      }else{
-        api::Sort boolType = SOLVER->getBooleanSort();
-        avar = PARSER_STATE->bindVar(attr_name, boolType);
-      }
-      if( success ){
-        //Will set the attribute on auxiliary var (preserves attribute on
-        //formula through rewriting).
-        retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
-        Command* c = new SetUserAttributeCommand( attr_name, avar.getExpr() );
-        c->setMuted(true);
-        PARSER_STATE->preemptCommand(c);
-      }
-    } else {
-      PARSER_STATE->attributeNotSupported(attr);
-    }
+    PARSER_STATE->attributeNotSupported(attr);
   }
   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK
     ( term[patexpr, e2]
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h
index 4a66d76aa..e99e8daf2 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.h
@@ -25,7 +25,6 @@ class OpBlack : public CxxTest::TestSuite
   void tearDown() override {}
 
   void testGetKind();
-  void testGetSort();
   void testIsNull();
   void testOpFromKind();
   void testGetIndicesString();
@@ -39,19 +38,10 @@ class OpBlack : public CxxTest::TestSuite
 void OpBlack::testGetKind()
 {
   Op x;
-  TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
   x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
   TS_ASSERT_THROWS_NOTHING(x.getKind());
 }
 
-void OpBlack::testGetSort()
-{
-  Op x;
-  TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
-  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
-  TS_ASSERT_THROWS_NOTHING(x.getSort());
-}
-
 void OpBlack::testIsNull()
 {
   Op x;
-- 
2.30.2