@@ -96,15 +96,15 @@ object OptionsCli {
9696 val logAtRewrite : B ,
9797 val stats : B ,
9898 val par : Option [Z ],
99- val branchParMode : LogikaBranchPar .Type ,
100- val branchPar : Option [ Z ] ,
99+ val branchPar : LogikaBranchPar .Type ,
100+ val rwPar : B ,
101101 val dontSplitFunQuant : B ,
102102 val splitAll : B ,
103103 val splitContract : B ,
104104 val splitIf : B ,
105105 val splitMatch : B ,
106- val rwTrace : B ,
107106 val rwMax : Z ,
107+ val rwTrace : B ,
108108 val elideEncoding : B ,
109109 val rawInscription : B ,
110110 val rlimit : Z ,
@@ -278,11 +278,9 @@ import OptionsCli._
278278 |-p, --par Enable parallelization (with CPU cores percentage to
279279 | use) (accepts an optional integer; min is 1; max is
280280 | 100; default is 100)
281- | --par-branch-mode Branch parallelization mode (expects one of { all,
281+ | --par-branch Branch parallelization mode (expects one of { all,
282282 | returns, disabled }; default: all)
283- | --par-branch Enable parallelization (with CPU cores percentage to
284- | use) (accepts an optional integer; min is 1; max is
285- | 100; default is 100)
283+ | --par-rw Enable rewriting parallelization
286284 |
287285 |Path Splitting Options:
288286 | --dont-split-pfq Do not force splitting in quantifiers and proof
@@ -293,9 +291,9 @@ import OptionsCli._
293291 | --split-match Split on match expressions and statements
294292 |
295293 |Rewriting Options:
296- | --rw-trace Disable rewriting trace
297294 | --rw-max Maximum number of rewriting (expects an integer; min
298295 | is 1; default is 100)
296+ | --rw-trace Disable rewriting trace
299297 |
300298 |SMT2 Options:
301299 | --elide-encoding Strip out SMT2 encoding in feedback
@@ -345,15 +343,15 @@ import OptionsCli._
345343 var logAtRewrite : B = true
346344 var stats : B = false
347345 var par : Option [Z ] = None ()
348- var branchParMode : LogikaBranchPar .Type = LogikaBranchPar .All
349- var branchPar : Option [ Z ] = None ()
346+ var branchPar : LogikaBranchPar .Type = LogikaBranchPar .All
347+ var rwPar : B = true
350348 var dontSplitFunQuant : B = false
351349 var splitAll : B = false
352350 var splitContract : B = false
353351 var splitIf : B = false
354352 var splitMatch : B = false
355- var rwTrace : B = true
356353 var rwMax : Z = 100
354+ var rwTrace : B = true
357355 var elideEncoding : B = false
358356 var rawInscription : B = false
359357 var rlimit : Z = 2000000
@@ -549,19 +547,16 @@ import OptionsCli._
549547 case Some (v) => par = v
550548 case _ => return None ()
551549 }
552- } else if (arg == " --par-branch-mode "
550+ } else if (arg == " --par-branch"
553551 val o : Option [LogikaBranchPar .Type ] = parseLogikaBranchPar(args, j + 1 )
554552 o match {
555- case Some (v) => branchParMode = v
553+ case Some (v) => branchPar = v
556554 case _ => return None ()
557555 }
558- } else if (arg == " --par-branch"
559- val o : Option [Option [Z ]] = parseNumFlag(args, j + 1 , Some (1 ), Some (100 )) match {
560- case o@ Some (None ()) => j = j - 1 ; Some (Some (100 ))
561- case o => o
562- }
556+ } else if (arg == " --par-rw"
557+ val o : Option [B ] = { j = j - 1 ; Some (! rwPar) }
563558 o match {
564- case Some (v) => branchPar = v
559+ case Some (v) => rwPar = v
565560 case _ => return None ()
566561 }
567562 } else if (arg == " --dont-split-pfq"
@@ -594,18 +589,18 @@ import OptionsCli._
594589 case Some (v) => splitMatch = v
595590 case _ => return None ()
596591 }
597- } else if (arg == " --rw-trace"
598- val o : Option [B ] = { j = j - 1 ; Some (! rwTrace) }
599- o match {
600- case Some (v) => rwTrace = v
601- case _ => return None ()
602- }
603592 } else if (arg == " --rw-max"
604593 val o : Option [Z ] = parseNum(args, j + 1 , Some (1 ), None ())
605594 o match {
606595 case Some (v) => rwMax = v
607596 case _ => return None ()
608597 }
598+ } else if (arg == " --rw-trace"
599+ val o : Option [B ] = { j = j - 1 ; Some (! rwTrace) }
600+ o match {
601+ case Some (v) => rwTrace = v
602+ case _ => return None ()
603+ }
609604 } else if (arg == " --elide-encoding"
610605 val o : Option [B ] = { j = j - 1 ; Some (! elideEncoding) }
611606 o match {
@@ -675,7 +670,7 @@ import OptionsCli._
675670 isOption = F
676671 }
677672 }
678- return Some (LogikaOption (help, parseArguments(args, j), background, manual, smt2Caching, transitionCaching, infoFlow, charBitWidth, fpRounding, useReal, intBitWidth, interprocedural, interproceduralContracts, strictPureMode, line, loopBound, callBound, patternExhaustive, pureFun, sat, skipMethods, skipTypes, logPc, logPcLines, logRawPc, logVc, logVcDir, logDetailedInfo, logAtRewrite, stats, par, branchParMode, branchPar , dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwTrace, rwMax , elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
673+ return Some (LogikaOption (help, parseArguments(args, j), background, manual, smt2Caching, transitionCaching, infoFlow, charBitWidth, fpRounding, useReal, intBitWidth, interprocedural, interproceduralContracts, strictPureMode, line, loopBound, callBound, patternExhaustive, pureFun, sat, skipMethods, skipTypes, logPc, logPcLines, logRawPc, logVc, logVcDir, logDetailedInfo, logAtRewrite, stats, par, branchPar, rwPar , dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace , elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
679674 }
680675
681676 def parseArguments (args : ISZ [String ], i : Z ): ISZ [String ] = {
0 commit comments