fixing occurs occurs check and simplifying filtering

vprover · Apr 30, 2019 · 9d3eacc · 9d3eacc
1 parent 3f8a4d8
commit 9d3eacc
Show file tree

Hide file tree

Showing 14 changed files with 80 additions and 84 deletions.
diff --git a/Indexing/SubstitutionTree.cpp b/Indexing/SubstitutionTree.cpp
@@ -819,26 +819,25 @@ SubstitutionTree::QueryResult SubstitutionTree::UnificationsIterator::next()
 
   LeafData& ld=ldIterator.next();
 
-  bool retSub, newSub;
+  bool retSub;
 
   if(usePlaceholders){
     unsigned ut = fo(nodeEntrances);
     retSub = retrieveSubstitution && (ut == FIRST_ORDER);
-    newSub = retrieveSubstitution && (ut == HIGHER_ORDER_UNDER_VAR); 
   } else {
     retSub = retrieveSubstitution;
-    newSub = false;
   }
 
-  if(newSub){
+  /*if(newSub){
     second_subst.reset();
     bool unify = second_subst.unify(placeHolderFreeQueryTerm, QUERY_BANK, ld.term, RESULT_BANK);
 
     second_subst.mark(unify);
 
     return QueryResult(make_pair(&ld, ResultSubstitution::fromSubstitution(
         &second_subst, QUERY_BANK, RESULT_BANK)), UnificationConstraintStackSP()); 
-  }else if(retSub) {
+  }else */ 
+  if(retSub) {
     Renaming normalizer;
     if(literalRetrieval) {
       normalizer.normalizeVariables(ld.literal);

diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp
@@ -817,8 +817,7 @@ class SubstitutionTree
     virtual NodeIterator getNodeIterator(IntermediateNode* n);
 
     static const unsigned FIRST_ORDER=0;
-    static const unsigned HIGHER_ORDER_UNDER_VAR=1;
-    static const unsigned HIGHER_ORDER=2;
+    static const unsigned HIGHER_ORDER=1;
 
     void createInitialBindings(Term* t);
     /**
@@ -843,7 +842,7 @@ class SubstitutionTree
     static const int NORM_RESULT_BANK=3;
 
     SUBST_CLASS subst;
-    SUBST_CLASS second_subst;
+   // SUBST_CLASS second_subst;
     VarStack svStack;
 
   private:

diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp
@@ -156,11 +156,7 @@ struct Superposition::ApplicableCombRewritesFn
     ResultSubstitutionSP rs = arg.second.substitution;
     //subsitution is a smartPtr to a ResultSubstituion object. 
     if(!rs.isEmpty()){
-      if(rs->tryGetRobSubstitution()->getMark()){
-        return pvi(getSingletonIterator(arg));
-      } else {
-        return VirtualIterator<QueryResType>::getEmpty();
-      }
+      return pvi(getSingletonIterator(arg));
     } else {
       return pvi(CombResultIterator(arg));
     }

diff --git a/Kernel/CombSubstIterator.cpp b/Kernel/CombSubstIterator.cpp
@@ -93,17 +93,23 @@ void CombSubstitution::populateTransformations(UnificationPair& up)
   }
 
   if(hoterml->isVar()){
-    Transform trs = make_pair(ELIMINATE,FIRST);
-    up.transformsLeft.push(trs);
-    return;        
+    VarSpec vs = VarSpec(hoterml->head.var(), hoterml->headInd);
+    if(!occursOrNotPure(vs, hotermr)){
+      Transform trs = make_pair(ELIMINATE,FIRST);
+      up.transformsLeft.push(trs);
+      return;        
+    }
   }
 
   // if unification is between two variables arbitrarily choose to eliminate
   // left of pair
   if(hotermr->isVar() && !hoterml->isVar()){
-    Transform trs = make_pair(ELIMINATE,SECOND);
-    up.transformsRight.push(trs);
-    return;        
+    VarSpec vs = VarSpec(hotermr->head.var(), hotermr->headInd);
+    if(!occursOrNotPure(vs, hoterml)){
+      Transform trs = make_pair(ELIMINATE,SECOND);
+      up.transformsRight.push(trs);
+      return;
+    }        
   }  
 
   if(hoterml->sameFirstOrderHead(hotermr)){
@@ -115,18 +121,12 @@ void CombSubstitution::populateTransformations(UnificationPair& up)
     return;      
   }
 
-  if(hoterml->underAppliedCombTerm() || hotermr->underAppliedCombTerm()){
-    Transform trs = make_pair(ADD_ARG,BOTH);
-    up.transformsBoth.push(trs);
-    return; 
-  }
-
-  if(hoterml->combHead() && !hoterml->underAppliedCombTerm()){
+  if(hoterml->combHead() /*&& !hoterml->underAppliedCombTerm()*/){
     AlgorithmStep as = reduceStep(hoterml);
     Transform trs = make_pair(as,FIRST);
     up.transformsLeft.push(trs);
     return;  
-  } else if(hotermr->combHead() && !hotermr->underAppliedCombTerm()){
+  } else if(hotermr->combHead() /*&& !hotermr->underAppliedCombTerm()*/){
     AlgorithmStep as = reduceStep(hotermr);
     Transform trs = make_pair(as,SECOND);
     up.transformsRight.push(trs);
@@ -176,6 +176,7 @@ void CombSubstitution::populateSide(const HOTerm_ptr hoterm, ApplyTo at, Transfo
   CALL("CombSubstitution::populateSide");
 
   //cout << "Populating for term " + hoterm->toStringWithTopLevelSorts() << endl;
+  //cout << "other is " + other->toStringWithTopLevelSorts() << endl;
 
   ASS(hoterm->varHead());
   //KX_NARROW admissable as long as var has a single argument
@@ -305,20 +306,7 @@ bool CombSubstitution::transform(Transform t, bool furtherOptions){
   }
 
   if(t.second == BOTH && t.first != ID){
-    ASS((t.first == ADD_ARG) || (t.first == DECOMP));
-
-    if(t.first == ADD_ARG){
-      unsigned freshArgSort = HSH::domain(terml->sort());
-      TermList newArg = env.signature->getDummy(_nextDummy++);
-      HOTerm_ptr fcl = HSH::createHOTerm(newArg, freshArgSort);
-      HOTerm_ptr fcr = HSH::createHOTerm(newArg, freshArgSort);
-      terml->addArg(fcl);
-      termr->addArg(fcr);
-      up->lsRight = UNDEFINED;
-      up->lsLeft = UNDEFINED;
-      up->slsRight = UNDEFINED;
-      up->slsLeft = UNDEFINED;
-    }
+    ASS(/*(t.first == ADD_ARG) ||*/ (t.first == DECOMP));
 
     if(t.first == DECOMP){
       ASS(terml->sameFirstOrderHead(termr));
@@ -342,13 +330,9 @@ bool CombSubstitution::transform(Transform t, bool furtherOptions){
     vs = t.second == FIRST ? VarSpec(terml->head.var(), terml->headInd) 
                            : VarSpec(termr->head.var(), termr->headInd);
     HOTerm_ptr ht = t.second == FIRST ? termr : terml; 
-    if(occursOrNotPure(vs, ht)){
-      succeeded =  false;
-    } else {
-      eliminate(vs, ht);
-      addToSolved(vs, ht);
-      _unificationPairs.pop();
-    }
+    eliminate(vs, ht);
+    addToSolved(vs, ht);
+    _unificationPairs.pop();
   }
 
   //split here so we can check early for failure
@@ -384,7 +368,7 @@ bool CombSubstitution::transform(Transform t, bool furtherOptions){
     }
   }
 
-  if(t.first != SPLIT && t.first != ELIMINATE && t.first != DECOMP && t.first != ADD_ARG){
+  if(t.first != SPLIT && t.first != ELIMINATE && t.first != DECOMP /*&& t.first != ADD_ARG*/){
     if(t.second == FIRST){
       transform(terml, termr, t.first);
       up->slsLeft = up->lsLeft;
@@ -418,6 +402,17 @@ void CombSubstitution::transform(HOTerm_ptr term, HOTerm_ptr other, AlgorithmSte
 
   //cout << "carrying out transformation with " + term->toString(false, true) << endl;
 
+  if(as >= I_REDUCE && as <= S_REDUCE){
+    while(term->underAppliedCombTerm()){
+      unsigned freshArgSort = HSH::domain(term->sort());
+      TermList newArg = env.signature->getDummy(_nextDummy++);
+      HOTerm_ptr fcl = HSH::createHOTerm(newArg, freshArgSort);
+      HOTerm_ptr fcr = HSH::createHOTerm(newArg, freshArgSort);
+      term->addArg(fcl);
+      other->addArg(fcr);
+    }
+  }
+
   if(as == I_REDUCE){
     ASS(term->headComb() == SS::I_COMB);
     iReduce(term);

diff --git a/Kernel/CombSubstIterator.hpp b/Kernel/CombSubstIterator.hpp
@@ -180,8 +180,8 @@ class CombSubstitution
       }
 
       PairType getPairType() {      
-        if(terml->varHead()){
-          if(termr->varHead()){
+        if(terml->isAppliedVar()){
+          if(termr->isAppliedVar()){
             if(terml->sameVarHead(termr, true)){
               return FLEX_FLEX_SAME_HEAD;
             } else {
@@ -190,9 +190,12 @@ class CombSubstitution
           } else {
             return FLEX_RIGID_LEFT;
           }
-        } else if(termr->varHead()){
+        } else if(termr->isAppliedVar()){
           return FLEX_RIGID_RIGHT;
         }
+        //<X,X> is not really a rigid-rigid term
+        //however we treat it as such because there are no transforms out of a 
+        //variable
         return RIGID_RIGID;
       }
 

diff --git a/Kernel/LookaheadLiteralSelector.cpp b/Kernel/LookaheadLiteralSelector.cpp
@@ -266,8 +266,6 @@ struct LookaheadLiteralSelector::GenIteratorIterator
       DECL_RETURN_TYPE(bool);
       OWN_RETURN_TYPE operator()(TermQueryResult tqr){
         if(tqr.substitution.isEmpty()){
-          return true;   
-        } else if(tqr.substitution->tryGetRobSubstitution()->getMark()){
           return true;
         }
         return false;

diff --git a/Kernel/MainLoop.cpp b/Kernel/MainLoop.cpp
@@ -145,7 +145,8 @@ ImmediateSimplificationEngine* MainLoop::createISE(Problem& prb, const Options&
     res->addFront(new ProxyElimination::ORIMPANDRemovalISE2());
   }
 
-  if(opt.combinatorElimination() != Options::CombElimination::AXIOMS){
+  if(opt.combinatorElimination() != Options::CombElimination::AXIOMS &&
+     opt.combinatorElimination() != Options::CombElimination::OFF){
 	  res->addFront(new ProxyElimination::CombinatorEliminationISE());
   }
   // Only add if there are distinct groups 

diff --git a/Kernel/RobSubstitution.cpp b/Kernel/RobSubstitution.cpp
@@ -64,8 +64,7 @@ const int RobSubstitution::SPECIAL_INDEX=-2;
 const int RobSubstitution::UNBOUND_INDEX=-1;
 
 const unsigned FIRST_ORDER=0;
-const unsigned HIGHER_ORDER_UNDER_VAR=1;
-const unsigned HIGHER_ORDER=2;
+const unsigned HIGHER_ORDER=1;
 
 /**
  * If @b t1 and @b t2 can possibly be unified by Robinson's unif
@@ -384,7 +383,7 @@ bool RobSubstitution::unify(TermSpec t1, TermSpec t2, unsigned& ut)
         break;
       }
       if(_doPlaceHolderChecks && containsPlaceHolderSubterm(dt2)){
-        ut = std::max(ut, HIGHER_ORDER_UNDER_VAR);
+        ut = HIGHER_ORDER;
       }
       bind(v1,dt2);
     } else if(dt2.isVar()) {
@@ -394,7 +393,7 @@ bool RobSubstitution::unify(TermSpec t1, TermSpec t2, unsigned& ut)
         break;
       }
       if(_doPlaceHolderChecks && containsPlaceHolderSubterm(dt1)){
-        ut = std::max(ut, HIGHER_ORDER_UNDER_VAR);
+        ut = HIGHER_ORDER;
       }
       bind(v2,dt1);
     } else{

diff --git a/Kernel/RobSubstitution.hpp b/Kernel/RobSubstitution.hpp
@@ -53,7 +53,7 @@ class RobSubstitution
   USE_ALLOCATOR(RobSubstitution);
 
   RobSubstitution() : _nextUnboundAvailable(0),_nextAuxAvailable(0),
-                      _doPlaceHolderChecks(false), _unified(true) {}
+                      _doPlaceHolderChecks(false){}
 
   SubstIterator matches(Literal* base, int baseIndex,
 	  Literal* instance, int instanceIndex, bool complementary);
@@ -80,7 +80,7 @@ class RobSubstitution
     _bank.reset();
     _nextAuxAvailable=0;
     _nextUnboundAvailable=0;
-    _unified = true;
+    //_unified = true;
   }
   /**
    * Bind special variable to a specified term
@@ -116,13 +116,13 @@ class RobSubstitution
     _doPlaceHolderChecks = true;
   }
 
-  void mark(bool success){
+  /*void mark(bool success){
     _unified = success;
-  }
+  }*/
 
-  bool getMark(){
+  /*bool getMark(){
     return _unified;
-  }
+  }*/
 
   /** Specifies instance of a variable (i.e. (variable, variable bank) pair) */
   struct VarSpec
@@ -311,7 +311,7 @@ class RobSubstitution
   mutable unsigned _nextUnboundAvailable;
   unsigned _nextAuxAvailable;
   bool _doPlaceHolderChecks;
-  bool _unified;
+  //bool _unified;
 
 
   class BindingBacktrackObject

diff --git a/Shell/LambdaElimination.cpp b/Shell/LambdaElimination.cpp
@@ -776,7 +776,7 @@ void LambdaElimination::process(Stack<int> _vars, Stack<unsigned> _sorts, Stack<
        if(_processing.var() == (unsigned)lambdaVar){ //an expression of the form \x.x
             unsigned iSort = env.sorts->addFunctionSort(lambdaVarSort, lambdaVarSort);
             TermList ts = addHolConstant("iCOMB", iSort, added, Signature::Symbol::I_COMB);
-            if(added && env.options->combinatorElimination() != Options::CombElimination::INFERENCE_RULES){
+            if(added && env.options->combinatorElimination() > Options::CombElimination::INFERENCE_RULES){
               addCombinatorAxiom(ts, iSort, lambdaVarSort, Signature::Symbol::I_COMB);
             }
             addToProcessed(ts, _argNums);
@@ -883,7 +883,7 @@ TermList LambdaElimination::addKComb(unsigned appliedToArg, TermList arg)
 
     bool added;
     ts = addHolConstant("kCOMB",appliedToZeroArgs, added, Signature::Symbol::K_COMB);
-    if(added && env.options->combinatorElimination() != Options::CombElimination::INFERENCE_RULES){
+    if(added && env.options->combinatorElimination() > Options::CombElimination::INFERENCE_RULES){
        addCombinatorAxiom(ts, appliedToZeroArgs, argSort, Signature::Symbol::K_COMB, HSH::domain(appliedToArg));
     }   
     TermList applied;
@@ -918,7 +918,7 @@ TermList LambdaElimination::addComb(unsigned appliedToArgs, TermList arg1, TermL
        default:
           ASSERTION_VIOLATION;
     }
-    if(added && env.options->combinatorElimination() != Options::CombElimination::INFERENCE_RULES){
+    if(added && env.options->combinatorElimination() > Options::CombElimination::INFERENCE_RULES){
         addCombinatorAxiom(ts, appliedToZeroArgs, arg1sort, comb, arg2sort, arg3sort);
     }
 

diff --git a/Shell/Options.cpp b/Shell/Options.cpp
@@ -1120,7 +1120,7 @@ void Options::Options::init()
 
       _combinatorElimination = ChoiceOptionValue<CombElimination>("combinator_elimination","combelim",
                                                                    CombElimination::AXIOMS,
-                                                                   {"axioms","inference_rules","both"});
+                                                                   {"off","inference_rules", "axioms","both"});
       _combinatorElimination.description=
       "Turns on a set of inference rules used to eliminate "
       "SKI combinator from clauses. An example rule is: \n"

diff --git a/Shell/Options.hpp b/Shell/Options.hpp
@@ -372,8 +372,9 @@ class Options
     * dealt with by inference rules or both
     */
   enum class CombElimination : unsigned int {
-    AXIOMS = 0,
+    OFF = 0,
     INFERENCE_RULES = 1,
+    AXIOMS = 2,
     BOTH = 3    
   };
 

diff --git a/Testprob b/Testprob
@@ -1,3 +1,9 @@
-tff(a,type, i : ($rat * $rat) > $rat).
-tff(a,axiom, ![X:$rat, Y:$rat]:i(X, Y) =  X).
-tff(a,conjecture, ![X:$rat, Y:$rat] : (X = i(X,Y))).
+tff(a,type, isSon : ($i * $i) > $o).
+tff(a,type, isGrandson : ($i * $i) > $o).
+tff(a,type, ahmed : $i).
+tff(a,type, ali : $i).
+tff(a,type, zayd : $i).
+tff(ax1, axiom, ![X:$i, Y:$i, Z:$i]: (isSon(X, Y) & isSon(Y, Z)  =>  isGrandson(X,Z))).
+tff(ax2, axiom, isSon(ahmed, ali)).
+tff(ax2, axiom, isSon(ali, zayd)).
+tff(conj, conjecture, isGrandson(ahmed,zayd)).
diff --git a/Testprob9 b/Testprob9
@@ -1,13 +1,12 @@
-%thf(a,type, a : $i).
 %thf(a,type, iCOM : $i > $i).
 %thf(a,type, kCOM : ($i > $i) > $i > $i > $i).
-thf(a, type, a : $i).
-thf(a, type, b : $i).
-thf(a, type, c : $i).
-thf(a, type, f : $i > $i).
-thf(a, type, g : $i > $i).
-thf(a, type, h : $i > $i).
+%thf(a, type, a : $i).
+%thf(a, type, b : $i).
+%thf(a, type, c : $i).
+%thf(a, type, f : $i > $i).
+%thf(a, type, g : $i > $i).
+%thf(a, type, h : $i > $i).
 %thf(a, axiom, (![X:$i > $i, Y:$i] : ((kCOM @ X @ Y) = X))).
-thf(a, axiom, ![X: $i] : ((f @ X) = a ) ).
-thf(a, axiom, ![Y: $i > $i] : ((f @ ( Y @ b)) = c ) ).
-thf(a, conjecture, a = c).
+%thf(a, axiom, ![X: $i] : ((f @ X) = a ) ).
+thf(a, conjecture, ?[Y: $i] : (Y =  ((^[X] : X) @ Y ))).
+%thf(a, conjecture, a = c).