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 e8af3b829a0cc1d691edcd52e756a808f31046d2..3aef9da9262770b2b2e0526ee18ddc991d330ab2 100644 (file)
--- a/src/Backend/cnfexpr.cc
+++ b/src/Backend/cnfexpr.cc
@@ -36,8 +36,6 @@
    C port of CNF SAT Conversion Copyright Brian Demsky 2017.
  */
 
-#define LITCAPACITY 4
-#define MERGESIZE 5
 
 VectorImpl(LitVector, LitVector *, 4)
 
@@ -289,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));