summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules/theory_rewriterules.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules/theory_rewriterules.h')
-rw-r--r--src/theory/rewriterules/theory_rewriterules.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index e47fd2fd4..d1c3eecf3 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -30,6 +30,7 @@
#include "theory/inst_match_impl.h"
#include "util/stats.h"
#include "theory/rewriterules/theory_rewriterules_preprocess.h"
+#include "theory/model.h"
namespace CVC4 {
namespace theory {
@@ -182,6 +183,7 @@ private:
inside check */
typedef std::vector< RuleInst* > QRuleInsts;
QRuleInsts d_ruleinsts_to_add;
+
public:
/** true and false for predicate */
Node d_true;
@@ -199,6 +201,7 @@ private:
/** Usual function for theories */
void check(Theory::Effort e);
Node explain(TNode n);
+ void collectModelInfo( TheoryModel* m );
void notifyEq(TNode lhs, TNode rhs);
std::string identify() const {
return "THEORY_REWRITERULES";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback