Format

cvc5 · Nov 1, 2024 · 3171fc8 · 3171fc8
1 parent 371f550
commit 3171fc8
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 20 deletions.
diff --git a/src/kind.h b/src/kind.h
@@ -19,16 +19,16 @@ namespace ethos {
 enum class Kind
 {
   NONE = 0,
-  
+
   // types
   TYPE,
   FUNCTION_TYPE,
   PROOF_TYPE,
   ABSTRACT_TYPE,
   BOOL_TYPE,
   QUOTE_TYPE,
-  OPAQUE_TYPE, // an argument marked :opaque, temporary during parsing
-  
+  OPAQUE_TYPE,  // an argument marked :opaque, temporary during parsing
+
   // terms
   APPLY,
   LAMBDA,

diff --git a/src/state.cpp b/src/state.cpp
@@ -161,7 +161,7 @@ State::State(Options& opts, Stats& stats)
   bind("true", d_true);
   d_false = Expr(new Literal(false));
   bind("false", d_false);
-  
+
   // builtin lists
   d_listType = Expr(mkSymbolInternal(Kind::CONST, "eo::List", d_type));
   bind("eo::List", d_listType);
@@ -175,14 +175,15 @@ State::State(Options& opts, Stats& stats)
   d_listCons = Expr(mkSymbolInternal(Kind::CONST, "eo::List::cons", consType));
   bind("eo::List::cons", d_listCons);
   markConstructorKind(d_listCons, Attr::RIGHT_ASSOC_NIL, d_listNil);
-  
+
   // we do not export eo::null
   // for now, eo::? is (undocumented) syntax for abstract type
   bind("eo::?", d_absType);
   // self is a distinguished parameter
   d_self = Expr(mkSymbolInternal(Kind::PARAM, "eo::self", d_absType));
   bind("eo::self", d_self);
-  d_conclusion = Expr(mkSymbolInternal(Kind::PARAM, "eo::conclusion", d_boolType));
+  d_conclusion =
+      Expr(mkSymbolInternal(Kind::PARAM, "eo::conclusion", d_boolType));
   // eo::conclusion is not globally bound, since it can only appear
   // in :requires.
 }
@@ -554,10 +555,7 @@ Expr State::mkBoolType()
   return d_boolType;
 }
 
-Expr State::mkListType()
-{
-  return d_listType;
-}
+Expr State::mkListType() { return d_listType; }
 
 Expr State::mkProofType(const Expr& proven)
 {

diff --git a/src/state.h b/src/state.h
@@ -141,7 +141,8 @@ class State
    */
   Expr mkParameterized(const ExprValue* hd, const std::vector<Expr>& params);
   /**
-   * Make (eo::List::Cons <args>) if args is non-empty or eo::List::nil otherwise.
+   * Make (eo::List::Cons <args>) if args is non-empty or eo::List::nil
+   * otherwise.
    */
   Expr mkList(const std::vector<Expr>& args);
   //--------------------------------------

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -179,9 +179,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_IS_BOOL:
     case Kind::EVAL_IS_VAR:
     case Kind::EVAL_DT_CONSTRUCTORS:
-    case Kind::EVAL_DT_SELECTORS:
-      ret = (nargs==1);
-      break;
+    case Kind::EVAL_DT_SELECTORS: ret = (nargs == 1); break;
     case Kind::EVAL_NIL:
       ret = (nargs>=1);
       break;
@@ -1179,12 +1177,13 @@ Expr TypeChecker::evaluateLiteralOpInternal(
     case Kind::EVAL_DT_SELECTORS:
     {
       AppInfo* ac = d_state.getAppInfo(args[0]);
-      if (ac!=nullptr)
+      if (ac != nullptr)
       {
-        Assert (args[0]->isGround());
+        Assert(args[0]->isGround());
         Attr a = ac->d_attrCons;
-        if ((a==Attr::DATATYPE && k==Kind::EVAL_DT_CONSTRUCTORS) ||
-            (a==Attr::DATATYPE_CONSTRUCTOR && k==Kind::EVAL_DT_SELECTORS))
+        if ((a == Attr::DATATYPE && k == Kind::EVAL_DT_CONSTRUCTORS)
+            || (a == Attr::DATATYPE_CONSTRUCTOR
+                && k == Kind::EVAL_DT_SELECTORS))
         {
           return ac->d_attrConsTerm;
         }
@@ -1459,8 +1458,7 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
     case Kind::EVAL_TO_BIN:
       return getOrSetLiteralTypeRule(Kind::BINARY);
     case Kind::EVAL_DT_CONSTRUCTORS:
-    case Kind::EVAL_DT_SELECTORS:
-      return d_state.mkListType().getValue();
+    case Kind::EVAL_DT_SELECTORS: return d_state.mkListType().getValue();
     default:break;
   }
   if (out)