Working

cvc5 · Oct 30, 2024 · 620b150 · 620b150
1 parent 75e4c3f
commit 620b150
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 4 deletions.
diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp
@@ -278,13 +278,13 @@ bool CmdParser::parseNextCommand()
       for (std::pair<const ExprValue* const, std::vector<Expr>>& d : dts)
       {
         Expr dt = Expr(d.first);
-        Expr ctuple = d_state.mkExpr(Kind::TUPLE, d.second);
+        Expr ctuple = d_state.mkList(d.second);
         d_state.markConstructorKind(dt, attr, ctuple);
       }
       for (std::pair<const ExprValue* const, std::vector<Expr>>& c : dtcons)
       {
         Expr cons = Expr(c.first);
-        Expr stuple = d_state.mkExpr(Kind::TUPLE, c.second);
+        Expr stuple = d_state.mkList(c.second);
         d_state.markConstructorKind(cons, Attr::DATATYPE_CONSTRUCTOR, stuple);
       }
       d_lex.eatToken(Token::RPAREN);

diff --git a/src/kind.cpp b/src/kind.cpp
@@ -92,6 +92,8 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_TO_RAT: o << "EVAL_TO_RAT"; break;
     case Kind::EVAL_TO_BIN: o << "EVAL_TO_BIN"; break;
     case Kind::EVAL_TO_STRING: o << "EVAL_TO_STRING"; break;
+    // datatypes
+    case Kind::EVAL_DEF_OF: o << "EVAL_DEF_OF"; break;
     default: o << "UnknownKind(" << unsigned(k) << ")"; break;
   }
   return o;
@@ -167,6 +169,8 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_TO_RAT: ss << "to_q";break;
         case Kind::EVAL_TO_BIN: ss << "to_bin";break;
         case Kind::EVAL_TO_STRING: ss << "to_str";break;
+        // datatypes
+        case Kind::EVAL_DEF_OF: ss << "def_of"; break;
         default:ss << "[" << k << "]";break;
         }
       }
@@ -256,7 +260,9 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_TO_RAT:
     case Kind::EVAL_TO_BIN:
-    case Kind::EVAL_TO_STRING:return true; break;
+    case Kind::EVAL_TO_STRING:
+    // datatypes
+    case Kind::EVAL_DEF_OF: return true; break;
     default: break;
   }
   return false;

diff --git a/src/kind.h b/src/kind.h
@@ -101,7 +101,9 @@ enum class Kind
   EVAL_TO_INT,
   EVAL_TO_RAT,
   EVAL_TO_BIN,
-  EVAL_TO_STRING
+  EVAL_TO_STRING,
+  // datatypes
+  EVAL_DEF_OF
 };
 
 /** Print a kind to the stream, for debugging */

diff --git a/src/state.cpp b/src/state.cpp
@@ -145,6 +145,8 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("concat", Kind::EVAL_CONCAT);
   bindBuiltinEval("extract", Kind::EVAL_EXTRACT);
   bindBuiltinEval("find", Kind::EVAL_FIND);
+  // datatypes
+  bindBuiltinEval("def_of", Kind::EVAL_DEF_OF);
 
   // as
   bindBuiltinEval("as", Kind::AS);
@@ -972,6 +974,18 @@ Expr State::mkParameterized(const ExprValue* hd, const std::vector<Expr>& params
   return mkExpr(Kind::PARAMETERIZED, {mkExpr(Kind::TUPLE, params), Expr(hd)});
 }
 
+Expr State::mkList(const std::vector<Expr>& args)
+{
+  if (args.empty())
+  {
+    return d_listNil;
+  }
+  std::vector<Expr> largs;
+  largs.push_back(d_listCons);
+  largs.insert(largs.end(), args.begin(), args.end());
+  return mkExpr(Kind::APPLY, largs);
+}
+
 ExprValue* State::mkLiteralInternal(Literal& l)
 {
   d_stats.d_mkExprCount++;

diff --git a/src/state.h b/src/state.h
@@ -138,6 +138,9 @@ class State
    * Make parameterized with given parameters
    */
   Expr mkParameterized(const ExprValue* hd, const std::vector<Expr>& params);
+  /**
+   */
+  Expr mkList(const std::vector<Expr>& args);
   //--------------------------------------
   /** Get the constructor kind for symbol v */
   Attr getConstructorKind(const ExprValue* v) const;

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -178,6 +178,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_IS_STR:
     case Kind::EVAL_IS_BOOL:
     case Kind::EVAL_IS_VAR:
+    case Kind::EVAL_DEF_OF:
       ret = (nargs==1);
       break;
     case Kind::EVAL_NIL:
@@ -1173,6 +1174,20 @@ Expr TypeChecker::evaluateLiteralOpInternal(
       }
     }
     break;
+    case Kind::EVAL_DEF_OF:
+    {
+      AppInfo* ac = d_state.getAppInfo(args[0]);
+      if (ac!=nullptr)
+      {
+        Assert (args[0]->isGround());
+        Attr a = ac->d_attrCons;
+        if (a==Attr::DATATYPE || a==Attr::DATATYPE_CONSTRUCTOR)
+        {
+          return ac->d_attrConsTerm;
+        }
+      }
+    }
+    break;
     default:
       break;
   }