main = WST07Heuristic

# TRS Standard
trs = TRSToQTRS:qtrs
qtrs = workOnTRS

workOnTRS = Maybe(Timer(10000,trsmanyrrr)):QTRSDependencyPairs:qdp

trsmanyrrr = Repeat(0, *, Any( \
        QTRSRRR[Order = KBOPOLO], \
        QTRSRRR[Order = POLO[Degree = 1, Range = 5, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]], \
        QTRSRRR[Order = PMatroNat[Engine = MINISAT, Range = 1, Dimension = 3, Collapse = False]], \
        QTRSRRR[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = True, Lex = False, Prec = True, Permute = False, Xgengrc = True, Afstype = MONOTONEAFS]], \
        QTRSRRR[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = MONOTONEAFS]] \
        ))




qdp = Repeat(0, *, First(QDPDependencyGraph:Maybe(QDPNonSCC), QDPUsableRules[BeComplete = True, UseApplicativeCeRules = False], Any(redPair, loopingQDP), loopingQDP2))

loopingQDP = Timer(10000, QDPNonTerm[TotalLimit = 3, LeftLimit = 3, RightLimit = 3])
loopingQDP2 = QDPNonTerm[TotalLimit = 8, LeftLimit = 8, RightLimit = 8]

redPair = First( \
    Any( \
        Timer(2000, QDPSizeChange[Subterm = True]), \
        Timer(10000, QDPUsableRulesRP[AllowATransformation = False, Degree = 1, Range = 2, MaxSimpleDegree = 5, Engine = MINISAT]), \
        Timer(10000, QDPMRR[Order = POLO[Degree = 1, Range = 3, Autostrict = False, MaxSimpleDegree = 10000, Engine = MINISAT]]), \
        Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 3, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 1, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = NEGPOLO[Engine = MINISAT[Version = 2], Range = 2, NegConstantRange=-2, PosConstantRange = 2, NegRangeCriterion = DAMPEN, PartialDioEval = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = FULLAFS], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = GPOLORATSIMPLE[Degree = 1, DenominatorRange = 4, NumeratorRange = 16, Heuristic = FULLRAT, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=False, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]])), \
    Any( \
        Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 5, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 3, Dimension = 4, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = True, Lex = False, Prec = True, Permute = False, Xgengrc = True, Afstype = FULLAFS], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 5, Degree = 1], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 1, Degree = SIMPLE_MIXED], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = 0, Max = 3, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -2, Max = 2, Dimension = 2, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])), \
    Any( \
        Solve(QDPSemanticLabelling[CarrierSetSize = 2, Strategy="semlab", AllowQuasi=True, Engine=SAT4J, IncrementalEngine=INCREMENTAL] : Repeat(0, *, redPair)), \
        QDPReductionPair[Order = MATRO[Engine = MINISAT, SatConverter=PLAIN[UseShifts=True, UseBinaryShifts=False, SumType=DUAL_COMB], Range=16, Denominator=4, Rational=True, Type=COLLAPSINGDPTUPLE[Size=2]]], \
        QDPReductionPair[Order = PMatroArcticInt[Collapse=True, Engine=MINISAT, Dimension=1, Max=5, Unary=True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Collapse=True, Engine=MINISAT, Dimension=3, Max=2, Min = -1, Unary=True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Collapse=True, Engine=MINISAT, Dimension=2, Max=4, Min = -2, Unary=True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 7, Dimension = 2, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 4, Dimension = 3, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]))        


# GTRS
gtrs = GTRSToQTRS:qtrs


# SRS Standard
srs = TRSToQTRS:qsrs
qsrs = qtrs
qsrsold = Any(QTRSLoopFinder, \
           workOnSRS)

workOnSRS = Maybe(srsrrr):QTRSDependencyPairs:srsdp
workOnSRS2 = Maybe(srsrrr2):QTRSDependencyPairs:srsdp2

#srsrrr = Timer(15000, srsmanyrrr)
srsrrr = Timer(15000, Repeat(0, *, Any(QTRSRRR[Order = KBOPOLO])))

