1
2 /*
3 * File TermAlgebra.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 #include "Kernel/Clause.hpp"
20 #include "Kernel/Formula.hpp"
21 #include "Kernel/FormulaUnit.hpp"
22 #include "Kernel/Inference.hpp"
23
24 using namespace Kernel;
25 using namespace Lib;
26
27 namespace Shell {
28
TermAlgebraConstructor(unsigned functor,Lib::Array<unsigned> destructors)29 TermAlgebraConstructor::TermAlgebraConstructor(unsigned functor, Lib::Array<unsigned> destructors)
30 : _functor(functor), _hasDiscriminator(false), _destructors(destructors)
31 {
32 _type = env.signature->getFunction(_functor)->fnType();
33 ASS_REP(env.signature->getFunction(_functor)->termAlgebraCons(), env.signature->functionName(_functor));
34 ASS_EQ(_type->arity(), destructors.size());
35 }
36
TermAlgebraConstructor(unsigned functor,unsigned discriminator,Lib::Array<unsigned> destructors)37 TermAlgebraConstructor::TermAlgebraConstructor(unsigned functor, unsigned discriminator, Lib::Array<unsigned> destructors)
38 : _functor(functor), _hasDiscriminator(true), _discriminator(discriminator), _destructors(destructors)
39 {
40 _type = env.signature->getFunction(_functor)->fnType();
41 ASS_REP(env.signature->getFunction(_functor)->termAlgebraCons(), env.signature->functionName(_functor));
42 ASS_EQ(_type->arity(), destructors.size());
43 }
44
arity()45 unsigned TermAlgebraConstructor::arity() { return _type->arity(); }
argSort(unsigned ith)46 unsigned TermAlgebraConstructor::argSort(unsigned ith) { return _type->arg(ith); }
rangeSort()47 unsigned TermAlgebraConstructor::rangeSort() { return _type->result(); }
48
recursive()49 bool TermAlgebraConstructor::recursive()
50 {
51 CALL("TermAlgebraConstructor::recursive");
52
53 for (unsigned i=0; i < _type->arity(); i++) {
54 if (_type->arg(i) == _type->result()) {
55 // this constructor has a recursive argument
56 return true;
57 }
58 }
59 return false;
60 }
61
discriminatorName()62 Lib::vstring TermAlgebraConstructor::discriminatorName()
63 {
64 CALL("TermAlgebraConstructor::discriminatorName");
65
66 return "$is" + env.signature->functionName(_functor);
67 }
68
TermAlgebra(unsigned sort,unsigned n,TermAlgebraConstructor ** constrs,bool allowsCyclicTerms)69 TermAlgebra::TermAlgebra(unsigned sort,
70 unsigned n,
71 TermAlgebraConstructor** constrs,
72 bool allowsCyclicTerms) :
73 _sort(sort),
74 _n(n),
75 _allowsCyclicTerms(allowsCyclicTerms),
76 _constrs(n)
77 {
78 for (unsigned i = 0; i < n; i++) {
79 ASS(constrs[i]->rangeSort() == _sort);
80 _constrs[i] = constrs[i];
81 }
82 }
83
emptyDomain()84 bool TermAlgebra::emptyDomain()
85 {
86 CALL("TermAlgebra::emptyDomain");
87
88 if (_n == 0) {
89 return true;
90 }
91
92 if (_allowsCyclicTerms) {
93 return false;
94 }
95
96 for (unsigned i = 0; i < _n; i++) {
97 if (!(_constrs[i]->recursive())) {
98 return false;
99 }
100 }
101 return true;
102 }
103
finiteDomain()104 bool TermAlgebra::finiteDomain()
105 {
106 CALL("TermAlgebra::finiteDomain");
107
108 for (unsigned i = 0; i < _n; i++) {
109 if (_constrs[i]->arity() > 0) {
110 return false;
111 }
112 }
113
114 return true;
115 }
116
infiniteDomain()117 bool TermAlgebra::infiniteDomain()
118 {
119 CALL("TermAlgebra::infiniteDomain");
120
121 for (unsigned i = 0; i < _n; i++) {
122 if (_constrs[i]->recursive()) {
123 return true;
124 }
125 }
126
127 return false;
128 }
129
getSubtermPredicateName()130 Lib::vstring TermAlgebra::getSubtermPredicateName() {
131 return "$subterm" + env.sorts->sortName(_sort);
132 }
133
getSubtermPredicate()134 unsigned TermAlgebra::getSubtermPredicate() {
135 CALL("TermAlgebra::getSubtermPredicate");
136
137 bool added;
138 unsigned s = env.signature->addPredicate(getSubtermPredicateName(), 2, added);
139
140 if (added) {
141 // declare a binary predicate subterm
142 Stack<unsigned> args;
143 args.push(_sort); args.push(_sort);
144 env.signature->getPredicate(s)->setType(OperatorType::getPredicateType(args.size(),args.begin()));
145 }
146
147 return s;
148 }
149
150 }
151