New C++ API: Remove Op::getSort(). (#4208)
authorAina Niemetz <aina.niemetz@gmail.com>
Sat, 4 Apr 2020 01:53:41 +0000 (18:53 -0700)
committerGitHub <noreply@github.com>
Sat, 4 Apr 2020 01:53:41 +0000 (18:53 -0700)
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/python/cvc4.pxi
src/parser/smt2/Smt2.g
test/unit/api/op_black.h

index 2e6e70d6bd766f741f8f003afa49f6f9628af3ce..ba42c4a9304d055ccb7555cdd4529c68a8001bc3 100644 (file)
@@ -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(); }
index edff95a2f3b876309b7fe7144df0bd78b3819329..a2683e77302ce668cc94fad8a6c1d9d9381f4504 100644 (file)
@@ -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
    */
index 60bd89cbd3abf271374ce106534c28ce1d1df8e8..1489b34a60596b1f7442e5f35c74e1077940032c 100644 (file)
@@ -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()
 
index 1d0fb71cbee7e836f078860d65f2cf1a5df92a35..35227e7cece16156674e88fc88bd871b7ba38602 100644 (file)
@@ -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]
index 4a66d76aa5a322fcb9e4fd033b5d5142d30dc9aa..e99e8daf2a112f225e26aa518fc15e4756ea5960 100644 (file)
@@ -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;