#ifndef CSOLVER_H
#define CSOLVER_H
-#include "classlist.h"
+#include "classes.h"
#include "ops.h"
-#include "structs.h"
+#include "corestructs.h"
+#include "asthash.h"
class CSolver {
public:
/** This function creates an element constrant. */
Element *getElementConst(VarType type, uint64_t value);
+ Boolean *getBooleanTrue();
+
+ Boolean *getBooleanFalse();
+
/** This function creates a boolean variable. */
Boolean *getBooleanVar(VarType type);
Vector<Order *> *getOrders() { return &allOrders;}
Tuner *getTuner() { return tuner; }
-
- HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+
+ SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
SATEncoder *getSATEncoder() {return satEncoder;}
void replaceBooleanWithTrue(Boolean *bexpr);
void replaceBooleanWithFalse(Boolean *bexpr);
void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+ CSolver *clone();
+ void autoTune(uint budget);
-
- MEMALLOC;
+ void setTuner(Tuner * _tuner) { tuner = _tuner; }
+ long long getElapsedTime() { return elapsedTime; }
+ long long getEncodeTime();
+ long long getSolveTime();
+
+ CMEMALLOC;
private:
void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;
+ Boolean * boolTrue;
+ Boolean * boolFalse;
+
+ /** These two tables are used for deduplicating entries. */
+ BooleanMatchMap boolMap;
+ ElementMatchMap elemMap;
+
SATEncoder *satEncoder;
bool unsat;
Tuner *tuner;
+
+ long long elapsedTime;
};
#endif