1
2 /*
3 * File ConstantRemover.cpp.
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 ConstantRemover.cpp
21 * Implements class ConstantRemover.
22 */
23 #if GNUMP
24
25 #include "Lib/Environment.hpp"
26
27 #include "Kernel/Constraint.hpp"
28 #include "Kernel/Signature.hpp"
29
30 #include "Statistics.hpp"
31
32 #include "ConstantRemover.hpp"
33
34 namespace Shell
35 {
36
37 using namespace Lib;
38 using namespace Kernel;
39
ConstantRemover()40 ConstantRemover::ConstantRemover()
41 : _varCnt(env.signature->vars())
42 {
43 reset();
44 }
45
apply(ConstraintRCList * & lst)46 bool ConstantRemover::apply(ConstraintRCList*& lst)
47 {
48 CALL("ConstantRemover::apply");
49
50 if(!scan(lst)) {
51 reset();
52 return false;
53 }
54
55 bool anyUpdated = false;
56 ConstraintRCList::DelIterator cit(lst);
57 while(cit.hasNext()) {
58 ConstraintRCPtr c0 = cit.next();
59 ConstraintRCPtr c = c0;
60 Constraint::CoeffIterator coeffIt(c0->coeffs());
61 while(coeffIt.hasNext()) {
62 const Constraint::Coeff& coeff = coeffIt.next();
63 Var v = coeff.var;
64 const DefiningPair& d = _vals[v];
65 if(!d.isTight) {
66 continue;
67 }
68 bool needsLeft = coeff.isNegative();
69 c = ConstraintRCPtr(Constraint::resolve(v, *c, needsLeft ? *d.left : *d.right, false));
70 }
71 if(c!=c0) {
72 env.statistics->updatedByConstantPropagation++;
73 anyUpdated = true;
74 if(c->isTautology()) {
75 cit.del();
76 }
77 else {
78 cit.replace(c);
79 }
80 }
81 }
82 ASS(anyUpdated); //at least the constant definition itself should be always removed
83
84 reset();
85 return anyUpdated;
86 }
87
reset()88 void ConstantRemover::reset()
89 {
90 CALL("ConstantRemover::reset");
91
92 _vals.init(_varCnt, DefiningPair());
93 }
94
scan(ConstraintRCList * lst)95 bool ConstantRemover::scan(ConstraintRCList* lst)
96 {
97 CALL("ConstantRemover::scan");
98
99 ConstraintRCList::Iterator cit(lst);
100 while(cit.hasNext()) {
101 ConstraintRCPtr c = cit.next();
102 if(c->coeffCnt()!=1 || c->type()!=CT_GREQ) {
103 continue;
104 }
105 const Constraint::Coeff& coeff = (*c)[0];
106 Var v = coeff.var;
107 bool left = coeff.isPositive();
108
109 //Here we simply assign into appropriate field in the _vals array.
110 //We ignore the fact that there can be multiple bounds of the
111 //same type for one variable. We can do this because the
112 //SubsumptionRemover will eventually ensure there will remain only
113 //the strictest bound.
114 if(left) {
115 _vals[v].left = c;
116 }
117 else {
118 _vals[v].right = c;
119 }
120 }
121
122 bool haveConstant = false;
123 for(Var v = 0; v<_varCnt; v++) {
124 DefiningPair& d = _vals[v];
125 if(!d.left || !d.right || d.left->freeCoeff()!=-d.right->freeCoeff()
126 || (*d.left)[0].value!=-(*d.right)[0].value) {
127 continue;
128 }
129 d.isTight = true;
130 haveConstant = true;
131 env.statistics->constantVariables++;
132 }
133
134 return haveConstant;
135 }
136
137
138 }
139 #endif //GNUMP
140
141