#include "csolver.h"
#include "element.h"
#include "order.h"
+#include "predicate.h"
Boolean::Boolean(ASTNodeType _type) :
ASTNode(_type),
inputs(array, asize) {
}
-BooleanPredicate::~BooleanPredicate() {
+Boolean * BooleanVar::clone(CSolver *solver, CloneMap *map) {
+ if (map->boolean.contains(this)) {
+ return map->boolean.get(this);
+ } else {
+ Boolean * bvar=solver->getBooleanVar(type);
+ map->boolean.put(this, bvar);
+ return bvar;
+ }
+}
+
+Boolean * BooleanOrder::clone(CSolver * solver, CloneMap *map) {
+ Order * ordercopy=order->clone(map);
+ return solver->orderConstraint(ordercopy, first, second);
+}
+
+Boolean * BooleanLogic::clone(CSolver * solver, CloneMap *map) {
+ Boolean * array[inputs.getSize()];
+ for(uint i=0;i<inputs.getSize();i++) {
+ array[i]=inputs.get(i)->clone(solver, map);
+ }
+ return solver->applyLogicalOperation(op, array, inputs.getSize());
+}
+
+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(map);
+ Boolean * defstatus=(undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL;
+
+ return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus);
}
public:
Boolean(ASTNodeType _type);
virtual ~Boolean() {}
+ virtual Boolean * clone(CSolver * solver, CloneMap *map);
Polarity polarity;
BooleanValue boolVal;
Vector<Boolean *> parents;
class BooleanVar : public Boolean {
public:
BooleanVar(VarType t);
+ Boolean * clone(CSolver * solver, CloneMap *map);
+
VarType vtype;
Edge var;
MEMALLOC;
class BooleanOrder : public Boolean {
public:
BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
+ Boolean * clone(CSolver * solver, CloneMap *map);
+
Order *order;
uint64_t first;
uint64_t second;
class BooleanPredicate : public Boolean {
public:
BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus);
- ~BooleanPredicate();
+ Boolean * clone(CSolver * solver, CloneMap *map);
+
Predicate *predicate;
FunctionEncoding encoding;
Array<Element *> inputs;
class BooleanLogic : public Boolean {
public:
BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize);
+ Boolean * clone(CSolver * solver, CloneMap *map);
+
LogicOp op;
Array<Boolean *> inputs;
MEMALLOC;
#include "constraint.h"
#include "function.h"
#include "table.h"
+#include "csolver.h"
Element::Element(ASTNodeType _type) :
ASTNode(_type),
GETELEMENTPARENTS(array[i])->push(this);
}
-ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) {
- uint64_t array[] = {value};
- set = new Set(_type, array, 1);
+ElementConst::ElementConst(uint64_t _value, VarType _type, Set * _set) :
+ Element(ELEMCONST),
+ set(_set),
+ value(_value) {
}
Set *getElementSet(Element *This) {
return NULL;
}
-ElementFunction::~ElementFunction() {
+Element * ElementConst::clone(CSolver *solver, CloneMap * map) {
+ return solver->getElementConst(type, value);
}
-
-ElementConst::~ElementConst() {
- delete set;
+
+Element * ElementSet::clone(CSolver *solver, CloneMap * map) {
+ Element * e = map->element.get(this);
+ if (e != NULL)
+ return e;
+ e = solver->getElementVar(set->clone(solver, map));
+ map->element.put(e, e);
+ return e;
}
-Element::~Element() {
+Element * ElementFunction::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);
+ }
+ Element * e = solver->applyFunction(function->clone(solver, map), array, inputs.getSize(), overflowstatus->clone(solver, map));
+ return e;
}
class Element : public ASTNode {
public:
Element(ASTNodeType type);
- virtual ~Element();
+ virtual ~Element() {}
Vector<ASTNode *> parents;
ElementEncoding encoding;
+ virtual Element * clone(CSolver * solver, CloneMap * map);
MEMALLOC;
};
class ElementConst : public Element {
public:
- ElementConst(uint64_t value, VarType type);
- ~ElementConst();
+ ElementConst(uint64_t value, VarType type, Set *_set);
Set *set;
uint64_t value;
+ Element * clone(CSolver * solver, CloneMap * map);
MEMALLOC;
};
public:
ElementSet(Set *s);
Set *set;
+ Element * clone(CSolver * solver, CloneMap * map);
MEMALLOC;
};
class ElementFunction : public Element {
public:
ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
- ~ElementFunction();
Function *function;
Array<Element *> inputs;
Boolean *overflowstatus;
FunctionEncoding functionencoding;
+ Element * clone(CSolver * solver, CloneMap * map);
MEMALLOC;
};
public:
Function(FunctionType _type) : type(_type) {}
FunctionType type;
- MEMALLOC;
virtual ~Function() {}
+ virtual Function * clone(CSolver * solver, CloneMap *map);
+ MEMALLOC;
};
class FunctionOperator : public Function {
FunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range, OverFlowBehavior overflowbehavior);
uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
bool isInRangeFunction(uint64_t val);
+ Function * clone(CSolver * solver, CloneMap *map);
MEMALLOC;
};
Table *table;
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
+ Function * clone(CSolver * solver, CloneMap *map);
MEMALLOC;
};
#include "mutableset.h"
+#include "csolver.h"
MutableSet::MutableSet(VarType t) : Set(t) {
}
void MutableSet::addElementMSet(uint64_t element) {
members->push(element);
}
+
+Set * MutableSet::clone(CSolver * solver, CloneMap *map) {
+ Set * s=map->set.get(this);
+ if (s != NULL)
+ return s;
+ s=solver->createMutableSet(type);
+ for(uint i=0; i<members->getSize();i++) {
+ solver->addItem((MutableSet *) s, members->get(i));
+ }
+ map->set.put(this, s);
+ return s;
+}
public:
MutableSet(VarType t);
void addElementMSet(uint64_t element);
+ Set * clone(CSolver * solver, CloneMap *map);
MEMALLOC;
};
#endif
HashTableOrderPair *orderPairTable;
HashSetOrderElement *elementTable;
OrderGraph *graph;
+ Order * clone(CloneMap *map);
Vector<BooleanOrder *> constraints;
OrderEncoding order;
void initializeOrderHashTable();
public:
Predicate(PredicateType _type) : type(_type) {}
virtual ~Predicate() {}
+ virtual Predicate * clone(CloneMap *map);
PredicateType type;
MEMALLOC;
};
public:
PredicateOperator(CompOp op, Set **domain, uint numDomain);
bool evalPredicateOperator(uint64_t *inputs);
+ Predicate * clone(CloneMap *map);
CompOp op;
Array<Set *> domains;
MEMALLOC;
class PredicateTable : public Predicate {
public:
PredicateTable(Table *table, UndefinedBehavior undefBehavior);
+ Predicate * clone(CloneMap *map);
Table *table;
UndefinedBehavior undefinedbehavior;
MEMALLOC;
#include "set.h"
#include <stddef.h>
+#include "csolver.h"
Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
members = new Vector<uint64_t>();
if (!isRange)
delete members;
}
+
+Set * Set::clone(CSolver * solver, CloneMap *map) {
+ Set * s=map->set.get(this);
+ if (s != NULL)
+ return s;
+ if (isRange) {
+ s=solver->createRangeSet(type, low, high);
+ } else {
+ s=solver->createSet(type, members->expose(), members->getSize());
+ }
+ map->set.put(this, s);
+ return s;
+}
Set(VarType t);
Set(VarType t, uint64_t *elements, uint num);
Set(VarType t, uint64_t lowrange, uint64_t highrange);
- ~Set();
+ virtual ~Set();
bool exists(uint64_t element);
uint getSize();
uint64_t getElement(uint index);
-
+ virtual Set * clone(CSolver * solver, CloneMap *map);
+
VarType type;
bool isRange;
uint64_t low;//also used to count unique items
typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
typedef HashTable<OrderNode *, HashSetOrderNode *, uintptr_t, 4> HashTableNodeToNodeSet;
typedef HashTable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashTableOrderPair;
+typedef HashTable<Order *, Order *, uintptr_t, 4> OrderMap;
+typedef HashTable<Boolean *, Boolean *, uintptr_t, 4> BooleanMap;
+typedef HashTable<Element *, Element *, uintptr_t, 4> ElementMap;
+typedef HashTable<Set *, Set *, uintptr_t, 4> SetMap;
+
+typedef struct CloneMap {
+ OrderMap order;
+ BooleanMap boolean;
+ ElementMap element;
+ SetMap set;
+} CloneMap;
typedef HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
typedef HSIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HSIteratorOrderEdge;
typedef HSIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HSIteratorOrderNode;
+
#endif
delete tuner;
}
+CSolver * CSolver::clone() {
+ CSolver * copy=new CSolver();
+ CloneMap map;
+ HSIteratorBoolean * it=getConstraints();
+ while(it->hasNext()) {
+ Boolean *b=it->next();
+ b->clone(copy, &map);
+ }
+ delete it;
+ return copy;
+}
+
Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
Set *set = new Set(type, elements, numelements);
allSets.push(set);
}
Element *CSolver::getElementConst(VarType type, uint64_t value) {
- Element *element = new ElementConst(value, type);
+ uint64_t array[] = {value};
+ Set * set = new Set(type, array, 1);
+ allSets.push(set);
+ Element *element = new ElementConst(value, type, set);
allElements.push(element);
return element;
}
void replaceBooleanWithTrue(Boolean *bexpr);
void replaceBooleanWithFalse(Boolean *bexpr);
void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
-
+ CSolver * clone();
MEMALLOC;