search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
188 stars 45 forks source link

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

Open phantamanta44 opened 2 years ago

phantamanta44 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

kfriedberger commented 2 years ago

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