X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FAST%2Fboolean.cc;h=4ca9c404522deb2e324fc617580e8243d2159b37;hp=62f6bff6fc7c9e4c133aa10ce2f0abb04480761e;hb=3b44d67aa34198bde59d8b346ea316ba7fb6d73d;hpb=cd2da835188cf0bbe3502c61dc66cc803f26cbfa

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 62f6bff..4ca9c40 100644
--- 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,23 +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) {
-	solver->allBooleans.push(this);
+	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();
 }