From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Aug 2020 21:35:19 +0000 (-0500)
Subject: Update datatypes in cvc parser to the new API (#4826)
X-Git-Tag: cvc5-1.0.0~3051
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f332d9eb50796d0dde8302d463ed830fc6770133;p=cvc5.git

Update datatypes in cvc parser to the new API (#4826)

This is leftover from the parser conversion. This is towards eliminating all remaining Expr-level calls in the parser.

Notice that 2 parser-level checks for records are eliminated in this PR, since we do not export record objects in the new API.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index fe5f5e636..091b5a22b 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1646,9 +1646,9 @@ tupleStore[CVC4::api::Term& f]
         ss << "tuple is of length " << length << "; cannot update index " << k;
         PARSER_STATE->parseError(ss.str());
       }
-      const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
+      const api::Datatype& dt = t.getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f);
+          api::APPLY_SELECTOR, dt[0][k].getSelectorTerm(), f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1675,13 +1675,9 @@ recordStore[CVC4::api::Term& f]
            << "its type: " << t;
         PARSER_STATE->parseError(ss.str());
       }
-      const Record& rec = ((DatatypeType)t.getType()).getRecord();
-      if(! rec.contains(id)) {
-        PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
-      }
-      const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
+      const api::Datatype& dt = t.getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f);
+          api::APPLY_SELECTOR, dt[0][id].getSelectorTerm(), f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1820,13 +1816,9 @@ postfixTerm[CVC4::api::Term& f]
           if(! type.isRecord()) {
             PARSER_STATE->parseError("record-select applied to non-record");
           }
-          const Record& rec = ((DatatypeType)type.getType()).getRecord();
-          if(!rec.contains(id)){
-            PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
-          }
-          const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
+          const api::Datatype& dt = type.getDatatype();
           f = SOLVER->mkTerm(api::APPLY_SELECTOR,
-                             api::Term(SOLVER, dt[0][id].getSelector()),
+                             dt[0][id].getSelectorTerm(),
                              f);
         }
       | k=numeral
@@ -1841,9 +1833,9 @@ postfixTerm[CVC4::api::Term& f]
             ss << "tuple is of length " << length << "; cannot access index " << k;
             PARSER_STATE->parseError(ss.str());
           }
-          const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
+          const api::Datatype& dt = type.getDatatype();
           f = SOLVER->mkTerm(api::APPLY_SELECTOR,
-                             api::Term(SOLVER, dt[0][k].getSelector()),
+                             dt[0][k].getSelectorTerm(),
                              f);
         }
       )
@@ -1883,8 +1875,8 @@ relationTerm[CVC4::api::Term& f]
       args.push_back(f);
       types.push_back(f.getSort());
       api::Sort t = SOLVER->mkTupleSort(types);
-      const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
-      args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
+      const api::Datatype& dt = t.getDatatype();
+      args.insert(args.begin(), dt[0].getConstructorTerm());
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }
   | IDEN_TOK LPAREN formula[f] RPAREN
@@ -2135,8 +2127,8 @@ simpleTerm[CVC4::api::Term& f]
           types.push_back((*i).getSort());
         }
         api::Sort dtype = SOLVER->mkTupleSort(types);
-        const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-        args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
+        const api::Datatype& dt = dtype.getDatatype();
+        args.insert(args.begin(), dt[0].getConstructorTerm());
         f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
       }
     }
@@ -2145,9 +2137,8 @@ simpleTerm[CVC4::api::Term& f]
   | LPAREN RPAREN
     { std::vector<api::Sort> types;
       api::Sort dtype = SOLVER->mkTupleSort(types);
-      const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      f = MK_TERM(api::APPLY_CONSTRUCTOR,
-                  api::Term(SOLVER, dt[0].getConstructor()));
+      const api::Datatype& dt = dtype.getDatatype();
+      f = MK_TERM(api::APPLY_CONSTRUCTOR, dt[0].getConstructorTerm());
     }
 
     /* empty record literal */
@@ -2155,9 +2146,8 @@ simpleTerm[CVC4::api::Term& f]
     {
       api::Sort dtype = SOLVER->mkRecordSort(
           std::vector<std::pair<std::string, api::Sort>>());
-      const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      f = MK_TERM(api::APPLY_CONSTRUCTOR,
-                  api::Term(SOLVER, dt[0].getConstructor()));
+      const api::Datatype& dt = dtype.getDatatype();
+      f = MK_TERM(api::APPLY_CONSTRUCTOR, dt[0].getConstructorTerm());
     }
     /* empty set literal */
   | LBRACE RBRACE
@@ -2254,8 +2244,8 @@ simpleTerm[CVC4::api::Term& f]
         typeIds.push_back(std::make_pair(names[i], args[i].getSort()));
       }
       api::Sort dtype = SOLVER->mkRecordSort(typeIds);
-      const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
+      const api::Datatype& dt = dtype.getDatatype();
+      args.insert(args.begin(), dt[0].getConstructorTerm());
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }