Review

vprover · Apr 23, 2024 · 79fd6d0 · 79fd6d0
1 parent 35dd7f4
commit 79fd6d0
Show file tree

Hide file tree

Showing 10 changed files with 70 additions and 71 deletions.
diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp
@@ -54,7 +54,7 @@ using namespace Indexing;
 using namespace Saturation;
 
 template<bool applyVSubst>
-struct ForwardDemodulation::Applicator : SubstApplicator {
+struct Applicator : SubstApplicator {
   Applicator(ResultSubstitution* subst, const RobSubstitution& vSubst) : subst(subst), vSubst(vSubst) {}
   TermList operator()(unsigned v) const override {
     auto res = subst->applyToBoundResult(v);
@@ -167,14 +167,11 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
         auto subs = qr.unifier;
         ASS(subs->isIdentityOnQueryWhenResultBound());
 
-        ScopedPtr<SubstApplicator> appl;
-        if (lhs.isVar()) {
-          appl = new Applicator<true>(subs.ptr(), subst);
-        } else {
-          appl = new Applicator<false>(subs.ptr(), subst);
-        }
+        Applicator<true> varSubst(subs.ptr(), subst);
+        Applicator<false> notVarSubst(subs.ptr(), subst);
+        auto appl = lhs.isVar() ? (SubstApplicator*)&varSubst : (SubstApplicator*)&notVarSubst;
 
-        if (!preordered && (_preorderedOnly || !ordering.isGreater(AppliedTerm(trm),AppliedTerm(rhs,appl.ptr(),true)))) {
+        if (!preordered && (_preorderedOnly || !ordering.isGreater(AppliedTerm(trm),AppliedTerm(rhs,appl,true)))) {
           // if (ordering.compare(AppliedTerm(trm),AppliedTerm(rhs,&appl,true))==Ordering::GREATER) {
           //   USER_ERROR("is greater " + trm.toString() + " " + subs->applyToBoundResult(rhs).toString());
           // }

diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp
@@ -36,8 +36,6 @@ class ForwardDemodulation
   void detach() override;
   bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override = 0;
 protected:
-  template<bool> struct Applicator;
-
   bool _preorderedOnly;
   bool _encompassing;
   DemodulationHelper _helper;

diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp
@@ -60,18 +60,18 @@ class KBO::State
   }
 
   template<bool unidirectional>
-  Result traverseLex(const AppliedTerm& t1, const AppliedTerm& t2);
+  Result traverseLex(AppliedTerm t1, AppliedTerm t2);
   template<bool unidirectional>
-  Result traverseNonLex(const AppliedTerm& t1, const AppliedTerm& t2);
+  Result traverseNonLex(AppliedTerm t1, AppliedTerm t2);
 
-  template<int coef, bool varsOnly> void traverse(const AppliedTerm& tt);
+  template<int coef, bool varsOnly> void traverse(AppliedTerm tt);
 
-  Result result(const AppliedTerm& t1, const AppliedTerm& t2);
+  Result result(AppliedTerm t1, AppliedTerm t2);
 protected:
   template<int coef> void recordVariable(unsigned var);
 
   bool checkVars() const { return _negNum <= 0; }
-  Result innerResult(const AppliedTerm& t1, const AppliedTerm& t2);
+  Result innerResult(TermList t1, TermList t2);
   Result applyVariableCondition(Result res)
   {
     if(_posNum>0 && (res==LESS || res==LESS_EQ || res==EQUAL)) {
@@ -102,7 +102,7 @@ class KBO::State
  * traverse(Term*,int) for both terms/literals in case their
  * top functors are different.)
  */
-Ordering::Result KBO::State::result(const AppliedTerm& t1, const AppliedTerm& t2)
+Ordering::Result KBO::State::result(AppliedTerm t1, AppliedTerm t2)
 {
   Result res;
   if(_weightDiff) {
@@ -129,9 +129,9 @@ Ordering::Result KBO::State::result(const AppliedTerm& t1, const AppliedTerm& t2
   return res;
 }
 
-Ordering::Result KBO::State::innerResult(const AppliedTerm& tl1, const AppliedTerm& tl2)
+Ordering::Result KBO::State::innerResult(TermList tl1, TermList tl2)
 {
-  ASS(!TermList::sameTopFunctor(tl1.term,tl2.term));
+  ASS(!TermList::sameTopFunctor(tl1,tl2));
 
   if(_posNum>0 && _negNum>0) {
     return INCOMPARABLE;
@@ -141,17 +141,17 @@ Ordering::Result KBO::State::innerResult(const AppliedTerm& tl1, const AppliedTe
   if(_weightDiff) {
     res=_weightDiff>0 ? GREATER : LESS;
   } else {
-    if(tl1.term.isVar()) {
+    if(tl1.isVar()) {
       ASS_EQ(_negNum,0);
       res=LESS;
-    } else if(tl2.term.isVar()) {
+    } else if(tl2.isVar()) {
       ASS_EQ(_posNum,0);
       res=GREATER;
-    } else if(tl1.term.term()->isSort()){
-      res=_kbo.compareTypeConPrecedences(tl1.term.term()->functor(), tl2.term.term()->functor());
+    } else if(tl1.term()->isSort()){
+      res=_kbo.compareTypeConPrecedences(tl1.term()->functor(), tl2.term()->functor());
       ASS_REP(res==GREATER || res==LESS, res);//precedence ordering must be total
     } else {
-      res=_kbo.compareFunctionPrecedences(tl1.term.term()->functor(), tl2.term.term()->functor());
+      res=_kbo.compareFunctionPrecedences(tl1.term()->functor(), tl2.term()->functor());
       ASS_REP(res==GREATER || res==LESS, res);//precedence ordering must be total
     }
   }
@@ -182,7 +182,7 @@ void KBO::State::recordVariable(unsigned var)
 }
 
 template<int coef, bool varsOnly>
-void KBO::State::traverse(const AppliedTerm& tt)
+void KBO::State::traverse(AppliedTerm tt)
 {
   static_assert(coef==1 || coef==-1);
 
@@ -232,7 +232,7 @@ void KBO::State::traverse(const AppliedTerm& tt)
 }
 
 template<bool unidirectional>
-Ordering::Result KBO::State::traverseLex(const AppliedTerm& tl1, const AppliedTerm& tl2)
+Ordering::Result KBO::State::traverseLex(AppliedTerm tl1, AppliedTerm tl2)
 {
   ASS(tl1.term.isTerm() && tl2.term.isTerm());
   auto t1 = tl1.term.term();
@@ -278,7 +278,7 @@ Ordering::Result KBO::State::traverseLex(const AppliedTerm& tl1, const AppliedTe
     AppliedTerm s(*ss,tl1.applicator,ssAboveVar);
     AppliedTerm t(*tt,tl2.applicator,ttAboveVar);
 
-    if(s==t) {
+    if(s.equalsShallow(t)) {
       //if content is the same, neither weightDiff nor varDiffs would change
       continue;
     }
@@ -351,7 +351,7 @@ Ordering::Result KBO::State::traverseLex(const AppliedTerm& tl1, const AppliedTe
         traverse<1,unidirectional>(s);
         traverse<-1,unidirectional>(t);
         if(_lexResult==EQUAL) {
-          _lexResult=innerResult(s, t);
+          _lexResult=innerResult(s.term, t.term);
           lexValidDepth=depth;
           ASS(_lexResult!=EQUAL);
           ASS(_lexResult!=GREATER_EQ);
@@ -371,7 +371,7 @@ Ordering::Result KBO::State::traverseLex(const AppliedTerm& tl1, const AppliedTe
 }
 
 template<bool unidirectional>
-Ordering::Result KBO::State::traverseNonLex(const AppliedTerm& tl1, const AppliedTerm& tl2)
+Ordering::Result KBO::State::traverseNonLex(AppliedTerm tl1, AppliedTerm tl2)
 {
   traverse<1,unidirectional>(tl1);
   traverse<-1,unidirectional>(tl2);
@@ -804,9 +804,9 @@ Ordering::Result KBO::compare(TermList tl1, TermList tl2) const
   return compare(AppliedTerm(tl1),AppliedTerm(tl2));
 }
 
-Ordering::Result KBO::compare(AppliedTerm&& tl1, AppliedTerm&& tl2) const
+Ordering::Result KBO::compare(AppliedTerm tl1, AppliedTerm tl2) const
 {
-  if(tl1==tl2) {
+  if(tl1.equalsShallow(tl2)) {
     return EQUAL;
   }
   if(tl1.term.isVar()) {
@@ -843,9 +843,9 @@ Ordering::Result KBO::compare(AppliedTerm&& tl1, AppliedTerm&& tl2) const
   return res;
 }
 
-Ordering::Result KBO::isGreaterOrEq(AppliedTerm&& tl1, AppliedTerm&& tl2) const
+Ordering::Result KBO::isGreaterOrEq(AppliedTerm tl1, AppliedTerm tl2) const
 {
-  if (tl1 == tl2) {
+  if (tl1.equalsShallow(tl2)) {
     return EQUAL;
   }
   if (tl1.term.isVar()) {
@@ -915,7 +915,7 @@ Ordering::Result KBO::isGreaterOrEq(AppliedTerm&& tl1, AppliedTerm&& tl2) const
   return res;
 }
 
-bool KBO::isGreater(AppliedTerm&& lhs, AppliedTerm&& rhs) const
+bool KBO::isGreater(AppliedTerm lhs, AppliedTerm rhs) const
 {
   return isGreaterOrEq(std::move(lhs),std::move(rhs))==GREATER;
 }
@@ -934,7 +934,7 @@ int KBO::symbolWeight(const Term* t) const
   return _funcWeights.symbolWeight(t);
 }
 
-unsigned KBO::computeWeight(const AppliedTerm& tt) const
+unsigned KBO::computeWeight(AppliedTerm tt) const
 {
   if (tt.term.isVar()) {
     return _funcWeights._specialWeights._variableWeight;

diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp
@@ -156,12 +156,12 @@ class KBO
   using PrecedenceOrdering::compare;
   Result compare(TermList tl1, TermList tl2) const override;
 
-  Result compare(AppliedTerm&& t1, AppliedTerm&& t2) const override;
-  bool isGreater(AppliedTerm&& t1, AppliedTerm&& t2) const override;
+  Result compare(AppliedTerm t1, AppliedTerm t2) const override;
+  bool isGreater(AppliedTerm t1, AppliedTerm t2) const override;
 
 protected:
-  Result isGreaterOrEq(AppliedTerm&& tt1, AppliedTerm&& tt2) const;
-  unsigned computeWeight(const AppliedTerm& tt) const;
+  Result isGreaterOrEq(AppliedTerm tt1, AppliedTerm tt2) const;
+  unsigned computeWeight(AppliedTerm tt) const;
 
   Result comparePredicates(Literal* l1, Literal* l2) const override;
 

diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp
@@ -83,9 +83,9 @@ Ordering::Result LPO::compare(TermList tl1, TermList tl2) const
   return compare(AppliedTerm(tl1),AppliedTerm(tl2));
 }
 
-Ordering::Result LPO::compare(AppliedTerm&& tl1, AppliedTerm&& tl2) const
+Ordering::Result LPO::compare(AppliedTerm tl1, AppliedTerm tl2) const
 {
-  if(tl1==tl2) {
+  if(tl1.equalsShallow(tl2)) {
     return EQUAL;
   }
   if(tl1.term.isVar()) {
@@ -95,12 +95,12 @@ Ordering::Result LPO::compare(AppliedTerm&& tl1, AppliedTerm&& tl2) const
   return clpo(tl1, tl2);
 }
 
-bool LPO::isGreater(AppliedTerm&& lhs, AppliedTerm&& rhs) const
+bool LPO::isGreater(AppliedTerm lhs, AppliedTerm rhs) const
 {
   return lpo(std::move(lhs),std::move(rhs))==GREATER;
 }
 
-Ordering::Result LPO::clpo(const AppliedTerm& tl1, const AppliedTerm& tl2) const
+Ordering::Result LPO::clpo(AppliedTerm tl1, AppliedTerm tl2) const
 {
   ASS(tl1.term.isTerm());
   if(tl2.term.isVar()) {
@@ -130,7 +130,7 @@ Ordering::Result LPO::clpo(const AppliedTerm& tl1, const AppliedTerm& tl2) const
  * All TermList* are stored in reverse order (by design in Term),
  * hence the weird pointer arithmetic
  */
-Ordering::Result LPO::cMA(const AppliedTerm& s, const AppliedTerm& t, const TermList* tl, unsigned arity) const
+Ordering::Result LPO::cMA(AppliedTerm s, AppliedTerm t, const TermList* tl, unsigned arity) const
 {
   for (unsigned i = 0; i < arity; i++) {
     switch(clpo(s, AppliedTerm(*(tl - i),t))) {
@@ -148,7 +148,7 @@ Ordering::Result LPO::cMA(const AppliedTerm& s, const AppliedTerm& t, const Term
   return GREATER;
 }
 
-Ordering::Result LPO::cLMA(const AppliedTerm& s, const AppliedTerm& t, const TermList* sl, const TermList* tl, unsigned arity) const
+Ordering::Result LPO::cLMA(AppliedTerm s, AppliedTerm t, const TermList* sl, const TermList* tl, unsigned arity) const
 {
   for (unsigned i = 0; i < arity; i++) {
     switch(compare(AppliedTerm(*(sl - i),s), AppliedTerm(*(tl - i),t))) {
@@ -167,7 +167,7 @@ Ordering::Result LPO::cLMA(const AppliedTerm& s, const AppliedTerm& t, const Ter
   return EQUAL;
 }
 
-Ordering::Result LPO::cAA(const AppliedTerm& s, const AppliedTerm& t, const TermList* sl, const TermList* tl, unsigned arity1, unsigned arity2) const
+Ordering::Result LPO::cAA(AppliedTerm s, AppliedTerm t, const TermList* sl, const TermList* tl, unsigned arity1, unsigned arity2) const
 {
   switch (alpha(sl, arity1, s, t)) {
   case GREATER:
@@ -180,7 +180,7 @@ Ordering::Result LPO::cAA(const AppliedTerm& s, const AppliedTerm& t, const Term
 }
 
 // greater iff some exists s_i in sl such that s_i >= t
-Ordering::Result LPO::alpha(const TermList* sl, unsigned arity, const AppliedTerm& s, const AppliedTerm& t) const
+Ordering::Result LPO::alpha(const TermList* sl, unsigned arity, AppliedTerm s, AppliedTerm t) const
 {
   ASS(t.term.isTerm());
   for (unsigned i = 0; i < arity; i++) {
@@ -192,9 +192,9 @@ Ordering::Result LPO::alpha(const TermList* sl, unsigned arity, const AppliedTer
 }
 
 // unidirectional comparison function (returns correct result if tt1 > tt2 or tt1 = tt2)
-Ordering::Result LPO::lpo(const AppliedTerm& tt1, const AppliedTerm& tt2) const
+Ordering::Result LPO::lpo(AppliedTerm tt1, AppliedTerm tt2) const
 {
-  if(tt1==tt2) {
+  if(tt1.equalsShallow(tt2)) {
     return EQUAL;
   }
   if (tt1.term.isVar()) {
@@ -218,7 +218,7 @@ Ordering::Result LPO::lpo(const AppliedTerm& tt1, const AppliedTerm& tt2) const
   }
 }
 
-Ordering::Result LPO::lexMAE(const AppliedTerm& s, const AppliedTerm& t, const TermList* sl, const TermList* tl, unsigned arity) const
+Ordering::Result LPO::lexMAE(AppliedTerm s, AppliedTerm t, const TermList* sl, const TermList* tl, unsigned arity) const
 {
   for (unsigned i = 0; i < arity; i++) {
     switch (lpo(AppliedTerm(*(sl - i),s), AppliedTerm(*(tl - i),t))) {
@@ -236,7 +236,7 @@ Ordering::Result LPO::lexMAE(const AppliedTerm& s, const AppliedTerm& t, const T
 }
 
 // greater if s is greater than every term in tl
-Ordering::Result LPO::majo(const AppliedTerm& s, const AppliedTerm& t, const TermList* tl, unsigned arity) const
+Ordering::Result LPO::majo(AppliedTerm s, AppliedTerm t, const TermList* tl, unsigned arity) const
 {
   for (unsigned i = 0; i < arity; i++) {
     if (lpo(s, AppliedTerm(*(tl - i), t)) != GREATER) {

diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp
@@ -46,23 +46,23 @@ class LPO
 
   using PrecedenceOrdering::compare;
   Result compare(TermList tl1, TermList tl2) const override;
-  Result compare(AppliedTerm&& tl1, AppliedTerm&& tl2) const override;
+  Result compare(AppliedTerm tl1, AppliedTerm tl2) const override;
   void showConcrete(std::ostream&) const override;
 
-  bool isGreater(AppliedTerm&& tl1, AppliedTerm&& tl2) const override;
+  bool isGreater(AppliedTerm tl1, AppliedTerm tl2) const override;
 
 protected:
   Result comparePredicates(Literal* l1, Literal* l2) const override;
   Result comparePrecedences(const Term* t1, const Term* t2) const;
 
-  Result cLMA(const AppliedTerm& s, const AppliedTerm& t, const TermList* sl, const TermList* tl, unsigned arity) const;
-  Result cMA(const AppliedTerm& s, const AppliedTerm& t, const TermList* tl, unsigned arity) const;
-  Result cAA(const AppliedTerm& s, const AppliedTerm& t, const TermList* sl, const TermList* tl, unsigned arity1, unsigned arity2) const;
-  Result alpha(const TermList* sl, unsigned arity, const AppliedTerm& s, const AppliedTerm& t) const;
-  Result clpo(const AppliedTerm& tl1, const AppliedTerm& tl2) const;
-  Result lpo(const AppliedTerm& tl1, const AppliedTerm& tl2) const;
-  Result lexMAE(const AppliedTerm& s, const AppliedTerm& t, const TermList* sl, const TermList* tl, unsigned arity) const;
-  Result majo(const AppliedTerm& s, const AppliedTerm& t, const TermList* tl, unsigned arity) const;
+  Result cLMA(AppliedTerm s, AppliedTerm t, const TermList* sl, const TermList* tl, unsigned arity) const;
+  Result cMA(AppliedTerm s, AppliedTerm t, const TermList* tl, unsigned arity) const;
+  Result cAA(AppliedTerm s, AppliedTerm t, const TermList* sl, const TermList* tl, unsigned arity1, unsigned arity2) const;
+  Result alpha(const TermList* sl, unsigned arity, AppliedTerm s, AppliedTerm t) const;
+  Result clpo(AppliedTerm tl1, AppliedTerm tl2) const;
+  Result lpo(AppliedTerm tl1, AppliedTerm tl2) const;
+  Result lexMAE(AppliedTerm s, AppliedTerm t, const TermList* sl, const TermList* tl, unsigned arity) const;
+  Result majo(AppliedTerm s, AppliedTerm t, const TermList* tl, unsigned arity) const;
 };
 
 }

diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp
@@ -272,7 +272,7 @@ Ordering::Result PrecedenceOrdering::compare(Literal* l1, Literal* l2) const
   return comparePredicates(l1, l2);
 } // PrecedenceOrdering::compare()
 
-bool Ordering::containsVar(const AppliedTerm& s, TermList var)
+bool Ordering::containsVar(AppliedTerm s, TermList var)
 {
   ASS(var.isVar());
   if (!s.aboveVar) {
@@ -291,12 +291,12 @@ bool Ordering::containsVar(const AppliedTerm& s, TermList var)
   return false;
 }
 
-Ordering::Result Ordering::compare(AppliedTerm&& lhs, AppliedTerm&& rhs) const
+Ordering::Result Ordering::compare(AppliedTerm lhs, AppliedTerm rhs) const
 {
   NOT_IMPLEMENTED;
 }
 
-bool Ordering::isGreater(AppliedTerm&& lhs, AppliedTerm&& rhs) const
+bool Ordering::isGreater(AppliedTerm lhs, AppliedTerm rhs) const
 {
   NOT_IMPLEMENTED;
 }

diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp
@@ -64,10 +64,10 @@ class Ordering
    * @b t1 and @b t2 */
   virtual Result compare(TermList t1,TermList t2) const = 0;
   /** Same as @b compare, for applied (substituted) terms. */
-  virtual Result compare(AppliedTerm&& t1, AppliedTerm&& t2) const;
+  virtual Result compare(AppliedTerm t1, AppliedTerm t2) const;
   /** Optimised function used for checking that @b t1 is greater than @b t2,
    * under some substitutions captured by @b AppliedTerm. */
-  virtual bool isGreater(AppliedTerm&& t1, AppliedTerm&& t2) const;
+  virtual bool isGreater(AppliedTerm t1, AppliedTerm t2) const;
 
   virtual void show(std::ostream& out) const = 0;
 
@@ -108,7 +108,7 @@ class Ordering
 
   Result compareEqualities(Literal* eq1, Literal* eq2) const;
 
-  static bool containsVar(const AppliedTerm& s, TermList var);
+  static bool containsVar(AppliedTerm s, TermList var);
 
 private:
   void createEqualityComparator();