HOL improvements (continued)

Inferences/Choice.cpp

@@ -57,8 +57,8 @@ Clause* Choice::createChoiceAxiom(TermList op, TermList set)
   t2 =          HC::app(setSort, set, t2);
 
   return Clause::fromLiterals(
-      { Literal::createEquality(true, t1, TermList(Term::foolFalse()), AtomicSort::boolSort()),
-        Literal::createEquality(true, t2, TermList(Term::foolTrue()), AtomicSort::boolSort())},
+      { Literal::createEquality(true, t1, HOL::create::bottom(), AtomicSort::boolSort()),
+        Literal::createEquality(true, t2, HOL::create::top(), AtomicSort::boolSort())},
        NonspecificInference0(UnitInputType::AXIOM, InferenceRule::HILBERTS_CHOICE_INSTANCE)
   );
 }

Inferences/HOL/CNFOnTheFly.cpp

@@ -64,10 +64,6 @@ ClauseIterator produceClauses(Clause* c, bool generating, SkolemisingFormulaInde
   if(generating && (eager || simp)){ return ClauseIterator::getEmpty(); }
   if(!generating && gen){ return ClauseIterator::getEmpty(); }
 
-  if (instantiations) {
-    INVALID_OPERATION("Options::CNFOnTheFly::CONJ_EAGER not yet supported");
-  }
-
   static TermStack args;
 
   for (const auto& lit : *c) {
@@ -180,13 +176,38 @@ ClauseIterator produceClauses(Clause* c, bool generating, SkolemisingFormulaInde
       case Proxy::PI:
       case Proxy::SIGMA: {
         ASS_EQ(args.size(), 1);
+        ClauseStack instCls;
         TermList srt = *SortHelper::getResultSort(head.term()).term()->nthArgument(0);
         TermList newTerm;
         Proxy proxy;
-        if((prox == Proxy::PI && positive) ||
-          (prox == Proxy::SIGMA && !positive)){
+        if ((prox == Proxy::PI && positive) || (prox == Proxy::SIGMA && !positive)) {
           proxy = Proxy::PI;
           newTerm = piRemoval(args[0], c, srt);
+          if (instantiations && !args[0].isVar()) {
+            auto insts = env.signature->getInstantiations();
+            for (const auto& t : iterTraits(insts->iter())) {
+              ASS(t.isTerm());
+              static RobSubstitution subst;
+              subst.reset();
+
+              auto tSort = SortHelper::getResultSort(t.term());
+              auto aSort = srt.domain();
+
+              if (!subst.unify(tSort,0,aSort,1)) {
+                continue;
+              }
+              auto tS = subst.apply(t, 0);
+              auto argS = subst.apply(args[0],1); 
+
+              RStack<Literal*> resLits;
+              for (const auto& curr : *c) {
+                resLits->push(curr == lit
+                  ? boolEq(HOL::create::app(argS, tS), rhs)
+                  : subst.apply(curr, 1));
+              }
+              instCls.push(Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::HEURISTIC_INSTANTIATION, c)));
+            }
+          }
         } else {
           ASS(term.isTerm());
           bool newTermCreated = false;
@@ -209,8 +230,8 @@ ClauseIterator produceClauses(Clause* c, bool generating, SkolemisingFormulaInde
           }
           proxy = Proxy::SIGMA;
         }
-        return pvi(iterItems(replaceLits(c, lit, proxy, false,
-          positive ? eqTroo(newTerm) : eqFols(newTerm))));
+        return pvi(concatIters(iterItems(replaceLits(c, lit, proxy, false,
+          positive ? eqTroo(newTerm) : eqFols(newTerm))), getPersistentIterator(ClauseStack::Iterator(instCls))));
       }
     }
   }

Inferences/InferenceEngine.cpp

