Add useful functions

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index a0048bd50aebfe529dc9361f902af821a0416f59..7c3771095a2ca448eab0ab4e84dea940be384da7 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -14,7 +14,7 @@ Boolean::Boolean(ASTNodeType _type) :
 
 BooleanConst::BooleanConst(bool _isTrue) :
        Boolean(BOOLCONST),
-       isTrue(_isTrue) {
+       istrue(_isTrue) {
 }
 
 BooleanVar::BooleanVar(VarType t) :
@@ -49,7 +49,7 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a
 }
 
 Boolean *BooleanConst::clone(CSolver *solver, CloneMap *map) {
-       if (isTrue)
+       if (istrue)
                return solver->getBooleanTrue();
        else
                return solver->getBooleanFalse();

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 7dd0bb3ed2c2d38e014781bce9f1f476c75e1332..afcf512499aa40561b580bce56dc544c0af721cf 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -13,7 +13,9 @@ class Boolean : public ASTNode {
 public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
-       virtual Boolean *clone(CSolver *solver, CloneMap *map) { ASSERT(0); return NULL; }
+       virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
+       virtual bool isTrue() {return false;}
+       virtual bool isFalse() {return false;}
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;
@@ -25,7 +27,9 @@ class BooleanConst : public Boolean {
  public:
        BooleanConst(bool isTrue);
        Boolean *clone(CSolver *solver, CloneMap *map);
-       bool isTrue;
+       bool isTrue() {return istrue;}
+       bool isFalse() {return !istrue;}
+       bool istrue;
        CMEMALLOC;
 };
 

diff --git a/src/csolver.cc b/src/csolver.cc
index 5ee5157d31f29246f3d6dddd0c7058947d217e6f..310d535489f365cb6fddf73b4f6ccae8d99ff0ef 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -221,16 +221,14 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) {
                        return ((BooleanLogic *) array[0])->inputs.get(0);
                } else if (array[0]->type == BOOLCONST) {
-                       bool isTrue = ((BooleanConst *) array[0])->isTrue;
-                       return isTrue ? boolFalse : boolTrue;
+                       return array[0]->isTrue() ? boolFalse : boolTrue;
                }
                break;
        }
        case SATC_XOR: {
                for(uint i=0;i<2;i++) {
                        if (array[i]->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) array[i])->isTrue;
-                               if (isTrue) {
+                               if (array[i]->isTrue()) {
                                        newarray[0]=array[1-i];
                                        return applyLogicalOperation(SATC_NOT, newarray, 1);
                                } else
@@ -244,8 +242,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                        if (b->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) b)->isTrue;
-                               if (isTrue)
+                               if (b->isTrue())
                                        return b;
                                else
                                        continue;
@@ -279,8 +276,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                        if (b->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) b)->isTrue;
-                               if (isTrue)
+                               if (b->isTrue())
                                        continue;
                                else
                                        return b;
@@ -297,16 +293,14 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
        }
        case SATC_IMPLIES: {
                if (array[0]->type == BOOLCONST) {
-                       BooleanConst *b=(BooleanConst *) array[0];
-                       if (b->isTrue) {
+                       if (array[0]->isTrue()) {
                                return array[1];
                        } else {
                                return boolTrue;
                        }
                } else if (array[1]->type == BOOLCONST) {
-                       BooleanConst *b=(BooleanConst *) array[0];
-                       if (b->isTrue) {
-                               return b;
+                       if (array[1]->isTrue()) {
+                               return array[1];
                        } else {
                                return applyLogicalOperation(SATC_NOT, array, 1);
                        }