diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-28 09:51:33 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-28 09:51:44 -0600 |
commit | d3822db24e15e255766866a47e6ffa0d8d91911b (patch) | |
tree | 221298973f410f4305f74cd6041b6a017aaa3075 /src/theory/rewriterules/theory_rewriterules.h | |
parent | 587bc5c82e2921a72cec58dc2ec69e3e0ed71866 (diff) |
More optimizations of quantifier instantiation data structures.
Diffstat (limited to 'src/theory/rewriterules/theory_rewriterules.h')
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index ea9eb4769..30e6f9709 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -81,7 +81,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; ~RewriteRule(); bool noGuard()const throw () { return guards.size() == 0; }; - bool inCache(TheoryRewriteRules & re, InstMatch & im)const; + bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const; void toStream(std::ostream& out) const; @@ -249,7 +249,7 @@ private: void addRewriteRule(const Node r); void computeMatchBody ( const RewriteRule * r, size_t start = 0); void addMatchRuleTrigger(const RewriteRule* r, - InstMatch & im, bool delay = true); + rrinst::InstMatch & im, bool delay = true); Node normalizeConjunction(NodeBuilder<> & conjunction); |