diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-14 22:58:53 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-14 22:58:53 +0000 |
| commit | 8a672c060d2b3946c542c82bd6ca8f89892216ee (patch) | |
| tree | 6a79291dfb1fa21c2394af6d11a4f1b478a63b12 /src/theory/quantifiers/macros.h | |
| parent | 73bf2532d70177ee768c508ef971b969994cea2c (diff) | |
replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros
Diffstat (limited to 'src/theory/quantifiers/macros.h')
| -rwxr-xr-x | src/theory/quantifiers/macros.h | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h new file mode 100755 index 000000000..d93070481 --- /dev/null +++ b/src/theory/quantifiers/macros.h @@ -0,0 +1,51 @@ +/********************* */
+/*! \file macros.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Pre-process step for detecting quantifier macro definitions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_MACROS_H
+#define __CVC4__QUANTIFIERS_MACROS_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifierMacros{
+private:
+ void process( Node n, bool pol, std::vector< Node >& args, Node f );
+ bool containsOp( Node n, Node op );
+ bool isMacroKind( Node n, bool pol );
+ //map from operators to macro definition ( basis, definition )
+ std::map< Node, std::pair< Node, Node > > d_macro_defs;
+private:
+ Node simplify( Node n );
+public:
+ QuantifierMacros(){}
+ ~QuantifierMacros(){}
+
+ void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+};
+
+}
+}
+}
+
+#endif
|