test_class.declarator: SEED = 1000L
test_class.modifier: private static final
test_class.original_string: private static final long SEED = 1000L;
test_class.type: long
test_class.var_name: SEED
test_class.file: sjsc/src/test/java/com/samsung/sjs/theorysolver/TheorySolverTest.java
test_class.identifier: TheorySolverTest
test_case.body: @Test
      public void testBasics() {
  
          List<Object> all = Arrays.asList("a", "b", "c", "d", "e", "f", "g", "h");
  
          for (int i = 0; i < 100; ++i) {
              Random r = new Random(SEED + i);
  
              Collection<Object> truthy = all.stream()
                      .filter(x -> r.nextBoolean())
                      .collect(Collectors.toSet());
  
              Theory<Object, Void> theory = positive -> {
                  Collection<Object> bad = positive.stream()
                          .filter(x -> !truthy.contains(x))
                          .collect(Collectors.toSet());
                  if (bad.size() > 0) {
                      // Construct a random, nonempty unsat core.
                      Collection<Object> unsat = new HashSet<>();
                      unsat.add(bad.iterator().next());
                      bad.stream().filter(x -> r.nextBoolean()).forEach(unsat::add);
                      return Either.right(unsat);
                  } else {
                      return Either.left(null);
                  }
              };
  
              Pair<Void, Collection<Object>> result = TheorySolver.solve(
                  theory, new SatFixingSetFinder<>(new Sat4J()),
                  Collections.emptyList(), all);
  
              Assert.assertEquals(all.size() - truthy.size(), result.getRight().size());
              Assert.assertEquals(truthy, all.stream().filter(x -> !result.getRight().contains(x)).collect(Collectors.toSet()));
          }
  
      }
test_case.class_method_signature: TheorySolverTest.testBasics()
test_case.full_signature: @Test public void testBasics()
test_case.identifier: testBasics
test_case.invocations: asList collect filter stream nextBoolean toSet collect filter stream contains toSet size add next iterator forEach filter stream nextBoolean right left solve emptyList assertEquals size size size getRight assertEquals collect filter stream contains getRight toSet
test_case.modifiers: @Test public
test_case.parameters: ()
test_case.return: void
test_case.signature: void testBasics()
focal_class.declarator: SHUFFLE = false
focal_class.modifier: private static final
focal_class.original_string: private static final boolean SHUFFLE = false;
focal_class.type: boolean
focal_class.var_name: SHUFFLE
focal_class.declarator: NOISY = true
focal_class.modifier: private static final
focal_class.original_string: private static final boolean NOISY = true;
focal_class.type: boolean
focal_class.var_name: NOISY
focal_class.file: sjsc/src/main/java/com/samsung/sjs/theorysolver/TheorySolver.java
focal_class.identifier: TheorySolver
focal_class.class_method_signature: TheorySolver.timed(Supplier<T> f, String msg)
focal_class.full_signature: private static T timed(Supplier<T> f, String msg)
focal_class.identifier: timed
focal_class.modifiers: private static
focal_class.parameters: (Supplier<T> f, String msg)
focal_class.return: T
focal_class.signature: T timed(Supplier<T> f, String msg)
focal_class.class_method_signature: TheorySolver.extendClause(int[] clause, int i)
focal_class.full_signature: static int[] extendClause(int[] clause, int i)
focal_class.identifier: extendClause
focal_class.modifiers: static
focal_class.parameters: (int[] clause, int i)
focal_class.return: int[]
focal_class.signature: int[] extendClause(int[] clause, int i)
focal_class.class_method_signature: TheorySolver.enumerateFixingSets(
              FixingSetFinder<Constraint> fixingSetFinder,
              Theory<Constraint, Model> theorySolver,
              Collection<Constraint> hardConstraints,
              Collection<Constraint> softConstraints,
              FixingSetListener<Constraint, Model> listener)
focal_class.full_signature: public static void enumerateFixingSets(
              FixingSetFinder<Constraint> fixingSetFinder,
              Theory<Constraint, Model> theorySolver,
              Collection<Constraint> hardConstraints,
              Collection<Constraint> softConstraints,
              FixingSetListener<Constraint, Model> listener)
