diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-12-03 12:09:14 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-12-03 12:09:14 -0500 |
commit | 2121eaac7e63875f1e6ba53076535d25fd561c04 (patch) | |
tree | bbfba9957b3d64d43604e645c7b42b77a8baa530 /src/theory | |
parent | 160134dc043c28308865d2b91648ba412d0749d4 (diff) | |
parent | fa6ac807d931518790df89206c4f3aeceff8e395 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/theory')
23 files changed, 912 insertions, 191 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index cfaa6d1ad..9e3fed20a 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -197,16 +197,17 @@ void CandidateGeneratorQEAll::reset( Node eqc ) { Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ - Node n = (*d_eq); + TNode n = (*d_eq); ++d_eq; if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ - if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n ); + if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 ){ - n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index ); + nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); } d_firstTime = false; //an equivalence class with the same type as the pattern, return it - return n; + return nh; } } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index ffe64beba..bf9409f06 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -248,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ Node t = getModelTerm( conj->d_candidates[i] ); model_terms.push_back( t ); - Trace("cegqi-engine") << t << " "; + Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " "; } Trace("cegqi-engine") << std::endl; d_quantEngine->addInstantiation( q, model_terms, false ); @@ -279,7 +279,7 @@ bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node for( unsigned i=0; i<n.size(); i++ ){ Node nv = getModelValue( n[i] ); v.push_back( nv ); - Trace("cegqi-engine") << nv << " "; + Trace("cegqi-engine") << n[i] << " -> " << nv << " "; if( nv.isNull() ){ success = false; } diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 06552196d..2f8822b53 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -352,7 +352,8 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) { }
bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
- return e==Theory::EFFORT_FULL;
+ // synchonized with instantiation engine
+ return d_quantEngine->getInstWhenNeedsCheck( e );
}
bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8918a6dac..b9e8aef09 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -530,12 +530,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ //skip inst constant nodes while( nv<maxs[index] && nv<=max_i && r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ - childIndex[index]++; - nv = childIndex[index]+1; + nv++; } } if( nv<maxs[index] && nv<=max_i ){ - childIndex[index]++; + childIndex[index] = nv; index++; }else{ childIndex.pop_back(); @@ -545,8 +544,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } success = index>=0; if( success ){ - Trace("inst-alg-rd") << "Try instantiation..." << std::endl; - index--; + Trace("inst-alg-rd") << "Try instantiation { "; + for( unsigned j=0; j<childIndex.size(); j++ ){ + Trace("inst-alg-rd") << childIndex[j] << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; //try instantiation std::vector< Node > terms; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ @@ -560,6 +562,8 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ Trace("inst-alg-rd") << "Success!" << std::endl; ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); return STATUS_UNKNOWN; + }else{ + index--; } } }while( success ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index ade6d4313..b53919aaf 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){ } @@ -178,37 +178,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } bool InstantiationEngine::needsCheck( Theory::Effort e ){ - if( e==Theory::EFFORT_FULL ){ - d_ierCounter++; - } - //determine if we should perform check, based on instWhenMode - bool performCheck = false; - if( options::instWhenMode()==INST_WHEN_FULL ){ - performCheck = ( e >= Theory::EFFORT_FULL ); - }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){ - performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck(); - }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); - }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ - performCheck = ( e >= Theory::EFFORT_LAST_CALL ); - }else{ - performCheck = true; - } - static int ierCounter2 = 0; - if( e==Theory::EFFORT_LAST_CALL ){ - ierCounter2++; - //with bounded integers, skip every other last call, - // since matching loops may occur with infinite quantification - if( ierCounter2%2==0 && options::fmfBoundInt() ){ - performCheck = false; - } - } - return performCheck; + return d_quantEngine->getInstWhenNeedsCheck( e ); } void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ - Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl; double clSet = 0; if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 2fa37ac35..2d427ae0a 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -84,8 +84,6 @@ private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; - /** inst round counter */ - int d_ierCounter; /** whether each quantifier is active */ std::map< Node, bool > d_quant_active; /** whether we have added cbqi lemma */ diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index a8774440e..793e4a611 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -44,6 +44,8 @@ sort INST_PATTERN_LIST_TYPE \ # a list of instantiation patterns operator INST_PATTERN_LIST 1: "a list of instantiation patterns" +operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure." + typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule @@ -51,6 +53,7 @@ typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule +typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule # for rewrite rules # types... diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index dad173ff5..cac78af46 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies -option nnfQuant --nnf-quant bool :default false +option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas option clauseSplit --clause-split bool :default false @@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation -option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false only add one instantiation per quantifier per round for mbqi option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false only add instantiations for one quantifier per round for mbqi @@ -196,5 +196,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions +option termDbInstClosure --term-db-inst-closure bool :default false + only consider inst closure terms for E-matching endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 08fcf319d..e9f85d454 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -29,17 +29,17 @@ namespace quantifiers { static const std::string instWhenHelp = "\ Modes currently supported by the --inst-when option:\n\ \n\ -full (default)\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +full\n\ + Run instantiation round at full effort, before theory combination.\n\ \n\ full-delay \n\ + Run instantiation round at full effort, before theory combination, after\n\ all other theories have finished.\n\ \n\ -full-last-call\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ last-call\n\ + Run instantiation at last call effort, after theory combination and\n\ and theories report sat.\n\ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0ed175393..1e6ec3a02 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -309,11 +309,19 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); + if( body[0].getKind()==OR || body[0].getKind()==AND ){ + k = body[0].getKind()==AND ? OR : AND; for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - children.push_back( computeNNF( body[0][i].notNode() ) ); + Node nc = computeNNF( body[0][i].notNode() ); + if( nc.getKind()==k ){ + for( unsigned j=0; j<nc.getNumChildren(); j++ ){ + children.push_back( nc[j] ); + } + }else{ + children.push_back( nc ); + } } - k = body[0].getKind()==AND ? OR : AND; }else if( body[0].getKind()==IFF ){ for( int i=0; i<2; i++ ){ Node nn = i==0 ? body[0][i] : body[0][i].notNode(); @@ -335,10 +343,18 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; bool childrenChanged = false; + bool isAssoc = body.getKind()==AND || body.getKind()==OR; for( int i=0; i<(int)body.getNumChildren(); i++ ){ Node nc = computeNNF( body[i] ); - children.push_back( nc ); - childrenChanged = childrenChanged || nc!=body[i]; + if( isAssoc && nc.getKind()==body.getKind() ){ + for( unsigned j=0; j<nc.getNumChildren(); j++ ){ + children.push_back( nc[j] ); + } + childrenChanged = true; + }else{ + children.push_back( nc ); + childrenChanged = childrenChanged || nc!=body[i]; + } } if( childrenChanged ){ return NodeManager::currentNM()->mkNode( body.getKind(), children ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a95de086a..34c40c8c4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -111,13 +111,17 @@ Node TermDb::getOperator( Node n ) { } } -void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ +void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){ //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ return; } + bool rec = false; if( d_processed.find( n )==d_processed.end() ){ d_processed.insert(n); + if( withinInstClosure ){ + d_iclosure_processed.insert( n ); + } d_type_map[ n.getType() ].push_back( n ); //if this is an atomic trigger, consider adding it //Call the children? @@ -137,9 +141,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ d_op_map[op].push_back( n ); added.insert( n ); - for( size_t i=0; i<n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant ); - if( options::eagerInstQuant() ){ + if( options::eagerInstQuant() ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ int addedLemmas = 0; for( size_t i=0; i<d_op_triggers[op].size(); i++ ){ @@ -149,10 +152,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } } } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant ); - } + } + rec = true; + }else if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ + d_iclosure_processed.insert( n ); + rec = true; + } + if( rec ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + addTerm( n[i], added, withinQuant, withinInstClosure ); } } } @@ -317,30 +325,65 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, } bool TermDb::hasTermCurrent( Node n ) { - //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); - if( options::termDbMode()==TERM_DB_ALL ){ - return true; - }else if( options::termDbMode()==TERM_DB_RELEVANT ){ - return d_has_map.find( n )!=d_has_map.end(); - }else{ - Assert( false ); + if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ return false; + }else{ + //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE + if( options::termDbMode()==TERM_DB_ALL ){ + return true; + }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + return d_has_map.find( n )!=d_has_map.end(); + }else{ + Assert( false ); + return false; + } } } -void TermDb::setHasTerm( Node n ) { - if( inst::Trigger::isAtomicTrigger( n ) ){ - if( d_has_map.find( n )==d_has_map.end() ){ - d_has_map[n] = true; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - setHasTerm( n[i] ); +Node TermDb::getHasTermEqc( Node r ) { + if( hasTermCurrent( r ) ){ + return r; + }else{ + if( options::termDbInstClosure() ){ + std::map< Node, Node >::iterator it = d_has_eqc.find( r ); + if( it==d_has_eqc.end() ){ + Node h; + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( h.isNull() && !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + ++eqc_i; + if( hasTermCurrent( n ) ){ + h = n; + } + } + d_has_eqc[r] = h; + return h; + }else{ + return it->second; } + }else{ + //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc + return Node::null(); + } + } +} + +void TermDb::setHasTerm( Node n ) { + //if( inst::Trigger::isAtomicTrigger( n ) ){ + if( d_has_map.find( n )==d_has_map.end() ){ + d_has_map[n] = true; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + setHasTerm( n[i] ); } + } + /* }else{ for( unsigned i=0; i<n.getNumChildren(); i++ ){ setHasTerm( n[i] ); } } + */ } void TermDb::reset( Theory::Effort effort ){ @@ -356,6 +399,7 @@ void TermDb::reset( Theory::Effort effort ){ //compute has map if( options::termDbMode()==TERM_DB_RELEVANT ){ d_has_map.clear(); + d_has_eqc.clear(); eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2b151bb04..cb9f5eeef 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -123,6 +123,8 @@ private: QuantifiersEngine* d_quantEngine; /** terms processed */ std::hash_set< Node, NodeHashFunction > d_processed; + /** terms processed */ + std::hash_set< Node, NodeHashFunction > d_iclosure_processed; private: /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; @@ -144,6 +146,8 @@ public: std::map< Node, std::vector< Node > > d_op_map; /** has map */ std::map< Node, bool > d_has_map; + /** map from reps to a term in eqc in d_has_map */ + std::map< Node, Node > d_has_eqc; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; @@ -152,7 +156,7 @@ public: /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; /** add a term to the database */ - void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); + void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false ); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); /** get operator*/ @@ -176,6 +180,8 @@ public: bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ bool hasTermCurrent( Node n ); + /** get has term eqc */ + Node getHasTermEqc( Node r ); //for model basis private: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5c68e52a7..de0f98af6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), - d_numRestarts(0), d_masterEqualityEngine(0) { d_numInstantiations = 0; @@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) { } } +void TheoryQuantifiers::computeCareGraph() { + //do nothing +} + void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { if(fullModel) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { @@ -126,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) { case kind::FORALL: assertUniversal( assertion ); break; + case kind::INST_CLOSURE: + getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); + break; + case kind::EQUAL: + //do nothing + break; case kind::NOT: { switch( assertion[0].getKind()) { case kind::FORALL: assertExistential( assertion ); break; + case kind::EQUAL: + //do nothing + break; + case kind::INST_CLOSURE: //cannot negate inst closure default: Unhandled(assertion[0].getKind()); break; @@ -182,23 +195,7 @@ bool TheoryQuantifiers::flipDecision(){ //}else{ // return false; //} - - if( !d_out->flipDecision() ){ - return restart(); - } - return true; -} - -bool TheoryQuantifiers::restart(){ - static const int restartLimit = 0; - if( d_numRestarts==restartLimit ){ - Debug("quantifiers-flip") << "No more restarts." << std::endl; - return false; - }else{ - d_numRestarts++; - Debug("quantifiers-flip") << "Do restart." << std::endl; - return true; - } + return false; } void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index aace13b24..6d3fa4d46 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -44,17 +44,15 @@ private: /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; - /** number of restarts */ - int d_numRestarts; eq::EqualityEngine* d_masterEqualityEngine; - +private: + void computeCareGraph(); public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); - void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); @@ -73,7 +71,6 @@ public: private: void assertUniversal( Node n ); void assertExistential( Node n ); - bool restart(); };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 5d86c29c0..341e656c7 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -84,6 +84,12 @@ struct QuantifierInstPatternTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::INST_PATTERN ); + if( check ){ + TypeNode tn = n[0].getType(check); + if( tn.isFunction() ){ + throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms."); + } + } return nodeManager->instPatternType(); } };/* struct QuantifierInstPatternTypeRule */ @@ -120,6 +126,20 @@ struct QuantifierInstPatternListTypeRule { };/* struct QuantifierInstPatternListTypeRule */ +struct QuantifierInstClosureTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::INST_CLOSURE ); + if( check ){ + TypeNode tn = n[0].getType(check); + if( tn.isBoolean() ){ + throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean"); + } + } + return nodeManager->booleanType(); + } +};/* struct QuantifierInstClosureTypeRule */ + class RewriteRuleTypeRule { public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 04b6c5d16..d6c6f4667 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -171,8 +171,9 @@ d_lemmas_produced_c(u){ d_builder = NULL; } - //options d_total_inst_count_debug = 0; + d_ierCounter = 0; + d_ierCounter_lc = 0; } QuantifiersEngine::~QuantifiersEngine(){ @@ -251,6 +252,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } + if( e==Theory::EFFORT_FULL ){ + d_ierCounter++; + }else if( e==Theory::EFFORT_LAST_CALL ){ + d_ierCounter_lc++; + } bool needsCheck = false; bool needsModel = false; bool needsFullModel = false; @@ -472,9 +478,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){ return Node::null(); } -void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ +void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ std::set< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant ); + getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); //maybe have triggered instantiations if we are doing eager instantiation if( options::eagerInstQuant() ){ flushLemmas(); @@ -825,6 +831,30 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { + //determine if we should perform check, based on instWhenMode + bool performCheck = false; + if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){ + performCheck = ( e >= Theory::EFFORT_FULL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ + performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ + performCheck = ( e >= Theory::EFFORT_LAST_CALL ); + }else{ + performCheck = true; + } + if( e==Theory::EFFORT_LAST_CALL ){ + //with bounded integers, skip every other last call, + // since matching loops may occur with infinite quantification + if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){ + performCheck = false; + } + } + return performCheck; +} + void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ //take default output channel if none is provided diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 199fe79b9..ac782a536 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -169,6 +169,9 @@ private: std::map< Node, int > d_total_inst_debug; std::map< Node, int > d_temp_inst_debug; int d_total_inst_count_debug; + /** inst round counters */ + int d_ierCounter; + int d_ierCounter_lc; private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: @@ -273,6 +276,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** get number of waiting lemmas */ int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } + /** get needs check */ + bool getInstWhenNeedsCheck( Theory::Effort e ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); /** is term eligble for instantiation? */ @@ -290,7 +295,7 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false ); + void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; /** debug print equality engine */ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 69b089c84..016983059 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1157,9 +1157,10 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) } case kind::REGEXP_INTER: { //TODO: Overapproximation for now - for(unsigned i=0; i<r.getNumChildren(); i++) { - getCharSet(r[i], cset, vset); - } + //for(unsigned i=0; i<r.getNumChildren(); i++) { + //getCharSet(r[i], cset, vset); + //} + getCharSet(r[0], cset, vset); break; } case kind::REGEXP_STAR: { @@ -1382,7 +1383,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { } } Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ) { - Trace("regexp-intersect") << "Starting INTERSECT:\n "<< mkString(r1) << ",\n " << mkString(r2) << std::endl; + //(checkConstRegExp(r1) && checkConstRegExp(r2)) + Trace("regexp-intersect") << "Starting INTERSECT(" << cnt << "):\n "<< mkString(r1) << ",\n " << mkString(r2) << std::endl; //if(Trace.isOn("regexp-debug")) { // Trace("regexp-debug") << "... with cache:\n"; // for(std::map< PairNodes, Node >::const_iterator itr=cache.begin(); @@ -1397,9 +1399,9 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node std::pair < Node, Node > p(r1, r2); std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p); Node rNode; - if(itr != d_inter_cache.end()) { - rNode = itr->second; - } else { +// if(itr != d_inter_cache.end()) { +// rNode = itr->second; +// } else { if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) { rNode = d_emptyRegexp; } else if(r1 == d_emptySingleton || r2 == d_emptySingleton) { @@ -1414,79 +1416,138 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node rNode = d_emptyRegexp; } } else if(r1 == r2) { - rNode = convert1(cnt, r1); + rNode = r1; //convert1(cnt, r1); } else { PairNodes p(r1, r2); std::map< PairNodes, Node >::const_iterator itrcache = cache.find(p); if(itrcache != cache.end()) { rNode = itrcache->second; } else { - if(checkConstRegExp(r1) && checkConstRegExp(r2)) { - std::vector< unsigned > cset; - std::set< unsigned > cset1, cset2; - std::set< Node > vset1, vset2; - firstChars(r1, cset1, vset1); - firstChars(r2, cset2, vset2); - std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(), - std::inserter(cset, cset.begin())); - std::vector< Node > vec_nodes; - Node delta_exp; - int flag = delta(r1, delta_exp); - int flag2 = delta(r2, delta_exp); - if(flag != 2 && flag2 != 2) { - if(flag == 1 && flag2 == 1) { - vec_nodes.push_back(d_emptySingleton); - } else { - //TODO - spflag = true; - } - } - if(Trace.isOn("regexp-debug")) { - Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = "; - for(std::vector<unsigned>::const_iterator itr = cset.begin(); - itr != cset.end(); itr++) { - CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); - Trace("regexp-debug") << c << ", "; - } - Trace("regexp-debug") << std::endl; + std::vector< unsigned > cset; + std::set< unsigned > cset1, cset2; + std::set< Node > vset1, vset2; + firstChars(r1, cset1, vset1); + firstChars(r2, cset2, vset2); + std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(), + std::inserter(cset, cset.begin())); + std::vector< Node > vec_nodes; + Node delta_exp; + int flag = delta(r1, delta_exp); + int flag2 = delta(r2, delta_exp); + if(flag != 2 && flag2 != 2) { + if(flag == 1 && flag2 == 1) { + vec_nodes.push_back(d_emptySingleton); + } else { + //TODO + spflag = true; } + } + if(Trace.isOn("regexp-debug")) { + Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = "; for(std::vector<unsigned>::const_iterator itr = cset.begin(); itr != cset.end(); itr++) { CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); - Node r1l = derivativeSingle(r1, c); - Node r2l = derivativeSingle(r2, c); - std::map< PairNodes, Node > cache2(cache); - PairNodes p(r1, r2); - cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); - Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); - rt = convert1(cnt, rt); - if(spflag) { - //TODO: - return Node::null(); - } - rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, - NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) ); - vec_nodes.push_back(rt); + Trace("regexp-debug") << c << ", "; } - rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : - NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); - rNode = Rewriter::rewrite( rNode ); - } else { - //TODO: non-empty var set - spflag = true; + Trace("regexp-debug") << std::endl; + } + for(std::vector<unsigned>::const_iterator itr = cset.begin(); + itr != cset.end(); itr++) { + CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); + Node r1l = derivativeSingle(r1, c); + Node r2l = derivativeSingle(r2, c); + std::map< PairNodes, Node > cache2(cache); + PairNodes p(r1, r2); + cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); + Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); + //if(spflag) { + //return Node::null(); + //} + rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, + NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) ); + vec_nodes.push_back(rt); } + rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : + NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); + rNode = Rewriter::rewrite( rNode ); + rNode = convert1(cnt, rNode); + rNode = Rewriter::rewrite( rNode ); } } - d_inter_cache[p] = rNode; - } - Trace("regexp-intersect") << "End of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; +// d_inter_cache[p] = rNode; +// } + Trace("regexp-intersect") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; return rNode; } + +Node RegExpOpr::removeIntersection(Node r) { + Assert( checkConstRegExp(r) ); + std::map < Node, Node >::const_iterator itr = d_rm_inter_cache.find(r); + Node retNode; + if(itr != d_rm_inter_cache.end()) { + retNode = itr->second; + } else { + switch(r.getKind()) { + case kind::REGEXP_EMPTY: { + retNode = r; + break; + } + case kind::REGEXP_SIGMA: { + retNode = r; + break; + } + case kind::STRING_TO_REGEXP: { + retNode = r; + break; + } + case kind::REGEXP_CONCAT: { + std::vector< Node > vec_nodes; + for(unsigned i=0; i<r.getNumChildren(); i++) { + Node tmpNode = removeIntersection( r[i] ); + vec_nodes.push_back( tmpNode ); + } + retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes) ); + break; + } + case kind::REGEXP_UNION: { + std::vector< Node > vec_nodes; + for(unsigned i=0; i<r.getNumChildren(); i++) { + Node tmpNode = removeIntersection( r[i] ); + vec_nodes.push_back( tmpNode ); + } + retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) ); + break; + } + case kind::REGEXP_INTER: { + retNode = removeIntersection( r[0] ); + for(unsigned i=1; i<r.getNumChildren(); i++) { + bool spflag = false; + Node tmpNode = removeIntersection( r[i] ); + retNode = intersect( retNode, tmpNode, spflag ); + } + break; + } + case kind::REGEXP_STAR: { + retNode = removeIntersection( r[0] ); + retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode) ); + break; + } + default: { + Unreachable(); + } + } + d_rm_inter_cache[r] = retNode; + } + Trace("regexp-intersect") << "Remove INTERSECTION( " << mkString(r) << " ) = " << mkString(retNode) << std::endl; + return retNode; +} + Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { - //std::map< unsigned, std::set< PairNodes > > cache; - std::map< PairNodes, Node > cache; if(checkConstRegExp(r1) && checkConstRegExp(r2)) { - return intersectInternal2(r1, r2, cache, spflag, 1); + Node rr1 = removeIntersection(r1); + Node rr2 = removeIntersection(r2); + std::map< PairNodes, Node > cache; + return intersectInternal2(rr1, rr2, cache, spflag, 1); } else { spflag = true; return Node::null(); @@ -1653,8 +1714,115 @@ void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) { } } +void RegExpOpr::flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec) { + Assert(false); + Assert(checkConstRegExp(r)); + switch( r.getKind() ) { + case kind::REGEXP_EMPTY: { + //TODO + break; + } + case kind::REGEXP_SIGMA: { + CVC4::String s("a"); + std::pair< CVC4::String, unsigned > tmp(s, 0); + //TODO + break; + } + case kind::STRING_TO_REGEXP: { + Assert(r[0].isConst()); + CVC4::String s = r[0].getConst< CVC4::String >(); + std::pair< CVC4::String, unsigned > tmp(s, 0); + //TODO + break; + } + case kind::REGEXP_CONCAT: { + for(unsigned i=0; i<r.getNumChildren(); i++) { + //TODO + } + break; + } + case kind::REGEXP_UNION: { + for(unsigned i=0; i<r.getNumChildren(); ++i) { + //TODO + } + break; + } + case kind::REGEXP_INTER: { + //TODO + break; + } + case kind::REGEXP_STAR: { + //TODO + break; + } + default: { + Unreachable(); + } + } +} + +void RegExpOpr::disjunctRegExp(Node r, std::vector<Node> &vec_or) { + switch(r.getKind()) { + case kind::REGEXP_EMPTY: { + vec_or.push_back(r); + break; + } + case kind::REGEXP_SIGMA: { + vec_or.push_back(r); + break; + } + case kind::STRING_TO_REGEXP: { + vec_or.push_back(r); + break; + } + case kind::REGEXP_CONCAT: { + disjunctRegExp(r[0], vec_or); + for(unsigned i=1; i<r.getNumChildren(); i++) { + std::vector<Node> vec_con; + disjunctRegExp(r[i], vec_con); + std::vector<Node> vec_or2; + for(unsigned k1=0; k1<vec_or.size(); k1++) { + for(unsigned k2=0; k2<vec_con.size(); k2++) { + Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_or[k1], vec_con[k2]) ); + if(std::find(vec_or2.begin(), vec_or2.end(), tmp) == vec_or2.end()) { + vec_or2.push_back( tmp ); + } + } + } + vec_or = vec_or2; + } + break; + } + case kind::REGEXP_UNION: { + for(unsigned i=0; i<r.getNumChildren(); ++i) { + std::vector<Node> vec_or2; + disjunctRegExp(r[i], vec_or2); + vec_or.insert(vec_or.end(), vec_or2.begin(), vec_or2.end()); + } + break; + } + case kind::REGEXP_INTER: { + Assert(checkConstRegExp(r)); + Node rtmp = r[0]; + bool spflag = false; + for(unsigned i=1; i<r.getNumChildren(); ++i) { + rtmp = intersect(rtmp, r[i], spflag); + } + disjunctRegExp(rtmp, vec_or); + break; + } + case kind::REGEXP_STAR: { + vec_or.push_back(r); + break; + } + default: { + Unreachable(); + } + } +} + //printing -std::string RegExpOpr::niceChar( Node r ) { +std::string RegExpOpr::niceChar(Node r) { if(r.isConst()) { std::string s = r.getConst<CVC4::String>().toString() ; return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s ); @@ -1666,12 +1834,12 @@ std::string RegExpOpr::niceChar( Node r ) { std::string RegExpOpr::mkString( Node r ) { std::string retStr; if(r.isNull()) { - retStr = "Empty"; + retStr = "Phi"; } else { int k = r.getKind(); switch( k ) { case kind::REGEXP_EMPTY: { - retStr += "Empty"; + retStr += "Phi"; break; } case kind::REGEXP_SIGMA: { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index ce3093528..3b898e5f5 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -64,6 +64,7 @@ private: std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache; std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache; std::map< PairNodes, Node > d_inter_cache; + std::map< Node, Node > d_rm_inter_cache; std::map< Node, std::vector< PairNodes > > d_split_cache; //bool checkStarPlus( Node t ); void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ); @@ -79,6 +80,7 @@ private: Node convert1(unsigned cnt, Node n); void convert2(unsigned cnt, Node n, Node &r1, Node &r2); Node intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ); + Node removeIntersection(Node r); void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); //TODO: for intersection @@ -96,6 +98,8 @@ public: Node intersect(Node r1, Node r2, bool &spflag); Node complement(Node r, int &ret); void splitRegExp(Node r, std::vector< PairNodes > &pset); + void flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec); + void disjunctRegExp(Node r, std::vector<Node> &vec_or); std::string mkString( Node r ); }; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ead8a44f8..0df551847 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,9 +55,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_regexp_memberships(c), d_regexp_ucached(u), d_regexp_ccached(c), - d_str_re_map(c), + d_pos_memberships(c), + d_neg_memberships(c), d_inter_cache(c), d_inter_index(c), + d_processed_memberships(c), d_regexp_ant(c), d_input_vars(u), d_input_var_lsum(u), @@ -484,8 +486,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { if( n.getKind() == kind::VARIABLE && options::stringFMF() ) { d_input_vars.insert(n); } - } - if (n.getType().isBoolean()) { + } else if (n.getType().isBoolean()) { // Get triggered for both equal and dis-equal d_equalityEngine.addTriggerPredicate(n); } else { @@ -2514,6 +2515,318 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) { } } +Node TheoryStrings::normalizeRegexp(Node r) { + Node nf_r = r; + if(d_nf_regexps.find(r) != d_nf_regexps.end()) { + nf_r = d_nf_regexps[r]; + } else { + std::vector< Node > nf_exp; + if(!d_regexp_opr.checkConstRegExp(r)) { + switch( r.getKind() ) { + case kind::REGEXP_EMPTY: + case kind::REGEXP_SIGMA: { + break; + } + case kind::STRING_TO_REGEXP: { + if(r[0].isConst()) { + break; + } else { + if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) { + nf_r = mkConcat( d_normal_forms[r[0]] ); + Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl; + nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end()); + nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) ); + } + } + } + case kind::REGEXP_CONCAT: + case kind::REGEXP_UNION: + case kind::REGEXP_INTER: { + bool flag = false; + std::vector< Node > vec_nodes; + for(unsigned i=0; i<r.getNumChildren(); ++i) { + Node rtmp = normalizeRegexp(r[i]); + vec_nodes.push_back(rtmp); + if(rtmp != r[i]) { + flag = true; + } + } + if(flag) { + Node rtmp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes); + nf_r = Rewriter::rewrite( rtmp ); + } + } + case kind::REGEXP_STAR: { + Node rtmp = normalizeRegexp(r[0]); + if(rtmp != r[0]) { + rtmp = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, rtmp); + nf_r = Rewriter::rewrite( rtmp ); + } + } + default: { + Unreachable(); + } + } + } + d_nf_regexps[r] = nf_r; + d_nf_regexps_exp[r] = nf_exp; + } + return nf_r; +} + +bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps) { + std::map< Node, std::vector< Node > > unprocessed_x_exps; + std::map< Node, std::vector< Node > > unprocessed_memberships; + std::map< Node, std::vector< Node > > unprocessed_memberships_bases; + bool addLemma = false; + + Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl; + + for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); + itr_xr != d_pos_memberships.end(); ++itr_xr ) { + Node x = (*itr_xr).first; + NodeList* lst = (*itr_xr).second; + Node nf_x = x; + std::vector< Node > nf_x_exp; + if(d_normal_forms.find( x ) != d_normal_forms.end()) { + //nf_x = mkConcat( d_normal_forms[x] ); + nf_x_exp.insert(nf_x_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end()); + //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl; + } else { + Assert(false); + } + Trace("regexp-nf") << "Checking Memberships for N(" << x << ") = " << nf_x << " :" << std::endl; + + std::vector< Node > vec_x; + std::vector< Node > vec_r; + for(NodeList::const_iterator itr_lst = lst->begin(); + itr_lst != lst->end(); ++itr_lst) { + Node r = *itr_lst; + Node nf_r = normalizeRegexp((*lst)[0]); + Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r); + if(d_processed_memberships.find(memb) == d_processed_memberships.end()) { + if(d_regexp_opr.checkConstRegExp(nf_r)) { + vec_x.push_back(x); + vec_r.push_back(r); + } else { + Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r << ") = " << nf_r << std::endl; + //TODO: handle symbolic ones + addLemma = true; + } + d_processed_memberships.insert(memb); + } + } + if(!vec_x.empty()) { + if(unprocessed_x_exps.find(nf_x) == unprocessed_x_exps.end()) { + unprocessed_x_exps[nf_x] = nf_x_exp; + unprocessed_memberships[nf_x] = vec_r; + unprocessed_memberships_bases[nf_x] = vec_x; + } else { + unprocessed_x_exps[nf_x].insert(unprocessed_x_exps[nf_x].end(), nf_x_exp.begin(), nf_x_exp.end()); + unprocessed_memberships[nf_x].insert(unprocessed_memberships[nf_x].end(), vec_r.begin(), vec_r.end()); + unprocessed_memberships_bases[nf_x].insert(unprocessed_memberships_bases[nf_x].end(), vec_x.begin(), vec_x.end()); + } + } + } + //Intersection + for(std::map< Node, std::vector< Node > >::const_iterator itr = unprocessed_memberships.begin(); + itr != unprocessed_memberships.end(); ++itr) { + Node nf_x = itr->first; + std::vector< Node > exp( unprocessed_x_exps[nf_x] ); + Node r = itr->second[0]; + //get nf_r + Node inter_r = d_nf_regexps[r]; + exp.insert(exp.end(), d_nf_regexps_exp[r].begin(), d_nf_regexps_exp[r].end()); + Node x = unprocessed_memberships_bases[itr->first][0]; + Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r); + exp.push_back(memb); + for(std::size_t i=1; i < itr->second.size(); i++) { + //exps + Node r2 = itr->second[i]; + Node inter_r2 = d_nf_regexps[r2]; + exp.insert(exp.end(), d_nf_regexps_exp[r2].begin(), d_nf_regexps_exp[r2].end()); + Node x2 = unprocessed_memberships_bases[itr->first][i]; + memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x2, r2); + exp.push_back(memb); + //intersection + bool spflag = false; + inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag); + if(inter_r == d_emptyRegexp) { + //conflict + Node antec = exp.size() == 1? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp); + Node conc; + sendLemma(antec, conc, "INTERSEC CONFLICT"); + addLemma = true; + break; + } + } + //infer + if(!d_conflict) { + memb = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, inter_r) ); + memb_with_exps[memb] = exp; + } else { + break; + } + } + + return addLemma; +} + +bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) { + Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl; + Assert( d_regexp_opr.checkConstRegExp(r) ); + + if( !s.isEmptyString() ) { + Node dc = r; + + for(unsigned i=0; i<s.size(); ++i) { + CVC4::String c = s.substr(i, 1); + Node dc2; + int rt = d_regexp_opr.derivativeS(dc, c, dc2); + dc = dc2; + if(rt == 0) { + Unreachable(); + } else if(rt == 2) { + return false; + } + } + r = dc; + } + + return true; +} + +Node TheoryStrings::applyRSplit(Node s1, Node s2, Node r) { + Assert(d_regexp_opr.checkConstRegExp(r)); + + std::vector< std::pair< Node, Node > > vec_can; + d_regexp_opr.splitRegExp(r, vec_can); + //TODO: lazy cache or eager? + std::vector< Node > vec_or; + + for(unsigned int i=0; i<vec_can.size(); i++) { + Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first); + Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second); + Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) ); + vec_or.push_back( c ); + } + Node conc = vec_or.size()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) ); + return conc; +} + +bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) { + if(XinR_with_exps.size() > 0) { + //TODO: get vector, var, store. + return true; + } else { + return false; + } +} + +bool TheoryStrings::checkMembershipsWithoutLength( + std::map< Node, std::vector< Node > > &memb_with_exps, + std::map< Node, std::vector< Node > > &XinR_with_exps) { + for(std::map< Node, std::vector< Node > >::const_iterator itr = memb_with_exps.begin(); + itr != memb_with_exps.end(); ++itr) { + Node memb = itr->first; + Node s = memb[0]; + Node r = memb[1]; + if(s.isConst()) { + memb = Rewriter::rewrite( memb ); + if(memb == d_false) { + Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); + Node conc; + sendLemma(antec, conc, "MEMBERSHIP CONFLICT"); + //addLemma = true; + return true; + } else { + Assert(memb == d_true); + } + } else if(s.getKind() == kind::VARIABLE) { + //add to XinR + XinR_with_exps[itr->first] = itr->second; + } else { + Assert(s.getKind() == kind::STRING_CONCAT); + Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); + Node conc; + for( unsigned i=0; i<s.getNumChildren(); i++ ) { + if(s[i].isConst()) { + CVC4::String str( s[0].getConst< String >() ); + //R-Consume, see Tianyi's thesis + if(!applyRConsume(str, r)) { + sendLemma(antec, conc, "R-Consume CONFLICT"); + //addLemma = true; + return true; + } + } else { + //R-Split, see Tianyi's thesis + if(i == s.getNumChildren() - 1) { + //add to XinR + Node memb2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s[i], r); + XinR_with_exps[itr->first] = itr->second; + } else { + Node s1 = s[i]; + std::vector< Node > vec_s2; + for( unsigned j=i+1; j<s.getNumChildren(); j++ ) { + vec_s2.push_back(s[j]); + } + Node s2 = mkConcat(vec_s2); + conc = applyRSplit(s1, s2, r); + if(conc == d_true) { + break; + } else if(conc.isNull() || conc == d_false) { + conc = Node::null(); + sendLemma(antec, conc, "R-Split Conflict"); + //addLemma = true; + return true; + } else { + sendLemma(antec, conc, "R-Split"); + //addLemma = true; + return true; + } + } + } + } + } + } + return false; +} + +bool TheoryStrings::checkMemberships2() { + bool addedLemma = false; + d_nf_regexps.clear(); + d_nf_regexps_exp.clear(); + std::map< Node, std::vector< Node > > memb_with_exps; + std::map< Node, std::vector< Node > > XinR_with_exps; + + addedLemma = normalizePosMemberships( memb_with_exps ); + if(!d_conflict) { + // main procedure + addedLemma |= checkMembershipsWithoutLength( memb_with_exps, XinR_with_exps ); + //TODO: check addlemma + if (!addedLemma && !d_conflict) { + for(std::map< Node, std::vector< Node > >::const_iterator itr = XinR_with_exps.begin(); + itr != XinR_with_exps.end(); ++itr) { + std::vector<Node> vec_or; + d_regexp_opr.disjunctRegExp( itr->first, vec_or ); + Node tmp = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_or); + Trace("regexp-process") << "Got r: " << itr->first << " to " << tmp << std::endl; + /* + if(r.getKind() == kind::REGEXP_STAR) { + //TODO: apply R-Len + addedLemma = applyRLen(XinR_with_exps); + } else { + //TODO: split + } + */ + } + Assert(false); //TODO:tmp + } + } + + return addedLemma; +} + bool TheoryStrings::checkMemberships() { bool addedLemma = false; bool changed = false; @@ -2523,8 +2836,8 @@ bool TheoryStrings::checkMemberships() { Trace("regexp-debug") << "Checking Memberships ... " << std::endl; //if(options::stringEIT()) { //TODO: Opt for normal forms - for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin(); - itr_xr != d_str_re_map.end(); ++itr_xr ) { + for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); + itr_xr != d_pos_memberships.end(); ++itr_xr ) { bool spflag = false; Node x = (*itr_xr).first; NodeList* lst = (*itr_xr).second; @@ -3132,11 +3445,11 @@ void TheoryStrings::addMembership(Node assertion) { Node r = atom[1]; if(polarity) { NodeList* lst; - NodeListMap::iterator itr_xr = d_str_re_map.find( x ); - if( itr_xr == d_str_re_map.end() ){ + NodeListMap::iterator itr_xr = d_pos_memberships.find( x ); + if( itr_xr == d_pos_memberships.end() ){ lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_str_re_map.insertDataFromContextMemory( x, lst ); + d_pos_memberships.insertDataFromContextMemory( x, lst ); } else { lst = (*itr_xr).second; } @@ -3147,16 +3460,29 @@ void TheoryStrings::addMembership(Node assertion) { } } lst->push_back( r ); - }/* else { - if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { + } else { + /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); - d_regexp_memberships.push_back( a ); + }*/ + NodeList* lst; + NodeListMap::iterator itr_xr = d_neg_memberships.find( x ); + if( itr_xr == d_neg_memberships.end() ){ + lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_neg_memberships.insertDataFromContextMemory( x, lst ); } else { - d_regexp_memberships.push_back( assertion ); + lst = (*itr_xr).second; } - }*/ + //check + for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { + if( r == *itr ) { + return; + } + } + lst->push_back( r ); + } d_regexp_memberships.push_back( assertion ); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d9326c316..623647942 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -245,7 +245,18 @@ private: bool checkLengthsEqc(); bool checkCardinality(); bool checkInductiveEquations(); + //check membership constraints + Node normalizeRegexp(Node r); + bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps); + bool applyRConsume( CVC4::String &s, Node &r); + Node applyRSplit(Node s1, Node s2, Node r); + bool applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps); + bool checkMembershipsWithoutLength( + std::map< Node, std::vector< Node > > &memb_with_exps, + std::map< Node, std::vector< Node > > &XinR_with_exps); bool checkMemberships(); + //temp + bool checkMemberships2(); bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp); @@ -325,10 +336,17 @@ private: NodeList d_regexp_memberships; NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; + // stored assertions + NodeListMap d_pos_memberships; + NodeListMap d_neg_memberships; + // semi normal forms for symbolic expression + std::map< Node, Node > d_nf_regexps; + std::map< Node, std::vector< Node > > d_nf_regexps_exp; // intersection - NodeListMap d_str_re_map; NodeNodeMap d_inter_cache; NodeIntMap d_inter_index; + // processed memberships + NodeSet d_processed_memberships; // antecedant for why regexp membership must be true NodeNodeMap d_regexp_ant; // membership length diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c952a7b3c..dfec0a795 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -100,7 +100,7 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { if(!preNode.isNull()) { if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) { preNode = rewriteConcatString( - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); preNode = Node::null(); } else { @@ -143,7 +143,10 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); } else { if(!preNode.isNull()) { - node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + bool bflag = (preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ); + if(node_vec.empty() || !bflag ) { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + } } if(node_vec.size() > 1) { retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec); @@ -160,25 +163,42 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; Node retNode = node; std::vector<Node> node_vec; - bool flag = false; + bool allflag = false; for(unsigned i=0; i<node.getNumChildren(); ++i) { if(node[i].getKind() == kind::REGEXP_UNION) { Node tmpNode = prerewriteOrRegExp( node[i] ); if(tmpNode.getKind() == kind::REGEXP_UNION) { for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) { - node_vec.push_back( tmpNode[j] ); + if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) { + if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) { + node_vec.push_back( tmpNode[j] ); + } + } } + } else if(tmpNode.getKind() == kind::REGEXP_EMPTY) { + //nothing + } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) { + allflag = true; + retNode = tmpNode; + break; } else { - node_vec.push_back( tmpNode ); + if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) { + node_vec.push_back( tmpNode ); + } } - flag = true; } else if(node[i].getKind() == kind::REGEXP_EMPTY) { - flag = true; + //nothing + } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) { + allflag = true; + retNode = node[i]; + break; } else { - node_vec.push_back( node[i] ); + if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) { + node_vec.push_back( node[i] ); + } } } - if(flag) { + if(!allflag) { std::vector< Node > nvec; retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ) : node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec); @@ -187,6 +207,55 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { return retNode; } +Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) { + Assert( node.getKind() == kind::REGEXP_INTER ); + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; + Node retNode = node; + std::vector<Node> node_vec; + bool emptyflag = false; + //Node allNode = Node::null(); + for(unsigned i=0; i<node.getNumChildren(); ++i) { + if(node[i].getKind() == kind::REGEXP_INTER) { + Node tmpNode = prerewriteAndRegExp( node[i] ); + if(tmpNode.getKind() == kind::REGEXP_INTER) { + for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) { + if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) { + node_vec.push_back( tmpNode[j] ); + } + } + } else if(tmpNode.getKind() == kind::REGEXP_EMPTY) { + emptyflag = true; + retNode = tmpNode; + break; + } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) { + //allNode = tmpNode; + } else { + if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) { + node_vec.push_back( tmpNode ); + } + } + } else if(node[i].getKind() == kind::REGEXP_EMPTY) { + emptyflag = true; + retNode = node[i]; + break; + } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) { + //allNode = node[i]; + } else { + if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) { + node_vec.push_back( node[i] ); + } + } + } + if(!emptyflag) { + std::vector< Node > nvec; + retNode = node_vec.size() == 0 ? + NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) : + node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, node_vec); + } + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; + return retNode; +} + bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; i<t.getNumChildren(); ++i ) { @@ -603,6 +672,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } +bool TheoryStringsRewriter::hasEpsilonNode(TNode node) { + for(unsigned int i=0; i<node.getNumChildren(); i++) { + if(node[i].getKind() == kind::STRING_TO_REGEXP && node[i][0].getKind() == kind::CONST_STRING && node[i][0].getConst<String>().isEmptyString()) { + return true; + } + } + return false; +} + RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { Node retNode = node; Node orig = retNode; @@ -614,9 +692,36 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { retNode = prerewriteConcatRegExp(node); } else if(node.getKind() == kind::REGEXP_UNION) { retNode = prerewriteOrRegExp(node); + }else if(node.getKind() == kind::REGEXP_INTER) { + retNode = prerewriteAndRegExp(node); } else if(node.getKind() == kind::REGEXP_STAR) { if(node[0].getKind() == kind::REGEXP_STAR) { retNode = node[0]; + } else if(node[0].getKind() == kind::STRING_TO_REGEXP && node[0][0].getKind() == kind::CONST_STRING && node[0][0].getConst<String>().isEmptyString()) { + retNode = node[0]; + } else if(node[0].getKind() == kind::REGEXP_EMPTY) { + retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, + NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); + } else if(node[0].getKind() == kind::REGEXP_UNION) { + Node tmpNode = prerewriteOrRegExp(node[0]); + if(tmpNode.getKind() == kind::REGEXP_UNION) { + if(hasEpsilonNode(node[0])) { + std::vector< Node > node_vec; + for(unsigned int i=0; i<node[0].getNumChildren(); i++) { + if(node[0][i].getKind() == kind::STRING_TO_REGEXP && node[0][i][0].getKind() == kind::CONST_STRING && node[0][i][0].getConst<String>().isEmptyString()) { + //return true; + } else { + node_vec.push_back(node[0][i]); + } + } + retNode = node_vec.size()==1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec); + retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode); + } + } else if(tmpNode.getKind() == kind::STRING_TO_REGEXP && tmpNode[0].getKind() == kind::CONST_STRING && tmpNode[0].getConst<String>().isEmptyString()) { + retNode = tmpNode; + } else { + retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, tmpNode); + } } } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 9d04f107f..a1098f631 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -37,10 +37,12 @@ public: static Node rewriteConcatString(TNode node); static Node prerewriteConcatRegExp(TNode node); static Node prerewriteOrRegExp(TNode node); + static Node prerewriteAndRegExp(TNode node); static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); + static bool hasEpsilonNode(TNode node); static RewriteResponse preRewrite(TNode node); static inline void init() {} |