Searched refs:destructorFunctor (Results 1 – 5 of 5) sorted by relevance
54 unsigned destructorFunctor(unsigned ith) { return _destructors[ith]; } in destructorFunctor() function in Shell::TermAlgebraConstructor
1195 Literal* lit = Literal::create1(c->destructorFunctor(j), true, x); in addExhaustivenessAxiom()1199 Term* t = Term::create1(c->destructorFunctor(j), x); in addExhaustivenessAxiom()
1040 unsigned destructorFunctor = isPredicate ? env.signature->addPredicate(destructorName, 1, added) in buildTermAlgebraConstructor() local1050 env.signature->getPredicate(destructorFunctor)->setType(destructorType); in buildTermAlgebraConstructor()1052 env.signature->getFunction(destructorFunctor)->setType(destructorType); in buildTermAlgebraConstructor()1055 ALWAYS(_declaredFunctions.insert(destructorName, make_pair(destructorFunctor, !isPredicate))); in buildTermAlgebraConstructor()1057 destructorFunctors[i] = destructorFunctor; in buildTermAlgebraConstructor()
544 unsigned dj = con->destructorFunctor(j); in performStructInductionTwo()643 unsigned dj = con->destructorFunctor(j); in performStructInductionThree()
1217 return c->destructorFunctor(proj); in getProjectionFunctor()1243 if (projFunctor == c->destructorFunctor(i)) { in findProjection()