#srsrrr2 = Timer(25000, srsmanyrrr)
srsrrr2 = Timer(15000, Repeat(0, *, Any(QTRSRRR[Order = KBOPOLO])))
        
srsmanyrrr = Repeat(0, *, Any( \
        QTRSRRR[Order = KBOPOLO], \
        QTRSRRR[Order = POLO[Degree = 1, Range = 3, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]], \
        QTRSRRR[Order = PMatroNat[Engine = MINISAT, Range = 1, Dimension = 3, Collapse = False]], \
        QTRSRRR[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = MONOTONEAFS]] \
        ))

srsmanyrrr2 = Repeat(0, *, Any( \
        QTRSRRR[Order = KBOPOLO], \
        QTRSRRR[Order = POLO[Degree = 1, Range = 2, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]], \
        QTRSRRR[Order = PMatroNat[Engine = MINISAT, Range = 1, Dimension = 2, Collapse = False]]
        ))


srsdp = Solve(Repeat(0, *, First(QDPDependencyGraph:Maybe(QDPNonSCC),srsRedPair)))
srsdp2 = Solve(Repeat(0, *, First(QDPDependencyGraph:Maybe(QDPNonSCC),srsRedPair2)))

srsRedPair = First( \
    Any( \
        Timer(2000, QDPSizeChange[Subterm = True]), \
        Timer(10000, QDPMRR[Order = POLO[Degree = 1, Range = 3, Autostrict = False, MaxSimpleDegree = 10000, Engine = MINISAT]]), \
        Timer(10000, QDPReductionPair[Order = NEGPOLO[Engine = MINISAT[Version = 2], Range = 2, NegConstantRange=-2, PosConstantRange = 2, NegRangeCriterion = DAMPEN, PartialDioEval = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 1, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 5, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])), \
    Any( \
        Timer(10000, QDPReductionPair[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = FULLAFS], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPUsableRulesRP[AllowATransformation = False, Degree = 1, Range = 3, MaxSimpleDegree = 5, Engine = MINISAT]), \
        Timer(10000, QDPReductionPair[Order = GPOLORATSIMPLE[Degree = 1, DenominatorRange = 4, NumeratorRange = 16, Heuristic = FULLRAT, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=False, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]]), \
        Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 2, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 3, Dimension = 3, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 5, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])), \
    Any( \
        QDPSemanticLabelling[CarrierSetSize = 2, Strategy="semlab", AllowQuasi=False, Engine=SAT4J, IncrementalEngine=INCREMENTAL], \
        QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 2, Degree = SIMPLE_MIXED], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = MATRO[Engine = MINISAT, SatConverter=PLAIN[UseShifts=True, UseBinaryShifts=False, SumType=DUAL_COMB], Range=16, Denominator=4, Rational=True, Type=COLLAPSINGDPTUPLE[Size=2]]], \
        QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 6, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 3, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 2, Dimension = 7, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]))

srsRedPair2 = First( \
    Any( \
        Timer(4000, QDPSizeChange[Subterm = True]), \
        Timer(10000, QDPReductionPair[Order = NEGPOLO[Engine = MINISAT[Version = 2], Range = 2, NegConstantRange=-2, PosConstantRange = 2, NegRangeCriterion = DAMPEN, PartialDioEval = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 1, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 5, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])), \
    Any( \
        Timer(10000, QDPReductionPair[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = FULLAFS], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = GPOLORATSIMPLE[Degree = 1, DenominatorRange = 4, NumeratorRange = 16, Heuristic = FULLRAT, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=False, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]]), \
        Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 2, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]), \
        Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 5, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])), \
    Any( \
        QDPSemanticLabelling[CarrierSetSize = 2, Strategy="semlab", AllowQuasi=False, Engine=SAT4J, IncrementalEngine=INCREMENTAL], \
        QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 2, Degree = SIMPLE_MIXED], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = MATRO[Engine = MINISAT, SatConverter=PLAIN[UseShifts=True, UseBinaryShifts=False, SumType=DUAL_COMB], Range=8, Denominator=2, Rational=True, Type=COLLAPSINGDPTUPLE[Size=2]]], \
        QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 6, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False], \
        QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 3, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]))