X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Fquantifiers%2Finst_match.h;h=324b2c7368fb481525db64178aa2375775c1b2b7;hb=4fb65ae4d0018dc01fe79df8bbf7f3ec0ff583b9;hp=b9e61be20c801082c350dc93db25fc4497022f1a;hpb=a485a56258bdac2cdb2214dbcae5268b11f1d95b;p=cvc5.git diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index b9e61be20..324b2c736 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -1,204 +1,100 @@ /********************* */ /*! \file 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 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Francois Bobot + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. 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__QUANTIFIERS__INST_MATCH_H -#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#include "util/hash.h" -#include "context/cdo.h" +#include -#include -#include - -#include "context/cdlist.h" #include "expr/node.h" namespace CVC4 { namespace theory { -class QuantifiersEngine; class EqualityQuery; namespace inst { -/** basic class defining an instantiation */ +/** Inst match + * + * This is the basic class specifying an instantiation. Its domain size (the + * size of d_vals) is the number of bound variables of the quantified formula + * that is passed to its constructor. + * + * The values of d_vals may be null, which indicate that the field has + * yet to be initialized. + */ class InstMatch { - /* map from variable to ground terms */ - std::map< Node, Node > d_map; public: - InstMatch(); + InstMatch(){} + explicit InstMatch(TNode q); InstMatch( InstMatch* m ); - - /** set the match of v to m */ - bool setMatch( EqualityQuery* q, TNode v, TNode m ); - /* This version tell if the variable has been set */ - bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set); - /** fill all unfilled values with m */ - bool add( InstMatch& m ); - /** if compatible, fill all unfilled values with m and return true - return false otherwise */ + /* map from variable to ground terms */ + std::vector d_vals; + /** add match m + * + * This adds the initialized fields of m to this match for each field that is + * not already initialized in this match. + */ + void add(InstMatch& m); + /** merge with match m + * + * This method returns true if the merge was successful, that is, all jointly + * initialized fields of this class and m are equivalent modulo the equalities + * given by q. + */ bool merge( EqualityQuery* q, InstMatch& m ); + /** is this complete, i.e. are all fields non-null? */ + bool isComplete(); + /** is this empty, i.e. are all fields the null node? */ + bool empty(); + /** clear the instantiation, i.e. set all fields to the null node */ + void clear(); /** debug print method */ - void debugPrint( const char* c ); - /** is complete? */ - bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } - /** make complete */ - void makeComplete( Node f, QuantifiersEngine* qe ); - /** make internal representative */ - //void makeInternalRepresentative( QuantifiersEngine* qe ); - /** make representative */ - void makeRepresentative( QuantifiersEngine* qe ); - /** get value */ - Node getValue( Node var ) const; - /** clear */ - void clear(){ d_map.clear(); } - /** is_empty */ - bool empty(){ return d_map.empty(); } + void debugPrint(const char* c); /** to stream */ inline void toStream(std::ostream& out) const { out << "INST_MATCH( "; - for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( it != d_map.begin() ){ out << ", "; } - out << it->first << " -> " << it->second; + bool printed = false; + for( unsigned i=0; i " << d_vals[i]; + printed = true; + } } out << " )"; } - - - //for rewrite rules - - /** apply rewrite */ - void applyRewrite(); - /** erase */ - template - void erase(Iterator begin, Iterator end){ - for(Iterator i = begin; i != end; ++i){ - d_map.erase(*i); - }; - } - void erase(Node node){ d_map.erase(node); } - /** get */ - Node get( TNode var ) { return d_map[var]; } - /** set */ - void set(TNode var, TNode n); - size_t size(){ return d_map.size(); } - /* iterator */ - std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; - std::map< Node, Node >::iterator end(){ return d_map.end(); }; - std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); }; - /* Node used for matching the trigger only for mono-trigger (just for - efficiency because I need only that) */ - Node d_matched; -};/* class InstMatch */ + /** get the i^th term in the instantiation */ + Node get(size_t i) const; + /** set/overwrites the i^th field in the instantiation with n */ + void setValue(size_t i, TNode n); + /** set the i^th term in the instantiation to n + * + * This method returns true if the i^th field was previously uninitialized, + * or is equivalent to n modulo the equalities given by q. + */ + bool set(EqualityQuery* q, size_t i, TNode n); +}; inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { m.toStream(out); return out; } -/** trie for InstMatch objects */ -class InstMatchTrie { -public: - class ImtIndexOrder { - public: - std::vector< int > d_order; - };/* class InstMatchTrie ImtIndexOrder */ -private: - /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ - void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ); - /** exists match */ - bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); -public: - /** the data */ - std::map< Node, InstMatchTrie > d_data; -public: - InstMatchTrie(){} - ~InstMatchTrie(){} -public: - /** return true if m exists in this trie - modEq is if we check modulo equality - modInst is if we return true if m is an instance of a match that exists - */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL ); - /** add match m for quantifier f, take into account equalities if modEq = true, - if imtio is non-null, this is the order to add to trie - return true if successful - */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL ); -};/* class InstMatchTrie */ - - -/** trie for InstMatch objects */ -class CDInstMatchTrie { -public: - class ImtIndexOrder { - public: - std::vector< int > d_order; - };/* class InstMatchTrie ImtIndexOrder */ -private: - /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ - void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ); - /** exists match */ - bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); -public: - /** the data */ - std::map< Node, CDInstMatchTrie* > d_data; - /** is valid */ - context::CDO< bool > d_valid; -public: - CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} - ~CDInstMatchTrie(){} -public: - /** return true if m exists in this trie - modEq is if we check modulo equality - modInst is if we return true if m is an instance of a match that exists - */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL ); - /** add match m for quantifier f, take into account equalities if modEq = true, - if imtio is non-null, this is the order to add to trie - return true if successful - */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL ); -};/* class CDInstMatchTrie */ - -class InstMatchTrieOrdered{ -private: - InstMatchTrie::ImtIndexOrder* d_imtio; - InstMatchTrie d_imt; -public: - InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){} - ~InstMatchTrieOrdered(){} - /** get ordering */ - InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; } - /** get trie */ - InstMatchTrie* getTrie() { return &d_imt; } -public: - /** add match m, return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ - return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio ); - } - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ - return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio ); - } -};/* class InstMatchTrieOrdered */ - }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; @@ -206,4 +102,4 @@ typedef CVC4::theory::inst::InstMatch InstMatch; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */