diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-12 14:23:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-12 14:23:31 -0500 |
commit | 75d70649e2d72d6d6bb46f47cf96ee523b718cb9 (patch) | |
tree | f413238a6a8ee90d9c47327bd0a0de18906af809 /src/theory/quantifiers/rewrite_engine.h | |
parent | fcd3d91281891bda5d5f4fe60ebb2d282de439c6 (diff) |
Give rewrite engine pointer to conflict-based instantiation module (#3174)
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.h')
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 717f4009b..5832d2817 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -18,8 +18,9 @@ #ifndef CVC4__REWRITE_ENGINE_H #define CVC4__REWRITE_ENGINE_H -#include "context/context.h" -#include "context/context_mm.h" +#include <map> +#include <vector> + #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" @@ -30,9 +31,6 @@ namespace quantifiers { class RewriteEngine : public QuantifiersModule { - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; - typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; std::vector< Node > d_rr_quant; std::vector< Node > d_priority_order; std::map< Node, Node > d_rr; @@ -45,10 +43,14 @@ class RewriteEngine : public QuantifiersModule bool d_needsSort; std::map< Node, std::map< Node, Node > > d_inst_const_node; Node getInstConstNode( Node n, Node q ); -private: + + private: int checkRewriteRule( Node f, Theory::Effort e ); -public: - RewriteEngine( context::Context* c, QuantifiersEngine* qe ); + + public: + RewriteEngine(context::Context* c, + QuantifiersEngine* qe, + QuantConflictFind* qcf); bool needsCheck(Theory::Effort e) override; void check(Theory::Effort e, QEffort quant_e) override; @@ -57,6 +59,14 @@ public: bool checkCompleteFor(Node q) override; /** Identify this module */ std::string identify() const override { return "RewriteEngine"; } + + private: + /** + * A pointer to the quantifiers conflict find module of the quantifiers + * engine. This is the module that computes instantiations for rewrite rule + * quantifiers. + */ + QuantConflictFind* d_qcf; }; } |