summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r--src/prop/theory_proxy.cpp9
1 files changed, 8 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 5de97d0d8..63a09169f 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -23,9 +23,10 @@
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "proof/cnf_proof.h"
+#include "smt/command.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/lemma_input_channel.h"
#include "smt_util/lemma_output_channel.h"
-#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/statistics_registry.h"
@@ -236,5 +237,11 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
return d_decisionEngine->getPolarity(var);
}
+void TheoryProxy::dumpStatePop() {
+ if(Dump.isOn("state")) {
+ Dump("state") << PopCommand();
+ }
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback