dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

Specify `python2` instead of assuming default #357

Open maxvonhippel opened 3 years ago

maxvonhippel commented 3 years ago

Currently the script fails if your default python is version 3, in this fashion:

(base) max@max-XPS-13-9310:~/tools/dreal3/dReal-3.16.06.02-linux/bin$ ./dReach -k 10      bouncing_ball.drh --verbose --precision 0.001 --visualize
  File "<string>", line 1
    import os,sys; print os.path.realpath("./dReach")
                         ^
SyntaxError: invalid syntax
usage: ./dReach options <*.drh> <options to dReal>

dReach: Bounded Model Checking for for Nonlinear Hybrid Systems

OPTIONS:

   -k <N> / -u <N>  specify the upperbound of unrolling steps (default: 3)

   -l <N>           specify the lowerbound of unrolling steps (default: 0)

   -b               use BMC heuristic with disjunctive path encoding (default: do not use)

   -r               -b and filter unreachable modes from SMT encoding (default: do not use)

   -e               -r and filter continuous variables from SMT encoding (default: do not use)

   -d               disjunctive path encoding (default: do not use)

   -z               apply exit codes (default: do not use):
                                51 if SAT,
                                52 if UNSAT,
                                1 abnormal termination

   -n               parse new .drh file format (default: do not use)

   -s               parse new .drh file format and use synchronous encoding (default: do not use)

EXAMPLE:

   dReach -k 10      bouncing_ball.drh --verbose --precision 0.001 --visualize
   dReach -l 3 -u 10 bouncing_ball.drh --verbose --precision 0.001 --visualize

an easy fix is just to specify that you want to use version 2. On my system, and indeed on most systems, if you say python2 it'll use 2.7, which is probably what you intend.

Thanks for making contributions to dReal! Before opening a pull-request, please check the following things: