1 2 /* 3 * File Property.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file Property.hpp (syntactic properties of problems) 21 * 22 * @since 06/06/2001 Manchester 23 * @since 17/07/2003 Manchester, changed to new representation 24 * @since 02/12/2003 Manchester, allocation changed to use Allocator 25 * @since 20/05/2007 Manchester, changed to new term representation 26 */ 27 28 29 #ifndef __Property__ 30 #define __Property__ 31 32 #include "Lib/DArray.hpp" 33 #include "Lib/Array.hpp" 34 #include "Lib/DHSet.hpp" 35 #include "Kernel/Unit.hpp" 36 #include "Kernel/Theory.hpp" 37 #include "Lib/VString.hpp" 38 #include "SMTLIBLogic.hpp" 39 40 namespace Kernel { 41 class Clause; 42 class FormulaUnit; 43 class Literal; 44 class Term; 45 class TermList; 46 class Formula; 47 } 48 49 namespace Shell { 50 51 using namespace std; 52 using namespace Kernel; 53 using namespace Lib; 54 55 /** 56 * Represents syntactic properties of problems. 57 */ 58 class Property 59 { 60 public: 61 /** 62 * CASC category 63 */ 64 enum Category { 65 NEQ, 66 HEQ, 67 PEQ, 68 HNE, 69 NNE, 70 FEQ, 71 FNE, 72 EPR, 73 UEQ 74 }; 75 76 // Various boolean properties. 77 /** CNF of the problem has a positive literal x=y */ 78 static const uint64_t PR_HAS_X_EQUALS_Y = 1ul; // 2^0 79 /** Problem has function definitions f(X) = t[X] */ 80 static const uint64_t PR_HAS_FUNCTION_DEFINITIONS = 2ul; // 2^1 81 /** Problem contains a subset axiom */ 82 static const uint64_t PR_HAS_SUBSET = 4ul; // 2^2 83 /** Problem contains extensionality axiom */ 84 static const uint64_t PR_HAS_EXTENSIONALITY = 8ul; // 2^3 85 /** Problem contains an axiomatisation of group theory */ 86 static const uint64_t PR_GROUP = 16ul; // 2^4 87 /** Problem contains an axiomatisation of ring theory */ 88 static const uint64_t PR_RING = 32ul; // 2^5 89 /** Problem contains an axiomatisation of robbins algebras */ 90 static const uint64_t PR_ROBBINS_ALGEBRA = 64ul; // 2^6 91 /** Problem contains an axiomatisation of non-associative rings */ 92 static const uint64_t PR_NA_RING = 128ul; // 2^7 93 /** Problem contains an axiomatisation of boolean algebras */ 94 static const uint64_t PR_BOOLEAN_ALGEBRA = 256ul; // 2^8 95 /** Problem contains an axiomatisation of lattice theory */ 96 static const uint64_t PR_LATTICE = 512ul; // 2^9 97 /** Problem contains an axiomatisation of lattice-ordered groups */ 98 static const uint64_t PR_LO_GROUP = 1024ul; // 2^10 99 /** Problem contains an axiomatisation of the B combinator */ 100 static const uint64_t PR_COMBINATOR_B = 2048ul; // 2^11 101 /** Problem contains an axiomatisation of a combinator S,T,O or Q */ 102 static const uint64_t PR_COMBINATOR = 4096ul; // 2^12 103 /** Problem contains the condensed detachment axiom 104 * ~theorem(X) \/ ~theorem(imply(X,Y)) \/ theorem(Y) */ 105 static const uint64_t PR_HAS_CONDENSED_DETACHMENT1 = 8192ul; // 2^13 106 /** Problem contains the condensed detachment axiom 107 * ~theorem(X) \/ ~theorem(or(not(X),Y)) \/ theorem(Y) */ 108 static const uint64_t PR_HAS_CONDENSED_DETACHMENT2 = 16384ul; // 2^14 109 /** field axioms from TPTP */ 110 static const uint64_t PR_HAS_FLD1 = 32768ul; // 2^15 111 /** other field axioms from TPTP */ 112 static const uint64_t PR_HAS_FLD2 = 65536ul; // 2^16 113 /** Problem contains literal X=t with t non-containing X */ 114 static const uint64_t PR_HAS_INEQUALITY_RESOLVABLE_WITH_DELETION = 131072ul; // 2^17 115 /** Uses string sort */ 116 static const uint64_t PR_HAS_STRINGS = 262144ul; // 2^18 117 /** Uses integer sort */ 118 static const uint64_t PR_HAS_INTEGERS = 524288ul; // 2^19 119 /** Uses rational sort */ 120 static const uint64_t PR_HAS_RATS = 1048576ul; // 2^20 121 /** Uses real sort */ 122 static const uint64_t PR_HAS_REALS = 2097152ul; // 2^21 123 /** Has sort declarations */ 124 static const uint64_t PR_SORTS = 4194304ul; // 2^22 125 /** Uses integer comparisons $less, $lesseq, $greater, $greatereq */ 126 static const uint64_t PR_INTEGER_COMPARISON = 8388608ul; // 2^23 127 /** Uses rational comparisons $less, $lesseq, $greater, $greatereq */ 128 static const uint64_t PR_RAT_COMPARISON = 16777216ul; // 2^24 129 /** Uses real comparisons $less, $lesseq, $greater, $greatereq */ 130 static const uint64_t PR_REAL_COMPARISON = 33554432ul; // 2^25 131 /** Uses integer functions $uminus,$sum,$difference */ 132 static const uint64_t PR_INTEGER_LINEAR = 67108864ul; // 2^26 133 /** Uses rational functions $uminus,$sum,$difference */ 134 static const uint64_t PR_RAT_LINEAR = 134217728ul; // 2^27 135 /** Uses real functions $uminus,$sum,$difference */ 136 static const uint64_t PR_REAL_LINEAR = 268435456ul; // 2^28 137 /** Uses integer non-linear functions $product,$quotient,$remainder */ 138 static const uint64_t PR_INTEGER_NONLINEAR = 536870912ul; // 2^29 139 /** Uses integer non-linear functions $product,$quotient,$remainder */ 140 static const uint64_t PR_RAT_NONLINEAR = 1073741824ul; // 2^30 141 /** Uses integer non-linear functions $product,$quotient,$remainder */ 142 static const uint64_t PR_REAL_NONLINEAR = 2147483648ul; // 2^31 143 /** Uses number conversion functions $floor, $ceiling, $truncate, $round, $is_int, $is_rat, $to_int, $to_int, $to_rat, $to_real */ 144 static const uint64_t PR_NUMBER_CONVERSION = 4294967296ul; // 2^32 145 /** when skolemised, will become ground, probably useless */ 146 static const uint64_t PR_ESSENTIALLY_GROUND = 8589934592ul; // 2^33 147 /** uses list axioms */ 148 static const uint64_t PR_LIST_AXIOMS = 17179869184ul; // 2^34 149 /** uses boolean variables */ 150 static const uint64_t PR_HAS_BOOLEAN_VARIABLES = 34359738368ul; // 2^35 151 /** uses Arrays, should these be split? */ 152 static const uint64_t PR_HAS_ARRAYS = 68719476736ul; // 2^36 153 /** has a finite domain axiom */ 154 static const uint64_t PR_HAS_FINITE_DOMAIN = 137438953472ul; // 2^37 155 /** has if-then-else */ 156 static const uint64_t PR_HAS_ITE = 274877906944ul; // 2^38 157 /** has let-in */ 158 static const uint64_t PR_HAS_LET_IN = 549755813888ul; // 2^39 159 /* has data type constructors */ 160 static const uint64_t PR_HAS_DT_CONSTRUCTORS = 1099511627776ul; // 2^40 161 /* has co-algrebaic data type constructors */ 162 static const uint64_t PR_HAS_CDT_CONSTRUCTORS = 2199023255552ul; // 2^41 163 164 public: 165 CLASS_NAME(Property); 166 USE_ALLOCATOR(Property); 167 168 static Property* scan(UnitList*); 169 void add(UnitList*); 170 ~Property(); 171 172 /** Return the CASC category of the problem */ category() const173 Category category() const { return _category;} 174 static vstring categoryToString(Category cat); 175 vstring categoryString() const; 176 177 vstring toString() const; 178 vstring toSpider(const vstring& problemName) const; 179 180 /** Total number of clauses in the problem. */ clauses() const181 int clauses() const { return _goalClauses + _axiomClauses; } 182 /** Total number of formulas in the problem */ formulas() const183 int formulas() const { return _goalFormulas + _axiomFormulas; } 184 /** Total number of unit clauses in the problem */ unitClauses() const185 int unitClauses() const { return _unitGoals + _unitAxioms; } 186 /** Total number of Horn clauses in the problem */ hornClauses() const187 int hornClauses() const { return _hornGoals + _hornAxioms; } 188 /** Total number of atoms in the problem */ atoms() const189 int atoms() const { return _atoms; } 190 /** Total number of equality atoms in the problem */ equalityAtoms() const191 int equalityAtoms() const { return _equalityAtoms; } 192 /** Total number of positive equality atoms in the problem, does not work correctly 193 with formulas since polarity is not taken into account */ positiveEqualityAtoms() const194 int positiveEqualityAtoms() const { return _positiveEqualityAtoms; } 195 /** True if has formulas */ hasFormulas() const196 bool hasFormulas() const { return _axiomFormulas || _goalFormulas; } 197 /** Maximal arity of a function in the problem */ maxFunArity() const198 int maxFunArity() const { return _maxFunArity; } 199 /** Total number of variables in problem */ totalNumberOfVariables() const200 int totalNumberOfVariables() const { return _totalNumberOfVariables;} 201 202 /** The problem has property p */ hasProp(uint64_t p) const203 bool hasProp(uint64_t p) const { return _props & p; } 204 /** Add property p to the list of properties */ addProp(uint64_t p)205 void addProp(uint64_t p) { _props |= p; } 206 /** Remove a property from the list of properties */ dropProp(uint64_t p)207 void dropProp(uint64_t p) { _props &= ~p; } 208 /** Return props as an integer, mainly for debugging */ props() const209 uint64_t props() const { return _props; } 210 211 /** 212 * To be used from outside of the Property class when a preprocessing 213 * rule may add into problem new operation 214 * 215 * @c t may be either a term or a literal 216 */ 217 void scanForInterpreted(Term* t); 218 hasInterpretedOperation(Interpretation i) const219 bool hasInterpretedOperation(Interpretation i) const { 220 if(i >= _interpretationPresence.size()){ return false; } 221 return _interpretationPresence[i]; 222 } hasInterpretedOperation(Interpretation i,OperatorType * type) const223 bool hasInterpretedOperation(Interpretation i, OperatorType* type) const { 224 return _polymorphicInterpretations.find(std::make_pair(i,type)); 225 } 226 227 /** Problem contains an interpreted symbol excluding equality */ hasInterpretedOperations() const228 bool hasInterpretedOperations() const { return _hasInterpreted; } hasInterpretedEquality() const229 bool hasInterpretedEquality() const { return _hasInterpretedEquality; } 230 /** Problem contains non-default sorts */ hasNonDefaultSorts() const231 bool hasNonDefaultSorts() const { return _hasNonDefaultSorts; } hasFOOL() const232 bool hasFOOL() const { return _hasFOOL; } usesSort(unsigned sort) const233 bool usesSort(unsigned sort) const { 234 CALL("Property::usesSort"); 235 if(_usesSort.size() <= sort) return false; 236 return _usesSort[sort]; 237 } usesSingleSort() const238 bool usesSingleSort() const { return _sortsUsed==1; } sortsUsed() const239 unsigned sortsUsed() const { return _sortsUsed; } onlyFiniteDomainDatatypes() const240 bool onlyFiniteDomainDatatypes() const { return _onlyFiniteDomainDatatypes; } knownInfiniteDomain() const241 bool knownInfiniteDomain() const { return _knownInfiniteDomain; } 242 setSMTLIBLogic(SMTLIBLogic smtLibLogic)243 void setSMTLIBLogic(SMTLIBLogic smtLibLogic) { 244 CALL("Property::setSMTLIBLogic"); 245 _smtlibLogic = smtLibLogic; 246 } getSMTLIBLogic() const247 SMTLIBLogic getSMTLIBLogic() const { 248 return _smtlibLogic; 249 } 250 allNonTheoryClausesGround()251 bool allNonTheoryClausesGround(){ return _allNonTheoryClausesGround; } 252 253 private: 254 // constructor, operators new and delete 255 explicit Property(); 256 257 static bool hasXEqualsY(const Clause* c); 258 static bool hasXEqualsY(const Formula*); 259 260 // reading in properties of problems 261 void scan(Unit*); 262 263 // these two are the only ones which start the deep iteration 264 void scan(Clause*); 265 void scan(FormulaUnit*); 266 267 void scan(Literal* lit, int polarity, unsigned cLen, bool goal); 268 void scan(Formula*, int polarity); 269 void scan(TermList ts,bool unit,bool goal); 270 271 void scanSort(unsigned sort); 272 273 char axiomTypes() const; 274 char goalTypes() const; 275 char equalityContent() const; 276 char nonGroundUnitContent() const; 277 char groundPositiveContent() const; 278 char goalsAreGround() const; 279 char setClauseSize() const; 280 char setLiteralSize() const; 281 char setTermSize() const; 282 char maxPredArity() const; 283 284 // structure 285 int _goalClauses; 286 int _axiomClauses; 287 288 int _positiveEqualityAtoms; 289 int _equalityAtoms; 290 int _atoms; 291 292 int _goalFormulas; 293 int _axiomFormulas; 294 int _subformulas; 295 296 int _terms; 297 int _unitGoals; 298 int _unitAxioms; 299 int _hornGoals; 300 int _hornAxioms; 301 int _equationalClauses; 302 int _pureEquationalClauses; 303 int _groundUnitAxioms; 304 int _positiveAxioms; 305 int _groundPositiveAxioms; 306 int _groundGoals; 307 int _maxFunArity; 308 int _maxPredArity; 309 310 /** Number of variables in this clause, used during counting */ 311 int _variablesInThisClause; 312 /** Total number of variables in all clauses */ 313 int _totalNumberOfVariables; 314 /** Maximal number of variables in a clause */ 315 int _maxVariablesInClause; 316 /** Symbols in this formula, used during counting 317 Functions are positive, predicates stored in the negative part 318 **/ 319 DHSet<int>* _symbolsInFormula; 320 321 /** Bitwise OR of all properties of this problem */ 322 uint64_t _props; 323 324 /** CASC category of the problem, computed by read() */ 325 Category _category; 326 327 /** Problem contains an interpreted symbol including equality */ 328 bool _hasInterpreted; 329 bool _hasInterpretedEquality; 330 /** Problem contains non-default sorts */ 331 bool _hasNonDefaultSorts; 332 unsigned _sortsUsed; 333 Array<bool> _usesSort; 334 335 /** Makes sense for all interpretations, but for polymorphic ones we also keep 336 * the more precise information about which monomorphisations are present (see below). 337 */ 338 DArray<bool> _interpretationPresence; 339 DHSet<Theory::MonomorphisedInterpretation> _polymorphicInterpretations; 340 341 bool _hasFOOL; 342 343 bool _onlyFiniteDomainDatatypes; 344 bool _knownInfiniteDomain; 345 346 bool _allClausesGround; 347 bool _allNonTheoryClausesGround; 348 bool _allQuantifiersEssentiallyExistential; 349 SMTLIBLogic _smtlibLogic; 350 }; // class Property 351 352 } 353 354 #endif // __Property__ 355