Rename some functions and cleanup

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

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index 0799ffa4fc36f78c251d6698558bfe6c523057e8..c2a5bc9f9d3769c8592419e7069c358ab1f6e2db 100644 (file)
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -1,8 +1,45 @@
 #include "cnfexpr.h"
+#include <stdio.h>
+/* 
+V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
+Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.  If
+you download or use the software, send email to Pete Manolios
+(pete@ccs.neu.edu) with your name, contact information, and a short
+note describing what you want to use BAT for.  For any reuse or
+distribution, you must make clear to others the license terms of this
+work.
+
+Contact Pete Manolios if you want any of these conditions waived.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+*/
+
+/* 
+C port of CNF SAT Conversion Copyright Brian Demsky 2017. 
+*/
 
 #define LITCAPACITY 4
 #define MERGESIZE 5
 
+VectorImpl(LitVector, LitVector *, 4)
+
 static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
 
 LitVector * allocLitVector() {
@@ -62,17 +99,17 @@ void addLiteralLitVector(LitVector *This, Literal l) {
                                This->size = 0; //either true or false now depending on whether this is a conj or disj
                        return;
                }
-               if ((++This->size) >= This->capacity) {
-                       This->capacity <<= 1;
-                       This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
-               }
-               
-               if (vec_size < MERGESIZE) {
-                       memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
-                       This->literals[i]=l;
-               } else {
-                       This->literals[vec_size]=l;
-               }
+       }
+       if ((++This->size) >= This->capacity) {
+               This->capacity <<= 1;
+               This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
+       }
+       
+       if (vec_size < MERGESIZE) {
+               memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
+               This->literals[i]=l;
+       } else {
+               This->literals[vec_size]=l;
        }
 }
 
@@ -80,7 +117,7 @@ CNFExpr * allocCNFExprBool(bool isTrue) {
        CNFExpr *This=ourmalloc(sizeof(CNFExpr));
        This->litSize=0;
        This->isTrue=isTrue;
-       allocInlineVectorLitVector(&This->clauses, 2);
+       initVectorLitVector(&This->clauses, 2);
        initLitVector(&This->singletons);
        return This;
 }
@@ -89,7 +126,7 @@ CNFExpr * allocCNFExprLiteral(Literal l) {
        CNFExpr *This=ourmalloc(sizeof(CNFExpr));
        This->litSize=1;
        This->isTrue=false;
-       allocInlineVectorLitVector(&This->clauses, 2);
+       initVectorLitVector(&This->clauses, 2);
        initLitVector(&This->singletons);
        addLiteralLitVector(&This->singletons, l);
        return This;
@@ -122,7 +159,7 @@ void conjoinCNFLit(CNFExpr *This, Literal l) {
        addLiteralLitVector(&This->singletons, l);
        uint newsize=getSizeLitVector(&This->singletons);
        if (newsize==0)
-               clearCNF(This, false); //We found a conflict
+               clearCNFExpr(This, false); //We found a conflict
        else
                This->litSize+=getSizeLitVector(&This->singletons);
 }
@@ -154,7 +191,7 @@ void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
        if (expr->litSize==0) {
                if (!This->isTrue) {
-                       clearCNF(This, false);
+                       clearCNFExpr(This, false);
                }
                if (destroy) {
                        deleteCNFExpr(expr);
@@ -176,7 +213,7 @@ void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                addLiteralLitVector(&This->singletons, l);
                if (getSizeLitVector(&This->singletons)==0) {
                        //Found conflict...
-                       clearCNF(This, false);
+                       clearCNFExpr(This, false);
                        if (destroy) {
                                deleteCNFExpr(expr);
                        }
@@ -306,7 +343,7 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
        /** Handle the special cases */
        if (expr->litSize == 0) {
                if (expr->isTrue) {
-                       clearCNF(This, true);
+                       clearCNFExpr(This, true);
                }
                if (destroy) {
                        deleteCNFExpr(expr);
@@ -408,5 +445,21 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                deleteCNFExpr(expr);
 }
 
-
-
+void printCNFExpr(CNFExpr *This) {
+       for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+               if (i!=0)
+                       printf(" ^ ");
+               Literal l=getLiteralLitVector(&This->singletons,i);
+               printf ("%d",l);
+       }
+       for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+               LitVector *lv=getVectorLitVector(&This->clauses,i);
+               printf(" ^ (");
+               for(uint j=0;j<getSizeLitVector(lv);j++) {
+                       if (j!=0)
+                               printf(" v ");
+                       printf("%d", getLiteralLitVector(lv, j));
+               }
+               printf(")");
+       }
+}