summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/rewrite_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.h')
-rwxr-xr-xsrc/theory/quantifiers/rewrite_engine.h13
1 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 424530696..ef3337e53 100755
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -18,19 +18,17 @@
#ifndef __CVC4__REWRITE_ENGINE_H
#define __CVC4__REWRITE_ENGINE_H
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
+#include "context/cdchunk_list.h"
#include "context/context.h"
#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
+#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-class QuantInfo;
-
class RewriteEngine : public QuantifiersModule
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
@@ -57,7 +55,8 @@ public:
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
void registerQuantifier( Node f );
- void assertNode( Node n );
+ void assertNode( Node n );
+ bool checkCompleteFor( Node q );
/** Identify this module */
std::string identify() const { return "RewriteEngine"; }
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback