}
case ELEMCONST: {
ElementConst * ec=(ElementConst *) e;
- return ((uint)(uintptr_t) ec->set) ^ ((uint) ec->value);
+ return ((uint) ec->value);
}
default:
ASSERT(0);
case ELEMCONST: {
ElementConst * ec1=(ElementConst *) e1;
ElementConst * ec2=(ElementConst *) e2;
- return (ec1->set == ec2->set) &&
- (ec1->value == ec2->value);
+ return (ec1->value == ec2->value);
}
default:
ASSERT(0);
#ifndef ASTHASH_H
#define ASTHASH_H
#include "classlist.h"
+#include "hashtable.h"
uint hashBoolean(Boolean * boolean);
bool compareBoolean(Boolean *b1, Boolean *b2);
uint hashElement(Element *element);
bool compareElement(Element *e1, Element *e2);
+typedef HashTable<Boolean *, Boolean *, uintptr_t, 4, hashBoolean, compareBoolean> BooleanMatchMap;
+
+typedef HashTable<Element *, Element *, uintptr_t, 4, hashElement, compareElement> ElementMatchMap;
+
#endif
Element *CSolver::getElementConst(VarType type, uint64_t value) {
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;
+ Element *e = elemMap.get(element);
+ if (e == NULL) {
+ allSets.push(set);
+ allElements.push(element);
+ elemMap.put(element, element);
+ return element;
+ } else {
+ delete set;
+ delete element;
+ return e;
+ }
}
Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
- allElements.push(element);
- return element;
+ Element *e = elemMap.get(element);
+ if (e == NULL) {
+ allElements.push(element);
+ elemMap.put(element, element);
+ return element;
+ } else {
+ delete element;
+ return e;
+ }
}
Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
- allBooleans.push(boolean);
- return boolean;
+ Boolean * b = boolMap.get(boolean);
+ if (b == NULL) {
+ boolMap.put(boolean, boolean);
+ allBooleans.push(boolean);
+ return boolean;
+ } else {
+ delete boolean;
+ return b;
+ }
}
Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
Boolean *boolean = new BooleanLogic(this, op, array, asize);
- allBooleans.push(boolean);
- return boolean;
+ Boolean *b = boolMap.get(boolean);
+ if (b == NULL) {
+ boolMap.put(boolean, boolean);
+ allBooleans.push(boolean);
+ return boolean;
+ } else {
+ delete boolean;
+ return b;
+ }
}
Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
#include "classlist.h"
#include "ops.h"
#include "structs.h"
+#include "asthash.h"
class CSolver {
public:
MEMALLOC;
private:
- void assignID(Boolean * b);
- void assignID(Element * e);
void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;
+ /** These two tables are used for deduplicating entries. */
+ BooleanMatchMap boolMap;
+ ElementMatchMap elemMap;
+
SATEncoder *satEncoder;
bool unsat;
Tuner *tuner;
- uint booleanID;
- uint elementID;
long long elapsedTime;
};