Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)

Fixes #4092 and fixes #4134.

Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 5b28f669d..ecf86376c 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -154,11 +154,15 @@ public:
   //is well sorted
   bool isWellSortedFormula( Node n );
   bool isWellSorted( Node n );
-  //get constraints for being well-typed according to computed sub-types
-  void getSortConstraints( Node n, SortInference::UnionFind& uf );
 private:
   // store monotonicity for original sorts as well
  std::map<TypeNode, bool> d_non_monotonic_sorts_orig;
+ /**
+  * Returns true if k is the APPLY_UF kind and we are not using higher-order
+  * techniques. This is called in places where we want to know whether to
+  * treat a term as uninterpreted function.
+  */
+ bool isHandledApplyUf(Kind k) const;
 };
 
 }