-bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
- if( doCache ){
- if( doRewrite ){
- lem = Rewriter::rewrite(lem);
- }
- Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
- BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
- if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
- d_lemmas_produced_c[ lem ] = true;
- d_lemmas_waiting.push_back( lem );
- Trace("inst-add-debug") << "Added lemma" << std::endl;
- return true;
- }else{
- Trace("inst-add-debug") << "Duplicate." << std::endl;
- return false;
- }
- }else{
- //do not need to rewrite, will be rewritten after sending
- d_lemmas_waiting.push_back( lem );
- return true;
- }
-}
-
-bool QuantifiersEngine::addTrustedLemma(TrustNode tlem,
- bool doCache,
- bool doRewrite)
-{
- Node lem = tlem.getProven();
- if (!addLemma(lem, doCache, doRewrite))
- {
- return false;
- }
- d_lemmasWaitingPg[lem] = tlem.getGenerator();
- return true;
-}
-
-bool QuantifiersEngine::removeLemma( Node lem ) {
- std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
- if( it!=d_lemmas_waiting.end() ){
- d_lemmas_waiting.erase( it, it + 1 );
- d_lemmas_produced_c[ lem ] = false;
- return true;
- }else{
- return false;
- }
-}
-
-void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
- d_phase_req_waiting[lit] = req;
-}
-