Add sort_or_str option which carries through string representation fo…

…r unknown sorts

src/smtlibparser.yy

@@ -86,6 +86,11 @@ US "_"
 %nterm <smt::TermVec *> s_expr_list
 %nterm <smt::Term> atom
 %nterm <smt::Term> bvconst
+/* same as sort but if sort is null
+   stores a string.
+   originally introduced for self-referential datatypes
+*/
+%nterm <std::pair<smt::Sort, std::string>> sort_or_str
 %nterm <smt::Sort> sort
 %nterm <smt::SortVec> sort_list
 %nterm <std::pair<std::string, std::size_t>> sort_dec
@@ -404,55 +409,98 @@ bvconst:
    }
 ;
 
-sort:
+sort_or_str:
    SYMBOL
    {
      smt::Sort res;
      // check built-in sort kinds first
      smt::SortKind sk = drv.lookup_sortkind($1);
-     if (sk == smt::NUM_SORT_KINDS)
+     try
      {
-       // got the dedicated null enum
-       // check defined sorts
-       res = drv.lookup_sort($1);
+        if (sk == smt::NUM_SORT_KINDS)
+        {
+          // got the dedicated null enum
+          // check defined sorts
+          res = drv.lookup_sort($1);
+        }
+        else if (sk == smt::UNINTERPRETED)
+        {
+          // uninterpreted sorts also stored with defined sorts
+          res = drv.lookup_sort($1);
+        }
+        else
+        {
+          res = drv.solver()->make_sort(sk);
+        }
      }
-     else if (sk == smt::UNINTERPRETED)
+     catch (SmtException & e)
      {
-       // uninterpreted sorts also stored with defined sorts
-       res = drv.lookup_sort($1);
+       ;
      }
-     else
+
+     std::string repr;
+     if (!res)
      {
-       res = drv.solver()->make_sort(sk);
+       // only carry along string representation
+       // if sort is null
+       repr = $1;
      }
-     $$ = res;
+     $$ = {res, repr};
    }
    | indprefix SYMBOL NAT RP
    {
      // this one is intended for bit-vectors
      smt::SortKind sk = drv.lookup_sortkind($2);
      if (sk == smt::NUM_SORT_KINDS)
      {
-       // got dedicated null enum
-       yy::parser::error(@2, std::string("Unrecognized sort: ") + $2);
-       YYERROR;
+       $$ = {nullptr, "(_ " + $2 + $3 + ")"};
+     }
+     else
+     {
+       $$ = {drv.solver()->make_sort(sk, std::stoi($3)), ""};
      }
-     $$ = drv.solver()->make_sort(sk, std::stoi($3));
    }
    | LP SYMBOL sort_list RP
    {
      smt::SortKind sk = drv.lookup_sortkind($2);
      if (sk == smt::ARRAY)
      {
-     // this one is intended for arrays
-       $$ = drv.solver()->make_sort(sk, $3[0], $3[1]);
+       // this one is intended for arrays
+       $$ = {drv.solver()->make_sort(sk, $3[0], $3[1]), ""};
      }
      else
      {
-       // defined or declared sort
-       smt::Sort sort_con = drv.lookup_sort($2);
-       $$ = drv.solver()->make_sort(sort_con, $3);
+       try
+       {
+         // defined or declared sort
+         smt::Sort sort_con = drv.lookup_sort($2);
+         $$ = {drv.solver()->make_sort(sort_con, $3), ""};
+       }
+       catch(SmtException & e)
+       {
+         std::string repr = "(";
+         for (const auto & s : $3)
+         {
+           repr += s->to_string();
+           repr += " ";
+         }
+         repr += ")";
+
+         $$ = {nullptr, repr};
+       }
+     }
+   }
+;
+
+sort:
+   sort_or_str
+   {
+     if (!$1.first)
+     {
+       yy::parser::error(@1, "Unknown sort: " + $1.second);
+       YYERROR;
      }
+     $$ = $1.first;
    }
 ;