package hu.webarticum.jsatbuilder.solver.sat4j;

import java.util.List;

import org.sat4j.core.VecInt;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

import hu.webarticum.jsatbuilder.solver.core.AbstractSolver;
import hu.webarticum.jsatbuilder.solver.core.Solver;

abstract public class AbstractSat4jSolver extends AbstractSolver {
    
    protected volatile ISolver solver = null;
    
    @Override
    public boolean run() {
        status = STATUS.RUNNING;
        buildSolver();
        status = runSolver();
        return (status==STATUS.SAT);
    }
    
    @Override
    synchronized public void close() {
        if (solver!=null) {
            if (status == STATUS.RUNNING) {
                solver.expireTimeout();
                status = STATUS.ABORTED;
            }
            solver.reset();
        }
    }
    
    protected void buildSolver() {
        getSat4jSolver();
        solver.setTimeout(getTimeout());
        solver.newVar(variables.size());
        
        try {
            fillSolver();
        } catch (Exception e) {
            messages.add("Exception: " + e.getLocalizedMessage());
            status = STATUS.UNSAT;
            solver.reset();
            return;
        }
    }
    
    protected void fillSolver() throws Exception {
        List<Solver.Clause> _normalClauses = getNormalClausesForDecision();
        for (Clause clause: _normalClauses) {
            solver.addClause(createSat4jVecInt(clause));
        }
        for (SpecialClauseWrapper specialClauseWrapper: specialClauseWrappers) {
            if (specialClauseWrapper.minimum != null && specialClauseWrapper.maximum != null) {
                if (specialClauseWrapper.minimum.intValue() == specialClauseWrapper.maximum.intValue()) {
                    solver.addExactly(createSat4jVecInt(specialClauseWrapper.clause), specialClauseWrapper.minimum);
                } else {
                    solver.addAtLeast(createSat4jVecInt(specialClauseWrapper.clause), specialClauseWrapper.minimum);
                    solver.addAtMost(createSat4jVecInt(specialClauseWrapper.clause), specialClauseWrapper.maximum);
                }
            } else if (specialClauseWrapper.minimum != null) {
                solver.addAtLeast(createSat4jVecInt(specialClauseWrapper.clause), specialClauseWrapper.minimum);
            } else if (specialClauseWrapper.maximum != null) {
                solver.addAtMost(createSat4jVecInt(specialClauseWrapper.clause), specialClauseWrapper.maximum);
            } else {
                solver.addClause(createSat4jVecInt(specialClauseWrapper.clause));
            }
        }
    }

    protected STATUS runSolver() {
        model = new Model();
        
        boolean solved;
        try {
            solved = solver.isSatisfiable();
        } catch (TimeoutException e) {
            if (status == STATUS.ABORTED) {
                messages.add("Aborted");
            } else {
                messages.add("Timeout reached: " + getTimeout());
            }
            return STATUS.ABORTED;
        }
        
        if (status == STATUS.ABORTED) {
            messages.add("Aborted");
            return STATUS.ABORTED;
        }
        
        if (!solved) {
            messages.add("Unsolvable");
            solver.reset();
            return STATUS.UNSAT;
        }
        
        for (int index: solver.model()) {
            model.put(variables.get(Math.abs(index) - 1), index > 0);
        }
        
        return STATUS.SAT;
    }
    
    protected VecInt createSat4jVecInt(Clause clause) {
        List<Literal> literals = clause.getLiterals();
        int[] literalArray = new int[literals.size()];
        int i = 0;
        for (Literal literal: literals) {
            Object variable = literal.getVariable();
            int value = variables.indexOf(variable)+1;
            if (!literal.isPositive()) {
                value = -value;
            }
            literalArray[i] = value;
            i++;
        }
        return new VecInt(literalArray);
    }

    protected int getTimeout() {
        return 100000;
    }

    public ISolver getSat4jSolver() {
        if (solver == null) {
            solver = createSolver();
        }
        return solver;
    }
    
    abstract protected ISolver createSolver();
    
}

@@ -2745,32 +2745,128 @@
 solved;%0A        
+%0A        if (status == STATUS.UNSAT) %7B%0A            solved = false;%0A        %7D else %7B%0A            
 try %7B%0A          
@@ -2859,32 +2859,36 @@
 y %7B%0A            
+  
+  
 solved = solver.
@@ -2904,32 +2904,36 @@
 able();%0A        
+    
 %7D catch (Timeout
@@ -2951,32 +2951,36 @@
 ) %7B%0A            
+   
+ 
 if (status == ST
@@ -3003,32 +3003,36 @@
                 
+    
 messages.add(%22Ab
@@ -3032,32 +3032,36 @@
 add(%22Aborted%22);%0A
+    
             %7D el
@@ -3073,32 +3073,36 @@
                 
+    
 messages.add(%22Ti
@@ -3139,32 +3139,36 @@
 ));%0A            
+    
 %7D%0A            re
@@ -3157,32 +3157,36 @@
   %7D%0A            
+ 
+   
 return STATUS.AB
@@ -3184,32 +3184,46 @@
 STATUS.ABORTED;%0A
+            %7D%0A
         %7D%0A      

Fix contradiction bug