lgloptl.h

OPT(abstime,0,0,1,"print absolute time when reporting");
OPT(activity,0,0,2,"activity based clause reduction");
OPT(agility,1,0,1,"enable agility based restart skipping");
OPT(agilitylim,70,0,100,"agility limit for restarts in percent");
OPT(bate,1,0,1,"basic ATE removal during probing");
OPT(batewait,2,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(bca,0,0,2,"enable blocked clause addition (1=weak,2=strong)");
OPT(bcaddlimldscale,2,-7,7,"bca added clause limit ld scale");
OPT(bcamaxeff,10*M,0,I,"BCA maximum number of steps");
OPT(bcaminuse,100,0,I,"min number of literals required to be usable");
OPT(bcawait,2,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(bkwdocclim,100,0,I,"backward occurrence limit");
OPT(bkwdresched,1,0,1,"reschedule variables during backward");
OPT(bkwdroundlim,7,1,I,"bkwd round limit");
OPT(bkwdscale,100,1,10000,"bkwd steps vs elm steps in percent");
OPT(blkboost,10,1,10000,"initial BCE boost");
OPT(blkboostvlim,10*M,0,I,"BCE boost variable limit");
OPT(blkclslim,1*M,3,I,"max blocked clause size");
OPT(blklarge,1,0,1,"BCE of large clauses");
OPT(blkmaxeff,800*M,-1,I,"max effort in BCE (-1=unlimited)");
OPT(blkmineff,50*M,0,I,"min effort in BCE");
OPT(blkocclim1,100*K,1,I,"one-sided max occ of BCE");
OPT(blkocclim,1*M,3,I,"max occ in BCE");
OPT(blkocclim2,10*K,2,I,"two-sided max occ of BCE");
OPT(blkreleff,100,0,K,"rel effort in BCE");
OPT(blkresched,1,0,1,"reschedule tried but failed literals");
OPT(blkrtc,0,0,1,"run BCE until completion");
OPT(blksmall,1,0,1,"BCE of small clauses");
OPT(blksuccessmaxwortc,6,1,I,"BCE success max without run-to-completion");
OPT(blksuccessrat,100,1,I,"BCE success ratio");
OPT(block,0,0,1,"blocked clause elimination (BCE)");
OPT(blockwait,1,0,1,"wait for BVE");
OPT(boost,1,0,1,"enable boosting of preprocessors");
OPT(bumpreasonlits,1,0,1,"bump reason literals too");
OPT(bumpsimp,0,0,1,"bump during simplification too");
OPT(card,1,0,1,"cardinality constraint reasoning");
OPT(cardcut,2,0,2,"1=gomoroy-cuts,2=strengthen");
OPT(cardexpam1,3,2,I,"min length of exported at-most-one constraint");
OPT(cardglue,0,-1,MAXGLUE,"use lrg red cls too (-1=irr,0=moved,...)");
OPT(cardignused,0,0,1,"ignore already used literals in extraction");
OPT(cardmaxeff,300*M,-1,I,"max effort for cardmineff reasoning");
OPT(cardmaxlen,1000,0,I,"maximal length of cardinality constraints");
OPT(cardmineff,2*M,0,I,"min effort for cardmineff reasoning");
OPT(cardminlen,3,0,I,"minimal length of (initial) card constraints");
OPT(cardocclim1,300,0,I,"one-sided cardinality constraints occ limit");
OPT(cardocclim2,15,0,I,"two-sided cardinality constraints occ limit");
OPT(cardreleff,5,0,10*K,"rel effort for cardinality reasoning");
OPT(cardreschedint,10,1,I,"reschedule variable for card reasoning");
OPT(carduse,2,0,3,"use clauses (1=oneside,2=bothsidetoo,3=anyside)");
OPT(cardwait,0,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(classify,2,0,3,"classifier for parameter setting");
OPT(cce2wait,1,0,I,"wait for ATE to finish before doing ABCE");
OPT(cce,3,0,3,"covered clause elimination (1=ate,2=abce,3=acce)");
OPT(cce3wait,2,0,I,"wait for ABCE to finish before doing ACCE");
OPT(cceateint,2,1,I,"frequency of only ATE");
OPT(cceboost,10,1,1000,"CCE boost");
OPT(cceboostdel,3,0,100,"initial CCE boost delay");
OPT(cceboostint,5,1,I,"CCE boost interval");
OPT(cceboostvlim,10*M,0,I,"CCE boost variable limit");
OPT(ccemaxeff,I,-1,I,"max effort in covered clause elimination");
OPT(ccemaxround,3,0,I,"cce maximum rounds");
OPT(ccemineff,30*M,0,I,"min effort in covered clause elimination");
OPT(ccereleff,50,0,K,"rel effort in covered clause elimination");
OPT(ccertc,0,0,2,"run CCE until completition (1=almost-no-limit)");
OPT(ccertcint,15,1,I,"run CCE until completion interval");
OPT(ccertcintvlim,2*M,1,I,"run CCE until completion int var limit");
OPT(ccesuccessrat,100,1,I,"CCE success ratio");
OPT(ccewait,2,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(check,0,0,3,"check level");
OPT(clim,-1,-1,I,"conflict limit");
OPT(compact,0,0,2,"compactify after 'lglsat/lglsimp' (1=UNS,2=SAT)");
OPT(deco,1,0,1,"learn decision-only clauses too");
OPT(deco1opt,1,0,1,"optimized deco 1");
OPT(decolim,100,0,I,"decision-only clauses glue limit");
OPT(decompose,1,0,1,"enable decompose");
OPT(defragfree,50,10,K,"defragmentation free watches limit");
OPT(defragint,10*M,100,I,"defragmentation pushed watches interval");
OPT(delmax,10,0,10,"maximum delay");
OPT(dlim,-1,-1,I,"decision limit");
OPT(druplig,0,0,1,"connect to Druplig library");
OPT(drupligcheck,0,0,1,"enable checking of proof by Druplig");
OPT(drupligtrace,0,0,1,"enable tracing of proof by Druplig");
OPT(drupligtraceorig,0,0,1,"trace original clauses too");
OPT(elim,1,0,1,"bounded variable eliminiation (BVE)");
OPT(elmaxeff,800*M,-1,I,"max effort in BVE (-1=unlimited)");
OPT(elmblk,1,0,1,"enable BCE during BVE");
OPT(elmblkwait,1,0,1,"wait for BVE to be completed once");
OPT(elmboost,20,1,1000,"elimination boost");
OPT(elmboostdel,3,0,100,"initial elimination boost delay");
OPT(elmboostint,5,1,I,"elimination boost interval");
OPT(elmboostvlim,4*M,1,I,"elimination boost var lim");
OPT(elmclslim,1*M,3,I,"max antecendent size in elimination");
OPT(elmfull,0,0,1,"no elimination limits");
OPT(elmineff,20*M,0,I,"min effort in BVE");
OPT(elmlitslim,200,0,I,"one side literals limit for elimination");
OPT(elmocclim1,1000,1,I,"one-sided max occ of BVE");
OPT(elmocclim,1*M,3,I,"max occurrences in BVE");
OPT(elmocclim2,100,2,I,"two-sided max occ of BVE");
OPT(elmoccsumforced,0,0,10,"forced occurrence sum");
OPT(elmreleff,200,0,10*K,"rel effort in BVE");
OPT(elmresched,0,0,7,"reschedule variables (1=else,2=boost,4=full)");
OPT(elmroundlim,3,1,I,"variable elimination rounds limit");
OPT(elmrtc,0,0,2,"run BVE until completion (1=almost-no-limit)");
OPT(elmrtcint,10,1,I,"run BVE until completion interval");
OPT(elmrtcintvlim,500*K,1,I,"run BVE until completion int var limit");
OPT(elmotfstr,1,0,1,"on-the-fly strengthening during BVE");
OPT(elmotfsub,1,0,1,"on-the-fly subsumption during BVE");
OPT(elmsuccessmaxwortc,4,1,I,"BVE success max without run-to-completion");
OPT(elmsuccessrat,100,1,I,"BVE success ratio");
OPT(exitonabort,0,0,1,"exit instead abort after internal error");
OPT(factmax,100000,1,I,"maximum factor");
OPT(factor,3,0,3,"{cls,occ}lim factors (0=const1,1=ld,2=lin,3=sqr)");
OPT(features,0,0,I,"print features after that many simplifications");
OPT(gauss,1,0,1,"enable gaussian elimination");
OPT(gausscardweak,1,0,1,"extract XOR from cardinality constraints");
OPT(gaussexptrn,1,0,1,"export trn cls from gaussian elimination");
OPT(gaussextrall,1,0,1,"extract all xors (with duplicates)");
OPT(gaussmaxeff,50*M,-1,I,"max effort in gaussian elimination");
OPT(gaussmaxor,20,2,64,"maximum xor size in gaussian elimination");
OPT(gaussmineff,2*M,0,I,"min effort in gaussian elimination");
OPT(gaussreleff,2,0,10*K,"rel effort in gaussian elimination");
OPT(gausswait,2,0,2,"wait for BCE (1) and/or BVE (2) for XOR extraction");
OPT(gluekeep,4,1,I,"keep clauses with this original glue");
OPT(gluekeepsize,15,1,I,"but limit them to this size");
OPT(gluemacdfast,5,0,32,"e for fast (D)EMA with alpha=2^-e");
OPT(gluemacdslow,16,0,32,"e for slow (D)EMA with alpha=2^-e");
OPT(gluemacdsmooth,3,0,32,"e for avg EMA with alpha=2^-e");
OPT(gluescale,4,1,5,"glue scaling: 1=ar1,2=ar2,3=sqrt,4=sqrtld,5=ld");
OPT(hbrdom,2,0,2,"0=root-impl-tree,1=lca-impl-tree,2=lca-big-dag");
OPT(import,1,0,1,"import external indices and map them");
OPT(incredcint,1,1,I,"incremental reduce conflict interval");
OPT(incredconfslim,0,0,100,"incremental reduce conflict limit");
OPT(incsavevisits,0,0,1,"incremental start new visits counter");
OPT(inprocessing,1,0,1,"enable inprocessing");
OPT(irrlim,1,0,1,"use irredundant clauses as limit for simps");
OPT(itsmacdfast,12,0,32,"e for fast (D)EMA with alpha=2^-e");
OPT(itsmacdslow,18,0,32,"e for slow (D)EMA with alpha=2^-e");
OPT(itsmacdsmooth,10,0,32,"e for avg EMA with alpha=2^-e");
OPT(jlevelmacdfast,12,0,32,"e for fast (D)EMA with alpha=2^-e");
OPT(jlevelmacdslow,14,0,32,"e for slow (D)EMA with alpha=2^-e");
OPT(jlevelmacdsmooth,10,0,32,"e for avg EMA with alpha=2^-e");
OPT(jwhred,1,0,2,"JWH score based on redundant clauses too (2=only)");
OPT(keepmaxglue,1,0,1,"keep maximum glue clauses");
OPT(keepmaxglueint,1,1,I,"keep maximum glue clause interval (1 always)");
OPT(lhbr,1,0,1, "enable lazy hyber binary reasoning");
OPT(lkhd,2,-1,4, "-1=LOCS,0=LIS,1=JWH,2=TREELOOK,3=LENSUM,4=RELEVANCE");
OPT(locs,0,-1,I,"use local search (-1=always otherwise how often)");
OPT(locsbanner,0,0,1,"print version number of LOCS component");
OPT(locsboost,2,0,100,"initial local search boost");
OPT(locscint,10*K,1,I,"conflict interval for LOCS");
OPT(locsclim,1*M,0,(I>>8),"clause limit for local search");
OPT(locset,2,0,2,"initialize local search phases (1=prev,2=cur)");
OPT(locsexport,1,0,1,"export phases from local search");
OPT(locsmaxeff,100000,0,I,"max effort in local search");
OPT(locsmineff,1000,0,I,"min effort in local search");
OPT(locsred,0,0,4,"apply local search on redundant clauses too");
OPT(locsreleff,5,0,100,"rel effort in local search");
OPT(locsrtc,0,0,1,"run local search until completion");
OPT(locsvared,100,0,1000,"max variable reduction for LOCS");
OPT(locswait,2,0,2,"wait for BCE(1) and/or BVE(2)");
OPT(log,-1,-1,5,"log level");
OPT(maxscaledglue,MAXGLUE,0,MAXGLUE,"maximum scaled glue bound");
OPT(memlim,-1,-1,I,"memory limit in MB (-1=no limit)");
OPT(minimize,2,0,2,"minimize learned clauses (1=local,2=recursive)");
OPT(minlocalgluelim,200,0,I,"glue limit for using local minimization");
OPT(minlocalsizelim,3000,0,I,"size limit for using local minimization");
OPT(minrecgluelim,100,0,I,"glue limit for using recursive minimization");
OPT(minrecsizelim,1000,0,I,"size limit for using recursive minimization");
OPT(move,2,0,2,"move redundant cls (1=only-binary,2=ternary-too)");
OPT(otfs,0,0,1,"enable on-the-fly subsumption");
OPT(penmax,4,0,16,"maximum penalty");
OPT(phase,0,-1,1,"default initial phase (-1=neg,0=JeroslowWang,1=pos)");
OPT(phaseluckfactor,200,100,10*K,"min phase luck factor (pos/neg)");
OPT(phaselucklim,100,0,1000,"phase luck limit in promille");
OPT(phaseluckmaxround,10,0,I,"maximum number of phase luck checks");
OPT(phasesave,1,-1,1,"save and use previous phase (-1=reverse)");
OPT(plain,0,0,1,"plain mode disables all preprocessing");
OPT(plim,-1,-1,I,"propagation limit (thousands)");
OPT(poison,1,0,1,"poison optimization for clause minimization");
OPT(prbasic,1,0,2,"enable basic probing procedure (1=roots-only)");
OPT(prbasicmaxeff,400*M,-1,I,"max effort in basic probing");
OPT(prbasicmineff,M,0,I,"min effort in basic probing");
OPT(prbasicreleff,50,0,10*K,"rel effort in basic probing");
OPT(prbasicroundlim,8,1,I,"basic probing round limit");
OPT(prbasicrtc,0,0,1,"run basic probing until completion");
OPT(prbrtc,0,0,1,"run all probing until completion");
OPT(prbsimple,2,0,3,"simple probing (1=shallow,2=deep,3=touchall)");
OPT(prbsimpleboost,10,1,1000,"initial simple probing boost");
OPT(prbsimpleliftdepth,2,1,4,"simple probing lifting depth");
OPT(prbsimplemaxeff,200*M,-1,I,"max effort in simple probing");
OPT(prbsimplemineff,2*M,0,I,"min effort in simple probing");
OPT(prbsimplereleff,40,0,10*K,"rel effort in simple probing");
OPT(prbsimplertc,0,0,1,"run simple probing until completion");
OPT(probe,1,0,1,"enable probing");
OPT(profile,1,0,4,"profile level");
OPT(profilelong,0,0,1,"print long profile information");
OPT(promote,1,0,1,"keep clauses with reduced glue longer");
OPT(promotegluelim,8,0,MG,"promoted clauses reduced glue limit");
OPT(prune,0,0,1,"pruning through satisfication");
OPT(pruneclim,1000,0,I,"maximum conflict limit");
OPT(pruneinit,2,1,I,"initial decision interval");
OPT(prunelevel,2,1,I,"maximum decision level");
OPT(prunesize,10,2,I,"maximum clause size");
OPT(prunemin,0,0,I,"minimum decision interval");
OPT(prunemax,1000000,1,I,"maximum decision interval");
OPT(prunepure,1,0,1,"find and treat pure literals explicitly");
OPT(prunered,1,0,1,"learned pruning clauses as redundant clauses");
OPT(prunevsids,0,0,1,"pruning decisions using default heuristic");
OPT(pure,1,0,1,"enable pure literal elimination during BCE");
OPT(quatres,1,0,1,"enable quaternay resolution");
OPT(quatreswait,2,0,2,"wait with quaternay resolution");
OPT(queuesort,1,0,1,"sort decision queue by JWH score");
OPT(randec,0,0,1,"enable random decisions order");
OPT(randecint,809,2,I/2,"random decision order interval");
OPT(randphase,0,0,1,"enable random decision phases");
OPT(randphaseint,503,2,I/2,"random decision phases interval");
OPT(redcls,1,0,1,"reduce literals in learned clauses");
OPT(redclsglue,6,0,I,"upper glue limit for clause reduction");
OPT(redclsize,30,0,I,"size limit reducing literals in learned clauses");
OPT(redclsmaxdec,5,1,I,"max decisions checked per lit");
OPT(redclsmaxdepth,10,1,I,"max depth for propagation per lit");
OPT(redclsmaxlrg,10,0,I,"max large checked per lit for redcls");
OPT(redclsmaxprops,100,0,I,"max props per lit for redcls");
OPT(redclstype,4,2,4,"type of clauses used for reduction");
OPT(reduce,1,0,1,"enable clause reduction");
OPT(reducefixed,0,0,1,"enabled fixed bound on learned clauses");
OPT(reduceinc,300,1,10*M,"reduce limit increment");
OPT(reduceinit,2*K,1,100*M,"initial reduce limit");
OPT(reducereset,0,0,2,"enable reduce increment reset");
OPT(restart,1,0,1,"enable restarting");
OPT(restartfixed,0,0,1,"fixed restart");
OPT(restartblock,0,0,2,"enable restart blocking (1=conflict,2=restart)");
OPT(restartblocklim,200,1,K,"restart blocking limit percent (glucose R)");
OPT(restartblockbound,10*K,0,I,"restart blocking conflict lower bound");
OPT(restartcheckforced,1,0,1,"enable skipping restarts if not forced");
OPT(restartdelay,1,0,1,"enable restart delaying based on jump level");
OPT(restartdelaylim,50,1,K,"restart delaying limit in percent");
OPT(restartint,10,1,I,"base restart interval");
OPT(restartforcelim,115,1,K,"restart forcing limit percent (glucose K)");
OPT(restartforcemode,1,0,2,"forced restart mode (0=avg,1=ema,2=macd)");
OPT(restartpen1,1,0,1,"increase restart interval if few units");
OPT(restartpen2,1,0,1,"increase restart interval if few binary clauses");
OPT(restartpen3,1,0,1,"increase restart interval if few ternary clauses");
OPT(restartpenstab,1,0,1,"increase restart interval if stabilizing");
OPT(retireint,4,0,1000,"retire inactive clauses inprocessing phases count");
OPT(retiremin,1,0,I,"minimum glue for retirement");
OPT(retirenb,1,0,1,"enabled inactive clause retirement");
OPT(reusetrail,1,0,1,"reuse trail");
OPT(rmincpen,4,0,32,"logarithm of watcher removal penalty");
OPT(scincinc,250,1,10*K,"score increment increment in per mille");
OPT(scincincdelta,10,0,10*K,"delta score inc inc in per mille");
OPT(scincincincint,100*K,1,I,"score inc inc inc interval");
OPT(scincincmin,50,1,10*K,"min score inc inc in per mille");
OPT(scincincmode,1,0,2,"score inc inc mode (0=keep,1=delta,2=avg)");
OPT(scoreshift,24,0,64,"score shift");
OPT(seed,0,0,I,"random number generator seed");
OPT(simpbintinc,100,1,I,"inprocessing binary interval increment");
OPT(simpbintinclim,10*K,1,I,"inprocessing bin int inc limit");
OPT(simpcintdelay,2000,0,I,"inprocessing conflict delay");
OPT(simpcintinc,20*K,10,M,"inprocessing conflict interval increment");
OPT(simpcintincdiv,1,0,3,"cintinc reduction: 0=no,1=div1,2=div2,3=heur");
OPT(simpcintmaxhard,10*M,-1,I,"hard max conflict interval limit");
OPT(simpcintmaxsoft,1*M,-1,I,"soft max conflict interval limit");
OPT(simpidiv,3,1,100,"simplification inter delay divisor");
OPT(simpincdelmaxfact,50,0,1000,"inproc incremental delay max fact");
OPT(simpincdelmaxmin,10*K,0,I,"inproc incremental delay max min confs");
OPT(simpinitdelay,0,0,I,"initial simplification delay");
OPT(simpintsizepen,0,0,1,"penalize interval (positively) by size");
OPT(simpiscale,100,1,10000,"relative simplification inter delay scale");
OPT(simpitdelay,10,0,1000,"delay inpr by simpitdelay/delta-conf-per-it");
OPT(simpjleveldecdelay,1,0,1,"delay simp if jlevel decreases");
OPT(simpitintdecdelay,1,0,1,"delay simp if iteration interval decreases");
OPT(simpitintinc,10,1,I,"inprocessing iteration interval increment");
OPT(simpitintinclim,1*K,1,I,"inprocessing its int inc limit");
OPT(simplify,2,0,2,"enable simplification");
OPT(simprtc,5,1,100,"min var reduction for simplification RTC");
OPT(simptintinc,1000,1,I,"inprocessing ternary interval increment");
OPT(simptintinclim,10*K,1,I,"inprocessing trn int inc limit");
OPT(simpvarchg,100,1,1000, "simp remaining vars percentage change lim");
OPT(simpvarlim,100,0,I, "simp remaining vars min limit");
OPT(sizemaxpen,5,0,20,"maximum logarithmic size penalty");
OPT(sizepen,1*M,1,I,"number of clauses size penalty starting point");
OPT(sleeponabort,0,0,I,"sleep this seconds before abort/exit");
OPT(smallirr,90,0,100,"max percentage irr lits for BCE and VE");
OPT(smallve,1,0,1,"enable small number variables elimination");
OPT(smallvevars,FUNVAR,4,FUNVAR, "variables small variable elimination");
OPT(smallvewait,0,0,1,"wait with small variable elimination");
OPT(sortlits,0,0,1,"sort lits of cls during garbage collection");
OPT(stabema,7,0,32,"e for stability EMA with alpha=2^-e");
OPT(subl,0,0,10*K,"try to subsume this many recent learned clauses");
OPT(sweep,1,0,1,"enabled SAT sweeping");
OPT(sweepboost,10,1,1000,"sweeping boost");
OPT(sweepboostdel,4,0,100,"initial sweeping boost delay");
OPT(sweepboostint,7,1,I,"sweeping boost interval");
OPT(sweepboostvlim,1*M,1,I,"sweeping boost var lim");
OPT(sweepfacdec,10,1,100,"decisions limit factor");
OPT(sweepforgive,2,0,I,"forgive that many unsucessful rounds");
OPT(sweepirr,3,0,3,"irredundant clauses (1=bin,2=trn,3=lrg)");
OPT(sweepmaxdec,10*K,0,I,"maximum decisions in one sweep implies check");
OPT(sweepmaxeff,200*M,-1,I,"max effort in sweeping");
OPT(sweepmaxround,3,-1,I,"maximum rounds in sweeping");
OPT(sweepmindec,100,0,I,"mininum decisions in one sweep implies check");
OPT(sweepmineff,M,0,I,"min effort in sweeping");
OPT(sweepred,3,0,3,"include redundant clauses (1=bin,2=trn,3=lrg)");
OPT(sweepreleff,3,0,10*K,"rel effort in sweeping");
OPT(sweeprtc,0,0,1,"run sweeping until completion");
OPT(sweeprtcint,14,1,I,"run sweeping until completion interval");
OPT(sweeprtcintvlim,100*K,1,I,"run sweeping until completion int var lim");
OPT(sweepsuccessmaxwortc,6,1,I,"sweeping success max wo run-to-completion");
OPT(sweepsuccessrat,1000,1,I,"sweeping success ratio");
OPT(sweepwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(synclsall,1,0,1,"always synchronize all unconsumed clauses");
OPT(synclsglue,8,0,I,"clause synchronization glue limit");
OPT(synclsint,100,0,1000,"clause synchronization confs interval");
OPT(synclslen,40,0,I,"clause synchronization length limit");
OPT(syncunint,111111,0,M,"unit synchronization steps interval");
OPT(termint,122222,0,M,"termination check interval");
OPT(ternres,1,0,1,"generate ternary resolvents");
OPT(ternresboost,5,1,100,"initial ternary resolution boost");
OPT(ternresrtc,0,0,1,"run ternary resolvents until completion");
OPT(ternreswait,2,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(tlevelema,12,0,32,"e for EMA with alpha=2^-e");
OPT(transred,1,0,1,"enable transitive reduction");
OPT(transredwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(trapiflush,0,0,1,"flush API trace after each call");
OPT(trdmaxeff,2*M,-1,I,"max effort in transitive reduction");
OPT(trdmineff,100*K,0,I,"min effort in transitive reduction");
OPT(trdreleff,10,0,10*K,"rel effort in transitive reduction");
OPT(treelook,1,0,2,"enable tree-based look-ahead (2=scheduleprobing)");
OPT(treelookboost,10,1,100000,"tree-based look-head boost factor");
OPT(treelookfull,0,0,1,"do not limit tree-based look-head");
OPT(treelookmaxeff,50*M,-1,I,"max effort in tree-look based probing");
OPT(treelookmineff,300*K,0,I,"min effort in tree-look based probing");
OPT(treelookreleff,2,0,10*K,"rel effort in tree-look based probing");
OPT(treelookrtc,0,0,1,"run tree-based look-ahead until completion");
OPT(trep,0,0,1,"enable time based interval reporting");
OPT(trepint,55555,1,I,"interval for time based reporting");
OPT(trnreleff,10,0,K,"rel effort in ternary resolutions");
OPT(trnrmaxeff,200*M,-1,I,"max effort in ternary resolutions");
OPT(trnrmineff,4*M,0,I,"min effort in ternary resolutions");
OPT(unhdatrn,2,0,2,"unhide redundant ternary clauses (1=move,2=force)");
OPT(unhdextstamp,1,0,1,"used extended stamping features");
OPT(unhdhbr,0,0,1,"enable unhiding hyper binary resolution");
OPT(unhdlnpr,3,0,I,"unhide no progress round limit");
OPT(unhdmaxeff,20*M,-1,I,"max effort in unhiding");
OPT(unhdmineff,100*K,0,I,"min effort in unhiding");
OPT(unhdreleff,2,0,10*K,"rel effort in unhiding");
OPT(unhdroundlim,20,0,100,"unhide round limit");
OPT(unhide,1,0,1,"enable unhiding");
OPT(unhidewait,0,0,2,"wait for BCE (1) and/or BVE (2)");
OPT(usedtwice,1,0,1,"used twice optimization for clause minimization");
OPT(verbose,0,-1,5,"verbosity level");
OPT(wait,1,0,1,"enable or disable all waiting");
OPT(waitmax,4,-1,I,"max simps to wait (-1=nomax)");
OPT(witness,1,0,1,"print witness");