SMT backend confusion

[ott2]

In current conjure Repository version 3fcbbbbab (2021-12-17 13:08:56 +0300) calling an SMT solver backend other than Boolector fails, because the version of Savile Row which conjure installs always thinks it is calling Boolector even when Z3 or Yices are being used.

SR wants to use -m to specify the model as per Boolector, but neither Z3 nor Yices support this flag.

Is this a conjure reversion, should SR be updated to a newer version, has this never worked, or something else (like an SR change or bug)?

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

Error:
    Savile Row stdout: Created output file for domain filtering conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-minion
Created output SMT file conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-smt
In dichotomic search, lower: 0 upper: 45

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

    Savile Row exit-code: 1
Using cached models.
Savile Row: model000001.eprime ../graph-param-weighted/graph-weighted-50-sparsish-connected-2017070302.param
Running minion for domain filtering.
Running solver: z3

and similarly for yices, while boolector works fine.

[ozgurakgun]

If you pass -v to Conjure, it will print (among other things) the exact call to Savile Row. Might help identify where the problem is.

[ott2]

Using the following options for Savile Row:
    savilerow -in-param conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-param -in-eprime conjure-output/model000001.eprime -out-minion conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-minion -out-sat conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-dimacs -out-smt conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-smt -out-aux conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-aux -out-info conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime-info -out-minizinc conjure-output/model000001-graph-weighted-50-sparsish-connected-2017070302.eprime.mzn -run-solver -S0 -solutions-to-stdout-one-line -num-solutions 1 -smt -smt-nested -smt-bv -smtsolver-bin yices-smt2

So it seems SR is the problem. I assume this is the SR which conjure installs, as it seems to be the only one in my path.

[ozgurakgun]

You can run savilerow -help | head -n1 to see SR version.

I won't be able to look into this for a week at least (I am away). If @pwn1 has time he might.

[ott2]

Savile Row 1.9.1 (Repository Version: 2ac988043 (2021-09-10 10:51:58 +0100)) which seems quite a bit older than the latest, but I don't see any obvious SMT changes in SR for some time. So this might have been there for some time. I took a quick look at the SR source and in src/solver/SMTsolver.java the getCommand doesn't seem to use satSolverName to determine which command flags to use, but maybe those are set elsewhere. In any case, this seems an SR-only problem, not Conjure.

@pwn1 might be able to take a look when work resumes.

[pwn1]

Savile Row is doing what it's told, even though that doesn't make sense. It is told to produce the BV (nested) encoding, and run yices-smt2 and that combination does not work.

If you take out the -smt-bv flag I would expect it to work, otherwise you could take out all the SMT flags and just use -yices2 (I think you would also need to use -yices2-bin if it is not in Savile Row's bin folder)

[ozgurakgun]

Did anyone figure out what the fix should be here then?

The relevant code for constructing SR calls with an SMT solver is here: https://github.com/conjure-cp/conjure/blob/e47d019ee0fd73d814b4bbc88f639f8c2fa51279/src/Conjure/UI/MainHelper.hs#L894-L902

And this is what we claim to support: https://github.com/conjure-cp/conjure/blob/e47d019ee0fd73d814b4bbc88f639f8c2fa51279/docs/conjure-help.txt#L258-L265

So:

• boolector-bv
• yices-bv
• yices-lia
• yices-idl
• z3-bv
• z3-lia
• z3-nia
• z3-idl

We always pass -smt-nested

I thought yices supported the bv encoding, does it not?

[ozgurakgun]

bump @pwn1 + @ott2

[ozgurakgun]

Hi @pwn1 - just wondering whether yices is supposed to support the bv encoding. If it doesn't, I think the fix is removing that option from Conjure.

[pwn1]

@ozgurakgun Sorry, just looking at this now, since @ott2 posted it as an issue in the SR issue tracker. SR does not attempt to guess which solver type it is dealing with from the -smtsolver-bin flag, and it has default solvers for each logic (boolector for BV). I would like to remove -smtsolver-bin, it is clearly causing confusion. You can use the pattern "-solvertype -solvertype-bin blahblah" for solvertype \in { z3, yices2, boolector }.

Do you agree to remove the -smtsolver-bin flag?

[ozgurakgun]

I guess that flag doesn't hurt, right? What happens if the binary name was different for example?

Conjure now passes the relevant flag so this is fixed when used from Conjure. See commit that closes this issue above: https://github.com/conjure-cp/conjure/commit/35231b77c52bffcac1e82cb97aa31531be0bc70a