Fix and simplify handling of overloaded symbols

src/cmd_parser.cpp

@@ -112,6 +112,8 @@ bool CmdParser::parseNextCommand()
       {
         d_state.pushAssumptionScope();
       }
+      // note we typically expect d_state.getAssumptionLevel() to be zero
+      // when using ASSUME, but we do not check for this here.
       std::string name = d_eparser.parseSymbol();
       // parse what is proven
       Expr proven = d_eparser.parseFormula();
@@ -850,7 +852,10 @@ bool CmdParser::parseNextCommand()
           d_lex.parseError("Cannot pop at level zero");
         }
         std::vector<Expr> as = d_state.getCurrentAssumptions();
-        Assert (as.size()==1);
+        // The size of assumptions should be one, but may contain more
+        // assumptions if e.g. we encountered assume in a nested assumption
+        // scope. Nevertheless, as[0] is always the first assumption in
+        // the assume-push.
         // push the assumption
         children.push_back(as[0]);
       }

src/expr_info.h

@@ -27,18 +27,25 @@ using AttrMap = std::map<Attr, std::vector<Expr>>;
 class AppInfo
 {
 public:
-  AppInfo() : d_attrCons( ), d_kind(Kind::NONE) {}
+  AppInfo() : d_attrCons( ), d_kind(Kind::NONE), d_isOverloaded(false) {}
   /** Attribute */
   Attr d_attrCons;
   /** Attribute */
   Expr d_attrConsTerm;
   /** Associated kind */
   Kind d_kind;
   /**
-   * The symbols that are overloads of this symbol at the time this symbol was
-   * bound, including itself. This vector is either empty or has size >=2.
+   * Whether this symbol is overloaded. The overloads for this symbol are
+   * maintained in State::d_overloads[d_overloadName].
    */
-  std::vector<Expr> d_overloads;
+  bool d_isOverloaded;
+  /**
+   * The name of the symbol, if overloaded. Note this is required to be
+   * stored explicitly to handle cases where symbols are bound to terms that do
+   * not have their given name, e.g. (define s () (+ 1 1)) maps "s" to the term
+   * (+ 1 1), which does not have the name "s".
+   */
+  std::string d_overloadName;
 };
 
 }  // namespace ethos

src/kind.cpp

@@ -162,6 +162,7 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_INT_MOD: ss << "zmod";break;
         case Kind::EVAL_RAT_DIV: ss << "qdiv";break;
         case Kind::EVAL_IS_NEG: ss << "is_neg";break;
+        case Kind::EVAL_GT: return "gt";break;
         // strings
         case Kind::EVAL_LENGTH: ss << "len"; break;
         case Kind::EVAL_CONCAT: ss << "concat"; break;

src/state.cpp

@@ -237,14 +237,17 @@ void State::popScope()
       std::map<std::string, Expr>::iterator its = d_symTable.find(d_decls[i]);
       Assert (its!=d_symTable.end());
       // it should be overloaded
-      AppInfo* ai = getAppInfo(its->second.getValue());
-      Assert (ai!=nullptr);
+      std::vector<Expr>& ov = d_overloads[d_decls[i]];
       // we always have at least 2 overloads
-      Assert (ai->d_overloads.size()>=2);
+      Assert (ov.size()>=2);
       // was overloaded, we revert the binding
-      ai->d_overloads.pop_back();
-      Expr tmp = ai->d_overloads.back();
+      ov.pop_back();
+      Expr tmp = ov.back();
       its->second = tmp;
+      if (ov.size()==1)
+      {
+        d_overloads.erase(d_decls[i]);
+      }
       continue;
     }
     Trace("overload") << "** unbind " << d_decls[i] << std::endl;
@@ -665,10 +668,12 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
         // must call mkExpr again, since we may auto-evaluate
         return mkExpr(ai->d_kind, achildren);
       }
-      if (!ai->d_overloads.empty())
+      if (ai->d_isOverloaded)
       {
         Trace("overload") << "Use overload when constructing " << k << " " << children << std::endl;
-        Expr ret = getOverloadInternal(ai->d_overloads, children);
+        std::vector<Expr>& ov = d_overloads[ai->d_overloadName];
+        Assert (ov.size()>=2);
+        Expr ret = getOverloadInternal(ov, children);
         if (!ret.isNull())
         {
           vchildren[0] = ret.getValue();
@@ -946,10 +951,12 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
       {
         dummyChildren.emplace_back(mkSymbol(Kind::CONST, "tmp", t));
       }
-      if (ai!=nullptr && !ai->d_overloads.empty())
+      if (ai!=nullptr && ai->d_isOverloaded)
       {
         Trace("overload") << "...overloaded" << std::endl;
-        reto = getOverloadInternal(ai->d_overloads, dummyChildren, ftype.second.getValue());
+        std::vector<Expr>& ov = d_overloads[ai->d_overloadName];
+        Assert (ov.size()>=2);
+        reto = getOverloadInternal(ov, dummyChildren, ftype.second.getValue());
       }
       else
       {
@@ -1137,25 +1144,17 @@ bool State::bind(const std::string& name, const Expr& e)
   if (its!=d_symTable.end())
   {
     Trace("overload") << "** overload: " << name << std::endl;
-    // if already bound, we overload
-    AppInfo& ai = d_appData[its->second.getValue()];
-    std::vector<Expr>& ov = ai.d_overloads;
+    // if already bound, mark as overloaded
     AppInfo& ain = d_appData[e.getValue()];
-    std::vector<Expr>& ovn = ain.d_overloads;
+    ain.d_isOverloaded = true;
+    ain.d_overloadName = name;
+    std::vector<Expr>& ov = d_overloads[name];
     if (ov.empty())
     {
       // if first time overloading, add the original symbol
-      ovn.emplace_back(its->second);
-    }
-    else
-    {
-      // Otherwise, carry all of the overloads from the previous symbol.
-      // Note that since we carry the overloads for each symbol, the space
-      // required here is quadratic, but the number of overloads per symbol
-      // should be very small.
-      ovn.insert(ovn.end(), ov.begin(), ov.end());
+      ov.emplace_back(its->second);
     }
-    ovn.emplace_back(e);
+    ov.emplace_back(e);
     // add to declaration
     if (!d_declsSizeCtx.empty())
     {

src/state.h

@@ -282,6 +282,11 @@ class State
    *   d_overloadedDecls = { "A", "A", "B" }.
    */
   std::vector<std::string> d_overloadedDecls;
+  /**
+   * Maps symbols that are bound to >= 2 terms to the list of all terms bound
+   * to that symbol. Each vector in the range of this map has size >=2.
+   */
+  std::map<std::string, std::vector<Expr>> d_overloads;
   /**
    * Context size, which is the size of d_decls at the time of when each
    * current pushScope was called.

tests/CMakeLists.txt

@@ -139,6 +139,7 @@ set(ethos_test_file_list
     param-dt-parse-amb-fun.eo
     datatypes-split-rule-param.eo
     datatypes-split-rule-param-uinst.eo
+    overload-define.eo
 )
 
 if(ENABLE_ORACLES)

tests/overload-define.eo

@@ -0,0 +1,10 @@
+(declare-type Int ())
+(declare-consts <numeral> Int)
+(declare-const f (-> Int Int Int))
+
+(define g () (f 0))
+(define g () (f 1))
+
+(declare-const P (-> Int Bool))
+
+(assume @p0 (P (g 0)))