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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
/*
* 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
*/
#ifndef __TERM_ALGEBRA__
#define __TERM_ALGEBRA__
#include "Forwards.hpp"
#include "Lib/Array.hpp"
#include "Lib/Metaiterators.hpp"
#include "Lib/Set.hpp"
#include "Kernel/InductionTemplate.hpp"
#include "Kernel/OperatorType.hpp"
using namespace Kernel;
namespace Shell {
class TermAlgebraConstructor {
public:
/* A term algebra constructor, described by its name, range,
arity, and for each argument: the name of its destructor and
its sort*/
TermAlgebraConstructor(unsigned functor, Lib::Array<unsigned> destructors);
TermAlgebraConstructor(unsigned functor, std::initializer_list<unsigned> destructors);
TermAlgebraConstructor(unsigned functor, unsigned discriminator, Lib::Array<unsigned> destructors);
unsigned arity() const;
unsigned numTypeArguments() const;
TermList argSort(unsigned ith) const;
TermList rangeSort() const;
/* True iff one of the arguments has the same sort as the range */
bool recursive();
/* The numbers of the constructor and destructors functions in the
environment signature. These functions should be called only
after createSymbols() has been called once */
unsigned functor() const { return _functor; }
unsigned destructorFunctor(unsigned ith) const {
ASS_L(ith,arity()-numTypeArguments());
return _destructors[ith];
}
bool hasDiscriminator() { return _hasDiscriminator; }
unsigned discriminator();
class IterArgSorts
{
TermAlgebraConstructor& _self;
unsigned _idx;
public:
DECL_ELEMENT_TYPE(TermList);
IterArgSorts(TermAlgebraConstructor& ta) : _self(ta), _idx(0) {}
bool hasNext() const
{ return _idx < _self.arity(); }
auto next()
{ return _self.argSort(_idx++); }
};
Lib::IterTraits<IterArgSorts> iterArgSorts()
{ return Lib::iterTraits(IterArgSorts(*this)); }
friend std::ostream& operator<<(std::ostream& out, TermAlgebraConstructor const& self);
private:
std::string discriminatorName();
Kernel::OperatorType* _type;
unsigned _functor;
bool _hasDiscriminator;
unsigned _discriminator;
Lib::Array<unsigned> _destructors;
};
typedef Lib::Array<TermAlgebraConstructor*> ConstructorArray;
class TermAlgebra {
public:
/* An algebra described by its name, sort, number of constructors,
the constructors themselves (whose range must be the algebra
sort), and their cyclicity. If allowsCyclicTerms is false, and
the option -tar is not set to off, then the acyclicity rule
will be enforced for terms of this algebra*/
TermAlgebra(TermList sort,
unsigned n,
TermAlgebraConstructor** constrs,
bool allowsCyclicTerms = false);
TermAlgebra(TermList sort,
Lib::Array<TermAlgebraConstructor*> constrs,
bool allowsCyclicTerms = false);
TermAlgebra(TermList sort,
std::initializer_list<TermAlgebraConstructor*> constrs,
bool allowsCyclicTerms = false);
unsigned nTypeArgs() const { return _sort.term()->arity(); }
unsigned nConstructors() const { return _n; }
TermList sort() const { return _sort; }
TermAlgebraConstructor* constructor(unsigned ith) { ASS_L(ith, _n); return _constrs[ith]; }
class IterCons
{
TermAlgebra& _ta;
unsigned _idx;
public:
DECL_ELEMENT_TYPE(TermAlgebraConstructor*);
IterCons(TermAlgebra& ta) : _ta(ta), _idx(0) {}
bool hasNext() const
{ return _idx < _ta.nConstructors(); }
TermAlgebraConstructor* next()
{ return _ta.constructor(_idx++); }
};
Lib::IterTraits<IterCons> iterCons()
{ return Lib::iterTraits(IterCons(*this)); }
/** returns all sorts contained in the term algebra instance `sort`, including `sort` itself.
* consider for example:
* nat ::= S(nat) | Zero
* atree(x) ::= Node(atree(x), x, nat, atree(x)) | Leaf
* intp ::= P(int,int)
*
* then subSorts(atree(intp)) == { int, nat, intp, atree(intp) }
*/
static Lib::Set<TermList> subSorts(TermList sort);
bool allowsCyclicTerms() { return _allowsCyclicTerms; }
/* True iff the algebra defines an empty domain, which could be
due to:
- having no constructors
- not allowing cyclic terms and having only recursive constructors
*/
bool emptyDomain();
/* True iff all the constructors are constants */
bool finiteDomain();
/* True iff one of the constructors is recursive */
bool infiniteDomain();
/* The predicate of the subterm relation, used only if the option
-tac is set to "axiom"*/
std::string getSubtermPredicateName();
unsigned getSubtermPredicate();
void getTypeSub(Kernel::Term* t, Kernel::Substitution& subst);
/**
* These three induction templates correspond to the schemas presented in the CADE 2019 paper.
* Examples use list datatype nil, cons(head,tail)
*
* - one: based on constructors
* (F[nil] ⋀ ∀ x,y. (F[y] → F[cons(x,y)])) → ∀ z. F[z]
*
* - two: based on well-founded induction using subterms
* (∀ x. (x = cons(head(x),tail(x)) → F[tail(x)]) → F[x]) → ∀ y. F[y]
*
* - three: based on well-founded induction using subterm predicate
* (note that this needs the axiomatisation of the subterm predicate)
* (∀ x. (∀ y. (subterm(y,x) → F[y]) → F[x]) → ∀ z. F[z]
*/
/* Constructor-based induction template. */
const InductionTemplate* getInductionTemplateOne();
const InductionTemplate* getInductionTemplateTwo();
const InductionTemplate* getInductionTemplateThree();
/**
* Given a set of (possibly variable) term algebra terms in @b availables
* and a term algebra term @b e, compute a new set of terms in @b availables
* which covers the same term algebra terms, except for terms covered by @b e.
*/
static void excludeTermFromAvailables(Kernel::TermStack& availables, Kernel::TermList e, unsigned& var);
friend std::ostream& operator<<(std::ostream& out, TermAlgebra const& self);
private:
TermList _sort;
unsigned _n; /* number of constructors */
bool _allowsCyclicTerms;
ConstructorArray _constrs;
std::unique_ptr<const InductionTemplate> _indTemplOne;
std::unique_ptr<const InductionTemplate> _indTemplTwo;
std::unique_ptr<const InductionTemplate> _indTemplThree;
};
}
#endif