import java.util.logging.Logger
import java.util.logging.Level
import java.util.stream.StreamSpliterators.InfiniteSupplyingSpliterator;

import Sequenic.T3.Config
import Sequenic.T3.Pool
import Sequenic.T3.Sequence.Datatype.SUITE
import Sequenic.T3.Generator.Generator
import static Sequenic.T3.Generator.GenCombinators.FirstOf
import static Sequenic.T3.Generator.Value.ValueMGCombinators.*
import Sequenic.T3.T3groovyAPI
import Sequenic.T3.T3instrGroovyAPI
import Sequenic.T3.SuiteUtils.Query.*
import static Sequenic.T3.SuiteUtils.Query.StepPredicate.*
import static Sequenic.T3.SuiteUtils.Query.SeqPredicate.*
import static Sequenic.T3.SuiteUtils.Query.LTLQuery.*
import static Sequenic.T3.SuiteUtils.Query.Alg2Query.*
import static Sequenic.T3.SuiteUtils.Query.Equation.*
import Sequenic.T3.SuiteUtils.Inference.InvariantFile
import Sequenic.T3.SuiteUtils.Inference.SubcaseInvariantFile

logger = Logger.getLogger(Examples.BinarySearchTree.class.getName())
logger.setLevel(Level.SEVERE)

config = new Config(CUT : Examples.BinarySearchTree,
                    regressionMode : true,
                    injectOracles : false,
                    fieldUpdateProbability : 0,
                    suiteSizeMultiplierPerGoal : 10
                    )
                    
gen1 = UnguardedValue(MixedOneOf(0,1,2)).If(isSubclassOf(Comparable)) ;
gen2 = UnguardedValue(MixedOneOf(-10,-2,-1,0,1,2)).If(isSubclassOf(Comparable)) ;
t3a  = new T3groovyAPI(config)
t3b  = new T3groovyAPI(gen1,config)
t3c  = new T3groovyAPI(gen2,config)
suitegen = { -> t3a.ADT() + t3b.ADT() + t3c.ADT() }
suite = suitegen()

// infer oracles from the suite:
inf = new SubcaseInvariantFile(threshold:5 , relativeThreshold:0.001).withLogger(logger)
double[] bounds = [0]
inf.addDiscreteBounds(".", bounds)
inf.read(suite)
k = inf.infer(suitegen, 9)
t3a.info(suite)
inf.cleanup().print()
if (k!=null) println ">> oracles consistent after " + k + " iterations" ; else println ">> oracles still inconsistent "
suite.save(".","bst",false)
inf.save("bst.orc")