diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-24 18:37:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-24 18:37:22 +0000 |
commit | 1f48835b7252757bb778a93bdac2d62e1dea59bc (patch) | |
tree | 1b2f2cda4091a146a2ddfbfcf137459e712fcc17 /src/theory/rewriterules | |
parent | e2611a54c5479086df0c4a80f56597aae80b5c4e (diff) |
Fix the memout issue seen in recent nightly regressions (was due to a
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/rewriterules')
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_params.h | 2 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_preprocess.h | 28 |
2 files changed, 17 insertions, 13 deletions
diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h index de51215d1..5e7db156b 100644 --- a/src/theory/rewriterules/theory_rewriterules_params.h +++ b/src/theory/rewriterules/theory_rewriterules_params.h @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H #define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h index c90edcf27..3cd540ad0 100644 --- a/src/theory/rewriterules/theory_rewriterules_preprocess.h +++ b/src/theory/rewriterules/theory_rewriterules_preprocess.h @@ -15,9 +15,10 @@ ** **/ +#include "cvc4_private.h" -#ifndef __CVC4__REWRITERULES_H -#define __CVC4__REWRITERULES_H +#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H +#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H #include <vector> #include <ext/hash_set> @@ -31,7 +32,7 @@ namespace CVC4 { namespace theory { namespace rewriterules { -namespace rewriter{ +namespace rewriter { typedef Node TMPNode; typedef std::vector<Node> Subst; @@ -43,7 +44,7 @@ namespace rewriter{ /** match the node and add in Vars the found variables */ virtual Node run(TMPNode node) = 0; virtual bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars) = 0; - }; + };/* struct Step */ struct FinalStep : Step { Node body; @@ -54,7 +55,7 @@ namespace rewriter{ subst.begin(), subst.end()); } - }; + };/* struct FinalStep */ typedef std::hash_map< Node, int, NodeHashFunction > PVars; @@ -106,7 +107,7 @@ namespace rewriter{ return false; } - }; + };/* struct Pattern */ struct Args : Step { @@ -144,7 +145,7 @@ namespace rewriter{ void clear(){ d_matches.clear(); } - }; + };/* struct Args */ class RRPpRewrite : public uf::TheoryUF::PpRewrite { Args d_pattern; @@ -164,13 +165,14 @@ public: return d_pattern.add(pattern,body,pvars,vars); } -}; +};/* class RRPpRewrite */ -} +}/* CVC4::theory::rewriterules::rewriter namespace */ -} -} -} -#endif /* __CVC4__REWRITERULES_H */ +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H */ |