#include "function.h"
#include "table.h"
#include "csolver.h"
+#include "boolean.h"
Element::Element(ASTNodeType _type) :
ASTNode(_type),
#include "mymemory.h"
#include "structs.h"
#include "astnode.h"
+#include "corestructs.h"
#include "functionencoding.h"
#include "elementencoding.h"
-#include "boolean.h"
class Element : public ASTNode {
public:
virtual ~Element() {}
Vector<ASTNode *> parents;
ElementEncoding encoding;
+ inline ElementEncoding *getElementEncoding(){ return &encoding; }
virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
virtual void serialize(Serializer* serializer) =0;
virtual void updateParents() {}
Set * getRange();
void updateParents();
Function * getFunction() {return function;}
+ inline FunctionEncoding *getElementFunctionEncoding() {return &functionencoding;}
CMEMALLOC;
private:
Function *function;
};
-static inline ElementEncoding *getElementEncoding(Element *e) {
- return &e->encoding;
-}
-static inline FunctionEncoding *getElementFunctionEncoding(ElementFunction *func) {
- return &func->functionencoding;
-}
#endif
#include "set.h"
#include "csolver.h"
#include "tunable.h"
+#include "boolean.h"
EncodingGraph::EncodingGraph(CSolver * _solver) :
solver(_solver) {
typedef int Literal;
-struct Edge;
-typedef struct Edge Edge;
-
struct Node;
typedef struct Node Node;
#include "set.h"
Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
- switch (getElementEncoding(elem)->type) {
+ switch (elem->getElementEncoding()->type) {
case ONEHOT:
return getElementValueOneHotConstraint(elem, value);
case UNARY:
Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) {
ASTNodeType type = elem->type;
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
- ElementEncoding *elemEnc = getElementEncoding(elem);
+ ElementEncoding *elemEnc = elem->getElementEncoding();
for (uint i = 0; i < elemEnc->encArraySize; i++) {
if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) {
ASTNodeType type = elem->type;
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
- ElementEncoding *elemEnc = getElementEncoding(elem);
+ ElementEncoding *elemEnc = elem->getElementEncoding();
for (uint i = 0; i < elemEnc->encArraySize; i++) {
if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
ASTNodeType type = elem->type;
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
- ElementEncoding *elemEnc = getElementEncoding(elem);
+ ElementEncoding *elemEnc = elem->getElementEncoding();
for (uint i = 0; i < elemEnc->encArraySize; i++) {
if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
if (elemEnc->numVars == 0)
Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) {
ASTNodeType type = element->type;
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
- ElementEncoding *elemEnc = getElementEncoding(element);
+ ElementEncoding *elemEnc = element->getElementEncoding();
if (elemEnc->low <= elemEnc->high) {
if (value < elemEnc->low || value > elemEnc->high)
return E_False;
}
void SATEncoder::generateElementEncoding(Element *element) {
- ElementEncoding *encoding = getElementEncoding(element);
+ ElementEncoding *encoding = element->getElementEncoding();
ASSERT(encoding->type != ELEM_UNASSIGNED);
if (encoding->variables != NULL)
return;
void SATEncoder::encodeElementSATEncoder(Element *element) {
/* Check to see if we have already encoded this element. */
- if (getElementEncoding(element)->variables != NULL)
+ if (element->getElementEncoding()->variables != NULL)
return;
/* Need to encode. */
}
void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
- switch (getElementFunctionEncoding(function)->type) {
+ switch (function->getElementFunctionEncoding()->type) {
case ENUMERATEIMPLICATIONS:
encodeEnumTableElemFunctionSATEncoder(function);
break;
encodeElementSATEncoder(elem0);
Element *elem1 = constraint->inputs.get(1);
encodeElementSATEncoder(elem1);
- ElementEncoding *ee0 = getElementEncoding(elem0);
- ElementEncoding *ee1 = getElementEncoding(elem1);
+ ElementEncoding *ee0 = elem0->getElementEncoding();
+ ElementEncoding *ee1 = elem1->getElementEncoding();
ASSERT(ee0->numVars == ee1->numVars);
uint numVars = ee0->numVars;
switch (predicate->getOp()) {
#include "array.h"
#include "corestructs.h"
+
unsigned int table_entry_hash_function(TableEntry *This);
bool table_entry_equals(TableEntry *key1, TableEntry *key2);
unsigned int order_node_hash_function(OrderNode *This);
#ifndef ELEMENTENCODING_H
#define ELEMENTENCODING_H
#include "classlist.h"
-#include "naiveencoder.h"
-#include "constraint.h"
+#include "common.h"
class ElementEncoding {
public:
}
void naiveEncodingElement(Element *This) {
- ElementEncoding *encoding = getElementEncoding(This);
+ ElementEncoding *encoding = This->getElementEncoding();
if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
encoding->setElementEncodingType(BINARYINDEX);
encoding->encodingArrayInitialization();
Element *element = function->inputs.get(i);
naiveEncodingElement(element);
}
- FunctionEncoding *encoding = getElementFunctionEncoding(function);
+ FunctionEncoding *encoding = function->getElementFunctionEncoding();
if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
- getElementFunctionEncoding(function)->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
+ function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
}
}
}
uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
- ElementEncoding *elemEnc = getElementEncoding(element);
+ ElementEncoding *elemEnc = element->getElementEncoding();
if (elemEnc->numVars == 0)//case when the set has only one item
return element->getRange()->getElement(0);
switch (elemEnc->type) {
#ifndef CLASSLIST_H
#define CLASSLIST_H
-#include "mymemory.h"
#include <inttypes.h>
#include "classes.h"
-#include "AST/astnode.h"
+#include "astnode.h"
class BooleanOrder;
class EncodingNode;
class EncodingEdge;
+class ElementEncoding;
+class FunctionEncoding;
+
struct IncrementalSolver;
typedef struct IncrementalSolver IncrementalSolver;
struct TableEntry;
typedef struct TableEntry TableEntry;
typedef int TunableParam;
-
+struct Edge;
+typedef struct Edge Edge;
#endif
#include "preprocess.h"
#include "serializer.h"
#include "deserializer.h"
+#include "naiveencoder.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),