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