X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FAST%2Fboolean.cc;h=647f548d352f21e5a98c149ce519b427941099bc;hp=a0048bd50aebfe529dc9361f902af821a0416f59;hb=238830745ba3939323c285b722c9ae512b7baa9b;hpb=87e67ce60ad79d235655d7c74276ba27d1d98632 diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index a0048bd..647f548 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -5,16 +5,18 @@ #include "order.h" #include "predicate.h" +uint64_t Boolean::counter = 0; + Boolean::Boolean(ASTNodeType _type) : ASTNode(_type), polarity(P_UNDEFINED), boolVal(BV_UNDEFINED), - parents() { + parents(), id(counter++) { } BooleanConst::BooleanConst(bool _isTrue) : Boolean(BOOLCONST), - isTrue(_isTrue) { + istrue(_isTrue) { } BooleanVar::BooleanVar(VarType t) : @@ -28,53 +30,59 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : order(_order), first(_first), second(_second) { +} + +void BooleanOrder::updateParents() { order->constraints.push(this); } -BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) : +BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus) : Boolean(PREDICATEOP), predicate(_predicate), encoding(this), inputs(_inputs, _numInputs), undefStatus(_undefinedStatus) { - for (uint i = 0; i < _numInputs; i++) { - _inputs[i]->parents.push(this); - } } -BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) : +BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) : Boolean(LOGICOP), op(_op), + replaced(false), inputs(array, asize) { } +BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) { + bool isnegated = e.isNegated(); + Boolean *b = e->clone(solver, map); + BooleanEdge be = BooleanEdge(b); + return isnegated ? be.negate() : be; +} + Boolean *BooleanConst::clone(CSolver *solver, CloneMap *map) { - if (isTrue) - return solver->getBooleanTrue(); - else - return solver->getBooleanFalse(); + return solver->getBooleanTrue().getRaw(); } Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) { Boolean *b = (Boolean *) map->get(this); if (b != NULL) return b; - Boolean *bvar = solver->getBooleanVar(type); - map->put(this, bvar); - return bvar; + BooleanEdge bvar = solver->getBooleanVar(type); + Boolean *base = bvar.getRaw(); + map->put(this, base); + return base; } Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) { Order *ordercopy = order->clone(solver, map); - return solver->orderConstraint(ordercopy, first, second); + return solver->orderConstraint(ordercopy, first, second).getRaw(); } Boolean *BooleanLogic::clone(CSolver *solver, CloneMap *map) { - Boolean *array[inputs.getSize()]; + BooleanEdge array[inputs.getSize()]; for (uint i = 0; i < inputs.getSize(); i++) { - array[i] = inputs.get(i)->clone(solver, map); + array[i] = cloneEdge(solver, map, inputs.get(i)); } - return solver->applyLogicalOperation(op, array, inputs.getSize()); + return solver->applyLogicalOperation(op, array, inputs.getSize()).getRaw(); } Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) { @@ -83,7 +91,128 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) { array[i] = inputs.get(i)->clone(solver, map); } Predicate *pred = predicate->clone(solver, map); - Boolean *defstatus = (undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL; + BooleanEdge defstatus = undefStatus ? cloneEdge(solver, map, undefStatus) : BooleanEdge(); + + return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw(); +} + +void BooleanPredicate::updateParents() { + for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this); + if (undefStatus) + undefStatus->parents.push(this); +} + +void BooleanLogic::updateParents() { + for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this); +} + +void BooleanVar::serialize(Serializer *serializer) { + if (serializer->isSerialized(this)) + return; + serializer->addObject(this); + serializer->mywrite(&type, sizeof(ASTNodeType)); + BooleanVar *This = this; + serializer->mywrite(&This, sizeof(BooleanVar *)); + serializer->mywrite(&vtype, sizeof(VarType)); +} + +void BooleanVar::print() { + model_print("BooleanVar<%p>\n", this); +} + +void BooleanConst::print() { + model_print("BooleanConst<%p>:%s\n", this, istrue ? "TRUE" : "FALSE"); +} + +void BooleanOrder::serialize(Serializer *serializer) { + if (serializer->isSerialized(this)) + return; + serializer->addObject(this); + order->serialize(serializer); - return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus); + serializer->mywrite(&type, sizeof(ASTNodeType)); + BooleanOrder *This = this; + serializer->mywrite(&This, sizeof(BooleanOrder *)); + serializer->mywrite(&order, sizeof(Order *)); + serializer->mywrite(&first, sizeof(uint64_t)); + serializer->mywrite(&second, sizeof(uint64_t)); } + +void BooleanOrder::print() { + model_print("{BooleanOrder<%p>: First= %lu, Second = %lu on Order:\n", this, first, second); + order->print(); + model_print("}\n"); +} + +void BooleanPredicate::serialize(Serializer *serializer) { + if (serializer->isSerialized(this)) + return; + serializer->addObject(this); + + predicate->serialize(serializer); + uint size = inputs.getSize(); + for (uint i = 0; i < size; i++) { + Element *input = inputs.get(i); + input->serialize(serializer); + } + serializeBooleanEdge(serializer, undefStatus); + + serializer->mywrite(&type, sizeof(ASTNodeType)); + BooleanPredicate *This = this; + serializer->mywrite(&This, sizeof(BooleanPredicate *)); + serializer->mywrite(&predicate, sizeof(Predicate *)); + serializer->mywrite(&size, sizeof(uint)); + for (uint i = 0; i < size; i++) { + Element *input = inputs.get(i); + serializer->mywrite(&input, sizeof(Element *)); + } + Boolean *undefStat = undefStatus != BooleanEdge(NULL) ? undefStatus.getRaw() : NULL; + serializer->mywrite(&undefStat, sizeof(Boolean *)); +} + +void BooleanPredicate::print() { + model_print("{BooleanPredicate<%p>:\n", this); + predicate->print(); + model_print("elements:\n"); + uint size = inputs.getSize(); + for (uint i = 0; i < size; i++) { + Element *input = inputs.get(i); + input->print(); + } + model_print("}\n"); +} + +void BooleanLogic::serialize(Serializer *serializer) { + if (serializer->isSerialized(this)) + return; + serializer->addObject(this); + uint size = inputs.getSize(); + for (uint i = 0; i < size; i++) { + BooleanEdge input = inputs.get(i); + serializeBooleanEdge(serializer, input); + } + serializer->mywrite(&type, sizeof(ASTNodeType)); + BooleanLogic *This = this; + serializer->mywrite(&This, sizeof(BooleanLogic *)); + serializer->mywrite(&op, sizeof(LogicOp)); + serializer->mywrite(&size, sizeof(uint)); + for (uint i = 0; i < size; i++) { + Boolean *input = inputs.get(i).getRaw(); + serializer->mywrite(&input, sizeof(Boolean *)); + } +} + +void BooleanLogic::print() { + model_print("{BooleanLogic<%p>: %s\n", this, + op == SATC_AND ? "AND" : op == SATC_OR ? "OR" : op == SATC_NOT ? "NOT" : + op == SATC_XOR ? "XOR" : op == SATC_IFF ? "IFF" : "IMPLIES"); + uint size = inputs.getSize(); + for (uint i = 0; i < size; i++) { + BooleanEdge input = inputs.get(i); + if (input.isNegated()) + model_print("!"); + input.getBoolean()->print(); + } + model_print("}\n"); +} +