1 2 /* 3 * File Grounding.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 Grounding.hpp 21 * Defines class Grounding. 22 */ 23 24 #ifndef __Grounding__ 25 #define __Grounding__ 26 27 #include "Forwards.hpp" 28 29 #include "Lib/DArray.hpp" 30 #include "Lib/DHMap.hpp" 31 #include "Lib/Stack.hpp" 32 #include "Lib/VirtualIterator.hpp" 33 34 namespace Shell 35 { 36 37 using namespace Kernel; 38 using namespace Lib; 39 40 class Grounding 41 { 42 public: 43 static ClauseList* simplyGround(ClauseIterator clauses); 44 45 ClauseList* ground(Clause* clause); 46 47 48 static ClauseList* getEqualityAxioms(bool otherThanReflexivity); 49 private: 50 static void getLocalEqualityAxioms(unsigned sort, bool otherThanReflexivity, ClauseList*& acc); 51 52 53 struct GroundingApplicator 54 { 55 GroundingApplicator(); 56 void initForClause(Clause* cl); 57 bool newAssignment(); 58 TermList apply(unsigned var); 59 private: 60 DHMap<unsigned, unsigned, IdentityHash> _varNumbering; 61 Stack<TermList> _constants; 62 DArray<unsigned> _indexes; 63 unsigned _maxIndex; 64 int _varCnt; 65 bool _beforeFirst; 66 }; 67 68 69 GroundingApplicator _ga; 70 }; 71 72 } 73 74 #endif /* __Grounding__ */ 75