From 57722c892910a388c39c9c8f519542496b3d07f6 Mon Sep 17 00:00:00 2001 From: Ahmed Bhayat Date: Thu, 25 Nov 2021 09:31:02 +0000 Subject: [PATCH 1/6] fixing bug whereby KBOforEPR was tried incorrectly in the presence of not 0-ary type constructors --- Shell/Property.cpp | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/Shell/Property.cpp b/Shell/Property.cpp index aba2240da2..8a05c5784c 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -656,10 +656,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 +683,16 @@ void Property::scan(TermList ts,bool unit,bool goal) break; } } else { + int arity = t->arity(); + + if (arity > _maxFunArity) { + _maxFunArity = arity; + } + + if(t->isSort()){ + return; + } + scanForInterpreted(t); _symbolsInFormula.insert(t->functor()); @@ -724,15 +730,10 @@ void Property::scan(TermList ts,bool unit,bool goal) _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; - } } } From 3de6ab687df7fca14647d9701f69cc3f32a77284 Mon Sep 17 00:00:00 2001 From: Ahmed Bhayat Date: Thu, 25 Nov 2021 10:06:27 +0000 Subject: [PATCH 2/6] fixing comments, updating implementation --- Kernel/Ordering.cpp | 2 ++ Shell/Property.cpp | 19 ++++++++++++------- Shell/Property.hpp | 3 +++ Shell/SubexpressionIterator.hpp | 6 ++---- 4 files changed, 19 insertions(+), 11 deletions(-) diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp index 56d4baf646..66fd8b2b9c 100644 --- 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/Shell/Property.cpp b/Shell/Property.cpp index 8a05c5784c..4206467d52 100644 --- 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), @@ -683,13 +684,9 @@ void Property::scan(TermList ts,bool unit,bool goal) break; } } else { - int arity = t->arity(); - - if (arity > _maxFunArity) { - _maxFunArity = arity; - } - if(t->isSort()){ + if(t->arity() > _maxTypeConArity) + _maxTypeConArity = t->arity(); return; } @@ -725,15 +722,23 @@ void Property::scan(TermList ts,bool unit,bool goal) _hasLogicalProxy = true; } + // TODO change this to use Term::numOfTypeArgs() once + // Micahel's PR is merged OperatorType* type = func->fnType(); if(!t->isApplication() && type->typeArgsArity()){ _hasPolymorphicSym = true; } + int arity = t->arity(); + + if (arity > _maxFunArity) { + _maxFunArity = arity; + } + for (int i = 0; i < arity; i++) { scanSort(SortHelper::getArgSort(t, i)); } - scanSort(SortHelper::getResultSort(t)); + scanSort(SortHelper::getResultSort(t)); } } diff --git a/Shell/Property.hpp b/Shell/Property.hpp index 471cc6b9eb..d1257db7bd 100644 --- 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 */ + int 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; + int _maxTypeConArity; /** Number of variables in this clause, used during counting */ int _variablesInThisClause; diff --git a/Shell/SubexpressionIterator.hpp b/Shell/SubexpressionIterator.hpp index 04ec2c4449..2e5de03cba 100644 --- 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: From f8b211ae8ce414841f0b2b786e936a38e647a1ec Mon Sep 17 00:00:00 2001 From: Ahmed Bhayat Date: Thu, 25 Nov 2021 21:59:57 +0000 Subject: [PATCH 3/6] improving indentation --- Shell/Property.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Shell/Property.cpp b/Shell/Property.cpp index 4206467d52..93b810db50 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -685,8 +685,9 @@ void Property::scan(TermList ts,bool unit,bool goal) } } else { if(t->isSort()){ - if(t->arity() > _maxTypeConArity) - _maxTypeConArity = t->arity(); + if(t->arity() > _maxTypeConArity){ + _maxTypeConArity = t->arity(); + } return; } From 57f4567f11dacfe59b141d29e4dc2cc7b47e6adc Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 30 Nov 2021 12:26:30 +0100 Subject: [PATCH 4/6] one warning --- Shell/Property.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Shell/Property.hpp b/Shell/Property.hpp index d1257db7bd..ab804eaf08 100644 --- a/Shell/Property.hpp +++ b/Shell/Property.hpp @@ -188,7 +188,7 @@ class Property /** Maximal arity of a function in the problem */ int maxFunArity() const { return _maxFunArity; } /** Maximal arity of a type con in the problem */ - int maxTypeConArity() const { return _maxTypeConArity; } + unsigned maxTypeConArity() const { return _maxTypeConArity; } /** Total number of variables in problem */ int totalNumberOfVariables() const { return _totalNumberOfVariables;} @@ -305,7 +305,7 @@ class Property int _groundGoals; int _maxFunArity; int _maxPredArity; - int _maxTypeConArity; + unsigned _maxTypeConArity; /** Number of variables in this clause, used during counting */ int _variablesInThisClause; From 3be915406afe5acc913bb404da4ea772d5f6c955 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 30 Nov 2021 12:34:02 +0100 Subject: [PATCH 5/6] fix TODO --- Shell/Property.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Shell/Property.cpp b/Shell/Property.cpp index 93b810db50..293cd2b61e 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -723,10 +723,7 @@ void Property::scan(TermList ts,bool unit,bool goal) _hasLogicalProxy = true; } - // TODO change this to use Term::numOfTypeArgs() once - // Micahel's PR is merged - OperatorType* type = func->fnType(); - if(!t->isApplication() && type->typeArgsArity()){ + if(!t->isApplication() && t->numTypeArguments() > 0){ _hasPolymorphicSym = true; } From 1bec8ad2551f9e5ffda975290022d26f358ab140 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 30 Nov 2021 12:34:18 +0100 Subject: [PATCH 6/6] one other warning (from Michael) --- SAT/Z3Interfacing.hpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/SAT/Z3Interfacing.hpp b/SAT/Z3Interfacing.hpp index 49592b4c14..f5a8c250d5 100644 --- 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; }