<commit_before>/**
 * @author <NAME>
 * @author <NAME>
 * @author <NAME>
 * Toyota InfoTechnology Center, USA
 * 465 N Bernardo Ave, Mountain View, CA 94043
 */
package dl.logicsolvers.abstractions;

import interfaces.text.*;
import java.util.*;
//import java.io.*;

import dl.semantics.*;
import dl.syntax.*;

public abstract class LogicSolverInterface {

// Basic ways to do "quantifier elimination"
	public abstract LogicSolverResult checkValidity( String filename, dLFormula thisFormula, String comment ) 
				throws Exception;
	 
// Basic ways to find an instance
	public abstract LogicSolverResult findInstance( String filename, List<dLFormula> theseFormulas, String comment ) 
				throws Exception;

// Convenient aliases for findInstance
	public LogicSolverResult findInstance( dLFormula thisFormula ) throws Exception {
		ArrayList<dLFormula> theseFormulas = new ArrayList<dLFormula>();
		theseFormulas.add( thisFormula );

		return findInstance( theseFormulas );
	}

	public LogicSolverResult findInstance( List<dLFormula> theseFormulas ) throws Exception {
		String filename = generateFilename();
		String comment = generateFindInstanceComment( theseFormulas );

		return findInstance( filename, theseFormulas, comment );
	}

	public LogicSolverResult findInstance( String filename, dLFormula thisFormula, String comment ) throws Exception {
		ArrayList<dLFormula> theseFormulas = new ArrayList<dLFormula>();
		theseFormulas.add( thisFormula );

		return findInstance( filename, theseFormulas, comment );
	}
// Even more convenient!
	public Valuation sample( dLFormula formula ) {
		ArrayList<dLFormula> formulas = new ArrayList<>();
		formulas.add( formula );
		return sample( formulas );
	}

	public Valuation sample( ArrayList<dLFormula> formulas ) {
		Valuation point = null;
		try {
			point = findInstance( formulas ).valuation;
		} catch ( Exception e ) {
			e.printStackTrace();
		} 

		return point;
	}

	public ArrayList<Valuation> multiSample( dLFormula formula, int numSamples, double resolution ) {
		ArrayList<dLFormula> formulas = new ArrayList<>();
		formulas.add( formula );

		return multiSample( formulas, numSamples, resolution );

	}
	public ArrayList<Valuation> clusterSample(dLFormula formula, int numSamples, ArrayList<Double> radii ) throws Exception {
		
		ArrayList<Valuation> points = multiSample(formula,numSamples,radii.get(0));
		for (int i=1;i<radii.size();i++)
		{
			points=clusterSampleBase(formula,points,numSamples,radii.get(i),radii.get(i-1));
		}
		return points;
	}
	
	protected ArrayList<Valuation> clusterSampleBase(dLFormula formula, ArrayList<Valuation> center_points,int numSamples, double SR, double BR) throws Exception{
		ArrayList<Valuation> points= new ArrayList<Valuation>();
		for (int i=0;i<center_points.size();i++)
		{
			points.addAll(multiSample(new AndFormula(formula,createBallExclusionFormula(center_points.get(i),new Real(BR)).negate()),numSamples,SR));
		}
		return points;
	}

