1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
#include "Inferences/ALASCA/FwdDemodulation.hpp"
#include "Saturation/SaturationAlgorithm.hpp"
#define DEBUG(...) // DBG(__VA_ARGS__)
using Demod = Inferences::ALASCA::Demodulation;
////////////////////////////////////////////////////////////////////////////////////////////////////
// INDEXING
////////////////////////////////////////////////////////////////////////////////////////////////////
namespace Inferences {
namespace ALASCA {
void FwdDemodulation::attach(SaturationAlgorithm* salg)
{
ForwardSimplificationEngine::attach(salg);
_index = _salg->getSimplifyingIndex<AlascaIndex<Demodulation::Lhs>>();
_index->setShared(_shared);
}
void FwdDemodulation::detach()
{
ASS(_salg);
_index = nullptr;
ForwardSimplificationEngine::detach();
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// RULE APPLICATION
////////////////////////////////////////////////////////////////////////////////////////////////////
/**
* Perform forward simplification on @b cl
*
* Return true if the simplification is applicable on @b cl,
* set @b replacement to a replacing clause if there is one (otherwise keep @b replacement = nullptr)
*
* @b premises will contain clauses that justify the simplification
* performed.
*/
bool FwdDemodulation::perform(Clause* toSimplify, Clause*& replacement, ClauseIterator& premises)
{
ASS_EQ(replacement, NULL)
Stack<Literal*> simplified;
for (auto rhs : Rhs::iter(*_shared, toSimplify)) {
// DEBUG("simplifyable position: ", pos.term, " in ", *pos.lit)
for (auto lhs : _index->generalizations(rhs.term)) {
auto simplified = Demodulation::apply(*_shared, *lhs.data, rhs);
if (simplified.isSome()) {
replacement = simplified.unwrap();
premises = pvi(iterItems(lhs.data->clause()));
return true;
}
}
}
premises = ClauseIterator::getEmpty();
return false;
}
} // namespace ALASCA
} // namespace Inferences