From 3e3ed11b9ff677885f71437a2024ebc454cee954 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Thu, 9 Nov 2017 14:58:47 +0100 Subject: [PATCH] OperatorType class for types of predicate and function symbols; perfectly hashed --- FMB/DefinitionIntroduction.hpp | 2 +- FMB/FiniteModelMultiSorted.cpp | 16 +- FMB/FiniteModelMultiSorted.hpp | 2 +- FMB/FunctionRelationshipInference.cpp | 2 +- FMB/Monotonicity.cpp | 6 +- FMB/SortInference.cpp | 14 +- Forwards.hpp | 1 + Inferences/TermAlgebraReasoning.cpp | 8 +- InstGen/ModelPrinter.cpp | 8 +- Kernel/Signature.cpp | 20 +-- Kernel/Signature.hpp | 20 +-- Kernel/SortHelper.cpp | 4 +- Kernel/SortHelper.hpp | 2 +- Kernel/Sorts.cpp | 207 ++++++++++---------------- Kernel/Sorts.hpp | 153 ++++++++++++------- Kernel/Term.cpp | 6 +- Kernel/Theory.cpp | 28 ++-- Kernel/Theory.hpp | 6 +- Lib/Hash.hpp | 16 ++ Parse/SMTLIB.cpp | 16 +- Parse/SMTLIB.hpp | 2 +- Parse/SMTLIB2.cpp | 21 ++- Parse/TPTP.cpp | 24 +-- Shell/AnswerExtractor.cpp | 4 +- Shell/EqualityProxy.cpp | 6 +- Shell/EqualityProxy.hpp | 2 +- Shell/FOOLElimination.cpp | 6 +- Shell/GeneralSplitting.cpp | 2 +- Shell/Grounding.cpp | 2 +- Shell/InequalitySplitting.cpp | 2 +- Shell/Naming.cpp | 2 +- Shell/NewCNF.cpp | 12 +- Shell/Property.cpp | 4 +- Shell/Skolem.cpp | 4 +- Shell/TPTPPrinter.cpp | 8 +- Shell/TermAlgebra.cpp | 2 +- Shell/TermAlgebra.hpp | 3 +- Shell/TheoryAxioms.cpp | 2 +- Shell/UIHelper.cpp | 2 +- 39 files changed, 329 insertions(+), 318 deletions(-) diff --git a/FMB/DefinitionIntroduction.hpp b/FMB/DefinitionIntroduction.hpp index 8fd0ca1a96..104bdfefef 100644 --- a/FMB/DefinitionIntroduction.hpp +++ b/FMB/DefinitionIntroduction.hpp @@ -133,7 +133,7 @@ namespace FMB { if(!_introduced.find(t)){ unsigned newConstant = env.signature->addFreshFunction(0,"fmbdef"); unsigned srt = SortHelper::getResultSort(t); - env.signature->getFunction(newConstant)->setType(new FunctionType(srt)); + env.signature->getFunction(newConstant)->setType(OperatorType::getConstantsType(srt)); Term* c = Term::createConstant(newConstant); _introduced.insert(t,c); if(term==t) retC=c; diff --git a/FMB/FiniteModelMultiSorted.cpp b/FMB/FiniteModelMultiSorted.cpp index eb592db239..61a9905383 100644 --- a/FMB/FiniteModelMultiSorted.cpp +++ b/FMB/FiniteModelMultiSorted.cpp @@ -70,7 +70,7 @@ FiniteModelMultiSorted::FiniteModelMultiSorted(DHMap sizes) : unsigned arity=env.signature->functionArity(f); f_offsets[f]=offsets; - FunctionType* sig = env.signature->getFunction(f)->fnType(); + OperatorType* sig = env.signature->getFunction(f)->fnType(); unsigned add = _sizes.get(sig->result()); for(unsigned i=0;iarg(i)); } @@ -84,7 +84,7 @@ FiniteModelMultiSorted::FiniteModelMultiSorted(DHMap sizes) : unsigned arity=env.signature->predicateArity(p); p_offsets[p]=offsets; - PredicateType* sig = env.signature->getPredicate(p)->predType(); + OperatorType* sig = env.signature->getPredicate(p)->predType(); unsigned add = 1; for(unsigned i=0;iarg(i)); } @@ -126,7 +126,7 @@ void FiniteModelMultiSorted::addFunctionDefinition(unsigned f, const DArraygetFunction(f)->fnType(); + OperatorType* sig = env.signature->getFunction(f)->fnType(); for(unsigned i=0;iarg(i)); @@ -160,7 +160,7 @@ void FiniteModelMultiSorted::addPredicateDefinition(unsigned p, const DArraygetPredicate(p)->predType(); + OperatorType* sig = env.signature->getPredicate(p)->predType(); for(unsigned i=0;iarg(i)); @@ -279,7 +279,7 @@ vstring FiniteModelMultiSorted::toString() if(!printIntroduced && env.signature->getFunction(f)->introduced()) continue; vstring name = env.signature->functionName(f); - FunctionType* sig = env.signature->getFunction(f)->fnType(); + OperatorType* sig = env.signature->getFunction(f)->fnType(); modelStm << "tff("<sortName(sig->arg(i)); @@ -366,7 +366,7 @@ vstring FiniteModelMultiSorted::toString() if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue; vstring name = env.signature->predicateName(f); - PredicateType* sig = env.signature->getPredicate(f)->predType(); + OperatorType* sig = env.signature->getPredicate(f)->predType(); modelStm << "tff("<sortName(sig->arg(i)); @@ -450,7 +450,7 @@ unsigned FiniteModelMultiSorted::evaluateGroundTerm(Term* term) if(args[i]==0) USER_ERROR("Could not evaluate "+term->toString()); } - FunctionType* sig = env.signature->getFunction(term->functor())->fnType(); + OperatorType* sig = env.signature->getFunction(term->functor())->fnType(); unsigned var = f_offsets[term->functor()]; unsigned mult = 1; for(unsigned i=0;igetPredicate(lit->functor())->predType(); + OperatorType* sig = env.signature->getPredicate(lit->functor())->predType(); unsigned var = p_offsets[lit->functor()]; unsigned mult = 1; for(unsigned i=0;isortName(srt)+"_"+Lib::Int::toString(c); unsigned f = env.signature->addFreshFunction(0,name.c_str()); - env.signature->getFunction(f)->setType(new FunctionType(srt)); + env.signature->getFunction(f)->setType(OperatorType::getConstantsType(srt)); t = Term::createConstant(f); _domainConstants.insert(pair,t); _domainConstantsRev.insert(t,pair); diff --git a/FMB/FunctionRelationshipInference.cpp b/FMB/FunctionRelationshipInference.cpp index 4b36184e13..c5c467b646 100644 --- a/FMB/FunctionRelationshipInference.cpp +++ b/FMB/FunctionRelationshipInference.cpp @@ -217,7 +217,7 @@ ClauseList* FunctionRelationshipInference::getCheckingClauses() unsigned initial_functions = env.signature->functions(); for(unsigned f=0; f < initial_functions; f++){ - FunctionType* ftype = env.signature->getFunction(f)->fnType(); + OperatorType* ftype = env.signature->getFunction(f)->fnType(); unsigned ret_srt = ftype->result(); unsigned arity = env.signature->functionArity(f); diff --git a/FMB/Monotonicity.cpp b/FMB/Monotonicity.cpp index ed5ea4adf6..76950ea87e 100644 --- a/FMB/Monotonicity.cpp +++ b/FMB/Monotonicity.cpp @@ -196,7 +196,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, DArray< if(!isMonotonic[s]){ vstring name = "sortPredicate_"+env.sorts->sortName(s); unsigned p = env.signature->addFreshPredicate(1,name.c_str()); - env.signature->getPredicate(p)->setType(new PredicateType({s})); + env.signature->getPredicate(p)->setType(OperatorType::getPredicateType({s})); sortPredicates[s] = p; } else{ sortPredicates[s]=0; } @@ -236,7 +236,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, DArray< // Next the non-empty constraint unsigned skolemConstant = env.signature->addSkolemFunction(0); - env.signature->getFunction(skolemConstant)->setType(new FunctionType(s)); + env.signature->getFunction(skolemConstant)->setType(OperatorType::getConstantsType(s)); Literal* psk = Literal::create1(p,true,TermList(Term::createConstant(skolemConstant))); Clause* nonEmpty = new(1) Clause(1,Unit::InputType::AXIOM, new Inference(Inference::INPUT)); (*nonEmpty)[0] = psk; @@ -351,7 +351,7 @@ void Monotonicity::addSortFunctions(bool withMon, ClauseList*& clauses) if(!isMonotonic[s]){ vstring name = "sortFunction_"+env.sorts->sortName(s); unsigned f = env.signature->addFreshFunction(1,name.c_str()); - env.signature->getFunction(f)->setType(new FunctionType({s},s)); + env.signature->getFunction(f)->setType(OperatorType::getFunctionType({s},s)); sortFunctions[s] = f; } else{ sortFunctions[s]=0; } diff --git a/FMB/SortInference.cpp b/FMB/SortInference.cpp index 4621f27530..76e52a9fe1 100644 --- a/FMB/SortInference.cpp +++ b/FMB/SortInference.cpp @@ -117,7 +117,7 @@ void SortInference::doInference() for(unsigned f=0;ffunctions();f++){ if(_del_f[f]) continue; unsigned arity = env.signature->functionArity(f); - FunctionType* ftype = env.signature->getFunction(f)->fnType(); + OperatorType* ftype = env.signature->getFunction(f)->fnType(); //cout << env.signature->functionName(f) << " : " << env.sorts->sortName(ftype->result()) << endl;; unsigned dsort = (*_sig->vampireToDistinct.get(ftype->result()))[0]; //cout << env.signature->functionName(f) << " : " << dsort << endl; @@ -134,7 +134,7 @@ void SortInference::doInference() unsigned dsort = (*_sig->vampireToDistinct.get(s))[0]; if(_sig->sortedConstants[dsort].isEmpty()){ unsigned fresh = env.signature->addFreshFunction(0,"fmbFreshConstant"); - env.signature->getFunction(fresh)->setType(new FunctionType(s)); + env.signature->getFunction(fresh)->setType(OperatorType::getConstantsType(s)); _sig->sortedConstants[dsort].push(fresh); } } @@ -145,7 +145,7 @@ void SortInference::doInference() for(unsigned f=0;ffunctions();f++){ if(f < _del_f.size() && _del_f[f]) continue; unsigned arity = env.signature->functionArity(f); - FunctionType* ftype = env.signature->getFunction(f)->fnType(); + OperatorType* ftype = env.signature->getFunction(f)->fnType(); _sig->functionSignatures[f].ensure(arity+1); for(unsigned i=0;ifunctionSignatures[f][i]=(*_sig->vampireToDistinct.get(ftype->arg(i)))[0]; @@ -156,7 +156,7 @@ void SortInference::doInference() for(unsigned p=1;ppredicates();p++){ if(_del_p[p]) continue; unsigned arity = env.signature->predicateArity(p); - PredicateType* ptype = env.signature->getPredicate(p)->predType(); + OperatorType* ptype = env.signature->getPredicate(p)->predType(); _sig->predicateSignatures[p].ensure(arity); for(unsigned i=0;ipredicateSignatures[p][i]=(*_sig->vampireToDistinct.get(ptype->arg(i)))[0]; @@ -504,7 +504,7 @@ void SortInference::doInference() _sig->functionSignatures[f][arity] = rangeSort; Signature::Symbol* fnSym = env.signature->getFunction(f); - FunctionType* fnType = fnSym->fnType(); + OperatorType* fnType = fnSym->fnType(); if(parentSet[rangeSort]){ #if VDEBUG //cout << "FUNCTION " << env.signature->functionName(f) << endl; @@ -563,7 +563,7 @@ void SortInference::doInference() unsigned srt = freshMap.get(f); unsigned dsrt = _sig->parents[srt]; unsigned vsrt = (*_sig->distinctToVampire.get(dsrt))[0]; - env.signature->getFunction(f)->setType(new FunctionType(vsrt)); + env.signature->getFunction(f)->setType(OperatorType::getConstantsType(vsrt)); env.signature->getFunction(f)->markIntroduced(); } @@ -583,7 +583,7 @@ void SortInference::doInference() _sig->predicateSignatures[p].ensure(arity); Signature::Symbol* prSym = env.signature->getPredicate(p); - PredicateType* prType = prSym->predType(); + OperatorType* prType = prSym->predType(); for(unsigned i=0;i class RCPtr; template class SingleParamEvent; template class DArray; template class Stack; +template class Vector; template class List; template class BinaryHeap; template class SharedSet; diff --git a/Inferences/TermAlgebraReasoning.cpp b/Inferences/TermAlgebraReasoning.cpp index 24987c39c6..b8044f062b 100644 --- a/Inferences/TermAlgebraReasoning.cpp +++ b/Inferences/TermAlgebraReasoning.cpp @@ -212,7 +212,7 @@ namespace Inferences { unsigned int _index; // between 0 and _length Literal* _lit; Clause* _clause; - FunctionType* _type; // type of f + OperatorType* _type; // type of f }; struct InjectivityGIE::SubtermEqualityFn @@ -252,7 +252,7 @@ namespace Inferences { Literal *lit = (*c)[i]; if (sameConstructorsEquality(lit) && lit->isPositive()) { if (lit->nthArgument(0)->term()->arity() == 1) { - FunctionType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType(); + OperatorType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType(); Literal *newlit = Literal::createEquality(true, *lit->nthArgument(0)->term()->nthArgument(0), *lit->nthArgument(1)->term()->nthArgument(0), @@ -273,7 +273,7 @@ namespace Inferences { Literal *lit = (*c)[i]; if (sameConstructorsEquality(lit) && !lit->polarity()) { unsigned arity = lit->nthArgument(0)->term()->arity(); - FunctionType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType(); + OperatorType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType(); for (unsigned j = 0; j < arity; j++) { Literal *l = Literal::createEquality(true, *lit->nthArgument(0)->term()->nthArgument(j), @@ -303,7 +303,7 @@ namespace Inferences { for (int i = length - 1; i >= 0; i--) { if (litCondition(c, i)) { Literal *lit = (*c)[i]; - FunctionType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType(); + OperatorType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType(); unsigned oldLength = c->length(); unsigned arity = lit->nthArgument(0)->term()->arity(); unsigned newLength = oldLength + arity - 1; diff --git a/InstGen/ModelPrinter.cpp b/InstGen/ModelPrinter.cpp index 8471671c6a..8761332f0c 100644 --- a/InstGen/ModelPrinter.cpp +++ b/InstGen/ModelPrinter.cpp @@ -57,12 +57,12 @@ bool ModelPrinter::haveNonDefaultSorts() unsigned funs = env.signature->functions(); for(unsigned i=0; igetFunction(i)->fnType(); + OperatorType* type = env.signature->getFunction(i)->fnType(); if(!type->isAllDefault()) { return false; } } unsigned preds = env.signature->predicates(); for(unsigned i=1; igetPredicate(i)->predType(); + OperatorType* type = env.signature->getPredicate(i)->predType(); if(!type->isAllDefault()) { return false; } } return true; @@ -206,7 +206,7 @@ void ModelPrinter::generateNewInstances(Literal* base, TermStack& domain, DHSet< static DArray args; static DArray variables; static DArray nextIndexes; - PredicateType* predType = env.signature->getPredicate(base->functor())->predType(); + OperatorType* predType = env.signature->getPredicate(base->functor())->predType(); args.ensure(arity); variables.ensure(arity); @@ -343,7 +343,7 @@ void ModelPrinter::analyzeEqualityAndPopulateDomain() vstring firstTermStr = firstTerm.toString(); unsigned eqClassSort = SortHelper::getResultSort(firstTerm.term()); unsigned reprFunc = env.signature->addStringConstant(firstTermStr); - FunctionType* reprType = new FunctionType(eqClassSort); + OperatorType* reprType = OperatorType::getConstantsType(eqClassSort); env.signature->getFunction(reprFunc)->setType(reprType); TermList reprTerm = TermList(Term::create(reprFunc, 0, 0)); _rewrites.insert(firstTerm, reprTerm); diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index b73503f9ba..b09bb069f7 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -155,7 +155,7 @@ void Signature::Symbol::addToDistinctGroup(unsigned group,unsigned this_number) * should be different from the default type, this function must be * called before any call to @c fnType() or @c predType(). */ -void Signature::Symbol::setType(BaseType* type) +void Signature::Symbol::setType(OperatorType* type) { CALL("Signature::Symbol::setType"); ASS(!_type); @@ -168,7 +168,7 @@ void Signature::Symbol::setType(BaseType* type) * This can be unsafe so should only be used when you know it is safe to * change the type i.e. nothing yet relies on the type of this symbol */ -void Signature::Symbol::forceType(BaseType* type) +void Signature::Symbol::forceType(OperatorType* type) { CALL("Signature::Symbol::forceType"); if(_type){ delete _type; } @@ -181,14 +181,14 @@ void Signature::Symbol::forceType(BaseType* type) * If the @c setType() function was not called before, the function * symbol is assigned a default type. */ -FunctionType* Signature::Symbol::fnType() const +OperatorType* Signature::Symbol::fnType() const { CALL("Signature::Symbol::fnType"); if (!_type) { - _type = new FunctionType(arity(), (unsigned*)0, Sorts::SRT_DEFAULT); + _type = OperatorType::getFunctionType(arity(), (unsigned*)0, Sorts::SRT_DEFAULT); } - return static_cast(_type); + return _type; } /** @@ -197,14 +197,14 @@ FunctionType* Signature::Symbol::fnType() const * If the @c setType() function was not called before, the function * symbol is assigned a default type. */ -PredicateType* Signature::Symbol::predType() const +OperatorType* Signature::Symbol::predType() const { CALL("Signature::Symbol::predType"); if (!_type) { - _type = new PredicateType(arity(), (unsigned*)0); + _type = OperatorType::getPredicateType(arity(), (unsigned*)0); } - return static_cast(_type); + return _type; } @@ -285,7 +285,7 @@ unsigned Signature::addInterpretedFunction(Interpretation interpretation, const _funs.push(sym); _funNames.insert(symbolKey, fnNum); ALWAYS(_iSymbols.insert(interpretation, fnNum)); - BaseType* fnType = Theory::getOperationType(interpretation); + OperatorType* fnType = Theory::getOperationType(interpretation); ASS(fnType->isFunctionType()); sym->setType(fnType); return fnNum; @@ -317,7 +317,7 @@ unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const _predNames.insert(symbolKey,predNum); ALWAYS(_iSymbols.insert(interpretation, predNum)); if (predNum!=0) { - BaseType* predType = Theory::getOperationType(interpretation); + OperatorType* predType = Theory::getOperationType(interpretation); ASS_REP(!predType->isFunctionType(), predType->toString()); sym->setType(predType); } diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index be3f47614e..8421e7ab29 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -89,7 +89,7 @@ class Signature /** marks term algebra constructors */ unsigned _termAlgebraCons : 1; /** Either a FunctionType of a PredicateType object */ - mutable BaseType* _type; + mutable OperatorType* _type; /** List of distinct groups the constant is a member of, all members of a distinct group should be distinct from each other */ List* _distinctGroups; /** number of times it is used in the problem */ @@ -198,10 +198,10 @@ class Signature Note that this should only be called on a constant **/ void addToDistinctGroup(unsigned group,unsigned this_number); - void setType(BaseType* type); - void forceType(BaseType* type); - FunctionType* fnType() const; - PredicateType* predType() const; + void setType(OperatorType* type); + void forceType(OperatorType* type); + OperatorType* fnType() const; + OperatorType* predType() const; CLASS_NAME(Signature::Symbol); USE_ALLOCATOR(Symbol); @@ -244,7 +244,7 @@ class Signature { CALL("IntegerSymbol"); - setType(new FunctionType(Sorts::SRT_INTEGER)); + setType(OperatorType::getConstantsType(Sorts::SRT_INTEGER)); } CLASS_NAME(Signature::IntegerSymbol); USE_ALLOCATOR(IntegerSymbol); @@ -264,7 +264,7 @@ class Signature { CALL("RationalSymbol"); - setType(new FunctionType(Sorts::SRT_RATIONAL)); + setType(OperatorType::getConstantsType(Sorts::SRT_RATIONAL)); } CLASS_NAME(Signature::RationalSymbol); USE_ALLOCATOR(RationalSymbol); @@ -284,7 +284,7 @@ class Signature { CALL("RealSymbol"); - setType(new FunctionType(Sorts::SRT_REAL)); + setType(OperatorType::getConstantsType(Sorts::SRT_REAL)); } CLASS_NAME(Signature::RealSymbol); USE_ALLOCATOR(RealSymbol); @@ -467,9 +467,9 @@ class Signature unsigned getFoolConstantSymbol(bool isTrue){ if(!_foolConstantsDefined){ _foolFalse = addFunction("$$false",0); - getFunction(_foolFalse)->setType(new FunctionType(Sorts::SRT_BOOL)); + getFunction(_foolFalse)->setType(OperatorType::getConstantsType(Sorts::SRT_BOOL)); _foolTrue = addFunction("$$true",0); - getFunction(_foolTrue)->setType(new FunctionType(Sorts::SRT_BOOL)); + getFunction(_foolTrue)->setType(OperatorType::getConstantsType(Sorts::SRT_BOOL)); _foolConstantsDefined=true; } return isTrue ? _foolTrue : _foolFalse; diff --git a/Kernel/SortHelper.cpp b/Kernel/SortHelper.cpp index f145de6f73..ea5a885708 100644 --- a/Kernel/SortHelper.cpp +++ b/Kernel/SortHelper.cpp @@ -39,7 +39,7 @@ using namespace Kernel; * Return the type of a term or a literal @c t * @author Andrei Voronkov */ -BaseType& SortHelper::getType(Term* t) +OperatorType& SortHelper::getType(Term* t) { CALL("SortHelper::getType(Term*)"); @@ -768,7 +768,7 @@ bool SortHelper::areImmediateSortsValid(Term* t) return true; } - BaseType& type = getType(t); + OperatorType& type = getType(t); unsigned arity = t->arity(); for (unsigned i=0; inthArgument(i); diff --git a/Kernel/SortHelper.hpp b/Kernel/SortHelper.hpp index 6cdbd96ff9..150fbe0ffd 100644 --- a/Kernel/SortHelper.hpp +++ b/Kernel/SortHelper.hpp @@ -77,7 +77,7 @@ class SortHelper { static bool areSortsValid(Clause* cl); static bool areImmediateSortsValid(Term* t); - static BaseType& getType(Term* t); + static OperatorType& getType(Term* t); static bool areSortsValid(Term* t, DHMap& varSorts); private: diff --git a/Kernel/Sorts.cpp b/Kernel/Sorts.cpp index 059041b421..f98f7cab17 100644 --- a/Kernel/Sorts.cpp +++ b/Kernel/Sorts.cpp @@ -223,122 +223,101 @@ const vstring& Sorts::sortName(unsigned idx) const } // Sorts::sortName /** - * Initialise a base type. If @c sorts is is NULL, all arguments will be - * initalised by the default sort, otherwise, by sorts from the array @c sorts + * Pre-initialise an OperatorKey. + * + * If @c sorts is is NULL, all arguments will be initalized by the default sort, + * otherwise, by sorts from the array @c sorts * @author Andrei Voronkov */ -BaseType::BaseType(unsigned arity, const unsigned* sorts) +OperatorType::OperatorKey* OperatorType::setupKey(unsigned arity, const unsigned* sorts) { - CALL("BaseType::BaseType"); + CALL("OperatorType::setupKey(unsigned,const unsigned*)"); - if (!arity) { - _args = 0; - return; - } + OperatorKey* key = OperatorKey::allocate(arity+1); - _args = SortVector::allocate(arity); if (!sorts) { // initialise all argument types to the default type for (unsigned i = 0; i < arity; i++) { - (*_args)[i] = Sorts::SRT_DEFAULT; + (*key)[i] = Sorts::SRT_DEFAULT; + } + } else { + // initialise all the argument types to those taken from sorts + for (unsigned i = 0; i < arity; i++) { + (*key)[i] = sorts[i]; } - return; - } - // initialise all the argument types to thos taken from sorts - for (unsigned i = 0; i < arity; i++) { - (*_args)[i] = sorts[i]; } -} // BaseType::BaseType + return key; +} /** - * Initialise a base type from an initializer list of sorts. + * Pre-initialise an OperatorKey from an initializer list of sorts. */ -BaseType::BaseType(std::initializer_list sorts) +OperatorType::OperatorKey* OperatorType::setupKey(std::initializer_list sorts) { - CALL("BaseType::BaseType"); + CALL("OperatorType::setupKey(std::initializer_list)"); - if (sorts.size() == 0) { - _args = 0; - return; - } + OperatorKey* key = OperatorKey::allocate(sorts.size()+1); - _args = SortVector::allocate(sorts.size()); - // initialise all the argument types to thos taken from sorts + // initialise all the argument types to those taken from sorts unsigned i = 0; for (auto sort : sorts) { - (*_args)[i++] = sort; + (*key)[i++] = sort; } -} // BaseType::BaseType + + return key; +} /** - * Destrory the type and deallocate its arguments, if any - * @author Andrei Voronkov - */ -BaseType::~BaseType() + * Pre-initialise an OperatorKey from unsing a uniform range. + */ +OperatorType::OperatorKey* OperatorType::setupKeyUniformRange(unsigned arity, unsigned argsSort) { - CALL("BaseType::~BaseType"); + CALL("OperatorType::setupKeyUniformRange"); + + OperatorKey* key = OperatorKey::allocate(arity+1); - if (_args) { - _args->deallocate(); + static Stack argSorts; + argSorts.reset(); + for (unsigned i=0; i(*this).result() != - static_cast(o).result()) { - return false; - } - } - unsigned len = arity(); - if (len != o.arity()) { - return false; - } - for (unsigned i=0; i < len; i++) { - if (arg(i) != o.arg(i)) { - return false; - } + OperatorType* resultType; + if (_operatorTypes.find(key,resultType)) { + key->deallocate(); + return resultType; } - return true; -} // BaseType::operator== -/** + resultType = new OperatorType(key); + _operatorTypes.insert(key,resultType); + return resultType; +} + +/** * Return the string representation of arguments of a non-atomic * functional or a predicate sort in the form (t1 * ... * tn) * @since 04/05/2013 bug fix (comma was used instead of *) * @author Andrei Voronkov */ -vstring BaseType::argsToString() const +vstring OperatorType::argsToString() const { - CALL("BaseType::argsToString"); + CALL("OperatorType::argsToString"); vstring res = "("; unsigned ar = arity(); @@ -351,72 +330,38 @@ vstring BaseType::argsToString() const } res += ')'; return res; -} // BaseType::argsToString() - -/** - * Return the TPTP string representation of the predicate type. - * @author Andrei Voronkov - */ -vstring PredicateType::toString() const -{ - CALL("PredicateType::toString"); - return arity() ? argsToString() + " > $o" : "$o"; -} // PredicateType::toString +} // OperatorType::argsToString() /** - * Create a type of the form (argSort * ... * argSort) -> rangeSort - * @author Evgeny Kotelnikov + * Return the TPTP string representation of the OpertorType. */ -PredicateType* PredicateType::makeTypeUniformRange(unsigned arity, unsigned argsSort) +vstring OperatorType::toString() const { - CALL("PredicateType::makeTypeUniformRange"); - - static Stack argSorts; - argSorts.reset(); - for (unsigned i=0; i " : "") + + (isPredicateType() ? "$o" : env.sorts->sortName(result())); +} /** - * Return the TPTP string representation of the function type. + * True if all arguments of this type have sort @c str + * and so is the result sort if we are talking about a function type. * @author Andrei Voronkov */ -vstring FunctionType::toString() const +bool OperatorType::isSingleSortType(unsigned srt) const { - CALL("FunctionType::toString"); - return (arity() ? argsToString() + " > " : "") + env.sorts->sortName(result()); -} // FunctionType::toString + CALL("OperatorType::isAllDefault"); -/** - * True if this function type has the form (srt * ... * srt) -> srt - * @author Andrei Voronkov - */ -bool FunctionType::isSingleSortType(unsigned srt) const -{ - CALL("FunctionType::isSingleSortType"); + unsigned len = arity(); + for (unsigned i = 0; i rangeSort - * @author Andrei Voronkov - * @author Evgeny Kotelnikov, move to FunctionType - */ -FunctionType* FunctionType::makeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned rangeSort) -{ - CALL("FunctionType::makeTypeUniformRange"); - - static Stack argSorts; - argSorts.reset(); - for (unsigned i=0; i _sorts; /** true if there is a sort different from built-ins */ bool _hasSort; - }; -class BaseType +/** + * The OperatorType class represents the predicate and function types (which are not sorts in first-order logic). + * These are determined by their kind (either PREDICATE or FUNCTION), arity, a corresponding list of argument sorts, + * and a return sort in the case of functions. + * + * The class stores all this data in one Vector*, of length arity+1, + * where the last element is the return sort for functions and "MAX_UNSIGNED" for predicates (which distinguishes the two kinds). + * + * The objects of this class are perfectly shared (so that equal predicate / function types correspond to equal pointers) + * and are obtained via static methods (to guarantee the sharing). + */ +class OperatorType { public: - CLASS_NAME(BaseType); - USE_ALLOCATOR(BaseType); + CLASS_NAME(OperatorType); + USE_ALLOCATOR(OperatorType); - virtual ~BaseType(); +private: + typedef Vector OperatorKey; // Vector of argument sorts together with "FFFF" appended for predicates and resultSort appended for functions + OperatorKey* _key; - unsigned arg(unsigned idx) const - { - CALL("BaseType::arg"); - return (*_args)[idx]; + // constructors kept private + OperatorType(OperatorKey* key) : _key(key) {} + + /** + * Convenience functions for creating a key + */ + static OperatorKey* setupKey(unsigned arity, const unsigned* sorts=0); + static OperatorKey* setupKey(std::initializer_list sorts); + static OperatorKey* setupKeyUniformRange(unsigned arity, unsigned argsSort); + + typedef Map OperatorTypes; + // we should delete all the stored OperatorTypes inside at the end of the world, when this get destroyed + static OperatorTypes _operatorTypes; + + static OperatorType* getTypeFromKey(OperatorKey* key); + + static const unsigned PREDICATE_FLAG = std::numeric_limits::max(); + +public: + ~OperatorType() { _key->deallocate(); } + + static OperatorType* getPredicateType(unsigned arity, const unsigned* sorts=0) { + CALL("OperatorType::getPredicateType(unsigned,const unsigned*)"); + + OperatorKey* key = setupKey(arity,sorts); + (*key)[arity] = PREDICATE_FLAG; + return getTypeFromKey(key); } - unsigned arity() const { return _args ? _args->length() : 0; } - virtual bool isSingleSortType(unsigned sort) const; - bool isAllDefault() const { return isSingleSortType(Sorts::SRT_DEFAULT); } + static OperatorType* getPredicateType(std::initializer_list sorts) { + CALL("OperatorType::getPredicateType(std::initializer_list)"); - virtual bool isFunctionType() const { return false; } + OperatorKey* key = setupKey(sorts); + (*key)[sorts.size()] = PREDICATE_FLAG; + return getTypeFromKey(key); + } - bool operator==(const BaseType& o) const; - bool operator!=(const BaseType& o) const { return !(*this==o); } + static OperatorType* getPredicateTypeUniformRange(unsigned arity, unsigned argsSort) { + CALL("OperatorType::getPredicateTypeUniformRange"); - virtual vstring toString() const = 0; -protected: - BaseType(unsigned arity, const unsigned* sorts=0); - BaseType(std::initializer_list sorts); + OperatorKey* key = setupKeyUniformRange(arity,argsSort); + (*key)[arity] = PREDICATE_FLAG; + return getTypeFromKey(key); + } - vstring argsToString() const; -private: - typedef Vector SortVector; - SortVector* _args; -}; + static OperatorType* getFunctionType(unsigned arity, const unsigned* sorts, unsigned resultSort) { + CALL("OperatorType::getFunctionType"); -class PredicateType : public BaseType -{ -public: - CLASS_NAME(PredicateType); - USE_ALLOCATOR(PredicateType); + OperatorKey* key = setupKey(arity,sorts); + (*key)[arity] = resultSort; + return getTypeFromKey(key); + } - PredicateType(unsigned arity, const unsigned* argumentSorts) - : BaseType(arity, argumentSorts) {} - PredicateType(std::initializer_list sorts) : BaseType(sorts) {} + static OperatorType* getFunctionType(std::initializer_list sorts, unsigned resultSort) { + CALL("OperatorType::getFunctionType(std::initializer_list)"); - virtual vstring toString() const; + OperatorKey* key = setupKey(sorts); + (*key)[sorts.size()] = resultSort; + return getTypeFromKey(key); + } - static PredicateType* makeTypeUniformRange(unsigned arity, unsigned argsSort); -}; + static OperatorType* getFunctionTypeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned resultSort) { + CALL("OperatorType::getFunctionTypeTypeUniformRange"); -class FunctionType : public BaseType -{ -public: - CLASS_NAME(FunctionType); - USE_ALLOCATOR(FunctionType); + OperatorKey* key = setupKeyUniformRange(arity,argsSort); + (*key)[arity] = resultSort; + return getTypeFromKey(key); + } - FunctionType(unsigned arity, const unsigned* argumentSorts, unsigned resultSort) - : BaseType(arity, argumentSorts), _result(resultSort) {} - FunctionType(unsigned resultSort) - : BaseType(0, 0), _result(resultSort) {} - FunctionType(std::initializer_list argSorts, unsigned resultSort) - : BaseType(argSorts), _result(resultSort) {} + /** + * Convenience function for creating OperatorType for constants (as symbols). + * Constants are function symbols of 0 arity, so just provide the result sort. + */ + static OperatorType* getConstantsType(unsigned resultSort) { return getFunctionType(0,nullptr,resultSort); } + + unsigned arity() const { return _key->length()-1; } + + unsigned arg(unsigned idx) const + { + CALL("OperatorType::arg"); + return (*_key)[idx]; + } - unsigned result() const { return _result; } + bool isPredicateType() const { return (*_key)[arity()] == PREDICATE_FLAG; }; + bool isFunctionType() const { return (*_key)[arity()] != PREDICATE_FLAG; }; + unsigned result() const { + CALL("OperatorType::result"); + ASS(isFunctionType()); + return (*_key)[arity()]; + } - virtual bool isSingleSortType(unsigned sort) const; - virtual bool isFunctionType() const { return true; } + vstring toString() const; - virtual vstring toString() const; + bool isSingleSortType(unsigned sort) const; + bool isAllDefault() const { return isSingleSortType(Sorts::SRT_DEFAULT); } + + bool operator==(const OperatorType& o) const { return _key == o._key; } + bool operator!=(const OperatorType& o) const { return !(*this==o); } - static FunctionType* makeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned rangeSort); private: - unsigned _result; + vstring argsToString() const; }; } diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp index 0a12e2fd1d..bcc4c7c31b 100644 --- a/Kernel/Term.cpp +++ b/Kernel/Term.cpp @@ -419,8 +419,8 @@ vstring Term::headToString() const bool isPredicate = binding.isTerm() && binding.term()->isBoolean(); vstring functor = isPredicate ? env.signature->predicateName(sd->getFunctor()) : env.signature->functionName(sd->getFunctor()); - BaseType* type = isPredicate ? (BaseType*)env.signature->getPredicate(sd->getFunctor())->predType() - : (BaseType*)env.signature->getFunction(sd->getFunctor())->fnType(); + OperatorType* type = isPredicate ? env.signature->getPredicate(sd->getFunctor())->predType() + : env.signature->getFunction(sd->getFunctor())->fnType(); const IntList* variables = sd->getVariables(); vstring variablesList = ""; @@ -464,7 +464,7 @@ vstring Term::headToString() const unsigned tupleFunctor = sd->getFunctor(); TermList binding = sd->getBinding(); - FunctionType* fnType = env.signature->getFunction(tupleFunctor)->fnType(); + OperatorType* fnType = env.signature->getFunction(tupleFunctor)->fnType(); vstring symbolsList = ""; for (unsigned i = 0; i < IntList::length(symbols); i++) { diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp index 888d44396c..55b619605f 100644 --- a/Kernel/Theory.cpp +++ b/Kernel/Theory.cpp @@ -1179,8 +1179,8 @@ unsigned Theory::Tuples::getProjectionFunctor(unsigned proj, unsigned tupleSort) bool Theory::Tuples::findProjection(unsigned projFunctor, bool isPredicate, unsigned &proj) { CALL("Theory::Tuples::findProjection"); - BaseType* projType = isPredicate ? static_cast(env.signature->getPredicate(projFunctor)->predType()) - : static_cast(env.signature->getFunction(projFunctor)->fnType()); + OperatorType* projType = isPredicate ? env.signature->getPredicate(projFunctor)->predType() + : env.signature->getFunction(projFunctor)->fnType(); if (projType->arity() != 1) { return false; @@ -1213,7 +1213,7 @@ bool Theory::Tuples::findProjection(unsigned projFunctor, bool isPredicate, unsi * * @c i must be a type conversion operation. */ -FunctionType* Theory::getConversionOperationType(Interpretation i) +OperatorType* Theory::getConversionOperationType(Interpretation i) { CALL("Theory::getConversionOperationType"); @@ -1246,7 +1246,7 @@ FunctionType* Theory::getConversionOperationType(Interpretation i) default: ASSERTION_VIOLATION; } - return new FunctionType({from}, to); + return OperatorType::getFunctionType({from}, to); } Sorts::StructuredSort Theory::getInterpretedSort(StructuredSortInterpretation ssi) { @@ -1388,7 +1388,7 @@ vstring Theory::getInterpretationName(Interpretation interp) { } } -BaseType* Theory::getStructuredSortOperationType(Interpretation i) { +OperatorType* Theory::getStructuredSortOperationType(Interpretation i) { CALL("Theory::getStructuredSortOperationType"); ASS(theory->isStructuredSortInterpretation(i)); @@ -1404,13 +1404,13 @@ BaseType* Theory::getStructuredSortOperationType(Interpretation i) { switch (ssi) { case StructuredSortInterpretation::ARRAY_SELECT: - return new FunctionType({ theorySort, indexSort }, valueSort); + return OperatorType::getFunctionType({ theorySort, indexSort }, valueSort); case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - return new PredicateType({ theorySort, indexSort }); + return OperatorType::getPredicateType({ theorySort, indexSort }); case StructuredSortInterpretation::ARRAY_STORE: - return new FunctionType({ theorySort, indexSort, innerSort }, valueSort); + return OperatorType::getFunctionType({ theorySort, indexSort, innerSort }, valueSort); default: ASSERTION_VIOLATION; @@ -1424,7 +1424,7 @@ BaseType* Theory::getStructuredSortOperationType(Interpretation i) { /** * Return type of the function representing interpreted function/predicate @c i. */ -BaseType* Theory::getOperationType(Interpretation i) +OperatorType* Theory::getOperationType(Interpretation i) { CALL("Theory::getOperationType"); ASS_NEQ(i, EQUAL); @@ -1447,9 +1447,9 @@ BaseType* Theory::getOperationType(Interpretation i) domainSorts.init(arity, sort); if (isFunction(i)) { - return new FunctionType(arity, domainSorts.array(), sort); + return OperatorType::getFunctionType(arity, domainSorts.array(), sort); } else { - return new PredicateType(arity, domainSorts.array()); + return OperatorType::getPredicateType(arity, domainSorts.array()); } } @@ -1463,7 +1463,7 @@ void Theory::defineTupleTermAlgebra(unsigned arity, unsigned* sorts) { } unsigned functor = env.signature->addFreshFunction(arity, "tuple"); - FunctionType* tupleType = new FunctionType(arity, sorts, tupleSort); + OperatorType* tupleType = OperatorType::getFunctionType(arity, sorts, tupleSort); env.signature->getFunction(functor)->setType(tupleType); env.signature->getFunction(functor)->markTermAlgebraCons(); @@ -1473,10 +1473,10 @@ void Theory::defineTupleTermAlgebra(unsigned arity, unsigned* sorts) { unsigned destructor; if (projSort == Sorts::SRT_BOOL) { destructor = env.signature->addFreshPredicate(1, "proj"); - env.signature->getPredicate(destructor)->setType(new PredicateType({ tupleSort })); + env.signature->getPredicate(destructor)->setType(OperatorType::getPredicateType({ tupleSort })); } else { destructor = env.signature->addFreshFunction(1, "proj"); - env.signature->getFunction(destructor)->setType(new FunctionType({ tupleSort }, projSort)); + env.signature->getFunction(destructor)->setType(OperatorType::getFunctionType({ tupleSort }, projSort)); } destructors[i] = destructor; } diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp index b4d7e13ab7..5b0d87f590 100644 --- a/Kernel/Theory.hpp +++ b/Kernel/Theory.hpp @@ -451,8 +451,8 @@ class Theory static bool isFunction(Interpretation i); static bool isInequality(Interpretation i); static Sorts::StructuredSort getInterpretedSort(StructuredSortInterpretation ssi); - static BaseType* getOperationType(Interpretation i); - static BaseType* getStructuredSortOperationType(Interpretation i); + static OperatorType* getOperationType(Interpretation i); + static OperatorType* getStructuredSortOperationType(Interpretation i); static bool hasSingleSort(Interpretation i); static unsigned getOperationSort(Interpretation i); static bool isConversionOperation(Interpretation i); @@ -568,7 +568,7 @@ class Theory Term* representRealConstant(vstring str); private: Theory(); - static FunctionType* getConversionOperationType(Interpretation i); + static OperatorType* getConversionOperationType(Interpretation i); DHMap _arraySkolemFunctions; diff --git a/Lib/Hash.hpp b/Lib/Hash.hpp index c3546d5b27..f55cbebe86 100644 --- a/Lib/Hash.hpp +++ b/Lib/Hash.hpp @@ -55,6 +55,18 @@ struct StackHash { } }; +template +struct VectorHash { + template + static unsigned hash(const Vector& s) { + unsigned res = 2166136261u; + for (unsigned i = 0; i < s.length(); i++) { + res = HashUtils::combine(res, ElementHash::hash(s[i])); + } + return res; + } +}; + /** * Hash functions for various types. */ @@ -78,6 +90,10 @@ class Hash static unsigned hash(Stack obj) { return StackHash::hash(obj); } + template + static unsigned hash(Vector* obj) + { return VectorHash::hash(*obj); } + // Careful: using this default on structs may cause big trouble! // Even when all fields are properly initialized, there can remain "holes" // within the "sizeof" bytes containing garbage, due to alignment politics! diff --git a/Parse/SMTLIB.cpp b/Parse/SMTLIB.cpp index ef52d3bf1f..590ef4888b 100644 --- a/Parse/SMTLIB.cpp +++ b/Parse/SMTLIB.cpp @@ -306,7 +306,7 @@ void SMTLIB::doSortDeclarations() } } -BaseType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo) +OperatorType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo) { CALL("SMTLIB::getSymbolType"); @@ -323,7 +323,7 @@ BaseType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo) argSorts.push(getSort(argSortName)); } - return new FunctionType(arity, argSorts.begin(), rangeSort); + return OperatorType::getFunctionType(arity, argSorts.begin(), rangeSort); } void SMTLIB::doFunctionDeclarations() @@ -335,8 +335,8 @@ void SMTLIB::doFunctionDeclarations() FunctionInfo& fnInfo = _funcs[i]; unsigned arity = fnInfo.argSorts.size(); - BaseType* type = getSymbolType(fnInfo); - bool isPred = !type->isFunctionType(); + OperatorType* type = getSymbolType(fnInfo); + bool isPred = type->isPredicateType(); unsigned symNum; Signature::Symbol* sym; @@ -518,7 +518,7 @@ void SMTLIB::ensureArgumentSorts(bool pred, unsigned symNum, TermList* args) { CALL("SMTLIB::ensureArgumentSorts"); - BaseType* type; + OperatorType* type; if(pred) { type = env.signature->getPredicate(symNum)->predType(); } @@ -1192,7 +1192,7 @@ bool SMTLIB::tryReadDistinct(LExpr* e, Formula*& res) } bool added; - BaseType* type = PredicateType::makeTypeUniformRange(arity, sort); + OperatorType* type = OperatorType::getPredicateTypeUniformRange(arity, sort); //this is a bit of a quick hack, we need to come up with //a proper way to have a polymorphic $distinct predicate @@ -1201,7 +1201,7 @@ bool SMTLIB::tryReadDistinct(LExpr* e, Formula*& res) env.signature->getPredicate(predNum)->setType(type); } else { - BaseType* prevType = env.signature->getPredicate(predNum)->predType(); + OperatorType* prevType = env.signature->getPredicate(predNum)->predType(); if(*type==*prevType) { delete type; } @@ -1420,7 +1420,7 @@ Formula* SMTLIB::nameFormula(Formula* f, vstring fletVarName) fletVarName = StringUtils::sanitizeSuffix(fletVarName); unsigned predNum = env.signature->addFreshPredicate(varCnt, "sP", fletVarName.c_str()); - BaseType* type = new PredicateType(varCnt, argSorts.begin()); + OperatorType* type = OperatorType::getPredicateType(varCnt, argSorts.begin()); Signature::Symbol* predSym = env.signature->getPredicate(predNum); predSym->setType(type); diff --git a/Parse/SMTLIB.hpp b/Parse/SMTLIB.hpp index 022abfd269..0eff76ad04 100644 --- a/Parse/SMTLIB.hpp +++ b/Parse/SMTLIB.hpp @@ -78,7 +78,7 @@ class SMTLIB { * * This function can be called if the mode is at least DECLARE_SORTS. */ - BaseType* getSymbolType(const FunctionInfo& fnInfo); + OperatorType* getSymbolType(const FunctionInfo& fnInfo); /** * Return parsed formula. diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index 5d7bfc2516..36f574889e 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -766,14 +766,14 @@ SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& nam bool added; unsigned symNum; Signature::Symbol* sym; - BaseType* type; + OperatorType* type; if (rangeSort == Sorts::SRT_BOOL) { // predicate symNum = env.signature->addPredicate(name, argSorts.size(), added); sym = env.signature->getPredicate(symNum); - type = new PredicateType(argSorts.size(),argSorts.begin()); + type = OperatorType::getPredicateType(argSorts.size(),argSorts.begin()); LOG1("declareFunctionOrPredicate-Predicate"); } else { // proper function @@ -785,7 +785,7 @@ SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& nam sym = env.signature->getFunction(symNum); - type = new FunctionType(argSorts.size(), argSorts.begin(), rangeSort); + type = OperatorType::getFunctionType(argSorts.size(), argSorts.begin(), rangeSort); LOG1("declareFunctionOrPredicate-Function"); } @@ -978,7 +978,7 @@ TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName, unsigned functor = env.signature->addFunction(constrName, arity, added); ASS(added); - BaseType* constructorType = new FunctionType(arity, argSorts.begin(), taSort); + OperatorType* constructorType = OperatorType::getFunctionType(arity, argSorts.begin(), taSort); env.signature->getFunction(functor)->setType(constructorType); env.signature->getFunction(functor)->markTermAlgebraCons(); @@ -1001,8 +1001,8 @@ TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName, : env.signature->addFunction(destructorName, 1, added); ASS(added); - BaseType* destructorType = isPredicate ? (BaseType*) new PredicateType(1, &taSort) - : (BaseType*) new FunctionType(1, &taSort, destructorSort); + OperatorType* destructorType = isPredicate ? OperatorType::getPredicateType(1, &taSort) + : OperatorType::getFunctionType(1, &taSort, destructorSort); LOG1("build destructor "+destructorName+": "+destructorType->toString()); @@ -1296,14 +1296,14 @@ void SMTLIB2::parseLetPrepareLookup(LExpr* exp) TermList trm; if (sort == Sorts::SRT_BOOL) { unsigned symb = env.signature->addFreshPredicate(0,"sLP"); - PredicateType* type = new PredicateType(0, nullptr); + OperatorType* type = OperatorType::getPredicateType(0, nullptr); env.signature->getPredicate(symb)->setType(type); Formula* atom = new AtomicFormula(Literal::create(symb,0,true,false,nullptr)); trm = TermList(Term::createFormula(atom)); } else { unsigned symb = env.signature->addFreshFunction (0,"sLF"); - FunctionType* type = new FunctionType(0, nullptr, sort); + OperatorType* type = OperatorType::getFunctionType(0, nullptr, sort); env.signature->getFunction(symb)->setType(type); trm = TermList(Term::createConstant(symb)); @@ -1497,8 +1497,7 @@ bool SMTLIB2::parseAsUserDefinedSymbol(const vstring& id,LExpr* exp) Signature::Symbol* symbol = isTrueFun ? env.signature->getFunction(symbIdx) : env.signature->getPredicate(symbIdx); - BaseType* type = isTrueFun ? static_cast(symbol->fnType()) - : static_cast(symbol->predType()); + OperatorType* type = isTrueFun ? symbol->fnType() : symbol->predType(); unsigned arity = symbol->arity(); @@ -2044,7 +2043,7 @@ void SMTLIB2::parseRankedFunctionApplication(LExpr* exp) bool added; unsigned pred = env.signature->addPredicate(c->discriminatorName(), 1, added); ASS(added); - PredicateType* type = new PredicateType({ sort }); + OperatorType* type = OperatorType::getPredicateType({ sort }); env.signature->getPredicate(pred)->setType(type); c->addDiscriminator(pred); // this predicate is not declare for the parser as it has a reserved name diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index bda72cbd53..c7fc21d4ce 100644 --- a/Parse/TPTP.cpp +++ b/Parse/TPTP.cpp @@ -1889,10 +1889,10 @@ void TPTP::endBinding() { : env.signature->addFreshFunction (arity,name.c_str()); if (isPredicate) { - PredicateType* type = new PredicateType(arity, argSorts.begin()); + OperatorType* type = OperatorType::getPredicateType(arity, argSorts.begin()); env.signature->getPredicate(symbolNumber)->setType(type); } else { - FunctionType* type = new FunctionType(arity, argSorts.begin(), bindingSort); + OperatorType* type = OperatorType::getFunctionType(arity, argSorts.begin(), bindingSort); env.signature->getFunction(symbolNumber)->setType(type); } @@ -1954,10 +1954,10 @@ void TPTP::endTupleBinding() { unsigned symbol; if (isPredicate) { symbol = env.signature->addFreshPredicate(0, name.c_str()); - env.signature->getPredicate(symbol)->setType(new PredicateType(0, 0)); + env.signature->getPredicate(symbol)->setType(OperatorType::getPredicateType(0, 0)); } else { symbol = env.signature->addFreshFunction(0, name.c_str()); - env.signature->getFunction(symbol)->setType(new FunctionType(sort)); + env.signature->getFunction(symbol)->setType(OperatorType::getConstantsType(sort)); } IntList::push(symbol, constants); @@ -2499,7 +2499,7 @@ Formula* TPTP::createPredicateApplication(vstring name, unsigned arity) } // not equality or distinct Literal* lit = new(arity) Literal(pred,arity,true,false); - PredicateType* type = env.signature->getPredicate(pred)->predType(); + OperatorType* type = env.signature->getPredicate(pred)->predType(); bool safe = true; for (int i = arity-1;i >= 0;i--) { unsigned sort = type->arg(i); @@ -2543,7 +2543,7 @@ TermList TPTP::createFunctionApplication(vstring name, unsigned arity) } Term* t = new(arity) Term; t->makeSymbol(fun,arity); - FunctionType* type = env.signature->getFunction(fun)->fnType(); + OperatorType* type = env.signature->getFunction(fun)->fnType(); bool safe = true; for (int i = arity-1;i >= 0;i--) { unsigned sort = type->arg(i); @@ -3052,7 +3052,7 @@ void TPTP::endTff() if (!added) { USER_ERROR("Function symbol type is declared after its use: " + name); } - env.signature->getFunction(fun)->setType(new FunctionType(sortNumber)); + env.signature->getFunction(fun)->setType(OperatorType::getConstantsType(sortNumber)); return; } @@ -3099,7 +3099,7 @@ void TPTP::endTff() USER_ERROR("Predicate symbol type is declared after its use: " + name); } symbol = env.signature->getPredicate(pred); - symbol->setType(new PredicateType(arity, sorts.begin())); + symbol->setType(OperatorType::getPredicateType(arity, sorts.begin())); } else { unsigned fun = arity == 0 @@ -3109,7 +3109,7 @@ void TPTP::endTff() USER_ERROR("Function symbol type is declared after its use: " + name); } symbol = env.signature->getFunction(fun); - symbol->setType(new FunctionType(arity, sorts.begin(), returnSortNumber)); + symbol->setType(OperatorType::getFunctionType(arity, sorts.begin(), returnSortNumber)); } } // endTff @@ -3866,7 +3866,7 @@ unsigned TPTP::addIntegerConstant(const vstring& name, Set& overflow, b if (added) { overflow.insert(name); Signature::Symbol* symbol = env.signature->getFunction(fun); - symbol->setType(new FunctionType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_INTEGER)); + symbol->setType(OperatorType::getConstantsType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_INTEGER)); } else if (!overflow.contains(name)) { USER_ERROR((vstring)"Cannot use name '" + name + "' as an atom name since it collides with an integer number"); @@ -3902,7 +3902,7 @@ unsigned TPTP::addRationalConstant(const vstring& name, Set& overflow, if (added) { overflow.insert(name); Signature::Symbol* symbol = env.signature->getFunction(fun); - symbol->setType(new FunctionType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_RATIONAL)); + symbol->setType(OperatorType::getConstantsType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_RATIONAL)); } else if (!overflow.contains(name)) { USER_ERROR((vstring)"Cannot use name '" + name + "' as an atom name since it collides with an rational number"); @@ -3934,7 +3934,7 @@ unsigned TPTP::addRealConstant(const vstring& name, Set& overflow, bool if (added) { overflow.insert(name); Signature::Symbol* symbol = env.signature->getFunction(fun); - symbol->setType(new FunctionType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_REAL)); + symbol->setType(OperatorType::getConstantsType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_REAL)); } else if (!overflow.contains(name)) { USER_ERROR((vstring)"Cannot use name '" + name + "' as an atom name since it collides with an real number"); diff --git a/Shell/AnswerExtractor.cpp b/Shell/AnswerExtractor.cpp index 02a2fc1a84..7e811b4709 100644 --- a/Shell/AnswerExtractor.cpp +++ b/Shell/AnswerExtractor.cpp @@ -71,7 +71,7 @@ void AnswerExtractor::tryOutputAnswer(Clause* refutation) InterpretedLiteralEvaluator eval; unsigned p = env.signature->addFreshPredicate(1,"p"); unsigned sort = SortHelper::getResultSort(aLit.term()); - PredicateType* type = new PredicateType({sort}); + OperatorType* type = OperatorType::getPredicateType({sort}); env.signature->getPredicate(p)->setType(type); Literal* l = Literal::create1(p,true,aLit); Literal* res =0; @@ -355,7 +355,7 @@ Literal* AnswerLiteralManager::getAnswerLiteral(Formula::VarList* vars,Formula* unsigned vcnt = litArgs.size(); unsigned pred = env.signature->addFreshPredicate(vcnt,"ans"); Signature::Symbol* predSym = env.signature->getPredicate(pred); - predSym->setType(new PredicateType(sorts.size(), sorts.begin())); + predSym->setType(OperatorType::getPredicateType(sorts.size(), sorts.begin())); predSym->markAnswerPredicate(); return Literal::create(pred, vcnt, true, false, litArgs.begin()); } diff --git a/Shell/EqualityProxy.cpp b/Shell/EqualityProxy.cpp index e6519414f4..aab21d2f3b 100644 --- a/Shell/EqualityProxy.cpp +++ b/Shell/EqualityProxy.cpp @@ -180,7 +180,7 @@ void EqualityProxy::addAxioms(UnitList*& units) * equalities. */ bool EqualityProxy::getArgumentEqualityLiterals(unsigned cnt, LiteralStack& lits, - Stack& vars1, Stack& vars2, BaseType* symbolType, bool skipSortsWithoutEquality) + Stack& vars1, Stack& vars2, OperatorType* symbolType, bool skipSortsWithoutEquality) { CALL("EqualityProxy::getArgumentEqualityLiterals"); ASS_EQ(cnt, symbolType->arity()); @@ -229,7 +229,7 @@ void EqualityProxy::addCongruenceAxioms(UnitList*& units) if (arity == 0) { continue; } - FunctionType* fnType = fnSym->fnType(); + OperatorType* fnType = fnSym->fnType(); getArgumentEqualityLiterals(arity, lits, vars1, vars2, fnType, false); Term* t1 = Term::create(i, arity, vars1.begin()); Term* t2 = Term::create(i, arity, vars2.begin()); @@ -359,7 +359,7 @@ unsigned EqualityProxy::getProxyPredicate(unsigned sort) } unsigned newPred = env.signature->addFreshPredicate(2,"sQ","eqProxy"); Signature::Symbol* predSym = env.signature->getPredicate(newPred); - BaseType* predType = new PredicateType({sort, sort}); + OperatorType* predType = OperatorType::getPredicateType({sort, sort}); predSym->setType(predType); predSym->markEqualityProxy(); diff --git a/Shell/EqualityProxy.hpp b/Shell/EqualityProxy.hpp index 403191d10a..4aff572ac2 100644 --- a/Shell/EqualityProxy.hpp +++ b/Shell/EqualityProxy.hpp @@ -74,7 +74,7 @@ class EqualityProxy void addAxioms(UnitList*& units); void addCongruenceAxioms(UnitList*& units); bool getArgumentEqualityLiterals(unsigned cnt, LiteralStack& lits, Stack& vars1, - Stack& vars2, BaseType* symbolType, bool skipSortsWithoutEquality); + Stack& vars2, OperatorType* symbolType, bool skipSortsWithoutEquality); Literal* apply(Literal* lit); Literal* makeProxyLiteral(bool polarity, TermList arg0, TermList arg1, unsigned sort); diff --git a/Shell/FOOLElimination.cpp b/Shell/FOOLElimination.cpp index b933f35984..9ab4130e83 100644 --- a/Shell/FOOLElimination.cpp +++ b/Shell/FOOLElimination.cpp @@ -924,11 +924,11 @@ unsigned FOOLElimination::introduceFreshSymbol(Context context, const char* pref CALL("FOOLElimination::introduceFreshSymbol"); unsigned arity = (unsigned)sorts.size(); - BaseType* type; + OperatorType* type; if (context == FORMULA_CONTEXT) { - type = new PredicateType(arity, sorts.begin()); + type = OperatorType::getPredicateType(arity, sorts.begin()); } else { - type = new FunctionType(arity, sorts.begin(), resultSort); + type = OperatorType::getFunctionType(arity, sorts.begin(), resultSort); } unsigned symbol; diff --git a/Shell/GeneralSplitting.cpp b/Shell/GeneralSplitting.cpp index b12c43a2cc..a4e7a6f719 100644 --- a/Shell/GeneralSplitting.cpp +++ b/Shell/GeneralSplitting.cpp @@ -242,7 +242,7 @@ bool GeneralSplitting::apply(Clause*& cl, UnitList*& resultStack) unsigned namingPred=env.signature->addNamePredicate(minDeg); - BaseType* npredType = new PredicateType(minDeg, argSorts.begin()); + OperatorType* npredType = OperatorType::getPredicateType(minDeg, argSorts.begin()); env.signature->getPredicate(namingPred)->setType(npredType); if(mdvColor!=COLOR_TRANSPARENT && otherColor!=COLOR_TRANSPARENT) { diff --git a/Shell/Grounding.cpp b/Shell/Grounding.cpp index 156943ed50..2ddc398ba9 100644 --- a/Shell/Grounding.cpp +++ b/Shell/Grounding.cpp @@ -180,7 +180,7 @@ ClauseList* Grounding::getEqualityAxioms(bool otherThanReflexivity) continue; } - PredicateType* predType = env.signature->getPredicate(pred)->predType(); + OperatorType* predType = env.signature->getPredicate(pred)->predType(); args.ensure(arity); for(unsigned i=0;iaddNamePredicate(1); unsigned srt = SortHelper::getEqualityArgumentSort(lit); - BaseType* type = new PredicateType({srt}); + OperatorType* type = OperatorType::getPredicateType({srt}); Signature::Symbol* predSym = env.signature->getPredicate(predNum); predSym->setType(type); diff --git a/Shell/Naming.cpp b/Shell/Naming.cpp index fb003d173e..0f3988c7f4 100644 --- a/Shell/Naming.cpp +++ b/Shell/Naming.cpp @@ -1161,7 +1161,7 @@ Literal* Naming::getDefinitionLiteral(Formula* f, Formula::VarList* freeVars) { predArgs.push(TermList(uvar, false)); } - predSym->setType(new PredicateType(length, domainSorts.begin())); + predSym->setType(OperatorType::getPredicateType(length, domainSorts.begin())); return Literal::create(pred, length, true, false, predArgs.begin()); } diff --git a/Shell/NewCNF.cpp b/Shell/NewCNF.cpp index 160355b95d..a6afe30a02 100644 --- a/Shell/NewCNF.cpp +++ b/Shell/NewCNF.cpp @@ -556,7 +556,7 @@ TermList NewCNF::eliminateLet(Term::SpecialTermData *sd, TermList contents) IntList* symbols = sd->getTupleSymbols(); unsigned bodySort = sd->getSort(); - FunctionType* tupleType = env.signature->getFunction(tupleFunctor)->fnType(); + OperatorType* tupleType = env.signature->getFunction(tupleFunctor)->fnType(); Term* bindingTuple = binding.term()->getSpecialData()->getTupleTerm(); unsigned arity = IntList::length(symbols); @@ -595,13 +595,13 @@ TermList NewCNF::eliminateLet(Term::SpecialTermData *sd, TermList contents) IntList* symbols = sd->getTupleSymbols(); unsigned bodySort = sd->getSort(); - FunctionType* tupleType = env.signature->getFunction(tupleFunctor)->fnType(); + OperatorType* tupleType = env.signature->getFunction(tupleFunctor)->fnType(); unsigned tupleSort = tupleType->result(); ASS_EQ(tupleType->arity(), IntList::length(symbols)); unsigned tuple = env.signature->addFreshFunction(0, "tuple"); - env.signature->getFunction(tuple)->setType(new FunctionType(tupleSort)); + env.signature->getFunction(tuple)->setType(OperatorType::getConstantsType(tupleSort)); TermList tupleTerm = TermList(Term::createConstant(tuple)); @@ -740,11 +740,11 @@ TermList NewCNF::nameLetBinding(unsigned symbol, Formula::VarList* bindingVariab } if (isPredicate) { - PredicateType* type = new PredicateType(nameArity, sorts.begin()); + OperatorType* type = OperatorType::getPredicateType(nameArity, sorts.begin()); freshSymbol = env.signature->addFreshPredicate(nameArity, "lG"); env.signature->getPredicate(freshSymbol)->setType(type); } else { - FunctionType* type = new FunctionType(nameArity, sorts.begin(), nameSort); + OperatorType* type = OperatorType::getFunctionType(nameArity, sorts.begin(), nameSort); freshSymbol = env.signature->addFreshFunction(nameArity, "lG"); env.signature->getFunction(freshSymbol)->setType(type); } @@ -1095,7 +1095,7 @@ Literal* NewCNF::createNamingLiteral(Formula* f, List* free) predArgs.push(TermList(uvar, false)); } - predSym->setType(new PredicateType(length, domainSorts.begin())); + predSym->setType(OperatorType::getPredicateType(length, domainSorts.begin())); return Literal::create(pred, length, true, false, predArgs.begin()); } diff --git a/Shell/Property.cpp b/Shell/Property.cpp index 51eff89c62..521b5d673c 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -531,7 +531,7 @@ void Property::scan(Literal* lit, int polarity, unsigned cLen, bool goal) pred->markInGoal(); } - PredicateType* type = pred->predType(); + OperatorType* type = pred->predType(); for (int i=0; iarg(i)); } @@ -597,7 +597,7 @@ void Property::scan(TermList ts,bool unit,bool goal) if(goal){ func->markInGoal();} int arity = t->arity(); - FunctionType* type = func->fnType(); + OperatorType* type = func->fnType(); for (int i = 0; i < arity; i++) { scanSort(type->arg(i)); } diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index aed97529ea..d8936a8851 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -139,7 +139,7 @@ unsigned Skolem::addSkolemFunction(unsigned arity, unsigned* domainSorts, unsigned fun = env.signature->addSkolemFunction(arity, suffix); Signature::Symbol* fnSym = env.signature->getFunction(fun); - fnSym->setType(new FunctionType(arity, domainSorts, rangeSort)); + fnSym->setType(OperatorType::getFunctionType(arity, domainSorts, rangeSort)); return fun; } @@ -163,7 +163,7 @@ unsigned Skolem::addSkolemPredicate(unsigned arity, unsigned* domainSorts, const unsigned pred = env.signature->addSkolemPredicate(arity, suffix); Signature::Symbol* pSym = env.signature->getPredicate(pred); - pSym->setType(new PredicateType(arity, domainSorts)); + pSym->setType(OperatorType::getPredicateType(arity, domainSorts)); return pred; } diff --git a/Shell/TPTPPrinter.cpp b/Shell/TPTPPrinter.cpp index 3ff0b98417..15258e039b 100644 --- a/Shell/TPTPPrinter.cpp +++ b/Shell/TPTPPrinter.cpp @@ -201,7 +201,7 @@ void TPTPPrinter::outputSymbolTypeDefinitions(unsigned symNumber, bool function) Signature::Symbol* sym = function ? env.signature->getFunction(symNumber) : env.signature->getPredicate(symNumber); - BaseType* type = function ? static_cast(sym->fnType()) : static_cast(sym->predType()); + OperatorType* type = function ? sym->fnType() : sym->predType(); if(type->isAllDefault()) { return; @@ -258,13 +258,13 @@ void TPTPPrinter::ensureNecesarySorts() } unsigned i; List *_usedSorts(0); - BaseType* type; + OperatorType* type; Signature::Symbol* sym; unsigned sorts = env.sorts->count(); //check the sorts of the function symbols and collect information about used sorts for (i = 0; i < env.signature->functions(); i++) { sym = env.signature->getFunction(i); - type = static_cast(sym->fnType()); + type = sym->fnType(); unsigned arity = sym->arity(); if (arity > 0) { for (unsigned i = 0; i < arity; i++) { @@ -276,7 +276,7 @@ void TPTPPrinter::ensureNecesarySorts() //check the sorts of the predicates and collect information about used sorts for (i = 0; i < env.signature->predicates(); i++) { sym = env.signature->getPredicate(i); - type = static_cast(sym->predType()); + type = sym->predType(); unsigned arity = sym->arity(); if (arity > 0) { for (unsigned i = 0; i < arity; i++) { diff --git a/Shell/TermAlgebra.cpp b/Shell/TermAlgebra.cpp index 5220c0e852..89d655ae70 100644 --- a/Shell/TermAlgebra.cpp +++ b/Shell/TermAlgebra.cpp @@ -141,7 +141,7 @@ unsigned TermAlgebra::getSubtermPredicate() { // declare a binary predicate subterm Stack args; args.push(_sort); args.push(_sort); - env.signature->getPredicate(s)->setType(new PredicateType(args.size(),args.begin())); + env.signature->getPredicate(s)->setType(OperatorType::getPredicateType(args.size(),args.begin())); } return s; diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index 7cf024ecab..3b4f0fad6d 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -25,6 +25,7 @@ #include "Lib/List.hpp" #include "Lib/Array.hpp" #include "Lib/VString.hpp" +#include "Kernel/Sorts.hpp" namespace Shell { class TermAlgebraConstructor { @@ -59,7 +60,7 @@ namespace Shell { Lib::vstring discriminatorName(); private: - Kernel::FunctionType* _type; + Kernel::OperatorType* _type; unsigned _functor; bool _hasDiscriminator; unsigned _discriminator; diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp index b12fbc50e5..e9c997a5b8 100644 --- a/Shell/TheoryAxioms.cpp +++ b/Shell/TheoryAxioms.cpp @@ -587,7 +587,7 @@ void TheoryAxioms::addIntegerDividesAxioms(Interpretation divides, Interpretatio // create a skolem function with signature srt*srt>srt unsigned skolem = env.signature->addSkolemFunction(2); Signature::Symbol* sym = env.signature->getFunction(skolem); - sym->setType(new FunctionType({srt,srt},srt)); + sym->setType(OperatorType::getFunctionType({srt,srt},srt)); TermList skXY(Term::create2(skolem,n,y)); TermList msxX(Term::create2(mulFun,skXY,n)); Literal* msxXeqY = Literal::createEquality(true,msxX,y,srt); diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index a7664113c3..a880b2420c 100644 --- a/Shell/UIHelper.cpp +++ b/Shell/UIHelper.cpp @@ -594,7 +594,7 @@ void UIHelper::outputSymbolTypeDeclarationIfNeeded(ostream& out, bool function, } } - BaseType* type = function ? static_cast(sym->fnType()) : sym->predType(); + OperatorType* type = function ? sym->fnType() : sym->predType(); if (type->isAllDefault()) { return;