summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.h
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2012-06-08 05:56:08 +0000
committerKshitij Bansal <kshitij@cs.nyu.edu>2012-06-08 05:56:08 +0000
commit8cd22903675724e29249ce089ee77c7c4d3897fb (patch)
tree64ea92a2a0f8721b7e1b15796824f6259567aa75 /src/prop/theory_proxy.h
parent6685546d585212559b97d5722161ad52ff5c4121 (diff)
Merge from decision branch (till r3663)
(no performace or search behavior changes expected)
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r--src/prop/theory_proxy.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 2fac0ab7b..99aab8286 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -119,6 +119,10 @@ public:
bool isDecisionEngineDone();
+ bool isDecisionRelevant(SatVariable var);
+
+ SatValue getDecisionPolarity(SatVariable var);
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback