--- /dev/null
+((nil . ((indent-tabs-mode . t))))
\ No newline at end of file
MKDIR_P = mkdir -p
OBJ_DIR = bin
-CPP_SOURCES := constraint.cc inc_solver.cc set.cc
+CPP_SOURCES := constraint.cc inc_solver.cc set.cc mutableset.cc element.cc function.cc order.cc table.cc predicate.cc
OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
class Constraint;
class IncrementalSolver;
+class Set;
+class MutableSet;
+class Element;
+class Function;
+class Predicate;
+class Table;
+class Order;
typedef unsigned int uint;
+typedef uint64_t VarType;
#endif
}
andarray[andi++]=new Constraint(OR, ori, orarray);
- value=value+(1<<(__builtin_ctz(value))); //flip the last one
+ value=value+(1<<(__builtin_ctz(value))); //flip the last one
}
}
--- /dev/null
+#ifndef CSOLVER_H
+#define CSOLVER_H
+#include "classlist.h"
+#include "ops.h"
+
+class CSolver {
+ Set * createSet(Type type, uint64_t ** elements);
+ Set * createSet(Type type, uint64_t lowrange, uint64_t highrange);
+ MutableSet * createMutableSet(Type type);
+
+ void addItem(MutableSet * set, uint64_t element);
+ int64_t createUniqueItem(MutableSet * set);
+
+ Element * getElementVar(Set * set);
+ Constraint * getBooleanVar();
+
+ Function * createFunctionOperator(enum ArithOp op, Set ** domain, Set * range, enum OverFlowBehavior overflowbehavior, Constraint * overflowstatus);
+ Function * createFunctionOperator(enum ArithOp op); //Does Not Overflow
+ Predicate * createPredicateOperator(enum CompOp op, Set ** domain);
+
+ Table * createTable(Set **domains, Set * range);
+ void addTableEntry(Element ** inputs, Element *result);
+ Function * completeTable(struct Table *);
+
+ Element * applyFunction(Function * function, Element ** array);
+ Constraint * applyPredicate(Predicate * predicate, Element ** inputs);
+ Constraint * applyLogicalOperation(enum LogicOp op, Constraint ** array);
+
+ void addConstraint(Constraint * constraint);
+
+ Order * createOrder(enum OrderType type, Set * set);
+ Constraint * orderedConstraint(Order * order, uint64_t first, uint64_t second);
+};
+#endif
--- /dev/null
+#include "element.h"
+
+Element::Element(Set * s) :
+ set(s) {
+}
--- /dev/null
+#ifndef ELEMENT_H
+#define ELEMENT_H
+#include "classlist.h"
+#include "mymemory.h"
+
+class Element {
+ public:
+ Element(Set *s);
+ MEMALLOC;
+ private:
+ Set *set;
+};
+#endif
--- /dev/null
+#include "function.h"
--- /dev/null
+#ifndef FUNCTION_H
+#define FUNCTION_H
+#include "classlist.h"
+#include "mymemory.h"
+class Function {
+ public:
+
+ MEMALLOC;
+ private:
+};
+#endif
capacitymask = initialcapacity - 1;
threshold = (unsigned int)(initialcapacity * loadfactor);
- size = 0; // Initial number of elements in the hash
+ size = 0; // Initial number of elements in the hash
}
/** @brief Hash table destructor */
exit(EXIT_FAILURE);
}
- table = newtable; // Update the global hashtable upon resize()
+ table = newtable; // Update the global hashtable upon resize()
capacity = newsize;
capacitymask = newsize - 1;
search->val = bin->val;
}
- _free(oldtable); // Free the memory of the old hash table
+ _free(oldtable); // Free the memory of the old hash table
}
double getLoadFactor() {return loadfactor;}
unsigned int getCapacity() {return capacity;}
--- /dev/null
+#include "mutableset.h"
+
--- /dev/null
+#ifndef MUTABLESET_H
+#define MUTABLESET_H
+#include "set.h"
+
+class MutableSet : Set {
+public:
+ void addElement(uint64_t element) { members->push_back(element); }
+};
+#endif
void operator delete[](void *p, size_t size) { \
model_free(p); \
} \
- void * operator new(size_t size, void *p) { /* placement new */ \
+ void * operator new(size_t size, void *p) { /* placement new */ \
return p; \
}
--- /dev/null
+#ifndef OPS_H
+#define OPS_H
+enum LogicOp {AND, OR, NOT, XOR, IMPLIES};
+enum ArithOp {ADD, SUB};
+enum CompOp {EQUALS};
+enum OrderType {PARTIAL, TOTAL};
+
+/**
+ * FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
+ * OVERFLOWSETSFLAG -- sets the flag if the operation overflows
+ * FLAGIFFOVERFLOW -- flag is set iff the operation overflows
+ * IGNORE -- doesn't constrain output if the result cannot be represented
+ * WRAPAROUND -- wraps around like stand integer arithmetic
+ */
+enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW};
+
+#endif
--- /dev/null
+#ifndef ORDER_H
+#define ORDER_H
+#include "classlist.h"
+#include "mymemory.h"
+
+class Order {
+ public:
+ MEMALLOC;
+
+ private:
+};
+#endif
--- /dev/null
+#include "predicate.h"
--- /dev/null
+#ifndef PREDICATE_H
+#define PREDICATE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+class Predicate {
+ public:
+
+ MEMALLOC;
+ private:
+};
+#endif
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
#include "set.h"
#include <stddef.h>
#include <cassert>
-Node::Node(uint64 val, Node* r, Node* l){
- range=false;
- beginOrVal=val;
- left = l;
- right=r;
-}
-
-Node::Node(uint64 val):Node(val, NULL, NULL){}
-
-Node::Node(uint64 begin, uint64 end, Node* r, Node* l){
- range=true;
- beginOrVal=begin;
- this->end= end;
- right=r;
- left=l;
-}
-
-Node::Node(uint64 begin, uint64 end):Node(begin, end, NULL, NULL){}
-
-Comparison Node::compare(uint64 val){
- if(range){
- if(val> end)
- return GREATER;
- else if(val < beginOrVal)
- return LESS;
- else
- return EQUAL;
- }else{
- if(val> beginOrVal)
- return GREATER;
- else if(val< beginOrVal)
- return LESS;
- else
- return EQUAL;
- }
+Set::Set(VarType t, uint64_t* elements, int num) :
+ type (t),
+ isRange(false),
+ low(0),
+ high(0),
+ members(new ModelVector<uint64_t>()) {
+ members->reserve(num);
+ for(int i=0;i<num;i++)
+ members->push_back(elements[i]);
}
-void Node::addNode(Node* n){
- assert(!n->isRange());
- Comparison comp = compare(n->getBeginOrRange());
- if(comp == GREATER){
- if(right!=NULL)
- right->addNode(n);
- else
- right=n;
- }else if(comp == LESS){
- if(left!= NULL)
- left->addNode(n);
- else
- left = n;
- }
-
+Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) :
+ type(t),
+ isRange(true),
+ low(lowrange),
+ high(highrange),
+ members(NULL) {
}
-Set::Set(Type t, uint64* elements, int num){
- type=t;
- size=num;
- for(int i=0; i<num; i++){
- addItem(elements[i]);
- }
+Set::~Set() {
+ if (isRange)
+ delete members;
}
-
-Set::Set(Type t, uint64 lowrange, uint64 highrange){
- assert(highrange>lowrange);
- type =t;
- size = highrange-lowrange+1;
- root = new Node(lowrange,highrange);
-}
-
-Set::Set(Type t): type(t),
- size(0),
- root(NULL)
-{
-}
-
-void Set::addItem(uint64 element){
- Node* n = new Node(element);
- if(root==NULL)
- root=n;
- else
- root->addNode(n);
-}
-
-
\ No newline at end of file
/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/*
* File: set.h
* Author: hamed
*
#ifndef SET_H
#define SET_H
-#include "types.h"
+#include "classlist.h"
+#include "stl-model.h"
+#include "mymemory.h"
-enum Comparison{LESS, EQUAL, GREATER};
+class Set {
+public:
+ Set(VarType t, uint64_t * elements, int num);
+ Set(VarType t, uint64_t lowrange, uint64_t highrange);
+ ~Set();
-class Node{
+ MEMALLOC;
private:
- bool range;
- // If it isn't a range, begin contains the actual value of the element
- uint64 beginOrVal;
- uint64 end;
- Node* right;
- Node* left;
-public:
- Node(uint64 val, Node* r, Node* l);
- Node(uint64 val);
- Node(uint64 begin, uint64 end, Node* r, Node* l);
- Node(uint64 begin, uint64 end);
- bool isRange(){return range;}
- uint64 getBeginOrRange(){return beginOrVal;}
- Comparison compare(uint64 val);
- /**
- * Searches the tree, if new node exists in the tree ( whether its value
- * is in range of another node, or there is another node with the value of
- * node n) this function just returns!
- * @param n
- */
- void addNode(Node* n);
-};
-// For now, we can consider it as a simple binary tree, but we can have fancier
-// trees for future
-class Set{
- Type type;
- uint64 size;
- Node* root;
- Set(Type t, uint64 * elements, int num);
- Set(Type t, uint64 lowrange, uint64 highrange);
- Set(Type t);
- /**
- * For know all sets are considered to be mutable, we can change it later on
- * if it was necessary.
- * @param set
- * @param element
- */
- void addItem(uint64 element);
- ELEMENT* createUniqueItem(Set * set);
+ VarType type;
+ bool isRange;
+ uint64_t low, high;
+protected:
+ ModelVector<uint64_t> *members;
};
-
-
-#endif /* SET_H */
+#endif/* SET_H */
--- /dev/null
+#include "table.h"
--- /dev/null
+#ifndef TABLE_H
+#define TABLE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+class Table {
+ public:
+ MEMALLOC;
+ private:
+};
+#endif
+++ /dev/null
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/*
- * File: Type.h
- * Author: hamed
- *
- * Created on June 13, 2017, 1:33 PM
- */
-
-#ifndef TYPE_H
-#define TYPE_H
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-typedef unsigned long int uint64;
-typedef uint64 Type;
-
-struct Element{
- uint64 value;
-};
-
-typedef struct Element ELEMENT;
-#ifdef __cplusplus
-}
-#endif
-
-#endif /* TYPE_H */
-