diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 23:20:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 23:20:09 -0500 |
commit | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (patch) | |
tree | b5c785e9a5e16d430f45b2a40f78e40247111233 /src/theory/quantifiers/quant_util.h | |
parent | 4b580ea3876055f701b13e67e0e4e78abbe47674 (diff) |
(Move-only) Split quant util (#1306)
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 88 |
1 files changed, 1 insertions, 87 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index ad6ab509d..95cd7e5e4 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -316,41 +316,6 @@ public: static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c); }; -/** QuantRelevance -* This class is used for implementing SinE-style heuristics (e.g. see Hoder et -* al CADE 2011) -* This is enabled by the option --relevant-triggers. -*/ -class QuantRelevance : public QuantifiersUtil -{ -private: - /** for computing relevance */ - bool d_computeRel; - /** map from quantifiers to symbols they contain */ - std::map< Node, std::vector< Node > > d_syms; - /** map from symbols to quantifiers */ - std::map< Node, std::vector< Node > > d_syms_quants; - /** relevance for quantifiers and symbols */ - std::map< Node, int > d_relevance; - /** compute symbols */ - void computeSymbols( Node n, std::vector< Node >& syms ); -public: - QuantRelevance( bool cr ) : d_computeRel( cr ){} - ~QuantRelevance(){} - virtual bool reset(Theory::Effort e) override { return true; } - /** Called for new quantifiers after ownership of quantified formulas are - * finalized */ - virtual void registerQuantifier(Node q) override; - /** Identify this module (for debugging, dynamic configuration, etc..) */ - virtual std::string identify() const override { return "QuantRelevance"; } - /** set relevance */ - void setRelevance( Node s, int r ); - /** get relevance */ - int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } - /** get number of quantifiers for symbol s */ - int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } -}; - class QuantPhaseReq { private: @@ -400,58 +365,7 @@ public: virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ -class QuantEPR -{ -private: - void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ); - /** non-epr */ - std::map< TypeNode, bool > d_non_epr; - /** axioms for epr */ - std::map< TypeNode, Node > d_epr_axiom; -public: - QuantEPR(){} - virtual ~QuantEPR(){} - /** constants per type */ - std::map< TypeNode, std::vector< Node > > d_consts; - /* reset */ - //bool reset( Theory::Effort e ) {} - /** identify */ - //std::string identify() const { return "QuantEPR"; } - /** register assertion */ - void registerAssertion( Node assertion ); - /** finish init */ - void finishInit(); - /** is EPR */ - bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); } - /** is EPR constant */ - bool isEPRConstant( TypeNode tn, Node k ); - /** add EPR constant */ - void addEPRConstant( TypeNode tn, Node k ); - /** get EPR axiom */ - Node mkEPRAxiom( TypeNode tn ); - /** has EPR axiom */ - bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); } -}; - -class TermRecBuild { -private: - std::vector< Node > d_term; - std::vector< std::vector< Node > > d_children; - std::vector< Kind > d_kind; - std::vector< bool > d_has_op; - std::vector< unsigned > d_pos; - void addTerm( Node n ); -public: - TermRecBuild(){} - void init( Node n ); - void push( unsigned p ); - void pop(); - void replaceChild( unsigned i, Node n ); - Node getChild( unsigned i ); - Node build( unsigned p=0 ); -}; - } } -#endif +#endif /* __CVC4__THEORY__QUANT_UTIL_H */ |