summaryrefslogtreecommitdiff
path: root/src/theory/theory.h
diff options
context:
space:
mode:
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>2020-09-16 12:45:01 -0500
committerGitHub <noreply@github.com>2020-09-16 12:45:01 -0500
commit2c2f05c96e021006275a2bc70b9ede70b280616d (patch)
treedb702d7b8fbd14dd8003b1f03c02b77c89d2fced /src/theory/theory.h
parent0534ea1bbee9a3a7049580449ab25025a4f92a9a (diff)
Dump commands in internal code using command printing functions. (#5040)
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r--src/theory/theory.h6
1 files changed, 0 insertions, 6 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 77652f874..da651d259 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -32,8 +32,6 @@
#include "expr/node.h"
#include "options/options.h"
#include "options/theory_options.h"
-#include "smt/command.h"
-#include "smt/dump.h"
#include "smt/logic_request.h"
#include "theory/assertion.h"
#include "theory/care_graph.h"
@@ -911,10 +909,6 @@ inline theory::Assertion Theory::get() {
Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
- if(Dump.isOn("state")) {
- Dump("state") << AssertCommand(fact.d_assertion.toExpr());
- }
-
return fact;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback