diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:47 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:56 -0500 |
commit | c87ee73ad3d51c238700f236c18e425b80e8e7ac (patch) | |
tree | aa4214b0fa7d6ef275605253fee88899fa3ce230 /src/theory/quantifiers/conjecture_generator.cpp | |
parent | a2923ec61b601b0e3f4f78f22fffc1c2421f0d81 (diff) |
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index fa71f0132..f4eb67d74 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1572,7 +1572,6 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, if( d_match_status_child_num==0 ){ //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); - //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc ); Assert( !eqc.isNull() ); TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f ); if( tat ){ @@ -1726,9 +1725,9 @@ void TermGenEnv::collectSignatureInformation() { d_func_kind.clear(); d_func_args.clear(); TypeNode tnull; - for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ - if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){ - Node nn = getTermDatabase()->getGroundTerm( it->first, 0 ); + for( std::map< Node, std::vector< Node > >::iterator it = getTermDatabase()->d_op_map.begin(); it != getTermDatabase()->d_op_map.end(); ++it ){ + if( !it->second.empty() ){ + Node nn = it->second[0]; Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; @@ -1750,7 +1749,7 @@ void TermGenEnv::collectSignatureInformation() { d_typ_tg_funcs[nn.getType()].push_back( it->first ); d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED ); Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl; - getTermDatabase()->computeUfEqcTerms( it->first ); + //getTermDatabase()->computeUfEqcTerms( it->first ); } } Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl; |