summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/rewrite_engine.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-07-29 16:08:45 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-07-29 16:08:45 -0400
commitda9eec6aa0fc0f6c29f2c3fdb08bd45ba9c27808 (patch)
treedca1b2fb1d1c213a94d5b2902aed4a24895aae3f /src/theory/quantifiers/rewrite_engine.h
parentbc3db83a6856016c9c838fbabdd29f962aa60769 (diff)
Fix numerous compiler warnings on various platforms
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.h')
-rwxr-xr-xsrc/theory/quantifiers/rewrite_engine.h108
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback