Merge pull request #301 from vprover/ahmed-fix-kboforepr-bug

Fix KBOForEPR polymorphism bug
vprover · Nov 30, 2021 · 106b95b · 106b95b
2 parents 1128390 + 1bec8ad
commit 106b95b
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 17 deletions.
diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp
@@ -130,6 +130,7 @@ Ordering* Ordering::create(Problem& prb, const Options& opt)
     // - user specified symbol weights
     // TODO fix this! 
     if(prb.getProperty()->maxFunArity()==0 
+        && prb.getProperty()->maxTypeConArity() == 0
         && !env.colorUsed
         && env.options->predicateWeights() == ""
         && env.options->functionWeights() == ""
@@ -145,6 +146,7 @@ Ordering* Ordering::create(Problem& prb, const Options& opt)
   default:
     ASSERTION_VIOLATION;
   }
+  //TODO currently do not show SKIKBO
   if (opt.showSimplOrdering()) {
     env.beginOutput();
     out->show(env.out());

diff --git a/SAT/Z3Interfacing.hpp b/SAT/Z3Interfacing.hpp
@@ -169,7 +169,7 @@ class Z3Interfacing : public PrimitiveProofRecordingSATSolver
         return true;
 
       // compare sort arguments
-      for(int i = 0; i < l.forSorts->numTypeArguments(); i++)
+      for(unsigned i = 0; i < l.forSorts->numTypeArguments(); i++)
         // sorts are perfectly shared
         if(!l.forSorts->nthArgument(i)->sameContent(r.forSorts->nthArgument(i)))
           return false;
@@ -185,7 +185,7 @@ class Z3Interfacing : public PrimitiveProofRecordingSATSolver
           : env.signature->getFunction(self.id)->name()
       );
       if(self.forSorts)
-        for(int i = 0; i < self.forSorts->numTypeArguments(); i++)
+        for(unsigned i = 0; i < self.forSorts->numTypeArguments(); i++)
           out << " " << self.forSorts->nthArgument(i)->toString();
       return out;
     }
@@ -281,7 +281,7 @@ namespace std {
       size_t operator()(SAT::Z3Interfacing::FuncOrPredId const& self) {
         unsigned hash = Lib::HashUtils::combine(self.id, self.isPredicate);
         if(self.forSorts)
-          for(int i = 0; i < self.forSorts->numTypeArguments(); i++)
+          for(unsigned i = 0; i < self.forSorts->numTypeArguments(); i++)
             hash = Lib::HashUtils::combine(hash, self.forSorts->nthArgument(i)->content());
         return hash;
       }

diff --git a/Shell/Property.cpp b/Shell/Property.cpp
@@ -66,6 +66,7 @@ Property::Property()
     _groundGoals(0),
     _maxFunArity(0),
     _maxPredArity(0),
+    _maxTypeConArity(0),
     _totalNumberOfVariables(0),
     _maxVariablesInClause(0),
     _props(0),
@@ -656,10 +657,6 @@ void Property::scan(TermList ts,bool unit,bool goal)
     return;
   }
 
-  if(ts.term()->isSort()){
-    return;
-  }
-
   ASS(ts.isTerm());
   Term* t = ts.term();
 
@@ -687,6 +684,13 @@ void Property::scan(TermList ts,bool unit,bool goal)
         break;
     }
   } else {
+    if(t->isSort()){
+      if(t->arity() > _maxTypeConArity){
+        _maxTypeConArity = t->arity();
+      }
+      return;
+    }
+
     scanForInterpreted(t);
 
     _symbolsInFormula.insert(t->functor());
@@ -719,20 +723,20 @@ void Property::scan(TermList ts,bool unit,bool goal)
       _hasLogicalProxy = true;
     }
 
-    OperatorType* type = func->fnType();
-    if(!t->isApplication() && type->typeArgsArity()){
+    if(!t->isApplication() && t->numTypeArguments() > 0){
       _hasPolymorphicSym = true;
     }
 
     int arity = t->arity();
-    for (int i = 0; i < arity; i++) {
-      scanSort(SortHelper::getArgSort(t, i));
-    }
-    scanSort(SortHelper::getResultSort(t));
 
     if (arity > _maxFunArity) {
       _maxFunArity = arity;
     }
+
+    for (int i = 0; i < arity; i++) {
+      scanSort(SortHelper::getArgSort(t, i));
+    }
+    scanSort(SortHelper::getResultSort(t));  
   }
 }
 

diff --git a/Shell/Property.hpp b/Shell/Property.hpp
@@ -187,6 +187,8 @@ class Property
   bool hasFormulas() const { return _axiomFormulas || _goalFormulas; }
   /** Maximal arity of a function in the problem */
   int maxFunArity() const { return _maxFunArity; }
+  /** Maximal arity of a type con in the problem */
+  unsigned maxTypeConArity() const { return _maxTypeConArity; }
   /** Total number of variables in problem */
   int totalNumberOfVariables() const { return _totalNumberOfVariables;}
 
@@ -303,6 +305,7 @@ class Property
   int _groundGoals;
   int _maxFunArity;
   int _maxPredArity;
+  unsigned _maxTypeConArity;
 
   /** Number of variables in this clause, used during counting */
   int _variablesInThisClause;

diff --git a/Shell/SubexpressionIterator.hpp b/Shell/SubexpressionIterator.hpp
@@ -52,10 +52,8 @@ namespace Shell {
        * we first propagate the negative polarity from the formula to its underlying
        * boolean term, and then from the boolean terms to their underlying formulas.
        *
-       * NOTE: this iterator returns sort terms as well. As of 08/07/2021, the only 
-       * use of this iterator is in Property.cpp where sorts are NOT required. 
-       * However, sorts are sub-expressions, so to keep the iterator intuitive we
-       * leave the code as is.
+       * NOTE: this iterator returns sort terms as well. As of 25/11/2021, the only 
+       * use of this iterator is in Property.cpp.
        */
       class Expression {
         public: