RegSTAB v2.0.0
SEE 'doc/manual.pdf' FOR AN ``EXHAUSTIVE'' DOCUMENTATION.
RegSTAB is a SAT-Solver able to deal with formula schemata e.g. /\i=1..n P_i where n is a variable.
Command: 'regstab' (machine independent bytecode version) or 'regstab.opt' (optimized native version)
The input formula shall be given on stdin or in a file provided on command-line.
RegSTAB answers "satisfiable" or "unsatisfiable"
Informal syntax:
* /\, \/, ->, <->, (+) respectively denote the conjunction, disjunction, implication, equivalence and exclusive or
* ~ denotes negation
* literals should be written P_e where:
- P can be any sequence of upper-case letters
- e is either an integer, or a variable (any sequence of lower-case letters), or i+k where i is a variable and k an integer
* iterations should be written /\i=K..e ... or \/i=K..e ... where K is an integer and e an expression of the previous form
* constraints can be given by ending the formula with "| cstr" where cstr is of the form "n{>,>=,=}K", n is a variable, K an integer.
Examples:
$regstab.opt
P_1
SATISFIABLE
$regstab.opt
P_1 /\ P_2
SATISFIABLE
$regstab.opt
~P_1 /\ P_1
UNSATISFIABLE
$regstab.opt
\/i=1..n P_i
SATISFIABLE
$regstab
\/i=1..n P_i /\ /\i=1..n ~P_i
UNSATISFIABLE
$regstab
P_1 /\ /\i=1..n (~P_i \/ P_i+1) /\ ~P_n | n>=1
UNSATISFIABLE
$regstab
P_1 /\ /\i=1..n (~P_i \/ P_i+1) /\ ~P_n
SATISFIABLE
$regstab --help
regstab [file] - says if the schema in file is satisfiable, schema taken on stdin if no file provided
--exclude-vars If the schema is satisfiable, exclude the given variables of the printed model
-l Print the lemmas used in the deduction
--lemmas Print the lemmas database (all lemmas, not just those used in the deduction)
-m Print a model when the schema is satisfiable
--model Same as -m
--not-tune-gc Turn off garbage collector tuning
-p Output the proof in the given file when the schema is unsatisfiable
--machine-proof When the proof is generated, generate it in a "machine"-oriented way, see documentation
--no-utf8 Display text in ASCII rather than UTF8
--human-xml Output XML in such a way that it is (a bit) more readable by humans
--proof Same as -p
--used-lemmas Same as -l
--stats Provide statistics once the execution is over (number of rules applied, number of lemmas, ...)
-s Same as --stats
--use-inclusion Use inclusion instead of equality to detect cycles (generally slower but gives more concise proofs)
--verbose Verbose level (1 to 3)
-v Same as --verbose
-x Same as --exclude-vars
-help Display this list of options
--help Display this list of options