Edits to merge

[satune.git] / src / Backend / constraint.cc

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index df812dfe682918e3132ff3c2c1c6e71784cbbbd0..7c3a094701d3c12ffa08d5a3fba5c83dd6b3f4d8 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -4,6 +4,7 @@
 #include "inc_solver.h"
 #include "cnfexpr.h"
 #include "common.h"
+#include "qsort.h"
 /*
    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -59,6 +60,8 @@ CNF *createCNF() {
        initDefVectorEdge(&cnf->constraints);
        initDefVectorEdge(&cnf->args);
        cnf->solver = allocIncrementalSolver();
+       cnf->solveTime = 0;
+       cnf->encodeTime = 0;
        return cnf;
 }
 
@@ -82,6 +85,8 @@ void resizeCNF(CNF *cnf, uint newCapacity) {
        uint newMask = newCapacity - 1;
        for (uint i = 0; i < oldCapacity; i++) {
                Node *n = old_array[i];
+               if (n == NULL)
+                       continue;
                uint hashCode = n->hashCode;
                uint newindex = hashCode & newMask;
                for (;; newindex = (newindex + 1) & newMask) {
@@ -135,6 +140,7 @@ Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
                }
        }
        *n_ptr = allocNode(type, numEdges, edges, hashvalue);
+       cnf->size++;
        Edge e = {*n_ptr};
        return e;
 }
@@ -182,7 +188,7 @@ int comparefunction(const Edge *e1, const Edge *e2) {
 
 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
        ASSERT(numEdges != 0);
-       qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
+       bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
        uint initindex = 0;
        while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
                initindex++;
@@ -316,9 +322,11 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 
 void addConstraintCNF(CNF *cnf, Edge constraint) {
        pushVectorEdge(&cnf->constraints, constraint);
-       model_print("****ADDING NEW Constraint*****\n");
+#ifdef CONFIG_DEBUG
+       model_print("****SATC_ADDING NEW Constraint*****\n");
        printCNF(constraint);
        model_print("\n******************************\n");
+#endif
 }
 
 Edge constraintNewVar(CNF *cnf) {
@@ -328,10 +336,16 @@ Edge constraintNewVar(CNF *cnf) {
 }
 
 int solveCNF(CNF *cnf) {
+       long long startTime = getTimeNano();
        countPass(cnf);
        convertPass(cnf, false);
        finishedClauses(cnf->solver);
-       return solve(cnf->solver);
+       long long startSolve = getTimeNano();
+       int result = solve(cnf->solver);
+       long long finishTime = getTimeNano();
+       cnf->encodeTime = startSolve - startTime;
+       cnf->solveTime = finishTime - startSolve;
+       return result;
 }
 
 bool getValueCNF(CNF *cnf, Edge var) {
@@ -826,8 +840,8 @@ CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
                                int eL = argExp->litSize;                       // lits in argument
                                int aC = getClauseSizeCNF(accum);               // clauses in accum
                                int eC = getClauseSizeCNF(argExp);      // clauses in argument
-
-                               if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
+                               //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
+                               if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
                                        disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
                                } else {
                                        disjoinCNFExpr(accum, argExp, destroy);
@@ -885,26 +899,26 @@ Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
        return constraintAND(cnf, numvars, array);
 }
 
-Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
-       if(numvars == 0 )
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+       if (numvars == 0 )
                return E_False;
-       Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
+       Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
        for (uint i = 1; i < numvars; i++) {
                Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
-               Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); 
-               result = constraintOR2(cnf, lt, eq); 
+               Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+               result = constraintOR2(cnf, lt, eq);
        }
        return result;
 }
 
-Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
-       if(numvars == 0 )
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+       if (numvars == 0 )
                return E_True;
-       Edge result =constraintIMPLIES(cnf, var1[0], var2[0]);
+       Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
        for (uint i = 1; i < numvars; i++) {
                Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
-               Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); 
-               result = constraintOR2(cnf, lt, eq); 
+               Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+               result = constraintOR2(cnf, lt, eq);
        }
        return result;
 }