Z3 implements Solver { @Override public Optional<Map<Variable, Constant>> maxsat(List<Node> hard, List<Node> soft) { if (customFuMalikBound.isPresent()) { return customMaxsat(hard, soft, customFuMalikBound.get()); } else { return standardMaxsat(hard, soft); } } Z3(); void enableCustomMaxsatWithBound(int i); void disableCustomMaxsat(); @Override Optional<Map<Variable, Constant>> maxsat(List<Node> hard, List<Node> soft); @Override Optional<Map<Variable, Constant>> sat(List<Node> clauses);  }
@Test public void testMaxsat() { ArrayList<Node> hard = new ArrayList<>(); ProgramVariable x = ProgramVariable.mkInt("x"); ProgramVariable y = ProgramVariable.mkInt("y"); ProgramVariable a = ProgramVariable.mkBool("a"); ProgramVariable b = ProgramVariable.mkBool("b"); hard.add(new Equal(x, IntConst.of(1))); hard.add(new Equal(y, IntConst.of(2))); hard.add(new Or(a, new Equal(x, y))); hard.add(new Or(b, new LessOrEqual(x, y))); ArrayList<Node> soft = new ArrayList<>(); soft.add(new Not(a)); soft.add(new Not(b)); Optional<Map<Variable, Constant>> result = solver.maxsat(hard, soft); assertTrue(result.isPresent()); boolean aVal = ((BoolConst) result.get().get(a)).getValue(); boolean bVal = ((BoolConst) result.get().get(b)).getValue(); assertTrue(aVal || bVal); assertFalse(aVal && bVal); solver.enableCustomMaxsatWithBound(2); Optional<Map<Variable, Constant>> result2 = solver.maxsat(hard, soft); try { assertTrue(result2.isPresent()); boolean aVal2 = ((BoolConst) result2.get().get(a)).getValue(); boolean bVal2 = ((BoolConst) result2.get().get(b)).getValue(); assertTrue(aVal2 || bVal2); assertFalse(aVal2 && bVal2); } finally { solver.disableCustomMaxsat(); } }