	public ArrayList<Valuation> multiSample( List<dLFormula> thisSet, int numberOfPoints, double suggestedRadius ) {
                ArrayList<dLFormula> queryFormulas = new ArrayList<dLFormula>();
                ArrayList<Valuation> samplePoints = new ArrayList<Valuation>();
                Valuation thisPoint;

                queryFormulas.addAll( thisSet );

                for ( int i = 0; i < numberOfPoints; i++ ) { 
                        thisPoint = sample( queryFormulas );
                        if ( thisPoint != null && !thisPoint.isEmpty() ) { 
                                samplePoints.add( thisPoint );
                                try {
                                	queryFormulas.add( createBallExclusionFormula( thisPoint, new Real(suggestedRadius) ) );
                                } catch ( Exception e ) {
                                	e.printStackTrace();
				}
                                //System.out.println("Iteration: " + i + ";  Ball Exclusion Formula: " +
                                //                      createBallExclusionFormula( thisPoint, new Real(suggestedRadius) ).toMathematicaString() );

                        } else {
                                break;
                        }
                }<commit_msg>Parallelized clustersample<commit_after>/**
 * @author <NAME>
 * @author <NAME>
 * @author <NAME>
 * Toyota InfoTechnology Center, USA
 * 465 N Bernardo Ave, Mountain View, CA 94043
 */
package dl.logicsolvers.abstractions;

import interfaces.text.*;
import java.util.*;
import java.util.concurrent.Callable;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
import java.util.List;
//import java.io.*;

import dl.semantics.*;
import dl.syntax.*;

public abstract class LogicSolverInterface {

// Basic ways to do "quantifier elimination"
	public abstract LogicSolverResult checkValidity( String filename, dLFormula thisFormula, String comment ) 
				throws Exception;
	 
// Basic ways to find an instance
	public abstract LogicSolverResult findInstance( String filename, List<dLFormula> theseFormulas, String comment ) 
				throws Exception;

// Convenient aliases for findInstance
	public LogicSolverResult findInstance( dLFormula thisFormula ) throws Exception {
		ArrayList<dLFormula> theseFormulas = new ArrayList<dLFormula>();
		theseFormulas.add( thisFormula );

		return findInstance( theseFormulas );
	}

	public LogicSolverResult findInstance( List<dLFormula> theseFormulas ) throws Exception {
		String filename = generateFilename();
		String comment = generateFindInstanceComment( theseFormulas );

		return findInstance( filename, theseFormulas, comment );
	}

	public LogicSolverResult findInstance( String filename, dLFormula thisFormula, String comment ) throws Exception {
		ArrayList<dLFormula> theseFormulas = new ArrayList<dLFormula>();
		theseFormulas.add( thisFormula );

		return findInstance( filename, theseFormulas, comment );
	}
// Even more convenient!
	public Valuation sample( dLFormula formula ) {
		ArrayList<dLFormula> formulas = new ArrayList<>();
		formulas.add( formula );
		return sample( formulas );
	}

	public Valuation sample( ArrayList<dLFormula> formulas ) {
		Valuation point = null;
		try {
			point = findInstance( formulas ).valuation;
		} catch ( Exception e ) {
			e.printStackTrace();
		} 

		return point;
	}

	public ArrayList<Valuation> multiSample( dLFormula formula, int numSamples, double resolution ) {
		ArrayList<dLFormula> formulas = new ArrayList<>();
		formulas.add( formula );

		return multiSample( formulas, numSamples, resolution );

	}
	
	public ArrayList<Valuation> clusterSample(dLFormula formula, int numSamples, ArrayList<Double> radii,int parallelize_flag ) throws Exception {


		ArrayList<Valuation> points = multiSample(formula,numSamples,radii.get(0));
			for (int i=1;i<radii.size();i++)
			{
				points=clusterSampleBase(formula,points,numSamples,radii.get(i),radii.get(i-1),parallelize_flag);
			}
		
		
		return points;
	}
	
	/*
	 * else{
			ExecutorService executor=Executors.newFixedThreadPool(points.size());
			Callable<Integer> task = new Callable() {
					public int run()
					{
				    try {
				        TimeUnit.SECONDS.sleep(1);
				        return 123;
				    }
				    catch (InterruptedException e) {
				        throw new IllegalStateException("task interrupted", e);
				    }
				}

					@Override
					public Integer call() throws Exception {
						// TODO Auto-generated method stub
						return 123;
					}
			
			};
			Future<Integer> future = executor.submit(task);
			
			
		}
	 */
	protected ArrayList<Valuation> clusterSampleBase(final dLFormula formula, final ArrayList<Valuation> center_points,final int numSamples, final double SR, final double BR,int parallelize_flag) throws Exception{
			ArrayList<Future<ArrayList<Valuation>>> futures = new ArrayList<Future<ArrayList<Valuation>>>();
			ArrayList<Valuation> points= new ArrayList<Valuation>();
			ExecutorService executor=Executors.newFixedThreadPool(1);

			if(parallelize_flag==1){

				executor=Executors.newFixedThreadPool(center_points.size());
				}
				else
				{
				executor=Executors.newFixedThreadPool(1);

				}
			for (int i=0;i<center_points.size();i++)
			{	final int j=i;
				
				Callable<ArrayList<Valuation>> task = new Callable<ArrayList<Valuation>>() {
						public ArrayList<Valuation> call() throws Exception {
							// TODO Auto-generated method stub
	
							    try {
							    	
							        ArrayList<Valuation> newpoints=(multiSample(new AndFormula(formula,createBallExclusionFormula(center_points.get(j),new Real(BR)).negate()),numSamples,SR));
							        return newpoints;
							    }
							    catch (InterruptedException e) {
							        throw new IllegalStateException("task interrupted", e);
							    }						
						}
				
				};
				Future<ArrayList<Valuation>> future = executor.submit(task);
				futures.add(future);
			}
			
			for (Future<ArrayList<Valuation>> future: futures)
			{
				points.addAll(future.get());
			}
			return points;
		}
	

	public ArrayList<Valuation> multiSample( List<dLFormula> thisSet, int numberOfPoints, double suggestedRadius ) {
                ArrayList<dLFormula> queryFormulas = new ArrayList<dLFormula>();
                ArrayList<Valuation> samplePoints = new ArrayList<Valuation>();
                Valuation thisPoint;

                queryFormulas.addAll( thisSet );

                for ( int i = 0; i < numberOfPoints; i++ ) { 
                        thisPoint = sample( queryFormulas );
                        if ( thisPoint != null && !thisPoint.isEmpty() ) { 
                                samplePoints.add( thisPoint );
                                try {
                                	queryFormulas.add( createBallExclusionFormula( thisPoint, new Real(suggestedRadius) ) );
                                } catch ( Exception e ) {
                                	e.printStackTrace();
				}
                                //System.out.println("Iteration: " + i + ";  Ball Exclusion Formula: " +
                                //                      createBallExclusionFormula( thisPoint, new Real(suggestedRadius) ).toMathematicaString() );

                        } else {
                                break;
                        }
                }
{'fraction_non_alphanumeric': 0.09966265060240964, 'fraction_numerical': 0.003469879518072289, 'mean_word_length': 2.911044101017716, 'pattern_counts': {'":': 0, '<': 83, '<?xml version=': 0, '>': 77, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '934534', 'n_tokens_mistral': 3267, 'n_tokens_neox': 2740, 'n_words': 686}