src/csolver.h

   1 #ifndef CSOLVER_H
   2 #define CSOLVER_H
   3 #include "classlist.h"
   4 #include "ops.h"
   5 #include "structs.h"
   6
   7 class CSolver {
   8 public:
   9         CSolver();
  10         ~CSolver();
  11
  12         /** This function creates a set containing the elements passed in the array. */
  13         Set *createSet(VarType type, uint64_t *elements, uint num);
  14
  15         /** This function creates a set from lowrange to highrange (inclusive). */
  16
  17         Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
  18
  19         /** This function creates a mutable set. */
  20
  21         MutableSet *createMutableSet(VarType type);
  22
  23         /** This function adds a new item to a set. */
  24
  25         void addItem(MutableSet *set, uint64_t element);
  26
  27         /** This function adds a new unique item to the set and returns it.
  28             This function cannot be used in conjunction with manually adding
  29             items to the set. */
  30
  31         uint64_t createUniqueItem(MutableSet *set);
  32
  33         /** This function creates an element variable over a set. */
  34
  35         Element *getElementVar(Set *set);
  36
  37         /** This function creates an element constrant. */
  38         Element *getElementConst(VarType type, uint64_t value);
  39
  40         /** This function creates a boolean variable. */
  41
  42         Boolean *getBooleanVar(VarType type);
  43
  44         /** This function creates a function operator. */
  45
  46         Function *createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,
  47                                                                                                                                          OverFlowBehavior overflowbehavior);
  48
  49         /** This function creates a predicate operator. */
  50
  51         Predicate *createPredicateOperator(CompOp op, Set **domain, uint numDomain);
  52
  53         Predicate *createPredicateTable(Table *table, UndefinedBehavior behavior);
  54
  55         /** This function creates an empty instance table.*/
  56
  57         Table *createTable(Set **domains, uint numDomain, Set *range);
  58
  59         Table *createTableForPredicate(Set **domains, uint numDomain);
  60         /** This function adds an input output relation to a table. */
  61
  62         void addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result);
  63
  64         /** This function converts a completed table into a function. */
  65
  66         Function *completeTable(Table *, UndefinedBehavior behavior);
  67
  68         /** This function applies a function to the Elements in its input. */
  69
  70         Element *applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
  71
  72         /** This function applies a predicate to the Elements in its input. */
  73
  74         Boolean *applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus);
  75
  76         Boolean *applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
  77
  78         /** This function applies a logical operation to the Booleans in its input. */
  79
  80         Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
  81
  82         /** This function adds a boolean constraint to the set of constraints
  83             to be satisfied */
  84
  85         void addConstraint(Boolean *constraint);
  86
  87         /** This function instantiates an order of type type over the set set. */
  88         Order *createOrder(OrderType type, Set *set);
  89
  90         /** This function instantiates a boolean on two items in an order. */
  91         Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
  92
  93         /** When everything is done, the client calls this function and then csolver starts to encode*/
  94         int startEncoding();
  95
  96         /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
  97         uint64_t getElementValue(Element *element);
  98
  99         /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
 100         bool getBooleanValue(Boolean *boolean);
 101
 102         HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 103
 104         void setUnSAT() { unsat = true; }
 105
 106         bool isUnSAT() { return unsat; }
 107
 108         Vector<Order *> *getOrders() { return &allOrders;}
 109
 110         Tuner *getTuner() { return tuner; }
 111
 112         HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
 113
 114         SATEncoder *getSATEncoder() {return satEncoder;}
 115
 116         void replaceBooleanWithTrue(Boolean *bexpr);
 117         void replaceBooleanWithFalse(Boolean *bexpr);
 118         void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
 119         CSolver *clone();
 120
 121         MEMALLOC;
 122
 123 private:
 124         void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
 125         void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
 126         void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
 127         void handleANDTrue(BooleanLogic *bexpr, Boolean *child);
 128         void handleORFalse(BooleanLogic *bexpr, Boolean *child);
 129
 130         /** This is a vector of constraints that must be satisfied. */
 131         HashSetBoolean constraints;
 132
 133         /** This is a vector of all boolean structs that we have allocated. */
 134         Vector<Boolean *> allBooleans;
 135
 136         /** This is a vector of all set structs that we have allocated. */
 137         Vector<Set *> allSets;
 138
 139         /** This is a vector of all element structs that we have allocated. */
 140         Vector<Element *> allElements;
 141
 142         /** This is a vector of all predicate structs that we have allocated. */
 143         Vector<Predicate *> allPredicates;
 144
 145         /** This is a vector of all table structs that we have allocated. */
 146         Vector<Table *> allTables;
 147
 148         /** This is a vector of all order structs that we have allocated. */
 149         Vector<Order *> allOrders;
 150
 151         /** This is a vector of all function structs that we have allocated. */
 152         Vector<Function *> allFunctions;
 153
 154         SATEncoder *satEncoder;
 155         bool unsat;
 156         Tuner *tuner;
 157 };
 158 #endif