From c66adaedd084f9b68455ed50614130d4cb506458 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Thu, 17 Aug 2017 22:07:12 -0700
Subject: [PATCH] edits

---
 src/AST/rewriter.c | 15 +++++++++++++++
 src/csolver.c      |  1 +
 src/csolver.h      |  2 ++
 3 files changed, 18 insertions(+)

diff --git a/src/AST/rewriter.c b/src/AST/rewriter.c
index e432cf1..7bbbf6d 100644
--- a/src/AST/rewriter.c
+++ b/src/AST/rewriter.c
@@ -1,7 +1,12 @@
 #include "rewriter.h"
 #include "boolean.h"
+#include "csolver.h"
 
 void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) {
+	if (containsHashSetBoolean(This->constraints, bexpr)) {
+		removeHashSetBoolean(This->constraints, bexpr);
+	}
+
 	uint size = getSizeVectorBoolean(&bexpr->parents);
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = getVectorBoolean(&bexpr->parents, i);
@@ -27,6 +32,11 @@ void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) {
 }
 
 void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) {
+	if (containsHashSetBoolean(This->constraints, oldb)) {
+		removeHashSetBoolean(This->constraints, oldb);
+		addHashSetBoolean(This->constraints, newb);
+	}
+
 	uint size = getSizeVectorBoolean(&oldb->parents);
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = getVectorBoolean(&oldb->parents, i);
@@ -124,6 +134,11 @@ void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
 }
 
 void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr) {
+	if (containsHashSetBoolean(This->constraints, bexpr)) {
+		This->unsat=true;
+		removeHashSetBoolean(This->constraints, bexpr);
+	}
+	
 	uint size = getSizeVectorBoolean(&bexpr->parents);
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = getVectorBoolean(&bexpr->parents, i);
diff --git a/src/csolver.c b/src/csolver.c
index 8d66d7e..2295e7b 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -12,6 +12,7 @@
 
 CSolver *allocCSolver() {
 	CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
+	This->unsat = false;
 	This->constraints = allocDefHashSetBoolean();
 	This->allBooleans = allocDefVectorBoolean();
 	This->allSets = allocDefVectorSet();
diff --git a/src/csolver.h b/src/csolver.h
index 607bca6..e225d08 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -6,6 +6,8 @@
 
 struct CSolver {
 	SATEncoder *satEncoder;
+	bool unsat;
+
 	/** This is a vector of constraints that must be satisfied. */
 	HashSetBoolean *constraints;
 
-- 
2.34.1