summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h11
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5c73da1f6..2871d5559 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -309,8 +309,10 @@ class TheoryEngine {
}
struct SharedLiteral {
- /** The node/theory pair for the assertion */
- /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */
+ /**
+ * The node/theory pair for the assertion. THEORY_LAST indicates this is a SAT
+ * literal and should be sent to the SAT solver
+ */
NodeTheoryPair toAssert;
/** This is the node that we will use to explain it */
Node toExplain;
@@ -319,7 +321,7 @@ class TheoryEngine {
: toAssert(assertion, receivingTheory),
toExplain(original)
{ }
- };/* struct SharedLiteral */
+ };
/**
* Map from nodes to theories.
@@ -728,6 +730,9 @@ private:
/** Visitor for collecting shared terms */
SharedTermsVisitor d_sharedTermsVisitor;
+ /** Prints the assertions to the debug stream */
+ void printAssertions(const char* tag);
+
};/* class TheoryEngine */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback