regb / scala-smtlib Goto Github PK

Have you considered publishing this library on SonaType Central Repository?
I think that it would be useful to have it as an ordinary library from SBT, instead of requiring to have it as a subproject (downloading it from GitHub).

Thanks!

System info:

$ z3 -version
Z3 version 4.8.10 - 64 bit

Using the latest commit of scala-smtlib, models are not annotated with the model symbol anymore, for example a model return by the latest z3 is the following:

(
  (define-fun z () Int
    1)
  (define-fun y () Int
    1)
  (define-fun x () Int
    2)
)

While on older version, it was:

(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    2)
  (define-fun z () Int
    1)
)

No unit test is currently broken because they use hard-coded models.
The fix is quite simple in essence: removing lines 130 to 133 of ParserCommandResponses is enough to get responses to parse again. This has to be mirrored in the printer too.

However, properly fixing it probably requires dealing with both the old and the new format.

I appreciate the small examples in the Getting Started section of the README page. Are there full code examples that use scala-smtlib similar to those found in that Getting Started section? I tried browsing through the codebase, but there does not seem to be full examples included. Please correct me if I'm wrong.

Thanks,
Josh

I'm working on a couple of projects (some open source, some commercial) that use SMT solvers from Scala. I'd like to avoid re-inventing the wheel and would be interesting in using / contributing to this library. Could you add a LICENSE file to this repo to clarify its licensing terms? Thanks!

Calling CVC4Interpreter.buildDefault yields an EOFException. However, adding -i or --no-incremental in the parameter list resolves the issue
(tested with CVC4 v1.5)

package org.combinators.cls.smt.examples
import smtlib.interpreters.CVC4Interpreter

object foo extends App {
  def bI: CVC4Interpreter = {
    val executable = "cvc4"
    val args = Array("-q",
      "--produce-models",
      "--no-incremental",
      "--dt-rewrite-error-sel",
      "--print-success",
      "--lang", "smt")
    new CVC4Interpreter(executable, args)
  }
  bI //works
  CVC4Interpreter.buildDefault //fails
}

Exception in thread "main" smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen]
	at smtlib.parser.ParserCommon.check(ParserCommon.scala:90)
	at smtlib.parser.ParserCommon.check$(ParserCommon.scala:88)
	at smtlib.parser.Parser.check(Parser.scala:8)
	at smtlib.parser.ParserCommandsResponses.parseGenResponse(ParserCommandsResponses.scala:31)
	at smtlib.parser.ParserCommandsResponses.parseGenResponse$(ParserCommandsResponses.scala:27)
	at smtlib.parser.Parser.parseGenResponse(Parser.scala:8)
	at smtlib.interpreters.CVC4Interpreter.<init>(CVC4Interpreter.scala:14)
	at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42)
	at org.combinators.cls.smt.examples.foo$.delayedEndpoint$org$combinators$cls$smt$examples$foo$1(foo.scala:16)
	at org.combinators.cls.smt.examples.foo$delayedInit$body.apply(foo.scala:4)
	at scala.Function0.apply$mcV$sp(Function0.scala:34)
	at scala.Function0.apply$mcV$sp$(Function0.scala:34)
	at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:12)
	at scala.App.$anonfun$main$1$adapted(App.scala:76)
	at scala.collection.immutable.List.foreach(List.scala:389)
	at scala.App.main(App.scala:76)
	at scala.App.main$(App.scala:74)
	at org.combinators.cls.smt.examples.foo$.main(foo.scala:4)
	at org.combinators.cls.smt.examples.foo.main(foo.scala)

According to mvnrepository, the last published artifact of this library has been 0.2.2-12-g91e7214.

Most notably, support for Scala 2.13 is not yet published on Maven central, while it is supported by the version hosted in this repository.

Are there any plans to publish the latest version?

Hi , I can't find examples for uninterpreted sorts like tuples,would u like to provide some? Thanks!

I have an example test with combinatorial explosion (yeah, it sucks I know) which makes scala-smtlib crash due to a stack overflow in the PrettyPrinter methods.

I don't know exactly how this works now in the latest scala versions, but would it be possible to annotate methods for tail recursion or something?

Just like DefineFunsRec, DefineFunRec also yields 3x success which should be considered in the parseResponseOf function of CVC4Interpreter :

case DefineFunRec(_) =>
 // CVC4 translates definefunrec in three commands per function,
 // and thus emits 3x (success)
 val res = for (i <- 1 to 3) yield {
   parser.parseGenResponse
 }

 res.find(_ != Success).getOrElse(Success)

When I run integration tests, I get the following for most of the tests:

smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen]
[info]   at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90)

Here is the full output of running sbt it:test. All unit tests pass when running sbt test.

Specs that might be relevant:

• scala-smtlib commit 3e23701
• sbt version 0.13.7
• openjdk version "1.8.0_131"
• Z3 version 4.5.1
• CVC4 version 1.5
• Debian GNU/Linux 8
• Linux kernel 4.9.0-0.bpo.3-amd64

I am getting the following error:

scala> semantics.HeapConsistencyChecker.test()
scala.MatchError: ALL (of class smtlib.parser.Commands$ALL$)
  at smtlib.printer.TerminalTreesPrinter$class.printLogic(TerminalTreesPrinter.scala:62)
  at smtlib.printer.RecursivePrinter$.printLogic(RecursivePrinter.scala:10)
  at smtlib.printer.RecursivePrinter$.printCommand(RecursivePrinter.scala:162)
  at smtlib.printer.RecursivePrinter$$anonfun$printScript$1.apply(RecursivePrinter.scala:16)
  at smtlib.printer.RecursivePrinter$$anonfun$printScript$1.apply(RecursivePrinter.scala:15)
  at scala.collection.immutable.List.foreach(List.scala:381)
  at smtlib.printer.RecursivePrinter$.printScript(RecursivePrinter.scala:15)
  at smtlib.printer.Printer$class.toString(Printer.scala:27)
  at smtlib.printer.RecursivePrinter$.toString(RecursivePrinter.scala:10)
  at semantics.HeapConsistencyChecker$.test(HeapConsistencyChecker.scala:12)
  ... 43 elided

when trying to run:

object Test {
  import smtlib.parser.Commands._
  import smtlib.parser.Terms._
  import smtlib.theories.Ints._

  def test() {
    val x = QualifiedIdentifier(SimpleIdentifier(SSymbol("x")))
    val y = QualifiedIdentifier(SimpleIdentifier(SSymbol("y")))
    val pf = smtlib.printer.RecursivePrinter.toString(Script(
      List(SetLogic(ALL),
           DeclareFun(SSymbol("x"), Seq(), IntSort()),
           DeclareFun(SSymbol("y"), Seq(), IntSort()),
           Assert(LessThan(NumeralLit(0), Add(x, y))),
           CheckSat()
           ))) //(assert (< 0 (+ x y)))
    print(pf)
  }
}