diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-31 18:35:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-31 18:35:45 +0000 |
commit | ceca24424da629db2e133f7864b0bac03ad44829 (patch) | |
tree | 6b50c8337f6617ee11718cede5fbaf35a21d6a6c /src/prop/sat.h | |
parent | b04d7ee960729bcde8677be3682a2d64789f825b (diff) |
Fixes to Valuation.
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index 88df366e2..f9e135c0d 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -232,8 +232,12 @@ public: void setCnfStream(CnfStream* cnfStream); + /** Call value() during the search.*/ SatLiteralValue value(SatLiteral l); + /** Call value() when the search is done.*/ + SatLiteralValue modelValue(SatLiteral l); + int getLevel() const; void push(); @@ -294,6 +298,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) { } inline SatLiteralValue SatSolver::value(SatLiteral l) { + return d_minisat->value(l); +} + +inline SatLiteralValue SatSolver::modelValue(SatLiteral l) { return d_minisat->modelValue(l); } |