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/bv/theory_bv.cpp | |
parent | 20fc32c0c4a2518673e1cbaa0afb3c4fb284ffe6 (diff) |
Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this.
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fec93e033..f0981044b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -495,7 +495,36 @@ void TheoryBV::propagate(Effort e) { } } +eq::EqualityEngine * TheoryBV::getEqualityEngine() { + return NULL; +} +bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { +#if 0 + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if( core ){ + //get the constant equivalence classes + bool retVal = false; + for( unsigned i=0; i<vars.size(); i++ ){ + Node n = vars[i]; + if( core->getEqualityEngine()->hasTerm( n ) ){ + Node nr = core->getEqualityEngine()->getRepresenative( n ); + if( nr.isConst() ){ + subs.push_back( nr ); + exp[n].push_back( n.eqNode( nr ) ); + retVal = true; + }else{ + subs.push_back( n ); + } + } + } + //return true if the substitution is non-trivial + return retVal; + } +#endif + return false; +} + Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: |