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
/*
* 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 FOOLElimination.hpp
* Defines class FOOLElimination.
*/
#ifndef __FOOLElimination__
#define __FOOLElimination__
#include "Forwards.hpp"
using namespace Kernel;
using namespace Shell;
/**
* A class with function @b apply() that eliminates all expressions
* that are not syntactically first-order, that is:
* - formulas in term context
* - terms in formula context
* - $ite-terms
* - $let-terms
*/
class FOOLElimination {
public:
FOOLElimination();
void apply(Problem& prb);
void apply(UnitList*& units);
/** Check if the unit contains expressions that are not syntactically first-order */
static bool needsElimination(FormulaUnit* unit);
private:
FormulaUnit* apply(FormulaUnit* fu);
/** The currently processed unit */
Unit* _unit;
/** A list of definitions, produced during preprocessing */
UnitList* _defs;
/** A list of definitions (a sublist of the above, but not sharing memory),
* relevant to the currently processed unit. To become part of its premises. */
UnitList* _currentDefs;
bool _higherOrder;
bool _polymorphic;
/** Add a new definitions to _defs */
void addDefinition(FormulaUnit* unit);
/** Lexical scope of the current unit */
DHMap<unsigned,TermList> _varSorts;
/** Process a given part of the unit */
FormulaList* process(FormulaList* fs);
Formula* process(Formula* f);
// A context in one of two possible values, so we model it with bool constants
typedef bool Context;
static const Context TERM_CONTEXT = true;
static const Context FORMULA_CONTEXT = false;
// Processing of TermList and Term* returns a TermList or a Formula*,
// depending on the context
void process(TermList ts, Context context, TermList& termResult, Formula*& formulaResult);
void process(Term* term, Context context, TermList& termResult, Formula*& formulaResult);
// Shortcuts for process(TermList)
TermList process(TermList terms);
Formula* processAsFormula(TermList terms);
// Shortcuts for process(Term*)
TermList process(Term* term);
Formula* processAsFormula(Term* term);
// Depending on the context, build an equivalence or an equality
// between pairs of arguments
static Formula* buildEq(Context context, Formula* lhsFormula, Formula* rhsFormula,
TermList lhsTerm, TermList rhsTerm, TermList termSort);
static void buildApplication(unsigned function, Context context, TermStack& vars,
TermList& functionApplication, Formula*& predicateApplication);
// Creates a stack of sorts for the given variables, using the sorting
// context of the current formula
void collectSorts(VList* vars, TermStack& typeVars, TermStack& termVars, TermStack& allVars, TermStack& termVarSorts);
// Converts a boolean term t to a formula 't = true'
static Formula* toEquality(TermList booleanTerm);
// Introduces a fresh predicate or function (depending on the context) symbol
// with given arguments and result sort
static unsigned introduceFreshSymbol(Context context, const char* prefix,
TermStack sorts, TermList resultSort, unsigned typeArgsArity);
// In order to add some meaning to a fresh symbol we prefix it with a given string
// Three different prefixes for three kinds of fresh symbols
static const char* ITE_PREFIX;
static const char* LET_PREFIX;
static const char* BOOL_PREFIX;
static const char* MATCH_PREFIX;
// Report that a given formula or a term has been rewritten during defooling
// The term or formula is passed as its string representation
static void reportProcessed(std::string inputRepr, std::string outputRepr);
};
#endif // __FOOLElimination__