Found bug... Don't update parent's list until we know we aren't going to be freed

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

diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index fcb75bdb247f91b4a659be8371867bedb37a3c49..0b832c19ef738201a8e32da3ee2c9e348cf808c7 100644 (file)
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -11,7 +11,7 @@ struct LitVector {
        uint capacity;
        Literal *literals;
 };
-typedef CNFClause CNFClause;
+typedef struct LitVector LitVector;
 
 VectorDef(LitVector, LitVector *)
 
@@ -22,11 +22,37 @@ struct CNFExpr {
        LitVector singletons;
 };
 
-typedef CNFExpr CNFExpr;
+typedef struct CNFExpr CNFExpr;
+
+LitVector *allocLitVector();
+void initLitVector(LitVector *This);
+void clearLitVector(LitVector *This);
+void freeLitVector(LitVector *This);
+LitVector *cloneLitVector(LitVector *orig);
+void deleteLitVector(LitVector *This);
+void addLiteralLitVector(LitVector *This, Literal l);
+Literal getLiteralLitVector(LitVector *This, uint index);
+void setLiteralLitVector(LitVector *This, uint index, Literal l);
+LitVector *mergeLitVectorLiteral(LitVector *This, Literal l);
+LitVector *mergeLitVectors(LitVector *This, LitVector *expr);
+
+static inline uint getSizeLitVector(LitVector *This) {return This->size;}
+static inline void setSizeLitVector(LitVector *This, uint size) {This->size = size;}
+
+CNFExpr *allocCNFExprBool(bool isTrue);
+CNFExpr *allocCNFExprLiteral(Literal l);
+void deleteCNFExpr(CNFExpr *This);
+void clearCNFExpr(CNFExpr *This, bool isTrue);
+void printCNFExpr(CNFExpr *This);
+
+void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
+static inline bool alwaysTrueCNF(CNFExpr *This) {return (This->litSize == 0) && This->isTrue;}
+static inline bool alwaysFalseCNF(CNFExpr *This) {return (This->litSize == 0) && !This->isTrue;}
+static inline uint getLitSizeCNF(CNFExpr *This) {return This->litSize;}
+static inline uint getClauseSizeCNF(CNFExpr *This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
+void conjoinCNFLit(CNFExpr *This, Literal l);
+void disjoinCNFLit(CNFExpr *This, Literal l);
+void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
+void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
 
-bool alwaysTrueCNF(CNFExpr * This);
-bool alwaysFalseCNF(CNFExpr * This);
-uint getLitSizeCNF(CNFExpr * This);
-void clearCNF(CNFExpr *This, bool isTrue);
-uint getClauseSizeCNF(CNFExpr * This);
 #endif