From 6b5c0f7d7d4e454f7eb3a1ca8ede68a1844084c7 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Fri, 8 Dec 2023 10:22:02 +0000 Subject: [PATCH] do not consider {inequality,general} splitting as naming a formula --- Kernel/Signature.hpp | 2 ++ Shell/GeneralSplitting.cpp | 2 +- Shell/InequalitySplitting.cpp | 4 ++-- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 307aa7469..e1971b528 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -429,7 +429,9 @@ class Signature unsigned addSkolemTypeCon(unsigned arity,const char* suffix = 0); unsigned addFreshPredicate(unsigned arity, const char* prefix, const char* suffix = 0); unsigned addSkolemPredicate(unsigned arity,const char* suffix = 0); + // add a predicate naming a sub-formula - if you are not sure, use `addFreshPredicate` unsigned addNamePredicate(unsigned arity); + // same as `addNamePredicate`, but produces a function of Boolean sort unsigned addNameFunction(unsigned arity); void addEquality(); unsigned getApp(); diff --git a/Shell/GeneralSplitting.cpp b/Shell/GeneralSplitting.cpp index cc18b91ce..c333fb0e6 100644 --- a/Shell/GeneralSplitting.cpp +++ b/Shell/GeneralSplitting.cpp @@ -227,7 +227,7 @@ bool GeneralSplitting::apply(Clause*& cl, UnitList*& resultStack) } - unsigned namingPred=env.signature->addNamePredicate(minDeg); + unsigned namingPred=env.signature->addFreshPredicate(minDeg, "sQ", "gsp"); OperatorType* npredType = OperatorType::getPredicateType(minDeg, argSorts.begin()); env.signature->getPredicate(namingPred)->setType(npredType); diff --git a/Shell/InequalitySplitting.cpp b/Shell/InequalitySplitting.cpp index 47cbc2531..451cdaeb1 100644 --- a/Shell/InequalitySplitting.cpp +++ b/Shell/InequalitySplitting.cpp @@ -157,11 +157,11 @@ Literal* InequalitySplitting::splitLiteral(Literal* lit, UnitInputType inpType, unsigned fun; OperatorType* type; if(!_appify){ - fun=env.signature->addNamePredicate(vars.size() + 1); + fun=env.signature->addFreshPredicate(vars.size() + 1, "sQ", "ins"); type = OperatorType::getPredicateType({srt}, vars.size()); } else { srt = AtomicSort::arrowSort(srt, AtomicSort::boolSort()); - fun=env.signature->addNameFunction(vars.size()); + fun=env.signature->addFreshFunction(vars.size(), "sQ", "ins"); type = OperatorType::getConstantsType(srt, vars.size()); }