diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-16 11:07:36 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-16 11:07:36 +0200 |
commit | 548582b252170f35a602705a109d88a608611cca (patch) | |
tree | abcfe42578de4b4a99905ed76e1df23c396820ef /src/theory/rep_set.cpp | |
parent | bad7f4fe4dca4c6511c2862bf81b6791640ac78f (diff) |
Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 6a64f762e..a90a4cf17 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -29,6 +29,7 @@ void RepSet::clear(){ d_type_complete.clear(); d_tmap.clear(); d_values_to_terms.clear(); + d_type_rlv_rep.clear(); } bool RepSet::hasRep( TypeNode tn, Node n ) { @@ -91,7 +92,7 @@ int RepSet::getIndexFor( Node n ) const { bool RepSet::complete( TypeNode t ){ std::map< TypeNode, bool >::iterator it = d_type_complete.find( t ); if( it==d_type_complete.end() ){ - //remove all previous + //remove all previous for( unsigned i=0; i<d_type_reps[t].size(); i++ ){ d_tmap.erase( d_type_reps[t][i] ); } @@ -116,6 +117,15 @@ bool RepSet::complete( TypeNode t ){ } } +int RepSet::getNumRelevantGroundReps( TypeNode t ) { + std::map< TypeNode, int >::iterator it = d_type_rlv_rep.find( t ); + if( it==d_type_rlv_rep.end() ){ + return 0; + }else{ + return it->second; + } +} + void RepSet::toStream(std::ostream& out){ #if 0 for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ @@ -193,7 +203,7 @@ bool RepSetIterator::initialize(){ //FIXME: // terms in rep_set are now constants which mapped to terms through TheoryModel // thus, should introduce a constant and a term. for now, just a term. - + //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; |