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