PolyPaver | Documentation | Command Line Invocation


polypaver [OPTIONS] [PROBLEM_ID]
  Tries to decide numerical conjectures (problems) using polynomial enclosures.
  [PROBLEM_ID] specifies one or more conjectures as follows:
  <name>.pp [<conclusion number>]: like a single VC in SPARK .siv
  <name>.siv [<vc name> [<conclusion number>]]: SPARK-generated VCs
  <name>.tptp: TPTP file with fof formulas (ignoring includes)
  <name>.form: using internal syntax (machine generated)

Problem parameters:
  -i --tightnessvalues=ITEM  value(s) of T to try (if the formula has an
                             unbound variable T) (eg "2^0..10" or "1..10" or
                             "1,10,100") (default = 1)
Box solving effort:
  -s --startdegree=INT       first polynomial degree to try on each box
                             (default = degree)
  -d --degree=INT            maximum polynomial degree (default = 0)
  -z --maxsize=INT           maximum polynomial term size (default = 100)
  -e --effort=INT            for approximating point-wise sqrt and exp
                             (default = 10)
  -I --minintegrexp=INT      n to compute approximate integration step using
                             2^(-n)
Box subdivision strategy:
  -o --order=ORDER           sub-problem processing order, bfs for
                             breadth-first or dfs for depth-first, (default =
                             dfs)
  -f --splitintfirst         split integer valued domains until they are
                             exact before splitting the continuous domains
  -m --mindepth=INT          minimum bisection depth (default = 0)
  -b --maxdepth=INT          maximum bisection depth (default = 1000)
  -u --maxqueuelength=INT    maximum queue size (default = 50 for depth-first
                             and 5000 for breadth-first order)
  -t --time=INT              timeout in seconds (default = 7*24*3600 ie 1
                             week)                                                                                                                                          
Verbosity:
  -q --quiet                 no reporting of progress on the console (default
                             off)
  -v --verbose               report extra progress details on the console
                             (default off)
Plotting:
  -w --plotwidth=INT         plot width for 2D problems, 0 mean no plotting
                             (default)
  -h --plotheight=INT        plot height for 2D problems, 0 mean no plotting
                             (default)
  -? --help                  Display help message
  -V --version               Print version information
     --numeric-version       Print just the version number