Home
last modified time | relevance | path

Searched refs:TermEnumMaster (Results 1 – 2 of 2) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsygus_enumerator.h213 class TermEnumMaster; variable
303 class TermEnumMaster : public TermEnum
306 TermEnumMaster();
427 std::map<TypeNode, TermEnumMaster> d_masterEnum;
H A Dsygus_enumerator.cpp549 std::map<TypeNode, TermEnumMaster>::iterator it = d_masterEnum.find(tn); in getMasterEnumForType()
589 SygusEnumerator::TermEnumMaster::TermEnumMaster() in TermEnumMaster() function in CVC4::theory::quantifiers::SygusEnumerator::TermEnumMaster
601 bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se, in initialize()
621 Node SygusEnumerator::TermEnumMaster::getCurrent() in getCurrent()
651 bool SygusEnumerator::TermEnumMaster::increment() in increment()
676 bool SygusEnumerator::TermEnumMaster::incrementInternal() in incrementInternal()
897 bool SygusEnumerator::TermEnumMaster::initializeChildren() in initializeChildren()
938 bool SygusEnumerator::TermEnumMaster::initializeChild(unsigned i, in initializeChild()