add new class

[satune.git] / src / Backend / cnfexpr.cc

diff --git a/src/Backend/cnfexpr.cc b/src/Backend/cnfexpr.cc
index 1aa6cf0abc09d388cb89481b5b5cc822969d7f22..e8af3b829a0cc1d691edcd52e756a808f31046d2 100644 (file)
--- a/src/Backend/cnfexpr.cc
+++ b/src/Backend/cnfexpr.cc
@@ -1,5 +1,6 @@
 #include "cnfexpr.h"
 #include <stdio.h>
+#include "common.h"
 /*
    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -169,6 +170,7 @@ void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
                ourfree(This->singletons.literals);
                ourfree(This->clauses.array);
                This->litSize = expr->litSize;
+               This->singletons.size = expr->singletons.size;
                This->singletons.literals = expr->singletons.literals;
                This->singletons.capacity = expr->singletons.capacity;
                This->clauses.size = expr->clauses.size;
@@ -190,7 +192,7 @@ void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 
 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
        if (expr->litSize == 0) {
-               if (!This->isTrue) {
+               if (!expr->isTrue) {
                        clearCNFExpr(This, false);
                }
                if (destroy) {
@@ -416,7 +418,7 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                                mergeArray[mergeIndex++] = merge;
                        }
                }
-               deleteLitVector(lThis);//Done with this litVector
+               deleteLitVector(lThis); //Done with this litVector
        }
 
        /** Finally do the singleton, singleton pairs */