conjure-cp / conjure

Conjure: The Automated Constraint Modelling Tool
Other
96 stars 20 forks source link

Add an additional command line argument to SR so it does not have to guess which solver to use (fix #505) #556

Closed ozgurakgun closed 1 year ago

ozgurakgun commented 1 year ago

Does this fix it you think @ott2?

ott2 commented 1 year ago

Looks good to me:

conjure solve --solver=z3 graph-shortcheaptour-2017070301.essence ../graph-param-weighted/graph-weighted-50-sparsish-connected-2017070301.param

gives

    Savile Row stderr: ERROR: boolector exited with error code:109 and error message:
Error: invalid command line option: -m
For usage information: z3 -h

while

conjure-fix-smt-cli  solve --solver=z3 graph-shortcheaptour-2017070301.essence ../graph-param-weighted/graph-weighted-50-sparsish-connected-2017070301.param

gives

Using cached models.
Savile Row: model000001.eprime ../graph-param-weighted/graph-weighted-50-sparsish-connected-2017070301.param
Running minion for domain filtering.
Running solver: z3
pwn1 commented 1 year ago

Sorry, brain not working -- intended to post in the issue, not here.