diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-11 06:15:32 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-11 06:15:32 +0000 |
| commit | c7ccddcad95d7b6534a83a873c522b115530a553 (patch) | |
| tree | b62e3239620d0650d6e9d28af8746fbf47f4b19d /src/prop | |
| parent | a7f004fad9947f3a953dbd6d14838f1e04f105eb (diff) | |
Boolean variables were marked as theory literals by mistake. Fixed, should give us back the SAT performance we had before the theory stuff.
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/cnf_stream.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 634ba00d4..a5924a544 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -109,8 +109,9 @@ SatLiteral TseitinCnfStream::handleAtom(const TNode& node) { Assert(!isCached(node), "atom already mapped!"); Debug("cnf") << "handleAtom(" << node << ")" << endl; - - SatLiteral lit = newLiteral(node, true); + + bool theoryLiteral = node.getKind() != kind::VARIABLE; + SatLiteral lit = newLiteral(node, theoryLiteral); switch(node.getKind()) { case TRUE: |