From 5acc529bd875195ce227a1c6376e4e19b8880723 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Fri, 10 Nov 2017 13:45:56 +0100 Subject: [PATCH] structured inpretretations done differently --- Kernel/InterpretedLiteralEvaluator.cpp | 7 - Kernel/Signature.cpp | 154 ++++---- Kernel/Signature.hpp | 58 +-- Kernel/Sorts.hpp | 2 - Kernel/Theory.cpp | 512 ++++++++----------------- Kernel/Theory.hpp | 110 +----- Parse/SMTLIB2.cpp | 28 +- Parse/TPTP.cpp | 24 +- Shell/Property.cpp | 16 +- Shell/Property.hpp | 15 +- Shell/TheoryAxioms.cpp | 80 ++-- Shell/TheoryAxioms.hpp | 9 +- 12 files changed, 374 insertions(+), 641 deletions(-) diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp index 48b4ed6bd3..91820cd66f 100644 --- a/Kernel/InterpretedLiteralEvaluator.cpp +++ b/Kernel/InterpretedLiteralEvaluator.cpp @@ -281,13 +281,6 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator virtual bool canEvaluate(Interpretation interp) { CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluate"); - - //only interpreted operations with non-single argument sort are array operations - if (theory->isArrayOperation(interp)) - { - unsigned opSort = theory->getArrayOperationSort(interp); - return opSort==T::getSort(); - } // This is why we cannot evaluate Equality here... we cannot determine its sort if (!theory->hasSingleSort(interp)) { return false; } //To skip conversions and EQUAL diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index b09bb069f7..39ed6d77ca 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -261,69 +261,6 @@ Signature::~Signature () } } // Signature::~Signature -/** - * Add interpreted function - */ -unsigned Signature::addInterpretedFunction(Interpretation interpretation, const vstring& name) -{ - CALL("Signature::addInterpretedFunction"); - ASS(Theory::isFunction(interpretation)); - - unsigned res; - if (_iSymbols.find(interpretation,res)) { // already declared - if (name!=functionName(res)) { - USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have"); - } - return res; - } - - vstring symbolKey = name+"_i"+Int::toString(interpretation); - ASS(!_funNames.find(symbolKey)); - - unsigned fnNum = _funs.length(); - InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation); - _funs.push(sym); - _funNames.insert(symbolKey, fnNum); - ALWAYS(_iSymbols.insert(interpretation, fnNum)); - OperatorType* fnType = Theory::getOperationType(interpretation); - ASS(fnType->isFunctionType()); - sym->setType(fnType); - return fnNum; -} // Signature::addInterpretedFunction - -/** - * Add interpreted predicate - */ -unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const vstring& name) -{ - CALL("Signature::addInterpretedPredicate"); - ASS(!Theory::isFunction(interpretation)); - - unsigned res; - if (_iSymbols.find(interpretation,res)) { // already declared - if (name!=predicateName(res)) { - USER_ERROR("Interpreted predicate '"+predicateName(res)+"' has the same interpretation as '"+name+"' should have"); - } - return res; - } - - vstring symbolKey = name+"_i"+Int::toString(interpretation); - - ASS(!_predNames.find(symbolKey)); - - unsigned predNum = _preds.length(); - InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation); - _preds.push(sym); - _predNames.insert(symbolKey,predNum); - ALWAYS(_iSymbols.insert(interpretation, predNum)); - if (predNum!=0) { - OperatorType* predType = Theory::getOperationType(interpretation); - ASS_REP(!predType->isFunctionType(), predType->toString()); - sym->setType(predType); - } - return predNum; -} // Signature::addInterpretedPredicate - /** * Add an integer constant to the signature. If defaultSort is true, treat it as * a term of the default sort, otherwise as an interepreted integer value. @@ -475,19 +412,88 @@ unsigned Signature::addRealConstant(const RealConstantType& value) return result; } +/** + * Add interpreted function + */ +unsigned Signature::addInterpretedFunction(Interpretation interpretation, OperatorType* type, const vstring& name) +{ + CALL("Signature::addInterpretedFunction(Interpretation,OperatorType*,const vstring&)"); + ASS(Theory::isFunction(interpretation)); + + Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type); + + unsigned res; + if (_iSymbols.find(mi,res)) { // already declared + if (name!=functionName(res)) { + USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have"); + } + return res; + } + + vstring symbolKey = name+"_i"+Int::toString(interpretation)+(Theory::isPolymorphic(interpretation) ? type->toString() : ""); + ASS(!_funNames.find(symbolKey)); + + unsigned fnNum = _funs.length(); + InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation); + _funs.push(sym); + _funNames.insert(symbolKey, fnNum); + ALWAYS(_iSymbols.insert(mi, fnNum)); + + OperatorType* fnType = Theory::getNonpolymorphicOperatorType(interpretation); + ASS(fnType->isFunctionType()); + sym->setType(fnType); + return fnNum; +} // Signature::addInterpretedFunction + +/** + * Add interpreted predicate + */ +unsigned Signature::addInterpretedPredicate(Interpretation interpretation, OperatorType* type, const vstring& name) +{ + CALL("Signature::addInterpretedPredicate(Interpretation,OperatorType*,const vstring&)"); + ASS(!Theory::isFunction(interpretation)); + + Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type); + + unsigned res; + if (_iSymbols.find(mi,res)) { // already declared + if (name!=predicateName(res)) { + USER_ERROR("Interpreted predicate '"+predicateName(res)+"' has the same interpretation as '"+name+"' should have"); + } + return res; + } + + vstring symbolKey = name+"_i"+Int::toString(interpretation)+(Theory::isPolymorphic(interpretation) ? type->toString() : ""); + + ASS(!_predNames.find(symbolKey)); + + unsigned predNum = _preds.length(); + InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation); + _preds.push(sym); + _predNames.insert(symbolKey,predNum); + ALWAYS(_iSymbols.insert(mi, predNum)); + if (predNum!=0) { + OperatorType* predType = Theory::getNonpolymorphicOperatorType(interpretation); + ASS_REP(!predType->isFunctionType(), predType->toString()); + sym->setType(predType); + } + return predNum; +} // Signature::addInterpretedPredicate + + /** * Return number of symbol that is interpreted by Interpretation @b interp. * * If no such symbol exists, it is created. */ -unsigned Signature::getInterpretingSymbol(Interpretation interp) +unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* type) { - CALL("Signature::getInterpretingSymbol"); + CALL("Signature::getInterpretingSymbol(Interpretation,OperatorType*)"); - ASS(Theory::instance()->isValidInterpretation(interp)); - + Theory::MonomorphisedInterpretation mi = std::make_pair(interp,type); + unsigned res; - if (_iSymbols.find(interp, res)) { + if (_iSymbols.find(mi, res)) { return res; } @@ -502,7 +508,7 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp) } name=name+Int::toString(i); } - addInterpretedFunction(interp, name); + addInterpretedFunction(interp, type, name); } else { if (predicateExists(name, arity)) { @@ -512,17 +518,11 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp) } name=name+Int::toString(i); } - addInterpretedPredicate(interp, name); + addInterpretedPredicate(interp, type, name); } //we have now registered a new function, so it should be present in the map - return _iSymbols.get(interp); -} - -unsigned Signature::getStructureInterpretationFunctor(unsigned theorySort, Theory::StructuredSortInterpretation ssi) { - CALL("Signature::getStructureInterpretationFunctor"); - Interpretation i = Theory::instance()->getInterpretation(theorySort, ssi); - return env.signature->getInterpretingSymbol(i); + return _iSymbols.get(mi); } const vstring& Signature::functionName(int number) diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 8421e7ab29..be53047459 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -335,10 +335,6 @@ class Signature unsigned addNamePredicate(unsigned arity); // Interpreted symbol declarations - - unsigned addInterpretedFunction(Interpretation itp, const vstring& name); - unsigned addInterpretedPredicate(Interpretation itp, const vstring& name); - unsigned addIntegerConstant(const vstring& number,bool defaultSort); unsigned addRationalConstant(const vstring& numerator, const vstring& denominator,bool defaultSort); unsigned addRealConstant(const vstring& number,bool defaultSort); @@ -347,27 +343,40 @@ class Signature unsigned addRationalConstant(const RationalConstantType& number); unsigned addRealConstant(const RealConstantType& number); - vstring getInterpretationName(Interpretation interp); - unsigned getInterpretingSymbol(Interpretation interp); - - unsigned getStructureInterpretationFunctor(unsigned theorySort, Theory::StructuredSortInterpretation ssi); + unsigned addInterpretedFunction(Interpretation itp, OperatorType* type, const vstring& name); + unsigned addInterpretedFunction(Interpretation itp, const vstring& name) + { + CALL("Signature::addInterpretedFunction(Interpretation,const vstring&)"); + ASS(!Theory::isPolymorphic(itp)); + return addInterpretedFunction(itp,Theory::getNonpolymorphicOperatorType(itp),name); + } - /** Return true iff there is a symbol interpreted by Interpretation @b interp */ - bool haveInterpretingSymbol(Interpretation interp) const { return _iSymbols.find(interp); } + unsigned addInterpretedPredicate(Interpretation itp, OperatorType* type, const vstring& name); + unsigned addInterpretedPredicate(Interpretation itp, const vstring& name) + { + CALL("Signature::addInterpretedPredicate(Interpretation,const vstring&)"); + ASS(!Theory::isPolymorphic(itp)); + return addInterpretedPredicate(itp,Theory::getNonpolymorphicOperatorType(itp),name); + } - /** - * Return true iff we have any declared interpreted symbols - * - * The equality symbol is always present and is interpreted, - * so we return true only if we have any other interpreted - * symbols. - */ - bool anyInterpretedSymbols() const + unsigned getInterpretingSymbol(Interpretation interp, OperatorType* type); + unsigned getInterpretingSymbol(Interpretation interp) { - CALL("Signature::anyInterpretedSymbols"); - ASS_G(_iSymbols.size(),0); //we always have equality which is interpreted + CALL("Signature::getInterpretingSymbol(Interpretation)"); + ASS(!Theory::isPolymorphic(interp)); + return getInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp)); + } - return _iSymbols.size()!=1; + /** Return true iff there is a symbol interpreted by Interpretation @b interp */ + bool haveInterpretingSymbol(Interpretation interp, OperatorType* type) const { + CALL("Signature::haveInterpretingSymbol(Interpretation, OperatorType*)"); + return _iSymbols.find(std::make_pair(interp,type)); + } + unsigned haveInterpretingSymbol(Interpretation interp) + { + CALL("Signature::haveInterpretingSymbol(Interpretation)"); + ASS(!Theory::isPolymorphic(interp)); + return haveInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp)); } /** return the name of a function with a given number */ @@ -533,13 +542,14 @@ class Signature bool _distinctGroupsAddedTo; /** - * Map from Interpretation values to function and predicate symbols representing them + * Map from MonomorphisedInterpretation values to function and predicate symbols representing them * * We mix here function and predicate symbols, but it is not a problem, as - * the Interpretation value already determines whether we deal with a function + * the MonomorphisedInterpretation value already determines whether we deal with a function * or a predicate. */ - DHMap _iSymbols; + DHMap _iSymbols; + /** the number of string constants */ unsigned _strings; /** the number of integer constants */ diff --git a/Kernel/Sorts.hpp b/Kernel/Sorts.hpp index cd862cba93..3a74868ad7 100644 --- a/Kernel/Sorts.hpp +++ b/Kernel/Sorts.hpp @@ -61,8 +61,6 @@ class Sorts { enum class StructuredSort { /** The structured sort for arrays **/ ARRAY, - /** The structured sort for lists, currently unused **/ - LIST, /** The structured sort for tuples */ TUPLE, /** not a real structured sort, it's here to denote the length of the StructuredSort enum */ diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp index 55b619605f..30cfc007b0 100644 --- a/Kernel/Theory.cpp +++ b/Kernel/Theory.cpp @@ -546,18 +546,6 @@ unsigned Theory::getArity(Interpretation i) CALL("Signature::InterpretedSymbol::getArity"); ASS(theory->isValidInterpretation(i)); - if (theory->isStructuredSortInterpretation(i)){ - switch (theory->convertToStructured(i)) { - case StructuredSortInterpretation::ARRAY_SELECT: - case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - return 2; - case StructuredSortInterpretation::ARRAY_STORE: - return 3; - default: - return 1; - } - } - switch(i) { case INT_IS_INT: case INT_IS_RAT: @@ -651,8 +639,15 @@ unsigned Theory::getArity(Interpretation i) case REAL_REMAINDER_E: case REAL_REMAINDER_T: case REAL_REMAINDER_F: + + case ARRAY_SELECT: + case ARRAY_BOOL_SELECT: + return 2; + case ARRAY_STORE: + + return 3; default: ASSERTION_VIOLATION_REP(i); @@ -668,15 +663,6 @@ bool Theory::isFunction(Interpretation i) CALL("Signature::InterpretedSymbol::isFunction"); ASS(theory->isValidInterpretation(i)); - if(theory->isStructuredSortInterpretation(i)){ - switch(theory->convertToStructured(i)){ - case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - return false; - default: - return true; - } - } - switch(i) { case INT_TO_INT: case INT_TO_RAT: @@ -738,6 +724,9 @@ bool Theory::isFunction(Interpretation i) case REAL_TRUNCATE: case REAL_ROUND: + case ARRAY_SELECT: + case ARRAY_STORE: + return true; case EQUAL: @@ -767,6 +756,9 @@ bool Theory::isFunction(Interpretation i) case REAL_IS_INT: case REAL_IS_RAT: case REAL_IS_REAL: + + case ARRAY_BOOL_SELECT: + return false; default: @@ -821,12 +813,35 @@ bool Theory::hasSingleSort(Interpretation i) case RAT_TO_REAL: case REAL_TO_INT: case REAL_TO_RAT: + + case ARRAY_SELECT: + case ARRAY_BOOL_SELECT: + case ARRAY_STORE: + return false; default: return true; } } +bool Theory::isPolymorphic(Interpretation i) +{ + CALL("Theory::isPolymorphic"); + + switch(i) { + case EQUAL: + return false; // for historical reasons equality is treated specially and does not count as polymorphic + + case ARRAY_SELECT: + case ARRAY_BOOL_SELECT: + case ARRAY_STORE: + + return true; + default: + return false; + } +} + /** * This function can be called for operations for which the * function @c hasSingleSort returns true @@ -835,13 +850,9 @@ unsigned Theory::getOperationSort(Interpretation i) { CALL("Theory::getOperationSort"); - ASS(hasSingleSort(i)); ASS(theory->isValidInterpretation(i)); - - if (theory->isStructuredSortInterpretation(i)) { - return theory->getStructuredOperationSort(i); - } + ASS(!isPolymorphic(i)); switch(i) { case INT_GREATER: @@ -1032,66 +1043,6 @@ bool Theory::isPartialFunction(Interpretation i) } } -unsigned Theory::getSymbolForStructuredSort(unsigned sort, StructuredSortInterpretation interp) -{ - return env.signature->getInterpretingSymbol(getInterpretation(sort,interp)); -} - -/** - * Return true if interpreted function @c i is an array operation. - * @author Laura Kovacs - * @since 31/08/2012, Vienna - */ -bool Theory::isArrayOperation(Interpretation i) -{ - CALL("Theory::isArrayFunction"); - if(!theory->isStructuredSortInterpretation(i)) return false; - return env.sorts->isOfStructuredSort(theory->getSort(i),Sorts::StructuredSort::ARRAY); -} - -/** -* This function can be called for array operations -* it returns the range domain (the sort of the output) of select and store -* @author Laura Kovacs -* @since 31/08/2012, Vienna -*/ -unsigned Theory::getArrayOperationSort(Interpretation i) -{ - CALL("Theory::getArrayOperationSort"); - ASS(isArrayOperation(i)); - - unsigned sort = theory->getSort(i); - - switch(theory->convertToStructured(i)) - { - case StructuredSortInterpretation::ARRAY_SELECT: - case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - return env.sorts->getArraySort(sort)->getInnerSort(); - case StructuredSortInterpretation::ARRAY_STORE: - return sort; - default: - ASSERTION_VIOLATION; - } -} - - - -/** -* This function returns the domain of array indexes (SRT_INT) -* @author Laura Kovacs -* @since 31/08/2012, Vienna -* @since 7/10/2015 update to support polymorphism in the index sort -*/ -unsigned Theory::getArrayDomainSort(Interpretation i) -{ - CALL("Theory::getArrayDomainSort"); - ASS(isArrayOperation(i)); - - unsigned sort = theory->getSort(i); - - return env.sorts->getArraySort(sort)->getIndexSort(); -} - /** * Get the number of the skolem function symbol used in the clause form of the * array extensionality axiom (of particular sort). @@ -1110,15 +1061,10 @@ unsigned Theory::getArrayExtSkolemFunction(unsigned sort) { return _arraySkolemFunctions.get(sort); } - bool isBool = (env.sorts->getArraySort(sort)->getInnerSort() == Sorts::SRT_BOOL); - - Interpretation store = getInterpretation(sort, StructuredSortInterpretation::ARRAY_STORE); - Interpretation select = getInterpretation(sort, isBool ? StructuredSortInterpretation::ARRAY_BOOL_SELECT - : StructuredSortInterpretation::ARRAY_SELECT); + Sorts::ArraySort* arraySort = env.sorts->getArraySort(sort); - unsigned arraySort = getArrayOperationSort(store); - unsigned indexSort = theory->getArrayDomainSort(select); - unsigned params[] = {arraySort, arraySort}; + unsigned indexSort = arraySort->getIndexSort(); + unsigned params[] = {sort, sort}; unsigned skolemFunction = Shell::Skolem::addSkolemFunction(2, params, indexSort, "arrayDiff"); _arraySkolemFunctions.insert(sort,skolemFunction); @@ -1249,173 +1195,140 @@ OperatorType* Theory::getConversionOperationType(Interpretation i) return OperatorType::getFunctionType({from}, to); } -Sorts::StructuredSort Theory::getInterpretedSort(StructuredSortInterpretation ssi) { - switch (ssi) { - case StructuredSortInterpretation::ARRAY_SELECT: - case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - case StructuredSortInterpretation::ARRAY_STORE: - return Sorts::StructuredSort::ARRAY; - case StructuredSortInterpretation::LIST_HEAD: - case StructuredSortInterpretation::LIST_TAIL: - case StructuredSortInterpretation::LIST_CONS: - case StructuredSortInterpretation::LIST_IS_EMPTY: - return Sorts::StructuredSort::LIST; - default: - ASSERTION_VIOLATION; - } -} - vstring Theory::getInterpretationName(Interpretation interp) { CALL("Theory::getInterpretationName"); - if (Theory::instance()->isStructuredSortInterpretation(interp)) { - switch (Theory::instance()->convertToStructured(interp)) { - case StructuredSortInterpretation::ARRAY_SELECT: - case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - return "$select"; - case StructuredSortInterpretation::ARRAY_STORE: - return "$store"; - default: - ASSERTION_VIOLATION_REP(interp); - } - } else { - switch (interp) { - case Theory::INT_SUCCESSOR: - //this one is not according the TPTP arithmetic (it doesn't have successor) - return "$successor"; - case Theory::INT_DIVIDES: - return "$divides"; - case Theory::INT_UNARY_MINUS: - case Theory::RAT_UNARY_MINUS: - case Theory::REAL_UNARY_MINUS: - return "$uminus"; - case Theory::INT_PLUS: - case Theory::RAT_PLUS: - case Theory::REAL_PLUS: - return "$sum"; - case Theory::INT_MINUS: - case Theory::RAT_MINUS: - case Theory::REAL_MINUS: - return "$difference"; - case Theory::INT_MULTIPLY: - case Theory::RAT_MULTIPLY: - case Theory::REAL_MULTIPLY: - return "$product"; - case Theory::INT_GREATER: - case Theory::RAT_GREATER: - case Theory::REAL_GREATER: - return "$greater"; - case Theory::INT_GREATER_EQUAL: - case Theory::RAT_GREATER_EQUAL: - case Theory::REAL_GREATER_EQUAL: - return "$greatereq"; - case Theory::INT_LESS: - case Theory::RAT_LESS: - case Theory::REAL_LESS: - return "$less"; - case Theory::INT_LESS_EQUAL: - case Theory::RAT_LESS_EQUAL: - case Theory::REAL_LESS_EQUAL: - return "$lesseq"; - case Theory::INT_IS_INT: - case Theory::RAT_IS_INT: - case Theory::REAL_IS_INT: - return "$is_int"; - case Theory::INT_IS_RAT: - case Theory::RAT_IS_RAT: - case Theory::REAL_IS_RAT: - return "$is_rat"; - case Theory::INT_IS_REAL: - case Theory::RAT_IS_REAL: - case Theory::REAL_IS_REAL: - return "$is_real"; - case Theory::INT_TO_INT: - case Theory::RAT_TO_INT: - case Theory::REAL_TO_INT: - return "$to_int"; - case Theory::INT_TO_RAT: - case Theory::RAT_TO_RAT: - case Theory::REAL_TO_RAT: - return "$to_rat"; - case Theory::INT_TO_REAL: - case Theory::RAT_TO_REAL: - case Theory::REAL_TO_REAL: - return "$to_real"; - case Theory::INT_ABS: - return "$abs"; - case Theory::INT_QUOTIENT_E: - case Theory::RAT_QUOTIENT_E: - case Theory::REAL_QUOTIENT_E: - return "$quotient_e"; - case Theory::INT_QUOTIENT_T: - case Theory::RAT_QUOTIENT_T: - case Theory::REAL_QUOTIENT_T: - return "$quotient_t"; - case Theory::INT_QUOTIENT_F: - case Theory::RAT_QUOTIENT_F: - case Theory::REAL_QUOTIENT_F: - return "$quotient_f"; - case Theory::INT_REMAINDER_T: - case Theory::RAT_REMAINDER_T: - case Theory::REAL_REMAINDER_T: - return "$remainder_t"; - case Theory::INT_REMAINDER_F: - case Theory::RAT_REMAINDER_F: - case Theory::REAL_REMAINDER_F: - return "$remainder_f"; - case Theory::INT_REMAINDER_E: - case Theory::RAT_REMAINDER_E: - case Theory::REAL_REMAINDER_E: - return "$remainder_e"; - case Theory::RAT_QUOTIENT: - case Theory::REAL_QUOTIENT: - return "$quotient"; - case Theory::INT_TRUNCATE: - case Theory::RAT_TRUNCATE: - case Theory::REAL_TRUNCATE: - return "truncate"; - case Theory::INT_FLOOR: - case Theory::RAT_FLOOR: - case Theory::REAL_FLOOR: - return "floor"; - case Theory::INT_CEILING: - case Theory::RAT_CEILING: - case Theory::REAL_CEILING: - return "ceiling"; - default: - ASSERTION_VIOLATION_REP(interp); - } + switch (interp) { + case INT_SUCCESSOR: + //this one is not according the TPTP arithmetic (it doesn't have successor) + return "$successor"; + case INT_DIVIDES: + return "$divides"; + case INT_UNARY_MINUS: + case RAT_UNARY_MINUS: + case REAL_UNARY_MINUS: + return "$uminus"; + case INT_PLUS: + case RAT_PLUS: + case REAL_PLUS: + return "$sum"; + case INT_MINUS: + case RAT_MINUS: + case REAL_MINUS: + return "$difference"; + case INT_MULTIPLY: + case RAT_MULTIPLY: + case REAL_MULTIPLY: + return "$product"; + case INT_GREATER: + case RAT_GREATER: + case REAL_GREATER: + return "$greater"; + case INT_GREATER_EQUAL: + case RAT_GREATER_EQUAL: + case REAL_GREATER_EQUAL: + return "$greatereq"; + case INT_LESS: + case RAT_LESS: + case REAL_LESS: + return "$less"; + case INT_LESS_EQUAL: + case RAT_LESS_EQUAL: + case REAL_LESS_EQUAL: + return "$lesseq"; + case INT_IS_INT: + case RAT_IS_INT: + case REAL_IS_INT: + return "$is_int"; + case INT_IS_RAT: + case RAT_IS_RAT: + case REAL_IS_RAT: + return "$is_rat"; + case INT_IS_REAL: + case RAT_IS_REAL: + case REAL_IS_REAL: + return "$is_real"; + case INT_TO_INT: + case RAT_TO_INT: + case REAL_TO_INT: + return "$to_int"; + case INT_TO_RAT: + case RAT_TO_RAT: + case REAL_TO_RAT: + return "$to_rat"; + case INT_TO_REAL: + case RAT_TO_REAL: + case REAL_TO_REAL: + return "$to_real"; + case INT_ABS: + return "$abs"; + case INT_QUOTIENT_E: + case RAT_QUOTIENT_E: + case REAL_QUOTIENT_E: + return "$quotient_e"; + case INT_QUOTIENT_T: + case RAT_QUOTIENT_T: + case REAL_QUOTIENT_T: + return "$quotient_t"; + case INT_QUOTIENT_F: + case RAT_QUOTIENT_F: + case REAL_QUOTIENT_F: + return "$quotient_f"; + case INT_REMAINDER_T: + case RAT_REMAINDER_T: + case REAL_REMAINDER_T: + return "$remainder_t"; + case INT_REMAINDER_F: + case RAT_REMAINDER_F: + case REAL_REMAINDER_F: + return "$remainder_f"; + case INT_REMAINDER_E: + case RAT_REMAINDER_E: + case REAL_REMAINDER_E: + return "$remainder_e"; + case RAT_QUOTIENT: + case REAL_QUOTIENT: + return "$quotient"; + case INT_TRUNCATE: + case RAT_TRUNCATE: + case REAL_TRUNCATE: + return "truncate"; + case INT_FLOOR: + case RAT_FLOOR: + case REAL_FLOOR: + return "floor"; + case INT_CEILING: + case RAT_CEILING: + case REAL_CEILING: + return "ceiling"; + case ARRAY_SELECT: + case ARRAY_BOOL_SELECT: + return "$select"; + case ARRAY_STORE: + return "$store"; + default: + ASSERTION_VIOLATION_REP(interp); } } -OperatorType* Theory::getStructuredSortOperationType(Interpretation i) { - CALL("Theory::getStructuredSortOperationType"); - - ASS(theory->isStructuredSortInterpretation(i)); +OperatorType* Theory::getArrayOperatorType(unsigned arraySort, Interpretation i) { + CALL("Theory::getArrayOperatorType"); - unsigned theorySort = theory->getSort(i); - StructuredSortInterpretation ssi = theory->convertToStructured(i); + Sorts::ArraySort* info = env.sorts->getArraySort(arraySort); - switch (theory->getInterpretedSort(ssi)) { - case Sorts::StructuredSort::ARRAY: { - unsigned indexSort = getArrayDomainSort(i); - unsigned valueSort = getArrayOperationSort(i); - unsigned innerSort = env.sorts->getArraySort(theorySort)->getInnerSort(); + unsigned indexSort = info->getIndexSort(); + unsigned innerSort = info->getInnerSort(); - switch (ssi) { - case StructuredSortInterpretation::ARRAY_SELECT: - return OperatorType::getFunctionType({ theorySort, indexSort }, valueSort); + switch (i) { + case Interpretation::ARRAY_SELECT: + return OperatorType::getFunctionType({ arraySort, indexSort }, innerSort); - case StructuredSortInterpretation::ARRAY_BOOL_SELECT: - return OperatorType::getPredicateType({ theorySort, indexSort }); + case Interpretation::ARRAY_BOOL_SELECT: + return OperatorType::getPredicateType({ arraySort, indexSort }); - case StructuredSortInterpretation::ARRAY_STORE: - return OperatorType::getFunctionType({ theorySort, indexSort, innerSort }, valueSort); + case Interpretation::ARRAY_STORE: + return OperatorType::getFunctionType({ arraySort, indexSort, innerSort }, arraySort); - default: - ASSERTION_VIOLATION; - } - } default: ASSERTION_VIOLATION; } @@ -1424,19 +1337,15 @@ OperatorType* Theory::getStructuredSortOperationType(Interpretation i) { /** * Return type of the function representing interpreted function/predicate @c i. */ -OperatorType* Theory::getOperationType(Interpretation i) +OperatorType* Theory::getNonpolymorphicOperatorType(Interpretation i) { - CALL("Theory::getOperationType"); - ASS_NEQ(i, EQUAL); + CALL("Theory::getNonpolymorphicOperationType"); + ASS(!isPolymorphic(i)); if (isConversionOperation(i)) { return getConversionOperationType(i); } - if (theory->isStructuredSortInterpretation(i)) { - return getStructuredSortOperationType(i); - } - unsigned sort; ASS(hasSingleSort(i)); sort = getOperationSort(i); @@ -1839,97 +1748,6 @@ Term* Theory::representRealConstant(vstring str) } } -/** - * Return term containing unary function interpreted as @b itp with - * @b arg as its first argument - */ -Term* Theory::fun1(Interpretation itp, TermList arg) -{ - CALL("Theory::fun1"); - ASS(isFunction(itp)); - ASS_EQ(getArity(itp), 1); - - unsigned fn=theory->getFnNum(itp); - return Term::create(fn, 1, &arg); -} - -/** - * Return term containing binary function interpreted as @b itp with - * arguments @b arg1 and @b arg2 - */ -Term* Theory::fun2(Interpretation itp, TermList arg1, TermList arg2) -{ - CALL("Theory::fun2"); - ASS(isFunction(itp)); - ASS_EQ(getArity(itp), 2); - - TermList args[]= {arg1, arg2}; - - unsigned fn=theory->getFnNum(itp); - return Term::create(fn, 2, args); -} - - -/** -* Return term containing trenary function interpreted as @b itp with -* arguments @b arg1 , @b arg2, @b arg3 -*/ -Term* Theory::fun3(Interpretation itp, TermList arg1, TermList arg2, TermList arg3) - { - CALL("Theory::fun3"); - ASS(isFunction(itp)); - ASS_EQ(getArity(itp), 3); - - TermList args[]= {arg1, arg2, arg3}; - - unsigned fn=theory->getFnNum(itp); - return Term::create(fn, 3, args); - } - - - - -/** - * Return literal containing binary predicate interpreted as @b itp with - * arguments @b arg1 and @b arg2 - * - * Equality cannot be created using this function, Term::createEquality has to be used. - */ -Literal* Theory::pred2(Interpretation itp, bool polarity, TermList arg1, TermList arg2) -{ - CALL("Theory::fun2"); - ASS(!isFunction(itp)); - ASS_EQ(getArity(itp), 2); - ASS_NEQ(itp,EQUAL); - - TermList args[]= {arg1, arg2}; - - unsigned pred=theory->getPredNum(itp); - return Literal::create(pred, 2, polarity, false, args); -} - -/** - * Return number of function that is intepreted as @b itp - */ -unsigned Theory::getFnNum(Interpretation itp) -{ - CALL("Theory::getFnNum"); - ASS(isFunction(itp)); - - return env.signature->getInterpretingSymbol(itp); -} - -/** - * Return number of predicate that is intepreted as @b itp - */ -unsigned Theory::getPredNum(Interpretation itp) -{ - CALL("Theory::getPredNum"); - ASS(!isFunction(itp)); - - return env.signature->getInterpretingSymbol(itp); -} - /** * Register that a predicate pred with a given polarity has the given * template. See tryGetInterpretedLaTeXName for explanation of templates diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp index 5b0d87f590..f15e451766 100644 --- a/Kernel/Theory.hpp +++ b/Kernel/Theory.hpp @@ -138,8 +138,6 @@ std::ostream& operator<< (ostream& out, const IntegerConstantType& val) { return out << val.toInner(); } - - /** * A class for representing rational numbers * @@ -375,84 +373,38 @@ class Theory RAT_TO_REAL, REAL_TO_INT, REAL_TO_RAT, - REAL_TO_REAL + REAL_TO_REAL, - // IMPORTANT - if you add something to end of this, update it in LastNonStructuredInterepretation + // array functions + ARRAY_SELECT, + ARRAY_BOOL_SELECT, + ARRAY_STORE, - //INVALID_INTERPRETATION // replaced by LastNonStructuredInterepretation + INVALID_INTERPRETATION // LEAVE THIS AS THE LAST ELEMENT OF THE ENUM }; - unsigned LastNonStructuredInterepretation(){ return REAL_TO_REAL; } + typedef std::pair MonomorphisedInterpretation; - /** - * Maximal element number in the enum Interpretation - * - * At some points we make use of the fact that we can iterate through all - * interpretations by going through the set {0,...,MAX_INTERPRETED_ELEMENT}. - */ - unsigned MaxInterpretedElement(){ - return LastNonStructuredInterepretation() + _structuredSortInterpretations.size(); - } - - unsigned numberOfInterpretations(){ - return LastNonStructuredInterepretation() + LastStructuredInterpretation(); + bool isValidInterpretation(Interpretation i){ + return i < INVALID_INTERPRETATION; } - bool isValidInterpretation(Interpretation i){ - return i <= MaxInterpretedElement(); + unsigned numberOfInterpretations() { + return INVALID_INTERPRETATION; } bool isPlus(Interpretation i){ return i == INT_PLUS || i == RAT_PLUS || i == REAL_PLUS; } - /* - * StructuredSortInterpretations begin from the last interpretation in Interpretation - * - * They will be initialised as MaxInterpretedElement()+1 - * - */ - - - /** enum for the kinds of StructuredSort interpretations **/ - enum class StructuredSortInterpretation - { - ARRAY_SELECT, - ARRAY_BOOL_SELECT, - ARRAY_STORE, - // currently unused - LIST_HEAD, - LIST_TAIL, - LIST_CONS, - LIST_IS_EMPTY - }; - unsigned LastStructuredInterpretation(){ - return static_cast(StructuredSortInterpretation::LIST_IS_EMPTY); - } - unsigned getSymbolForStructuredSort(unsigned sort, StructuredSortInterpretation interp); - Interpretation getInterpretation(unsigned sort, StructuredSortInterpretation i){ - auto key = make_pair(sort, i); - unsigned interpretation; - if (!_structuredSortInterpretations.find(key, interpretation)) { - interpretation = MaxInterpretedElement() + 1; - _structuredSortInterpretations.insert(key, interpretation); - } - return static_cast(interpretation); - } - bool isStructuredSortInterpretation(Interpretation i){ - return i > LastNonStructuredInterepretation(); - } - unsigned getSort(Interpretation i){ - return getData(i).first; - } - static vstring getInterpretationName(Interpretation i); static unsigned getArity(Interpretation i); static bool isFunction(Interpretation i); static bool isInequality(Interpretation i); - static Sorts::StructuredSort getInterpretedSort(StructuredSortInterpretation ssi); - static OperatorType* getOperationType(Interpretation i); - static OperatorType* getStructuredSortOperationType(Interpretation i); + static OperatorType* getNonpolymorphicOperatorType(Interpretation i); + + static OperatorType* getArrayOperatorType(unsigned arraySort, Interpretation i); + static bool hasSingleSort(Interpretation i); static unsigned getOperationSort(Interpretation i); static bool isConversionOperation(Interpretation i); @@ -460,9 +412,7 @@ class Theory static bool isNonLinearOperation(Interpretation i); static bool isPartialFunction(Interpretation i); - static bool isArrayOperation(Interpretation i); - static unsigned getArrayOperationSort(Interpretation i); - static unsigned getArrayDomainSort(Interpretation i); + static bool isPolymorphic(Interpretation i); unsigned getArrayExtSkolemFunction(unsigned i); @@ -497,9 +447,6 @@ class Theory Interpretation interpretPredicate(unsigned pred); Interpretation interpretPredicate(Literal* t); - unsigned getFnNum(Interpretation itp); - unsigned getPredNum(Interpretation itp); - void registerLaTeXPredName(unsigned func, bool polarity, vstring temp); void registerLaTeXFuncName(unsigned func, vstring temp); vstring tryGetInterpretedLaTeXName(unsigned func, bool pred,bool polarity=true); @@ -512,11 +459,6 @@ class Theory public: - Term* fun1(Interpretation itp, TermList arg); - Term* fun2(Interpretation itp, TermList arg1, TermList arg2); - Term* fun3(Interpretation itp, TermList arg1, TermList arg2, TermList arg3); - Literal* pred2(Interpretation itp, bool polarity, TermList arg1, TermList arg2); - /** * Try to interpret the term list as an integer constant. If it is an * integer constant, return true and save the constant in @c res, otherwise @@ -572,26 +514,6 @@ class Theory DHMap _arraySkolemFunctions; -public: - unsigned getStructuredOperationSort(Interpretation i){ - return getData(i).first; - } - StructuredSortInterpretation convertToStructured(Interpretation i){ - return getData(i).second; - } -private: - pair getData(Interpretation i){ - ASS(isStructuredSortInterpretation(i)); - auto it = _structuredSortInterpretations.items(); - while(it.hasNext()){ - auto entry = it.next(); - if(entry.second==i) return entry.first; - } - ASSERTION_VIOLATION; - } - - DHMap,unsigned> _structuredSortInterpretations; - public: class Tuples { public: diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index 36f574889e..5416523531 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -1650,7 +1650,7 @@ bool SMTLIB2::parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp) lastConjunct = new AtomicFormula(Literal::createEquality(true, first, second, sort)); } else { Interpretation intp = getFormulaSymbolInterpretation(fs,sort); - pred = Theory::instance()->getPredNum(intp); + pred = env.signature->getInterpretingSymbol(intp); lastConjunct = new AtomicFormula(Literal::create2(pred,true,first,second)); } @@ -1740,7 +1740,7 @@ bool SMTLIB2::parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp) complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); } - unsigned pred = Theory::instance()->getPredNum(Theory::REAL_IS_INT); + unsigned pred = env.signature->getInterpretingSymbol(Theory::REAL_IS_INT); Formula* res = new AtomicFormula(Literal::create1(pred,true,arg)); _results.push(res); @@ -1819,7 +1819,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); } - unsigned fun = Theory::instance()->getFnNum(Theory::INT_TO_REAL); + unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_TO_REAL); TermList res = TermList(Term::create1(fun,theInt)); _results.push(ParseResult(Sorts::SRT_REAL,res)); @@ -1833,7 +1833,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); } - unsigned fun = Theory::instance()->getFnNum(Theory::REAL_TO_INT); + unsigned fun = env.signature->getInterpretingSymbol(Theory::REAL_TO_INT); TermList res = TermList(Term::create1(fun,theReal)); _results.push(ParseResult(Sorts::SRT_INTEGER,res)); @@ -1858,13 +1858,16 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) } if (arraySort->getInnerSort() == Sorts::SRT_BOOL) { - unsigned pred = Theory::instance()->getSymbolForStructuredSort(arraySortIdx,Theory::StructuredSortInterpretation::ARRAY_BOOL_SELECT); + OperatorType* predType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_BOOL_SELECT); + unsigned pred = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,predType); Formula* res = new AtomicFormula(Literal::create2(pred,true,theArray,theIndex)); _results.push(ParseResult(res)); } else { - unsigned fun = Theory::instance()->getSymbolForStructuredSort(arraySortIdx,Theory::StructuredSortInterpretation::ARRAY_SELECT); + OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_SELECT); + unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,funType); + TermList res = TermList(Term::create2(fun,theArray,theIndex)); _results.push(ParseResult(arraySort->getInnerSort(),res)); @@ -1896,7 +1899,8 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); } - unsigned fun = Theory::instance()->getSymbolForStructuredSort(arraySortIdx,Theory::StructuredSortInterpretation::ARRAY_STORE); + OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_STORE); + unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,funType); TermList args[] = {theArray, theIndex, theValue}; TermList res = TermList(Term::Term::create(fun, 3, args)); @@ -1913,7 +1917,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); } - unsigned fun = Theory::instance()->getFnNum(Theory::INT_ABS); + unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_ABS); TermList res = TermList(Term::create1(fun,theInt)); _results.push(ParseResult(Sorts::SRT_INTEGER,res)); @@ -1928,7 +1932,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); } - unsigned fun = Theory::instance()->getFnNum(Theory::INT_REMAINDER_E); // TS_MOD is the always positive remainder, therefore INT_REMAINDER_E + unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_REMAINDER_E); // TS_MOD is the always positive remainder, therefore INT_REMAINDER_E TermList res = TermList(Term::create2(fun,int1,int2)); _results.push(ParseResult(Sorts::SRT_INTEGER,res)); @@ -1951,7 +1955,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) if (_results.isEmpty() || _results.top().isSeparator()) { if (ts == TS_MINUS) { // unary minus Interpretation intp = getUnaryMinusInterpretation(sort); - unsigned fun = Theory::instance()->getFnNum(intp); + unsigned fun = env.signature->getInterpretingSymbol(intp); TermList res = TermList(Term::create1(fun,first)); @@ -1964,7 +1968,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp) } Interpretation intp = getTermSymbolInterpretation(ts,sort); - unsigned fun = Theory::instance()->getFnNum(intp); + unsigned fun = env.signature->getInterpretingSymbol(intp); TermList second; if (_results.pop().asTerm(second) != sort) { @@ -2021,7 +2025,7 @@ void SMTLIB2::parseRankedFunctionApplication(LExpr* exp) complainAboutArgShortageOrWrongSorts("ranked function symbol",exp); } - unsigned pred = Theory::instance()->getPredNum(Theory::INT_DIVIDES); + unsigned pred = env.signature->getInterpretingSymbol(Theory::INT_DIVIDES); env.signature->recordDividesNvalue(divisorTerm); Formula* res = new AtomicFormula(Literal::create2(pred,true,divisorTerm,arg)); diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index c7fc21d4ce..64ebd47a3a 100644 --- a/Parse/TPTP.cpp +++ b/Parse/TPTP.cpp @@ -1480,9 +1480,9 @@ void TPTP::endTheoryFunction() { * endTermAsFormula(). */ - Theory::StructuredSortInterpretation ssi; + Theory::Interpretation itp; TermList args[3]; // all theory function use up to 3 arguments as for now - unsigned theorySort; + unsigned arraySort; TheoryFunction tf = _theoryFunctions.pop(); switch (tf) { @@ -1490,7 +1490,7 @@ void TPTP::endTheoryFunction() { TermList index = _termLists.pop(); TermList array = _termLists.pop(); - unsigned arraySort = sortOf(array); + arraySort = sortOf(array); if (!env.sorts->isOfStructuredSort(arraySort, Sorts::StructuredSort::ARRAY)) { USER_ERROR("$select is being incorrectly used on a type of array " + env.sorts->sortName(arraySort) + " that has not be defined"); } @@ -1502,12 +1502,11 @@ void TPTP::endTheoryFunction() { args[0] = array; args[1] = index; - theorySort = arraySort; if (env.sorts->getArraySort(arraySort)->getInnerSort() == Sorts::SRT_BOOL) { - ssi = Theory::StructuredSortInterpretation::ARRAY_BOOL_SELECT; + itp = Theory::Interpretation::ARRAY_BOOL_SELECT; } else { - ssi = Theory::StructuredSortInterpretation::ARRAY_SELECT; + itp = Theory::Interpretation::ARRAY_SELECT; } break; } @@ -1516,7 +1515,7 @@ void TPTP::endTheoryFunction() { TermList index = _termLists.pop(); TermList array = _termLists.pop(); - unsigned arraySort = sortOf(array); + arraySort = sortOf(array); if (!env.sorts->isOfStructuredSort(arraySort, Sorts::StructuredSort::ARRAY)) { USER_ERROR("store is being incorrectly used on a type of array that has not be defined"); } @@ -1535,8 +1534,7 @@ void TPTP::endTheoryFunction() { args[1] = index; args[2] = value; - ssi = Theory::StructuredSortInterpretation::ARRAY_STORE; - theorySort = arraySort; + itp = Theory::Interpretation::ARRAY_STORE; break; } @@ -1544,11 +1542,11 @@ void TPTP::endTheoryFunction() { ASSERTION_VIOLATION_REP(tf); } - Interpretation i = Theory::instance()->getInterpretation(theorySort, ssi); - unsigned symbol = env.signature->getStructureInterpretationFunctor(theorySort, ssi); - unsigned arity = Theory::getArity(i); + OperatorType* type = Theory::getArrayOperatorType(arraySort,itp); + unsigned symbol = env.signature->getInterpretingSymbol(itp, type); + unsigned arity = Theory::getArity(itp); - if (Theory::isFunction(i)) { + if (Theory::isFunction(itp)) { Term* term = Term::create(symbol, arity, args); _termLists.push(TermList(term)); } else { diff --git a/Shell/Property.cpp b/Shell/Property.cpp index 521b5d673c..63a218e059 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -90,8 +90,7 @@ Property::Property() _allQuantifiersEssentiallyExistential(true), _smtlibLogic(SMTLIBLogic::SMT_UNDEFINED) { - //TODO now MaxInterpretedElement is stateful this might be in the wrong place - _interpretationPresence.init(Theory::instance()->numberOfInterpretations()+1, false); + _interpretationPresence.init(Theory::instance()->numberOfInterpretations(), false); env.property = this; } // Property::Property @@ -628,17 +627,22 @@ void Property::scanForInterpreted(Term* t) itp = theory->interpretFunction(t); } _hasInterpreted = true; + if(itp < _interpretationPresence.size()){ _interpretationPresence[itp] = true; } + + if (Theory::isPolymorphic(itp)) { + OperatorType* type = t->isLiteral() ? + env.signature->getPredicate(t->functor())->predType() : env.signature->getFunction(t->functor())->fnType(); + + _polymorphicInterpretations.insert(std::make_pair(itp,type)); + } + if(Theory::isConversionOperation(itp)){ addProp(PR_NUMBER_CONVERSION); return; } - if(Theory::isArrayOperation(itp)){ - //addProp(PR_HAS_ARRAYS); - return; - } unsigned sort = Theory::getOperationSort(itp); if(Theory::isInequality(itp)){ diff --git a/Shell/Property.hpp b/Shell/Property.hpp index 11139c9519..d760491be7 100644 --- a/Shell/Property.hpp +++ b/Shell/Property.hpp @@ -31,6 +31,7 @@ #include "Lib/DArray.hpp" #include "Lib/Array.hpp" +#include "Lib/DHSet.hpp" #include "Kernel/Unit.hpp" #include "Kernel/Theory.hpp" #include "Lib/VString.hpp" @@ -215,11 +216,14 @@ class Property */ void scanForInterpreted(Term* t); - bool hasInterpretedOperation(Interpretation i) const { + bool hasInterpretedOperation(Interpretation i) const { if(i >= _interpretationPresence.size()){ return false; } return _interpretationPresence[i]; } - //bool hasArrayOperation(Interpretation i) const { return true; } + bool hasInterpretedOperation(Interpretation i, OperatorType* type) const { + return _polymorphicInterpretations.find(std::make_pair(i,type)); + } + /** Problem contains an interpreted symbol excluding equality */ bool hasInterpretedOperations() const { return _hasInterpreted; } bool hasInterpretedEquality() const { return _hasInterpretedEquality; } @@ -321,9 +325,14 @@ class Property /** Problem contains non-default sorts */ bool _hasNonDefaultSorts; unsigned _sortsUsed; - DArray _interpretationPresence; Array _usesSort; + /** Makes sense for all interpretations, but for polymorphic ones we also keep + * the more precise information about which monomorphisations are present (see below). + */ + DArray _interpretationPresence; + DHSet _polymorphicInterpretations; + bool _hasFOOL; bool _onlyFiniteDomainDatatypes; diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp index 19330a6e0f..bd86f78c48 100644 --- a/Shell/TheoryAxioms.cpp +++ b/Shell/TheoryAxioms.cpp @@ -828,19 +828,14 @@ void TheoryAxioms::addTruncateAxioms(Interpretation truncate, Interpretation les * @since 05/01/2014 Vienna, add axiom in clause form (we need skolem function in other places) * @author Bernhard Kragl */ -void TheoryAxioms::addArrayExtensionalityAxioms(Interpretation select, - Interpretation store, - unsigned skolemFn) +void TheoryAxioms::addArrayExtensionalityAxioms(unsigned arraySort, unsigned skolemFn) { CALL("TheoryAxioms::addArrayExtenstionalityAxioms"); - - ASS(theory->isFunction(select)); - ASS(theory->isArrayOperation(select)); - ASS_EQ(theory->getArity(select),2); - - unsigned sel = env.signature->getInterpretingSymbol(select); - unsigned rangeSort = theory->getArrayOperationSort(select); - unsigned arraySort = theory->getArrayOperationSort(store); + + unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT)); + + Sorts::ArraySort* si = env.sorts->getArraySort(arraySort); + unsigned rangeSort = si->getInnerSort(); TermList x(0,false); TermList y(1,false); @@ -861,18 +856,13 @@ void TheoryAxioms::addArrayExtensionalityAxioms(Interpretation select, * @since 25/08/2015 Gothenburg * @author Evgeny Kotelnikov */ -void TheoryAxioms::addBooleanArrayExtensionalityAxioms(Interpretation select, - Interpretation store, - unsigned skolemFn) +void TheoryAxioms::addBooleanArrayExtensionalityAxioms(unsigned arraySort, unsigned skolemFn) { CALL("TheoryAxioms::addBooleanArrayExtenstionalityAxioms"); - ASS(!theory->isFunction(select)); - ASS(theory->isArrayOperation(select)); - ASS_EQ(theory->getArity(select),2); + OperatorType* selectType = Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT); - unsigned sel = env.signature->getInterpretingSymbol(select); - unsigned arraySort = theory->getArrayOperationSort(store); + unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,selectType); TermList x(0,false); TermList y(1,false); @@ -896,22 +886,17 @@ void TheoryAxioms::addBooleanArrayExtensionalityAxioms(Interpretation select, * @author Laura Kovacs * @since 31/08/2012, Vienna */ -void TheoryAxioms::addArrayWriteAxioms(Interpretation select, Interpretation store) +void TheoryAxioms::addArrayWriteAxioms(unsigned arraySort) { CALL("TheoryAxioms::addArrayWriteAxioms"); - ASS(theory->isFunction(select)); - ASS(theory->isArrayOperation(select)); - ASS_EQ(theory->getArity(select),2); - - - unsigned func_select = env.signature->getInterpretingSymbol(select); - unsigned func_store = env.signature->getInterpretingSymbol(store); + unsigned func_select = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT)); + unsigned func_store = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE)); + + Sorts::ArraySort* si = env.sorts->getArraySort(arraySort); + unsigned rangeSort = si->getInnerSort(); + unsigned domainSort = si->getIndexSort(); - unsigned rangeSort = theory->getArrayOperationSort(select); - unsigned domainSort = theory->getArrayDomainSort(select); - //unsigned arraySort = theory->getOperationSort(store); - TermList i(0,false); TermList j(1,false); TermList v(2,false); @@ -938,20 +923,15 @@ void TheoryAxioms::addArrayWriteAxioms(Interpretation select, Interpretation sto * @author Laura Kovacs * @since 31/08/2012, Vienna */ -void TheoryAxioms::addBooleanArrayWriteAxioms(Interpretation select, Interpretation store) +void TheoryAxioms::addBooleanArrayWriteAxioms(unsigned arraySort) { CALL("TheoryAxioms::addArrayWriteAxioms"); - ASS(!theory->isFunction(select)); - ASS(theory->isArrayOperation(select)); - ASS_EQ(theory->getArity(select),2); + unsigned pred_select = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT)); + unsigned func_store = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE)); - unsigned pred_select = env.signature->getInterpretingSymbol(select); - unsigned func_store = env.signature->getInterpretingSymbol(store); - - //unsigned rangeSort = theory->getArrayOperationSort(select); - unsigned domainSort = theory->getArrayDomainSort(select); - //unsigned arraySort = theory->getOperationSort(store); + Sorts::ArraySort* si = env.sorts->getArraySort(arraySort); + unsigned domainSort = si->getIndexSort(); TermList a(0,false); TermList i(1,false); @@ -1161,28 +1141,24 @@ void TheoryAxioms::apply() unsigned arraySort = arraySorts.next(); bool isBool = (env.sorts->getArraySort(arraySort)->getInnerSort() == Sorts::SRT_BOOL); - - // Get Interpretation objects for functions - Interpretation arraySelect = theory->getInterpretation(arraySort, isBool ? Theory::StructuredSortInterpretation::ARRAY_BOOL_SELECT - : Theory::StructuredSortInterpretation::ARRAY_SELECT); - Interpretation arrayStore = theory->getInterpretation(arraySort,Theory::StructuredSortInterpretation::ARRAY_STORE); // Check if they are used - bool haveSelect = prop->hasInterpretedOperation(arraySelect); - bool haveStore = prop->hasInterpretedOperation(arrayStore); + Interpretation arraySelect = isBool ? Theory::ARRAY_BOOL_SELECT : Theory::ARRAY_SELECT; + bool haveSelect = prop->hasInterpretedOperation(arraySelect,Theory::getArrayOperatorType(arraySort,arraySelect)); + bool haveStore = prop->hasInterpretedOperation(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE)); if (haveSelect || haveStore) { unsigned sk = theory->getArrayExtSkolemFunction(arraySort); if (isBool) { - addBooleanArrayExtensionalityAxioms(arraySelect, arrayStore, sk); + addBooleanArrayExtensionalityAxioms(arraySort, sk); } else { - addArrayExtensionalityAxioms(arraySelect, arrayStore, sk); + addArrayExtensionalityAxioms(arraySort, sk); } if (haveStore) { if (isBool) { - addBooleanArrayWriteAxioms(arraySelect, arrayStore); + addBooleanArrayWriteAxioms(arraySort); } else { - addArrayWriteAxioms(arraySelect, arrayStore); + addArrayWriteAxioms(arraySort); } } modified = true; diff --git a/Shell/TheoryAxioms.hpp b/Shell/TheoryAxioms.hpp index b899995ee3..920c187270 100644 --- a/Shell/TheoryAxioms.hpp +++ b/Shell/TheoryAxioms.hpp @@ -89,9 +89,11 @@ static unsigned const EXPENSIVE = 1; Interpretation unaryMinus, TermList zeroElement); void addIntegerDividesAxioms(Interpretation divides, Interpretation multiply, TermList zero, TermList n); - void addBooleanArrayExtensionalityAxioms(Interpretation select, Interpretation store, unsigned skolem); - void addArrayExtensionalityAxioms(Interpretation select, Interpretation store, unsigned skolem); - void addBooleanArrayWriteAxioms(Interpretation select, Interpretation store); + void addBooleanArrayExtensionalityAxioms(unsigned arraySort, unsigned skolem); + void addArrayExtensionalityAxioms(unsigned arraySort, unsigned skolem); + void addBooleanArrayWriteAxioms(unsigned arraySort); + void addArrayWriteAxioms(unsigned arraySort); + void addTupleAxioms(unsigned tupleSort); void addFloorAxioms(Interpretation floor, Interpretation less, Interpretation unaryMinus, Interpretation plus, TermList oneElement); @@ -100,7 +102,6 @@ static unsigned const EXPENSIVE = 1; void addRoundAxioms(Interpretation round, Interpretation floor, Interpretation ceiling); void addTruncateAxioms(Interpretation truncate, Interpretation less, Interpretation unaryMinus, Interpretation plus, TermList zeroElement, TermList oneElement); - void addArrayWriteAxioms(Interpretation select, Interpretation store); // term algebra axioms void addExhaustivenessAxiom(TermAlgebra* ta);