class TheorySolver {

    public static <Constraint, Model> Pair<Model, Collection<Constraint>> solve(
            Theory<Constraint, Model> theorySolver,
            FixingSetFinder<Constraint> fixingSetFinder,
            List<Constraint> hardConstraints,
            List<Constraint> softConstraints) {

        FixingSetListener<Constraint, Model> listener = NOISY ?
            loggingListener() :
            FixingSetListener.dummyListener();

        fixingSetFinder.setup(softConstraints);

        // These two are complements of each other:
        //    - fixingSet is the constraints we are going to remove
        //    - positive  is the constraints we are going to keep
        //      (i.e. all those not in the fixing set)
        Collection<Constraint> fixingSet = new ArrayList<>();
        Collection<Constraint> positive = new LinkedHashSet<>();
        for (;;) {

            // Be polite---interruptions mean that someone else wants
            // this thread to stop what it's doing.
            if (Thread.currentThread().isInterrupted()) {
                throw new RuntimeException("thread was interrupted");
            }

            positive.addAll(hardConstraints);
            positive.addAll(softConstraints);
            positive.removeAll(fixingSet);

            // Check the proposed fixing set against the theory.
            Either<Model, Collection<Constraint>> result =
                timed(() -> theorySolver.check(positive), "CHECKING THEORY");

            if (result.right == null) {
                // The proposed fixing set works! We are done!
                if (NOISY) System.out.println("VALID MODEL");
                listener.onFixingSet(result.left, fixingSet);
                return Pair.of(result.left, fixingSet);
            } else {
                // The proposed fixing set didn't work. We will use the core
                // to adjust what fixing set gets returned next.

                // Inform the listener
                listener.onCore(result.right);

                // The fixing set finder shouldn't care about hard constraints
                Collection<Constraint> softCore = result.right.stream()
                    .filter(c -> !hardConstraints.contains(c))
                    .collect(Collectors.toList());

                if (softCore.isEmpty()) {
                    throw new IllegalStateException("Hard clauses are unsat!");
                }

                // Push the core to the fixing set finder
                fixingSet.clear();
                fixingSetFinder.addCore(softCore);
                timed(() -> fixingSetFinder.currentFixingSet(fixingSet, listener),
                    "FINDING FIXING SET");
                System.out.println("  --> PROPOSAL SIZE = " + fixingSet.size());
            }

        }

    }

}