From 9122ad62d12284ab934a3cda1c736889de01e519 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 30 Aug 2017 13:21:24 -0700 Subject: [PATCH] Add support for true and false and normalizing them away --- src/AST/boolean.cc | 12 +++++ src/AST/boolean.h | 8 +++ src/AST/ops.h | 2 +- src/csolver.cc | 119 ++++++++++++++++++++++++++++++++++++++++++++- src/csolver.h | 7 +++ 5 files changed, 146 insertions(+), 2 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 6f2f475..a0048bd 100644 --- 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 81ce9b4..894e6cb 100644 --- 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 c9de82d..1f9c197 100644 --- 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 06ecf78..39585a9 100644 --- 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;itype == 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;itype == 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 63ee0fd..52f1c98 100644 --- 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 allFunctions; + Boolean * boolTrue; + Boolean * boolFalse; + /** These two tables are used for deduplicating entries. */ BooleanMatchMap boolMap; ElementMatchMap elemMap; -- 2.34.1