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.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.SuitePrinter.Printer


// An example of querying an algebraic property.

config = new Config(CUT : Sequenic.T3.Examples.Item, suiteSizeMultiplierPerGoal:20)
t3 = new T3groovyAPI(config)
// generate a suite:
S = t3.ADT()
// an example of an algebraic property to check:
eq =        (clause("setCode(x) ; setCode(y)") >> {s-> s.retval}) 
     . equiv(clause("setCode(y) ; getCode()") )
// query:   
R = algquery(S).with(eq)
R.print()
R.numOfWitnesses