let create (problem_file_name: string) : flags =
let verbosity =
new flag_verbosity
FL_PrintLevel
"-pl"
"--print-level"
1
[]
in
let flags =
Bool (
new flag_bool
FL_Resolve
"-ar"
"--resolve"
["Apply the Resolve inference rule."]
true
)
::
Bool (
new flag_bool
FL_Subsume
"-as"
"--subsume"
["Apply the Subsume inference rule."]
true
)
::
Bool (
new flag_bool
FL_Compact
"-ac"
"--compact"
["Apply the Compact inference rule."]
true
)
::
Bool (
new flag_bool
FL_Productivity
"-pr"
"--productivity"
["Split only on productive remainders."]
true
)
::
Bool (
new flag_bool
FL_MixedLiterals
"-ml"
"--mixed-literals"
["Context literals may contain both universal and parametric variables."]
true
)
::
Bool (
new flag_bool
FL_FiniteDomain
"-fd"
"--finite-domain"
["Search for finite domain models (not refutational complete)."]
false
)
::
Bool (
new flag_bool
FL_FDFunctionality
"-fdf"
"--finite-domain-functionality"
["Add functionality axioms in --finite-domain mode.";
"Done by default if --print-model-tptp is true to ensure consistency.";
]
true
)
::
Lemma (
new flag_lemma
FL_Lemma
"-lm"
"--lemma"
["Computes and uses lemmas, i.e. clauses entailed by the input clause set.";
" - 'None' : compute no lemmas.";
" - 'Grounded' : start lemma computation from grounded closing clause.";
" - 'Lifted' : start lemma computation from closing clause.";
" - 'Propositional': use a propositional abstraction of the involved context literals.";
"'Lifted' computes more constraining lemmas in general,";
"but has a much higher computation overhead.";
]
LM_Grounded
)
::
Int (
new flag_int
FL_LemmaMin
"-lmmin"
"--lemma-min"
["See --lemma-max.";
"Must be > 0 and <= --lemma-max if --lemma-max is > 0, 0 otherwise."]
100
)
::
Int (
new flag_int
FL_LemmaMax
"-lmmax"
"--lemma-max"
["The maximum number of lemmas to store.";
"If exceeded, the worst lemmas are removed s.t. only --lemma-min lemmas remain.";
"If 0 there is no limit on the number of stored lemmas.";
]
500
)
::
Bool (
new flag_bool
FL_LemmaUIP
"-lmuip"
"--lemma-uip"
["Stops regression for computing a lemma at the first UIP.";
]
false
)
::
Int (
new flag_int
FL_LemmaParametricAssert
"-lmpa"
"--lemma-parametric-assert"
["By default Assert of literals containing parameters is not performed.";
"If a clause is learned at least n times as a lemma,";
"then parametric assert is activated for that clause.";
"If 0 then parametric assert is never performed."
]
0
)
::
Bool (
new flag_bool
FL_PlusV
"-pv"
"--plus-v"
["Use +v instead of -v for the initial interpretation."]
false
)
::
Equality (
new flag_equality
FL_Equality
"-eq"
"--equality"
["Specifies if the predicate '=' is interpreted as equality";
"(e.g. as in (p(a) = p(b)) ), and how equality is handled.";
" - 'None' : ignore equality";
" - 'Axioms' : add the standard equality axioms,";
" if the problem contains equality";
]
EQ_Axioms
)
::
Backtracking (
new flag_backtracking
FL_Backtracking
"-bt"
"--backtracking"
["Specifies the backtracking method.";
"Note: For Horn problems naive backtracking is always used";
"as no backtracking occurs.";
]
BT_Backjumping
)
::
IterativeDeepening (
new flag_iterative_deepening
FL_IterativeDeepening
"-id"
"--iterative-deepening"
["Specifies the criterion for the iterative deepening."]
IT_TermDepth
)
::
Int (
new flag_int
FL_DepthBound
"-db"
"--depth-bound"
["The initial iterative deepening bound."]
2
)
::
Bool (
new flag_bool
FL_LookaheadExceeding
"-lx"
"--lookahead-all"
["Apply the Close lookahead to all Assert candidate literals,";
"instead of only to the candidates within the current depth bound."]
false
)
::
Restart (
new flag_restart
FL_Restart
"-rs"
"--restart"
["Specifies how restarting is done when a branch is exhausted";
"within the current depth bound.";
"If a candidate exceeding the depth bound has been computed:";
" - 'Eager' restarts immediately with an increased depth bound.";
" - 'Lazy' marks the current choice point as incomplete.";
" When finding an exhausted branch it backtracks to the first choice point";
" where a candidate has been dropped and continues the derivation there.";
" - 'Delayed' ignores the candidate for the time being.";
" When finding an exhausted branch all exceeding candidates";
" are recomputed and checked for applicability.";
" For an incomplete branch backtracking is then done like in 'Lazy'";
"'Eager' is best for unsatisfiable problems, 'Delayed' for satisfiable ones,";
"and 'Lazy' is best in general.";
]
RS_Lazy
)
::
HornCandidates (
new flag_neg_assert_candidates
FL_NegAssertCandidates
"-nac"
"--neg-assert-candidates"
["Specifies how negative Assert candidates are treated,";
"they can be ignored without loss of completeness.";
" - 'Ignore' completely ignores negative candidates.";
" - 'Lookahead' uses negative candidates only for the Close lookahead.";
" - 'Use' uses negative candidates for all purposes.";
" 'Ignore' seems to be best for Horn, 'Use' for non-Horn problems."
]
NAC_Use
)
::
String (
new flag_string
FL_EProver
"-eprover"
"--eprover"
["Specify path to the eprover (www.eprover.org).";
"For a first-order tptp input eprover will be used as the clausifier.";
"If not specified, then 'eprover' will be searched for";
"in darwin's directory and the path.";
]
""
)
::
PreprocessSplit (
new flag_preprocess_split
FL_PreprocessSplit
"-pps"
"--preprocess-split"
["Preprocess input clauses by splitting.";
" - 'None' does no splitting.";
" - 'Ground' splits variable disjoint clause parts.";
" - 'NonGround' splits clause parts by a non-ground connection literal";
" as long as this reduces the number of variables per part.";
" (this implies 'Ground')";
"In general 'Ground' performs best."
]
PPS_Ground
)
::
Bool (
new flag_bool
FL_PreprocessUnit
"-ppu"
"--preprocess-unit"
["Preprocess input clauses by removing clauses (clause literals)";
"which are subsumed by (negated) unit clauses, up to fix point.";
]
true
)
::
Bool (
new flag_bool
FL_PreprocessPure
"-ppp"
"--preprocess-pure"
["Preprocess input clauses by removing clauses containing pure literals.";
]
true
)
::
Bool (
new flag_bool
FL_PreprocessResolution
"-ppr"
"--preprocess-resolution"
["Preprocess input clauses by adding resolvents of length <= 3.";
]
false
)
::
Bool (
new flag_bool
FL_PreprocessEquality
"-ppe"
"--preprocess-equality"
["Preprocess input clauses by simplifying trivial (dis)equalities.";
]
true
)
::
InputFormat (
new flag_input_format
FL_InputFormat
"-if"
"--input-format"
["Specifies the default format used to parse the input.";
"This setting is ignored if the format can be deduced from the file extension.";
]
FI_TPTP
)
::
Float (
new flag_float
FL_TimeOutCPU
"-to"
"--timeout-cpu"
["Terminates the prover after n seconds of used processor time.";
"A value less than or equal to 0 disables the timeout."]
0.0
)
::
Float (
new flag_float
FL_TimeOutWC
"-tow"
"--timeout-wc"
["Terminates the prover after n seconds of used real (wall clock) time.";
"A value less than or equal to 0 disables the timeout."]
0.0
)
::
Int (
new flag_int
FL_MemoryLimit
"-mem"
"--memory-limit"
["Terminates the prover if it occupies more than n MB of RAM.";
"A value less than or equal to 0 disables the limit."]
0
)
::
Int (verbosity :> flag_int)
::
Bool (
new flag_bool
FL_PrintConfiguration
"-pc"
"--print-configuration"
["Print the system configuration."]
false
)
::
Bool (
new flag_bool
FL_PrintPreprocessSplit
"-ppps"
"--print-preprocess-split"
["Print how input clauses are split in preprocessing."]
false
)
::
Bool (
new flag_bool
FL_PrintPreprocessUnit
"-pppu"
"--print-preprocess-unit"
["Print simplifications done by --preprocess-unit."]
false
)
::
Bool (
new flag_bool
FL_PrintPreprocessPure
"-pppp"
"--print-preprocess-resolution"
["Print simplifications done by --preprocess-resolution."]
true
)
::
Bool (
new flag_bool
FL_PrintPreprocessResolution
"-pppr"
"--print-preprocess-pure"
["Print simplifications done by --preprocess-pure."]
false
)
::
Bool (
new flag_bool
FL_PrintPreprocessEquality
"-pppe"
"--print-preprocess-equality"
["Print simplifications done by --preprocess-equality."]
false
)
::
Bool (
new flag_bool
FL_PrintEqualityAxioms
"-peq"
"--print-equality-axioms"
["Print the axioms added to an equality problem, if any."]
false
)
::
Bool (
new flag_bool
FL_PrintLemmas
"-plm"
"--print-lemmas"
["Prints each newly learned lemma, and lemmas kept over a restart.";
]
false
)
::
Bool (
new flag_bool
FL_PrintFiniteDomainSorts
"-pfds"
"--print-fd-sorts"
["Prints the sorts inferred from the unsorted first order problem.";
]
false
)
::
Bool (
new flag_bool
FL_PrintFiniteDomainTransformation
"-pfdt"
"--print-fd-transformation"
["Prints the transformation of the clause set generated in --finite-domain mode.";
]
false
)
::
Bool (
new flag_bool
FL_PrintFiniteDomainAxioms
"-pfda"
"--print-fd-axioms"
["Prints the axiomatization generated in --finite-domain mode.";
]
false
)
::
PrintFDProblem (
new flag_print_fd_problem
FL_PrintFiniteDomainProblem
"-pfdp"
"--print-fd-problem"
["Prints in--finite-domain mode the problem generated";
"for each entered domain size, using tptp cnf format.";
" - 'Silent' does nothing.";
" - 'Print' prints the problem.";
" - 'Exit' prints the problem and exits.";
"So, 'Print' can be used in a derivation to print the problem for each size,";
"and 'Exit' with --pl 0 to just generate and print the problem.";
]
PFD_Silent
)
::
Bool (
new flag_bool
FL_PrintStatistics
"-ps"
"--print-statistics"
["Print statistics after the derivation terminates."]
false
)
::
Bool (
new flag_bool
FL_PrintModelContext
"-pmc"
"--print-context"
["Print a found model in the context format."]
false
)
::
String (
new flag_file
FL_PrintModelContextFile
"-pmcf"
"--print-context-file"
["Print a found model in the context format to a file."]
""
)
::
Bool (
new flag_bool
FL_PrintModelDIG
"-pmd"
"--print-DIG"
["Print a found model in the DIG (Disjunctions of Implicit Generalizations) format."]
false
)
::
String (
new flag_file
FL_PrintModelDIGFile
"-pmdf"
"--print-DIG-file"
["Print a found model in the DIG format to a file."]
""
)
::
Bool (
new flag_bool
FL_PrintModelFinite
"-pmfd"
"--print-model-finite"
["Print the multiplication tables of a finite domain model."]
false
)
::
Bool (
new flag_bool
FL_PrintModelTPTP
"-pmtptp"
"--print-model-tptp"
["Print a model in TPTP format."]
false
)
::
String (
new flag_file
FL_PrintModelTPTPFile
"-pmtptpf"
"--print-model-tptp-file"
["Print a found model in the TPTP format to a file."]
""
)
::
Bool (
new flag_bool
FL_PrintDerivationOnline
"-pdo"
"--print-derivation-online"
["Print the derivation (Assert, Split, Close, ...) in real-time.";
]
false
)
::
Bool (
new flag_bool
FL_PrintDerivationContextUnifier
"-pdcu"
"--print-context-unifier"
["Modifies any derivation output by additionally printing the context unifier";
"for each Assert, Split, and Close application."]
false
)
::
Bool (
new flag_bool
FL_PrintAssertCandidates
"-pac"
"--print-assert-candidates"
["Print each applicable Assert candidate."]
false
)
::
Bool (
new flag_bool
FL_PrintSplitCandidates
"-psc"
"--print-split-candidates"
["Print each applicable Split candidate."]
false
)
::
Unit ((
new flag_help_short
FL_Help
"-h"
"--help"
["Print a short description of the program usage and options."]
) :> flag_unit
)
::
Unit ((
new flag_help_long
FL_Help
"-help"
"--more-help"
["Print a description of the program usage and options."]
) :> flag_unit
)
::
Unit ((
new flag_version
FL_Version
"-v"
"--version"
["Print the program version."]
) :> flag_unit
)
::
if Zip_wrapper.enabled then begin
String (
new flag_file
FL_ZippedSource
"-zip"
"--zipped-source"
["Get the input file from this zipped archive (also jar)."]
""
)
::
[]
end
else begin
[]
end
in
verbosity#set_flags flags;
{
flags = flags;
problem_file_name = problem_file_name;
}