Element::Element(ASTNodeType _type) :
ASTNode(_type),
encoding(this),
- anyValue(false) {
+ anyValue(false),
+ frozen(false){
}
ElementSet::ElementSet(Set *s) :
Vector<ASTNode *> parents;
ElementEncoding encoding;
inline ElementEncoding *getElementEncoding() { return &encoding; }
+ inline void freezeElement(){frozen = true;}
+ inline bool isFrozen(){return frozen;}
virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
virtual void serialize(Serializer *serializer) = 0;
virtual void print() = 0;
virtual Set *getRange() = 0;
CMEMALLOC;
bool anyValue;
+ bool frozen;
};
class ElementSet : public Element {
SetIteratorBooleanEdge *iterator = solver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
- if (constraint->type == PREDICATEOP)
+ if (!solver->isConstraintEncoded(constraint) && constraint->type == PREDICATEOP)
workList.push((BooleanPredicate *)constraint.getBoolean());
}
while (workList.getSize() != 0) {
addArrayClauseLiteral(cnf->solver, numliterals, literals);
}
+void freezeVariable(CNF *cnf, Edge e){
+ int literal = getEdgeVar(e);
+ freeze(cnf->solver, literal);
+}
+
void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
Node *andNode = cnfform.node_ptr;
int orvar = getEdgeVar(eorvar);
}
int solveCNF(CNF *cnf) {
- long long startTime = getTimeNano();
- finishedClauses(cnf->solver);
long long startSolve = getTimeNano();
model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
long long finishTime = getTimeNano();
- cnf->encodeTime = startSolve - startTime;
model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
cnf->solveTime = finishTime - startSolve;
model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
void addClause(CNF *cnf, uint numliterals, int *literals);
+void freezeVariable(CNF *cnf, Edge e);
Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
generateAnyValueBinaryValueEncoding(encoding);
}
+void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
+ ASSERT(encoding->element->frozen);
+ for(uint i=0; i< encoding->numVars; i++){
+ Edge e = encoding->variables[i];
+ ASSERT(edgeIsVarConst(e));
+ freezeVariable(cnf, e);
+ }
+}
+
void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
ASSERT(encoding->type == BINARYINDEX);
allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
int SATEncoder::solve(long timeout) {
cnf->solver->timeout = timeout;
+ long long startTime = getTimeNano();
+ finishedClauses(cnf->solver);
+ cnf->encodeTime = getTimeNano() - startTime;
+ if(solver->isIncrementalMode()){
+ solver->freezeElementsVariables();
+ }
return solveCNF(cnf);
}
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
- Edge c = encodeConstraintSATEncoder(constraint);
- addConstraintCNF(cnf, c);
+ if(!csolver->isConstraintEncoded(constraint)){
+ Edge c = encodeConstraintSATEncoder(constraint);
+ addConstraintCNF(cnf, c);
+ csolver->addEncodedConstraint(constraint);
+ }
}
delete iterator;
}
CNF *getCNF() { return cnf;}
long long getSolveTime() { return cnf->solveTime; }
long long getEncodeTime() { return cnf->encodeTime; }
+ void freezeElementVariables(ElementEncoding *encoding);
CMEMALLOC;
private:
--- /dev/null
+#include "csolver.h"
+
+#define INPUTSIZE 2
+#define DOMAINSIZE 3
+
+int main(int numargs, char **argv) {
+ CSolver *solver = new CSolver();
+ uint64_t set1[] = {3, 1, 2};
+ uint64_t set2[] = {3, 1, 7};
+ Set *s1 = solver->createSet(0, set1, DOMAINSIZE);
+ Set *s2 = solver->createSet(0, set2, DOMAINSIZE);
+ Element *e1 = solver->getElementVar(s1);
+ Element *e2 = solver->getElementVar(s2);
+ Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
+ Element *inputs[] = {e1, e2};
+ BooleanEdge b = solver->applyPredicate(equals, inputs, INPUTSIZE);
+ solver->addConstraint(b);
+ solver->freezeElement(e1);
+ solver->freezeElement(e2);
+ if (solver->solve() == 1){
+ int run = 1;
+ do{
+ printf("result %d: e1=%" PRIu64 " e2=%" PRIu64 "\n", run, solver->getElementValue(e1), solver->getElementValue(e2));
+ for(int i=0; i< INPUTSIZE; i++){
+ uint64_t val = solver->getElementValue(inputs[i]);
+ Element *econst = solver->getElementConst(0, val);
+ Element * tmpInputs[] = {inputs[i], econst};
+ BooleanEdge b = solver->applyPredicate(equals, tmpInputs, INPUTSIZE);
+ solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, b));
+ }
+ run++;
+ }while(solver->solveIncremental() == 1);
+ printf("After %d runs, there are no more models to find ...\n", run);
+ }else{
+ printf("UNSAT\n");
+ }
+ delete solver;
+}
boolFalse(boolTrue.negate()),
unsat(false),
booleanVarUsed(false),
+ incrementalMode(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();
}
}
}
+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());
+
+ 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;
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");
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) {
Set *getElementRange (Element *element);
void mustHaveValue(Element *element);
-
+
BooleanEdge getBooleanTrue();
BooleanEdge getBooleanFalse();
/** When everything is done, the client calls this function and then csolver starts to encode*/
int solve();
-
+ /**
+ * Incremental Solving for SATUNE.
+ * It only supports incremental solving for elements!
+ * No support for BooleanVar, BooleanOrder or using interpreters
+ * @return
+ */
+ int solveIncremental();
+
/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
uint64_t getElementValue(Element *element);
+ void freezeElement(Element *e);
+
/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
bool getBooleanValue(BooleanEdge boolean);
Tuner *getTuner() { return tuner; }
SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
-
+ bool isConstraintEncoded(BooleanEdge be) { return encodedConstraints.contains(be);}
+ void addEncodedConstraint(BooleanEdge be) {encodedConstraints.add(be);}
+
SATEncoder *getSATEncoder() {return satEncoder;}
void replaceBooleanWithTrue(BooleanEdge bexpr);
long long getEncodeTime();
long long getSolveTime();
long getSatSolverTimeout() { return satsolverTimeout;}
-
+ bool isIncrementalMode() {return incrementalMode;}
+ void freezeElementsVariables();
CMEMALLOC;
private:
void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
void handleFunction(ElementFunction *ef, BooleanEdge child);
-
+
//These two functions are helpers if the client has a pointer to a
//Boolean object that we have since replaced
BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
BooleanEdge doRewrite(BooleanEdge b);
/** This is a vector of constraints that must be satisfied. */
HashsetBooleanEdge constraints;
+ HashsetBooleanEdge encodedConstraints;
/** This is a vector of all boolean structs that we have allocated. */
Vector<Boolean *> allBooleans;
SATEncoder *satEncoder;
bool unsat;
bool booleanVarUsed;
+ bool incrementalMode;
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
projects / satune.git / commitdiff