void EncodingGraph::validate() {
- SetIteratorBooleanEdge* it= solver->getConstraints();
- while(it->hasNext()){
+ SetIteratorBooleanEdge *it = solver->getConstraints();
+ while (it->hasNext()) {
BooleanEdge be = it->next();
- if(be->type == PREDICATEOP){
+ if (be->type == PREDICATEOP) {
BooleanPredicate *b = (BooleanPredicate *)be.getBoolean();
- if(b->predicate->type == OPERATORPRED){
- PredicateOperator* predicate = (PredicateOperator*) b->predicate;
- if(predicate->getOp() == SATC_EQUALS){
+ if (b->predicate->type == OPERATORPRED) {
+ PredicateOperator *predicate = (PredicateOperator *) b->predicate;
+ if (predicate->getOp() == SATC_EQUALS) {
ASSERT(b->inputs.getSize() == 2);
- Element* e1= b->inputs.get(0);
- Element* e2= b->inputs.get(1);
- if(e1->type == ELEMCONST || e1->type == ELEMCONST)
+ Element *e1 = b->inputs.get(0);
+ Element *e2 = b->inputs.get(1);
+ if (e1->type == ELEMCONST || e1->type == ELEMCONST)
continue;
ElementEncoding *enc1 = e1->getElementEncoding();
ElementEncoding *enc2 = e2->getElementEncoding();
ASSERT(enc1->getElementEncodingType() != ELEM_UNASSIGNED);
ASSERT(enc2->getElementEncodingType() != ELEM_UNASSIGNED);
- if(enc1->getElementEncodingType() == enc2->getElementEncodingType() && enc1->getElementEncodingType() == BINARYINDEX && b->getFunctionEncoding()->type == CIRCUIT){
- for(uint i=0; i<enc1->encArraySize; i++){
- if(enc1->isinUseElement(i)){
+ if (enc1->getElementEncodingType() == enc2->getElementEncodingType() && enc1->getElementEncodingType() == BINARYINDEX && b->getFunctionEncoding()->type == CIRCUIT) {
+ for (uint i = 0; i < enc1->encArraySize; i++) {
+ if (enc1->isinUseElement(i)) {
uint64_t val1 = enc1->encodingArray[i];
- if(enc2->isinUseElement(i)){
+ if (enc2->isinUseElement(i)) {
ASSERT(val1 == enc2->encodingArray[i]);
- }else{
- for(uint j=0; j< enc2->encArraySize; j++){
- if(enc2->isinUseElement(j)){
+ } else {
+ for (uint j = 0; j < enc2->encArraySize; j++) {
+ if (enc2->isinUseElement(j)) {
ASSERT(val1 != enc2->encodingArray[j]);
}
}
}
}
//Now make sure that all the elements in the set are appeared in the encoding array!
- for(uint k=0; k< b->inputs.getSize(); k++){
+ for (uint k = 0; k < b->inputs.getSize(); k++) {
Element *e = b->inputs.get(k);
ElementEncoding *enc = e->getElementEncoding();
Set *s = e->getRange();
for (uint i = 0; i < s->getSize(); i++) {
uint64_t value = s->getElement(i);
- bool exist=false;
- for(uint j=0; j< enc->encArraySize; j++){
- if(enc->isinUseElement(j) && enc->encodingArray[j] == value){
+ bool exist = false;
+ for (uint j = 0; j < enc->encArraySize; j++) {
+ if (enc->isinUseElement(j) && enc->encodingArray[j] == value) {
exist = true;
break;
}
void EncodingGraph::encode() {
+ if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+ return;
+ buildGraph();
SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
- model_print("#SubGraph = %u", subgraphs.getSize());
+ model_print("#SubGraph = %u\n", subgraphs.getSize());
while (itesg->hasNext()) {
EncodingSubGraph *sg = itesg->next();
sg->encode();
ASSERT(encoding->isinUseElement(encodingIndex));
encoding->encodingArray[encodingIndex] = value;
}
- } else {
- model_print("DAMN in encode()\n");
- e->print();
}
}
break;
first->setEncoding(BINARYINDEX);
if (graph2 == NULL)
second->setEncoding(BINARYINDEX);
-
+
if (graph1 == NULL && graph2 == NULL) {
graph1 = new EncodingSubGraph();
subgraphs.add(graph1);
EncodingNode *tmp = left; left = right; right = tmp;
EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
}
- //model_print("Right=%p RGraph=%p\tLeft=%p LGraph=%p\n", right, rightGraph, left, leftGraph);
- uint leftSize = 0, rightSize = 0, newSize = 0, max = 0;
- uint64_t totalCost = 0;
+
+ uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
bool merge = false;
-// model_print("**************decideEdge*************\n");
-// model_print("LeftNode Size = %u\n", left->getSize());
-// model_print("rightNode Size = %u\n", right->getSize());
-// model_print("UnionSize = %u\n", left->s->getUnionSize(right->s));
-
if (leftGraph == NULL && rightGraph == NULL) {
leftSize = convertSize(left->getSize());
rightSize = convertSize(right->getSize());
newSize = convertSize(left->s->getUnionSize(right->s));
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;
- totalCost = (newSize - leftSize) * left->elements.getSize() +
- (newSize - rightSize) * right->elements.getSize();
- //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
- max = rightSize > leftSize ? rightSize : leftSize;
- if (newSize == max) {
- merge = true;
- }
} else if (leftGraph != NULL && rightGraph == NULL) {
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(right->getSize());
newSize = convertSize(leftGraph->estimateNewSize(right));
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
- totalCost = (newSize - leftSize) * leftGraph->numElements +
- (newSize - rightSize) * right->elements.getSize();
- //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
- max = rightSize > leftSize ? rightSize : leftSize;
- if (newSize == max) {
- merge = true;
- }
+ 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;
++// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
++ merge = left->measureSimilarity(right) > 1.5 || max == newSize;
} else {
//Neither are null
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(rightGraph->encodingSize);
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;
- // model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
- totalCost = (newSize - leftSize) * leftGraph->numElements +
- (newSize - rightSize) * rightGraph->numElements;
-// model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
-// model_print("RightGraph size=%u\n", rightGraph->encodingSize);
-// model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
- if (rightSize < 64 && leftSize < 64) {
- merge = true;
- }
+ 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;
}
-// model_print("******************************\n");
if (merge) {
//add the edge
mergeNodes(left, right);
return s->getSize();
}
+uint64_t EncodingNode::getIndex(uint index){
+ return s->getElement(index);
+}
+
VarType EncodingNode::getType() const {
return s->getType();
}
-static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+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){
+ uint common = 0;
+ for(uint i=0; i < s->getSize(); i++){
+ uint64_t item = s->getElement(i);
+ if(node->itemExists(item)){
+ 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();
+}
EncodingNode *EncodingGraph::createNode(Element *e) {
if (e->type == ELEMCONST)
#include "structs.h"
#include "graphstructs.h"
- #define FUDGEFACTOR 1.2
+ #define FUDGEFACTOR 1.2
#define CONVERSIONFACTOR 0.5
class EncodingGraph {
EncodingNode(Set *_s);
void addElement(Element *e);
uint getSize() const;
+ uint64_t getIndex(uint index);
VarType getType() const;
+ 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:
}
}
- void addClause(CNF *cnf, uint numliterals, int *literals){
+ void addClause(CNF *cnf, uint numliterals, int *literals) {
cnf->clausecount++;
addArrayClauseLiteral(cnf->solver, numliterals, literals);
}
if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
// proxy => expression
Edge cnfexpr = simplifyCNF(cnf, expression);
- Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
if (p == P_TRUE)
freeEdgeRec(expression);
outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
- outputCNFOR(cnf, cnfnegexpr, proxy);
freeEdgeCNF(cnfexpr);
- freeEdgeCNF(cnfnegexpr);
}
if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
// expression => proxy
Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
- Edge cnfexpr = simplifyCNF(cnf, expression);
freeEdgeRec(expression);
outputCNFOR(cnf, cnfnegexpr, proxy);
- outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
freeEdgeCNF(cnfnegexpr);
- freeEdgeCNF(cnfexpr);
}
}
#include "element.h"
#include "set.h"
#include "predicate.h"
-
+#include "csolver.h"
+#include "tunable.h"
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)
- generateAnyValueBinaryIndexEncoding(encoding);
+ if (encoding->element->anyValue){
+ uint setSize = encoding->element->getRange()->getSize();
+ uint encArraySize = encoding->encArraySize;
+ model_print("setSize=%u\tencArraySize=%u\n", setSize, encArraySize);
+ if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+ generateAnyValueBinaryIndexEncodingPositive(encoding);
+ } else {
- generateAnyValueBinaryIndexEncoding(encoding);
++ generateAnyValueBinaryIndexEncoding(encoding);
+ }
+ }
}
void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
}
}
+void SATEncoder::generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding) {
+ if (encoding->numVars == 0)
+ return;
+ Edge carray[encoding->encArraySize];
+ uint size = 0;
+ for (uint i = 0; i < encoding->encArraySize; i++) {
+ if (encoding->isinUseElement(i)) {
+ carray[size] = generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i);
+ size++;
+ }
+ }
+ addConstraintCNF(cnf, constraintOR(cnf, size, carray));
+}
+
void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
uint64_t minvalueminusoffset = encoding->low - encoding->offset;
uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
class SATEncoder {
public:
- int solve();
+ int solve(long timeout);
SATEncoder(CSolver *solver);
~SATEncoder();
void resetSATEncoder();
void generateElementEncoding(Element *element);
Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+ Edge encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint);
void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
Edge encodeOrderSATEncoder(BooleanOrder *constraint);
void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+ void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
CNF *cnf;
CSolver *solver;
#include "table.h"
#include "tableentry.h"
#include "order.h"
+#include "tunable.h"
#include <strings.h>
void naiveEncodingDecision(CSolver *This) {
SetIteratorBooleanEdge *iterator = This->getConstraints();
while (iterator->hasNext()) {
BooleanEdge b = iterator->next();
- naiveEncodingConstraint(b.getBoolean());
+ naiveEncodingConstraint(This, b.getBoolean());
}
delete iterator;
}
-void naiveEncodingConstraint(Boolean *This) {
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
switch (This->type) {
case BOOLEANVAR: {
return;
return;
}
case LOGICOP: {
- naiveEncodingLogicOp((BooleanLogic *) This);
+ naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
return;
}
case PREDICATEOP: {
- naiveEncodingPredicate((BooleanPredicate *) This);
+ naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
return;
}
default:
}
}
-void naiveEncodingLogicOp(BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
for (uint i = 0; i < This->inputs.getSize(); i++) {
- naiveEncodingConstraint(This->inputs.get(i).getBoolean());
+ naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
}
}
-void naiveEncodingPredicate(BooleanPredicate *This) {
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
FunctionEncoding *encoding = This->getFunctionEncoding();
if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
for (uint i = 0; i < This->inputs.getSize(); i++) {
Element *element = This->inputs.get(i);
- naiveEncodingElement(element);
+ naiveEncodingElement(csolver, element);
}
}
-void naiveEncodingElement(Element *This) {
+void naiveEncodingElement(CSolver *csolver, Element *This) {
ElementEncoding *encoding = This->getElementEncoding();
if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
- if(This->type != ELEMCONST){
+ if (This->type != ELEMCONST) {
model_print("INFO: naive encoder is making the decision about element %p....\n", This);
}
- encoding->setElementEncodingType(UNARY);
+ encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
encoding->encodingArrayInitialization();
}
ElementFunction *function = (ElementFunction *) This;
for (uint i = 0; i < function->inputs.getSize(); i++) {
Element *element = function->inputs.get(i);
- naiveEncodingElement(element);
+ naiveEncodingElement(csolver, element);
}
FunctionEncoding *encoding = function->getElementFunctionEncoding();
if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
}
void TunableSetting::print() {
+ model_print("Param %s = %u \t range=[%u,%u]", tunableParameterToString( (Tunables)param), selectedValue, lowValue, highValue);
if (hasVar) {
- model_print("VarType1 %" PRIu64 ", ", type1);
+ model_print("\tVarType1 %" PRIu64 ", ", type1);
model_print("VarType2 %" PRIu64 ", ", type2);
}
- model_print("Param %s = %u \t range=[%u,%u]\n", tunableParameterToString( (Tunables)param), selectedValue, lowValue, highValue);
+ model_print("\n");
}
unsigned int tunableSettingHash(TunableSetting *setting) {
setting1->param == setting2->param;
}
- ostream& operator<<(ostream& os, const TunableSetting& ts)
- {
- os << ts.hasVar <<" " << ts.type1 <<" " << ts.type2 << " " << ts.param << " " << ts.lowValue <<" "
- << ts.highValue << " " << ts.defaultValue << " " << ts.selectedValue;
- return os;
- }
+ ostream &operator<<(ostream &os, const TunableSetting &ts)
+ {
+ os << ts.hasVar << " " << ts.type1 << " " << ts.type2 << " " << ts.param << " " << ts.lowValue << " "
+ << ts.highValue << " " << ts.defaultValue << " " << ts.selectedValue;
+ return os;
+ }
SearchTuner::SearchTuner() {
ifstream myfile;
myfile.open (TUNEFILE, ios::in);
- if(myfile.is_open()){
+ if (myfile.is_open()) {
bool hasVar;
VarType type1;
VarType type2;
int highValue;
int defaultValue;
int selectedValue;
- while(myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue){
+ while (myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue) {
TunableSetting *setting;
-
- if(hasVar){
+
+ if (hasVar) {
setting = new TunableSetting(type1, type2, param);
- }else{
+ } else {
setting = new TunableSetting(param);
}
setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
boolFalse(boolTrue.negate()),
unsat(false),
tuner(NULL),
- elapsedTime(0)
+ elapsedTime(0),
+ satsolverTimeout(NOTIMEOUT)
{
satEncoder = new SATEncoder(this);
}
eop.doTransform();
EncodingGraph eg(this);
- eg.buildGraph();
eg.encode();
naiveEncodingDecision(this);
// eg.validate();
-
+
time2 = getTimeNano();
model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
satEncoder->encodeAllSATEncoder(this);
time1 = getTimeNano();
- model_print("Elapse Encode time: %f\n", (time1- startTime) / NANOSEC);
-
+ model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
model_print("Is problem UNSAT after encoding: %d\n", unsat);
- int result = unsat ? IS_UNSAT : satEncoder->solve();
- model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : " 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);
projects / satune.git / commitdiff