diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
commit | 51d642e075466bc6655cae9752350f6760b2bd0f (patch) | |
tree | 9c4e752e2d7ced10854c82555fa148b8e73e6d78 /src/theory/quantifiers/quant_util.h | |
parent | 4a8045f5f57c1e71dc4a2cdadc02ca09114c70af (diff) |
Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 116211bfb..d7e220b2e 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -110,38 +110,6 @@ public: virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ -class QuantLtePartialInst { -private: - // was this module invoked - bool d_wasInvoked; - //representatives per type - std::map< TypeNode, std::vector< Node > > d_reps; - // should we instantiate quantifier - std::map< Node, bool > d_do_inst; - // have we instantiated quantifier - std::map< Node, bool > d_inst; - std::map< Node, std::vector< Node > > d_vars; - /** pointer to quant engine */ - QuantifiersEngine * d_qe; - /** list of relevant quantifiers asserted in the current context */ - context::CDList<Node> d_lte_asserts; - /** reset */ - void reset(); - /** get instantiations */ - void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index ); - /** get eligible inst variables */ - void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); -public: - QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ); - /** add quantifier */ - bool addQuantifier( Node q ); - /** get instantiations */ - void getInstantiations( std::vector< Node >& lemmas ); - /** was invoked */ - bool wasInvoked() { return d_wasInvoked; } -}; - } } |