diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-16 12:24:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-16 12:25:29 -0500 |
commit | 36cfaab5caa86773e47a8cca8f4d8c0d5edec99f (patch) | |
tree | 19ce13bba397a6139ac42e658417074c462b2318 /src/theory/theory.cpp | |
parent | 20fc32c0c4a2518673e1cbaa0afb3c4fb284ffe6 (diff) |
Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this.
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 141 |
1 files changed, 141 insertions, 0 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 7e2b6df55..7fa74df6a 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -66,6 +66,7 @@ Theory::Theory(TheoryId id, context::Context* satContext, , d_sharedTermsIndex(satContext, 0) , d_careGraph(NULL) , d_quantEngine(NULL) + , d_extt(NULL) , d_checkTime(getFullInstanceName() + "::checkTime") , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime") , d_sharedTerms(satContext) @@ -311,5 +312,145 @@ TheoryId EntailmentCheckSideEffects::getTheoryId() const { EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { } + +ExtTheory::ExtTheory( Theory * p ) : d_parent( p ), +d_ext_func_terms( p->getSatContext() ), d_has_extf( p->getSatContext() ){ + +} + +void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { + if( !n.isConst() ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getNumChildren()>0 ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectVars( n[i], vars, visited ); + } + }else{ + vars.push_back( n ); + } + } + } +} + +//do inferences +void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) { + //all variables we need to find a substitution for + std::vector< Node > vars; + std::vector< Node > sub; + std::map< Node, std::vector< Node > > expc; + Trace("extt-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl; + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second ){ + Node n = (*it).first; + terms.push_back( n ); + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){ + if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){ + vars.push_back( iti->second.d_vars[i] ); + } + } + } + } + Trace("extt-debug") << "..." << terms.size() << " unreduced." << std::endl; + if( !terms.empty() ){ + //get the current substitution + if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){ + for( unsigned i=0; i<terms.size(); i++ ){ + //do substitution, rewrite + Node n = terms[i]; + Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() ); + std::vector< Node > expn; + if( ns!=n ){ + //build explanation: explanation vars = sub for each vars in FV( n ) + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){ + Node v = iti->second.d_vars[j]; + std::map< Node, std::vector< Node > >::iterator itx = expc.find( v ); + if( itx!=expc.end() ){ + for( unsigned k=0; k<itx->second.size(); k++ ){ + if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){ + expn.push_back( itx->second[k] ); + } + } + } + } + } + Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl; + //add to vector + sterms.push_back( ns ); + exp.push_back( expn ); + } + }else{ + for( unsigned i=0; i<terms.size(); i++ ){ + sterms.push_back( terms[i] ); + } + } + } +} + +//register term +void ExtTheory::registerTerm( Node n ) { + if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){ + if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ + Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl; + d_ext_func_terms[n] = true; + d_has_extf = true; + std::map< Node, bool > visited; + collectVars( n, d_extf_info[n].d_vars, visited ); + } + } +} + +//mark reduced +void ExtTheory::markReduced( Node n ) { + d_ext_func_terms[n] = false; + //TODO update has_extf +} + +//mark congruent +void ExtTheory::markCongruent( Node a, Node b ) { + NodeBoolMap::const_iterator it = d_ext_func_terms.find( b ); + if( it!=d_ext_func_terms.end() ){ + if( d_ext_func_terms.find( a )==d_ext_func_terms.end() ){ + d_ext_func_terms[a] = (*it).second; + }else{ + d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second; + } + d_ext_func_terms[b] = false; + } +} + +//is active +bool ExtTheory::isActive( Node n ) { + NodeBoolMap::const_iterator it = d_ext_func_terms.find( n ); + if( it!=d_ext_func_terms.end() ){ + return (*it).second; + }else{ + return false; + } +} +//get active +void ExtTheory::getActive( std::vector< Node >& active ) { + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second ){ + active.push_back( (*it).first ); + } + } +} + +void ExtTheory::getActive( std::vector< Node >& active, Kind k ) { + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second && (*it).first.getKind()==k ){ + active.push_back( (*it).first ); + } + } +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |