Commit c4bcc516 authored by leberre's avatar leberre
Browse files

Avoid having a directory dependency to org.sat4j.minisat.SolverFactory in...

Avoid having a directory dependency to org.sat4j.minisat.SolverFactory in AllMuses to avoid cycles between sat4j.tools and sat4j.minisat. The AllMuses class now requires a solver factory as constructor parameter.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1695 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent d4a7671f
......@@ -101,7 +101,7 @@ public class MUSLauncher extends AbstractLauncher {
if (args.length == 2) {
// retrieve minimization strategy
if ("all".equals(args[0])) {
allMuses = new AllMUSes(highLevel);
allMuses = new AllMUSes(highLevel, SolverFactory.instance());
solver = allMuses.getSolverInstance();
} else {
String className = "org.sat4j.tools.xplain." + args[0]
......
......@@ -32,8 +32,8 @@ package org.sat4j.tools;
import java.util.ArrayList;
import java.util.List;
import org.sat4j.core.ASolverFactory;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
......@@ -52,22 +52,24 @@ public class AllMUSes {
private final List<IVecInt> mssList;
private final List<IVecInt> secondPhaseClauses;
private final List<IVecInt> musList;
private final ASolverFactory<? extends ISolver> factory;
public AllMUSes(boolean group) {
public AllMUSes(boolean group, ASolverFactory<? extends ISolver> factory) {
if (!group) {
this.css = new FullClauseSelectorSolver<ISolver>(
SolverFactory.newDefault(), false);
factory.defaultSolver(), false);
} else {
this.css = new GroupClauseSelectorSolver<ISolver>(
SolverFactory.newDefault());
factory.defaultSolver());
}
mssList = new ArrayList<IVecInt>();
musList = new ArrayList<IVecInt>();
secondPhaseClauses = new ArrayList<IVecInt>();
this.mssList = new ArrayList<IVecInt>();
this.musList = new ArrayList<IVecInt>();
this.secondPhaseClauses = new ArrayList<IVecInt>();
this.factory = factory;
}
public AllMUSes() {
this(false);
public AllMUSes(ASolverFactory<? extends ISolver> factory) {
this(false, factory);
}
/**
......@@ -95,7 +97,7 @@ public class AllMUSes {
if (secondPhaseClauses.isEmpty()) {
computeAllMSS();
}
ISolver solver = SolverFactory.newDefault();
ISolver solver = factory.defaultSolver();
for (IVecInt v : secondPhaseClauses) {
try {
solver.addClause(v);
......@@ -112,7 +114,7 @@ public class AllMUSes {
if (secondPhaseClauses.isEmpty()) {
computeAllMSS();
}
ISolver solver = SolverFactory.newDefault();
ISolver solver = factory.defaultSolver();
for (IVecInt v : secondPhaseClauses) {
try {
solver.addClause(v);
......
......@@ -36,6 +36,7 @@ import java.util.List;
import org.junit.Before;
import org.junit.Test;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
......@@ -49,7 +50,7 @@ public class TestAllMUSes {
@Before
public void setUp() throws Exception {
this.allMUSes = new AllMUSes();
this.allMUSes = new AllMUSes(SolverFactory.instance());
this.solver = allMUSes.getSolverInstance();
}
......
......@@ -36,6 +36,7 @@ import java.util.List;
import org.junit.Before;
import org.junit.Test;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
......@@ -50,7 +51,7 @@ public class TestAllMUSesAndCheckTest {
@Before
public void setUp() throws Exception {
this.allMUSes = new AllMUSes();
this.allMUSes = new AllMUSes(SolverFactory.instance());
this.solver = allMUSes.getSolverInstance();
this.checkListener = new CheckMUSSolutionListener();
}
......
......@@ -7,6 +7,7 @@ import java.util.List;
import org.junit.Before;
import org.junit.Test;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IGroupSolver;
import org.sat4j.specs.IVecInt;
......@@ -17,7 +18,7 @@ public class TestAllMUSesGroupTest {
@Before
public void setUp() throws Exception {
this.allMUSes = new AllMUSes(true);
this.allMUSes = new AllMUSes(true, SolverFactory.instance());
this.solver = allMUSes.getSolverInstance();
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment