Searched refs:SharedTermsDatabase (Results 1 – 5 of 5) sorted by relevance
26 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, in SharedTermsDatabase() function in CVC4::SharedTermsDatabase42 SharedTermsDatabase::~SharedTermsDatabase() in ~SharedTermsDatabase()47 void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { in addEqualityToPropagate()71 SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const { in begin()76 SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const { in end()81 bool SharedTermsDatabase::hasSharedTerms(TNode atom) const { in hasSharedTerms()85 void SharedTermsDatabase::backtrack() { in backtrack()175 bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { in areEqual()237 void SharedTermsDatabase::checkForConflict() { in checkForConflict()248 bool SharedTermsDatabase::isKnown(TNode literal) const { in isKnown()[all …]
32 class SharedTermsDatabase : public context::ContextNotifyObj {78 SharedTermsDatabase& d_sharedTerms;80 EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} in EENotifyClass()160 SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);161 ~SharedTermsDatabase();
103 SharedTermsDatabase& d_sharedTerms;125 SharedTermsVisitor(SharedTermsDatabase& sharedTerms) in SharedTermsVisitor()
113 friend class SharedTermsDatabase; variable146 SharedTermsDatabase d_sharedTerms;882 SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } in getSharedTermsDatabase()
1373 SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); in assertFact()1374 SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); in assertFact()