Tons of bugs

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

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 6ec11935080b208c4202238ed614109266a6c2cc..4ca9c404522deb2e324fc617580e8243d2159b37 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -3,6 +3,7 @@
 #include "csolver.h"
 #include "element.h"
 #include "order.h"
+#include "predicate.h"
 
 Boolean::Boolean(ASTNodeType _type) :
        ASTNode(_type),
@@ -11,6 +12,11 @@ Boolean::Boolean(ASTNodeType _type) :
        parents() {
 }
 
+BooleanConst::BooleanConst(bool _isTrue) :
+       Boolean(BOOLCONST),
+       istrue(_isTrue) {
+}
+
 BooleanVar::BooleanVar(VarType t) :
        Boolean(BOOLEANVAR),
        vtype(t),
@@ -25,22 +31,68 @@ 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),
        inputs(_inputs, _numInputs),
        undefStatus(_undefinedStatus) {
        for (uint i = 0; i < _numInputs; i++) {
-               GETELEMENTPARENTS(_inputs[i])->push(this);
+               _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) {
+       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;
+       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).getRaw();
+}
+
+Boolean *BooleanLogic::clone(CSolver *solver, CloneMap *map) {
+       BooleanEdge array[inputs.getSize()];
+       for (uint i = 0; i < inputs.getSize(); i++) {
+               array[i] = cloneEdge(solver, map, inputs.get(i));
+       }
+       return solver->applyLogicalOperation(op, array, inputs.getSize()).getRaw();
 }
 
-BooleanPredicate::~BooleanPredicate() {
+Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
+       Element *array[inputs.getSize()];
+       for (uint i = 0; i < inputs.getSize(); i++) {
+               array[i] = inputs.get(i)->clone(solver, map);
+       }
+       Predicate *pred = predicate->clone(solver, map);
+       BooleanEdge defstatus = undefStatus ? cloneEdge(solver, map, undefStatus) : BooleanEdge();
+
+       return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw();
 }