/*
 *
 *  *  JavaSMT is an API wrapper for a collection of SMT solvers.
 *  *  This file is part of JavaSMT.
 *  *
 *  *  Copyright (C) 2007-2016  Dirk Beyer
 *  *  All rights reserved.
 *  *
 *  *  Licensed under the Apache License, Version 2.0 (the "License");
 *  *  you may not use this file except in compliance with the License.
 *  *  You may obtain a copy of the License at
 *  *
 *  *      http://www.apache.org/licenses/LICENSE-2.0
 *  *
 *  *  Unless required by applicable law or agreed to in writing, software
 *  *  distributed under the License is distributed on an "AS IS" BASIS,
 *  *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 *  *  See the License for the specific language governing permissions and
 *  *  limitations under the License.
 *
 *
 */

package org.sosy_lab.solver.basicimpl;

import org.sosy_lab.common.UniqueIdGenerator;
import org.sosy_lab.solver.api.BooleanFormula;
import org.sosy_lab.solver.api.BooleanFormulaManager;

import java.util.Random;

/**
 * Boolean fuzzer, useful for testing.
 */
public class Fuzzer {
  private final BooleanFormulaManager bfmgr;
  private final UniqueIdGenerator idGenerator;
  private static final String varNameTemplate = "VAR_";
  private BooleanFormula[] vars = new BooleanFormula[0];
  private final Random r = new Random();

  public Fuzzer(BooleanFormulaManager pBfmgr) {
    bfmgr = pBfmgr;
    idGenerator = new UniqueIdGenerator();
  }

  public BooleanFormula fuzz(int formulaSize, int maxNoVars) {
    vars = new BooleanFormula[maxNoVars];
    populateVars(maxNoVars);
    return recFuzz(formulaSize, maxNoVars);
  }

  private BooleanFormula recFuzz(int formulaSize, int maxNoVars) {
    if (formulaSize == 1) {
      return getVar(maxNoVars);
    } else {
      int pivot = formulaSize / 2;
      switch (r.nextInt(3)) {
        case 0:
          return bfmgr.or(recFuzz(pivot, maxNoVars), recFuzz(pivot, maxNoVars));
        case 1:
          return bfmgr.and(recFuzz(pivot, maxNoVars), recFuzz(pivot, maxNoVars));
        case 2:
          return bfmgr.not(recFuzz(formulaSize - 1, maxNoVars));
        default:
          throw new UnsupportedOperationException("Unexpected state");
      }
    }
  }

  private BooleanFormula getVar(int maxNoVars) {
    return vars[r.nextInt(maxNoVars)];
  }

  private void populateVars(int maxNoVars) {
    for (int i = 0; i < maxNoVars; i++) {
      vars[i] = getNewVar();
    }
  }

  private BooleanFormula getNewVar() {
    return bfmgr.makeVariable(varNameTemplate + idGenerator.getFreshId());
  }
}

@@ -1309,23 +1309,8 @@
 om r
- = new Random()
 ;%0A%0A 
@@ -1419,16 +1419,38 @@
 ator();%0A
+    r = new Random();%0A
   %7D%0A%0A  p
@@ -1610,27 +1610,145 @@
 mulaSize
-, maxNoVars
+);%0A  %7D%0A%0A  public BooleanFormula fuzz(int formulaSize, BooleanFormula... pVars) %7B%0A    vars = pVars;%0A    return recFuzz(formulaSize
 );%0A  %7D%0A%0A
@@ -1791,39 +1791,24 @@
  formulaSize
-, int maxNoVars
 ) %7B%0A    if (
@@ -1847,25 +1847,16 @@
  getVar(
-maxNoVars
 );%0A    %7D
@@ -1979,35 +1979,24 @@
 ecFuzz(pivot
-, maxNoVars
 ), recFuzz(p
@@ -1995,35 +1995,24 @@
 ecFuzz(pivot
-, maxNoVars
 ));%0A        
@@ -2059,27 +2059,16 @@
 zz(pivot
-, maxNoVars
 ), recFu
@@ -2075,27 +2075,16 @@
 zz(pivot
-, maxNoVars
 ));%0A    
@@ -2149,19 +2149,8 @@
  - 1
-, maxNoVars
 ));%0A
@@ -2288,29 +2288,16 @@
  getVar(
-int maxNoVars
 ) %7B%0A    
@@ -2318,25 +2318,27 @@
 nextInt(
-maxNoVars
+vars.length
 )%5D;%0A  %7D%0A

Update to fuzzer interface: allow to specify used variables.