COLIBRI2(1)

📦 version 0.6, in nixpkgs unstable

💖 NAME 💖

Colibri2 — that's the whole name bestie, that's the program. It's the star of this manual page, and honestly? Main character energy. 👑

✨ SYNOPSIS ✨

Colibri2 [OPTION]… [FILE]

okay so literally the shape of it is: the command, then some options if you feel like it, then maybe a file. That's the vibe check. 💅

Right at the top of the page, before we even hit the real sections, there's these three little options just vibing on their own — no heading, no nothing, they just showed up. Here they are, no cap:

  • --lra-threshold-max-repeat=INT (absent=50) — the max number of times the LRA interval domain can get modified between decisions. Fifty if you don't say otherwise 🎀
  • --linearize — lets simplex add linear approximations in some cases
  • --egraph-merging-rounds — allows more than one merging round between two congruence classes (the original says "more that one", and I'm just telling you it means more than one, okay 😭)

🌸 ARGUMENTS 🌸

  • FILE (absent=<stdin>) — this is your input problem file. And here's the tea: if you don't give it a file, Colibri2 slides into interactive mode and reads from stdin instead. So it's never lonely, it's just waiting for you to type at it 🫶

💜 OPTIONS 💜

These are the common options for the colibrics binary. There are. So many. Grab a snack. 🍓

  • ----no-int-to-bv — yes that is four dashes at the front, don't come for me, that's literally what's written. It switches the integer union and congruence domain over to the BitVector domain.
  • --array-blast-rule — use the array blast rule when it's suitable
  • --array-def-values — use inference rules for default values
  • --array-ext-cho — use "Choice" when applying unrestricted extensionality
  • --array-ext-comb — extended combinators
  • --array-no-res-aup — don't restrict the array's ⇑ (select over store) rule
  • --array-no-res-ext — don't restrict the array extensionality rule
  • --array-nseqs-no-ppg — use the NSeq solver for the theory of Arrays, with no systematic propagation
  • --array-use-inf-rules — use the old array decision procedure (retro icon behavior tbh)
  • -b, --backtrace — enables printing of backtraces.
  • --bv-use-bdd — (no description on the page, it's mysterious like that ✨)
  • --check-headers=BOOL (absent=false) — if true, then the presence of headers gets checked in the input file (and errors get raised if they're not there).
  • --check-status=ENUM (absent=no) — check the answer using smtlib (:status) or colibri (:colibri2-status) information. The check differs with unknown: in the first case any answer is accepted, in the second case only unknown.
  • --color=BOOL (absent=true) — activate coloring of output 🌈
  • --cut-fix-model=INT (absent=1000) — stop FixModel after the given number of conflicts (and you lose the possibility to answer unsat, so, consequences 💀)
  • --debug — print the parsed dolmen statement (after expansion of includes)
  • --debug-dotgui-only=VAL (absent COLIBRI2_DOTGUI_ONLY env) — display only the given node in the dotgui output --debug-flag dotgui
  • --debug-flag=VAL — debug flags! The --debug-flag=foo option, or more generally --debug-flag=foo:level, activates flag foo for the given level (empty means info). Level is case-insensitive and can be a full word or a single-letter abbreviation among (d)ebug, (i)nfo (n)otice, (w)arn(ing), (e)rror and (q)uiet. Levels display all the messages of that level or higher — for example the warning level prints both warning and error messages, but not info or debug messages. The value of all flags is set to notice unless specified. ikyk yk 🧚
  • --dec-at-operators — instead of deciding a boolean literal, decide at operators whose value can't be propagated to arguments (e.g. a true disjunction)
  • --def-max-delayed-decision-level=INT (absent=5)
  • --def-max-immediate-decision-level=INT (absent=0)
  • --def-max-unfolding-level=INT (absent=15)
  • --demon-no-avoid-retriggering
  • --dont-print-result — check the answer using smtlib (:status) or colibri (:colibri2-status) information. The check differs with unknown: in the first case any answer is accepted, in the second case only unknown. (yes, it's word-for-word the same description as --check-status, that's not me being lazy, that's just what the page says 🙈)
  • --eager-decision — do decisions with eager
  • --first-restart=INT (absent=0) — step of the first restart. Only one is done currently.
  • --fixed-choice-order
  • --float-threshold-max-repeat=INT (absent=5000) — number of maximum modification of a domain between decisions
  • -g, --gc — print statistics about the gc upon exiting
  • --get-model-no-function — skip the model of functions symbol and polymorphic constants during get-model
  • --get-model-safe — skip the model of values that are not sure to be correctly printed (implies get-model-no-function)
  • --header-lang-version=VAL — set the only allowed language version for headers. If not set, all conforming version numbers are allowed.
  • --header-licenses=[,…] — set the allowed set of licenses in the headers. An empty list means allow everything. 🎀
  • -i INPUT, --lang=INPUT, --input=INPUT — set the input language to INPUT (one of ae, dimacs, iCNF, smt2, smt2.6, psmt2, tptp, tptp-6.3.0 or zf). Pick your fighter 💅
  • --learning (absent COLIBRI2_LEARNING env) — activate learning.
  • --limit-last-effort=VALUE — deactivate last effort after the given time ( 90%steps, 90%time, 200steps, 200s )
  • --lra-dl — use the difference logic engine
  • --lra-dl-no-poly — don't use polynomes when building the difference logic graph
  • --lra-dl-no-rm — when the LRA representative changes [old_repr = repr + delta], add a constraint stating [old_repr - repr = delta] instead of removing [old_repr] and transferring its constraints to [repr].
  • --lra-fourier — use FourierMotskin engine instead of Simplex engine
  • --lra-incr-dl — use the incremental version of the difference logic engine. Sets --lra-dl too if it's not set.
  • --lra-keep-relations-in-patterns
  • --lra-new-intr-dom — use the new interval domain
  • --lra-pivot-intr-upd — use pivot to update intervals for all elements of pivot class whenever the interval domain of one element changes
  • --lra-relop-norm-to-le — normalize all relational operators (<, ≤, >, ≥) to ≤ (glow-up for inequality signs honestly ✨)
  • -m ENUM, --mode=ENUM — set the input mode. The full mode parses the entire file before iterating over its contents, whereas the incremental mode processes each declaration before parsing the next one. Default is incremental mode.
  • --max-steps=INT — maximum number of steps.
  • --max-warn=INT (absent=4611686018427387903) — maximum number of warnings to display (excess warnings get counted, and a count of silenced warnings gets reported at the end). That default number is giving "I will never run out of patience" 😭
  • --negate-goal — negate assertions marked with (! .. :colibri2 goal).
  • --no-dec — make no decisions, only propagation and model search (fixmodel)
  • --no-eager-instantiation — don't do eager instantiation
  • --no-fix-model — stop at the start of FixModel
  • --no-fm-simplex — don't use the simplex for simulating fourier-motskin
  • --no-nseq — do not support the NSeq theory (but possibly use its solver for Arrays)
  • --no-quant-regroup-forall-with-implies
  • --no-quant-remove-unused-variables
  • --no-simplex — don't use the simplex at all
  • --nseq-base — use the Base theory of N-Sequences
  • --nseq-ext — use the Ext theory of N-Sequences, takes over nseq-base
  • --nseq-no-dist-first — when checking equalities, do not start with distinct NSeqs. Do it for all.
  • --nseq-no-get-intro — don't introduce nseq.get terms to detect equalities or differences between n-sequences
  • --print-success — activate printing for success. 🎉
  • --quant-always-add-skolem — add quantifier skolemization (exists) even if the truth value is not known
  • --quant-old — use quant old heuristic
  • --quant-user-as-rr — user pattern are considered as rewrite rules (immediately applied)
  • --quantifier-add-def-from-axiom — handle axioms that look like definitions as definitions
  • --quantifier-and-cc-on-boolean-operators — match and apply congruence closure on : and, or, xor, imply and not
  • --quantifier-skip-forall — handle existential quantification but skip universal quantification
  • --remove-coercion-in-pattern — remove coercion in patterns
  • -s SIZE, --size=SIZE (absent=-1) — stop the program if it tries to use more than the SIZE memory space. Accepts the usual suffixes for sizes: k, M, G, T. Without a suffix, it defaults to a size in octet.
  • --show-steps — show the number of steps after solving.
  • --simplex-improve-distance — use the simplex for refining distance between variables
  • --smt-trace=VAL — create a partial trace in the given filename.
  • --smt-trace-mode=VAL — change how the partial traces are generated.
  • --somewhat-useful-bias=INT (absent=0) — deactivated if bias <= 0 (the name is sending me, "somewhat useful" 😭)
  • --sort-last-effort
  • -t TIME, --time=TIME (absent=-1s) — stop the program after a time lapse of TIME. Accepts the usual suffixes for durations: s, m, h, d. Without a suffix, it defaults to a time in seconds.
  • --trace=VAL — output tef json trace in the given file
  • --try-disprove-forall-using-domain — try to disprove forall by splitting the domain of the variables
  • --type=BOOL (absent=true) — decide whether to type-check input expressions. If false, only parsing is done.

🎀 GC OPTIONS 🎀

Options to fine-tune the gc. Only experts should use these. Like, genuinely. This is the "you know who you are" section. 🫶
  • --gc-a=INT (absent=0) — set Gc.allocation policy
  • --gc-i=INT (absent=100) — set Gc.major_heap_increment
  • --gc-O=INT (absent=500) — set Gc.max_overhead
  • --gc-o=INT (absent=200) — set Gc.space_overhead
  • --gc-s=INT (absent=1000000) — set Gc.minor_heap_size

🦋 COMMON OPTIONS 🦋

  • --help[=FMT] (default=auto) — show this help in format FMT. The value FMT must be one of auto, pager, groff or plain. With auto, the format is pager or plain whenever the TERM env var is dumb or undefined.
  • --version — show version information. ⭐

👑 EXIT STATUS 👑

Colibri2 exits with:

  1. 0 — on success.
  2. 123 — on indiscriminate errors reported on standard error.
  3. 124 — on command line parsing errors.
  4. 125 — on unexpected internal errors (bugs).

Numbers to live by. Memorize them. Periodt. 💅

🌈 ENVIRONMENT 🌈

These environment variables affect the execution of Colibri2:

  • COLIBRI2_DOTGUI_ONLY — see option --debug-dotgui-only.
  • COLIBRI2_LEARNING — activate learning.

💀 BUGS 💀

You can report bugs at https://git.frama-c.com/ — go off, tell them everything 🫶

💖 AUTHORS 💖

Francois Bobot <francois.bobot@cea.fr> — icon, legend, the moment. 👑

okay that's the whole page bestie, we ate and left no crumbs 🍓✨ — this was Colibri2 0.6, the COLIBRI2(1) manual, and yes the version number and the manual name are literally the last things on the page so I'm putting them in the sign-off like a good hostess. bye bye, have fun not crashing 💜🦋🎀

📦 where this page comes from