focal_class.identifier: enumerateFixingSets
focal_class.modifiers: public static
focal_class.parameters: (
              FixingSetFinder<Constraint> fixingSetFinder,
              Theory<Constraint, Model> theorySolver,
              Collection<Constraint> hardConstraints,
              Collection<Constraint> softConstraints,
              FixingSetListener<Constraint, Model> listener)
focal_class.return: void
focal_class.signature: void enumerateFixingSets(
              FixingSetFinder<Constraint> fixingSetFinder,
              Theory<Constraint, Model> theorySolver,
              Collection<Constraint> hardConstraints,
              Collection<Constraint> softConstraints,
              FixingSetListener<Constraint, Model> listener)
focal_class.class_method_signature: TheorySolver.solve(
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_class.full_signature: public static Pair<Model, Collection<Constraint>> solve(
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_class.identifier: solve
focal_class.modifiers: public static
focal_class.parameters: (
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_class.return: Pair<Model, Collection<Constraint>>
focal_class.signature: Pair<Model, Collection<Constraint>> solve(
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_class.class_method_signature: TheorySolver.without(Collection<T> collection, T element)
focal_class.full_signature: private static Collection<T> without(Collection<T> collection, T element)
focal_class.identifier: without
focal_class.modifiers: private static
focal_class.parameters: (Collection<T> collection, T element)
focal_class.return: Collection<T>
focal_class.signature: Collection<T> without(Collection<T> collection, T element)
focal_class.class_method_signature: TheorySolver.minimizeFixingSet(
          Theory<Constraint, Model> theorySolver,
          List<Constraint> hardConstraints,
          List<Constraint> softConstraints,
          Model model,
          Collection<Constraint> fixingSet)
focal_class.full_signature: public static Pair<Model, Collection<Constraint>> minimizeFixingSet(
          Theory<Constraint, Model> theorySolver,
          List<Constraint> hardConstraints,
          List<Constraint> softConstraints,
          Model model,
          Collection<Constraint> fixingSet)
focal_class.identifier: minimizeFixingSet
focal_class.modifiers: public static
focal_class.parameters: (
          Theory<Constraint, Model> theorySolver,
          List<Constraint> hardConstraints,
          List<Constraint> softConstraints,
          Model model,
          Collection<Constraint> fixingSet)
focal_class.return: Pair<Model, Collection<Constraint>>
focal_class.signature: Pair<Model, Collection<Constraint>> minimizeFixingSet(
          Theory<Constraint, Model> theorySolver,
          List<Constraint> hardConstraints,
          List<Constraint> softConstraints,
          Model model,
          Collection<Constraint> fixingSet)
focal_class.class_method_signature: TheorySolver.loggingListener()
focal_class.full_signature: private static FixingSetListener<Constraint, Model> loggingListener()
focal_class.identifier: loggingListener
focal_class.modifiers: private static
focal_class.parameters: ()
focal_class.return: FixingSetListener<Constraint, Model>
focal_class.signature: FixingSetListener<Constraint, Model> loggingListener()
focal_method.body: 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());
              }
  
          }
  
      }
focal_method.class_method_signature: TheorySolver.solve(
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_method.full_signature: public static Pair<Model, Collection<Constraint>> solve(
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_method.identifier: solve
focal_method.invocations: loggingListener dummyListener setup isInterrupted currentThread addAll addAll removeAll timed check println onFixingSet of onCore collect filter stream contains toList isEmpty clear addCore timed currentFixingSet println size
focal_method.modifiers: public static
focal_method.parameters: (
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)
focal_method.return: Pair<Model, Collection<Constraint>>
focal_method.signature: Pair<Model, Collection<Constraint>> solve(
              Theory<Constraint, Model> theorySolver,
              FixingSetFinder<Constraint> fixingSetFinder,
              List<Constraint> hardConstraints,
              List<Constraint> softConstraints)