diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-09 21:56:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-09 21:56:40 -0500 |
commit | 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 (patch) | |
tree | 427223e34ce9bd100ef4443c80b95a9526169363 /src/theory/quantifiers/equality_query.h | |
parent | 3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7 (diff) |
Split term database (#1206)
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
Diffstat (limited to 'src/theory/quantifiers/equality_query.h')
-rw-r--r-- | src/theory/quantifiers/equality_query.h | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h new file mode 100644 index 000000000..c3e0a8c5b --- /dev/null +++ b/src/theory/quantifiers/equality_query.h @@ -0,0 +1,76 @@ +/********************* */ +/*! \file equality_query.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Equality query class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +// TODO : (as part of #1171, #1214) further document and clean this class. +/** equality query object using theory engine */ +class EqualityQueryQuantifiersEngine : public EqualityQuery +{ +private: + /** pointer to theory engine */ + QuantifiersEngine* d_qe; + /** quantifiers equality inference */ + context::CDO< unsigned > d_eqi_counter; + /** internal representatives */ + std::map< TypeNode, std::map< Node, Node > > d_int_rep; + /** rep score */ + std::map< Node, int > d_rep_score; + /** reset count */ + int d_reset_count; + + /** processInferences : will merge equivalence classes in master equality engine, if possible */ + bool processInferences( Theory::Effort e ); + /** node contains */ + Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ); + /** get score */ + int getRepScore( Node n, Node f, int index, TypeNode v_tn ); + /** flatten representatives */ + void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); +public: + EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ); + virtual ~EqualityQueryQuantifiersEngine(); + /** reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "EqualityQueryQE"; } + /** general queries about equality */ + bool hasTerm( Node a ); + Node getRepresentative( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + eq::EqualityEngine* getEngine(); + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); + TNode getCongruentTerm( Node f, std::vector< TNode >& args ); + /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria. + If cbqi is active, this will return a term in the equivalence class of "a" that does + not contain instantiation constants, if such a term exists. + */ + Node getInternalRepresentative( Node a, Node f, int index ); +}; /* EqualityQueryQuantifiersEngine */ + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ |