More towards alf.as

src/expr.cpp

@@ -206,6 +206,22 @@ std::string Expr::getSymbol() const
 
 ExprValue* Expr::getValue() const { return d_value; }
 
+size_t Expr::getFunctionArity() const
+{
+  Expr et = *this;
+  size_t arity = 0;
+  while (et.getKind()==Kind::FUNCTION_TYPE)
+  {
+    arity += et.getNumChildren()-1;
+    et = et[et.getNumChildren()-1];
+    while (et.getKind()==Kind::EVAL_REQUIRES)
+    {
+      et = et[2];
+    }
+  }
+  return arity;
+}
+
 /**
  * SMT-LIB 2 quoting for symbols
  */

src/expr.h

@@ -157,7 +157,8 @@ class Expr
   std::string getSymbol() const;
   /** Get underlying value */
   ExprValue* getValue() const;
-
+  /** Get arity, where this is a function type. Used for overloading. */
+  size_t getFunctionArity() const;
  private:
   /** The underlying value */
   ExprValue* d_value;

src/state.cpp

@@ -824,40 +824,30 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
     {
       Trace("overload") << "process alf.as " << children[0] << " " << children[1] << std::endl;
       AppInfo* ai = getAppInfo(vchildren[0]);
-      Expr ret;
+      Expr ret = children[0];
       if (ai!=nullptr && !ai->d_overloads.empty())
       {
-        size_t arity = 0;
-        Expr cur = children[1];
-        while (cur.getKind()==Kind::FUNCTION_TYPE)
-        {
-          size_t nchild = cur.getNumChildren();
-          arity += nchild-1;
-          cur = cur[nchild-1];
-        }
-        Trace("overload") << "...overloaded with arity " << arity << std::endl;
+        size_t arity = children[1].getFunctionArity();
+        Trace("overload") << "...overloaded, check arity " << arity << std::endl;
         // look up the overload
         std::map<size_t, Expr>::iterator ito = ai->d_overloads.find(arity);
         if (ito!=ai->d_overloads.end())
         {
           ret = ito->second;
         }
+        // otherwise try the default (first) symbol parsed, which should be children[0]
       }
       else
       {
         Trace("overload") << "...not overloaded" << std::endl;
-        ret = children[0];
       }
-      if (!ret.isNull())
+      Expr tret = d_tc.getType(ret);
+      Trace("overload") << "Compare " << tret << " " << children[1] << std::endl;
+      // must be matchable
+      Ctx ctx;
+      if (d_tc.match(tret.getValue(), vchildren[1], ctx))
       {
-        Expr tret = d_tc.getType(ret);
-        Trace("overload") << "Compare " << tret << " " << children[1] << std::endl;
-        // must be matchable
-        Ctx ctx;
-        if (d_tc.match(tret.getValue(), vchildren[1], ctx))
-        {
-          return ret;
-        }
+        return ret;
       }
     }
   }
@@ -1021,16 +1011,7 @@ bool State::bind(const std::string& name, const Expr& e)
     AppInfo& ai = d_appData[its->second.getValue()];
     Expr ee = e;
     Expr et = d_tc.getType(ee);
-    size_t arity = 0;
-    while (et.getKind()==Kind::FUNCTION_TYPE)
-    {
-      arity++;
-      et = et[et.getNumChildren()-1];
-      while (et.getKind()==Kind::EVAL_REQUIRES)
-      {
-        et = et[2];
-      }
-    }
+    size_t arity = et.getFunctionArity();
     Trace("overload") << "Overload " << e << " for " << its->second << " with arity " << arity << std::endl;
     if (ai.d_overloads.find(arity)!=ai.d_overloads.end())
     {

tests/overloading-as.smt3

@@ -5,4 +5,4 @@
 (declare-const ho_pred (-> (-> Int Int) Bool))
 
 
-(assume @p0 (ho_pred (alf.as - (-> Bool Int))))
+(assume @p0 (ho_pred (alf.as - (-> Int Int))))