boolFalse(boolTrue.negate()),
unsat(false),
booleanVarUsed(false),
+ incrementalMode(false),
+ optimizationsOff(false),
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
allOrders.clear();
allFunctions.clear();
constraints.reset();
+ encodedConstraints.reset();
activeOrders.reset();
boolMap.reset();
elemMap.reset();
element->anyValue = true;
}
+void CSolver::freezeElementsVariables() {
+
+ for (uint i = 0; i < allElements.getSize(); i++) {
+ Element *e = allElements.get(i);
+ if (e->frozen) {
+ satEncoder->freezeElementVariables(&e->encoding);
+ }
+ }
+}
+
+
Set *CSolver::getElementRange (Element *element) {
return element->getRange();
}
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) {
return applyLogicalOperation(op, newarray, asize);
}
+BooleanEdge CSolver::applyAtMostOneConstraint (BooleanEdge *array, uint asize) {
+ if(asize == 0 || asize == 1){
+ return getBooleanTrue();
+ }
+ BooleanEdge newarray[asize*(asize-1)];
+ uint newsize = 0;
+ for (uint i = 0; i < asize -1; i++) {
+ for(uint j = i +1; j < asize; j++){
+ BooleanEdge oprand1 = array[i];
+ BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
+ newarray[newsize++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
+ }
+ }
+ return applyLogicalOperation(SATC_AND, newarray, newsize);
+}
+
+BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
+ BooleanEdge atleastOne = applyLogicalOperation(SATC_OR, array, asize);
+ BooleanEdge atmostOne = applyAtMostOneConstraint (array, asize);
+ return applyLogicalOperation(SATC_AND, atleastOne, atmostOne);
+}
+
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
- if (!useInterpreter()) {
+ if (!useInterpreter() && !optimizationsOff) {
BooleanEdge newarray[asize];
switch (op) {
case SATC_NOT: {
}
}
Boolean *constraint = new BooleanOrder(order, first, second);
- if (!useInterpreter() ) {
+ if (!useInterpreter() && !optimizationsOff ) {
Boolean *b = boolMap.get(constraint);
if (b == NULL) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (!useInterpreter()) {
+ if (!useInterpreter() && !optimizationsOff) {
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
}
}
+int CSolver::solveIncremental() {
+ if (isUnSAT()) {
+ return IS_UNSAT;
+ }
+
+
+ long long startTime = getTimeNano();
+ bool deleteTuner = false;
+ if (tuner == NULL) {
+ tuner = new DefaultTuner();
+ deleteTuner = true;
+ }
+ int result = IS_INDETER;
+ ASSERT (!useInterpreter());
+ if(!optimizationsOff){
+ 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);
+
+// IntegerEncodingTransform iet(this);
+// iet.doTransform();
+
+ //Doing element optimization on new constraints
+// ElementOpt eop(this);
+// eop.doTransform();
+
+ //Since no new element is added, we assuming adding new constraint
+ //has no impact on previous encoding decisions
+// EncodingGraph eg(this);
+// eg.encode();
+
+ naiveEncodingDecision(this);
+ // eg.validate();
+ //Order of sat solver variables don't change!
+// VarOrderingOpt bor(this, satEncoder);
+// bor.doTransform();
+
+ long long time2 = getTimeNano();
+ //Encoding newly added constraints
+ satEncoder->encodeAllSATEncoder(this);
+ long long 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;
+}
+
int CSolver::solve() {
if (isUnSAT()) {
return IS_UNSAT;
}
delete orderit;
}
+ long long time1, time2;
+
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);
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+ if(!optimizationsOff){
+ Preprocess pp(this);
+ pp.doTransform();
+ time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
- IntegerEncodingTransform iet(this);
- iet.doTransform();
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
- ElementOpt eop(this);
- eop.doTransform();
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
- EncodingGraph eg(this);
- eg.encode();
+ ElementOpt eop(this);
+ eop.doTransform();
+ EncodingGraph eg(this);
+ eg.encode();
+ }
naiveEncodingDecision(this);
// eg.validate();
-
- VarOrderingOpt bor(this, satEncoder);
- bor.doTransform();
-
- time2 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+ if(!optimizationsOff){
+ VarOrderingOpt bor(this, satEncoder);
+ bor.doTransform();
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+ }
satEncoder->encodeAllSATEncoder(this);
time1 = getTimeNano();
exit(-1);
}
+void CSolver::freezeElement(Element *e) {
+ e->freezeElement();
+ if (!incrementalMode) {
+ incrementalMode = true;
+ }
+}
+
bool CSolver::getBooleanValue(BooleanEdge bedge) {
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
projects / satune.git / blobdiff