edit

[satune.git] / src / Backend / nodeedge.c

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 340cdd0b3ed8735d4f6a38f3ff7b081a82f45168..634945365956d9441f14a59da127bdd9e7e582b6 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -4,7 +4,41 @@
 #include "inc_solver.h"
 #include "cnfexpr.h"
 
-/** Code ported from C++ BAT implementation of NICE-SAT */
+/* 
+V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
+Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.  If
+you download or use the software, send email to Pete Manolios
+(pete@ccs.neu.edu) with your name, contact information, and a short
+note describing what you want to use BAT for.  For any reuse or
+distribution, you must make clear to others the license terms of this
+work.
+
+Contact Pete Manolios if you want any of these conditions waived.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+*/
+
+/* 
+C port of CNF SAT Conversion Copyright Brian Demsky 2017. 
+*/
+
 
 VectorImpl(Edge, Edge, 16)
 
@@ -66,6 +100,7 @@ Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
        n->flags.wasExpanded=0;
        n->flags.cnfVisitedDown=0;
        n->flags.cnfVisitedUp=0;
+       n->flags.varForced=0;
        n->numEdges=numEdges;
        n->hashCode=hashcode;
        n->intAnnot[0]=0;n->intAnnot[1]=0;
@@ -102,7 +137,7 @@ Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
        uint hashvalue=type ^ numEdges;
        for(uint i=0;i<numEdges;i++) {
-               hashvalue ^= (uint) edges[i].node_ptr;
+               hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
                hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
        }
        return (uint) hashvalue;
@@ -157,7 +192,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 
        /** De-duplicate array */
        uint lowindex=0;
-       edges[lowindex++]=edges[initindex++];
+       edges[lowindex]=edges[initindex++];
 
        for(;initindex<numEdges;initindex++) {
                Edge e1=edges[lowindex];
@@ -167,8 +202,10 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
                                return E_False;
                        }
                } else
-                       edges[lowindex++]=edges[initindex];
+                       edges[++lowindex]=edges[initindex];
        }
+       lowindex++; //Make lowindex look like size
+       
        if (lowindex==1)
                return edges[0];
 
@@ -191,7 +228,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
                }
        }
        
-       return createNode(cnf, NodeType_AND, numEdges, edges);
+       return createNode(cnf, NodeType_AND, lowindex, edges);
 }
 
 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
@@ -280,6 +317,7 @@ Edge constraintNewVar(CNF *cnf) {
 void solveCNF(CNF *cnf) {
        countPass(cnf);
        convertPass(cnf, false);
+       finishedClauses(cnf->solver);
        solve(cnf->solver);
 }
 
@@ -293,12 +331,12 @@ void countPass(CNF *cnf) {
        deleteVectorEdge(ve);
 }
 
-void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
+void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
        //Skip constants and variables...
-       if (edgeIsVarConst(e))
+       if (edgeIsVarConst(eroot))
                return;
 
-       clearVectorEdge(stack);pushVectorEdge(stack, e);
+       clearVectorEdge(stack);pushVectorEdge(stack, eroot);
 
        bool isMatching=cnf->enableMatching;
        
@@ -512,7 +550,8 @@ void produceCNF(CNF * cnf, Edge e) {
        /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
        
        // propagate from positive to negative, negative to positive
-       propagate(cnf, & expPos, expNeg, true) || propagate(cnf, & expNeg, expPos, true);
+       if (!propagate(cnf, & expPos, expNeg, true))
+               propagate(cnf, & expNeg, expPos, true);
        
        // The polarity heuristic entails visiting the discovery polarity first
        if (isPosEdge(e)) {
@@ -526,7 +565,7 @@ void produceCNF(CNF * cnf, Edge e) {
 
 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
        if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
-               if (dest == NULL) {
+               if (*dest == NULL) {
                        *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                } else if (isProxy(*dest)) {
                        bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));