diff options
author | lianah <lianahady@gmail.com> | 2013-03-27 14:05:49 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-27 14:05:49 -0400 |
commit | cab30c6cac6921efc19fcc11b0cf5afa7770cb5b (patch) | |
tree | 1aeddc30df1721fc69e66e9db445d4adaf49a670 /src/theory/bv/bitblaster.cpp | |
parent | ec4a985f9b27740d0e84202bb7bcd5f5bdc8fb83 (diff) |
fixed some model stuff
Diffstat (limited to 'src/theory/bv/bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 6da3b8efc..9a52a05a5 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -428,9 +428,18 @@ bool Bitblaster::hasValue(TNode a) { } return true; } - +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * + * @return + */ Node Bitblaster::getVarValue(TNode a) { - Assert (d_termCache.find(a) != d_termCache.end()); + if (d_termCache.find(a) == d_termCache.end()) { + return Node(); + } Bits bits = d_termCache[a]; Integer value(0); for (int i = bits.size() -1; i >= 0; --i) { @@ -455,6 +464,10 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { Node const_value = getVarValue(var); + if(const_value == Node()) { + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " << var << " " << const_value << "))\n"; |