search

sosy-lab / java-smt

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

String solver of cvc5 has many incompatible errors #299

Closed xiaoxiongwang closed 9 months ago

xiaoxiongwang commented 1 year ago 
 SolverContext context = SolverContextFactory.createSolverContext(
                config, logger, shutdown.getNotifier(), SolverContextFactory.Solvers.CVC5);
StringFormula s = smgr.makeVariable("s");
BooleanFormula constraint2 = smgr.contains(s, smgr.makeString("hello world"));

It reports error: Exception in thread "main" io.github.cvc5.CVC5ApiException: Operator table.product expects two bags. Found two terms of types 'String' and 'String' respectively.

 SolverContext context = SolverContextFactory.createSolverContext(
                config, logger, shutdown.getNotifier(), SolverContextFactory.Solvers.CVC5);
StringFormula s = smgr.makeVariable("s");
BooleanFormula constraint2 = smgr.prefix(s, smgr.makeString("hello world"));

It reports error: Exception in thread "main" io.github.cvc5.CVC5ApiException: Invalid kind 'STRING_REPLACE', expected Terms with kind STRING_REPLACE must have at least 3 children and at most 3 children (the one under construction has 2) at io.github.cvc5.Solver.mkTerm(Native Method) at io.github.cvc5.Solver.mkTerm(Solver.java:521) at org.sosy_lab.java_smt.solvers.cvc5.CVC5StringFormulaManager.prefix(CVC5StringFormulaManager.java:77) at org.sosy_lab.java_smt.solvers.cvc5.CVC5StringFormulaManager.prefix(CVC5StringFormulaManager.java:19) at org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager.prefix(AbstractStringFormulaManager.java:116)

kfriedberger commented 1 year ago

It would be good to know more details:

From the given information, I can not yet reproduce the issue.

Just a guess: Did you use a self-compiled or incompatible version of CVC5 where the operators are enumerated differently?

xiaoxiongwang commented 1 year ago

It would be good to know more details:

  • What is your version of JavaSMT and CVC5?
  • operating system?

From the given information, I can not yet reproduce the issue.

Just a guess: Did you use a self-compiled or incompatible version of CVC5 where the operators are enumerated differently? 1.My version of CVC5 is commit d87874506a956c1d9f97233fff38ee25945e32d2 of https://github.com/cvc5/cvc5 and My version of JavaSMT is 3.14.2 2.My system is Ubuntu 18.04

xiaoxiongwang commented 1 year ago

self-compiled

The CVC5 is indeed a self-compiled version.

baierd commented 1 year ago

We can't really debug custom builds. We can however update CVC5 to the release version from march. Hopefully that will solve your issue.

xiaoxiongwang commented 1 year ago

We can't really debug custom builds. We can however update CVC5 to the release version from march. Hopefully that will solve your issue.

Thanks very much.

kfriedberger commented 1 year ago

The update to CVC5 v1.0.5 is available in Ivy, integated with 0fbd194dd09e073492ed26d16b63fdea33c8b3ed. I will publish CVC5 to Maven during the day and then prepare the next release of JavaSMT.

kfriedberger commented 1 year ago

CVC5 changed its internal naming for the library from libcvc5.so to libcvc5.so.1. Having an older version of CVC5 lying around might cause issues with incompatible operation enumerations.

kfriedberger commented 9 months ago

I am not sure whether this issue will bring any more insights. Thus, we will close it.