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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
/*
* 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 Naming.hpp
* Defines the naming technique
* @since 05/05/2005 Manchester
* @since 07/07/2007 Manchester, changed to new datastructures
*/
#ifndef __Naming__
#define __Naming__
#include "Kernel/Formula.hpp"
using namespace Kernel;
namespace Shell {
/**
* Class implementing the naming technique.
* @since 05/05/2005 Manchester
*/
class Naming
{
public:
Naming (int threshold, bool preserveEpr, bool appify);
FormulaUnit* apply(FormulaUnit* unit,UnitList*& defs);
private:
/** Encodes information about the position of the sub formula */
enum Where {
/** the subformula is only in the range of conjunctions */
ON_TOP,
/** the subformula is in the range of at least one equivalence */
UNDER_IFF,
/** the subformula has a positive polarity but has at least one
* disjunction above */
OTHER
};
/** Encodes phases in the iterative processing (see apply_iter)
* of the originally recursive (see apply_sub and apply_list) algorithm */
enum ApplyWhat {
APPLY_SUB_TOP,
APPLY_SUB_AND,
APPLY_SUB_OR,
APPLY_SUB_IFFXOR,
APPLY_SUB_FORALLEXISTS,
APPLY_LIST_TOP,
APPLY_LIST_POST
};
/** Encode what apply_sub returns (where pos and neg were originally passed by reference) */
struct ResultSub {
int pos;
int neg;
Formula* res;
};
/** Encode what apply_list returns (results and negResults live on heap) */
struct ResultList {
FormulaList* res;
};
/** Encode either ResultSub or ResultList*/
union Result {
ResultSub resSub;
ResultList resList;
};
/** Store local variables to survive recursive calls -- for the AND/OR sub-case*/
struct SubtaskAndOr {
int* cls;
int* negCls;
};
/** Store local variables to survive recursive calls -- for the FORALL/EXISTS sub-case*/
struct SubtaskForallExists {
bool varFlagSet;
};
/** Store apply_sub input and local variables */
struct TaskApplySub {
Formula* f;
Where where;
union {
SubtaskAndOr taskAndOr;
SubtaskForallExists taskForallExists;
};
};
/** Store apply_list input and local variables */
struct TaskApplyList {
FormulaList* fs;
Where where;
int* results;
int* negResults;
};
/** Encode data needed for simulating a recursive of either apply_sub or apply_list. */
struct Task {
ApplyWhat fncTag; // distinguish the two cases
union {
TaskApplySub taskApplySub;
TaskApplyList taskApplyList;
};
};
/** Threshold for naming. If a non-unit clause is going to be used
* the number of times greater than of equal to the threshold,
* it will be named.
*/
int _threshold;
/**
* Marks if we want to avoid causing introduction of any non-zero
* arity skolem functions
*
* Corresponds to the value of the epr_preserving_naming option.
*/
bool _preserveEpr;
bool _appify; // higher-order stuff
/**
* True if there are universally quantified variables at the scope of the current formula
*
* This value is maintained in the @b apply(Formula,Where,int&,int&) function
* if the @b _preserveEpr value is true.
*/
bool _varsInScope;
bool canBeInDefinition(Formula* f,Where where);
/** The list of definitions produced by naming for this unit*/
UnitList* _defs;
/** Replaces the two functions below with a non-recursive implementation. */
Formula* apply_iter(Formula* top_f);
Formula* apply_sub(Formula* subformula,Where where,int& pos,int& neg);
FormulaList* apply_list(FormulaList* subformulas,
Where where,
int* results,
int* resultsNeg);
Formula* introduceDefinition(Formula* f,bool iff);
Literal* getDefinitionLiteral(Formula* f, VList* freeVars);
}; // class Naming
}
#endif