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.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5227d32f0..0eaf61055 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -380,7 +380,7 @@ public:
return d_theoryOut.d_explanationNode;
}
- inline Node getExplanation(TNode node){
+ inline Node getExplanation(TNode node) {
d_theoryOut.d_explanationNode = Node::null();
theory::Theory* theory =
node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
@@ -388,6 +388,8 @@ public:
return d_theoryOut.d_explanationNode;
}
+ Node getValue(TNode node);
+
private:
class Statistics {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback