Tons of bugs

[satune.git] / src / AST / boolean.cc

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 7949cdc16dc6cb3335ecd0f3de2e7ed4589c4c2d..4ca9c404522deb2e324fc617580e8243d2159b37 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -9,8 +9,12 @@ Boolean::Boolean(ASTNodeType _type) :
        ASTNode(_type),
        polarity(P_UNDEFINED),
        boolVal(BV_UNDEFINED),
-       parents(),
-       idNumber(0) {
+       parents() {
+}
+
+BooleanConst::BooleanConst(bool _isTrue) :
+       Boolean(BOOLCONST),
+       istrue(_isTrue) {
 }
 
 BooleanVar::BooleanVar(VarType t) :
@@ -27,7 +31,7 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
        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),
@@ -38,32 +42,48 @@ BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uin
        }
 }
 
-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) {
+       for (uint i = 0; i < asize; i++) {
+               array[i]->parents.push(this);
+       }
+}
+
+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) {
+       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) {
@@ -72,7 +92,7 @@ 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);
+       return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw();
 }