diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rwxr-xr-x[-rw-r--r--] | src/theory/quantifiers/term_database.cpp | 455 |
1 files changed, 309 insertions, 146 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 8b09d8e5d..d3a5e178f 100644..100755 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -84,13 +84,13 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); if( options::ceGuidedInst() ){ - d_sygus_tdb = new TermDbSygus; + d_sygus_tdb = new TermDbSygus( c, qe ); }else{ d_sygus_tdb = NULL; } @@ -163,9 +163,18 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi //if this is an atomic trigger, consider adding it if( inst::Trigger::isAtomicTrigger( n ) ){ Trace("term-db") << "register term in db " << n << std::endl; + if( options::finiteModelFind() ){ + computeModelBasisArgAttribute( n ); + } + Node op = getMatchOperator( n ); + Trace("term-db-debug") << " match operator is : " << op << std::endl; d_op_map[op].push_back( n ); added.insert( n ); + + if( d_sygus_tdb ){ + d_sygus_tdb->registerEvalTerm( n ); + } if( options::eagerInstQuant() ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ @@ -178,6 +187,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi } } } + }else{ + setTermInactive( n ); } rec = true; } @@ -210,7 +221,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { for( unsigned i=0; i<d_op_map[f].size(); i++ ){ TNode n = d_op_map[f][i]; if( hasTermCurrent( n ) ){ - if( !n.getAttribute(NoMatchAttribute()) ){ + if( isTermActive( n ) ){ computeArgReps( n ); TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n; d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); @@ -220,7 +231,84 @@ void TermDb::computeUfEqcTerms( TNode f ) { } } +void TermDb::computeUfTerms( TNode f ) { + if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){ + d_op_nonred_count[ f ] = 0; + std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); + if( it!=d_op_map.end() ){ + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; + unsigned congruentCount = 0; + unsigned nonCongruentCount = 0; + unsigned alreadyCongruentCount = 0; + unsigned relevantCount = 0; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + //to be added to term index, term must be relevant, and exist in EE + if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + relevantCount++; + if( isTermActive( n ) ){ + computeArgReps( n ); + + Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; + for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ + Trace("term-db-debug") << d_arg_reps[n][i] << " "; + if( std::find( d_func_map_rel_dom[f][i].begin(), + d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){ + d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] ); + } + } + Trace("term-db-debug") << std::endl; + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] ); + Trace("term-db-debug2") << "...add term returned " << at << std::endl; + if( at!=n && ee->areEqual( at, n ) ){ + setTermInactive( n ); + Trace("term-db-debug") << n << " is redundant." << std::endl; + congruentCount++; + }else{ + if( at!=n && ee->areDisequal( at, n, false ) ){ + std::vector< Node > lits; + lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) ); + for( unsigned i=0; i<at.getNumChildren(); i++ ){ + if( at[i]!=n[i] ){ + lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() ); + } + } + Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); + if( Trace.isOn("term-db-lemma") ){ + Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; + if( !d_quantEngine->getTheoryEngine()->needCheck() ){ + Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + } + Trace("term-db-lemma") << " add lemma : " << lem << std::endl; + } + d_quantEngine->addLemma( lem ); + d_consistent_ee = false; + return; + } + nonCongruentCount++; + d_op_nonred_count[ f ]++; + } + }else{ + Trace("term-db-debug") << n << " is already redundant." << std::endl; + alreadyCongruentCount++; + } + }else{ + Trace("term-db-debug") << n << " is not relevant." << std::endl; + } + } + if( Trace.isOn("tdb") ){ + Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; + Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; + Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; + } + } + } +} + bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { + computeUfTerms( f ); Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r ); std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); if( it != d_func_map_rel_dom.end() ){ @@ -237,25 +325,23 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { //return a term n' equivalent to n // maximal subterms of n' are representatives in the equality engine qy -Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) { +Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ) { std::map< TNode, Node >::iterator itv = visited.find( n ); if( itv != visited.end() ){ return itv->second; } Trace("term-db-eval") << "evaluate term : " << n << std::endl; - Node ret; - if( n.getKind()==BOUND_VARIABLE ){ - return n; + Node ret = n; + if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ + //do nothing }else if( !qy->hasTerm( n ) ){ //term is not known to be equal to a representative in equality engine, evaluate it - if( n.getKind()==FORALL ){ - ret = Node::null(); - }else if( n.hasOperator() ){ + if( n.hasOperator() ){ TNode f = getMatchOperator( n ); std::vector< TNode > args; bool ret_set = false; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = evaluateTerm2( n[i], visited, qy ); + TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests ); if( c.isNull() ){ ret = Node::null(); ret_set = true; @@ -267,7 +353,7 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ ret_set = true; break; }else if( n.getKind()==kind::ITE && i==0 ){ - ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy ); + ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests ); ret_set = true; break; } @@ -295,6 +381,22 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ } ret = NodeManager::currentNM()->mkNode( n.getKind(), args ); ret = Rewriter::rewrite( ret ); + if( ret.getKind()==kind::EQUAL ){ + if( qy->areDisequal( ret[0], ret[1] ) ){ + ret = d_false; + } + } + if( useEntailmentTests ){ + if( ret.getKind()==kind::EQUAL || ret.getKind()==kind::GEQ ){ + for( unsigned j=0; j<2; j++ ){ + std::pair<bool, Node> et = d_quantEngine->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, j==0 ? ret : ret.negate() ); + if( et.first ){ + ret = j==0 ? d_true : d_false; + break; + } + } + } + } } } } @@ -316,14 +418,16 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su return n; }else if( n.getKind()==BOUND_VARIABLE ){ if( hasSubs ){ - Assert( subs.find( n )!=subs.end() ); - Trace("term-db-entail") << "...substitution is : " << subs[n] << std::endl; - if( subsRep ){ - Assert( qy->getEngine()->hasTerm( subs[n] ) ); - Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] ); - return subs[n]; - }else{ - return getEntailedTerm2( subs[n], subs, subsRep, hasSubs, qy ); + std::map< TNode, TNode >::iterator it = subs.find( n ); + if( it!=subs.end() ){ + Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; + if( subsRep ){ + Assert( qy->getEngine()->hasTerm( it->second ) ); + Assert( qy->getEngine()->getRepresentative( it->second )==it->second ); + return it->second; + }else{ + return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy ); + } } } }else if( n.getKind()==ITE ){ @@ -355,12 +459,12 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su return TNode::null(); } -Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) { +Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy, bool useEntailmentTests ) { if( qy==NULL ){ qy = d_quantEngine->getEqualityQuery(); } std::map< TNode, Node > visited; - return evaluateTerm2( n, visited, qy ); + return evaluateTerm2( n, visited, qy, useEntailmentTests ); } TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) { @@ -436,6 +540,8 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false ); } } + }else if( n.getKind()==FORALL && !pol ){ + return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy ); } return false; } @@ -457,6 +563,18 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return isEntailed2( n, subs, subsRep, true, pol, qy ); } +bool TermDb::isTermActive( Node n ) { + return d_inactive_map.find( n )==d_inactive_map.end(); + //return !n.getAttribute(NoMatchAttribute()); +} + +void TermDb::setTermInactive( Node n ) { + d_inactive_map[n] = true; + //Trace("term-db-debug2") << "set no match attribute" << std::endl; + //NoMatchAttribute nma; + //n.setAttribute(nma,true); +} + bool TermDb::hasTermCurrent( Node n, bool useMode ) { if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); @@ -556,10 +674,6 @@ void TermDb::presolve() { } bool TermDb::reset( Theory::Effort effort ){ - int nonCongruentCount = 0; - int congruentCount = 0; - int alreadyCongruentCount = 0; - int nonRelevantCount = 0; d_op_nonred_count.clear(); d_arg_reps.clear(); d_func_map_trie.clear(); @@ -614,89 +728,20 @@ bool TermDb::reset( Theory::Effort effort ){ } } +/* //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - d_op_nonred_count[ it->first ] = 0; - Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - Node n = it->second[i]; - //to be added to term index, term must be relevant, and exist in EE - if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ - if( !n.getAttribute(NoMatchAttribute()) ){ - if( options::finiteModelFind() ){ - computeModelBasisArgAttribute( n ); - } - computeArgReps( n ); - - Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ - Trace("term-db-debug") << d_arg_reps[n][i] << " "; - if( std::find( d_func_map_rel_dom[it->first][i].begin(), - d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){ - d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] ); - } - } - Trace("term-db-debug") << std::endl; - if( ee->hasTerm( n ) ){ - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; - } - Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); - if( at!=n && ee->areEqual( at, n ) ){ - NoMatchAttribute nma; - n.setAttribute(nma,true); - Trace("term-db-debug") << n << " is redundant." << std::endl; - congruentCount++; - }else{ - if( at!=n && ee->areDisequal( at, n, false ) ){ - std::vector< Node > lits; - lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) ); - for( unsigned i=0; i<at.getNumChildren(); i++ ){ - if( at[i]!=n[i] ){ - lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() ); - } - } - Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; - if( !d_quantEngine->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - } - Trace("term-db-lemma") << " add lemma : " << lem << std::endl; - } - d_quantEngine->addLemma( lem ); - d_consistent_ee = false; - return false; - } - nonCongruentCount++; - d_op_nonred_count[ it->first ]++; - } - }else{ - Trace("term-db-debug") << n << " is already redundant." << std::endl; - congruentCount++; - alreadyCongruentCount++; - } - }else{ - Trace("term-db-debug") << n << " is not relevant." << std::endl; - nonRelevantCount++; - } - } - } - Trace("term-db-stats") << "TermDb: Reset" << std::endl; - Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "functions : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - if( it->second.size()>0 ){ - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]); - } + computeUfTerms( it->first ); + if( !d_consistent_ee ){ + return false; } } +*/ return true; } TermArgTrie * TermDb::getTermArgTrie( Node f ) { + computeUfTerms( f ); std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); if( itut!=d_func_map_trie.end() ){ return &itut->second; @@ -725,11 +770,18 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { } TNode TermDb::getCongruentTerm( Node f, Node n ) { - computeArgReps( n ); - return d_func_map_trie[f].existsTerm( d_arg_reps[n] ); + computeUfTerms( f ); + std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); + if( itut!=d_func_map_trie.end() ){ + computeArgReps( n ); + return itut->second.existsTerm( d_arg_reps[n] ); + }else{ + return TNode::null(); + } } TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { + computeUfTerms( f ); return d_func_map_trie[f].existsTerm( args ); } @@ -822,6 +874,7 @@ void TermDb::makeInstantiationConstantsFor( Node q ){ Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ d_vars[q].push_back( q[0][i] ); + d_var_num[q][q[0][i]] = i; //make instantiation constants Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() ); d_inst_constants_map[ic] = q; @@ -832,9 +885,8 @@ void TermDb::makeInstantiationConstantsFor( Node q ){ ic.setAttribute( ivna, i ); InstConstantAttribute ica; ic.setAttribute( ica, q ); - //also set the no-match attribute - NoMatchAttribute nma; - ic.setAttribute(nma,true); + //also set the term inactive + setTermInactive( ic ); } } } @@ -892,11 +944,6 @@ Node TermDb::getInstConstAttr( Node n ) { } InstConstantAttribute ica; n.setAttribute(ica, q); - if( !q.isNull() ){ - //also set the no-match attribute - NoMatchAttribute nma; - n.setAttribute(nma,true); - } } return n.getAttribute(InstConstantAttribute()); } @@ -1005,9 +1052,12 @@ Node TermDb::getCounterexampleLiteral( Node q ){ Node TermDb::getInstConstantNode( Node n, Node q ){ makeInstantiationConstantsFor( q ); - Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(), - d_inst_constants[q].begin(), d_inst_constants[q].end() ); - return n2; + return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); +} + +Node TermDb::getVariableNode( Node n, Node q ) { + makeInstantiationConstantsFor( q ); + return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); } Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { @@ -1512,7 +1562,7 @@ struct sortTermOrder { //this function makes a canonical representation of a term ( // - orders variables left to right // - if apply_torder, then sort direct subterms of commutative operators -Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) { +Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) { Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; if( n.getKind()==BOUND_VARIABLE ){ std::map< TNode, TNode >::iterator it = subs.find( n ); @@ -1529,32 +1579,38 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun return it->second; } }else if( n.getNumChildren()>0 ){ - //collect children - Trace("canon-term-debug") << "Collect children" << std::endl; - std::vector< Node > cchildren; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - cchildren.push_back( n[i] ); - } - //if applicable, first sort by term order - if( apply_torder && isComm( n.getKind() ) ){ - Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; - sortTermOrder sto; - sto.d_tdb = this; - std::sort( cchildren.begin(), cchildren.end(), sto ); - } - //now make canonical - Trace("canon-term-debug") << "Make canonical children" << std::endl; - for( unsigned i=0; i<cchildren.size(); i++ ){ - cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder ); - } - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl; - cchildren.insert( cchildren.begin(), n.getOperator() ); - } - Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; - Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); - Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; - return ret; + std::map< TNode, Node >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + //collect children + Trace("canon-term-debug") << "Collect children" << std::endl; + std::vector< Node > cchildren; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + cchildren.push_back( n[i] ); + } + //if applicable, first sort by term order + if( apply_torder && isComm( n.getKind() ) ){ + Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; + sortTermOrder sto; + sto.d_tdb = this; + std::sort( cchildren.begin(), cchildren.end(), sto ); + } + //now make canonical + Trace("canon-term-debug") << "Make canonical children" << std::endl; + for( unsigned i=0; i<cchildren.size(); i++ ){ + cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited ); + } + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl; + cchildren.insert( cchildren.begin(), n.getOperator() ); + } + Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; + Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + visited[n] = ret; + return ret; + } }else{ Trace("canon-term-debug") << "...return 0-child term." << std::endl; return n; @@ -1564,7 +1620,8 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ std::map< TypeNode, unsigned > var_count; std::map< TNode, TNode > subs; - return getCanonicalTerm( n, var_count, subs, apply_torder ); + std::map< TNode, Node > visited; + return getCanonicalTerm( n, var_count, subs, apply_torder, visited ); } void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) { @@ -1790,6 +1847,18 @@ bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& c } } +void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr()); + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate(); + if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){ + cond.push_back( rc ); + } + getRelevancyCondition( n[0], cond ); + } +} + bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { if( n==t ){ return true; @@ -1856,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) { bool ret = false; if( n.getKind()==UNINTERPRETED_CONSTANT ){ ret = true; - }else{ + }else{ for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( containsUninterpretedConstant( n[i] ) ){ ret = true; @@ -1884,7 +1953,8 @@ Node TermDb::simpleNegate( Node n ){ bool TermDb::isAssoc( Kind k ) { return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || + k==STRING_CONCAT; } bool TermDb::isComm( Kind k ) { @@ -2184,11 +2254,15 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) { } } -TermDbSygus::TermDbSygus(){ +TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } +bool TermDbSygus::reset( Theory::Effort e ) { + return true; +} + TNode TermDbSygus::getVar( TypeNode tn, int i ) { while( i>=(int)d_fv[tn].size() ){ std::stringstream ss; @@ -2400,8 +2474,8 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; - Assert( n.getKind()==APPLY_CONSTRUCTOR ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( n.getKind()==APPLY_CONSTRUCTOR ); unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); Assert( n.getNumChildren()==dt[i].getNumArgs() ); std::map< TypeNode, int > var_count; @@ -3051,6 +3125,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > std::string name = std::string( str.begin() + found +1, str.end() ); out << name; }else{ + Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl; out << op; } if( n.getNumChildren()>0 ){ @@ -3118,3 +3193,91 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << n; } } + +Node TermDbSygus::getAnchor( Node n ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + return getAnchor( n[0] ); + }else{ + return n; + } +} + +void TermDbSygus::registerEvalTerm( Node n ) { + if( options::sygusDirectEval() ){ + if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ + Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl; + TypeNode tn = n[0].getType(); + if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + Node f = n.getOperator(); + Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl; + if( n[0].getKind()!=APPLY_CONSTRUCTOR ){ + d_evals[n[0]].push_back( n ); + TypeNode tn = n[0].getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + Assert( dt.isSygus() ); + d_eval_args[n[0]].push_back( std::vector< Node >() ); + for( unsigned j=1; j<n.getNumChildren(); j++ ){ + if( var_list[j-1].getType().isBoolean() ){ + //TODO: remove this case when boolean term conversion is eliminated + Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); + }else{ + d_eval_args[n[0]].back().push_back( n[j] ); + } + } + Node a = getAnchor( n[0] ); + d_subterms[a][n[0]] = true; + } + } + } + } + } +} + +void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) { + std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a ); + if( its!=d_subterms.end() ){ + Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl; + for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){ + Node n = itss->first; + Trace("sygus-eager-debug") << "...process : " << n << std::endl; + std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n ); + if( it!=d_eval_args.end() && !it->second.empty() ){ + TNode at = a; + TNode vt = v; + Node vn = n.substitute( at, vt ); + vn = Rewriter::rewrite( vn ); + unsigned start = d_node_mv_args_proc[n][vn]; + Node antec = n.eqNode( vn ).negate(); + TypeNode tn = n.getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl; + Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl; + Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn ); + Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl; + std::vector< Node > vars; + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + for( unsigned j=0; j<var_list.getNumChildren(); j++ ){ + vars.push_back( var_list[j] ); + } + //for each evaluation + for( unsigned i=start; i<it->second.size(); i++ ){ + Assert( vars.size()==it->second[i].size() ); + Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); + Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); + lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); + Trace("sygus-eager") << "Lemma : " << lem << std::endl; + lems.push_back( lem ); + } + d_node_mv_args_proc[n][vn] = it->second.size(); + } + } + } +} + |