From 9e28e36342fab5695783de7f29de995d26b92fa3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Oct 2024 10:11:47 -0500 Subject: [PATCH] Fix handling of overloaded symbols in standalone positions (#84) Previously we were using a policy of handling overloaded symbols that did not update the symbol table when a symbol was overloaded but instead kept a reference to it via the original expression. When an overloaded expression was applied, it would be disambiguated based on the other expressions that had the same name. This was incorrect for overloaded symbols that appear in unapplied positions, where we would always take the oldest expression. This fixes the issue by always updating the symbol table and by carrying the overloads to the new expression. This simplifies the logic a bit when expressions are unbound. --- NEWS.md | 3 ++- src/expr_info.h | 5 ++++- src/state.cpp | 41 +++++++++++++++++++++--------------- tests/CMakeLists.txt | 1 + tests/overload-standalone.eo | 14 ++++++++++++ 5 files changed, 45 insertions(+), 19 deletions(-) create mode 100644 tests/overload-standalone.eo diff --git a/NEWS.md b/NEWS.md index 4223b687..04073883 100644 --- a/NEWS.md +++ b/NEWS.md @@ -7,7 +7,8 @@ ethos 0.1.1 prerelease - Adds a new option `--normalize-num`, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals. - Makes the `set-option` command available in proofs and Eunoia files. - Adds `--include=X` and `--reference=X` to the command line interface for including (reference) files. -- Fixed a bug when applying operators with opaque arguments. +- Fixed the disambiguation of overloaded symbols that are not applied to arguments. +- Fixed the interpretation of operators that combine opaque and ordinary arguments. ethos 0.1.0 =========== diff --git a/src/expr_info.h b/src/expr_info.h index 1677da4c..045ce424 100644 --- a/src/expr_info.h +++ b/src/expr_info.h @@ -34,7 +34,10 @@ class AppInfo Expr d_attrConsTerm; /** Associated kind */ Kind d_kind; - /** Overloading */ + /** + * 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. + */ std::vector d_overloads; }; diff --git a/src/state.cpp b/src/state.cpp index fe2e72aa..d357e359 100644 --- a/src/state.cpp +++ b/src/state.cpp @@ -213,18 +213,16 @@ void State::popScope() if (!d_overloadedDecls.empty() && d_overloadedDecls.back()==d_decls[i]) { d_overloadedDecls.pop_back(); + std::map::iterator its = d_symTable.find(d_decls[i]); + Assert (its!=d_symTable.end()); // it should be overloaded - AppInfo* ai = getAppInfo(d_symTable[d_decls[i]].getValue()); + AppInfo* ai = getAppInfo(its->second.getValue()); Assert (ai!=nullptr); - Assert (!ai->d_overloads.empty()); + // we always have at least 2 overloads + Assert (ai->d_overloads.size()>=2); + // was overloaded, we revert the binding ai->d_overloads.pop_back(); - if (ai->d_overloads.size()==1) - { - Trace("overload") << "** no-overload: " << d_decls[i] << std::endl; - // no longer overloaded since the overload vector is now size one - ai->d_overloads.clear(); - } - // was overloaded, so we don't unbind + its->second = ai->d_overloads.back(); continue; } d_symTable.erase(d_decls[i]); @@ -723,7 +721,7 @@ Expr State::mkExpr(Kind k, const std::vector& children) } i++; } - Trace("type_checker") << "...return for " << children[0] << std::endl;// << ": " << Expr(curr) << std::endl; + Trace("type_checker") << "...return for " << children[0] << std::endl; return Expr(curr); } // otherwise partial?? @@ -1080,22 +1078,31 @@ bool State::bind(const std::string& name, const Expr& e) std::map::iterator its = d_symTable.find(name); if (its!=d_symTable.end()) { + Trace("overload") << "** overload: " << name << std::endl; // if already bound, we overload AppInfo& ai = d_appData[its->second.getValue()]; - // if the first time overloading, add the original - if (ai.d_overloads.empty()) + std::vector& ov = ai.d_overloads; + AppInfo& ain = d_appData[e.getValue()]; + std::vector& ovn = ain.d_overloads; + if (ov.empty()) + { + // if first time overloading, add the original symbol + ovn.emplace_back(its->second); + } + else { - Trace("overload") << "** overload: " << name << std::endl; - ai.d_overloads.push_back(its->second); + // 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()); } - ai.d_overloads.push_back(e); + ovn.emplace_back(e); // add to declaration if (!d_declsSizeCtx.empty()) { - d_decls.emplace_back(name); d_overloadedDecls.emplace_back(name); } - return true; } // Trace("state-debug") << "bind " << name << " -> " << &e << std::endl; d_symTable[name] = e; diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 612dd404..6d5913d4 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -126,6 +126,7 @@ set(ethos_test_file_list simple-reference.eo simple-quant-reference.eo simple-lra-reference.eo + overload-standalone.eo ) if(ENABLE_ORACLES) diff --git a/tests/overload-standalone.eo b/tests/overload-standalone.eo new file mode 100644 index 00000000..8fb5a335 --- /dev/null +++ b/tests/overload-standalone.eo @@ -0,0 +1,14 @@ +(declare-const or (-> Bool Bool Bool) :right-assoc-nil false) +(declare-const = (-> (! Type :var T :implicit) T T Bool)) + +(declare-const a Bool) +(declare-const b Bool) + +(define singleton-list ((T Type :implicit) (f (-> T T T)) (a T)) (eo::cons f a (eo::nil f))) + +(declare-rule refl ((T Type) (t T)) + :args (t) + :conclusion (= t t) +) + +(step @p0 (= (or b) (or b)) :rule refl :args ((singleton-list or b)))