Adding checks to avoid further processing on UNSAT Problems

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

diff --git a/src/Backend/cnfexpr.cc b/src/Backend/cnfexpr.cc
index b04044ad914fef1b31ac4264bc7faedab9bed8ff..3aef9da9262770b2b2e0526ee18ddc991d330ab2 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.
@@ -35,8 +36,6 @@
    C port of CNF SAT Conversion Copyright Brian Demsky 2017.
  */
 
-#define LITCAPACITY 4
-#define MERGESIZE 5
 
 VectorImpl(LitVector, LitVector *, 4)
 
@@ -288,7 +287,7 @@ void disjoinCNFLit(CNFExpr *This, Literal l) {
        This->litSize = litSize;
 }
 
-#define MERGETHRESHOLD 2
+
 LitVector *mergeLitVectors(LitVector *This, LitVector *expr) {
        uint maxsize = This->size + expr->size + MERGETHRESHOLD;
        LitVector *merged = (LitVector *)ourmalloc(sizeof(LitVector));
@@ -417,7 +416,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 */