summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules/theory_rewriterules.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules/theory_rewriterules.h')
-rw-r--r--src/theory/rewriterules/theory_rewriterules.h4
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback