MACE4(1)

📦 version 2009, in nixos 26.05, nixpkgs unstable

bestie, welcome to the MACE4(1) page — yes, the General Commands Manual one — for mace4. 🦋 It’s giving “niche Unix tool with main character energy,” and honestly? Obsessed.

✨ NAME ✨

mace4 — searches for finite countermodels of first-order statements. Periodt. 💅

🎀 SYNOPSIS 🎀

mace4 [options] < input-file > output-file

🌸 DESCRIPTION 🌸

This manual page is the brief little doc for the mace4 command. 💖

The program mace4 searches for finite structures satisfying first-order and equational statements — the same kind of statement that prover9(1) accepts. If the statement is the denial of some conjecture, any structures found by mace4 are counterexamples to the conjecture. Iconic behavior, no cap. 🌈

mace4 can be a valuable complement to prover9(1), looking for counterexamples before (or at the same time as) using prover9(1) to search for a proof. It can also be used to help debug input clauses and formulas for prover9(1). Like a little debugging bestie. 🫶

💅 OPTIONS 💅

A summary of options is included below. Options override the equivalent settings given in the input file. To set or clear a flag, you must give 1 or 0 as the value. Fr fr, that part matters. 👑

  • -help — tells mace4 to print a summary of these command-line options. The “help me help you” flag. 💖
  • -n n — gives the starting domain size for the search. The default value is 2. If you also give an -N option, mace4 will iterate domain sizes up through the -N value, using an increment given by the -I value. Otherwise, mace4 will search only for the -n value. Yes bestie, the page says -I there — I’m just relaying the lore. 💀
  • -N n — gives the ending domain size for the search. The default is 10.
  • -i n — gives the domain size increment for the search. The default is 1.
  • -q n — this flag overrides the parameter iterate. It says to try the sizes that are prime numbers, from -n up through -N. Prime-number slay. 🔥
  • -m n — stop searching when the *n*th structure has been found. The default is 1.
  • -t n — stop searching after n seconds. Timeout era. ⏰
  • -s n — allow at most n seconds for each domain size. The parameter can be used (together with -t) to give an overall time limit. Budgeting, but make it math. 💸
  • -b n — stop searching when (about) n megabytes of memory have been used. Memory vibe check. 🧠
  • -V n — a rule is needed for distinguishing variables from constants in clauses and formulas with free variables. If this flag is clear, variables start with (lower case) u through z. If this flag is set, variables in clauses start with (upper case) A through Z or _. Case-sensitive girlie behavior. 🔠
  • -P n — if this flag is set, all structures that are found are printed in standard form, which means they are suitable as input to other LADR programs such as isofilter(1) and interpformat(1). Standard form, very demure. 🎀
  • -p n — if this flag is set, and if -P is clear, all structures that are found are printed in a tabular form. Table moment. ✨
  • -R n — if this flag is set, a ring structure is is applied to the search. The operations {+,-,*} are assumed to be the ring of integers (mod domain_size). This method puts a tight constraint on the search, allowing much larger structures to be investigated. (The double “is” is in the source, bestie — I’m not fixing it. 💀)
  • -v n — if this flag is set, the output file receives information about the search, including the initial partial model (the part of the model that can be determined before backtracking starts) and timing and other statistics for each domain size. It does not give a trace of the backtracking, so it does not consume a lot of file space. Lowkey chill logging. 🍓
  • -T n — if the trace flag is set, detailed information about the search, including a trace of all assignments and backtracking, is printed to the standard output. This flag causes a lot of output, so it should be used only on small searches. Do not unleash this on a big search unless you want a wall of text, bestie. 😭

There also exist a number of advanced options, which are used for experimentation with search methods. They can be ignored by nearly all users. For descriptions of these options, see the original mace4 manual. Niche experimental lore, iykyk. 🧚

🌈 SEE ALSO 🌈

👑 AUTHOR 👑

The author credit literally says mace4 ws written by William McCune <mccune@cs.unm.edu> — yep, that’s the exact energy. 💖

This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by others).

okay that’s the whole page, bestie — footer vibes: MACE4(1), dated August 12, 2007. Bye, slay, and may your searches be finite and your countermodels be cute. 💋✨

📦 where this page comes from