diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-29 16:08:45 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-29 16:08:45 -0400 |
commit | da9eec6aa0fc0f6c29f2c3fdb08bd45ba9c27808 (patch) | |
tree | dca1b2fb1d1c213a94d5b2902aed4a24895aae3f /src/theory/quantifiers/rewrite_engine.h | |
parent | bc3db83a6856016c9c838fbabdd29f962aa60769 (diff) |
Fix numerous compiler warnings on various platforms
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.h')
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.h | 108 |
1 files changed, 54 insertions, 54 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 6783b20d0..2d9d751c2 100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -1,54 +1,54 @@ -/********************* */
-/*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013 New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
-**/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__REWRITE_ENGINE_H
-#define __CVC4__REWRITE_ENGINE_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
-
-namespace CVC4 {
-namespace theory {
-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::map< Node, Node > d_rr_guard;
- Node d_true;
- /** explicitly provided patterns */
- std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
- double getPriority( Node f );
-private:
- int checkRewriteRule( Node f );
-public:
- RewriteEngine( context::Context* c, QuantifiersEngine* qe );
-
- void check( Theory::Effort e );
- void registerQuantifier( Node f );
- void assertNode( Node n );
-};
-
-}
-}
-}
-
-#endif
\ No newline at end of file +/********************* */ +/*! \file bounded_integers.h +** \verbatim +** Original author: Andrew Reynolds +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief This class manages integer bounds for quantifiers +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__REWRITE_ENGINE_H +#define __CVC4__REWRITE_ENGINE_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/trigger.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { +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::map< Node, Node > d_rr_guard; + Node d_true; + /** explicitly provided patterns */ + std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; + double getPriority( Node f ); +private: + int checkRewriteRule( Node f ); +public: + RewriteEngine( context::Context* c, QuantifiersEngine* qe ); + + void check( Theory::Effort e ); + void registerQuantifier( Node f ); + void assertNode( Node n ); +}; + +} +} +} + +#endif |