edits

diff --git a/src/AST/rewriter.c b/src/AST/rewriter.c
index e432cf181b4f8515b8ec8699ef8714eb5a394e4f..7bbbf6d8513035c3667902f06daa51c5b9f88b1d 100644 (file)
--- 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 8d66d7ea4dfb291065269e17b223c72f247aba35..2295e7bd923b487fd86f50f65f258d6bcd730535 100644 (file)
--- 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 607bca675aa5900084f598afda2d5c54179eae66..e225d0890c7b5df4511821a4f2d522ac99cd8fa8 100644 (file)
--- 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;