Preprocessing extensions

Kernel/Inference.cpp

@@ -560,6 +560,8 @@ std::string Kernel::ruleName(InferenceRule rule)
     return "closure";
   case InferenceRule::FLATTEN:
     return "flattening";
+  case InferenceRule::MINISCOPE:
+    return "miniscoping";
   case InferenceRule::FOOL_ELIMINATION:
     return "fool elimination";
   case InferenceRule::FOOL_ITE_DEFINITION:
@@ -673,6 +675,8 @@ std::string Kernel::ruleName(InferenceRule rule)
     return "unused predicate definition removal";
   case InferenceRule::PURE_PREDICATE_REMOVAL:
     return "pure predicate removal";
+  case InferenceRule::PREDICATE_ELIMINATION:
+    return "predicate elimination";
   case InferenceRule::INEQUALITY_SPLITTING:
     return "inequality splitting";
   case InferenceRule::INEQUALITY_SPLITTING_NAME_INTRODUCTION:

Kernel/Inference.hpp

@@ -189,8 +189,8 @@ enum class InferenceRule : unsigned char {
 //      * f <=> ginto an implication f => g or g => f
 //      */
 //     HALF_EQUIV,
-//     /** miniscoping */
-//     MINISCOPE,
+  /** miniscoping: pushing quantifiers inside to minimize their scope */
+  MINISCOPE,
   /** normalizing inference */
   THEORY_NORMALIZATION,
   ALASCA_INTEGER_TRANSFORMATION,
@@ -389,6 +389,8 @@ enum class InferenceRule : unsigned char {
   UNUSED_PREDICATE_DEFINITION_REMOVAL,
   /** pure predicate removal */
   PURE_PREDICATE_REMOVAL,
+  /** predicate elimination by exhaustive resolution (preprocessing) */
+  PREDICATE_ELIMINATION,
   /** inequality splitting */
   INEQUALITY_SPLITTING,
   /** inequality splitting name introduction */

Makefile

@@ -366,6 +366,7 @@ VS_OBJ = Shell/AnswerLiteralManager.o\
          Shell/InterpretedNormalizer.o\
          Shell/LispLexer.o\
          Shell/LispParser.o\
+         Shell/Miniscoping.o\
          Shell/Naming.o\
          Shell/NNF.o\
          Shell/Normalisation.o\
@@ -392,6 +393,7 @@ VS_OBJ = Shell/AnswerLiteralManager.o\
          Shell/TheoryFlattening.o\
          Shell/TweeGoalTransformation.o\
          Shell/BlockedClauseElimination.o\
+         Shell/PredicateElimination.o\
          Shell/Token.o\
          Shell/TPTPPrinter.o\
          Shell/UIHelper.o\

Shell/BlockedClauseElimination.cpp

@@ -28,6 +28,7 @@
 #include "Lib/DHSet.hpp"
 #include "Lib/DHMap.hpp"
 #include "Lib/BinaryHeap.hpp"
+#include "Lib/Random.hpp"
 #include "Debug/TimeProfiling.hpp"
 #include "Lib/IntUnionFind.hpp"
 
@@ -98,6 +99,12 @@ void BlockedClauseElimination::apply(Problem& prb)
 
   // cout << "Queue initialized" << endl;
 
+  // under randomized preprocessing, each discovered blocking is with this probability
+  // ignored: the candidate is dropped and never re-enqueued, so the clause can only
+  // still get blocked via one of its other literals (the loss is monotone; to be tuned)
+  constexpr double RPR_SKIP_PROB = 0.1;
+  bool rpr = env.options->randomizedPreprocessing();
+
   while (!queue.isEmpty()) {
     Candidate* cand = queue.pop();
     ClWrapper* clw = cand->clw;
@@ -137,6 +144,9 @@ void BlockedClauseElimination::apply(Problem& prb)
     }
 
     // resolves to tautology with all partners -- blocked!
+    if (rpr && Random::getDouble(0.0,1.0) < RPR_SKIP_PROB) {
+      goto next_candidate;
+    }
     if (env.options->showPreprocessing()) {
       cout << "[PP] Blocked clause[" << cand->litIdx << "]: " << cl->toString() << endl;
     }

Shell/EqResWithDeletion.cpp

@@ -12,6 +12,9 @@
  * Implements class EqResWithDeletion.
  */
 
+#include "Lib/Environment.hpp"
+#include "Lib/Random.hpp"
+
 #include "Kernel/Clause.hpp"
 #include "Kernel/Inference.hpp"
 #include "Kernel/Problem.hpp"
@@ -120,6 +123,13 @@ bool EqResWithDeletion::scan(Literal* lit)
   static Shell::SynthesisALManager* synthMan = static_cast<Shell::SynthesisALManager*>(Shell::SynthesisALManager::getInstance());
 
   if(lit->isEquality() && lit->isNegative()) {
+    // under randomized preprocessing, each candidate inequality is with this probability
+    // left un-resolved for this pass; a pass in which all candidates get skipped ends
+    // the per-clause fixpoint, so skipped inequalities can survive in the result (to be tuned)
+    constexpr double RPR_SKIP_PROB = 0.2;
+    if(env.options->randomizedPreprocessing() && Random::getDouble(0.0,1.0) < RPR_SKIP_PROB) {
+      return false;
+    }
     TermList t0=*lit->nthArgument(0);
     TermList t1=*lit->nthArgument(1);
     if( t0.isVar() && !t1.containsSubterm(t0) && (!_ansLit || !t1.isTerm() || synthMan->isComputableOrVar(t1.term()) || !isFreeVariableOf(_ansLit,t0.var()))) {

Shell/FunctionDefinition.cpp

@@ -18,6 +18,7 @@
 #include "Debug/Assertion.hpp"
 #include "Lib/Allocator.hpp"
 #include "Lib/Environment.hpp"
+#include "Lib/Random.hpp"
 #include "Lib/ScopedLet.hpp"
 
 #include "Kernel/Clause.hpp"
@@ -182,8 +183,16 @@ bool FunctionDefinition::removeUnusedDefinitions(UnitList*& units, Problem* prb)
     }
   }
 
+  // under randomized preprocessing, each unused definition is with this probability
+  // kept in the problem instead of being removed (to be tuned)
+  constexpr double RPR_SKIP_PROB = 0.5; // unused usually don't matter than much (TPTP eval)
+  bool rpr = env.options->randomizedPreprocessing();
+
   while(toDo.isNonEmpty()) {
     Def* d=toDo.pop();
+    if(rpr && Random::getDouble(0.0,1.0) < RPR_SKIP_PROB) {
+      continue; // d->mark stays UNTOUCHED and the definition gets reinserted below
+    }
     d->mark=Def::REMOVED;
     ASS_EQ(d->defCl->length(), 1);
     ASS_EQ(occCounter[d->fun], 1);
@@ -241,11 +250,20 @@ void FunctionDefinition::reverse(Def* def){
  */
 bool FunctionDefinition::removeAllDefinitions(UnitList*& units)
 {
+  // under randomized preprocessing, each discovered definition is with this probability
+  // ignored, i.e. kept in the problem as a plain clause and never unfolded (to be tuned)
+  constexpr double RPR_SKIP_PROB = 0.2; // TPTP eval was much more sensitive to these
+  bool rpr = env.options->randomizedPreprocessing();
+
   UnitList::DelIterator scanIterator(units);
   while(scanIterator.hasNext()) {
     Clause* cl=static_cast<Clause*>(scanIterator.next());
     ASS(cl->isClause());
     Def* d=isFunctionDefinition(cl);
+    if(d && rpr && Random::getDouble(0.0,1.0) < RPR_SKIP_PROB) {
+      delete d;
+      d = 0;
+    }
     if(d) {
       d->defCl=cl;
       bool inserted = false;