-
Andrei Paskevich authored
default actions in case explicit options are missing. The command line has the following structure: why [options] [[file|-] [-t <theory> [-g <goal>]...]...]... Summary: Qualified theories come from the library, not from file. When the driver is not specified, pretty-print theories. When neither --prove nor --output are given, print tasks. When no theory is specified for a file, use every theory. When no goal is specified for a theory, use every goal. Examples: % why.opt [shows usage information] % why.opt test.why [prints the contents of test.why] % why.opt -t int.Int [prints the library theory int.Int] % why.opt -D drivers/z3.drv test.why [sends every task from test.why to stdout] % why.opt -D drivers/z3.drv -o directory test.why [creates ./directory/ if it's does not exist and sends every task to a separate file in ./directory/] % why.opt -D drivers/z3.drv --prove test.why -t ThA [calls the prover for every goal from theory ThA in test.why] % why.opt -D drivers/z3.drv --prove test.why -t ThA -g G1 -g G2 [calls the prover for G1 and G2 from theory ThA in test.why] % why.opt -D drivers/z3.drv -t int.Abs -g G1 test.why -t ThA [prints G1 from int.Abs and every goal from ThA in test.why]
77f29212