diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b4d6654b1..69220ad62 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -420,9 +420,40 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ } - // notify each theory using the statement above + // static learning for each theory using the statement above CVC4_FOR_EACH_THEORY } +Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) { + SimplifyCache::Scope cache(d_simplifyCache, in); + if(cache) { + outSubstitutions.insert(outSubstitutions.end(), + cache.get().second.begin(), + cache.get().second.end()); + return cache.get().first; + } + + size_t prevSize = outSubstitutions.size(); + + TNode atom = in.getKind() == kind::NOT ? in[0] : in; + + theory::Theory* theory = theoryOf(atom); + + Debug("simplify") << push << "simplifying " << in << " to " << theory->identify() << std::endl; + Node n = theory->simplify(in, outSubstitutions); + Debug("simplify") << "got from " << theory->identify() << " : " << n << std::endl << pop; + + atom = n.getKind() == kind::NOT ? n[0] : n; + + if(atom.getKind() == kind::EQUAL) { + theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType()); + Debug("simplify") << push << "simplifying " << n << " to " << typeTheory << std::endl; + n = d_theoryTable[typeTheory]->simplify(n, outSubstitutions); + Debug("simplify") << "got from " << d_theoryTable[typeTheory]->identify() << " : " << n << std::endl << pop; + } + + cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end()))); + return n; +} }/* CVC4 namespace */ |