diff options
Diffstat (limited to 'src/theory/inst_match_impl.h')
-rw-r--r-- | src/theory/inst_match_impl.h | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/src/theory/inst_match_impl.h b/src/theory/inst_match_impl.h new file mode 100644 index 000000000..18c4998b8 --- /dev/null +++ b/src/theory/inst_match_impl.h @@ -0,0 +1,125 @@ +/********************* */ +/*! \file inst_match.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief inst match class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_MATCH_IMPL_H +#define __CVC4__INST_MATCH_IMPL_H + +#include "theory/inst_match.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers_engine.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +template<bool modEq> +InstMatchTrie2<modEq>::InstMatchTrie2(context::Context* c, QuantifiersEngine* qe): + d_data(c->getLevel()), d_context(c), d_mods(c) { + d_eQ = qe->getEqualityQuery(); + d_eE = ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine(); +}; + +/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ +template<bool modEq> +void InstMatchTrie2<modEq>::addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel ) { + if( current == end ) return; + + Assert(root->e.find(current->second) == root->e.end()); + Tree * root2 = new Tree(currLevel); + root->e.insert(make_pair(current->second, root2)); + addSubTree(root2, ++current, end, currLevel ); +} + +/** exists match */ +template<bool modEq> +bool InstMatchTrie2<modEq>::existsInstMatch(InstMatchTrie2<modEq>::Tree * root, + mapIter & current, mapIter & end, + Tree * & e, mapIter & diverge) const{ + if( current == end ) { + Debug("Trie2") << "Trie2 Bottom " << std::endl; + --current; + return true; + }; //Already their + + if (current->first > diverge->first){ + // this point is the deepest point currently seen map are ordered + e = root; + diverge = current; + }; + + TNode n = current->second; + typename InstMatchTrie2<modEq>::Tree::MLevel::iterator it = + root->e.find( n ); + if( it!=root->e.end() && + existsInstMatch( (*it).second, ++current, end, e, diverge) ){ + Debug("Trie2") << "Trie2 Directly here " << n << std::endl; + --current; + return true; + } + Assert( it==root->e.end() || e != root ); + + // Even if n is in the trie others of the equivalence class + // can also be in it since the equality can have appeared + // after they have been added + if( modEq && d_eE->hasTerm( n ) ){ + //check modulo equality if any other instantiation match exists + eq::EqClassIterator eqc( d_eQ->getRepresentative( n ), d_eE ); + for( ;!eqc.isFinished();++eqc ){ + TNode en = (*eqc); + if( en == n ) continue; // already tested + typename InstMatchTrie2<modEq>::Tree::MLevel::iterator itc = + root->e.find( en ); + if( itc!=root->e.end() && + existsInstMatch( (*itc).second, ++current, end, e, diverge) ){ + Debug("Trie2") << "Trie2 Indirectly here by equality " << n << " = " << en << std::endl; + --current; + return true; + } + Assert( itc==root->e.end() || e != root ); + } + } + --current; + return false; +} + +template<bool modEq> +bool InstMatchTrie2<modEq>::addInstMatch( InstMatch& m ) { + mapIter begin = m.d_map.begin(); + mapIter end = m.d_map.end(); + InstMatchTrie2<modEq>::Tree * e = &d_data; + mapIter diverge = begin; + if( !existsInstMatch(e, begin, end, e, diverge ) ){ + Assert(!diverge->second.isNull()); + size_t currLevel = d_context->getLevel(); + addSubTree( e, diverge, end, currLevel ); + if(e->level != currLevel) + //If same level that e, will be removed at the same time than e + d_mods.push_back(make_pair(e,diverge->second)); + return true; + }else{ + return false; + } +} + +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__INST_MATCH_IMPL_H */ |