From 30db23fc8961ebf904e2f6f580c914451d278ed0 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 30 Aug 2017 19:01:06 -0700
Subject: [PATCH] Add useful functions

---
 src/AST/boolean.cc |  4 ++--
 src/AST/boolean.h  |  8 ++++++--
 src/csolver.cc     | 20 +++++++-------------
 3 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index a0048bd..7c37710 100644
--- 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 7dd0bb3..afcf512 100644
--- 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 5ee5157..310d535 100644
--- 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);
 			}
-- 
2.34.1