From b88133bc679c541798c2063fec2bc441e744328a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 31 Jul 2012 21:24:31 +0000 Subject: Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat. The namespaces weren't changed, only the file locations. --- src/theory/rewriterules/rr_inst_match.h | 266 ++++++++++++++++++++++++++++++++ 1 file changed, 266 insertions(+) create mode 100644 src/theory/rewriterules/rr_inst_match.h (limited to 'src/theory/rewriterules/rr_inst_match.h') diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h new file mode 100644 index 000000000..d2a246769 --- /dev/null +++ b/src/theory/rewriterules/rr_inst_match.h @@ -0,0 +1,266 @@ +/********************* */ +/*! \file rr_inst_match.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 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__THEORY__REWRITERULES__RR_INST_MATCH_H +#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H + +#include "theory/theory.h" +#include "util/hash.h" +#include "util/ntuple.h" + +#include +#include +#include + +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "context/cdlist.h" + +#include "theory/quantifiers/inst_match.h" +#include "expr/node_manager.h" +#include "expr/node_builder.h" + +#include "theory/quantifiers/options.h" +#include "theory/rewriterules/options.h" + +//#define USE_EFFICIENT_E_MATCHING + +namespace CVC4 { +namespace theory { + +namespace rrinst{ + +class CandidateGenerator +{ +public: + CandidateGenerator(){} + virtual ~CandidateGenerator(){}; + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( TNode eqc ) = 0; + virtual TNode getNextCandidate() = 0; + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + static inline bool isLegalCandidate( TNode n ){ + return !n.getAttribute(NoMatchAttribute()) && + ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) && + ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) ); +} + +}; + + +inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { + m.toStream(out); + return out; +} + +template class InstMatchTrie2; +template class InstMatchTrie2Pairs; + +template +class InstMatchTrie2Gen +{ + friend class InstMatchTrie2; + friend class InstMatchTrie2Pairs; + +private: + + class Tree { + public: + typedef std::hash_map< Node, Tree *, NodeHashFunction > MLevel; + MLevel e; + const size_t level; //context level of creation + Tree() CVC4_UNDEFINED; + const Tree & operator =(const Tree & t){ + Assert(t.e.empty()); Assert(e.empty()); + Assert(t.level == level); + return t; + } + Tree(size_t l): level(l) {}; + ~Tree(){ + for(typename MLevel::iterator i = e.begin(); i!=e.end(); ++i) + delete(i->second); + }; + }; + + + typedef std::pair Mod; + + class CleanUp{ + public: + inline void operator()(Mod * m){ + typename Tree::MLevel::iterator i = m->first->e.find(m->second); + Assert (i != m->first->e.end()); //should not have been already removed + m->first->e.erase(i); + }; + }; + + EqualityQuery* d_eQ; + CandidateGenerator * d_cG; + + context::Context* d_context; + context::CDList > d_mods; + + + typedef std::map::const_iterator mapIter; + + /** add the substitution given by the iterator*/ + void addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel); + /** test if it exists match, modulo uf-equations if modEq is true if + * return false the deepest point of divergence is put in [e] and + * [diverge]. + */ + bool existsInstMatch( Tree * root, + mapIter & current, mapIter & end, + Tree * & e, mapIter & diverge) const; + + /** add match m in the trie root + return true if it was never seen */ + bool addInstMatch( InstMatch& m, Tree * root); + +public: + InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* q); + InstMatchTrie2Gen(const InstMatchTrie2Gen &) CVC4_UNDEFINED; + const InstMatchTrie2Gen & operator =(const InstMatchTrie2Gen & e) CVC4_UNDEFINED; +}; + +template +class InstMatchTrie2 +{ + typename InstMatchTrie2Gen::Tree d_data; + InstMatchTrie2Gen d_backtrack; +public: + InstMatchTrie2(context::Context* c, QuantifiersEngine* q): d_data(0), + d_backtrack(c,q) {}; + InstMatchTrie2(const InstMatchTrie2 &) CVC4_UNDEFINED; + const InstMatchTrie2 & operator =(const InstMatchTrie2 & e) CVC4_UNDEFINED; + /** add match m in the trie, + return true if it was never seen */ + inline bool addInstMatch( InstMatch& m){ + return d_backtrack.addInstMatch(m,&d_data); + }; + +};/* class InstMatchTrie2 */ + +class Matcher +{ +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset the term to match, return false if there is no such term */ + virtual bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ) = 0; + /** get the next match. If it return false once you shouldn't call + getNextMatch again before doing a reset */ + virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** If reset, or getNextMatch return false they remove from the + InstMatch the binding that they have previously created */ + + /** virtual Matcher in order to have definned behavior */ + virtual ~Matcher(){}; +}; + + +class ApplyMatcher: public Matcher{ +private: + /** What to check first: constant and variable */ + std::vector< triple< TNode,size_t,EqualityQuery* > > d_constants; + std::vector< triple< TNode,size_t,EqualityQuery* > > d_variables; + /** children generators, only the sub-pattern which are + neither a variable neither a constant appears */ + std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens; + /** the variable that have been set by this matcher (during its own reset) */ + std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */ + /** the representant of the argument of the term given by the last reset */ + std::vector< Node > d_reps; +public: + /** The pattern we are producing matches for */ + Node d_pattern; +public: + /** constructors */ + ApplyMatcher( Node pat, QuantifiersEngine* qe); + /** destructor */ + ~ApplyMatcher(){/*TODO delete dandling pointers? */} + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ); + /** reset the term to match */ + bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ); + /** get the next match. */ + bool getNextMatch(InstMatch& m, QuantifiersEngine* qe); +private: + bool getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset); +}; + + +/* Match literal so you don't choose the equivalence class( */ +class PatMatcher +{ +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset the matcher, return false if there is no such term */ + virtual bool reset( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** get the next match. If it return false once you shouldn't call + getNextMatch again before doing a reset */ + virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** If reset, or getNextMatch return false they remove from the + InstMatch the binding that they have previously created */ +}; + +Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ); +PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ); + +/* Match literal so you don't choose the equivalence class( */ +class PatsMatcher +{ +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset the matcher, return false if there is no such term */ + virtual bool getNextMatch( QuantifiersEngine* qe ) = 0; + virtual const InstMatch& getInstMatch() = 0; + /** Add directly the instantiation to quantifiers engine */ + virtual int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe) = 0; +}; + +PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ); +PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ); + +/** return true if whatever Node is subsituted for the variables the + given Node can't match the pattern */ +bool nonunifiable( TNode t, TNode pat, const std::vector & vars); + +class InstMatchGenerator; + +}/* CVC4::theory rrinst */ + +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H */ -- cgit v1.2.3