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 db9bbfe6645c483740172669c586f7a7348623ed..0b832c19ef738201a8e32da3ee2c9e348cf808c7 100644 (file)
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -24,7 +24,7 @@ struct CNFExpr {
 
 typedef struct CNFExpr CNFExpr;
 
-LitVector * allocLitVector();
+LitVector *allocLitVector();
 void initLitVector(LitVector *This);
 void clearLitVector(LitVector *This);
 void freeLitVector(LitVector *This);
@@ -32,20 +32,24 @@ 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);
+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);
-bool alwaysTrueCNF(CNFExpr * This);
-bool alwaysFalseCNF(CNFExpr * This);
-uint getLitSizeCNF(CNFExpr * This);
-void clearCNF(CNFExpr *This, bool isTrue);
-uint getClauseSizeCNF(CNFExpr * This);
+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);