Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 6f2f4753bf2009bee5b31c6564710704750bdd7d..a0048bd50aebfe529dc9361f902af821a0416f59 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -12,6 +12,11 @@ Boolean::Boolean(ASTNodeType _type) :
        parents() {
 }
 
+BooleanConst::BooleanConst(bool _isTrue) :
+       Boolean(BOOLCONST),
+       isTrue(_isTrue) {
+}
+
 BooleanVar::BooleanVar(VarType t) :
        Boolean(BOOLEANVAR),
        vtype(t),
@@ -43,6 +48,13 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a
        inputs(array, asize) {
 }
 
+Boolean *BooleanConst::clone(CSolver *solver, CloneMap *map) {
+       if (isTrue)
+               return solver->getBooleanTrue();
+       else
+               return solver->getBooleanFalse();
+}
+
 Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
        Boolean *b = (Boolean *) map->get(this);
        if (b != NULL)

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 81ce9b41495be0612d2bd378e8a922c733c9d292..894e6cb071eee91e50ea839b98655b3641713a20 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -20,6 +20,14 @@ public:
        MEMALLOC;
 };
 
+class BooleanConst : public Boolean {
+ public:
+       BooleanConst(bool isTrue);
+       Boolean *clone(CSolver *solver, CloneMap *map);
+       bool isTrue;
+       MEMALLOC;
+};
+
 class BooleanVar : public Boolean {
 public:
        BooleanVar(VarType t);

diff --git a/src/AST/ops.h b/src/AST/ops.h
index c9de82de78db1aaabb70b48d50c90a4c668d2922..1f9c19761ba86539f847c48cc7d25fe813c4f0b5 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -35,7 +35,7 @@ typedef enum FunctionType FunctionType;
 enum PredicateType {TABLEPRED, OPERATORPRED};
 typedef enum PredicateType PredicateType;
 
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
+enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
 typedef enum ASTNodeType ASTNodeType;
 
 enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};

diff --git a/src/csolver.cc b/src/csolver.cc
index db42f316afaff7d19da8dbe610f822df5c53f84f..343754c48914cc18ae4c99fe80fba176c0446573 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -15,6 +15,8 @@
 #include "autotuner.h"
 
 CSolver::CSolver() :
+       boolTrue(new BooleanConst(true)),
+       boolFalse(new BooleanConst(false)),
        unsat(false),
        tuner(NULL),
        elapsedTime(0)
@@ -60,6 +62,8 @@ CSolver::~CSolver() {
                delete allFunctions.get(i);
        }
 
+       delete boolTrue;
+       delete boolFalse;
        delete satEncoder;
 }
 
@@ -183,6 +187,14 @@ Boolean *CSolver::getBooleanVar(VarType type) {
        return boolean;
 }
 
+Boolean *CSolver::getBooleanTrue() {
+       return boolTrue;
+}
+
+Boolean *CSolver::getBooleanFalse() {
+       return boolFalse;
+}
+
 Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
        return applyPredicateTable(predicate, inputs, numInputs, NULL);
 }
@@ -201,6 +213,106 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
+       Boolean * newarray[asize];
+       switch(op) {
+       case L_NOT: {
+               if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==L_NOT) {
+                       return ((BooleanLogic *) array[0])->inputs.get(0);
+               } else if (array[0]->type == BOOLCONST) {
+                       bool isTrue = ((BooleanConst *) array[0])->isTrue;
+                       return isTrue ? boolFalse : boolTrue;
+               }
+               break;
+       }
+       case L_XOR: {
+               for(uint i=0;i<2;i++) {
+                       if (array[i]->type == BOOLCONST) {
+                               bool isTrue = ((BooleanConst *) array[i])->isTrue;
+                               if (isTrue) {
+                                       newarray[0]=array[1-i];
+                                       return applyLogicalOperation(L_NOT, newarray, 1);
+                               } else
+                                       return array[1-i];
+                       }
+               }
+               break;
+       }
+       case L_OR: {
+               uint newindex=0;
+               for(uint i=0;i<asize;i++) {
+                       Boolean *b=array[i];
+                       if (b->type == BOOLCONST) {
+                               bool isTrue = ((BooleanConst *) b)->isTrue;
+                               if (isTrue)
+                                       return b;
+                               else
+                                       continue;
+                       } else
+                               newarray[newindex++]=b;
+               }
+               if (newindex==1)
+                       return newarray[0];
+               else if (newindex == 2) {
+                       bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == L_NOT;
+                       bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == L_NOT;
+
+                       if (isNot0 != isNot1) {
+                               if (isNot0) {
+                                       newarray[0] = ((BooleanLogic *) newarray[0])->inputs.get(0);
+                               } else {
+                                       Boolean *tmp =  ((BooleanLogic *) array[1])->inputs.get(0);
+                                       array[1] = array[0];
+                                       array[0] = tmp;
+                               }
+                               return applyLogicalOperation(L_IMPLIES, newarray, 2);
+                       }
+               } else {
+                       array = newarray;
+                       asize = newindex;
+               }
+               break;
+       }
+       case L_AND: {
+               uint newindex=0;
+               for(uint i=0;i<asize;i++) {
+                       Boolean *b=array[i];
+                       if (b->type == BOOLCONST) {
+                               bool isTrue = ((BooleanConst *) b)->isTrue;
+                               if (isTrue)
+                                       continue;
+                               else
+                                       return b;
+                       } else
+                               newarray[newindex++]=b;
+               }
+               if(newindex==1) {
+                       return newarray[0];
+               } else {
+                       array = newarray;
+                       asize = newindex;
+               }
+               break;
+       }
+       case L_IMPLIES: {
+               if (array[0]->type == BOOLCONST) {
+                       BooleanConst *b=(BooleanConst *) array[0];
+                       if (b->isTrue) {
+                               return array[1];
+                       } else {
+                               return boolTrue;
+                       }
+               } else if (array[1]->type == BOOLCONST) {
+                       BooleanConst *b=(BooleanConst *) array[0];
+                       if (b->isTrue) {
+                               return b;
+                       } else {
+                               return applyLogicalOperation(L_NOT, array, 1);
+                       }
+               }
+               break;
+       }
+       }
+       
        Boolean *boolean = new BooleanLogic(this, op, array, asize);
        Boolean *b = boolMap.get(boolean);
        if (b == NULL) {
@@ -220,7 +332,12 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second)
 }
 
 void CSolver::addConstraint(Boolean *constraint) {
-       constraints.add(constraint);
+       if (constraint == boolTrue)
+               return;
+       else if (constraint == boolFalse)
+               setUnSAT();
+       else
+               constraints.add(constraint);
 }
 
 Order *CSolver::createOrder(OrderType type, Set *set) {

diff --git a/src/csolver.h b/src/csolver.h
index 63ee0fdf057e84b155467f0f66a27105c1ba0813..52f1c98eb13a1d2ea2ede74a2c075622715c42b4 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -38,6 +38,10 @@ public:
        /** This function creates an element constrant. */
        Element *getElementConst(VarType type, uint64_t value);
 
+       Boolean *getBooleanTrue();
+
+       Boolean *getBooleanFalse();
+       
        /** This function creates a boolean variable. */
 
        Boolean *getBooleanVar(VarType type);
@@ -158,6 +162,9 @@ private:
        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;
 
+       Boolean * boolTrue;
+       Boolean * boolFalse;
+       
        /** These two tables are used for deduplicating entries. */
        BooleanMatchMap boolMap;
        ElementMatchMap elemMap;