#ifndef CSOLVER_H
#define CSOLVER_H
-#include "classlist.h"
+#include "classes.h"
#include "ops.h"
-#include "structs.h"
+#include "corestructs.h"
#include "asthash.h"
+#include "solver_interface.h"
class CSolver {
public:
Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
+ Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
+
/** This function creates a mutable set. */
MutableSet *createMutableSet(VarType type);
/** 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);
Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
+ /** This function applies a logical operation to the Booleans in its input. */
+
+ Boolean *applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2);
+
+ /** This function applies a logical operation to the Booleans in its input. */
+
+ Boolean *applyLogicalOperation(LogicOp op, Boolean *arg);
+
/** This function adds a boolean constraint to the set of constraints
to be satisfied */
Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
/** When everything is done, the client calls this function and then csolver starts to encode*/
- int startEncoding();
+ int solve();
/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
uint64_t getElementValue(Element *element);
HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
+ bool isTrue(Boolean *b);
+ bool isFalse(Boolean *b);
+
void setUnSAT() { unsat = true; }
bool isUnSAT() { return unsat; }
Vector<Order *> *getOrders() { return &allOrders;}
Tuner *getTuner() { return tuner; }
+ Transformer* getTransformer() {return transformer;}
- HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+ SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
SATEncoder *getSATEncoder() {return satEncoder;}
CSolver *clone();
void autoTune(uint budget);
+ void setTransformer(Transformer * _transformer) { transformer = _transformer; }
void setTuner(Tuner * _tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
long long getSolveTime();
- MEMALLOC;
+ CMEMALLOC;
private:
void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
void handleORFalse(BooleanLogic *bexpr, Boolean *child);
/** This is a vector of constraints that must be satisfied. */
- HashSetBoolean constraints;
+ HashsetBoolean constraints;
/** This is a vector of all boolean structs that we have allocated. */
Vector<Boolean *> allBooleans;
/** 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;
-
+ Transformer* transformer;
long long elapsedTime;
};
#endif