1 
2 /*
3  * File EqualityVariableRemover.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 EqualityVariableRemover.hpp
21  * Defines class EqualityVariableRemover.
22  */
23 
24 #ifndef __EqualityVariableRemover__
25 #define __EqualityVariableRemover__
26 #if GNUMP
27 #include "Forwards.hpp"
28 
29 #include "Lib/Set.hpp"
30 
31 #include "Kernel/V2CIndex.hpp"
32 
33 namespace Shell {
34 
35 using namespace Lib;
36 using namespace Kernel;
37 
38 class EqualityVariableRemover {
39 public:
EqualityVariableRemover()40   EqualityVariableRemover() { reset(); }
41 
42   bool apply(ConstraintRCList*& lst);
43 private:
44   void reset();
45   void scan(ConstraintRCList* lst);
46 
47   Var getEliminatedVariable(Constraint& c);
48 
49   void eliminate(Constraint* c, ConstraintRCList*& lst);
50 
51   bool allowedEquality(Constraint& c);
52 
53   struct ConstraintHash
54   {
55     static unsigned hash(const Constraint* c);
56     static bool equals(const Constraint* c1, const Constraint* c2);
57   };
58 
59   Set<Constraint*,ConstraintHash> _halves;
60   DHMap<Constraint*, Constraint*> _equalities;
61   V2CIndex _v2c;
62 };
63 
64 }
65 #endif //GNUMP
66 #endif // __EqualityVariableRemover__
67