Tons of bugs

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

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index b349c9a5468a67f35c20335a5a585516ce5fe779..4ca9c404522deb2e324fc617580e8243d2159b37 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -3,41 +3,96 @@
 #include "csolver.h"
 #include "element.h"
 #include "order.h"
+#include "predicate.h"
 
-Boolean::Boolean(ASTNodeType _type) : ASTNode(_type), polarity(P_UNDEFINED), boolVal(BV_UNDEFINED) {
-       initDefVectorBoolean(GETBOOLEANPARENTS(this));  
+Boolean::Boolean(ASTNodeType _type) :
+       ASTNode(_type),
+       polarity(P_UNDEFINED),
+       boolVal(BV_UNDEFINED),
+       parents() {
 }
 
-BooleanVar::BooleanVar(VarType t) : Boolean(BOOLEANVAR), vtype(t), var(E_NULL) {
+BooleanConst::BooleanConst(bool _isTrue) :
+       Boolean(BOOLCONST),
+       istrue(_isTrue) {
 }
 
-BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : Boolean(ORDERCONST), order(_order), first(_first), second(_second) {
-       pushVectorBooleanOrder(&order->constraints, this);
+BooleanVar::BooleanVar(VarType t) :
+       Boolean(BOOLEANVAR),
+       vtype(t),
+       var(E_NULL) {
 }
 
-BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) : Boolean(PREDICATEOP), predicate(_predicate), undefStatus(_undefinedStatus) {
-       initArrayInitElement(&inputs, _inputs, _numInputs);
+BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
+       Boolean(ORDERCONST),
+       order(_order),
+       first(_first),
+       second(_second) {
+       order->constraints.push(this);
+}
 
+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++) {
-               pushVectorASTNode(GETELEMENTPARENTS(_inputs[i]), this);
+               _inputs[i]->parents.push(this);
+       }
+}
+
+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);
        }
-       initPredicateEncoding(&encoding, this);
 }
 
-BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) : Boolean(LOGICOP), op(_op) {
-       initArrayInitBoolean(&inputs, array, asize);
-       pushVectorBoolean(solver->allBooleans, (Boolean *) 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::~Boolean() {
-       deleteVectorArrayBoolean(GETBOOLEANPARENTS(this));
+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;
 }
 
-BooleanPredicate::~BooleanPredicate() {
-       deleteInlineArrayElement(&inputs );
-       deleteFunctionEncoding(&encoding);
+Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) {
+       Order *ordercopy = order->clone(solver, map);
+       return solver->orderConstraint(ordercopy, first, second).getRaw();
 }
 
-BooleanLogic::~BooleanLogic() {
-       deleteInlineArrayBoolean(&inputs);
+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();
+}
+
+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();
 }