set -e
BASE=../
-SERVERS="dc-5.calit2.uci.edu dc-7.calit2.uci.edu dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu"
+SERVERS="dc-4.calit2.uci.edu dc-5.calit2.uci.edu dc-6.calit2.uci.edu dc-7.calit2.uci.edu dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu"
REMOTEDIR="/scratch/hamed/"
INFILE="constraint_compiler/"
SRC="constraint_compiler/src/"
rm -f $OUTFILE
tar -czvf $OUTFILE $INFILE
+cp $OUTFILE $SHAREDDIR
for SERVER in $SERVERS; do
- cp $OUTFILE $SHAREDDIR
- ssh $USER@$SERVER "mv $SHAREDDIR$OUTFILE $REMOTEDIR; cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh"
+ ssh $USER@$SERVER "cp $SHAREDDIR$OUTFILE $REMOTEDIR; cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh"
done
typedef enum ElementEncodingType ElementEncodingType;
-enum BooleanVarOrdering {CONSTRAINTORDERING=0, CHORONOLOGICALORDERING=1, REVERSEORDERING=2};
+enum BooleanVarOrdering {CONSTRAINTORDERING=0, ELEMENTORDERING=1, REVERSEORDERING=2};
typedef enum BooleanVarOrdering BooleanVarOrdering;
Polarity negatePolarity(Polarity This);
enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, SATC_FLAGFORCEUNDEFINED, SATC_UNDEFINEDSETSFLAG, SATC_FLAGIFFUNDEFINED};
typedef enum UndefinedBehavior UndefinedBehavior;
+enum InterpreterType {SATUNE, ALLOY, Z3, MATHSAT, SMTRAT};
+typedef enum InterpreterType InterpreterType;
+
+
#endif
}
uint convertSize(uint cost) {
- cost = FUDGEFACTOR * cost;// fudge factor
return NEXTPOW2(cost);
}
EncodingNode *tmp = left; left = right; right = tmp;
EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
}
-
- uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
+
+ uint leftSize = 0, rightSize = 0, newSize = 0, min = 0;
bool merge = false;
if (leftGraph == NULL && rightGraph == NULL) {
leftSize = convertSize(left->getSize());
newSize = convertSize(left->s->getUnionSize(right->s));
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
+ min = rightSize > leftSize ? leftSize : rightSize;
+ merge = left->measureSimilarity(right) > 1.5 || min == newSize;
} else if (leftGraph != NULL && rightGraph == NULL) {
- leftSize = convertSize(leftGraph->encodingSize);
+ leftSize = convertSize(leftGraph->numValues());
rightSize = convertSize(right->getSize());
newSize = convertSize(leftGraph->estimateNewSize(right));
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
- max = rightSize > leftSize? rightSize : leftSize;
-// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
- merge = left->measureSimilarity(right) > 1.5 || max == newSize;
+ min = rightSize > leftSize ? leftSize : rightSize;
+ merge = leftGraph->measureSimilarity(right) > 1.5 || min == newSize;
+// model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
} else {
//Neither are null
- leftSize = convertSize(leftGraph->encodingSize);
- rightSize = convertSize(rightGraph->encodingSize);
+ leftSize = convertSize(leftGraph->numValues());
+ rightSize = convertSize(rightGraph->numValues());
newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
// model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
- max = rightSize > leftSize? rightSize : leftSize;
-// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
- merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
+ min = rightSize > leftSize ? leftSize : rightSize;
+ merge = leftGraph->measureSimilarity(rightGraph) > 1.5 || min == newSize;
+// model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
}
if (merge) {
//add the edge
return s->getSize();
}
-uint64_t EncodingNode::getIndex(uint index){
+uint64_t EncodingNode::getIndex(uint index) {
return s->getElement(index);
}
return s->getType();
}
-bool EncodingNode::itemExists(uint64_t item){
- for(uint i=0; i< s->getSize(); i++){
- if(item == s->getElement(i))
- return true;
- }
- return false;
-}
-
-double EncodingNode::measureSimilarity(EncodingNode *node){
+double EncodingNode::measureSimilarity(EncodingNode *node) {
uint common = 0;
- for(uint i=0; i < s->getSize(); i++){
+ for (uint i = 0, j = 0; i < s->getSize() && j < node->s->getSize(); ) {
uint64_t item = s->getElement(i);
- if(node->itemExists(item)){
+ uint64_t item2 = node->s->getElement(j);
+ if (item < item2)
+ i++;
+ else if (item2 > item)
+ j++;
+ else {
+ i++;
+ j++;
common++;
}
}
-// model_print("common=%u\tsize1=%u\tsize2=%u\tsim1=%f\tsim2=%f\n", common, s->getSize(), node->getSize(), 1.0*common/s->getSize(), 1.0*common/node->getSize());
- return common*1.0/s->getSize() + common*1.0/node->getSize();
+
+ return common * 1.0 / s->getSize() + common * 1.0 / node->getSize();
}
EncodingNode *EncodingGraph::createNode(Element *e) {
#include "structs.h"
#include "graphstructs.h"
-#define FUDGEFACTOR 1.2
-#define CONVERSIONFACTOR 0.5
class EncodingGraph {
public:
uint getSize() const;
uint64_t getIndex(uint index);
VarType getType() const;
- double measureSimilarity(EncodingNode *node);
+ double measureSimilarity(EncodingNode *node);
void setEncoding(ElementEncodingType e) {encoding = e;}
ElementEncodingType getEncoding() {return encoding;}
- bool itemExists(uint64_t item);
bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
CMEMALLOC;
private:
#include "qsort.h"
EncodingSubGraph::EncodingSubGraph() :
- encodingSize(0),
- numElements(0),
maxEncodingVal(0) {
}
}
uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
- uint newSize = 0;
- SetIteratorEncodingNode *nit = sg->nodes.iterator();
- while (nit->hasNext()) {
- EncodingNode *en = nit->next();
- uint size = estimateNewSize(en);
- if (size > newSize)
- newSize = size;
+ uint newSize = sg->allValues.getSize() + allValues.getSize();
+ SetIterator64Int *it = sg->allValues.iterator();
+
+ while (it->hasNext()) {
+ uint64_t val = it->next();
+ if (allValues.contains(val))
+ newSize--;
}
- delete nit;
+ delete it;
return newSize;
}
double EncodingSubGraph::measureSimilarity(EncodingNode *node) {
uint common = 0;
- Hashset64Int intSet;
- SetIteratorEncodingNode *nit = nodes.iterator();
- while (nit->hasNext()) {
- EncodingNode *en = nit->next();
- for(uint i=0; i < en->getSize(); i++){
- intSet.add(en->getIndex(i));
- }
- }
- for(uint i=0; i < node->getSize(); i++){
- if(intSet.contains( node->getIndex(i) )){
+ uint size = node->getSize();
+ for (uint i = 0; i < size; i++) {
+ uint64_t val = node->getIndex(i);
+ if (allValues.contains(val))
common++;
- }
}
-// model_print("measureSimilarity:139: common=%u\t GraphSize=%u\tnodeSize=%u\tGraphSim=%f\tnodeSim=%f\n", common, intSet.getSize(), node->getSize(), 1.0*common/intSet.getSize(), 1.0*common/node->getSize());
- delete nit;
- return common*1.0/intSet.getSize() + common*1.0/node->getSize();
+ return common * 1.0 / allValues.getSize() + common * 1.0 / node->getSize();
}
double EncodingSubGraph::measureSimilarity(EncodingSubGraph *sg) {
uint common = 0;
- Hashset64Int set1;
- Hashset64Int set2;
- SetIteratorEncodingNode *nit = nodes.iterator();
- while (nit->hasNext()) {
- EncodingNode *en = nit->next();
- for(uint i=0; i < en->getSize(); i++){
- set1.add(en->getIndex(i));
- }
- }
- delete nit;
- nit = sg->nodes.iterator();
- while (nit->hasNext()) {
- EncodingNode *en = nit->next();
- for(uint i=0; i < en->getSize(); i++){
- set2.add(en->getIndex(i));
- }
- }
- delete nit;
- SetIterator64Int *setIter1 = set1.iterator();
- while(setIter1->hasNext()){
+ SetIterator64Int *setIter1 = allValues.iterator();
+ while (setIter1->hasNext()) {
uint64_t item1 = setIter1->next();
- if( set2.contains(item1)){
+ if ( sg->allValues.contains(item1)) {
common++;
}
}
delete setIter1;
-// model_print("measureSimilarity:139: common=%u\tGraphSize1=%u\tGraphSize2=%u\tGraphSize1=%f\tGraphSize2=%f\n", common, set1.getSize(), set2.getSize(), 1.0*common/set1.getSize(), 1.0*common/set2.getSize());
- return common*1.0/set1.getSize() + common*1.0/set2.getSize();
+ return common * 1.0 / allValues.getSize() + common * 1.0 / sg->allValues.getSize();
}
uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
- SetIteratorEncodingEdge *eeit = n->edges.iterator();
- uint newsize = n->getSize();
- while (eeit->hasNext()) {
- EncodingEdge *ee = eeit->next();
- if (ee->left != NULL && ee->left != n && nodes.contains(ee->left)) {
- uint intersectSize = n->s->getUnionSize(ee->left->s);
- if (intersectSize > newsize)
- newsize = intersectSize;
- }
- if (ee->right != NULL && ee->right != n && nodes.contains(ee->right)) {
- uint intersectSize = n->s->getUnionSize(ee->right->s);
- if (intersectSize > newsize)
- newsize = intersectSize;
- }
- if (ee->dst != NULL && ee->dst != n && nodes.contains(ee->dst)) {
- uint intersectSize = n->s->getUnionSize(ee->dst->s);
- if (intersectSize > newsize)
- newsize = intersectSize;
- }
+ uint nSize = n->getSize();
+ uint newSize = allValues.getSize() + nSize;
+ for (uint i = 0; i < nSize; i++) {
+ if (allValues.contains(n->getIndex(i)))
+ newSize--;
}
- delete eeit;
- return newsize;
+ return newSize;
+}
+
+uint EncodingSubGraph::numValues() {
+ return allValues.getSize();
}
void EncodingSubGraph::addNode(EncodingNode *n) {
nodes.add(n);
- uint newSize = estimateNewSize(n);
- numElements += n->elements.getSize();
- if (newSize > encodingSize)
- encodingSize = newSize;
+ uint size = n->getSize();
+ for (uint i = 0; i < size; i++)
+ allValues.add(n->getIndex(i));
}
SetIteratorEncodingNode *EncodingSubGraph::nodeIterator() {
void encode();
uint getEncoding(EncodingNode *n, uint64_t val);
uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;}
- double measureSimilarity(EncodingNode *n);
- double measureSimilarity(EncodingSubGraph *sg);
+ double measureSimilarity(EncodingNode *n);
+ double measureSimilarity(EncodingSubGraph *sg);
+ uint numValues();
CMEMALLOC;
private:
uint estimateNewSize(EncodingNode *n);
HashsetEncodingValue values;
HashsetEncodingNode nodes;
NVPMap map;
- uint encodingSize;
- uint numElements;
uint maxEncodingVal;
-
+ Hashset64Int allValues;
friend class EncodingGraph;
};
ElementOpt::ElementOpt(CSolver *_solver)
: Transform(_solver),
- updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+ updateSets(false)
{
}
if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
return;
+ //Set once we know we are going to use it.
+ updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
+
SetIteratorBooleanEdge *iterator = solver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
}
void Preprocess::doTransform() {
- if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+ if (!solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
return;
BooleanIterator bit(solver);
* and open the template in the editor.
*/
-/*
+/*
* File: VarOrderingOpt.cpp
* Author: hamed
- *
+ *
* Created on October 11, 2018, 5:31 PM
*/
#include "elementencoding.h"
#include "element.h"
-VarOrderingOpt::VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder): Transform(_solver){
+VarOrderingOpt::VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder) : Transform(_solver) {
satencoder = _satencoder;
}
VarOrderingOpt::~VarOrderingOpt() {
}
-void VarOrderingOpt::doTransform(){
+void VarOrderingOpt::doTransform() {
BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
- if ( direction == CONSTRAINTORDERING ){
+ if ( direction == CONSTRAINTORDERING ) {
return;
}
-
+
uint size = solver->allElements.getSize();
- if(direction == CHORONOLOGICALORDERING){
+ if (direction == ELEMENTORDERING) {
for (uint i = 0; i < size; i++) {
Element *el = solver->allElements.get(i);
ElementEncoding *encoding = el->getElementEncoding();
continue;
satencoder->encodeElementSATEncoder(el);
}
- }else{
- for (int i = size-1; i>0; i--) {
+ } else {
+ for (int i = size - 1; i > 0; i--) {
Element *el = solver->allElements.get(i);
ElementEncoding *encoding = el->getElementEncoding();
if (encoding->getElementEncodingType() == ELEM_UNASSIGNED)
* and open the template in the editor.
*/
-/*
+/*
* File: VarOrderingOpt.h
* Author: hamed
*
#include "transform.h"
-class VarOrderingOpt :Transform {
+class VarOrderingOpt : Transform {
public:
- VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder);
- void doTransform();
- virtual ~VarOrderingOpt();
+ VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder);
+ void doTransform();
+ virtual ~VarOrderingOpt();
private:
- SATEncoder* satencoder;
+ SATEncoder *satencoder;
};
-#endif /* VARORDERINGOPT_H */
+#endif/* VARORDERINGOPT_H */
fd_set rfds;
FD_ZERO(&rfds);
FD_SET(This->from_solver_fd, &rfds);
- fd_set * temp;
- if(This->timeout == NOTIMEOUT){
- retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, NULL);
- }else {
+ fd_set *temp;
+ if (This->timeout == NOTIMEOUT) {
+ retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
+ } else {
struct timeval tv;
tv.tv_sec = This->timeout;
tv.tv_usec = 0;
- retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, &tv);
+ retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
}
- if(retval == -1){
+ if (retval == -1) {
perror("Error in select()");
exit(EXIT_FAILURE);
}
- else if (retval){
+ else if (retval) {
printf("Data is available now.\n");
return readIntSolver(This);
- }else{
+ } else {
printf("Timeout for the solver\n");
return IS_INDETER;
}
pid_t solver_pid;
int to_solver_fd;
int from_solver_fd;
- long timeout;
+ long timeout;
};
IncrementalSolver *allocIncrementalSolver();
#include "predicate.h"
#include "csolver.h"
#include "tunable.h"
+#include <cmath>
void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
uint numParents = elem->parents.getSize();
ASSERT(encoding->type == BINARYINDEX);
allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
- if (encoding->element->anyValue){
+ if (encoding->element->anyValue) {
uint setSize = encoding->element->getRange()->getSize();
- uint encArraySize = encoding->encArraySize;
- if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+ int maxIndex = getMaximumUsedSize(encoding);
+ if (setSize == encoding->encArraySize && maxIndex == (int)setSize) {
+ return;
+ }
+ double ratio = (setSize * (1 + 2 * encoding->numVars)) / (encoding->numVars * (encoding->numVars + maxIndex * 1.0 - setSize));
+// model_print("encArraySize=%u\tmaxIndex=%d\tsetSize=%u\tmetric=%f\tnumBits=%u\n", encoding->encArraySize, maxIndex, setSize, ratio, encoding->numVars);
+ if ( ratio < pow(2, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 3)) {
generateAnyValueBinaryIndexEncodingPositive(encoding);
} else {
generateAnyValueBinaryIndexEncoding(encoding);
}
}
+int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+ for (int i = encoding->encArraySize - 1; i >= 0; i--) {
+ if (encoding->isinUseElement(i))
+ return i + 1;
+ }
+ ASSERT(false);
+ return -1;
+}
+
void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
if (encoding->numVars == 0)
return;
- int index = -1;
- for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
- if (encoding->isinUseElement(i)) {
- if (i + 1 < encoding->encArraySize) {
- index = i + 1;
- }
- break;
- }
- }
- if ( index != -1 ) {
+ int index = getMaximumUsedSize(encoding);
+ if ( index != (int)encoding->encArraySize ) {
addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
}
- index = index == -1 ? encoding->encArraySize - 1 : index - 1;
- for (int i = index; i >= 0; i--) {
+ for (int i = index - 1; i >= 0; i--) {
if (!encoding->isinUseElement(i)) {
addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
}
void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+ int getMaximumUsedSize(ElementEncoding *encoding);
void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
CNF *cnf;
CSolver *solver;
BooleanToEdgeMap booledgeMap;
VectorEdge *vector;
- friend class VarOrderingOpt;
+ friend class VarOrderingOpt;
};
void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
memcpy(array, _array, capacity * sizeof(type));
}
+ Vector(Vector<type> *v) :
+ size(v->size),
+ capacity(v->capacity),
+ array((type *) ourmalloc(sizeof(type) * v->capacity)) {
+ memcpy(array, v->array, capacity * sizeof(type));
+ }
void pop() {
size--;
}
array[index] = item;
}
+ void insertAt(uint index, type item) {
+ setSize(size + 1);
+ for (uint i = size - 1; i > index; i--) {
+ set(i, get(i - 1));
+ }
+ array[index] = item;
+ }
+
+ void removeAt(uint index) {
+ for (uint i = index; (i + 1) < size; i++) {
+ set(i, get(i + 1));
+ }
+ setSize(size - 1);
+ }
+
inline uint getSize() const {
return size;
}
#include "orderelement.h"
#include "structs.h"
#include "decomposeorderresolver.h"
-#include "tunabledependent.h"
+#include "searchtuner.h"
#define HASHNEXT(hash, newval) {hash += newval; hash += hash << 10; hash ^= hash >> 6;}
#define HASHFINAL(hash) {hash += hash << 3; hash ^= hash >> 11; hash += hash << 15;}
return true;
}
-unsigned int tunable_dependent_hash_function(TunableDependent *This){
- return (uint)This->dependent;
-}
-
-bool tunable_dependent_equals(TunableDependent *key1, TunableDependent *key2){
- return key1->dependent == key2->dependent;
-}
-
unsigned int order_node_hash_function(OrderNodeKey *This) {
return (uint) This->id;
}
return key1->newfirst == key2->newfirst &&
key1->newsecond == key2->newsecond;
}
+
+unsigned int tunableSettingHash(TunableSetting *setting) {
+ return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
+}
+
+bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
+ return setting1->hasVar == setting2->hasVar &&
+ setting1->type1 == setting2->type1 &&
+ setting1->type2 == setting2->type2 &&
+ setting1->param == setting2->param;
+}
bool table_entry_equals(TableEntry *key1, TableEntry *key2);
unsigned int order_node_hash_function(OrderNodeKey *This);
bool order_node_equals(OrderNodeKey *key1, OrderNodeKey *key2);
-unsigned int tunable_dependent_hash_function(TunableDependent *This);
-bool tunable_dependent_equals(TunableDependent *key1, TunableDependent *key2);
unsigned int order_edge_hash_function(OrderEdge *This);
bool order_edge_equals(OrderEdge *key1, OrderEdge *key2);
unsigned int order_element_hash_function(OrderElement *This);
bool order_element_equals(OrderElement *key1, OrderElement *key2);
unsigned int order_pair_hash_function(OrderPair *This);
bool order_pair_equals(OrderPair *key1, OrderPair *key2);
-
+unsigned int tunableSettingHash(TunableSetting *setting);
+bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2);
unsigned int doredge_hash_function(DOREdge *key);
bool doredge_equals(DOREdge *key1, DOREdge *key2);
typedef Hashset<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
typedef Hashset<OrderNodeKey *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> HashsetOrderNode;
-typedef Hashset<TunableDependent *, uintptr_t, PTRSHIFT, tunable_dependent_hash_function, tunable_dependent_equals> HashsetTunableDep;
typedef Hashset<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
typedef Hashset<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> HashsetOrderElement;
typedef Hashset<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> HashsetDOREdge;
typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
-typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
typedef Hashset<uint64_t, uint64_t, 0> Hashset64Int;
-typedef SetIterator<uint64_t, uint64_t, 0> SetIterator64Int;
+typedef Hashset<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> HashsetTunableSetting;
typedef Hashtable<OrderNodeKey *, HashsetOrderNode *, uintptr_t, PTRSHIFT> HashtableNodeToNodeSet;
typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, PTRSHIFT, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
typedef Hashtable<void *, void *, uintptr_t, PTRSHIFT> CloneMap;
-
-
typedef Hashtable<Set *, EncodingNode *, uintptr_t, PTRSHIFT> HashtableEncoding;
typedef SetIterator<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
typedef SetIterator<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
typedef SetIterator<OrderNodeKey *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
-typedef SetIterator<TunableDependent *, uintptr_t, PTRSHIFT, tunable_dependent_hash_function, tunable_dependent_equals> SetIteratorTunableDep;
typedef SetIterator<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
typedef SetIterator<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> SetIteratorDOREdge;
+typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
+typedef SetIterator<uint64_t, uint64_t, 0> SetIterator64Int;
+typedef SetIterator<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> SetIteratorTunableSetting;
#endif
if (This->type != ELEMCONST) {
model_print("INFO: naive encoder is making the decision about element %p....\n", This);
}
- encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
+ uint enc = csolver->getTuner()->getVarTunable(This->getRange()->getType(), NODEENCODING, &NodeEncodingDesc);
+ if (enc == ELEM_UNASSIGNED)
+ enc = csolver->getTuner()->getTunable(NAIVEENCODER, &NaiveEncodingDesc);
+ encoding->setElementEncodingType((ElementEncodingType)enc);
encoding->encodingArrayInitialization();
}
--- /dev/null
+#include "alloyinterpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "alloysig.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+#include "cppvector.h"
+#include "math.h"
+
+using namespace std;
+
+#define ALLOYFILENAME "satune.als"
+#define ALLOYSOLUTIONFILE "solution.sol"
+
+AlloyInterpreter::AlloyInterpreter(CSolver *_solver):
+ Interpreter(_solver)
+{
+ output.open(ALLOYFILENAME);
+ if(!output.is_open()){
+ model_print("AlloyEnc:Error in opening the dump file satune.als\n");
+ exit(-1);
+ }
+}
+
+AlloyInterpreter::~AlloyInterpreter(){
+ if(output.is_open()){
+ output.close();
+ }
+}
+
+ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
+ return new AlloyBoolSig(id);
+}
+
+ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
+ return new AlloyElementSig(id, ssig);
+}
+
+Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
+ return new AlloySetSig(id, set);
+}
+
+void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
+ output << "fact {" << endl;
+ for(uint i=0; i< facts.getSize(); i++){
+ char *cstr = facts.get(i);
+ writeToFile(cstr);
+ }
+ output << "}" << endl;
+}
+
+
+int AlloyInterpreter::getResult(){
+ ifstream input(ALLOYSOLUTIONFILE, ios::in);
+ string line;
+ while(getline(input, line)){
+ if(line.find("Unsatisfiable.")== 0){
+ return IS_UNSAT;
+ }
+ if(line.find("univ") == 0){
+ continue;
+ }
+ if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
+ const char delim [2] = ",";
+ char cline [line.size()+1];
+ strcpy ( cline, line.c_str() );
+ char *token = strtok(cline, delim);
+ while( token != NULL ) {
+ uint i1, i2, i3;
+ if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+ model_print("Signature%u = %u\n", i1, i3);
+ sigEnc.setValue(i1, i3);
+ }
+ token = strtok(NULL, delim);
+ }
+ }
+ }
+ return IS_SAT;
+}
+
+
+int AlloyInterpreter::getAlloyIntScope(){
+ double mylog = log2(sigEnc.getMaxValue() + 1);
+ return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+}
+
+void AlloyInterpreter::dumpFooter(){
+ output << "pred show {}" << endl;
+ output << "run show for " << getAlloyIntScope() << " int" << endl;
+}
+
+void AlloyInterpreter::dumpHeader(){
+ output << "open util/integer" << endl;
+}
+
+void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+ snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
+}
+
+string AlloyInterpreter::negateConstraint(string constr){
+ return "not ( " + constr + " )";
+}
+
+string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+ uint size = bl->inputs.getSize();
+ string array[size];
+ for (uint i = 0; i < size; i++)
+ array[i] = encodeConstraint(bl->inputs.get(i));
+ string op;
+ switch (bl->op){
+ case SATC_OR:
+ op = " or ";
+ break;
+ case SATC_AND:
+ op = " and ";
+ break;
+ case SATC_NOT:
+ op = " not ";
+ break;
+ case SATC_IFF:
+ op = " iff ";
+ break;
+ case SATC_IMPLIES:
+ op = " implies ";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
+ }
+ switch (bl->op) {
+ case SATC_OR:
+ case SATC_AND:{
+ ASSERT(size >= 2);
+ string res = "( ";
+ res += array[0];
+ for( uint i=1; i< size; i++){
+ res += op + array[i];
+ }
+ res += " )";
+ return res;
+ }
+ case SATC_NOT:{
+ return "not ( " + array[0] + " )";
+ }
+ case SATC_IMPLIES:
+ case SATC_IFF:
+ return "( " + array[0] + op + array[1] + " )";
+ case SATC_XOR:
+ default:
+ ASSERT(0);
+
+ }
+}
+
+string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
+ ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+ return *boolSig + " = 1";
+}
+
+string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+ FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
+ uint numDomains = elemFunc->inputs.getSize();
+ ASSERT(numDomains > 1);
+ ValuedSignature *inputs[numDomains];
+ string result;
+ for (uint i = 0; i < numDomains; i++) {
+ Element *elem = elemFunc->inputs.get(i);
+ inputs[i] = sigEnc.getElementSignature(elem);
+ if(elem->type == ELEMFUNCRETURN){
+ result += processElementFunction((ElementFunction *) elem, inputs[i]);
+ }
+ }
+ string op;
+ switch(function->op){
+ case SATC_ADD:
+ op = ".add";
+ break;
+ case SATC_SUB:
+ op = ".sub";
+ break;
+ default:
+ ASSERT(0);
+ }
+ result += *signature + " = " + *inputs[0];
+ for (uint i = 1; i < numDomains; i++) {
+ result += op + "["+ *inputs[i] +"]";
+ }
+ result += "\n";
+ return result;
+}
+
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+ switch (op) {
+ case SATC_EQUALS:
+ return *elemSig1 + " = " + *elemSig2;
+ case SATC_LT:
+ return *elemSig1 + " < " + *elemSig2;
+ case SATC_GT:
+ return *elemSig1 + " > " + *elemSig2;
+ default:
+ ASSERT(0);
+ }
+}
+
+
--- /dev/null
+#ifndef ALLOYINTERPRETER_H
+#define ALLOYINTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "interpreter.h"
+#include <iostream>
+#include <fstream>
+
+class AlloyInterpreter: public Interpreter{
+public:
+ AlloyInterpreter(CSolver *solver);
+ virtual ValuedSignature *getBooleanSignature(uint id);
+ virtual ValuedSignature *getElementSignature(uint id, Signature *ssig);
+ virtual Signature *getSetSignature(uint id, Set *set);
+ virtual ~AlloyInterpreter();
+protected:
+ virtual void dumpFooter();
+ virtual void dumpHeader();
+ int getAlloyIntScope();
+ virtual void compileRunCommand(char * command , size_t size);
+ virtual int getResult();
+ virtual void dumpAllConstraints(Vector<char *> &facts);
+ virtual string negateConstraint(string constr);
+ virtual string encodeBooleanLogic( BooleanLogic *bl);
+ virtual string encodeBooleanVar( BooleanVar *bv);
+ string encodeOperatorPredicate(BooleanPredicate *constraint);
+ virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
+ virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
+};
+
+#endif
--- /dev/null
+#include "alloysig.h"
+#include "set.h"
+
+bool AlloyBoolSig::encodeAbs = true;
+bool AlloySetSig::encodeAbs = true;
+bool AlloyElementSig::encodeAbs = true;
+
+AlloyBoolSig::AlloyBoolSig(uint id):
+ ValuedSignature(id)
+{
+}
+
+string AlloyBoolSig::toString() const{
+ return "Boolean" + to_string(id) + ".value";
+}
+
+string AlloyBoolSig::getSignature() const{
+ string str;
+ if(encodeAbs){
+ encodeAbs = false;
+ str += getAbsSignature();
+ }
+ str += "one sig Boolean" + to_string(id) + " extends AbsBool {}";
+ return str;
+}
+
+string AlloyBoolSig::getAbsSignature() const{
+ string str;
+ if(AlloySetSig::encodeAbs){
+ AlloySetSig::encodeAbs = false;
+ str += "abstract sig AbsSet {\
+ domain: set Int\
+ }\n";
+ }
+ str +="one sig BooleanSet extends AbsSet {}{\n\
+ domain = 0 + 1 \n\
+ }\n\
+ abstract sig AbsBool {\
+ value: Int\
+ }{\n\
+ value in BooleanSet.domain\n\
+ }\n";
+ return str;
+}
+
+AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig):
+ ValuedSignature(id),
+ ssig(_ssig)
+{
+}
+
+string AlloyElementSig::toString() const{
+ return "Element" + to_string(id) + ".value";
+}
+
+string AlloyElementSig::getSignature() const{
+ string str;
+ if(encodeAbs){
+ encodeAbs = false;
+ str += getAbsSignature();
+ }
+ str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\
+ value in " + *ssig + "\n\
+ }";
+ return str;
+}
+
+string AlloyElementSig::getAbsSignature() const{
+ return "abstract sig AbsElement {\n\
+ value: Int\n\
+ }\n";
+
+}
+
+AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){
+ ASSERT(set->getSize() > 0);
+ domain = to_string(set->getElement(0));
+ for(uint i=1; i< set->getSize(); i++){
+ domain += " + " + to_string(set->getElement(i));
+ }
+}
+
+string AlloySetSig::toString() const{
+ return "Set" + to_string(id) + ".domain";
+}
+
+string AlloySetSig::getSignature() const{
+ string str;
+ if(encodeAbs){
+ encodeAbs = false;
+ str += getAbsSignature();
+ }
+ str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\
+ domain = " + domain + "\n\
+ }";
+ return str;
+}
+
+string AlloySetSig::getAbsSignature() const{
+ return "abstract sig AbsSet {\n\
+ domain: set Int\n\
+ }\n";
+
+}
--- /dev/null
+#ifndef ALLOYSIG_H
+#define ALLOYSIG_H
+#include <string>
+#include <iostream>
+#include "signature.h"
+#include "classlist.h"
+using namespace std;
+
+class AlloyBoolSig: public ValuedSignature{
+public:
+ AlloyBoolSig(uint id);
+ virtual ~AlloyBoolSig(){}
+ virtual string toString() const;
+ virtual string getAbsSignature() const;
+ virtual string getSignature() const;
+private:
+ static bool encodeAbs;
+};
+
+class AlloySetSig: public Signature{
+public:
+ AlloySetSig(uint id, Set *set);
+ virtual ~AlloySetSig(){}
+ virtual string toString() const;
+ virtual string getAbsSignature() const;
+ virtual string getSignature() const;
+ static bool encodeAbs;
+private:
+ string domain;
+};
+
+class AlloyElementSig: public ValuedSignature{
+public:
+ AlloyElementSig(uint id, Signature *ssig);
+ virtual ~AlloyElementSig(){}
+ virtual string toString() const;
+ virtual string getAbsSignature() const;
+ virtual string getSignature() const;
+private:
+ Signature *ssig;
+ static bool encodeAbs;
+};
+
+#endif
--- /dev/null
+#include "interpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "signature.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+
+using namespace std;
+
+Interpreter::Interpreter(CSolver *_solver):
+ csolver(_solver),
+ sigEnc(this)
+{
+}
+
+Interpreter::~Interpreter(){
+}
+
+void Interpreter::encode(){
+ dumpHeader();
+ SetIteratorBooleanEdge *iterator = csolver->getConstraints();
+ Vector<char *> facts;
+ while(iterator->hasNext()){
+ BooleanEdge constraint = iterator->next();
+ string constr = encodeConstraint(constraint);
+ char *cstr = new char [constr.length()+1];
+ strcpy (cstr, constr.c_str());
+ facts.push(cstr);
+ }
+ dumpAllConstraints(facts);
+ for(uint i=0; i< facts.getSize(); i++){
+ char *cstr = facts.get(i);
+ delete[] cstr;
+ }
+ delete iterator;
+}
+
+uint Interpreter::getTimeout(){
+ uint timeout =csolver->getSatSolverTimeout();
+ return timeout == (uint)NOTIMEOUT? 1000: timeout;
+}
+
+int Interpreter::solve(){
+ dumpFooter();
+ int result = IS_INDETER;
+ char buffer [512];
+ if( output.is_open()){
+ output.close();
+ }
+ compileRunCommand(buffer, sizeof(buffer));
+ int status = system(buffer);
+ if (status == 0 || status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
+ //Read data in from results file
+ result = getResult();
+ } else {
+ model_print("Error in running command<returned %d>: %s\n", status, buffer);
+ exit(-1);
+ }
+ return result;
+}
+
+string Interpreter::encodeConstraint(BooleanEdge c){
+ Boolean *constraint = c.getBoolean();
+ string res;
+ switch(constraint->type){
+ case LOGICOP:{
+ res = encodeBooleanLogic((BooleanLogic *) constraint);
+ break;
+ }
+ case PREDICATEOP:{
+ res = encodePredicate((BooleanPredicate *) constraint);
+ break;
+ }
+ case BOOLEANVAR:{
+ res = encodeBooleanVar( (BooleanVar *) constraint);
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+ if(c.isNegated()){
+ return negateConstraint(res);
+ }
+ return res;
+}
+
+string Interpreter::encodePredicate( BooleanPredicate *bp){
+ switch (bp->predicate->type) {
+ case TABLEPRED:
+ ASSERT(0);
+ case OPERATORPRED:
+ return encodeOperatorPredicate(bp);
+ default:
+ ASSERT(0);
+ }
+}
+
+string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
+ PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
+ ASSERT(constraint->inputs.getSize() == 2);
+ string str;
+ Element *elem0 = constraint->inputs.get(0);
+ ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
+ ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0);
+ if(elem0->type == ELEMFUNCRETURN){
+ str += processElementFunction((ElementFunction *) elem0, elemSig1);
+ }
+ Element *elem1 = constraint->inputs.get(1);
+ ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
+ ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1);
+ if(elem1->type == ELEMFUNCRETURN){
+ str += processElementFunction((ElementFunction *) elem1, elemSig2);
+ }
+ str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
+ return str;
+}
+
+void Interpreter::writeToFile(string str){
+ if(!str.empty()){
+ output << str << endl;
+ }
+}
+
+bool Interpreter::getBooleanValue(Boolean *b){
+ return (bool)sigEnc.getValue(b);
+}
+
+uint64_t Interpreter::getValue(Element * element){
+ return (uint64_t)sigEnc.getValue(element);
+}
+
--- /dev/null
+#ifndef INTERPRETER_H
+#define INTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "signature.h"
+#include <iostream>
+#include <fstream>
+using namespace std;
+
+class Interpreter{
+public:
+ Interpreter(CSolver *solver);
+ void encode();
+ int solve();
+ void writeToFile(string str);
+ uint64_t getValue(Element *element);
+ bool getBooleanValue(Boolean *element);
+ virtual ValuedSignature *getBooleanSignature(uint id) = 0;
+ virtual ValuedSignature *getElementSignature(uint id, Signature *ssig) = 0;
+ virtual Signature *getSetSignature(uint id, Set *set) = 0;
+ virtual ~Interpreter();
+protected:
+ virtual void dumpFooter() = 0;
+ virtual void dumpHeader() = 0;
+ uint getTimeout();
+ virtual void compileRunCommand(char * command, size_t size) = 0;
+ string encodeConstraint(BooleanEdge constraint);
+ virtual int getResult() = 0;
+ virtual string negateConstraint(string constr) = 0;
+ virtual void dumpAllConstraints(Vector<char *> &facts) = 0;
+ virtual string encodeBooleanLogic( BooleanLogic *bl) = 0;
+ virtual string encodeBooleanVar( BooleanVar *bv) = 0;
+ string encodePredicate( BooleanPredicate *bp);
+ string encodeOperatorPredicate(BooleanPredicate *constraint);
+ virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature) = 0;
+ virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) = 0;
+ CSolver *csolver;
+ SignatureEnc sigEnc;
+ ofstream output;
+};
+
+#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: smtsolvers.cc
+ * Author: hamed
+ *
+ * Created on February 21, 2019, 12:26 PM
+ */
+
+#include "mathsatinterpreter.h"
+#include "solver_interface.h"
+
+MathSATInterpreter::MathSATInterpreter(CSolver *solver):
+ SMTInterpreter(solver)
+{
+}
+
+void MathSATInterpreter::compileRunCommand(char * command , size_t size){
+ snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+}
+
+MathSATInterpreter::~MathSATInterpreter(){
+}
+
+int MathSATInterpreter::getResult(){
+ ifstream input(SMTSOLUTIONFILE, ios::in);
+ string line;
+ while(getline(input, line)){
+ if(line.find("unsat")!= line.npos){
+ return IS_UNSAT;
+ }
+ if(line.find("(") != line.npos){
+ char cline [line.size()+1];
+ strcpy ( cline, line.c_str() );
+ char valuestr [512];
+ uint id;
+ if (2 == sscanf(cline,"%*[^0123456789]%u%*[^0123456789]%s", &id, valuestr)){
+ uint value;
+ if (strcmp (valuestr, "true)") == 0 ){
+ value =1;
+ }else if (strcmp(valuestr, "false)") == 0){
+ value = 0;
+ }else {
+ ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
+ }
+
+ model_print("Signature%u = %u\n", id, value);
+ sigEnc.setValue(id, value);
+ } else {
+ ASSERT(0);
+ }
+ }
+ }
+ return IS_SAT;
+}
\ No newline at end of file
--- /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: mathsatinterpreter.h
+ * Author: hamed
+ *
+ * Created on February 21, 2019, 12:26 PM
+ */
+
+#ifndef MATHSATINTERPRETER_H
+#define MATHSATINTERPRETER_H
+
+#include "smtinterpreter.h"
+
+
+class MathSATInterpreter: public SMTInterpreter{
+public:
+ MathSATInterpreter(CSolver *solver);
+ virtual ~MathSATInterpreter();
+protected:
+ virtual void compileRunCommand(char * command , size_t size);
+ virtual int getResult();
+};
+
+
+#endif /* SMTSOLVERS_H */
+
--- /dev/null
+#include "signature.h"
+#include "set.h"
+
+ValuedSignature::ValuedSignature(uint id):
+ Signature(id),
+ value(-1)
+{
+}
+
+int ValuedSignature::getValue(){
+ ASSERT(value != -1);
+ return value;
+}
+
+string Signature::operator+(const string& str){
+ return toString() + str;
+}
+
+string operator+(const string& str, const Signature& sig){
+ return str + sig.toString();
+}
--- /dev/null
+#ifndef SIGNATURE_H
+#define SIGNATURE_H
+#include <string>
+#include <iostream>
+#include "classlist.h"
+using namespace std;
+
+class Signature{
+public:
+ Signature(uint _id):id(_id){}
+ string operator+(const string& s);
+ virtual string toString() const = 0;
+ virtual string getAbsSignature() const =0;
+ virtual string getSignature() const =0;
+ virtual ~Signature(){}
+protected:
+ uint id;
+};
+
+class ValuedSignature: public Signature{
+public:
+ ValuedSignature(uint id);
+ int getValue();
+ void setValue(int v){value = v;}
+protected:
+ int value;
+};
+
+string operator+(const string& str, const Signature& sig);
+
+#endif
--- /dev/null
+#include "signatureenc.h"
+#include "element.h"
+#include "set.h"
+#include "signature.h"
+#include "interpreter.h"
+
+SignatureEnc::SignatureEnc(Interpreter *inter):
+ interpreter(inter),
+ maxValue(0)
+{
+}
+
+SignatureEnc::~SignatureEnc(){
+ for(uint i=0; i<signatures.getSize(); i++){
+ Signature *s = signatures.get(i);
+ delete s;
+ }
+}
+
+void SignatureEnc::updateMaxValue(Set *set){
+ for(uint i=0; i< set->getSize(); i++){
+ if(set->getElement(i) > maxValue){
+ maxValue = set->getElement(i);
+ }
+ }
+}
+
+ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
+ ValuedSignature *bsig = (ValuedSignature *)encoded.get((void *)bvar);
+ if(bsig == NULL){
+ bsig = interpreter->getBooleanSignature(getUniqueSigID());
+ encoded.put(bvar, bsig);
+ signatures.push(bsig);
+ interpreter->writeToFile(bsig->getSignature());
+ }
+ return bsig;
+}
+
+ValuedSignature *SignatureEnc::getElementSignature(Element *element){
+ ValuedSignature *esig = (ValuedSignature *)encoded.get((void *)element);
+ if(esig == NULL){
+ Set *set = element->getRange();
+ Signature *ssig = (Signature *)encoded.get((void *)set);
+ if(ssig == NULL){
+ ssig = interpreter->getSetSignature(getUniqueSigID(), set);
+ encoded.put(set, ssig);
+ signatures.push(ssig);
+ interpreter->writeToFile(ssig->getSignature());
+ updateMaxValue(set);
+ }
+ esig = interpreter->getElementSignature(getUniqueSigID(), ssig);
+ encoded.put(element, esig);
+ signatures.push(esig);
+ interpreter->writeToFile(esig->getSignature());
+
+ }
+ return esig;
+}
+
+void SignatureEnc::setValue(uint id, uint value){
+ ValuedSignature *sig = getValuedSignature(id);
+ ASSERT(sig != NULL);
+ sig->setValue(value);
+}
+
+int SignatureEnc::getValue(void *astnode){
+ ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
+ ASSERT(sig != NULL);
+ return sig->getValue();
+}
--- /dev/null
+#ifndef SIGNATUREENC_H
+#define SIGNATUREENC_H
+
+#include "classlist.h"
+#include "structs.h"
+#include "cppvector.h"
+
+class SignatureEnc {
+public:
+ SignatureEnc(Interpreter *_interpreter);
+ ~SignatureEnc();
+ void setValue(uint id, uint value);
+ ValuedSignature *getElementSignature(Element *element);
+ ValuedSignature *getBooleanSignature(Boolean *bvar);
+ int getValue(void *astnode);
+ uint64_t getMaxValue(){ return maxValue;}
+private:
+ ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
+ uint getUniqueSigID(){return signatures.getSize() +1;}
+ void updateMaxValue(Set *set);
+ CloneMap encoded;
+ Vector<Signature*> signatures;
+ Interpreter *interpreter;
+ uint64_t maxValue;
+};
+#endif
--- /dev/null
+#include "smtinterpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+#include "cppvector.h"
+#include "smtsig.h"
+
+using namespace std;
+
+SMTInterpreter::SMTInterpreter(CSolver *_solver):
+ Interpreter(_solver)
+{
+ output.open(SMTFILENAME);
+ if(!output.is_open()){
+ model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
+ exit(-1);
+ }
+}
+
+SMTInterpreter::~SMTInterpreter(){
+ if(output.is_open()){
+ output.close();
+ }
+}
+
+
+ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
+ return new SMTBoolSig(id);
+}
+
+ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
+ return new SMTElementSig(id, (SMTSetSig *)ssig);
+}
+
+Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
+ return new SMTSetSig(id, set);
+}
+
+void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts){
+ for(uint i=0; i< facts.getSize(); i++){
+ char *cstr = facts.get(i);
+ writeToFile("(assert " + string(cstr) + ")");
+ }
+}
+
+void SMTInterpreter::extractValue(char *idline, char *valueline){
+ uint id;
+ if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
+ char valuestr [512];
+ ASSERT(1 == sscanf(valueline,"%s)", valuestr));
+ uint value;
+ if (strcmp (valuestr, "true)") == 0 ){
+ value =1;
+ }else if (strcmp(valuestr, "false)") == 0){
+ value = 0;
+ }else {
+ ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
+ }
+
+ model_print("Signature%u = %u\n", id, value);
+ sigEnc.setValue(id, value);
+ } else {
+ ASSERT(0);
+ }
+}
+
+int SMTInterpreter::getResult(){
+ ifstream input(SMTSOLUTIONFILE, ios::in);
+ string line;
+ while(getline(input, line)){
+ if(line.find("unsat")!= line.npos){
+ return IS_UNSAT;
+ }
+ if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
+ string valueline;
+ ASSERT(getline(input, valueline));
+ char cline [line.size()+1];
+ strcpy ( cline, line.c_str() );
+ char vline [valueline.size()+1];
+ strcpy ( vline, valueline.c_str() );
+ extractValue(cline, vline);
+ }
+ }
+ return IS_SAT;
+}
+
+void SMTInterpreter::dumpFooter(){
+ output << "(check-sat)" << endl;
+ output << "(get-model)" << endl;
+}
+
+void SMTInterpreter::dumpHeader(){
+}
+
+void SMTInterpreter::compileRunCommand(char * command, size_t size){
+ snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+}
+
+string SMTInterpreter::negateConstraint(string constr){
+ return "( not " + constr + " )";
+}
+
+string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+ uint size = bl->inputs.getSize();
+ string array[size];
+ for (uint i = 0; i < size; i++)
+ array[i] = encodeConstraint(bl->inputs.get(i));
+ string op;
+ switch (bl->op){
+ case SATC_OR:
+ op = "or";
+ break;
+ case SATC_AND:
+ op = "and";
+ break;
+ case SATC_NOT:
+ op = "not";
+ break;
+ case SATC_IMPLIES:
+ op = "=>";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
+ }
+ switch (bl->op) {
+ case SATC_XOR:
+ case SATC_OR:
+ case SATC_AND:{
+ ASSERT(size >= 2);
+ string res = array[0];
+ for( uint i=1; i< size; i++){
+ res = "( " + op + " " + res + " " + array[i] + " )";
+ }
+ return res;
+ }
+ case SATC_NOT:{
+ return "( not " + array[0] + " )";
+ }
+ case SATC_IMPLIES:
+ return "( " + op + " " + array[0] + " " + array[1] + " )";
+ case SATC_IFF:
+ default:
+ ASSERT(0);
+
+ }
+}
+
+string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
+ ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+ return *boolSig + "";
+}
+
+string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+ FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
+ uint numDomains = elemFunc->inputs.getSize();
+ ASSERT(numDomains > 1);
+ ValuedSignature *inputs[numDomains];
+ string result;
+ for (uint i = 0; i < numDomains; i++) {
+ Element *elem = elemFunc->inputs.get(i);
+ inputs[i] = sigEnc.getElementSignature(elem);
+ if(elem->type == ELEMFUNCRETURN){
+ result += processElementFunction((ElementFunction *) elem, inputs[i]);
+ }
+ }
+ string op;
+ switch(function->op){
+ case SATC_ADD:
+ op = "+";
+ break;
+ case SATC_SUB:
+ op = "-";
+ break;
+ default:
+ ASSERT(0);
+ }
+ result += "( = " + *signature;
+ string tmp = "" + *inputs[0];
+ for (uint i = 1; i < numDomains; i++) {
+ tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
+ }
+ result += tmp + " )";
+ return result;
+}
+
+string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+ switch (op) {
+ case SATC_EQUALS:
+ return "( = " + *elemSig1 + " " + *elemSig2 +" )";
+ case SATC_LT:
+ return "( < " + *elemSig1 + " " + *elemSig2 + " )";
+ case SATC_GT:
+ return "(> " + *elemSig1 + " " + *elemSig2 + " )";
+ default:
+ ASSERT(0);
+ }
+}
+
+
--- /dev/null
+#ifndef SMTINTERPRETER_H
+#define SMTINTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "interpreter.h"
+#include <iostream>
+#include <fstream>
+
+#define SMTFILENAME "satune.smt"
+#define SMTSOLUTIONFILE "solution.sol"
+
+class SMTInterpreter: public Interpreter{
+public:
+ SMTInterpreter(CSolver *solver);
+ virtual ValuedSignature *getBooleanSignature(uint id);
+ virtual ValuedSignature *getElementSignature(uint id, Signature *ssig);
+ virtual Signature *getSetSignature(uint id, Set *set);
+ virtual ~SMTInterpreter();
+protected:
+ virtual void dumpFooter();
+ virtual void dumpHeader();
+ virtual void compileRunCommand(char * command , size_t size);
+ virtual int getResult();
+ virtual void dumpAllConstraints(Vector<char *> &facts);
+ virtual string negateConstraint(string constr);
+ virtual string encodeBooleanLogic( BooleanLogic *bl);
+ virtual string encodeBooleanVar( BooleanVar *bv);
+ virtual void extractValue(char *idline, char *valueline);
+ virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
+ virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
+};
+
+#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: smtratinterpreter.cc
+ * Author: hamed
+ *
+ * Created on February 21, 2019, 2:33 PM
+ */
+
+#include "smtratinterpreter.h"
+
+SMTRatInterpreter::SMTRatInterpreter(CSolver *solver):
+ SMTInterpreter(solver)
+{
+}
+
+void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
+ snprintf(command, size, "timeout %u ./smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+}
+
+SMTRatInterpreter::~SMTRatInterpreter(){
+}
--- /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: smtratinterpreter.h
+ * Author: hamed
+ *
+ * Created on February 21, 2019, 2:33 PM
+ */
+
+#ifndef SMTRATINTERPRETER_H
+#define SMTRATINTERPRETER_H
+#include "smtinterpreter.h"
+
+class SMTRatInterpreter: public SMTInterpreter{
+public:
+ SMTRatInterpreter(CSolver *solver);
+ virtual ~SMTRatInterpreter();
+protected:
+ void compileRunCommand(char * command , size_t size);
+};
+
+#endif /* SMTRATINTERPRETER_H */
+
--- /dev/null
+#include "smtsig.h"
+#include "set.h"
+
+SMTBoolSig::SMTBoolSig(uint id):
+ ValuedSignature(id)
+{
+}
+
+string SMTBoolSig::toString() const{
+ return "b" + to_string(id);
+}
+
+string SMTBoolSig::getSignature() const{
+ return "(declare-const b" + to_string(id) + " Bool)";
+}
+
+string SMTBoolSig::getAbsSignature() const{
+ return "";
+}
+
+SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig):
+ ValuedSignature(id),
+ ssig(_ssig)
+{
+}
+
+string SMTElementSig::toString() const{
+ return "e" + to_string(id);
+}
+
+string SMTElementSig::getSignature() const{
+ string str = "(declare-const e" + to_string(id) + " Int)\n";
+ string constraint = ssig->getAbsSignature();
+ size_t start_pos;
+ string placeholder = "$";
+ while((start_pos = constraint.find(placeholder)) != string::npos){
+ constraint.replace(start_pos, placeholder.size(), to_string(id));
+ }
+ //constraint.replace(constraint.begin(), constraint.end(), "$", );
+ str += constraint;
+ return str;
+}
+
+string SMTElementSig::getAbsSignature() const{
+ return "";
+
+}
+
+SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
+ ASSERT(set->getSize() > 0);
+ int min = set->getElement(0), max = set->getElement(set->getSize()-1);
+ Vector<int> holes;
+ int prev = set->getElement(0);
+ for(uint i=1; i< set->getSize(); i++){
+ int curr = set->getElement(i);
+ if(prev != curr -1){
+ for(int j=prev+1; j< curr; j++){
+ holes.push(j);
+ }
+ }
+ prev = curr;
+ }
+ constraint = "(assert (<= e$ " + to_string(max) +"))\n";
+ constraint += "(assert (>= e$ " + to_string(min) +"))\n";
+ for(uint i=0; i< holes.getSize(); i++){
+ constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
+ }
+}
+
+string SMTSetSig::toString() const{
+ return "";
+}
+
+string SMTSetSig::getSignature() const{
+ return "";
+}
+
+string SMTSetSig::getAbsSignature() const{
+ return constraint;
+
+}
--- /dev/null
+#ifndef SMTSIG_H
+#define SMTSIG_H
+#include <string>
+#include <iostream>
+#include "signature.h"
+#include "classlist.h"
+using namespace std;
+
+class SMTBoolSig: public ValuedSignature{
+public:
+ SMTBoolSig(uint id);
+ virtual ~SMTBoolSig(){}
+ virtual string toString() const;
+ virtual string getAbsSignature() const;
+ virtual string getSignature() const;
+};
+
+class SMTSetSig: public Signature{
+public:
+ SMTSetSig(uint id, Set *set);
+ virtual ~SMTSetSig(){}
+ virtual string toString() const;
+ virtual string getAbsSignature() const;
+ virtual string getSignature() const;
+private:
+ string constraint;
+};
+
+class SMTElementSig: public ValuedSignature{
+public:
+ SMTElementSig(uint id, SMTSetSig *ssig);
+ virtual ~SMTElementSig(){}
+ virtual string toString() const;
+ virtual string getAbsSignature() const;
+ virtual string getSignature() const;
+private:
+ SMTSetSig *ssig;
+};
+
+#endif
MKDIR_P = mkdir -p
OBJ_DIR = bin
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) $(wildcard Interpreter/*.cc)
-C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c)
+C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard Interpreter/*.c)
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard Interpreter/*.h)
OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
CFLAGS := -Wall -O0 -g
CXXFLAGS := -std=c++1y -pthread
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IInterpreter
LDFLAGS := -ldl -lrt -rdynamic -g
SHARED := -shared
${MKDIR_P} ${OBJ_DIR}/Backend
${MKDIR_P} ${OBJ_DIR}/Encoders
${MKDIR_P} ${OBJ_DIR}/Serialize
+ ${MKDIR_P} ${OBJ_DIR}/Interpreter
debug: CFLAGS += -DCONFIG_DEBUG
debug: all
#define READBUFFERSIZE 16384
-Deserializer::Deserializer(const char *file) :
+Deserializer::Deserializer(const char *file, InterpreterType itype) :
buffer((char *) ourmalloc(READBUFFERSIZE)),
bufferindex(0),
bufferbytes(0),
if (filedesc < 0) {
exit(-1);
}
+ if(itype != SATUNE){
+ solver->setInterpreter(itype);
+ }
}
Deserializer::~Deserializer() {
myread(&b, sizeof(BooleanVar *));
bool istrue;
myread(&istrue, sizeof(bool));
- map.put(b, istrue?solver->getBooleanTrue().getBoolean():
- solver->getBooleanFalse().getBoolean());
+ map.put(b, istrue ? solver->getBooleanTrue().getBoolean() :
+ solver->getBooleanFalse().getBoolean());
}
void Deserializer::deserializeBooleanOrder() {
*/
class Deserializer {
public:
- Deserializer(const char *file);
+ Deserializer(const char *file, InterpreterType itype = SATUNE);
CSolver *deserialize();
virtual ~Deserializer();
private:
--- /dev/null
+#include "csolver.h"
+#include "comptuner.h"
+#include "searchtuner.h"
+
+int main(int argc, char **argv) {
+ if (argc < 2) {
+ printf("You should specify number of runs\n");
+ exit(-1);
+ }
+ uint numruns;
+ sscanf(argv[1], "%u", &numruns);
+
+ CompTuner *multituner = new CompTuner(0, 0);
+ multituner->readData(numruns);
+ multituner->findBestThreeTuners();
+ delete multituner;
+ return 0;
+}
--- /dev/null
+#include "csolver.h"
+
+
+InterpreterType getInterpreterType(char * itype){
+ if(strcmp (itype,"--alloy") == 0){
+ return ALLOY;
+ } else if(strcmp (itype,"--z3") == 0){
+ return Z3;
+ } else if(strcmp (itype,"--smtrat") == 0){
+ return SMTRAT;
+ } else if(strcmp (itype,"--mathsat") == 0){
+ return MATHSAT;
+ } else {
+ printf("Unknown interpreter type: %s\n", itype);
+ printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
+ exit(-1);
+ }
+}
+
+int main(int argc, char **argv) {
+ printf("%d\n", argc);
+ if (argc != 2 && argc != 3) {
+ printf("You only specify the name of the file ...\n");
+ printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
+ exit(-1);
+ }
+ CSolver *solver;
+ if(argc == 3){
+ solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
+ } else {
+ solver = CSolver::deserialize(argv[1]);
+ }
+ int value = solver->solve();
+ if (value == 1) {
+ printf("%s is SAT\n", argv[1]);
+ } else {
+ printf("%s is UNSAT\n", argv[1]);
+ }
+ delete solver;
+ return 1;
+
+}
+++ /dev/null
-#include "csolver.h"
-
-
-int main(int argc, char **argv) {
- if (argc != 2) {
- printf("You only specify the name of the file ...");
- exit(-1);
- }
- CSolver *solver = CSolver::deserialize(argv[1]);
- solver->printConstraints();
- delete solver;
- return 1;
-
-}
--- /dev/null
+#include "csolver.h"
+#include "searchtuner.h"
+#include <stdlib.h>
+#include <iostream>
+#include <fstream>
+
+int main(int argc, char **argv) {
+ if (argc != 5) {
+ printf("You only specify the name of the file ...");
+ exit(-1);
+ }
+ char buffer[512];
+ CSolver *solver = CSolver::deserialize(argv[1]);
+ uint timeout;
+ sscanf(argv[2], "%u", &timeout);
+ SearchTuner *tuner = new SearchTuner(argv[3]);
+ solver->setTuner(tuner);
+ solver->setSatSolverTimeout(timeout);
+ int sat = solver->solve();
+ long long metric = solver->getElapsedTime();
+ ofstream myfile;
+ myfile.open (argv[4], ios::out | ios::trunc);
+ myfile << metric << endl;
+ myfile << sat << endl;
+ myfile.close();
+ //serialize out the tuner we used
+ snprintf(buffer, sizeof(buffer), "%sused", argv[3]);
+ tuner->serializeUsed(buffer);
+
+ delete solver;
+ delete tuner;
+ return 0;
+}
--- /dev/null
+#include "csolver.h"
+#include "comptuner.h"
+#include "searchtuner.h"
+
+int main(int argc, char **argv) {
+ if (argc < 2) {
+ printf("You should specify a tuner: %s <best.tuner>\n", argv[0]);
+ exit(-1);
+ }
+
+ SearchTuner *tuner = new SearchTuner(argv[1]);
+ tuner->print();
+ delete tuner;
+ return 0;
+}
#!/bin/bash
+export CLASSPATH=../bin/original.jar:.:$CLASSPATH
export LD_LIBRARY_PATH=../bin
# For Mac OSX
export DYLD_LIBRARY_PATH=../bin
# For sat_solver
export PATH=.:$PATH
-
+echo $@
$@
--- /dev/null
+#include "csolver.h"
+#include "searchtuner.h"
+#include "kmeanstuner.h"
+#include "satuner.h"
+#include "comptuner.h"
+#include "randomtuner.h"
+
+void printKnownTunerTypes(){
+ printf("Known Tuner Types:\nRandom Tuner=1\nComp Tuner=2\nKmeans Tuner=3\nSimulated Annealing Tuner=4\n");
+}
+
+BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout){
+ switch(tunertype){
+ case 1: return new RandomTuner(budget, timeout);
+ case 2: return new CompTuner(budget, timeout);
+ case 3: return new KMeansTuner(budget, rounds, timeout);
+ case 4: return new SATuner(budget, timeout);
+ default:
+ printf("Tuner type %u is unknown\n", tunertype);
+ printKnownTunerTypes();
+ exit(-1);
+ }
+
+}
+
+int main(int argc, char **argv) {
+ if (argc < 8) {
+ printf("You should specify: %s TunerType budget rounds timeout problemfilenames - tunerfilenames\n", argv[0]);
+ printKnownTunerTypes();
+ exit(-1);
+ }
+ uint tunertype;
+ uint budget;
+ uint rounds;
+ uint timeout;
+ sscanf(argv[1], "%u", &tunertype);
+ sscanf(argv[2], "%u", &budget);
+ sscanf(argv[3], "%u", &rounds);
+ sscanf(argv[4], "%u", &timeout);
+
+ BasicTuner *multituner = createTuner(tunertype, budget, rounds, timeout);
+ bool tunerfiles = false;
+ for (int i = 5; i < argc; i++) {
+ if (!tunerfiles) {
+ if (argv[i][0] == '-' && argv[i][1] == 0)
+ tunerfiles = true;
+ else
+ multituner->addProblem(argv[i]);
+ } else
+ multituner->addTuner(new SearchTuner(argv[i], true )); //add settings to usedsettigs
+ }
+
+ if (!tunerfiles) {
+ printf("You should specify %s budget rounds timeout problemfilenames - tunerfilenames", argv[0]);
+ exit(-1);
+ }
+
+ multituner->tune();
+ delete multituner;
+ return 0;
+}
--- /dev/null
+#include "csolver.h"
+#include "searchtuner.h"
+#include "tunable.h"
+#include <stdlib.h>
+
+int main(int argc, char **argv) {
+ SearchTuner *elem_bin = new SearchTuner();
+ SearchTuner *elem_onehot = new SearchTuner();
+ SearchTuner *elem_unary = new SearchTuner();
+ elem_bin->setTunable(NAIVEENCODER, &NaiveEncodingDesc, BINARYINDEX);
+ elem_onehot->setTunable(NAIVEENCODER, &NaiveEncodingDesc, ONEHOT);
+ elem_unary->setTunable(NAIVEENCODER, &NaiveEncodingDesc, UNARY);
+
+ elem_bin->serialize("binarytuner.conf");
+ elem_onehot->serialize("onehottuner.conf");
+ elem_unary->serialize("unarytuner.conf");
+ elem_bin->setTunable(ENCODINGGRAPHOPT, &onoff, 1);
+ elem_onehot->setTunable(ENCODINGGRAPHOPT, &onoff, 1);
+ elem_unary->setTunable(ENCODINGGRAPHOPT, &onoff, 1);
+ elem_bin->serialize("circuitbinarytuner.conf");
+ elem_onehot->serialize("circuitonehottuner.conf");
+ elem_unary->serialize("circuitunarytuner.conf");
+ delete elem_bin;
+ delete elem_onehot;
+ delete elem_unary;
+}
--- /dev/null
+#include "csolver.h"
+#include "serializetuner.h"
+#include <stdlib.h>
+#include <iostream>
+#include <fstream>
+
+int main(int argc, char **argv) {
+ if (argc != 5) {
+ printf("You only specify the name of the file ...");
+ exit(-1);
+ }
+ char buffer[512];
+ CSolver *solver = CSolver::deserialize(argv[1]);
+ uint timeout;
+ sscanf(argv[2], "%u", &timeout);
+ SerializeTuner *tuner = new SerializeTuner(argv[3]);
+ solver->setTuner(tuner);
+ solver->setSatSolverTimeout(timeout);
+ int sat = solver->solve();
+ long long metric = solver->getElapsedTime();
+ ofstream myfile;
+ myfile.open (argv[4], ios::out | ios::trunc);
+ myfile << metric << endl;
+ myfile << sat << endl;
+ myfile.close();
+ //serialize out the tuner we used
+ snprintf(buffer, sizeof(buffer), "%sused", argv[3]);
+ tuner->serializeUsed(buffer);
+
+ delete solver;
+ delete tuner;
+ return 0;
+}
budget(_budget), result(UNSETVALUE) {
}
+AutoTuner::~AutoTuner() {}
+
void AutoTuner::addProblem(CSolver *solver) {
solvers.push(solver);
}
return newTuner;
}
-#ifdef STATICENCGEN
-SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner) {
- SearchTuner *newTuner = oldTuner->copyUsed();
- result = newTuner->nextStaticTuner();
- return result==EXIT_FAILURE? newTuner: NULL;
-}
-#endif
-
void AutoTuner::tune() {
SearchTuner *bestTuner = NULL;
double bestScore = DBL_MAX;
double base_temperature = evaluateAll(oldTuner);
double oldScore = base_temperature;
-#ifdef STATICENCGEN
- while(true){
- SearchTuner *newTuner = mutateTuner(oldTuner);
- if(newTuner == NULL)
- return;
- double newScore = evaluateAll(newTuner);
- newTuner->printUsed();
- model_print("Received score %f\n", newScore);
- delete oldTuner;
- oldScore = newScore;
- oldTuner = newTuner;
- }
-#endif
-
for (uint i = 0; i < budget; i++) {
SearchTuner *newTuner = mutateTuner(oldTuner, i);
double newScore = evaluateAll(newTuner);
}
model_print("Best tuner:\n");
bestTuner->print();
- bestTuner->serialize();
+ bestTuner->serialize("TUNER.conf");
model_print("Received score %f\n", bestScore);
if (bestTuner != NULL)
delete bestTuner;
class AutoTuner {
public:
AutoTuner(uint budget);
+ virtual ~AutoTuner();
void addProblem(CSolver *solver);
- void tune();
+ virtual void tune();
CMEMALLOC;
-private:
+protected:
long long evaluate(CSolver *problem, SearchTuner *tuner);
double evaluateAll(SearchTuner *tuner);
SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
-#ifdef STATICENCGEN
- SearchTuner *mutateTuner(SearchTuner *oldTuner);
-#endif
Vector<CSolver *> solvers;
uint budget;
int result;
--- /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: basictuner.cc
+ * Author: hamed
+ *
+ * Created on December 17, 2018, 2:02 PM
+ */
+
+#include "basictuner.h"
+#include "common.h"
+#include "csolver.h"
+#include "searchtuner.h"
+#include <stdlib.h>
+#include <string.h>
+#include <iostream>
+#include <fstream>
+
+Problem::Problem(const char *_problem) :
+ problemnumber(-1),
+ result(TUNERUNSETVALUE),
+ besttime(LLONG_MAX)
+{
+ uint len = strlen(_problem);
+ problem = (char *) ourmalloc(len + 1);
+ memcpy(problem, _problem, len + 1);
+}
+
+Problem::~Problem() {
+ ourfree(problem);
+}
+
+void TunerRecord::setTime(Problem *problem, long long time) {
+ timetaken.put(problem, time);
+}
+
+void TunerRecord::print(){
+ model_print("*************TUNER NUMBER=%d***********\n", tunernumber);
+ tuner->print();
+ model_print("&&&&&&&&&&&&&USED SETTINGS &&&&&&&&&&&&\n");
+ tuner->printUsed();
+ model_print("\n");
+}
+
+void TunerRecord::printProblemsInfo(){
+ for (uint j = 0; j < problems.getSize(); j++) {
+ Problem *problem = problems.get(j);
+ model_print("Problem %s\n", problem->getProblem());
+ model_print("Time = %lld\n", getTime(problem));
+ }
+}
+
+long long TunerRecord::getTime(Problem *problem) {
+ if (timetaken.contains(problem))
+ return timetaken.get(problem);
+ else return -1;
+}
+
+TunerRecord *TunerRecord::changeTuner(SearchTuner *_newtuner) {
+ TunerRecord *tr = new TunerRecord(_newtuner);
+ for (uint i = 0; i < problems.getSize(); i++) {
+ tr->problems.push(problems.get(i));
+ }
+ return tr;
+}
+
+
+BasicTuner::BasicTuner(uint _budget, uint _timeout) :
+ budget(_budget), timeout(_timeout), execnum(0){
+}
+
+BasicTuner::~BasicTuner() {
+ for (uint i = 0; i < problems.getSize(); i++)
+ ourfree(problems.get(i));
+ for (uint i = 0; i < allTuners.getSize(); i++)
+ delete allTuners.get(i);
+}
+
+void BasicTuner::addProblem(const char *filename) {
+ Problem *p = new Problem(filename);
+ p->setProblemNumber(problems.getSize());
+ problems.push(p);
+}
+
+void BasicTuner::printData() {
+ model_print("*********** DATA DUMP ***********\n");
+ for (uint i = 0; i < allTuners.getSize(); i++) {
+ TunerRecord *tuner = allTuners.get(i);
+ SearchTuner *stun = tuner->getTuner();
+ model_print("Tuner %u\n", i);
+ stun->print();
+ model_print("----------------------------------\n\n\n");
+ for (uint j = 0; j < tuner->problemsSize(); j++) {
+ Problem *problem = tuner->getProblem(j);
+ model_print("Problem %s\n", problem->getProblem());
+ model_print("Time = %lld\n", tuner->getTime(problem));
+ }
+ }
+}
+
+bool BasicTuner::tunerExists(TunerRecord *tunerec){
+ SearchTuner *tuner = tunerec->getTuner();
+ for(uint i=0; i< explored.getSize(); i++){
+ if(explored.get(i)->getTuner()->equalUsed(tuner)){
+ model_print("************Tuner <%d> is replicate of Tuner <%d>\n", tunerec->getTunerNumber(), explored.get(i)->getTunerNumber());
+ return true;
+ }
+ }
+ return false;
+}
+
+void BasicTuner::addTuner(SearchTuner *tuner) {
+ TunerRecord *t = new TunerRecord(tuner);
+ tuners.push(t);
+ t->setTunerNumber( allTuners.getSize() );
+ allTuners.push(t);
+}
+
+long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
+ char buffer[512];
+ {
+ snprintf(buffer, sizeof(buffer), "problem%u", execnum);
+
+ ofstream myfile;
+ myfile.open (buffer, ios::out);
+
+
+ if (myfile.is_open()) {
+ myfile << problem->getProblem() << endl;
+ myfile << problem->getProblemNumber() << endl;
+ myfile.close();
+ }
+ }
+
+ {
+ snprintf(buffer, sizeof(buffer), "tunernum%u", execnum);
+
+ ofstream myfile;
+ myfile.open (buffer, ios::out);
+
+
+ if (myfile.is_open()) {
+ myfile << tuner->getTunerNumber() << endl;
+ myfile.close();
+ }
+ }
+
+ //Write out the tuner
+ snprintf(buffer, sizeof(buffer), "tuner%u", execnum);
+ tuner->getTuner()->serialize(buffer);
+
+ //compute timeout
+ uint timeinsecs = problem->getBestTime() / NANOSEC;
+ uint adaptive = (timeinsecs > 30) ? timeinsecs * 5 : 150;
+ uint maxtime = (adaptive < timeout) ? adaptive : timeout;
+
+ //Do run
+ snprintf(buffer, sizeof(buffer), "./run.sh deserializerun %s %u tuner%u result%u > log%u", problem->getProblem(), maxtime, execnum, execnum, execnum);
+ int status = system(buffer);
+
+ long long metric = -1;
+ int sat = IS_INDETER;
+
+ if (status == 0) {
+ //Read data in from results file
+ snprintf(buffer, sizeof(buffer), "result%u", execnum);
+
+ ifstream myfile;
+ myfile.open (buffer, ios::in);
+
+
+ if (myfile.is_open()) {
+ myfile >> metric;
+ myfile >> sat;
+ myfile.close();
+ }
+ updateTimeout(problem, metric);
+ snprintf(buffer, sizeof(buffer), "tuner%uused", execnum);
+ tuner->getTuner()->addUsed(buffer);
+ }
+ //Increment execution count
+ execnum++;
+
+ if (problem->getResult() == TUNERUNSETVALUE && sat != IS_INDETER) {
+ problem->setResult( sat );
+ } else if (problem->getResult() != sat && sat != IS_INDETER) {
+ model_print("******** Result has changed ********\n");
+ }
+ if (sat == IS_INDETER && metric != -1) {//The case when we have a timeout
+ metric = -1;
+ }
+ return metric;
+}
+
+SearchTuner *BasicTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
+ SearchTuner *newTuner = oldTuner->copyUsed();
+ uint numSettings = oldTuner->getSize();
+ uint settingsToMutate = (uint)(AUTOTUNERFACTOR * (((double)numSettings) * (budget - k)) / (budget));
+ if (settingsToMutate < 1)
+ settingsToMutate = 1;
+ model_print("Mutating %u settings\n", settingsToMutate);
+ while (settingsToMutate-- != 0) {
+ newTuner->randomMutate();
+ }
+ return newTuner;
+}
+
+int BasicTuner::subTunerIndex(SearchTuner *newTuner){
+ for (uint i=0; i< explored.getSize(); i++){
+ SearchTuner *tuner = explored.get(i)->getTuner();
+ if(tuner->isSubTunerof(newTuner)){
+ return i;
+ }
+ }
+ return -1;
+}
+
+
+void BasicTuner::updateTimeout(Problem *problem, long long metric) {
+ if (metric < problem->getBestTime()) {
+ problem->setBestTime( metric );
+ }
+}
--- /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: basictuner.h
+ * Author: hamed
+ *
+ * Created on December 17, 2018, 2:02 PM
+ */
+
+#ifndef BASICTUNER_H
+#define BASICTUNER_H
+#include "mymemory.h"
+#include "classlist.h"
+#include "cppvector.h"
+#include "hashtable.h"
+
+#define TUNERUNSETVALUE -1
+#define AUTOTUNERFACTOR 0.3
+
+class Problem {
+public:
+ Problem(const char *problem);
+ char *getProblem() {return problem;}
+ inline int getResult(){return result;}
+ inline int getProblemNumber(){return problemnumber;}
+ inline void setResult(int res){result = res;}
+ inline void setProblemNumber(int probNum){problemnumber = probNum;}
+ inline long long getBestTime() {return besttime ;}
+ inline void setBestTime(long long time) {besttime = time;}
+ ~Problem();
+ CMEMALLOC;
+private:
+ int problemnumber;
+ int result;
+ char *problem;
+ long long besttime;
+};
+
+class TunerRecord {
+public:
+ TunerRecord(SearchTuner *_tuner) : tuner(_tuner), tunernumber(-1), isduplicate(false) {}
+ TunerRecord(SearchTuner *_tuner, int _tunernumber) : tuner(_tuner), tunernumber(_tunernumber), isduplicate(false) {}
+ SearchTuner *getTuner() {return tuner;}
+ void inline addProblem(Problem * problem){problems.push(problem);}
+ TunerRecord *changeTuner(SearchTuner *_newtuner);
+ void updateTuner(SearchTuner *_newtuner) {tuner = _newtuner;}
+ long long getTime(Problem *problem);
+ void setTime(Problem *problem, long long time);
+ inline void setTunerNumber(int numb){tunernumber = numb;}
+ inline int getTunerNumber(){return tunernumber;}
+ inline uint problemsSize() {return problems.getSize();}
+ inline void setDuplicate(bool _duplicate) { isduplicate = _duplicate;}
+ inline bool isDuplicate() {return isduplicate;}
+ inline Problem *getProblem(uint index){return problems.get(index);}
+ void print();
+ void printProblemsInfo();
+ CMEMALLOC;
+private:
+ SearchTuner *tuner;
+ Vector<Problem *> problems;
+ Hashtable<Problem *, long long, uint64_t> timetaken;
+ int tunernumber;
+ friend void clearVector(Vector<TunerRecord *> *tunerV);
+ bool isduplicate;
+};
+
+class BasicTuner {
+public:
+ BasicTuner(uint _budget, uint _timeout);
+ void addProblem(const char *filename);
+ void addTuner(SearchTuner *tuner);
+ void printData();
+ virtual ~BasicTuner();
+ virtual void tune() = 0;
+ CMEMALLOC;
+protected:
+ long long evaluate(Problem *problem, TunerRecord *tuner);
+ /**
+ * returns the index of the tuner which is subtune of
+ * the newTuner
+ * @param newTuner
+ * @return
+ */
+ int subTunerIndex(SearchTuner *newTuner);
+ bool tunerExists(TunerRecord *tunerRec);
+ SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
+ void updateTimeout(Problem *problem, long long metric);
+ Vector<TunerRecord *> allTuners;
+ Vector<TunerRecord *> explored;
+ Vector<Problem *> problems;
+ Vector<TunerRecord *> tuners;
+ uint budget;
+ uint timeout;
+ int execnum;
+};
+
+#endif /* BASICTUNER_H */
+
--- /dev/null
+#include "comptuner.h"
+#include <float.h>
+#include <math.h>
+#include "searchtuner.h"
+#include <iostream>
+#include <fstream>
+#include "solver_interface.h"
+
+CompTuner::CompTuner(uint _budget, uint _timeout) :
+ BasicTuner(_budget, _timeout)
+{
+}
+
+CompTuner::~CompTuner(){
+
+}
+
+void CompTuner::findBestThreeTuners() {
+ if (allTuners.getSize() < 3) {
+ printData();
+ return;
+ }
+ TunerRecord *bestTuners[3];
+ double score = DBL_MAX;
+ for (uint i = 0; i < allTuners.getSize() - 2; i++) {
+ for (uint j = i + 1; j < allTuners.getSize() - 1; j++) {
+ for (uint k = j + 1; k < allTuners.getSize(); k++) {
+ TunerRecord *tuner1 = allTuners.get(i);
+ TunerRecord *tuner2 = allTuners.get(j);
+ TunerRecord *tuner3 = allTuners.get(k);
+ double mintimes[problems.getSize()];
+ for (uint l = 0; l < problems.getSize(); l++) {
+ Problem *problem = problems.get(l);
+ mintimes[l] = pow(min(tuner1->getTime(problem), tuner2->getTime(problem), tuner3->getTime(problem)), (double)1 / problems.getSize());
+ }
+ double result = 1;
+ for (uint l = 0; l < problems.getSize(); l++) {
+ result *= mintimes[l];
+ }
+ if (result < score) {
+ score = result;
+ bestTuners[0] = tuner1;
+ bestTuners[1] = tuner2;
+ bestTuners[2] = tuner3;
+ }
+ }
+ }
+ }
+ model_print("Best 3 tuners:\n");
+ for (uint i = 0; i < 3; i++) {
+ TunerRecord *tuner = bestTuners[i];
+ SearchTuner *stun = tuner->getTuner();
+ char buffer[512];
+ snprintf(buffer, sizeof(buffer), "best%u.tuner", i);
+ stun->serialize(buffer);
+ model_print("Tuner %u\n", tuner->getTunerNumber());
+ stun->print();
+ tuner->printProblemsInfo();
+ model_print("----------------------------------\n\n\n");
+ }
+}
+
+void CompTuner::readData(uint numRuns) {
+ for (uint i = 0; i < numRuns; i++) {
+ ifstream myfile;
+ char buffer[512];
+ uint tunernumber;
+ snprintf(buffer, sizeof(buffer), "tunernum%u", i);
+ myfile.open (buffer, ios::in);
+ myfile >> tunernumber;
+ myfile.close();
+ if (allTuners.getSize() <= tunernumber)
+ allTuners.setSize(tunernumber + 1);
+ if (allTuners.get(tunernumber) == NULL) {
+ snprintf(buffer, sizeof(buffer), "tuner%u", i);
+ allTuners.set(tunernumber, new TunerRecord(new SearchTuner(buffer), tunernumber));
+ }
+ //Add any new used records
+ snprintf(buffer, sizeof(buffer), "tuner%uused", i);
+ TunerRecord *tuner = allTuners.get(tunernumber);
+ tuner->getTuner()->addUsed(buffer);
+
+ char problemname[512];
+ uint problemnumber;
+ snprintf(buffer, sizeof(buffer), "problem%u", i);
+ myfile.open(buffer, ios::in);
+ myfile.getline(problemname, sizeof(problemname));
+ myfile >> problemnumber;
+ myfile.close();
+ if (problems.getSize() <= problemnumber)
+ problems.setSize(problemnumber + 1);
+ if (problems.get(problemnumber) == NULL)
+ problems.set(problemnumber, new Problem(problemname));
+ Problem *problem = problems.get(problemnumber);
+ long long metric = -1;
+ int sat = IS_INDETER;
+ //Read data in from results file
+ snprintf(buffer, sizeof(buffer), "result%u", i);
+
+ myfile.open (buffer, ios::in);
+
+
+ if (myfile.is_open()) {
+ myfile >> metric;
+ myfile >> sat;
+ myfile.close();
+ }
+ if (problem->getResult() == TUNERUNSETVALUE && sat != IS_INDETER) {
+ problem->setResult(sat);
+ } else if (problem->getResult() != sat && sat != IS_INDETER) {
+ model_print("******** Result has changed ********\n");
+ }
+
+ if (metric != -1) {
+ if (tuner->getTime(problem) == -1)
+ tuner->addProblem(problem);
+ tuner->setTime(problem, metric);
+ }
+
+ }
+
+}
+
+void CompTuner::tune() {
+ Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
+ for (uint b = 0; b < budget; b++) {
+ model_print("Round %u of %u\n", b, budget);
+ Hashtable<TunerRecord *, int, uint64_t> scores;
+ Vector<Vector<TunerRecord *> *> allplaces;
+ for(uint ii=0; ii< problems.getSize(); ii++){
+ allplaces.push(new Vector<TunerRecord *>());
+ }
+ for (uint j = 0; j < tunerV->getSize(); j++) {
+ TunerRecord *tuner = tunerV->get(j);
+
+ for (uint i = 0; i < problems.getSize(); i++) {
+ Vector<TunerRecord *> *places = allplaces.get(i);
+ Problem *problem = problems.get(i);
+ long long metric = tuner->getTime(problem);
+ if (metric == -1) {
+ metric = evaluate(problem, tuner);
+ if (tuner->getTime(problem) == -1) {
+ tuner->addProblem(problem);
+ }
+ model_print("%u.Problem<%s>\tTuner<%p, %d>\tMetric<%lld>\n", i, problem->getProblem(),tuner, tuner->getTunerNumber(), metric);
+ model_print("*****************************\n");
+ if (metric != -1)
+ tuner->setTime(problem, metric);
+ else
+ tuner->setTime(problem, -2);
+
+ if(tunerExists(tuner)){
+ //Solving the problem and noticing the tuner
+ //already exists
+ tuner->setDuplicate(true);
+ break;
+ }
+ }
+ if (metric >= 0) {
+ uint k = 0;
+ for (; k < places->getSize(); k++) {
+ if (metric < places->get(k)->getTime(problem))
+ break;
+ }
+ model_print("place[%u]=Tuner<%p,%d>\n", k, tuner, tuner->getTunerNumber());
+ places->insertAt(k, tuner);
+ }
+ }
+ }
+ for(uint ii=0; ii < problems.getSize(); ii++){
+ Problem *problem = problems.get(ii);
+ Vector<TunerRecord *> *places = allplaces.get(ii);
+ int points = 9;
+ for (uint k = 0; k < places->getSize() && points; k++) {
+ TunerRecord *tuner = places->get(k);
+ if(tuner->isDuplicate()){
+ continue;
+ }
+ int currScore = 0;
+ if (scores.contains(tuner))
+ currScore = scores.get(tuner);
+ currScore += points;
+ model_print("Problem<%s>\tTuner<%p,%d>\tmetric<%d>\n", problem->getProblem(), tuner, tuner->getTunerNumber(), currScore);
+ model_print("**************************\n");
+ scores.put(tuner, currScore);
+ points = points / 3;
+ }
+ }
+ for(uint ii=0; ii< problems.getSize(); ii++){
+ delete allplaces.get(ii);
+ }
+ Vector<TunerRecord *> ranking;
+ for (uint i = 0; i < tunerV->getSize(); i++) {
+ TunerRecord *tuner = tunerV->get(i);
+ int score = 0;
+ if (scores.contains(tuner))
+ score = scores.get(tuner);
+ uint j = 0;
+ for (; j < ranking.getSize(); j++) {
+ TunerRecord *t = ranking.get(j);
+ int tscore = 0;
+ if (scores.contains(t))
+ tscore = scores.get(t);
+ if (score > tscore)
+ break;
+ }
+ model_print("ranking[%u]=tuner<%p,%u>(Score=%d)\n", j, tuner, tuner->getTunerNumber(), score);
+ model_print("************************\n");
+ ranking.insertAt(j, tuner);
+ }
+ model_print("tunerSize=%u\trankingSize=%u\ttunerVSize=%u\n", tuners.getSize(), ranking.getSize(), tunerV->getSize());
+ for (uint i = tuners.getSize(); i < ranking.getSize(); i++) {
+ TunerRecord *tuner = ranking.get(i);
+ model_print("Removing tuner %u\n", tuner->getTunerNumber());
+ for (uint j = 0; j < tunerV->getSize(); j++) {
+ if (tunerV->get(j) == tuner)
+ tunerV->removeAt(j);
+ }
+ }
+ uint tSize = tunerV->getSize();
+ for (uint i = 0; i < tSize; i++) {
+ SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
+ while(subTunerIndex(tmpTuner) != -1){
+ model_print("******** New Tuner already explored...\n");
+ delete tmpTuner;
+ tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
+ }
+ TunerRecord *tmp = new TunerRecord(tmpTuner);
+ tmp->setTunerNumber(allTuners.getSize());
+ model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
+ allTuners.push(tmp);
+ tunerV->push(tmp);
+ }
+ }
+ printData();
+}
--- /dev/null
+#ifndef COMPTUNER_H
+#define COMPTUNER_H
+#include "classlist.h"
+#include "structs.h"
+#include "basictuner.h"
+
+
+class CompTuner : public BasicTuner {
+public:
+ CompTuner(uint budget, uint timeout);
+ virtual ~CompTuner();
+ void readData(uint numRuns);
+ void tune();
+ void findBestThreeTuners();
+protected:
+
+};
+
+inline long long min(long long num1, long long num2, long long num3) {
+ return num1 < num2 && num1 < num3 ? num1 :
+ num2 < num3 ? num2 : num3;
+}
+
+#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: kmeanstuner.cc
+ * Author: hamed
+ *
+ * Created on December 19, 2018, 4:16 PM
+ */
+
+#include "kmeanstuner.h"
+#include "float.h"
+#include "searchtuner.h"
+#include "math.h"
+
+KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) :
+ BasicTuner(budget, timeout),
+ rounds(_rounds) {
+}
+
+KMeansTuner::~KMeansTuner() {
+}
+
+void clearVector(Vector<TunerRecord *> *tunerV) {
+ for (uint j = 0; j < tunerV->getSize(); j++) {
+ TunerRecord *tuner = tunerV->get(j);
+ tuner->problems.clear();
+ }
+}
+
+void KMeansTuner::tune() {
+ Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
+ for (uint i = 0; i < rounds; i++) {
+ clearVector(tunerV);
+ mapProblemsToTuners(tunerV);
+ improveTuners(tunerV);
+ }
+ model_print("Best tuners\n");
+ for (uint j = 0; j < tunerV->getSize(); j++) {
+ TunerRecord *tuner = tunerV->get(j);
+ char buffer[256];
+ sprintf(buffer, "tuner%u.conf", j);
+ tuner->getTuner()->serialize(buffer);
+ tuner->getTuner()->print();
+ }
+ delete tunerV;
+}
+
+void KMeansTuner::improveTuners(Vector<TunerRecord *> *tunerV) {
+ for (uint j = 0; j < tunerV->getSize(); j++) {
+ TunerRecord *tuner = tunerV->get(j);
+ TunerRecord *newtuner = tune(tuner);
+ tunerV->set(j, newtuner);
+ }
+}
+
+double KMeansTuner::evaluateAll(TunerRecord *tuner) {
+ double product = 1;
+ for (uint i = 0; i < tuner->problemsSize(); i++) {
+ Problem *problem = tuner->getProblem(i);
+ long long metric = tuner->getTime(problem);
+ if (metric == -1) {
+ metric = evaluate(problem, tuner);
+ if (metric != -1)
+ tuner->setTime(problem, metric);
+ else
+ tuner->setTime(problem, -2);
+ }
+
+ double score = metric;
+ if (metric < 0)
+ score = timeout;
+ product *= score;
+ }
+ return pow(product, 1 / ((double)tuner->problemsSize()));
+}
+
+TunerRecord *KMeansTuner::tune(TunerRecord *tuner) {
+ TunerRecord *bestTuner = NULL;
+ double bestScore = DBL_MAX;
+
+ TunerRecord *oldTuner = tuner;
+ double base_temperature = evaluateAll(oldTuner);
+ double oldScore = base_temperature;
+
+ for (uint i = 0; i < budget; i++) {
+ SearchTuner *tmpTuner = mutateTuner(oldTuner->getTuner(), i);
+ TunerRecord *newTuner = oldTuner->changeTuner(tmpTuner);
+ newTuner->setTunerNumber( allTuners.getSize() );
+ allTuners.push(newTuner);
+ double newScore = evaluateAll(newTuner);
+ newTuner->getTuner()->printUsed();
+ model_print("Received score %f\n", newScore);
+ double scoreDiff = newScore - oldScore; //smaller is better
+ if (newScore < bestScore) {
+ bestScore = newScore;
+ bestTuner = newTuner;
+ }
+
+ double acceptanceP;
+ if (scoreDiff < 0) {
+ acceptanceP = 1;
+ } else {
+ double currTemp = base_temperature * (((double)budget - i) / budget);
+ acceptanceP = exp(-scoreDiff / currTemp);
+ }
+ double ran = ((double)random()) / RAND_MAX;
+ if (ran <= acceptanceP) {
+ oldScore = newScore;
+ oldTuner = newTuner;
+ }
+ }
+
+ return bestTuner;
+}
+
+void KMeansTuner::mapProblemsToTuners(Vector<TunerRecord *> *tunerV) {
+ for (uint i = 0; i < problems.getSize(); i++) {
+ Problem *problem = problems.get(i);
+ TunerRecord *bestTuner = NULL;
+ long long bestscore = 0;
+ for (uint j = 0; j < tunerV->getSize(); j++) {
+ TunerRecord *tuner = tunerV->get(j);
+ long long metric = tuner->getTime(problem);
+ if (metric == -1) {
+ metric = evaluate(problem, tuner);
+ if (metric != -1)
+ tuner->setTime(problem, metric);
+ else
+ tuner->setTime(problem, -2);
+ }
+ if ((bestTuner == NULL && metric >= 0) ||
+ (metric < bestscore && metric >= 0)) {
+ bestTuner = tuner;
+ bestscore = metric;
+ }
+ }
+ if (bestTuner != NULL)
+ bestTuner->addProblem(problem);
+ }
+}
\ No newline at end of file
--- /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: kmeanstuner.h
+ * Author: hamed
+ *
+ * Created on December 19, 2018, 4:16 PM
+ */
+
+#ifndef KMEANSTUNER_H
+#define KMEANSTUNER_H
+
+#include "basictuner.h"
+
+
+class KMeansTuner : public BasicTuner {
+public:
+ KMeansTuner(uint budget, uint rounds, uint timeout );
+ virtual ~KMeansTuner();
+ void tune();
+private:
+ double evaluateAll(TunerRecord *tuner);
+ void mapProblemsToTuners(Vector<TunerRecord *> *tunerV);
+ void improveTuners(Vector<TunerRecord *> *tunerV);
+ TunerRecord *tune(TunerRecord *tuner);
+ uint rounds;
+};
+
+#endif /* KMEANSTUNER_H */
+
--- /dev/null
+#include "randomtuner.h"
+#include "csolver.h"
+#include "searchtuner.h"
+#include "comptuner.h"
+#include <math.h>
+#include <stdlib.h>
+#include <limits>
+
+#define UNSETVALUE -1
+
+RandomTuner::RandomTuner(uint _budget, uint _timeout) :
+ BasicTuner(_budget, _timeout) {
+}
+
+RandomTuner::~RandomTuner(){
+
+}
+
+void RandomTuner::tune() {
+ for (uint r = 0; r < budget; r++) {
+ model_print("Round %u of %u\n", r, budget);
+ for (uint i = 0; i < tuners.getSize(); i++){
+ TunerRecord *tuner = tuners.get(i);
+ bool isNew = true;
+ for (uint j = 0; j < problems.getSize(); j++){
+ Problem *problem = problems.get(j);
+ long long metric = tuner->getTime(problem);
+ if(metric == -1){
+ metric = evaluate(problem, tuner);
+ ASSERT(tuner->getTime(problem) == -1);
+ tuner->addProblem(problem);
+ model_print("%u.Problem<%s>\tTuner<%p, %d>\tMetric<%lld>\n", i, problem->getProblem(),tuner, tuner->getTunerNumber(), metric);
+ if (metric != -1)
+ tuner->setTime(problem, metric);
+ else
+ tuner->setTime(problem, -2);
+ if(tunerExists(tuner)){
+ //Solving the problem and noticing the tuner
+ //already exists
+ isNew = false;
+ break;
+ }
+ }
+ }
+ if(isNew){
+ explored.push(tuner);
+ }
+
+ }
+ uint tSize = tuners.getSize();
+ for (uint i = 0; i < tSize; i++) {
+ SearchTuner *tmpTuner = mutateTuner(tuners.get(i)->getTuner(), budget);
+ while(subTunerIndex(tmpTuner) != -1){
+ tmpTuner->randomMutate();
+ }
+ TunerRecord *tmp = new TunerRecord(tmpTuner);
+ tmp->setTunerNumber(allTuners.getSize());
+ model_print("Mutated tuner %u to generate tuner %u\n", tuners.get(i)->getTunerNumber(), tmp->getTunerNumber());
+ allTuners.push(tmp);
+ tuners.set(i, tmp);
+ }
+ }
+ printData();
+
+}
--- /dev/null
+#ifndef RANDOMTUNER_H
+#define RANDOMTUNER_H
+#include "classlist.h"
+#include "structs.h"
+#include "comptuner.h"
+#include "basictuner.h"
+
+/**
+ * This is a Tuner which is being used for
+ */
+class RandomTuner : public BasicTuner {
+public:
+ RandomTuner(uint _budget, uint _timeout);
+ virtual ~RandomTuner();
+ void tune();
+protected:
+ bool randomMutation(SearchTuner *tuner);
+ TunerRecord *tune(SearchTuner *tuner);
+};
+
+#endif
--- /dev/null
+#include "satuner.h"
+#include <float.h>
+#include <math.h>
+#include "searchtuner.h"
+#include <iostream>
+#include <fstream>
+#include "solver_interface.h"
+#include <stdlib.h>
+
+SATuner::SATuner(uint _budget, uint _timeout) :
+ BasicTuner(_budget, _timeout)
+{
+}
+
+SATuner::~SATuner(){
+
+}
+
+void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric){
+ uint k = 0;
+ for (; k < places->getSize(); k++) {
+ if (metric < places->get(k)->getTime(problem))
+ break;
+ }
+ model_print("Problem<%s>:place[%u]=Tuner<%p,%d>\n", problem->getProblem(), k, tuner, tuner->getTunerNumber());
+ places->insertAt(k, tuner);
+}
+
+void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index, Vector<Vector<TunerRecord *> *> &allplaces){
+ TunerRecord *tuner = tunerV->get(index);
+ model_print("Removing Tuner %d\n", tuner->getTunerNumber());
+ tunerV->set(index, NULL);
+ for(uint i=0; i < allplaces.getSize(); i++){
+ Vector<TunerRecord *> *places = allplaces.get(i);
+ for(uint j=0; j < places->getSize(); j++){
+ if(tuner == places->get(j)){
+ places->removeAt(j);
+ break;
+ }
+ }
+ }
+
+}
+
+void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV){
+ for (int i= tunerV->getSize() -1; i >= 0; i--){
+ if(tunerV->get(i) == NULL){
+ tunerV->removeAt(i);
+ }
+ }
+ model_print("TunerV size after removing nulls = %u\n", tunerV->getSize());
+}
+
+void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces){
+ for(uint ii=0; ii< problems.getSize(); ii++){
+ allplaces.push(new Vector<TunerRecord *>());
+ }
+ for (uint j = 0; j< tunerV->getSize(); j++){
+ TunerRecord *tuner = tunerV->get(j);
+ for (uint i=0; i < problems.getSize(); i++){
+ Problem *problem = problems.get(i);
+ long long metric = evaluate(problem, tuner);
+ ASSERT(tuner->getTime(problem) == -1);
+ tuner->addProblem(problem);
+ if(metric != -1){
+ tuner->setTime(problem , metric);
+ }else{
+ tuner->setTime(problem , -2);
+ }
+ if(metric >=0){
+ Vector<TunerRecord *> *places = allplaces.get(i);
+ rankTunerForProblem(places, tuner, problem, metric);
+ }
+ }
+ }
+
+}
+
+void SATuner::tune() {
+ Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
+ Vector<Vector<TunerRecord *> *> allplaces;
+ uint tunerNumber = tuners.getSize();
+ //Initialization
+ initialize(tunerV, allplaces);
+ //Starting the body of algorithm
+ for (uint t = budget; t >0; t--) {
+ model_print("Current Temperature = %u\n", t);
+ Hashtable<TunerRecord *, int, uint64_t> scores;
+ for (uint i = 0; i < tunerNumber; i++) {
+ SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget-t);
+ int tunerIndex = subTunerIndex(tmpTuner);
+ TunerRecord *tmp = NULL;
+ if(tunerIndex == -1){
+ tmp = new TunerRecord(tmpTuner);
+ tmp->setTunerNumber(allTuners.getSize());
+ model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
+ allTuners.push(tmp);
+ }else{
+ //Previous tuners might get explored with new combination of tuners.
+ tmp = explored.get(tunerIndex);
+ model_print("Using exploread tuner <%u>\n", tmp->getTunerNumber());
+ }
+ tunerV->push(tmp);
+ }
+ ASSERT(tunerNumber * 2 == tunerV->getSize());
+ for (uint j = tunerNumber; j < tunerV->getSize(); j++) {
+ TunerRecord *tuner = tunerV->get(j);
+ for (uint i = 0; i < problems.getSize(); i++) {
+ Problem *problem = problems.get(i);
+ long long metric = tuner->getTime(problem);
+ if (metric == -1) {
+ metric = evaluate(problem, tuner);
+ if (tuner->getTime(problem) == -1) {
+ tuner->addProblem(problem);
+ }
+ model_print("%u.Problem<%s>\tTuner<%p, %d>\tMetric<%lld>\n", i, problem->getProblem(),tuner, tuner->getTunerNumber(), metric);
+ model_print("*****************************\n");
+ if (metric != -1)
+ tuner->setTime(problem, metric);
+ else
+ tuner->setTime(problem, -2);
+
+ }
+ if (metric >= 0) {
+ ASSERT(i < allplaces.getSize());
+ Vector<TunerRecord *> *places = allplaces.get(i);
+ model_print("Problem<%s>:place[size=%u]=Tuner<%p,%d>\n", problem->getProblem(), places->getSize(), tuner, tuner->getTunerNumber());
+ rankTunerForProblem(places, tuner, problem, metric);
+ }
+ }
+ }
+ for(uint ii=0; ii < problems.getSize(); ii++){
+ Problem *problem = problems.get(ii);
+ ASSERT(ii < allplaces.getSize());
+ Vector<TunerRecord *> *places = allplaces.get(ii);
+ int points = pow(tunerNumber*1.0, 2*tunerNumber - 1);
+ for (uint k = 0; k < places->getSize() && points; k++) {
+ TunerRecord *tuner = places->get(k);
+ int currScore = 0;
+ if (scores.contains(tuner))
+ currScore = scores.get(tuner);
+ currScore += points;
+ model_print("Problem<%s>\tTuner<%p,%d>\tmetric<%d>\n", problem->getProblem(), tuner, tuner->getTunerNumber(), currScore);
+ model_print("**************************\n");
+ scores.put(tuner, currScore);
+ points = points / tunerNumber;
+ }
+ }
+
+ for(uint i= 0; i < tunerNumber; i++){
+ ASSERT(i < tunerV->getSize());
+ TunerRecord *tuner1 = tunerV->get(i);
+ TunerRecord *tuner2 = tunerV->get(tunerNumber + i);
+ ASSERT( tunerNumber + i < tunerV->getSize());
+ model_print("Tuner1 = %d \tTuner2 = %d\n", tuner1->getTunerNumber(), tuner2->getTunerNumber());
+ ASSERT(scores.contains(tuner1));
+ ASSERT(scores.contains(tuner2));
+ int score1 = scores.get(tuner1);
+ int score2 = scores.get(tuner2);
+ if( score2 > score1 ){
+ removeTunerIndex(tunerV, i, allplaces);
+ } else if( score2 < score1){
+ model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1-score2)*1.0/t));
+ double prob = 1/(exp((score1-score2)*1.0/t) );
+ double random = ((double) rand() / (RAND_MAX));
+ model_print("prob=%f\trandom=%f\n", prob, random);
+ if(prob > random){
+ removeTunerIndex(tunerV, i, allplaces);
+ }else{
+ removeTunerIndex(tunerV, tunerNumber + i, allplaces);
+ }
+ } else{
+ double random = ((double) rand() / (RAND_MAX));
+ int index = random > 0.5? i : tunerNumber + i;
+ removeTunerIndex(tunerV, index, allplaces);
+ }
+ }
+ removeNullsFromTunerVector(tunerV);
+
+ }
+ for(uint ii=0; ii< allplaces.getSize(); ii++){
+ delete allplaces.get(ii);
+ }
+ printData();
+}
--- /dev/null
+#ifndef SATUNER_H
+#define SATUNER_H
+#include "classlist.h"
+#include "structs.h"
+#include "basictuner.h"
+
+/**
+*This tuner has the simulated annealing in its core
+*
+*/
+class SATuner : public BasicTuner {
+public:
+ SATuner(uint budget, uint timeout);
+ virtual ~SATuner();
+ void tune();
+protected:
+ void insertInPlace(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric);
+ void initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces);
+ void rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric);
+ void removeTunerIndex(Vector<TunerRecord *> *tunerV, int index, Vector<Vector<TunerRecord *> *> &allplaces);
+ void removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV);
+};
+
+
+#endif
#include "searchtuner.h"
-#include "tunabledependent.h"
#include <iostream>
#include <fstream>
-#include <valarray>
using namespace std;
-HashsetTunableDep initializeTunableDependencies()
-{
- HashsetTunableDep dep;
- dep.add(new TunableDependent(MUSTREACHGLOBAL, DECOMPOSEORDER));
- dep.add(new TunableDependent(MUSTREACHLOCAL, DECOMPOSEORDER));
- dep.add(new TunableDependent(MUSTREACHPRUNE, DECOMPOSEORDER));
- dep.add(new TunableDependent(MUSTEDGEPRUNE, DECOMPOSEORDER));
- dep.add(new TunableDependent(NODEENCODING, ENCODINGGRAPHOPT));
- dep.add(new TunableDependent(EDGEENCODING, ENCODINGGRAPHOPT));
- dep.add(new TunableDependent(ELEMENTOPTSETS, ELEMENTOPT));
- return dep;
-}
-
-
-HashsetTunableDep SearchTuner::tunableDependency = initializeTunableDependencies();
-
TunableSetting::TunableSetting(VarType _type, TunableParam _param) :
hasVar(true),
type1(_type),
model_print("\n");
}
-unsigned int tunableSettingHash(TunableSetting *setting) {
- return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
-}
-
-bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
- return setting1->hasVar == setting2->hasVar &&
- setting1->type1 == setting2->type1 &&
- setting1->type2 == setting2->type2 &&
- setting1->param == setting2->param;
-}
ostream &operator<<(ostream &os, const TunableSetting &ts)
{
SearchTuner::SearchTuner() {
-#ifdef STATICENCGEN
- graphEncoding =false;
- naiveEncoding = ELEM_UNASSIGNED;
-#endif
+}
+
+SearchTuner::SearchTuner(const char *filename, bool addused) {
ifstream myfile;
- myfile.open (TUNEFILE, ios::in);
+ myfile.open (filename, ios::in);
if (myfile.is_open()) {
bool hasVar;
VarType type1;
setting = new TunableSetting(param);
}
setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
- usedSettings.add(setting);
+ settings.add(setting);
+ if(addused){
+ usedSettings.add(setting);
+ }
}
myfile.close();
+ } else {
+ model_print("Warning: Tuner %s couldn't be loaded ... Using default tuner instead ....\n", filename);
+ }
+}
+
+bool SearchTuner::equalUsed(SearchTuner* tuner){
+ if(tuner->usedSettings.getSize() != usedSettings.getSize()){
+ return false;
+ }
+ bool result = true;
+ SetIteratorTunableSetting *iterator = usedSettings.iterator();
+ while(iterator->hasNext()){
+ TunableSetting *setting = iterator->next();
+ if(!tuner->usedSettings.contains(setting)){
+ result = false;
+ break;
+ }else{
+ TunableSetting *tunerSetting = tuner->usedSettings.get(setting);
+ if(tunerSetting->selectedValue != setting->selectedValue){
+ result = false;
+ break;
+ }
+ }
}
+ delete iterator;
+ return result;
+}
+
+void SearchTuner::addUsed(const char *filename) {
+ ifstream myfile;
+ myfile.open (filename, ios::in);
+ if (myfile.is_open()) {
+ bool hasVar;
+ VarType type1;
+ VarType type2;
+ TunableParam param;
+ int lowValue;
+ int highValue;
+ int defaultValue;
+ int selectedValue;
+ while (myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue) {
+ TunableSetting *setting;
+
+ if (hasVar) {
+ setting = new TunableSetting(type1, type2, param);
+ } else {
+ setting = new TunableSetting(param);
+ }
+ setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
+ if (!settings.contains(setting)) {
+ settings.add(setting);
+ usedSettings.add(setting);
+ } else {
+ TunableSetting *tmp = settings.get(setting);
+ settings.remove(tmp);
+ usedSettings.remove(tmp);
+ delete tmp;
+ settings.add(setting);
+ usedSettings.add(setting);
+ }
+ }
+ myfile.close();
+ }
+}
+
+bool SearchTuner::isSubTunerof(SearchTuner *newTuner){
+ SetIteratorTunableSetting *iterator = usedSettings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
+ if(!newTuner->settings.contains(setting)){
+ return false;
+ } else{
+ TunableSetting *newSetting = newTuner->settings.get(setting);
+ if(newSetting->selectedValue != setting->selectedValue){
+ return false;
+ }
+ }
+ }
+ delete iterator;
+ return true;
}
SearchTuner *SearchTuner::copyUsed() {
TunableSetting *copy = new TunableSetting(setting);
tuner->settings.add(copy);
}
-#ifdef STATICENCGEN
- if(naiveEncoding != ELEM_UNASSIGNED){
- tuner->graphEncoding = graphEncoding;
- tuner->naiveEncoding = naiveEncoding;
- }
-#endif
delete iterator;
return tuner;
}
delete iterator;
}
+void SearchTuner::setTunable(TunableParam param, TunableDesc *descriptor, uint value) {
+ TunableSetting *result = new TunableSetting(param);
+ result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
+ settings.add(result);
+ usedSettings.add(result);
+}
+
+void SearchTuner::setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value) {
+ setVarTunable(vartype, 0, param, descriptor, value);
+}
+
+void SearchTuner::setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value) {
+ TunableSetting *result = new TunableSetting(vartype1, vartype2, param);
+ result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
+ settings.add(result);
+ usedSettings.add(result);
+}
+
int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
TunableSetting setting(param);
TunableSetting *result = usedSettings.get(&setting);
return result->selectedValue;
}
-bool SearchTuner::validTunableSetting(TunableSetting* setting){
- TunableDependent tuneDep((Tunables)setting->param);
- bool result = true;
- while(tunableDependency.contains(&tuneDep)){
- TunableDependent *dependent = tunableDependency.get(&tuneDep);
- TunableSetting p(dependent->parent);
- if(!settings.contains(&p)){
- SetIteratorTunableSetting *iter = settings.iterator();
- while(iter->hasNext()){
- model_print("*******************\n");
- iter->next()->print();
- }
- delete iter;
- }
- ASSERT(settings.contains(&p));
- TunableSetting *parent = settings.get(&p);
- if(!(bool)parent->selectedValue){ //Check parent config is already off
- return false;
- }
- tuneDep.dependent = dependent->parent;
- }
- return result;
-}
-
void SearchTuner::randomMutate() {
- TunableSetting *randomSetting;
- do{
- randomSetting= settings.getRandomElement();
- }while(!validTunableSetting(randomSetting));
+ TunableSetting *randomSetting = settings.getRandomElement();
int range = randomSetting->highValue - randomSetting->lowValue;
int randomchoice = (random() % range) + randomSetting->lowValue;
if (randomchoice < randomSetting->selectedValue)
model_print("&&&&&&&&&&&&&&&&&&&&&&&\n");
}
-#ifdef STATICENCGEN
-int SearchTuner::nextStaticTuner() {
- if(naiveEncoding == ELEM_UNASSIGNED){
- naiveEncoding = ONEHOT;
- SetIteratorTunableSetting *iter = settings.iterator();
- while(iter->hasNext()){
- TunableSetting *setting = iter->next();
- if (setting->param == NAIVEENCODER){
- setting->selectedValue = ONEHOT;
- } else if(setting->param == ENCODINGGRAPHOPT){
- setting->selectedValue = false;
- }
- }
- delete iter;
- return EXIT_FAILURE;
- }
- int result=EXIT_FAILURE;
- if(naiveEncoding == BINARYINDEX && graphEncoding){
- model_print("Best tuner\n");
- return EXIT_SUCCESS;
- }else if (naiveEncoding == BINARYINDEX && !graphEncoding){
- naiveEncoding = ONEHOT;
- graphEncoding = true;
- }else {
- naiveEncoding = (ElementEncodingType)((int)naiveEncoding + 1);
- }
- SetIteratorTunableSetting *iter = settings.iterator();
- uint count = 0;
- while(iter->hasNext()){
- TunableSetting * setting = iter->next();
- if (setting->param == NAIVEENCODER){
- setting->selectedValue = naiveEncoding;
- count++;
- } else if(setting->param == ENCODINGGRAPHOPT){
- setting->selectedValue = graphEncoding;
- count++;
- }
- }
- model_print("Mutating %u settings\n", count);
- delete iter;
- return result;
-}
-#endif
-
void SearchTuner::print() {
SetIteratorTunableSetting *iterator = settings.iterator();
while (iterator->hasNext()) {
}
-void SearchTuner::serialize() {
+void SearchTuner::serialize(const char *filename) {
ofstream myfile;
- myfile.open (TUNEFILE, ios::out | ios::trunc);
+ myfile.open (filename, ios::out | ios::trunc);
SetIteratorTunableSetting *iterator = settings.iterator();
while (iterator->hasNext()) {
TunableSetting *setting = iterator->next();
delete iterator;
}
+void SearchTuner::serializeUsed(const char *filename) {
+ ofstream myfile;
+ myfile.open (filename, ios::out | ios::trunc);
+ SetIteratorTunableSetting *iterator = usedSettings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
+ myfile << *setting << endl;
+ }
+ myfile.close();
+ delete iterator;
+}
+
void SearchTuner::printUsed() {
SetIteratorTunableSetting *iterator = usedSettings.iterator();
while (iterator->hasNext()) {
#include "structs.h"
#include <ostream>
using namespace std;
-#define TUNEFILE "tune.conf"
class TunableSetting {
public:
friend unsigned int tunableSettingHash(TunableSetting *setting);
friend bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2);
friend class SearchTuner;
+ friend class SerializeTuner;
};
-unsigned int tunableSettingHash(TunableSetting *setting);
-bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2);
-
-typedef Hashset<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> HashsetTunableSetting;
-typedef SetIterator<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> SetIteratorTunableSetting;
-
class SearchTuner : public Tuner {
public:
SearchTuner();
+ SearchTuner(const char *filename, bool addused = false);
~SearchTuner();
- int getTunable(TunableParam param, TunableDesc *descriptor);
+ virtual int getTunable(TunableParam param, TunableDesc *descriptor);
int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
- int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
+ virtual int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
+ void setTunable(TunableParam param, TunableDesc *descriptor, uint value);
+ void setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value);
+ void setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value);
SearchTuner *copyUsed();
+ bool isSubTunerof(SearchTuner *newTuner);
void randomMutate();
uint getSize() { return usedSettings.getSize();}
void print();
void printUsed();
- void serialize();
-
+ void serialize(const char *file);
+ void serializeUsed(const char *file);
+ void addUsed(const char *file);
+ bool equalUsed(SearchTuner *tuner);
CMEMALLOC;
-private:
- bool validTunableSetting(TunableSetting* setting);
- static HashsetTunableDep tunableDependency;
+protected:
/** Used Settings keeps track of settings that were actually used by
the example. Mutating settings may cause the Constraint Compiler
not to query other settings.*/
HashsetTunableSetting usedSettings;
/** Settings contains all settings. */
HashsetTunableSetting settings;
-#ifdef STATICENCGEN
- bool graphEncoding;
- ElementEncodingType naiveEncoding;
-public:
- int nextStaticTuner();
-#endif
};
-
#endif
--- /dev/null
+#include "serializetuner.h"
+#include <iostream>
+#include <fstream>
+using namespace std;
+
+SerializeTuner::SerializeTuner(const char *filename) {
+ ifstream myfile;
+ myfile.open (filename, ios::in);
+ if (myfile.is_open()) {
+ bool hasVar;
+ VarType type1;
+ VarType type2;
+ TunableParam param;
+ int lowValue;
+ int highValue;
+ int defaultValue;
+ int selectedValue;
+ while (myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue) {
+ TunableSetting *setting;
+
+ if (hasVar) {
+ setting = new TunableSetting(type1, type2, param);
+ } else {
+ setting = new TunableSetting(param);
+ }
+ setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
+ settings.add(setting);
+ usedSettings.add(setting);
+ }
+ myfile.close();
+ } else {
+ model_print("Warning: Tuner %s couldn't be loaded ... Using default tuner instead ....\n", filename);
+ }
+}
+
+/*SearchTuner::~SearchTuner() {
+ SetIteratorTunableSetting *iterator = settings.iterator();
+ while (iterator->hasNext()) {
+ TunableSetting *setting = iterator->next();
+ delete setting;
+ }
+ delete iterator;
+ }*/
+
+
+int SerializeTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
+ TunableSetting setting(param);
+ TunableSetting *result = usedSettings.get(&setting);
+ if (result == NULL) {
+ result = settings.get(&setting);
+ if ( result == NULL) {
+ return descriptor->defaultValue;
+ }
+ usedSettings.add(result);
+ }
+ return result->selectedValue;
+}
+
+int SerializeTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+ TunableSetting setting(vartype1, vartype2, param);
+ TunableSetting *result = usedSettings.get(&setting);
+ if (result == NULL) {
+ result = settings.get(&setting);
+ if ( result == NULL) {
+ return descriptor->defaultValue;
+ }
+ usedSettings.add(result);
+ }
+ return result->selectedValue;
+}
--- /dev/null
+#ifndef SERIALIZETUNER_H
+#define SERIALIZETUNER_H
+#include "searchtuner.h"
+
+class SerializeTuner : public SearchTuner {
+public:
+ SerializeTuner(const char *filename);
+ int getTunable(TunableParam param, TunableDesc *descriptor);
+ int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
+ CMEMALLOC;
+};
+
+#endif
return descriptor->defaultValue;
}
-const char* tunableParameterToString(Tunables tunable){
- switch(tunable){
- case DECOMPOSEORDER:
- return "DECOMPOSEORDER";
- case MUSTREACHGLOBAL:
- return "MUSTREACHGLOBAL";
- case MUSTREACHLOCAL:
- return "MUSTREACHLOCAL";
- case MUSTREACHPRUNE:
- return "MUSTREACHPRUNE";
- case OPTIMIZEORDERSTRUCTURE:
- return "OPTIMIZEORDERSTRUCTURE";
- case ORDERINTEGERENCODING:
- return "ORDERINTEGERENCODING";
- case PREPROCESS:
- return "PREPROCESS";
- case NODEENCODING:
- return "NODEENCODING";
- case EDGEENCODING:
- return "EDGEENCODING";
- case MUSTEDGEPRUNE:
- return "MUSTEDGEPRUNE";
- case ELEMENTOPT:
- return "ELEMENTOPT";
- case ELEMENTOPTSETS:
- return "ELEMENTOPTSETS";
- case PROXYVARIABLE:
- return "PROXYVARIABLE";
- case ENCODINGGRAPHOPT:
- return "ENCODINGGRAPHOPT";
- case NAIVEENCODER:
- return "NAIVEENCODER";
- case MUSTVALUE:
- return "MUSTVALUE";
- default:
- ASSERT(0);
- }
+const char *tunableParameterToString(Tunables tunable) {
+ switch (tunable) {
+ case DECOMPOSEORDER:
+ return "DECOMPOSEORDER";
+ case MUSTREACHGLOBAL:
+ return "MUSTREACHGLOBAL";
+ case MUSTREACHLOCAL:
+ return "MUSTREACHLOCAL";
+ case MUSTREACHPRUNE:
+ return "MUSTREACHPRUNE";
+ case OPTIMIZEORDERSTRUCTURE:
+ return "OPTIMIZEORDERSTRUCTURE";
+ case ORDERINTEGERENCODING:
+ return "ORDERINTEGERENCODING";
+ case PREPROCESS:
+ return "PREPROCESS";
+ case NODEENCODING:
+ return "NODEENCODING";
+ case EDGEENCODING:
+ return "EDGEENCODING";
+ case MUSTEDGEPRUNE:
+ return "MUSTEDGEPRUNE";
+ case ELEMENTOPT:
+ return "ELEMENTOPT";
+ case ELEMENTOPTSETS:
+ return "ELEMENTOPTSETS";
+ case PROXYVARIABLE:
+ return "PROXYVARIABLE";
+ case ENCODINGGRAPHOPT:
+ return "ENCODINGGRAPHOPT";
+ case NAIVEENCODER:
+ return "NAIVEENCODER";
+ case MUSTVALUE:
+ return "MUSTVALUE";
+ case VARIABLEORDER:
+ return "VARIABLEORDER";
+ default:
+ ASSERT(0);
+ }
}
static TunableDesc onoff(0, 1, 1);
static TunableDesc offon(0, 1, 0);
static TunableDesc proxyparameter(1, 5, 2);
-static TunableDesc mustValueBinaryIndex(5, 9, 8);
+static TunableDesc mustValueBinaryIndex(0, 6, 3);
static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
-static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, BINARYINDEX);
static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
- ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
+ ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
typedef enum Tunables Tunables;
const char *tunableParameterToString(Tunables tunable);
--- /dev/null
+#!/bin/bash
+
+REPORTDIR=./report
+PICSDIR=$REPORTDIR/pics
+
+
+set -e
+if [ "$#" -lt 1 ]; then
+ echo "Illegal number of argument"
+ echo "./analyze.sh [path/to/log/folder]"
+ exit 1
+fi
+
+mkdir -p $PICSDIR
+python tunerloganalyzer.py -f $1
+cd $REPORTDIR
+make
--- /dev/null
+import numpy as np
+import matplotlib.pyplot as plt
+IMAGEDIR = "report/pics/"
+
+def generateHistograms(X, header):
+ global IMAGEDIR
+ for i, c in enumerate(X.T):
+ plt.hist(c)
+ plt.savefig(IMAGEDIR + header[i] + "-hist.pdf")
+ plt.clf()
+
+def generateScatterPlot(X, Y, header):
+ global IMAGEDIR
+ for i, feature in enumerate(X.T):
+ values = np.unique(feature)
+ values = np.sort(values)
+ geomean = []
+ for value in values:
+ a =Y[np.where(feature == value)]
+ a = np.array(list(map(lambda x : x**(1.0/len(a)), a)))
+ geomean.append(a.prod())
+ plt.plot(feature, Y, 'r.')
+ for ii in range(0, len(geomean)-1):
+ plt.plot(values[ii:ii + 2], geomean[ii:ii + 2], 'bo-')
+ plt.savefig(IMAGEDIR + header[i] + "-scat.pdf")
+ plt.clf()
+
+def plot(data, header):
+ global IMAGEDIR
+ header=header[6:-1]
+ data = np.array(data)
+ X = data[:, 6:-4]
+ X[X==''] = '-1'
+ X = X.astype(np.float)
+ Y = data[:, -2]
+ Y = Y.astype(np.float)
+ generateHistograms(X, header)
+ generateScatterPlot(X, Y, header)
+
+
+
+
--- /dev/null
+LATEX := pdflatex -halt-on-error
+FIGURES :=
+.SUFFIXES : .tex .bbl .aux .eps .ps .dot .pdf
+
+.tex.bbl:
+ bibtex $*
+
+.tex.aux:
+ latex $*
+
+%.eps: %.ps
+ ps2epsi $< $@
+
+%.ps: %.dot
+ dot -Tps $< -o $@
+
+%.pdf: %.dot
+ dot -Tpdf $< -o $@
+
+%.png: %.dot
+ dot -Tpng $< -o $@
+
+%.aux: %.tex
+ $(LATEX) $<
+
+#%.dot: %.dotpiece $(FIGHEAD) $(FIGFOOT)
+# cat $(FIGHEAD) $< $(FIGFOOT) > $@
+
+# latex the paper (default)
+new: biblinks newpaper
+
+# latex + bibtex the paper
+bib: bibpaper newpaper
+
+# save a backup of tex files in BACKUPS
+bak: backuppaper
+
+biblinks: figures
+ $(LATEX) paper.tex
+ $(LATEX) paper.tex
+
+bibsuppl: figures
+ $(LATEX) suppl.tex
+ $(LATEX) suppl.tex
+
+cl: cover-letter.tex
+ $(LATEX) cover-letter.tex
+
+newpaper: figures biblinks
+ $(LATEX) paper.tex
+
+suppl: figures bibsuppl
+ $(LATEX) suppl.tex
+
+
+bibpaper: paper.aux paper.bbl
+ latex paper.tex
+
+
+backuppaper:
+ @if [ ! -d BACKUPS ]; then mkdir BACKUPS; fi; \
+ crtdate=`date '+%m-%d-%y--%H:%M:%S'`; \
+ bakdir=BACKUPS/$$crtdate; \
+ mkdir $$bakdir; \
+ cp *.tex $$bakdir
+
+spell:
+ @for i in *.tex; \
+ do if [ $$i != "paper.tex" ]; then aspell -c $$i -p ./spell.lst; fi;\
+ done
+
+total:
+ pdflatex paper.tex
+ pdflatex paper.tex
+ pdflatex paper.tex
+ @echo ================================================================
+ pdflatex paper.tex | grep -E 'arning|erfull'
+ @echo ================================================================
+
+figures: $(FIGURES)
+
+errinjfig:
+ gnuplot err-inj-fig/nve2latex.cmds
+ epstopdf injectErrorFig.eps
+ mv injectErrorFig.* figures
+
+
+clean:
+ rm -f *.dvi *.log *.aux *.blg *.bbl *~ err-inj-fig/*~
+ rm -f paper.ps paper.pdf
+ rm -f injectErrorFig*
+ rm -rf $(PDF_DIR)
--- /dev/null
+@BOOK{Smith:2012qr,
+ title = {{B}ook {T}itle},
+ publisher = {Publisher},
+ author = {Smith, J.~M. and Jones, A.~B.},
+ year = {2012},
+ edition = {7th},
+}
+
+@ARTICLE{Smith:2013jd,
+ author = {Jones, A.~B. and Smith, J.~M.},
+ title = {{A}rticle {T}itle},
+ journal = {Journal title},
+ year = {2013},
+ volume = {13},
+ pages = {123-456},
+ number = {52},
+ month = {March},
+ publisher = {Publisher}
+}
\ No newline at end of file
--- /dev/null
+\documentclass[a4paper, 11pt]{article} % Font size (can be 10pt, 11pt or 12pt) and paper size (remove a4paper for US letter paper)\r
+\r
+\usepackage[protrusion=true,expansion=true]{microtype} % Better typography\r
+\usepackage{graphicx} % Required for including pictures\r
+\usepackage{wrapfig} % Allows in-line images\r
+\r
+\usepackage{mathpazo} % Use the Palatino font\r
+\usepackage[T1]{fontenc} % Required for accented characters\r
+\usepackage{float}\r
+\linespread{1.05} % Change line spacing here, Palatino benefits from a slight increase by default\r
+\r
+%---------------------------------------------------------------------------------------tyle{acmnumeric}\r
+% TITLE\r
+%----------------------------------------------------------------------------------------\r
+\r
+\title{\textbf{SATTune Tuning Report}}\r
+\r
+%\author{\textsc{Ford Prefect} % Author\r
+%\\{\textit{Interstellar University}}} % Institution\r
+\r
+%\date{\today} % Date\r
+\r
+%----------------------------------------------------------------------------------------\r
+\r
+\begin{document}\r
+\r
+\maketitle % Print the title section\r
+\r
+\r
+\input{tech}\r
+\r
+%\bibliographystyle{unsrt}\r
+%\bibliography{paper}\r
+\r
+\end{document}\r
--- /dev/null
+\section{Evaluation}\label{sec:eval}\r
+\r
+\subsection{Histogram Plots}\label{subsec:hist}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/EDGEENCODING-hist.pdf}\r
+ \caption{Encoding Edge Histogram: 0=Edge Unassiged, 1= Edge Break, 2= Edge Match}\r
+ \label{fig:edgeencoding}\r
+\end{figure}\r
+\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/ELEMENTOPTSETS-hist.pdf}\r
+ \caption{Element Opt Set Histogram: Whether tuner should update sets or not. 0= OFF, 1= ON}\r
+ \label{fig:elementoptset}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/ELEMENTOPT-hist.pdf}\r
+ \caption{Element Opt Histogram: 0 = OFF, 1= ON}\r
+ \label{fig:elementopt}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/ENCODINGGRAPHOPT-hist.pdf}\r
+ \caption{Encoding Graph Optimization Histogram: 0= OFF, 1=ON}\r
+ \label{fig:encodinggraph}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/MUSTEDGEPRUNE-hist.pdf}\r
+ \caption{Must Prune Histogram: 0= OFF, 1= ON}\r
+ \label{fig:mustedgeprune}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/MUSTVALUE-hist.pdf}\r
+ \caption{Must Value Histogram: Binary Index must have value heuristic. The value varies from 0-6}\r
+ \label{fig:mustvalue}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/NODEENCODING-hist.pdf}\r
+ \caption{Node Encoding Histogram: 0= Unassigned, 1= OneHot, 2= Unary, 3= BinaryIndex}\r
+ \label{fig:nodeencoding}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/NAIVEENCODER-hist.pdf}\r
+ \caption{Naive Encoder Histogram: 1= OneHot, 2=Unary, 3=BinaryIndex}\r
+ \label{fig:naiveencoder}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/PREPROCESS-hist.pdf}\r
+ \caption{Preprocess Histogram: Replace Boolean Variables with T or F based on their polarity. 0= OFF, 1= ON}\r
+ \label{fig:preprocess}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/PROXYVARIABLE-hist.pdf}\r
+ \caption{Proxy Variable Histogram: Threshold for using proxy variables. Value varies from 1 to 5}\r
+ \label{fig:proxyvariable}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/VARIABLEORDER-hist.pdf}\r
+ \caption{Variable Order Histogram: 0= ConstraintOrdering, 1= ElementOrdering, 2=ReverseOrdering}\r
+ \label{fig:variableorder}\r
+\end{figure}\r
+\r
+\clearpage\r
+\subsection{Scatter Plots}\label{subsec:scatter}\r
+\r
+Y axis represents execution time and X axis shows the possible value of for each knob.\r
+Geometric mean of each value has been calculated and they are connected with solid lines.\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/EDGEENCODING-scat.pdf}\r
+ \caption{Encoding Edge plot}\r
+ \label{fig:edgeencodings}\r
+\end{figure}\r
+\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/ELEMENTOPTSETS-scat.pdf}\r
+ \caption{Element Opt Set plot}\r
+ \label{fig:elementoptsets}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/ELEMENTOPT-scat.pdf}\r
+ \caption{Element Opt plot}\r
+ \label{fig:elementopts}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/ENCODINGGRAPHOPT-scat.pdf}\r
+ \caption{Encoding Graph Optimization plot}\r
+ \label{fig:encodinggraphs}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/MUSTEDGEPRUNE-scat.pdf}\r
+ \caption{Must Prune plot}\r
+ \label{fig:mustedgeprunes}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/MUSTVALUE-scat.pdf}\r
+ \caption{Must Value plot}\r
+ \label{fig:mustvalues}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/NODEENCODING-scat.pdf}\r
+ \caption{Node Encoding plot}\r
+ \label{fig:nodeencodings}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/NAIVEENCODER-scat.pdf}\r
+ \caption{Naive Encoder plot}\r
+ \label{fig:naiveencoders}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/PREPROCESS-scat.pdf}\r
+ \caption{Preprocess Plot}\r
+ \label{fig:preprocesss}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/PROXYVARIABLE-scat.pdf}\r
+ \caption{Proxy Variable plot}\r
+ \label{fig:proxyvariables}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+ \centering\r
+ \includegraphics[scale=0.6]{pics/VARIABLEORDER-scat.pdf}\r
+ \caption{Variable Order Plot}\r
+ \label{fig:variableorders}\r
+\end{figure}\r
+\r
--- /dev/null
+import re
+import argparse
+import sys
+import os
+import plot as pl
+
+class AutoTunerArgParser:
+ def __init__(self):
+ self.parser = argparse.ArgumentParser(description='Parsing the output log of the CSolver auto tuner ...')
+ self.parser.add_argument('--folder', '-f', metavar='bin', type=str, nargs=1,help='output log of running the autotuner ...')
+ self.args = self.parser.parse_args()
+
+ def getFolder(self):
+ return self.args.folder[0]
+
+PROBLEMS = []
+
+TUNABLEHEADER = ["DECOMPOSEORDER", "MUSTREACHGLOBAL", "MUSTREACHLOCAL", "MUSTREACHPRUNE", "OPTIMIZEORDERSTRUCTURE",
+ "ORDERINTEGERENCODING", "PREPROCESS", "NODEENCODING", "EDGEENCODING", "MUSTEDGEPRUNE", "ELEMENTOPT",
+ "ENCODINGGRAPHOPT", "ELEMENTOPTSETS", "PROXYVARIABLE", "MUSTVALUE", "NAIVEENCODER", "VARIABLEORDER",
+ "PROBLEM","SATTIME", "EXECTIME","TUNERNUMBER"]
+
+configs = {"EXECTIME": "-",
+ "SATTIME":"-",
+ "TESTCASE":"-",
+ "PREPROCESS" : "-",
+ "ELEMENTOPT" : "-",
+ "ELEMENTOPTSETS" : "-",
+ "PROXYVARIABLE" : "-",
+ "#SubGraph" : "-",
+ "NODEENCODING" : "-",
+ "EDGEENCODING" : "-",
+ "NAIVEENCODER" :"-",
+ "ENCODINGGRAPHOPT" : "-"
+ }
+
+REGEXES = {"EXECTIME": "CSOLVER solve time: (.*)",
+ "SATTIME":"SAT Solving time: (.*)",
+ "TESTCASE": "deserializing (.+) ...",
+ "PREPROCESS" : "Param PREPROCESS = (.*)range=\[0,1\]",
+ "ELEMENTOPT" : "Param ELEMENTOPT = (.*)range=\[0,1\]",
+ "ELEMENTOPTSETS" : "Param ELEMENTOPTSETS = (.*)range=\[0,1\]",
+ "PROXYVARIABLE" : "Param PROXYVARIABLE = (.*)range=\[1,5\]",
+ "#SubGraph" : "#SubGraph = (.*)",
+ "NODEENCODING" : "Param NODEENCODING = (.*)range=\[0,3\](.*)",
+ "EDGEENCODING" : "Param EDGEENCODING = (.*)range=\[0,2\](.*)",
+ "NAIVEENCODER" : "Param NAIVEENCODER = (.*)range=\[1,3\](.*)",
+ "ENCODINGGRAPHOPT" : "Param ENCODINGGRAPHOPT = (.*)range=\[0,1\]"
+ }
+
+def printHeader(file):
+ global TUNABLEHEADER
+ mystr=""
+ for header in TUNABLEHEADER:
+ mystr+=str(header)+","
+ file.write(mystr)
+ file.write("\n")
+
+def dump(file, row):
+ global TUNABLEHEADER
+ mystr=""
+ data = []
+ for i in range(len(TUNABLEHEADER)):
+ mystr += row[TUNABLEHEADER[i]]+ ","
+ data.append(row[TUNABLEHEADER[i]])
+ print ("mystr is:"+ mystr)
+ file.write(mystr)
+ file.write("\n")
+ return data
+
+def loadTunerInfo(row, filename):
+ with open(filename) as f:
+ for line in f:
+ numbers = re.findall('\d+',line)
+ numbers = list(map(int,numbers))
+ row[TUNABLEHEADER[numbers[3]]] = row[TUNABLEHEADER[numbers[3]]] + str(numbers[7])
+
+def loadSolverTime(row, filename):
+ global REGEXES
+ global configs
+ with open(filename) as f:
+ for line in f:
+ for regex in REGEXES:
+ p = re.compile(REGEXES[regex])
+ token = p.search(line)
+ if token is not None:
+ if regex == "TESTCASE":
+ configs[regex] = re.search(REGEXES[regex], line).group(1)
+ else:
+ configs[regex] = re.findall("\d+\.?\d*", line)[0]
+ row["SATTIME"] = configs["SATTIME"]
+ row["EXECTIME"] = configs["EXECTIME"]
+
+def loadProblemName(row,filename):
+ global PROBLEMS
+ with open(filename) as f:
+ problem = f.readline().replace("\n","")
+ probNumber = int(f.readline())
+ if probNumber >= len(PROBLEMS):
+ PROBLEMS.insert(probNumber,problem)
+ elif PROBLEMS[probNumber] != problem:
+ PROBLEMS[probNumber] = problem
+ row["PROBLEM"] = problem
+
+def loadTunerNumber(row, filename):
+ with open(filename) as f:
+ row["TUNERNUMBER"] = f.readline().replace("\n","")
+def analyzeLogs(file):
+ global configs
+ argprocess = AutoTunerArgParser()
+ printHeader(file)
+ rows = []
+ data = []
+ i = 0
+ while True :
+ row = {"DECOMPOSEORDER" : "",
+ "MUSTREACHGLOBAL" : "",
+ "MUSTREACHLOCAL" : "",
+ "MUSTREACHPRUNE" : "",
+ "OPTIMIZEORDERSTRUCTURE" : "",
+ "ORDERINTEGERENCODING" : "",
+ "PREPROCESS" : "",
+ "NODEENCODING" : "",
+ "EDGEENCODING" : "",
+ "MUSTEDGEPRUNE" : "",
+ "ELEMENTOPT" : "",
+ "ENCODINGGRAPHOPT" : "",
+ "ELEMENTOPTSETS" : "",
+ "PROXYVARIABLE" : "",
+ "MUSTVALUE" : "",
+ "NAIVEENCODER" : "",
+ "VARIABLEORDER" : "",
+ "PROBLEM":"",
+ "SATTIME":"",
+ "EXECTIME": "",
+ "TUNERNUMBER":""
+ }
+ try:
+ loadTunerNumber(row, argprocess.getFolder() + "/tunernum" + str(i))
+ loadTunerInfo(row, argprocess.getFolder()+"/tuner"+str(i)+"used")
+ loadSolverTime(row, argprocess.getFolder()+"/log"+str(i))
+ loadProblemName(row, argprocess.getFolder()+"/problem"+str(i))
+ data.append(dump(file, row))
+ rows.append(row)
+ except IOError:
+ break
+ i += 1
+ return rows, data
+
+def tunerCountAnalysis(file, rows):
+ global TUNABLEHEADER
+ global PROBLEMS
+ tunercount = {}
+ tunernumber = {}
+ for row in rows:
+ mystr=""
+ for i in range(18):
+ if not row[TUNABLEHEADER[i]]:
+ mystr += "."
+ else:
+ mystr+=row[TUNABLEHEADER[i]]
+ if mystr not in tunercount:
+ tunercount.update({mystr : 1})
+ tunernumber.update({mystr : str(row["TUNERNUMBER"])})
+ else :
+ tunercount[mystr] += 1
+ tunernumber[mystr] += "-" + str(row["TUNERNUMBER"])
+
+ problems = set(map(lambda x: x["PROBLEM"], rows))
+ print ("Number of repititive tuners")
+ for key in tunercount:
+ if tunercount[key] > 1:
+ print( key + "(ids:" + tunernumber[key] + ") = #" + str(tunercount[key]) )
+
+def combineRowForEachTuner(rows):
+ global PROBLEMS
+ newRows = []
+ combined = None
+ for row in rows:
+ if row["PROBLEM"] == PROBLEMS[0]:
+ combined = row
+ for key in row:
+ if row[key]:
+ combined[key] = row[key]
+ if row["PROBLEM"] == PROBLEMS[len(PROBLEMS)-1]:
+ newRows.append(combined)
+ return newRows
+
+def transformDataset(rows):
+ print(rows)
+
+
+def main():
+ global TUNABLEHEADER
+ file = open("tuner.csv", "w")
+ rows, data = analyzeLogs(file)
+ tunerCountAnalysis(file, combineRowForEachTuner(rows) )
+ file.close()
+ #transformDataset(data)
+ pl.plot(data, TUNABLEHEADER)
+
+
+if __name__ == "__main__":
+ main()
CCSOLVER(solver)->mustHaveValue( (Element *) element);
}
+void setInterpreter(void *solver, unsigned int type){
+ CCSOLVER(solver)->setInterpreter((InterpreterType)type);
+}
+
void *clone(void *solver) {
return CCSOLVER(solver)->clone();
}
\ No newline at end of file
void printConstraints(void *solver);
void serialize(void *solver);
void mustHaveValue(void *solver, void *element);
+void setAlloyEncoder(void *solver);
void *clone(void *solver);
#ifdef __cplusplus
}
class BooleanLogic;
class Serializer;
class ElementFunction;
+class Interpreter;
typedef uint64_t VarType;
typedef unsigned int uint;
class DOREdge;
class AutoTuner;
+class CompTuner;
class SearchTuner;
class TunableSetting;
+class SerializeTuner;
+
class TunableDesc;
-class TunableDependent;
class OrderResolver;
class DecomposeOrderResolver;
class EncodingNode;
class EncodingEdge;
class EncodingSubGraph;
-
+class SignatureEnc;
+class Signature;
+class ValuedSignature;
+class AlloyElementSig;
+class AlloySetSig;
+class AlloyBoolSig;
struct IncrementalSolver;
typedef struct IncrementalSolver IncrementalSolver;
struct TableEntry;
#include "config.h"
#include "time.h"
+#define NANOSEC 1000000000.0
#if 0
extern int model_out;
//#define CONFIG_DEBUG
#endif
-//#define STATICENCGEN
-
#ifndef CONFIG_ASSERT
#define CONFIG_ASSERT
#endif
#include "varorderingopt.h"
#include <time.h>
#include <stdarg.h>
+#include "alloyinterpreter.h"
+#include "smtinterpreter.h"
+#include "mathsatinterpreter.h"
+#include "smtratinterpreter.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
boolFalse(boolTrue.negate()),
unsat(false),
+ booleanVarUsed(false),
tuner(NULL),
elapsedTime(0),
- satsolverTimeout(NOTIMEOUT)
+ satsolverTimeout(NOTIMEOUT),
+ interpreter(NULL)
{
satEncoder = new SATEncoder(this);
}
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
}
+
+ if(interpreter != NULL){
+ delete interpreter;
+ }
delete boolTrue.getBoolean();
delete satEncoder;
boolTrue = BooleanEdge(new BooleanConst(true));
boolFalse = boolTrue.negate();
unsat = false;
+ booleanVarUsed = false;
elapsedTime = 0;
tuner = NULL;
satEncoder->resetSATEncoder();
return copy;
}
-CSolver *CSolver::deserialize(const char *file) {
+CSolver *CSolver::deserialize(const char *file, InterpreterType itype) {
model_print("deserializing %s ...\n", file);
- Deserializer deserializer(file);
+ Deserializer deserializer(file, itype);
return deserializer.deserialize();
}
BooleanEdge CSolver::getBooleanVar(VarType type) {
Boolean *boolean = new BooleanVar(type);
allBooleans.push(boolean);
+ if(!booleanVarUsed)
+ booleanVarUsed = true;
return BooleanEdge(boolean);
}
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
- BooleanEdge newarray[asize];
- switch (op) {
- case SATC_NOT: {
- return array[0].negate();
- }
- case SATC_IFF: {
- for (uint i = 0; i < 2; i++) {
- if (isTrue(array[i])) { // It can be undefined
- return array[1 - i];
- } else if (isFalse(array[i])) {
- newarray[0] = array[1 - i];
- return applyLogicalOperation(SATC_NOT, newarray, 1);
- } else if (array[i]->type == LOGICOP) {
- BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
- if (b->replaced) {
- return rewriteLogicalOperation(op, array, asize);
+ if(!useInterpreter()){
+ BooleanEdge newarray[asize];
+ switch (op) {
+ case SATC_NOT: {
+ return array[0].negate();
+ }
+ case SATC_IFF: {
+ for (uint i = 0; i < 2; i++) {
+ if (isTrue(array[i])) { // It can be undefined
+ return array[1 - i];
+ } else if (isFalse(array[i])) {
+ newarray[0] = array[1 - i];
+ return applyLogicalOperation(SATC_NOT, newarray, 1);
+ } else if (array[i]->type == LOGICOP) {
+ BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
+ if (b->replaced) {
+ return rewriteLogicalOperation(op, array, asize);
+ }
}
}
+ break;
}
- break;
- }
- case SATC_OR: {
- for (uint i = 0; i < asize; i++) {
- newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
+ case SATC_OR: {
+ for (uint i = 0; i < asize; i++) {
+ newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
+ }
+ return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
}
- return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
- }
- case SATC_AND: {
- uint newindex = 0;
- for (uint i = 0; i < asize; i++) {
- BooleanEdge b = array[i];
- if (b->type == LOGICOP) {
- if (((BooleanLogic *)b.getBoolean())->replaced)
- return rewriteLogicalOperation(op, array, asize);
+ case SATC_AND: {
+ uint newindex = 0;
+ for (uint i = 0; i < asize; i++) {
+ BooleanEdge b = array[i];
+ if (b->type == LOGICOP) {
+ if (((BooleanLogic *)b.getBoolean())->replaced)
+ return rewriteLogicalOperation(op, array, asize);
+ }
+ if (isTrue(b))
+ continue;
+ else if (isFalse(b)) {
+ return boolFalse;
+ } else
+ newarray[newindex++] = b;
+ }
+ if (newindex == 0) {
+ return boolTrue;
+ } else if (newindex == 1) {
+ return newarray[0];
+ } else {
+ bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
+ array = newarray;
+ asize = newindex;
}
- if (isTrue(b))
- continue;
- else if (isFalse(b)) {
- return boolFalse;
- } else
- newarray[newindex++] = b;
+ break;
+ }
+ case SATC_XOR: {
+ //handle by translation
+ return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
+ }
+ case SATC_IMPLIES: {
+ //handle by translation
+ return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
}
- if (newindex == 0) {
- return boolTrue;
- } else if (newindex == 1) {
- return newarray[0];
+ }
+
+ ASSERT(asize != 0);
+ Boolean *boolean = new BooleanLogic(this, op, array, asize);
+ Boolean *b = boolMap.get(boolean);
+ if (b == NULL) {
+ boolean->updateParents();
+ boolMap.put(boolean, boolean);
+ allBooleans.push(boolean);
+ return BooleanEdge(boolean);
} else {
- bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
- array = newarray;
- asize = newindex;
+ delete boolean;
+ return BooleanEdge(b);
}
- break;
- }
- case SATC_XOR: {
- //handle by translation
- return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
- }
- case SATC_IMPLIES: {
- //handle by translation
- return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
- }
- }
-
- ASSERT(asize != 0);
- Boolean *boolean = new BooleanLogic(this, op, array, asize);
- Boolean *b = boolMap.get(boolean);
- if (b == NULL) {
- boolean->updateParents();
- boolMap.put(boolean, boolean);
+ } else {
+ ASSERT(asize != 0);
+ Boolean *boolean = new BooleanLogic(this, op, array, asize);
allBooleans.push(boolean);
return BooleanEdge(boolean);
- } else {
- delete boolean;
- return BooleanEdge(b);
+
}
}
}
}
Boolean *constraint = new BooleanOrder(order, first, second);
- Boolean *b = boolMap.get(constraint);
-
- if (b == NULL) {
- allBooleans.push(constraint);
- boolMap.put(constraint, constraint);
- constraint->updateParents();
- if (order->graph != NULL) {
- OrderGraph *graph = order->graph;
- OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
- if (from != NULL) {
- OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
- if (to != NULL) {
- OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
- OrderEdge *invedge;
-
- if (edge != NULL && edge->mustPos) {
- replaceBooleanWithTrueNoRemove(constraint);
- } else if (edge != NULL && edge->mustNeg) {
- replaceBooleanWithFalseNoRemove(constraint);
- } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
- && invedge->mustPos) {
- replaceBooleanWithFalseNoRemove(constraint);
+ if (!useInterpreter() ){
+ Boolean *b = boolMap.get(constraint);
+
+ if (b == NULL) {
+ allBooleans.push(constraint);
+ boolMap.put(constraint, constraint);
+ constraint->updateParents();
+ if ( order->graph != NULL) {
+ OrderGraph *graph = order->graph;
+ OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
+ if (from != NULL) {
+ OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
+ if (to != NULL) {
+ OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
+ OrderEdge *invedge;
+
+ if (edge != NULL && edge->mustPos) {
+ replaceBooleanWithTrueNoRemove(constraint);
+ } else if (edge != NULL && edge->mustNeg) {
+ replaceBooleanWithFalseNoRemove(constraint);
+ } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+ && invedge->mustPos) {
+ replaceBooleanWithFalseNoRemove(constraint);
+ }
}
}
}
+ } else {
+ delete constraint;
+ constraint = b;
}
- } else {
- delete constraint;
- constraint = b;
}
-
BooleanEdge be = BooleanEdge(constraint);
return negate ? be.negate() : be;
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (isTrue(constraint))
- return;
- else if (isFalse(constraint)) {
- setUnSAT();
- }
- else {
- if (constraint->type == LOGICOP) {
- BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
- if (!constraint.isNegated()) {
- if (b->op == SATC_AND) {
- uint size = b->inputs.getSize();
- //Handle potential concurrent modification
- BooleanEdge array[size];
- for (uint i = 0; i < size; i++) {
- array[i] = b->inputs.get(i);
- }
- for (uint i = 0; i < size; i++) {
- addConstraint(array[i]);
+ if(!useInterpreter()){
+ if (isTrue(constraint))
+ return;
+ else if (isFalse(constraint)) {
+ setUnSAT();
+ }
+ else {
+ if (constraint->type == LOGICOP) {
+ BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
+ if (!constraint.isNegated()) {
+ if (b->op == SATC_AND) {
+ uint size = b->inputs.getSize();
+ //Handle potential concurrent modification
+ BooleanEdge array[size];
+ for (uint i = 0; i < size; i++) {
+ array[i] = b->inputs.get(i);
+ }
+ for (uint i = 0; i < size; i++) {
+ addConstraint(array[i]);
+ }
+ return;
}
+ }
+ if (b->replaced) {
+ addConstraint(doRewrite(constraint));
return;
}
}
- if (b->replaced) {
- addConstraint(doRewrite(constraint));
- return;
+ constraints.add(constraint);
+ Boolean *ptr = constraint.getBoolean();
+
+ if (ptr->boolVal == BV_UNSAT) {
+ setUnSAT();
}
- }
- constraints.add(constraint);
- Boolean *ptr = constraint.getBoolean();
- if (ptr->boolVal == BV_UNSAT) {
- setUnSAT();
+ replaceBooleanWithTrueNoRemove(constraint);
+ constraint->parents.clear();
}
-
- replaceBooleanWithTrueNoRemove(constraint);
+ } else{
+ constraints.add(constraint);
constraint->parents.clear();
}
}
}
}
-#define NANOSEC 1000000000.0
int CSolver::solve() {
long long startTime = getTimeNano();
bool deleteTuner = false;
tuner = new DefaultTuner();
deleteTuner = true;
}
-
-
- {
- SetIteratorOrder *orderit = activeOrders.iterator();
- while (orderit->hasNext()) {
- Order *order = orderit->next();
- if (order->graph != NULL) {
- delete order->graph;
- order->graph = NULL;
+ int result = IS_INDETER;
+ if(useInterpreter()){
+ interpreter->encode();
+ model_print("Problem encoded in Interpreter\n");
+ result = interpreter->solve();
+ model_print("Problem solved by Interpreter\n");
+ } else{
+
+ {
+ SetIteratorOrder *orderit = activeOrders.iterator();
+ while (orderit->hasNext()) {
+ Order *order = orderit->next();
+ if (order->graph != NULL) {
+ delete order->graph;
+ order->graph = NULL;
+ }
}
+ delete orderit;
}
- delete orderit;
- }
- computePolarities(this);
- long long time1 = getTimeNano();
- model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
- Preprocess pp(this);
- pp.doTransform();
- long long time2 = getTimeNano();
- model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
+ computePolarities(this);
+ long long time1 = getTimeNano();
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+ Preprocess pp(this);
+ pp.doTransform();
+ long long time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
- DecomposeOrderTransform dot(this);
- dot.doTransform();
- time1 = getTimeNano();
- model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
- IntegerEncodingTransform iet(this);
- iet.doTransform();
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
- ElementOpt eop(this);
- eop.doTransform();
+ ElementOpt eop(this);
+ eop.doTransform();
- EncodingGraph eg(this);
- eg.encode();
+ EncodingGraph eg(this);
+ eg.encode();
- naiveEncodingDecision(this);
-// eg.validate();
+ naiveEncodingDecision(this);
+ // eg.validate();
- VarOrderingOpt bor(this, satEncoder);
- bor.doTransform();
-
- time2 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
- satEncoder->encodeAllSATEncoder(this);
- time1 = getTimeNano();
+ VarOrderingOpt bor(this, satEncoder);
+ bor.doTransform();
- model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
- model_print("Is problem UNSAT after encoding: %d\n", unsat);
- int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
- model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : result == IS_INDETER? "INDETERMINATE" : " UNSAT");
- time2 = getTimeNano();
- elapsedTime = time2 - startTime;
- model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ satEncoder->encodeAllSATEncoder(this);
+ time1 = getTimeNano();
+
+ model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
+ model_print("Is problem UNSAT after encoding: %d\n", unsat);
+
+
+ result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
+ model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
+ time2 = getTimeNano();
+ elapsedTime = time2 - startTime;
+ model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ }
if (deleteTuner) {
delete tuner;
tuner = NULL;
return result;
}
+void CSolver::setInterpreter(InterpreterType type){
+ if(interpreter == NULL){
+ switch(type){
+ case SATUNE:
+ break;
+ case ALLOY:{
+ interpreter = new AlloyInterpreter(this);
+ break;
+ }case Z3:{
+ interpreter = new SMTInterpreter(this);
+ break;
+ }
+ case MATHSAT:{
+ interpreter = new MathSATInterpreter(this);
+ break;
+ }
+ case SMTRAT:{
+ interpreter = new SMTRatInterpreter(this);
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+ }
+}
+
void CSolver::printConstraints() {
SetIteratorBooleanEdge *it = getConstraints();
while (it->hasNext()) {
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return getElementValueSATTranslator(this, element);
+ return useInterpreter()? interpreter->getValue(element):
+ getElementValueSATTranslator(this, element);
default:
ASSERT(0);
}
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
- return getBooleanVariableValueSATTranslator(this, boolean);
+ return useInterpreter()? interpreter->getBooleanValue(boolean):
+ getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);
}
bool isFalse(BooleanEdge b);
void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
- void setSatSolverTimeout(long seconds){ satsolverTimeout = seconds;}
+ void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
bool isUnSAT() { return unsat; }
-
+ bool isBooleanVarUsed(){return booleanVarUsed;}
void printConstraint(BooleanEdge boolean);
void printConstraints();
void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
CSolver *clone();
void serialize();
- static CSolver *deserialize(const char *file);
+ static CSolver *deserialize(const char *file, InterpreterType itype = SATUNE);
void autoTune(uint budget);
void inferFixedOrders();
void inferFixedOrder(Order *order);
-
-
+ void setInterpreter(InterpreterType type);
+ bool useInterpreter() {return interpreter != NULL;}
void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
long long getSolveTime();
+ long getSatSolverTimeout() { return satsolverTimeout;}
CMEMALLOC;
SATEncoder *satEncoder;
bool unsat;
- Tuner *tuner;
+ bool booleanVarUsed;
+ Tuner *tuner;
long long elapsedTime;
- long satsolverTimeout;
+ long satsolverTimeout;
+ Interpreter *interpreter;
friend class ElementOpt;
- friend class VarOrderingOpt;
+ friend class VarOrderingOpt;
};
inline CompOp flipOp(CompOp op) {
+++ /dev/null
-#!/bin/bash
-# run as the following:
-# ./learn.sh [hexiom]
-# ./learn.sh [nqueens]
-# ./learn.sh [sudoku-csolver]
-# ./learn.sh [killerSudoku]
-
-
-
-BIN=./bin
-DUMP=$(find . -name "*.dump")
-cd $BIN
-for d in $DUMP; do
- if [[ $d = *$@* ]]; then
- echo $d
- ./run.sh deserializerautotune "."$d
- fi
-done
csolverlb.clone.restype = c_void_p
csolverlb.serialize.argtypes = [c_void_p]
csolverlb.serialize.restype = None
+ csolverlb.setInterpreter.argtypes = [c_void_p, c_uint]
+ csolverlb.setInterpreter.restype = None
return csolverlb
--- /dev/null
+#!/bin/bash
+# run as the following:
+# ./runbench.sh [hexiom] [timeout] [tuner.conf]
+# ./runbench.sh [nqueens] [timeout] [tuner.conf]
+# ./runbench.sh [sudoku-csolver] [timeout] [tuner.conf]
+# ./runbench.sh [killerSudoku] [timeout] [tuner.conf]
+
+if [ "$#" -lt 3 ]; then
+ echo "Illegal number of argument"
+ echo "./runbench.sh [benchmark] [timeout] [tuner.conf]"
+ exit 1
+fi
+
+
+BIN=./bin
+DUMP=$(find . -name "*.dump")
+cd $BIN
+for d in $DUMP; do
+ if [[ $d = *$1* ]]; then
+ echo $d
+ ./run.sh tunerrun "."$d $2 "../"$3 out.out
+ echo "Best tuner"
+ fi
+done
--- /dev/null
+#!/bin/bash
+
+#Terminate the script if even one command fails
+#set -e
+
+SATSOLVER=sat_solver
+CSOLVER=runcomptuner
+DESERALIZE=deserializerun
+MONITOR=tunermonitor
+SLEEPTIME=10
+FILE=monitor.log
+
+
+kill -9 `jobs -ps` &>$FILE
+
+while true; do
+ date >> $FILE
+ free >> $FILE
+ ps aux | grep $SATSOLVER | grep -v "grep" >> $FILE
+ ps aux | grep $CSOLVER | grep -v "run.sh" | grep -v "grep" >> $FILE
+ ps aux | grep $DESERALIZE | grep -v "run.sh" | grep -v "grep" >> $FILE
+ ps aux | grep $MONITOR | grep -v "grep" >> $FILE
+ echo "*************************" >> $FILE
+ sleep $SLEEPTIME
+done
projects / satune.git / commitdiff