Searched refs:QuantConflictFind (Results 1 – 6 of 6) sorted by relevance
32 class QuantConflictFind; variable50 bool doMatching( QuantConflictFind * p, QuantInfo * qi );99 bool reset_round(QuantConflictFind* p);101 bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );159 bool getNextMatch( QuantConflictFind * p ) { in getNextMatch()164 bool reset_round( QuantConflictFind * p );167 void initialize( QuantConflictFind * p, Node q, Node qn );180 void unsetMatch( QuantConflictFind * p, int v );181 bool isMatchSpurious( QuantConflictFind * p );192 class QuantConflictFind : public QuantifiersModule[all …]
1184 bool MatchGen::reset_round(QuantConflictFind* p) in reset_round()1838 QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c) in QuantConflictFind() function in CVC4::theory::quantifiers::QuantConflictFind1933 return QuantConflictFind::EFFORT_CONFLICT; in QcfEffortStart()1938 inline QuantConflictFind::Effort QcfEffortEnd() { in QcfEffortEnd()2101 void QuantConflictFind::computeRelevantEqr() { in computeRelevantEqr()2172 QuantConflictFind::Statistics::Statistics(): in Statistics()2180 QuantConflictFind::Statistics::~Statistics(){ in ~Statistics()2185 TNode QuantConflictFind::getZero( Kind k ) { in getZero()2201 case QuantConflictFind::EFFORT_INVALID: in operator <<()2204 case QuantConflictFind::EFFORT_CONFLICT: in operator <<()[all …]
119 QuantConflictFind * qcf = d_quantEngine->getConflictFind(); in checkRewriteRule()123 qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); in checkRewriteRule()229 QuantConflictFind * qcf = d_quantEngine->getConflictFind(); in registerQuantifier()
46 class QuantConflictFind; variable
67 class QuantConflictFind; variable149 quantifiers::QuantConflictFind* getConflictFind() const;372 std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
174 d_qcf.reset(new quantifiers::QuantConflictFind(this, c)); in QuantifiersEngine()362 quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const in getConflictFind()