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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
/*
* 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
*/
/**
* @file EqualityProxy.hpp
* Defines class EqualityProxy implementing the equality proxy transformation.
*/
#ifndef __EqualityProxyMono__
#define __EqualityProxyMono__
#include "Forwards.hpp"
#include "Kernel/Term.hpp"
#include "Options.hpp"
namespace Shell {
using namespace Lib;
using namespace Kernel;
// Monomorphic version of equality proxy transformation.
// When working with a monomorphic problem, both the poly and the mono
// versions can be used. Poly is default.
/**
* Applies the equality proxy transformation to the problem.
* It works as follows:
* <ol>
* <li>All literals s=t are replaced by E(s,t);</li>
* <li>all literals s != t are replaced by ~E(s,t);</li>
* <li>the clause E(x,x) is added;</li>
* <li>if _option is in {EP_RS,EP_RST,EP_RSTC} the symmetry clause ~E(x,y) \/ E(y,x) is added;</li>
* <li>if _option is in {EP_RST,EP_RSTC} the transitivity clause
* ~E(x,y) \/ ~E(y,z) \/ E(x,z) is added;</li>
* <li>if _option == EP_RSTC the congruence clauses are added:
* <ul>
* <li> ~E(x1,y1) \/ ... \/ ~E(xN,yN) \/ ~p(x1,...,xN) \/ p(y1,...,yN)
* for all predicates p except equality and E </li>
* <li> ~E(x1,y1) \/ ... \/ ~E(xN,yN) \/ E(f(x1,...,xN),f(y1,...,yN))
* for all non-constant functions f </li>
* </ul>
* </li>
* </ol>
*/
class EqualityProxyMono
{
public:
EqualityProxyMono(Options::EqualityProxy opt);
void apply(Problem& prb);
/** Reset static caches (for library use when running multiple proofs) */
static void resetStaticCaches();
void apply(UnitList*& units);
Clause* apply(Clause* cl);
private:
void addLocalAxioms(UnitList*& units, TermList sort);
void addAxioms(UnitList*& units);
void addCongruenceAxioms(UnitList*& units);
bool getArgumentEqualityLiterals(unsigned cnt, LiteralStack& lits, Stack<TermList>& vars1,
Stack<TermList>& vars2, OperatorType* symbolType, bool skipSortsWithoutEquality);
Literal* apply(Literal* lit);
Literal* makeProxyLiteral(bool polarity, TermList arg0, TermList arg1, TermList sort);
bool haveProxyPredicate(TermList sort) const;
unsigned getProxyPredicate(TermList sort);
Clause* createEqProxyAxiom(const LiteralStack& literalIt);
/** the equality proxy option value, passed in the constructor */
Options::EqualityProxy _opt;
/**
* Proxy predicate numbers for each sort (which can be a complex term, even in mono - think arrays)
* but must be ground (and shared).
*/
static DHMap<TermList, unsigned> s_proxyPredicates;
/** equality proxy predicate sorts */
static DHMap<unsigned,TermList> s_proxyPredicateSorts;
/** array of proxy definitions E(x,y) <=> x = y */
static DHMap<TermList, Unit*> s_proxyPremises;
};
};
#endif /* __EqualityProxy__ */