@@ -289,8 +289,7 @@ Clause* TautologyDeletionISE2::simplify(Clause* c)
 
   for(unsigned i = 0; i < c->length(); i++){
     Literal* lit = (*c)[i];
-    TermList lhs = *lit->nthArgument(0);
-    TermList rhs = *lit->nthArgument(1);
+    auto [lhs, rhs] = lit->eqArgs();
     if(!lit->polarity() && HOL::isBool(lhs) && HOL::isBool(rhs) &&
       (HOL::isTrue(lhs) != HOL::isTrue(rhs))){
       //false != true

Kernel/HOL/Convert.cpp

@@ -161,9 +161,9 @@ static TermList formulaToNameless(Formula *formula, const VarToIndexMap& map) {
     case Connective::BOOL_TERM:
       return termToNameless(formula->getBooleanTerm(), map);
     case Connective::TRUE:
-      return TermList(Term::foolTrue());
+      return HOL::create::top();
     case Connective::FALSE:
-      return TermList(Term::foolFalse());
+      return HOL::create::bottom();
     default:
       ASSERTION_VIOLATION;
   }
@@ -172,3 +172,19 @@ static TermList formulaToNameless(Formula *formula, const VarToIndexMap& map) {
 TermList HOL::convert::toNameless(TermList term) {
   return termToNameless(term, {});
 }
+
+TermList HOL::convert::toNameless(Formula* formula)
+{
+  // remove leading universal type quantifiers
+  if (formula->connective() == FORALL) {
+    auto vars = formula->vars();
+    while (vars && vars->head().second == AtomicSort::superSort()) {
+      vars = vars->tail();
+    }
+    if (vars != formula->vars()) {
+      auto f = formula->qarg();
+      formula = vars ? new QuantifiedFormula(FORALL, vars, f) : f;
+    }
+  }
+  return formulaToNameless(formula, {});
+}

Kernel/HOL/HOL.cpp

@@ -11,8 +11,9 @@
  * @file HOL.cpp
  */
 
-#include "Kernel/HOL/HOL.hpp"
+#include "HOL.hpp"
 
+#include "SubtermReplacer.hpp"
 #include "ToPlaceholders.hpp"
 #include "Kernel/Formula.hpp"
 
@@ -482,3 +483,43 @@ TermList HOL::createGeneralBinding(TermList head, const TermStack& sorts, unsign
   auto res = create::app(head, args);
   return surround ? create::surroundWithLambdas(res, sorts) : res;
 }
+
+TermStack HOL::getAbstractionTerms(Literal* lit)
+{
+  auto [lhs, rhs] = lit->eqArgs();
+  TermList eqSort = SortHelper::getEqualityArgumentSort(lit);
+
+  TermStack res;
+  auto dealWithArg = [&](TermList arg, TermList argSort){
+    if (arg.containsLooseDBIndex()) {
+      return;
+    }
+    using namespace create;
+    SubtermReplacer st(arg, getDeBruijnIndex(0,argSort), true);
+    TermList lhsReplaced = st.replace(lhs);
+    TermList rhsReplaced = st.replace(rhs);
+
+    TermList eq = app2(equality(eqSort), lhsReplaced, rhsReplaced);
+    eq = lit->polarity() ? app(neg(),eq) : eq; // reverse the polarity of the literal
+    res.push(namelessLambda(argSort,eq));
+  };
+
+  TermList lhsHead, rhsHead;
+  TermList lhsMatrix, rhsMatrix;
+  static TermStack lhsArgs;
+  static TermStack lhsArgSorts;
+  static TermStack rhsArgs;
+  static TermStack rhsArgSorts;
+
+  getHeadArgsAndArgSorts(lhs, lhsHead, lhsArgs, lhsArgSorts);
+  getHeadArgsAndArgSorts(rhs, rhsHead, rhsArgs, rhsArgSorts);
+  if (lhsHead.isTerm() && lhsHead.deBruijnIndex().isNone() && lhsHead == rhsHead) {
+    for(unsigned i = 0; i < lhsArgs.size(); i++){
+      dealWithArg(lhsArgs[i], lhsArgSorts[i]);
+    }
+    for(unsigned i = 0; i < rhsArgs.size(); i++){
+      dealWithArg(rhsArgs[i], rhsArgSorts[i]);
+    }
+  }
+  return res;
+}

Kernel/HOL/HOL.hpp

@@ -79,6 +79,14 @@ Stack<std::pair<TermList, UnificationInference>> getProjAndImitBindings(TermList
 
 TermList createGeneralBinding(TermList head, const TermStack& sorts, unsigned& freshVar, bool surround = true);
 
+// Creates abstractions of lit as described below to be used for heuristically
+// instantiating Π terms (proxified universal quantification, see CNFOnTheFly).
+//
+// If lit is of the form s ⋈ t, where ⋈ ∈ {=,≠}, s is λ x1,...,xn. f s1,...,sk,
+// and t is λ y1,...,ym. f t1,...,tl, then w.l.o.g. we create an abstracted
+// disequality λ x. s' ≠ t for each 1 ≤ i ≤ k where s' is s with si replaced with x.
+TermStack getAbstractionTerms(Literal* lit);
+
 } // namespace HOL
 
 namespace HOL::create {
@@ -130,6 +138,7 @@ namespace HOL::create {
 namespace HOL::convert {
 
 TermList toNameless(TermList term);
+TermList toNameless(Formula* formula);
 
 inline TermList toNameless(Term* term) {
   return toNameless(TermList(term));

Kernel/Inference.cpp

@@ -929,6 +929,8 @@ std::string Kernel::ruleName(InferenceRule rule)
     return "beta-eta normalization";
   case InferenceRule::EQ_TO_DISEQ:
     return "bool equality to disequality";
+  case InferenceRule::HEURISTIC_INSTANTIATION:
+    return "heuristic instantiation";
   case InferenceRule::PRIMITIVE_INSTANTIATION:
     return "primitive instantiation";
   case InferenceRule::IMITATION:

Kernel/Inference.hpp

@@ -348,6 +348,7 @@ enum class InferenceRule : unsigned char {
   NEGATIVE_EXTENSIONALITY,
   POSITIVE_EXTENSIONALITY,
   EQ_TO_DISEQ,
+  HEURISTIC_INSTANTIATION,
   /** The next five rules can be either simplifying or generating */
   NOT_PROXY_CLAUSIFICATION,
   AND_PROXY_CLAUSIFICATION,

Kernel/Signature.hpp

@@ -661,6 +661,14 @@ class Signature
     return &_choiceSymbols;
   }
 
+  void addInstantiation(TermList inst) {
+    _instantiations.insert(inst);
+  }
+
+  DHSet<TermList>* getInstantiations() {
+    return &_instantiations;
+  }
+
   /** return the number of functions */
   unsigned functions() const { return _funs.length(); }
   /** return the number of predicates */
@@ -993,7 +1001,9 @@ class Signature
   /** Stack of type constructor symbols */  
   Stack<Symbol*> _typeCons;
 
+  // TODO(HOL): these two don't belong in the signature
   DHSet<unsigned> _choiceSymbols;
+  DHSet<TermList> _instantiations;
 
   SymbolMap _funNames;
   SymbolMap _predNames;

Saturation/PredicateSplitPassiveClauseContainers.cpp

@@ -17,6 +17,7 @@
 
 #include "Shell/Options.hpp"
 #include "Kernel/Clause.hpp"
+#include "Kernel/HOL/HOL.hpp"
 #include "Kernel/Inference.hpp"
 #include "Lib/SharedSet.hpp"
 #include "Lib/Int.hpp"
@@ -481,6 +482,65 @@ float TheoryMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigned,
   return -std::numeric_limits<float>::max();
 }
 
+unsigned numOfAppVarsAndLambdas(TermList t, unsigned lambdaWeight, unsigned appliedVarWeight)
+{
+  if (t.isVar()) {
+    return 0;
+  }
+  const Term* tt = t.term();
+
+  static DHMap<const Term*,unsigned> cache;
+  unsigned* cached;
+  if (!cache.getValuePtr(tt,cached)) {
+    return *cached;
+  }
+
+  // it's OK that the entry in cache has already been created, will only possibly ask for proper subterms
+
+  unsigned res = 0;
+
+  if (tt->isLambdaTerm()) {
+    res = lambdaWeight + numOfAppVarsAndLambdas(tt->lambdaBody(), lambdaWeight, appliedVarWeight);
+  } else if (tt->isApplication()) {
+    TermStack args;
+    auto head = HOL::getHeadAndArgs(t, args);
+    ASS(!head.isLambdaTerm()); // should be beta-reduced
+    if (head.isVar()) {
+      res += appliedVarWeight;
+    }
+    while(!args.isEmpty()){
+      res += numOfAppVarsAndLambdas(args.pop(), lambdaWeight, appliedVarWeight);
+    }
+  }
+
+  // reallocation may occur in-between, so ask for the pointer again
+  ALWAYS(cached = cache.findPtr(tt));
+  *cached = res;
+  return res;
+}
+
+HoFeaturesMultiSplitPassiveClauseContainer::HoFeaturesMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, std::string name, std::vector<std::unique_ptr<PassiveClauseContainer>> queues) :
+PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), opt.hoSplitQueueCutoffs(), opt.hoSplitQueueRatios(), opt.hoSplitQueueLayeredArrangement()),
+_lambdaWeight(opt.hoSplitQueueLambdaWeight()), _appliedVarWeight(opt.hoSplitQueueAppVarWeight()) {}
+
+float HoFeaturesMultiSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const
+{
+  // calculate the number of higher-order features (applied variable and lambdas) in the clause
+  unsigned res = 0;
+  for (const auto& lit : *cl){
+    auto [lhs, rhs] = lit->eqArgs();
+    res = res + numOfAppVarsAndLambdas(lhs, _lambdaWeight, _appliedVarWeight)
+              + numOfAppVarsAndLambdas(rhs, _lambdaWeight, _appliedVarWeight);
+  }
+  return res;
+}
+
+float HoFeaturesMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigned, const Inference& inf) const
+{
+  // from the information provided we cannot estimate the feature sadly...
+  return 0;
+}
+
 AvatarMultiSplitPassiveClauseContainer::AvatarMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, std::string name, std::vector<std::unique_ptr<PassiveClauseContainer>> queues) :
 PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), opt.avatarSplitQueueCutoffs(), opt.avatarSplitQueueRatios(), opt.avatarSplitQueueLayeredArrangement()) {}
 

Saturation/PredicateSplitPassiveClauseContainers.hpp

@@ -106,6 +106,19 @@ class TheoryMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClaus
   mutable DHMap<unsigned, std::pair<float,float>> _teoryFeatureCache;
 };
 
+class HoFeaturesMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClauseContainer
+{
+public:
+  HoFeaturesMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, std::string name, std::vector<std::unique_ptr<PassiveClauseContainer>> queues);
+
+private:
+  float evaluateFeature(Clause* cl) const override;
+  float evaluateFeatureEstimate(unsigned numPositiveLiterals, const Inference& inf) const override;
+
+  const unsigned _lambdaWeight;
+  const unsigned _appliedVarWeight;
+};
+
 class AvatarMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClauseContainer
 {
 public: