#include "ordergraph.h"
#include "orderedge.h"
#include "orderanalysis.h"
+#include "elementopt.h"
#include <time.h>
#include <stdarg.h>
boolFalse(boolTrue.negate()),
unsat(false),
tuner(NULL),
- elapsedTime(0)
+ elapsedTime(0),
+ satsolverTimeout(NOTIMEOUT)
{
satEncoder = new SATEncoder(this);
}
}
CSolver *CSolver::deserialize(const char *file) {
- model_print("deserializing ...\n");
+ model_print("deserializing %s ...\n", file);
Deserializer deserializer(file);
return deserializer.deserialize();
}
return set;
}
-bool CSolver::itemExistInSet(Set *set, uint64_t item){
- return set->exists(item);
+bool CSolver::itemExistInSet(Set *set, uint64_t item) {
+ return set->exists(item);
}
VarType CSolver::getSetVarType(Set *set) {
return element;
}
-void CSolver::mustHaveValue(Element *element){
- element->getElementEncoding()->anyValue = true;
+void CSolver::mustHaveValue(Element *element) {
+ element->anyValue = true;
}
Set *CSolver::getElementRange (Element *element) {
Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
+ ASSERT(numArrays == 2);
Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
Element *e = elemMap.get(element);
if (e == NULL) {
}
}
-Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
- Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
+Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) {
+ Function *function = new FunctionOperator(op, range, overflowbehavior);
allFunctions.push(function);
return function;
}
-Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
- Predicate *predicate = new PredicateOperator(op, domain,numDomain);
+Predicate *CSolver::createPredicateOperator(CompOp op) {
+ Predicate *predicate = new PredicateOperator(op);
allPredicates.push(predicate);
return predicate;
}
return predicate;
}
-Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
- Table *table = new Table(domains,numDomain,range);
+Table *CSolver::createTable(Set *range) {
+ Table *table = new Table(range);
allTables.push(table);
return table;
}
-Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
- return createTable(domains, numDomain, NULL);
+Table *CSolver::createTableForPredicate() {
+ return createTable(NULL);
}
void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
- int t = 0;
setUnSAT();
}
else {
BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
if (!constraint.isNegated()) {
if (b->op == SATC_AND) {
- for (uint i = 0; i < b->inputs.getSize(); i++) {
- addConstraint(b->inputs.get(i));
+ 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;
}
#define NANOSEC 1000000000.0
int CSolver::solve() {
- long long starttime = getTimeNano();
+ long long startTime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
tuner = new DefaultTuner();
delete orderit;
}
computePolarities(this);
- long long time2 = getTimeNano();
- model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
+ long long time1 = getTimeNano();
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
Preprocess pp(this);
pp.doTransform();
- long long time3 = getTimeNano();
- model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+ long long time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
DecomposeOrderTransform dot(this);
dot.doTransform();
- long long time4 = getTimeNano();
- model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
IntegerEncodingTransform iet(this);
iet.doTransform();
+ ElementOpt eop(this);
+ eop.doTransform();
+
EncodingGraph eg(this);
- eg.buildGraph();
eg.encode();
naiveEncodingDecision(this);
- long long time5 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
+// eg.validate();
+
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
- long long startTime = getTimeNano();
satEncoder->encodeAllSATEncoder(this);
- long long endTime = getTimeNano();
+ time1 = getTimeNano();
- elapsedTime = endTime - startTime;
- model_print("Elapse Encode time: %f\n", elapsedTime / 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: %d\n", result);
-
+ 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);
if (deleteTuner) {
delete tuner;
tuner = NULL;
SetIteratorBooleanEdge *it = getConstraints();
while (it->hasNext()) {
BooleanEdge b = it->next();
- if (b.isNegated())
- model_print("!");
- b->print();
- model_print("\n");
+ b.print();
}
delete it;
}
void CSolver::printConstraint(BooleanEdge b) {
- if (b.isNegated())
- model_print("!");
- b->print();
- model_print("\n");
+ b.print();
}
uint64_t CSolver::getElementValue(Element *element) {
delete autotuner;
}
-//Set* CSolver::addItemsToRange(Element* element, uint num, ...){
-// va_list args;
-// va_start(args, num);
-// element->getRange()
-// uint setSize = set->getSize();
-// uint newSize = setSize+ num;
-// uint64_t members[newSize];
-// for(uint i=0; i<setSize; i++){
-// members[i] = set->getElement(i);
-// }
-// for( uint i=0; i< num; i++){
-// uint64_t arg = va_arg(args, uint64_t);
-// members[setSize+i] = arg;
-// }
-// va_end(args);
-// return createSet(set->getType(), members, newSize);
-//}
\ No newline at end of file
+