MathSAT does not allow variables of different sorts with the same name

[phantamanta44]

MathSAT throws an exception if two variables with the same name and different sorts are ever declared. For example:

SolverContextFactory.createSolverContext(SolverContextFactory.Solvers.MATHSAT5).use { solverCtx ->
    val ifm = solverCtx.formulaManager.integerFormulaManager
    val bfm = solverCtx.formulaManager.booleanFormulaManager
    solverCtx.newProverEnvironment().use { prover ->
        prover.addConstraint(ifm.equal(ifm.makeVariable("x"), ifm.makeNumber(0)))
        println(prover.isUnsat)
    }
    solverCtx.newProverEnvironment().use { prover ->
        prover.addConstraint(bfm.equivalence(bfm.makeVariable("x"), bfm.makeTrue()))
        println(prover.isUnsat)
    }
}

This snippet causes the exception:

Exception in thread "main" java.lang.IllegalArgumentException: A symbol with name `x' already exists, with type: Int
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_declare_function(Native Method)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaCreator.makeVariable(Mathsat5FormulaCreator.java:154)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaCreator.makeVariable(Mathsat5FormulaCreator.java:137)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5BooleanFormulaManager.makeVariableImpl(Mathsat5BooleanFormulaManager.java:37)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5BooleanFormulaManager.makeVariableImpl(Mathsat5BooleanFormulaManager.java:25)
	at org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager.makeVariable(AbstractBooleanFormulaManager.java:63)
	...

Whereas it works as expected for, e.g. Princess or Z3. I could imagine a solution where Mathsat5Formula is an intermediate representation of the formula that only gets "baked" into a MathSAT native formula when actually making a call to the prover, but that comes with some overhead, of course.

[kfriedberger]

Some solver provide that feature, some do not. Currently, this is expected behavior and we even have tests for that. See https://github.com/sosy-lab/java-smt/blob/0dc452dbd532e414abd08d42ef9b75d504168f77/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java#L1203 for tests.

Internal renaming of variables is avoided to not confuse the user, when querying models or dumping SMTLIB queries. In the future, we perhaps will add checks to Z3 and Prinzess to not allow identical-named variables any more.

[phantamanta44]

So then the idea is that the JavaSMT user should either generate a new solver context for every SMT call, or otherwise implement some kind of unique renaming thing themselves?

[kfriedberger]

yes, separate contexts will help here, or using a naming scheme for different types.

[kfriedberger]

Yes. Unique naming on user side is a good idea.