THIS(1)
🌸 THIS(1) 🌸
okay bestie, welcome to This — straight outta the User Commands manual, section 1 of your local man pages. It's the cvc5 theorem prover and it's genuinely that girl. Sit down, hydrate, we're going through every single flag together 🫶✨
💖 NAME 💖
This — Theorem prover for SMT problems 💅
🦋 DESCRIPTION 🦋
okay so the vibe here is:
cvc5 [options] [input-file]no cap. If you don't hand it an input file, or you literally just pass it -, cvc5 reads from standard input instead. lowkey iconic of it.
🎀 Most commonly-used cvc5 options 🎀
these are the main-character flags, the ones you'll actually reach for:
--incremental,-i— enable incremental solving [*]--lang=LANG,--input-language=LANG,-L LANG— force the input language (default is"auto"; peep--lang helpfor the tea)--output=TAG,-o TAG— enable output tag.--parse-only— exit right after parsing the input, no further [*]--preprocess-only— exit right after preprocessing the input [*]--quiet,-q— decrease verbosity (and yes, you can repeat it, go off)--rlimit=N— set the resource limit--rlimit-per=N,--reproducible-resource-limit=N— set the resource limit per query--stats— give you statistics on exit [*]--stats-all— print the unchanged (defaulted) statistics too [*]--stats-internal— print the internal (non-public) statistics as well [*]--tlimit=MS— set the time limit in milliseconds of wall clock time--tlimit-per=MS— set the time limit per query in milliseconds--verbose,-v— increase verbosity (also repeatable, we love options)--verbosity=N— the verbosity level of cvc5--decision=MODE,--decision-mode=MODE— choose the decision mode, see--decision=help--copyright— show cvc5's copyright info--early-exit— do not run destructors at exit; default on except in debug builds [*]--help,-h— the full command line reference--help-option-categories— print a summary of options for each category--help-regular,-H— the regular command line reference--interactive— force interactive shell / non-interactive mode [*]--print-success— print the"success"output that SMT-LIBv2 requires [*]--seed=N,--random-seed=N,-s N— seed for the random number generator--show-config— show cvc5's static configuration--version,-V— identify this cvc5 binary--force-logic=LOGIC— set the logic, and override all further user attempts to change it--strict-parsing— be less tolerant of non-conforming inputs, this is an alias for--parsing-mode=strict[*]--dag-thresh=N— dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)--expr-depth=N— print exprs to depth N (0 == default, -1 == no limit)--output-lang=LANG,--output-language=LANG— force the output language (default is"auto"; see--output-lang help)--proof-check=MODE— select the internal proof checking mode--proof-granularity=MODE— modes for proof granularity--proof-print-conclusion— print the conclusion of proof steps when printing AST [*]--proof-print-reference— print a reference to the original file instead of redeclaring [*]--enum-inst— enumerative instantiation: instantiate with ground terms from the relevant domain, then arbitrary ground terms before answering unknown [*]--full-saturate-quant— resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation [*]--print-inst=MODE— print format for printing instantiations--check-abducts— checks whether produced solutions to get-abduct are correct [*]--check-interpolants— checks whether produced solutions to get-interpolant are correct [*]--check-model-subsolver— use a subsolver to compute values when applicable in calls to get-value and check-models [*]--check-models— after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions [*]--check-proofs— after UNSAT/VALID, check the generated proof (with proof) [*]--check-synth-sol— checks whether produced solutions to functions-to-synthesize satisfy the conjecture [*]--check-unsat-cores— after UNSAT/VALID, produce and check an unsat core (heads up: expensive) [*]--debug-check-models— after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions [*]--produce-models,-m— support the get-value and get-model commands [*]--produce-proofs— produce proofs, support check-proofs and get-proof [*]--produce-unsat-cores— turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs. [*]--condense-function-values— condense values for functions in models rather than explicitly representing them [*]--default-function-value-mode=MODE— mode for choosing default values for functions
💫 Additional cvc5 options 💫
there's more. there's always more. she's thorough 💅
🧮 From the Arithmetic Theory module 🧮
--approx-branch-depth=N— maximum branch depth the approximate solver is allowed to take (EXPERTS only)--arith-brab— whether to use simple rounding, similar to a unit-cube test, for integers [*]--arith-eq-solver— whether to use the equality solver in the theory of arithmetic (EXPERTS only) [*]--arith-exp— enables non-standard extensions of the arithmetic solver (EXPERTS only) [*]--arith-prop=MODE— turns on arithmetic propagation (default is'old', see--arith-prop=help) (EXPERTS only)--arith-prop-clauses=N— rows shorter than this are propagated as clauses (EXPERTS only)--arith-rewrite-equalities— turns on the preprocessing rewrite that turns equalities into a conjunction of inequalities [*]--arith-static-learning— do arithmetic static learning for ite terms based on bounds when static learning is enabled [*]--collect-pivot-stats— collect the pivot history (EXPERTS only) [*]--cut-all-bounded— turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds (EXPERTS only) [*]--dio-decomps— let skolem variables for integer divisibility constraints leak from the dio solver (EXPERTS only) [*]--dio-solver— turns on the Linear Diophantine Equation solver (Griggio, JSAT 2012) (EXPERTS only) [*]--dio-turns=N— turns in a row dio solver cutting gets (EXPERTS only)--error-selection-rule=RULE— change the pivot rule for the basic variable (default is'min', see--pivot-rule help) (EXPERTS only)--fc-penalties— turns on degenerate pivot penalties (EXPERTS only) [*]--heuristic-pivots=N— the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection (EXPERTS only)--lemmas-on-replay-failure— attempt to use external lemmas if approximate solve integer failed (EXPERTS only) [*]--maxCutsInContext=N— maximum cuts in a given context before signalling a restart (EXPERTS only)--miplib-trick— turns on the preprocessing step of attempting to infer bounds on miplib problems (EXPERTS only) [*]--miplib-trick-subs=N— do substitution for miplib'tmp'vars if defined in <= N eliminated vars (EXPERTS only)--new-prop— use the new row propagation system (EXPERTS only) [*]--nl-cov— whether to use the cylindrical algebraic coverings solver for non-linear arithmetic [*]--nl-cov-force— forces using the cylindrical algebraic coverings solver, even in cases where it is possibly not safe to do so (EXPERTS only) [*]--nl-cov-lift=MODE— choose the Coverings lifting mode (EXPERTS only)--nl-cov-linear-model=MODE— whether to use the linear model as initial guess for the cylindrical algebraic coverings solver--nl-cov-proj=MODE— choose the Coverings projection operator (EXPERTS only)--nl-cov-prune— whether to prune intervals more aggressively (EXPERTS only) [*]--nl-cov-var-elim— whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver. It can not be used when producing proofs right now. (EXPERTS only) [*]--nl-ext=MODE— incremental linearization approach to non-linear--nl-ext-ent-conf— check for entailed conflicts in non-linear solver (EXPERTS only) [*]--nl-ext-factor— use factoring inference in non-linear incremental linearization solver [*]--nl-ext-flatten-mon— use inference schema based on flattening monomials [*]--nl-ext-inc-prec— whether to increment the precision for irrational function constraints (EXPERTS only) [*]--nl-ext-purify— purify non-linear terms at preprocess (EXPERTS only) [*]--nl-ext-rbound— use resolution-style inference for inferring new bounds in non-linear incremental linearization solver (EXPERTS only) [*]--nl-ext-rewrite— do context-dependent simplification based on rewrites in non-linear solver [*]--nl-ext-split-zero— initial splits on zero for all variables (EXPERTS only) [*]--nl-ext-tf-taylor-deg=N— initial degree of polynomials for Taylor approximation (EXPERTS only)--nl-ext-tf-tplanes— use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver [*]--nl-ext-tplanes— use non-terminating tangent plane strategy for non-linear incremental linearization solver [*]--nl-ext-tplanes-interleave— interleave tangent plane strategy for non-linear incremental linearization solver [*]--nl-icp— whether to use ICP-style propagations for non-linear arithmetic (EXPERTS only) [*]--nl-rlv=MODE— choose mode for using relevance of assertions in non-linear arithmetic (EXPERTS only)--nl-rlv-assert-bounds— use bound inference utility to prune when an assertion is entailed by another (EXPERTS only) [*]--pb-rewrites— apply pseudo boolean rewrites (EXPERTS only) [*]--pivot-threshold=N— sets the number of pivots using--pivot-ruleper basic variable per simplex instance before using variable order (EXPERTS only)
and bestie… we're not even done yet 👀 more parts are coming, don't go anywhere 🦋
--pp-assert-max-sub-size=N— the threshold for substituting an equality in ppAssert. (EXPERTS only) 🧪--prop-row-length=N— sets the maximum row length that gets used in propagation. (EXPERTS only)--replay-early-close-depth=N— multiples of the depths to try to close the approx log eagerly. (EXPERTS only)--replay-lemma-reject-cut=N— maximum complexity of any coefficient while outputting replaying cut lemmas. (EXPERTS only)--replay-num-err-penalty=N— number of solve integer attempts to skips after a numeric failure. (EXPERTS only) 😭--replay-reject-cut=N— maximum complexity of any coefficient while replaying cuts. (EXPERTS only)--restrict-pivots— have a pivot cap for simplex at effort levels below fullEffort. (EXPERTS only)[*]--revert-arith-models-on-unsat— revert the arithmetic model to a known safe model on unsat, if one is cached. (EXPERTS only)[*]🛟--rr-turns=N— round robin turn. (EXPERTS only) 🔄--se-solve-int— attempt to use the approximate solve integer method on standard effort. (EXPERTS only)[*]--simplex-check-period=N— the number of pivots to do in simplex before rechecking for a conflict on all variables. (EXPERTS only)--soi-qe— use quick explain to minimize the sum of infeasibility conflicts. (EXPERTS only)[*]--standard-effort-variable-order-pivots=N— limits the number of pivots in a single invocation of check() at a non-full effort level, using Bland's pivot rule. (EXPERTS only)--unate-lemmas=MODE— determines which lemmas to add before solving (default is'all', see--unate-lemmas=help). (EXPERTS only)--use-approx— attempt to use an approximate solver. (EXPERTS only)[*]--use-fcsimplex— use focusing and converging simplex (FMCAD 2013 submission). (EXPERTS only)[*]--use-soi— use sum of infeasibility simplex (FMCAD 2013 submission). (EXPERTS only)[*]
🍓 From the Arrays Theory module
--arrays-eager-index— turn on eager index splitting for generated array lemmas.[*]--arrays-eager-lemmas— turn on eager lemma generation for arrays. (EXPERTS only)[*]--arrays-exp— enable experimental features in the theory of arrays. (EXPERTS only)[*]🧪--arrays-optimize-linear— turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper). (EXPERTS only)[*]--arrays-prop=N— propagation effort for arrays:0is none,1is some,2is full. (EXPERTS only)--arrays-reduce-sharing— use model information to reduce size of care graph for arrays. (EXPERTS only)[*]--arrays-weak-equiv— use algorithm from Christ/Hoenicke (SMT 2014). (EXPERTS only)[*]
👜 From the Bags Theory module
--bags— enables the bags solver in applicable logics. (EXPERTS only)[*]
🧱 From the Base module
--err=erroutput|--diagnostic-output-channel=erroutput— Set the error (or diagnostic) output channel. Writes to stderr for"stderr"or"--", stdout for"stdout"or the given filename otherwise. (EXPERTS only)--in=input— Set the error (or diagnostic) output channel. Reads from stdin for"stdin"or"--"and the given filename otherwise. (EXPERTS only)--out=output|--regular-output-channel=output— Set the error (or diagnostic) output channel. Writes to stdout for"stdout"or"--", stderr for"stderr"or the given filename otherwise. (EXPERTS only)
ok bestie yes those three really do all say "Set the error (or diagnostic) output channel" in the source text, I'm not messing with you, that's literally what it says 💀 copy-paste era. Anyway.
--plugin-notify-sat-clause-in-solve— only inform plugins of SAT clauses when we are in the main solving loop of the SAT solver. (EXPERTS only)[*]--plugin-share-skolems— true if we permit sharing theory lemmas and SAT clauses with skolems. (EXPERTS only)[*]--rweight=VAL=N— set a single resource weight. (EXPERTS only) ⚖️--safe-mode=MODE— modes for restricting expert options and theories. (EXPERTS only) 🛡️--stats-every-query— in incremental mode, print stats after every satisfiability or validity query.[*]--trace=TAG|-t TAG— trace something (e.g.-t pushpop), can repeat and may contain wildcards like (e.g.-t theory::*). (EXPERTS only) 🔍
🔢 From the Bitvector Theory module
--bitblast=MODE— choose bitblasting mode, see--bitblast=help.--bitwise-eq— lift equivalence with one-bit bit-vectors to be boolean operations. (EXPERTS only)[*]--bool-to-bv=MODE— convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see--bool-to-bv=help.--bv-assert-input— assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver. (EXPERTS only)[*]--bv-eager-eval— perform eager context-dependent evaluation for applications of bv kinds in the equality engine.[*]--bv-eq-engine— enable equality engine when possible in bitvector theory. (EXPERTS only)[*]--bv-gauss-elim— simplify formula via Gaussian Elimination if applicable. (EXPERTS only)[*]--bv-intro-pow2— introduce bitvector powers of two as a preprocessing pass. (EXPERTS only)[*]--bv-propagate— use bit-vector propagation in the bit-blaster. (EXPERTS only)[*]--bv-rw-extend-eq— enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017-Preiner-scholl-smt08). (EXPERTS only)[*]--bv-sat-solver=MODE— choose which sat solver to use, see--bv-sat-solver=help.--bv-solver=MODE— choose bit-vector solver, see--bv-solver=help.--bv-to-bool— lift bit-vectors of size 1 to booleans when possible.[*]
🌳 From the Datatypes Theory module
--cdt-bisimilar— do bisimilarity check for co-datatypes. (EXPERTS only)[*]--datatypes-exp— enables reasoning about codatatypes and extended datatype terms. (EXPERTS only)[*]--dt-binary-split— do binary splits for datatype constructor types. (EXPERTS only)[*]--dt-blast-splits— when applicable, blast splitting lemmas for all variables at once. (EXPERTS only)[*]--dt-cyclic— do cyclicity check for datatypes. (EXPERTS only)[*]--dt-infer-as-lemmas— always send lemmas out instead of making internal inferences. (EXPERTS only)[*]--dt-nested-rec— allow nested recursion in datatype definitions. (EXPERTS only)[*]--dt-polite-optimize— turn on optimization for polite combination. (EXPERTS only)[*]--dt-share-sel— internally use shared selectors across multiple constructors. (EXPERTS only)[*]--sygus-abort-size=N— tells enumerative sygus to only consider solutions up to term sizeN(-1== no limit, default).--sygus-fair=MODE— if and how to apply fairness for sygus.--sygus-fair-max— use max instead of sum for multi-function sygus conjectures. (EXPERTS only)[*]--sygus-rewriter=MODE— if and how to apply rewriting for sygus symmetry breaking.--sygus-simple-sym-break=MODE— if and how to apply simple symmetry breaking based on the grammar for smart enumeration.--sygus-sym-break-lazy— lazily add symmetry breaking lemmas for terms. (EXPERTS only)[*]--sygus-sym-break-pbe— sygus symmetry breaking lemmas based on pbe conjectures.[*]--sygus-sym-break-rlv— add relevancy conditions to symmetry breaking lemmas. (EXPERTS only)[*]
🧠 From the Decision Heuristics module
--jh-rlv-order— maintain activity-based ordering for decision justification heuristic. (EXPERTS only)[*]--jh-skolem=MODE— policy for when to satisfy skolem definitions in justification heuristic. (EXPERTS only)--jh-skolem-rlv=MODE— policy for when to consider skolem definitions relevant in justification heuristic. (EXPERTS only)
✍️ From the Expression module
--type-checking— type check expressions. (EXPERTS only)[*]--wf-checking— check that terms passed to API methods are well formed (defaultfalsefor text interface). (EXPERTS only)[*]
🌈 From the Finite Field Theory module
--ff— enables the finite field solver in applicable logics. (EXPERTS only)[*]--ff-bitsum— parse bitsums. (EXPERTS only)[*]--ff-elim-disjunctive-bit— rewrite disjunctive bit constraints(or (= x 1) (= x 0))as(= (* x x) x). (EXPERTS only)[*]--ff-field-polys— include field polynomials in Groebner basis computation; don't do this. (EXPERTS only)[*]💀--ff-solver=MODE— which field solver (default:'gb'; see--ff-solver=help). (EXPERTS only)--ff-trace-gb— use a traced groebner basis engine. (EXPERTS only)[*]
🎈 From the Floating-Point module
--fp— enables the floating point theory in applicable logics. (EXPERTS only)[*]--fp-exp— Allow floating-point sorts of all sizes, rather than onlyFloat32(8/24) orFloat64(11/53) (experimental). (EXPERTS only)[*]🧪--fp-lazy-wb— Enable lazier word-blasting (on preNotifyFact instead of registerTerm). (EXPERTS only)[*]
🚗 From the Driver module
--dump-difficulty— dump the difficulty measure after every response to check-sat.[*]--dump-instantiations— output instantiations of quantified formulas after every UNSAT/VALID response.[*]--dump-instantiations-debug— output instantiations of quantified formulas after every UNSAT/VALID response, with debug information. (EXPERTS only)[*]--dump-models— output models after every SAT/INVALID/UNKNOWN response.[*]--dump-proofs— output proofs after every UNSAT/VALID response.[*]--dump-unsat-cores— output unsat cores after every UNSAT/VALID response.[*]--dump-unsat-cores-lemmas— output lemmas in unsat cores after every UNSAT/VALID response.[*]--force-no-limit-cpu-while-dump— Force no CPU limit when dumping models and proofs. (EXPERTS only)[*]--portfolio-dry-run— Print the strategies that would be run with--use-portfolio, without executing them. (EXPERTS only)[*]--portfolio-jobs=n— Number of parallel jobs the portfolio engine can run. (EXPERTS only)--segv-spin— spin on segfault/other crash waiting for gdb. (EXPERTS only)[*]🙈--show-trace-tags— dumps every single tag you could ever trace with (EXPERTS only) 👑--use-portfolio— turns on internal portfolio mode, picked based on the logic (EXPERTS only) [*]
🦋 From the Parallel module 🦋
--append-learned-literals-to-cubes— ships the learned literals out together with the cubes (EXPERTS only) [*]--checks-before-partition=N— how many standard-or-full-effort checks happen before we start partitioning (EXPERTS only)--checks-between-partitions=N— how many checks go down in between partitions (EXPERTS only)--compute-partitions=N— makes n partitions. heads up bestie: if n <2, computing partitions gets switched off completely (EXPERTS only)--partition-check=MODE | --check=MODE— picks whether the partitioning happens at a full check or a standard check (EXPERTS only)--partition-conflict-size=N— the number of literals in a cube; and if no partition size is set, then the partition conflict size gets chosen as log2 of the number of requested partitions (EXPERTS only)--partition-start-time=N— when to start creating partitions, in seconds (EXPERTS only)--partition-strategy=MODE | --partition=MODE— chooses the partition strategy mode (EXPERTS only)--partition-time-interval=N— how long to wait between scatter partitions (EXPERTS only)--partition-tlimit=N— time limit for partitioning, in seconds (EXPERTS only)--partition-when=MODE— chooses when to partition (EXPERTS only)--random-partitioning— creates random partitions (EXPERTS only) [*]--write-partitions-to=output | --partitions-out=output— sets the output channel where partitions get written (EXPERTS only)
🎀 From the Parser module 🎀
--filesystem-access— limits file system access when it's set to false (EXPERTS only) [*]--fresh-binders— always builds fresh variables when parsing binders, no exceptions (EXPERTS only) [*]--fresh-declarations— uses the API interface for fresh constants while parsing declarations and definitions [*]--global-declarations— forces every declaration and definition to be global while parsing [*]--parse-skolem-definitions— lets you parse skolems in the input file (EXPERTS only) [*]--parsing-mode=MODE— picks the parsing mode — run--parsing-mode=helpto see your options (EXPERTS only)--semantic-checks— switches on semantic checks, type checks included (EXPERTS only) [*]--term-sort-overload— allows terms and sorts to be overloaded (EXPERTS only) [*]
💅 From the Printing module 💅
--bv-print-consts-as-indexed-symbols— prints bit-vector constants in decimal (like(_ bv1 4)) instead of binary (like#b0001), and yeah it applies to SMT-LIB 2.x [*]--flatten-ho-chains— prints (binary) application chains all flattened out, e.g.(a b c)instead of((a b) c)(EXPERTS only) [*]--model-u-print=MODE— decides how uninterpreted elements get printed inside models--print-arith-lit-token— prints rationals and negative arithmetic literals as lexed tokens, e.g.1/4,-1.5(EXPERTS only) [*]--print-skolem-definitions— prints skolems based on their definitions, e.g.@ARRAY_DIFF_Nprints instead as(@array.diff A B)(EXPERTS only) [*]
🔥 From the Proof module 🔥
--check-proof-steps— checks proof steps for satisfiability, for refutation soundness testing. heads up tho: this only checks steps for non-core proof rules (EXPERTS only) [*]--check-proofs-complete— treats an incomplete proof as a failure (and yes, it's enabled by default in safe builds) (EXPERTS only) [*]--drat-binary-format— prints the DRAT proof in binary format (EXPERTS only) [*]--lfsc-expand-trust— prints the children of trusted proof steps (EXPERTS only) [*]--lfsc-flatten— flattens the steps in the LFSC proof (EXPERTS only) [*]--opt-res-reconstruction-size— optimizes resolution reconstruction so the proof gets smaller [*]--print-dot-clusters— says whether the proof node clusters (e.g. SAT, CNF, INPUT) get printed or not when you're using the dot format. (EXPERTS only) [*]--proof-alethe-define-skolems— in Alethe proofs, uses define-funs in the proof preamble for Skolemization terms (EXPERTS only) [*]--proof-alethe-res-pivots— adds pivots to Alethe resolution steps (EXPERTS only) [*]--proof-allow-trust— whether trust is allowed in the proof printer (when it applies) (EXPERTS only) [*]--proof-chain-m-res— uses chain multiset resolution [*]--proof-dag-global— dagifies terms in proofs using global definitions (EXPERTS only) [*]--proof-dot-dag— tells you if the dot proof gets printed as a DAG or as a tree (EXPERTS only) [*]--proof-elim-subtypes— eliminates subtypes (mixed arithmetic) in proofs (EXPERTS only) [*]--proof-format-mode=MODE— selects the language of the proof output (EXPERTS only)--proof-log— proof logging mode (EXPERTS only) [*]--proof-pedantic=N— throws an assertion failure for any incorrect rule application or untrusted lemma with pedantic level<=Nthat comes with a proof (EXPERTS only)--proof-pp-merge— merges subproofs in the final proof post-processor (EXPERTS only) [*]--proof-pre-simp-lookahead=N— the lookahead depth for merging proofs at previsit (EXPERTS only)--proof-prune-input— prunes unused input assumptions out of the final scope (EXPERTS only) [*]--proof-rewrite-rcons-rec-limit=N— the matching recursion limit for reconstructing proofs of theory rewrites--proof-rewrite-rcons-step-limit=N— the limit of steps considered when reconstructing proofs of theory rewrites--prop-proof-mode=MODE— modes for the type of proof the SAT solver generates--sat-proof-min-dimacs— minimizes the DIMACs emitted whenprop-proof-modeis set tosat-external-prove(EXPERTS only) [*]
🌈 From the SAT Layer module 🌈
--minisat-dump-dimacs— instead of actually solving, minisat dumps the asserted clauses in Dimacs format (EXPERTS only) [*]--minisat-simplification=MODE— the simplifications Minisat should perform. (EXPERTS only)--preregister-mode=MODE— modes for when to preregister literals.--random-freq=P | --random-frequency=P— sets the frequency of random decisions in the sat solver (P=0.0 by default) (EXPERTS only)--restart-int-base=N— sets the base restart interval for the sat solver (N=25 by default) (EXPERTS only)--restart-int-inc=F— sets the restart interval increase factor for the sat solver (F=3.0 by default) (EXPERTS only)--sat-random-seed=N— sets the random seed for the sat solver--sat-solver=MODE— chooses which sat solver to use — peep--sat-solver=helpfor the list (EXPERTS only)
🧚 From the Quantifiers module 🧚
--cbqi— enables conflict-based quantifier instantiation [*]--cbqi-all-conflict— adds every available conflicting instance during conflict-based instantiation [*]--cbqi-mode=MODE— what effort to apply the conflict find mechanism with--cbqi-skip-rd— an optimization: skips instances based on possibly irrelevant portions of quantified formulas (EXPERTS only) [*]--cbqi-tconstraint— enables entailment checks for t-constraints in the cbqi algorithm (EXPERTS only) [*]--cbqi-vo-exp— cbqi experimental variable ordering (EXPERTS only) [*]--cegis-sample=MODE— mode for using samples in the counterexample-guided inductive synthesis loop--cegqi— turns on counterexample-based quantifier instantiation [*]--cegqi-all— applies counterexample-based instantiation to all quantified formulas (EXPERTS only) [*]--cegqi-bv— uses the word-level inversion approach for counterexample-guided quantifier instantiation on bit-vectors [*]--cegqi-bv-ineq=MODE— chooses the mode for handling bit-vector inequalities with counterexample-guided instantiation (EXPERTS only)--cegqi-bv-interleave-value— interleaves model value instantiation with the word-level inversion approach (EXPERTS only) [*]--cegqi-bv-linear— linearizes adder chains for variables (EXPERTS only) [*]--cegqi-bv-rm-extract— swaps extract terms out for variables, for counterexample-guided instantiation on bit-vectors (EXPERTS only) [*]--cegqi-bv-solve-nl— tries to solve non-linear bv literals using model value projections (EXPERTS only) [*]--cegqi-full— turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation (EXPERTS only) [*]--cegqi-inf-int— uses integer infinity for vts in counterexample-based quantifier instantiation (EXPERTS only) [*]--cegqi-inf-real— uses real infinity for vts in counterexample-based quantifier instantiation (EXPERTS only) [*]--cegqi-innermost— only processes innermost quantified formulas in counterexample-based quantifier instantiation [*]--cegqi-midpoint— chooses substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation [*]--cegqi-min-bounds— uses the minimally constrained lower/upper bound for counterexample-based quantifier instantiation (EXPERTS only) [*]--cegqi-multi-inst— when it applies, does multi instantiations per quantifier per round in counterexample-based quantifier instantiation (EXPERTS only) [*]--cegqi-nested-qe— processes nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation [*]--cegqi-nopt— non-optimal bounds for counterexample-based quantifier instantiation (EXPERTS only) [*]--cegqi-round-up-lia— rounds up integer lower bounds in substitutions for counterexample-based quantifier instantiation (EXPERTS only) [*]--cond-var-split-quant=MODE— splits quantified formulas that lead to variable eliminations (EXPERTS only)--conjecture-gen— generates candidate conjectures for inductive proofs (EXPERTS only) [*]--conjecture-gen-gt-enum=N— how many ground terms to generate for model filtering (EXPERTS only)--conjecture-gen-max-depth=N— the maximum depth of terms to consider for conjectures (EXPERTS only)--conjecture-gen-per-round=N— how many conjectures to generate per instantiation round (EXPERTS only)--cons-exp-triggers— constructor expansion but for single-constructor datatype triggers ✨ (EXPERTS only)[*]--dt-stc-ind— strengthening for existential quantification over datatypes, grounded in structural induction 💅 (EXPERTS only)[*]--dt-var-exp-quant— datatype variables that are bound to exactly one constructor get expanded inside quantifiers 🌸 (EXPERTS only)[*]--e-matching— whether we do the heuristic E-matching thing or not 🦋[*]--elim-taut-quant— yeet the tautological disjuncts out of quantified formulas 🧹[*]--enum-inst-interleave— interleave enumerative instantiation with the other techniques, so they take turns like civilized queens 👑[*]--enum-inst-limit=N— max number of rounds of enumerative instantiation to apply (-1means no limit, bestie, go feral) (EXPERTS only)--enum-inst-rd— do we use relevant domain first for the enumerative instantiation strategy? that's the question 💭 (EXPERTS only)[*]--enum-inst-stratify— stratify the effort levels in enumerative instantiation, which lowkey favors speed over fairness 🏃♀️ (EXPERTS only)[*]--enum-inst-sum— enumerate tuples of quantifiers by increasing the sum of indices instead of the maximum, main character behavior fr fr ✨[*]--ext-rewrite-quant— extended rewriting, but applied to the bodies of quantified formulas 🎀[*]--finite-model-find— use the finite model finding heuristic for quantifier instantiation 🌈[*]--fmf-bound— finite model finding, but specifically on bounded quantification 📏[*]--fmf-bound-blast— send ALL the instantiations for bounded ranges in one single round, no holding back 💥 (EXPERTS only)[*]--fmf-bound-lazy— enforce bounds for bounded quantification lazily, by using proxy variables 🫧 (EXPERTS only)[*]--fmf-fun— find models for recursively defined functions; it assumes the functions are admissible 🧚 (EXPERTS only)[*]--fmf-fun-rlv— same as above, finds models for recursively defined functions, assumes the functions are admissible, and also allows an empty type when the function is irrelevant 💜 (EXPERTS only)[*]--fmf-mbqi=MODE— pick the mode for model-based quantifier instantiation 🎛️ (EXPERTS only)--fmf-type-completion-thresh=N— the max cardinality of an interpreted type for which exhaustive enumeration in finite model finding even gets attempted 🔢--full-sygus-verify— go all-in with full effort techniques instead of just answeringunknownwhen checking sygus candidates 😤 (EXPERTS only)[*]--global-negate— do a global negation of the input formula 🔄 (EXPERTS only)[*]--ho-elim— eagerly eliminate higher-order constraints, no waiting around ⚡ (EXPERTS only)[*]--ho-elim-store-ax— use the store axiom duringho-elim📦 (EXPERTS only)[*]--ho-matching— run the higher-order matching algorithm for triggers that have variable operators 🎯 (EXPERTS only)[*]--ho-merge-term-db— merge term indices modulo equality 🤝 (EXPERTS only)[*]--ieval=MODE— the mode for using instantiation evaluation 🧮--increment-triggers— generate extra triggers as needed during the search 🔍 (EXPERTS only)[*]--inst-local— instantiations stay local to the SAT context, they don't go wandering 🏠[*]--inst-max-level=N— maximum inst level of terms used to instantiate quantified formulas with (-1== no limit, which is the default) (EXPERTS only)--inst-max-rounds=N— maximum number of instantiation rounds (-1== no limit, which is the default) 🔁--inst-no-entail— do NOT consider instances of quantified formulas that are currently entailed 🚫[*]--inst-when=MODE— when to apply instantiation ⏰--inst-when-phase=N— how many instantiation rounds quantifiers takes (>=1) before theory combination is allowed to happen (EXPERTS only)--int-wf-ind— apply strengthening for integers based on well-founded induction 🧱 (EXPERTS only)[*]--ite-dtt-split-quant— splitites that have dt testers as their conditions ✂️ (EXPERTS only)[*]--ite-lift-quant=MODE— theitelifting mode for quantified formulas 🏗️--literal-matching=MODE— choose your literal matching mode 🎚️ (EXPERTS only)--macros-quant— perform quantifiers macro expansion 🪄[*]--macros-quant-mode=MODE— the mode for quantifiers macro expansion 🎛️--mbqi— use model-based quantifier instantiation 🧠[*]--mbqi-check-timeout=N— timeout (in milliseconds) for verifying subcalls for model-based instantiation (0== no limit) ⏳--mbqi-enum— use fast enumeration to augment instantiations from MBQI 🚀[*]--mbqi-enum-ext-vars-grammar— include variables that are defined in terms of others in the grammars for fast enumerative mbqi 📚 (EXPERTS only)[*]--mbqi-enum-free-syms-grammar— include free symbols from the body of the quantified formula in the grammars for fast enumerative mbqi 🆓 (EXPERTS only)[*]--mbqi-enum-global-syms-grammar— include global symbols from all available assertions in the grammars for fast enumerative mbqi 🌍 (EXPERTS only)[*]--mbqi-interleave— interleave model-based quantifier instantiation with the other techniques, they can share 🫶 (EXPERTS only)[*]--mbqi-nested-check— check nested quantified formulas in MBQI 🪆 (EXPERTS only)[*]--mbqi-one-inst-per-round— only add ONE instantiation per quantifier per round for mbqi, one at a time bestie ☝️[*]--miniscope-quant=MODE— miniscope mode for quantified formulas 🔬--miniscope-quant-user— miniscope quantified formulas that have user patterns 👤[*]--multi-trigger-cache— the caching version of multi triggers 🗃️[*]--multi-trigger-linear— an implementation of multi triggers where the max number of instantiations is linear with respect to the number of ground terms 📈[*]--multi-trigger-priority— only try multi triggers if single triggers give you zero instantiations 🥈[*]--multi-trigger-when-single— select multi triggers whenever single triggers exist 👯[*]--oracles— enable the interface to external oracles 🔮 (EXPERTS only)[*]--partial-triggers— use triggers that do NOT contain all the free variables 🙈 (EXPERTS only)[*]--pool-inst— pool-based instantiation: instantiate with ground terms that occur in user-specified pools 🏊♀️ (EXPERTS only)[*]--pre-skolem-quant=MODE— modes for applying skolemization eagerly to the bodies of quantified formulas 🪓--pre-skolem-quant-nested— apply skolemization to nested quantified formulas 🪆 (EXPERTS only)[*]--prenex-quant=MODE— prenex mode for quantified formulas 🧭 (EXPERTS only)--prenex-quant-user— prenex quantified formulas that have user patterns 👤[*]--print-inst-full— print instantiations for formulas that do NOT have given identifiers 🖨️[*]--purify-triggers— purify triggers, e.g.f( x+1 )becomesf( y ),x mapsto y-1🧼 (EXPERTS only)[*]--quant-alpha-equiv— infer alpha equivalence between quantified formulas 🔤[*]--quant-dsplit=MODE— mode for dynamic quantifiers splitting 💥--quant-fun-wd— assume that the function defined by quantifiers is well defined 🙏 (EXPERTS only)[*]--quant-ind— use every available technique for inductive reasoning 🧠✨ (EXPERTS only)[*]--quant-rep-mode=MODE— selection mode for representatives in the quantifiers engine 🎖️ (EXPERTS only)--register-quant-body-terms— consider ground terms inside the bodies of quantified formulas for matching 👀 (EXPERTS only)[*]--relational-triggers— choose relational triggers likex = f(y),x >= f(y)🔗 (EXPERTS only)[*]--relevant-triggers— prefer the triggers that are more relevant, based on SInE style analysis 🎯[*]--sub-cbqi— enable the conflict-based instantiation subsolver strategy 🧩[*]--sub-cbqi-timeout=N— timeout (in milliseconds) for subsolver calls forsub-cbqi⏳ (EXPERTS only)--sygus— support SyGuS commands 🎤[*]--sygus-add-const-grammar— statically add the constants that appear in the conjecture to the grammars ➕[*]--sygus-arg-relevant— static inference techniques for figuring out whether the arguments of functions-to-synthesize are relevant 🔎 (EXPERTS only)[*]--sygus-auto-unfold— enable the approach that automatically unfolds transition systems for directly solving invariant synthesis problems 🌀 (EXPERTS only)[*]--sygus-bool-ite-return-const— only use Boolean constants for return values in unification-based function synthesis 🅱️ (EXPERTS only)[*]--sygus-core-connective— use unsat core analysis to construct the Boolean connective for sygus conjectures 🧵[*]--sygus-crepair-abort— abort if the constant repair techniques aren't applicable 😵 (EXPERTS only)[*]--sygus-enum=MODE— mode for sygus enumeration 🔢--sygus-enum-fast-num-consts=N— the branching factor for the number of interpreted constants to consider for each size when you're using--sygus-enum=fast🌿 (EXPERTS only)--sygus-enum-random-p=P— the parameter of the geometric distribution used to determine the size of terms generated by--sygus-enum=random🎲 (EXPERTS only)--sygus-eval-unfold=MODE— modes for sygus evaluation unfolding 📂--sygus-expr-miner-check-timeout=N— timeout (in milliseconds) for satisfiability checks in expression miners ⏱️ (EXPERTS only)--sygus-filter-sol=MODE— mode for filtering sygus solutions 🧽 (EXPERTS only)--sygus-filter-sol-rev— compute backwards filtering, to figure out whether previous solutions get filtered based on later ones ⏪ (EXPERTS only)[*]--sygus-grammar-cons=MODE— mode for SyGuS grammar construction 🏗️--sygus-grammar-ho-partial— add partial function applications to the grammar 🧩 (EXPERTS only)[*]--sygus-grammar-norm— statically normalize sygus grammars based on flattening (linearization) 📐 (EXPERTS only)[*]--sygus-grammar-use-disj— use disjunctions in internally generated grammars. this is set tofalsewhen solving abduction queries. 🔀 (EXPERTS only)[*]--sygus-inference=MODE— mode for preprocessing arbitrary inputs to sygus conjectures 🪄 (EXPERTS only)--sygus-inst— enable the SyGuS instantiation quantifiers module 🎤[*]--sygus-inst-mode=MODE— select the instantiation lemma mode 🎚️ (EXPERTS only)--sygus-inst-scope=MODE— select the scope of ground terms 🔭 (EXPERTS only)--sygus-inst-term-sel=MODE— granularity for ground terms 🧂 (EXPERTS only)
okay bestie we are still in the OPTIONS mines and there is NO escape, but honestly? these are kinda iconic. keep scrolling, we're almost to the end of the alphabet 🫶
--sygus-inv-templ=MODE— the template mode for sygus invariant synthesis. your choices are: weaken the pre-condition, strengthen the post-condition, ornone. pick your fighter ✨--sygus-inv-templ-when-sg— use invariant templates (with solution reconstruction) for syntax guided problems. EXPERTS only[*]--sygus-min-grammar— statically minimize sygus grammars[*]--sygus-out=MODE— output mode for sygus--sygus-pbe— enable the approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures[*]🍓--sygus-pbe-multi-fair— when you're using multiple enumerators, make sure we only register the value of the minimal term size. EXPERTS only[*]--sygus-pbe-multi-fair-diff=N— same multiple-enumerator situation, except we only register values of minimal term size plus this value. default is0. EXPERTS only--sygus-qe-preproc— use quantifier elimination as a preprocessing step for sygus. EXPERTS only[*]--sygus-query-gen=MODE— mode for generating interesting satisfiability queries using SyGuS, for internal fuzzing. EXPERTS only--sygus-query-gen-dump-files=MODE— mode for dumping external files that correspond to interesting satisfiability queries withsygus-query-gen. EXPERTS only--sygus-query-gen-filter-solved— do not print queries that are solved. EXPERTS only[*]--sygus-query-gen-thresh=N— the number of points that we allow to be equal for enumerating satisfiable queries withsygus-query-gen. EXPERTS only--sygus-rec-fun— enable efficient support for recursive functions in sygus. EXPERTS only[*]🔥--sygus-rec-fun-eval-limit=N— use a hard limit for how many times, in a given evaluator call, a recursive function can be evaluated (so infinite loops can be avoided, periodt). EXPERTS only--sygus-rec-fun-infer— automatically infer recursive definitions for sygus. EXPERTS only[*]--sygus-repair-const— use the approach that repairs constants in sygus candidate solutions[*]--sygus-repair-const-timeout=N— timeout, in milliseconds, for the satisfiability check that repairs constants in sygus candidate solutions. EXPERTS only--sygus-rr-synth-accel— add dynamic symmetry breaking clauses based on candidate rewrites. EXPERTS only[*]--sygus-rr-synth-check— use a satisfiability check to verify the correctness of candidate rewrites. EXPERTS only[*]--sygus-rr-synth-filter-cong— filter candidate rewrites based on congruence. EXPERTS only[*]--sygus-rr-synth-filter-match— filter candidate rewrites based on matching. EXPERTS only[*]--sygus-rr-synth-filter-nl— filter out the non-linear candidate rewrites. EXPERTS only[*]--sygus-rr-synth-filter-order— filter candidate rewrites based on variable ordering. EXPERTS only[*]--sygus-rr-synth-input-nvars=N— the maximum number of variables per type that appear in rewrites fromsygus-rr-synth-input. EXPERTS only--sygus-rr-synth-rec— synthesize rewrite rules over all sygus grammar types, recursively. EXPERTS only[*]--sygus-sample-fp-uniform— sample floating-point values uniformly instead of in a biased fashion. EXPERTS only[*]--sygus-sample-grammar— when applicable, use the grammar for choosing sample points. EXPERTS only[*]--sygus-samples=N— number of points to consider when doing sygus rewriter sample testing. EXPERTS only--sygus-si=MODE— mode for processing single invocation synthesis conjectures--sygus-si-abort— abort if the synthesis conjecture is not single invocation[*]--sygus-si-rcons=MODE— policy for reconstructing solutions for single invocation conjectures--sygus-si-rcons-limit=N— number of rounds of enumeration to use during solution reconstruction (a negative value means unlimited). EXPERTS only--sygus-si-rcons-p=P— the parameter of the geometric distribution used to determine the number of unification patterns generated by single invocation techniques. EXPERTS only--sygus-stream— enumerate a stream of solutions instead of terminating after the first one[*]💅--sygus-unif-cond-independent-no-repeat-sol— Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis. EXPERTS only[*]--sygus-unif-pi=MODE— mode for synthesis via piecewise-independent unification--sygus-unif-shuffle-cond— Shuffle the condition pool when building solutions (this may change solution sizes, jsyk). EXPERTS only[*]--sygus-verify-inst-max-rounds=N— maximum number of instantiation rounds for sygus verification calls.-1== no limit, and the default is10. EXPERTS only--sygus-verify-timeout=N— timeout, in milliseconds, for verifying the satisfiability of synthesized terms.0== no limit.--term-db-mode=MODE— which ground terms to consider for instantiation--trigger-active-sel=MODE— selection mode to activate triggers. EXPERTS only--trigger-sel=MODE— selection mode for triggers--user-pat=MODE— policy for handling user-provided patterns for quantifier instantiation--user-pool=MODE— policy for handling user-provided pools for quantifier instantiation. EXPERTS only--var-elim-quant— enable simple variable elimination for quantified formulas[*]--var-ent-eq-elim-quant— enable variable elimination for quantified formulas that infers entailed equalities corresponding to eliminations[*]--var-ineq-elim-quant— enable variable elimination based on infinite projection of unbound arithmetic variables[*]
🦋 From the Separation Logic Theory module 🦋
--sep— enables the separation logic solver in applicable logics. EXPERTS only[*]--sep-min-refine— only add refinement lemmas for minimal (innermost) assertions. EXPERTS only[*]--sep-pre-skolem-emp— eliminate theempconstraint at preprocess time. EXPERTS only[*]
🎀 From the Sets Theory module 🎀
--rels-exp— enable the relations extension of the theory of sets. EXPERTS only[*]--sets-card-exp— enable the cardinality extension of the theory of sets. EXPERTS only[*]--sets-exp— enable extended symbols such as complement and universe in the theory of sets. EXPERTS only[*]--sets-proxy-lemmas— introduce proxy variables eagerly to shorten lemmas. EXPERTS only[*]
🌈 From the SMT Layer module 🌈
--abstract-values— in models, output arrays (and in the future, maybe others too) using abstract values, as required by the SMT-LIB standard. EXPERTS only[*]--ackermann— eliminate functions by ackermannization. EXPERTS only[*]--bv-to-int-use-pow2— use the internalpow2operator when translating shift notes. EXPERTS only[*]--bvand-integer-granularity=N— the granularity to use in--solve-bv-as-intmode and for theiandoperator (experimental). EXPERTS only--deep-restart=MODE— mode for deep restarts. EXPERTS only--deep-restart-factor=F— sets the threshold for average assertions per literal before a deep restart happens. EXPERTS only--difficulty-mode=MODE— choose the output mode forget-difficulty, see--difficulty-mode=help. EXPERTS only--early-ite-removal— remove ITEs early in preprocessing. EXPERTS only[*]--ext-rew-prep=MODE— mode for using the extended rewriter as a preprocessing pass, see--ext-rew-prep=help. EXPERTS only--foreign-theory-rewrite— Cross-theory rewrites. EXPERTS only[*]--iand-mode=mode— Set the refinement scheme for integer AND. EXPERTS only--interpolants-mode=MODE— choose the interpolants production mode, see--interpolants-mode=help--ite-simp— turn on ite simplification (Kim (and Somenzi) et al., SAT 2009). EXPERTS only[*]--learned-rewrite— rewrite the input based on learned literals[*]--minimal-unsat-cores— if an unsat core is produced, it gets reduced to a minimal unsat core. EXPERTS only[*]--model-cores=MODE— mode for producing model cores--model-var-elim-uneval— allow variable elimination based on unevaluatable terms to variables. EXPERTS only[*]--on-repeat-ite-simp— do the ite simplification pass again if repeating simplification. EXPERTS only[*]--print-cores-full— print all formulas regardless of whether they are named, e.g. in unsat cores[*]--produce-abducts— support theget-abductcommand[*]--produce-assertions|--interactive-mode— keep an assertions list. Note this option is always enabled.[*]--produce-assignments— support theget-assignmentcommand[*]--produce-difficulty— enable tracking of difficulty.[*]--produce-interpolants— turn on interpolation generation.[*]--produce-learned-literals— produce learned literals, supportget-learned-literals[*]--produce-unsat-assumptions— turn on unsat assumptions generation[*]--proof-mode=MODE— choose the proof mode, see--proof-mode=help. EXPERTS only--repeat-simp— make multiple passes with the nonclausal simplifier. EXPERTS only[*]--simp-ite-compress— enables compressing ites after ite simplification. EXPERTS only[*]--simp-with-care— enablessimplifyWithCarein ite simplification. EXPERTS only[*]--simplification=MODE|--simplification-mode=MODE— choose the simplification mode, see--simplification=help--simplification-bcp— apply Boolean constant propagation as a substitution during simplification. EXPERTS only[*]--solve-bv-as-int=MODE— mode for translating BVAnd to integer--solve-int-as-bv=N— attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)--solve-real-as-int— attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)[*]--sort-inference— calculate sort inference of the input problem, and convert the input based on monotonic sorts. EXPERTS only[*]--static-learning— use static learning (on by default)[*]⭐
okay bestie we are deep in the theory-solver basement now — this is where the EXPERTS-only knobs live and they are not kidding about that label 💀
--timeout-core-timeout=N— timeout (in milliseconds) for satisfiability checks for timeout cores (EXPERTS only)--unconstrained-simp— turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logicQF_ABV. (EXPERTS only) [*]--unsat-cores-mode=MODE— choose unsat core mode, see--unsat-cores-mode=help(EXPERTS only)
🎀 From the Strings Theory module: 🎀
--re-elim=MODE— regular expression elimination mode--re-first-class— allow regular expressions as first class terms (EXPERTS only) [*]--re-inter-mode=MODE— determines which regular expressions intersections to compute (EXPERTS only)--seq-array=MODE— use array-inspired solver for sequence updates in eager or lazy mode (EXPERTS only)--strings-alpha-card=N— the assumed cardinality of the alphabet of characters for strings, which is a prefix of the interval of unicode code points in the SMT-LIB standard (EXPERTS only)--strings-check-entail-len— check entailment between length terms to reduce splitting [*]--strings-deq-ext— use extensionality for string disequalities [*]--strings-eager-eval— perform eager context-dependent evaluation for applications of string kinds in the equality engine [*]--strings-eager-len-re— use regular expressions for eager length conflicts [*]--strings-eager-reg— do registration lemmas for terms during preregistration. If false, do registration lemmas for terms when they appear in asserted literals (EXPERTS only) [*]--strings-eager-solver— use the eager solver [*]--strings-exp— experimental features in the theory of strings [*]--strings-ff— do flat form inferences (EXPERTS only) [*]--strings-fmf— the finite model finding used by the theory of strings [*]--strings-infer-as-lemmas— always send lemmas out instead of making internal inferences (EXPERTS only) [*]--strings-infer-sym— generalized inferences in strings based on proxy symbols (EXPERTS only) [*]--strings-lazy-pp— perform string preprocessing lazily [*]--strings-len-norm— strings length normalization lemma (EXPERTS only) [*]--strings-mbr— use models to avoid reductions for extended functions that introduce quantified formulas [*]--strings-model-max-len=N— The maximum size of string values in models (EXPERTS only)--strings-process-loop-mode=MODE— determines how to process looping string equations--strings-re-derive-conf— use regular expression derive for conflict finding (EXPERTS only) [*]--strings-re-posc-eager— eager reduction of positive membership into concatenation (EXPERTS only) [*]--strings-rec-arith-approx— use possibly recursive reasoning when finding approximations for arithmetic string terms (EXPERTS only) [*]--strings-regexp-inclusion— use regular expression inclusion for finding conflicts and avoiding regular expression unfolding [*]--strings-rexplain-lemmas— regression explanations for string lemmas (EXPERTS only) [*]
🌈 From the Theory Layer module: 🌈
--assign-function-values— assign values for uninterpreted functions in models (EXPERTS only) [*]--conflict-process=MODE— mode for processing theory conflicts (EXPERTS only)--ee-mode=MODE— mode for managing equalities across theory solvers--lemma-inprocess=MODE— Modes for inprocessing lemmas. (EXPERTS only)--lemma-inprocess-infer-eq-lit— Infer equivalent literals when using lemma inprocess (EXPERTS only) [*]--lemma-inprocess-subs=MODE— Modes for substitutions for inprocessing lemmas. (EXPERTS only)--relevance-filter— enable analysis of relevance of asserted literals with respect to the input formula (EXPERTS only) [*]--tc-mode=MODE— mode for theory combination (EXPERTS only)--theoryof-mode=MODE— mode forTheory::theoryof()(EXPERTS only)
🦋 From the Uninterpreted Functions Theory module: 🦋
--eager-arith-bv-conv— eagerly expand bit-vector to arithmetic conversions during preprocessing [*]--model-based-arith-bv-conv— model-based inferences for bit-vector to arithmetic conversions (EXPERTS only) [*]--symmetry-breaker— use UF symmetry breaker (Deharbe et al., CADE 2011) [*]--uf-card-exp— allows logics with UF+cardinality (EXPERTS only) [*]--uf-ho-exp— enables the higher-order logic solver in applicable logics (EXPERTS only) [*]--uf-ho-ext— apply extensionality on function symbols (EXPERTS only) [*]--uf-lambda-qe— apply quantifier elimination eagerly when two lambdas are equated (EXPERTS only) [*]--uf-lazy-ll— do lambda lifting lazily [*]--uf-ss=MODE— mode of operation for uf with cardinality solver.--uf-ss-abort-card=N— tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at mostN(-1 == no limit, default)--uf-ss-fair— use fair strategy for finite model finding multiple sorts [*]--uf-ss-fair-monotone— group monotone sorts when enforcing fairness for finite model finding (EXPERTS only) [*]
[*] Each of these options has a --no-OPTIONNAME variant, which reverses the sense of the option.
so yeah, every single [*] one above has a --no- twin that flips it. iykyk 💅
and this build was:
compiled with GCC version 15.2.0 on Jan 23 2026 14:45:16👑 COPYRIGHT 👑
Copyright © 2009-2025 by the authors and their institutional affiliations listed at https://cvc5.github.io/people.html
This build of cvc5 uses GPLed libraries, and is thus covered by the GNU General Public License (GPL) version 3. Versions of cvc5 are available that are covered by the (modified) BSD license. If you want to license cvc5 under this license, please configure cvc5 with the --no-gpl option before building from sources.
THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.
This version of cvc5 is linked against the following non-(L)GPL'ed third party libraries.
- CaDiCaL - Simplified Satisfiability Solver See
https://github.com/arminbiere/cadicalfor copyright information. - CryptoMiniSat - An Advanced SAT Solver See
https://github.com/msoos/cryptominisatfor copyright information. - SymFPU - The Symbolic Floating Point Unit See
https://github.com/martin-cs/symfpu/tree/CVC4for copyright information.
This version of cvc5 is linked against the following third party libraries covered by the GPLv3 license. See licenses/gpl-3.0.txt for more information.
- CLN - Class Library for Numbers See
http://www.ginac.de/CLNfor copyright information.
See the file COPYING (distributed with the source code, and with all binaries) for the full cvc5 copyright, licensing, and (lack of) warranty information.
🔍 SEE ALSO 🔍
The full documentation for This is maintained as a Texinfo manual. If the info and This programs are properly installed at your site, the command
info Thisshould give you access to the complete manual.
and that's the whole page bestie!! 💖 this is cvc5 version 1.3.2, dated January 2026, and it's THIS(1). go forth and solve some SMT, you absolute icon ✨🎀
📦 where this page comes from
- ubuntu resolute: cvc5 1.3.2-1build1 · GPL-3.0-or-later
- ubuntu stonking: cvc5 1.3.2-1build1 · GPL-3.0-or-later
- 💖 girlified by deepseek-ai/DeepSeek-V4.1-Flash on : a language model's rewrite of the original, under its terms