diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-17 15:31:28 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-17 15:31:38 -0500 |
| commit | 66ee6c6472264be842f4e80a7106399d7f51d28a (patch) | |
| tree | 55c6adcdcadc41c7b34d46eea7081d8bdc2eb7a0 /src/theory/quantifiers/rewrite_engine.h | |
| parent | 8936ca3ab2a1b9e3612e08a73542f7a288ee1df8 (diff) | |
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.h')
| -rwxr-xr-x | src/theory/quantifiers/rewrite_engine.h | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h new file mode 100755 index 000000000..5160af602 --- /dev/null +++ b/src/theory/quantifiers/rewrite_engine.h @@ -0,0 +1,51 @@ +/********************* */
+/*! \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;
+ /** explicitly provided patterns */
+ std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
+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 |