Skip to content
This repository has been archived by the owner on Aug 19, 2024. It is now read-only.

Parse bitwuzla version number to provide appropriate command line args #721

Merged
merged 1 commit into from
Feb 26, 2024
Merged

Parse bitwuzla version number to provide appropriate command line args #721

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 29 additions & 1 deletion src/main/scala/chiseltest/formal/backends/smt/SMTLibSolver.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ package chiseltest.formal.backends.smt

import firrtl2.backends.experimental.smt._
import scala.collection.mutable
import scala.util.matching.Regex

object Yices2SMTLib extends Solver {
private val cmd = List("yices-smt2", "--incremental", "--smt2-model-format")
Expand Down Expand Up @@ -34,7 +35,34 @@ object BoolectorSMTLib extends Solver {
}

object BitwuzlaSMTLib extends Solver {
private val cmd = List("bitwuzla", "--smt2", "--incremental")
/* Bitwuzla accepts different command line arguments based on it's version
* See: https://github.com/bitwuzla/bitwuzla/blob/main/NEWS.md */
private def cmd = {
val version_regex: Regex = "([0-9]+).([0-9]+).([0-9]+)".r.unanchored
val version_cmd = List("bitwuzla", "--version")
val r = os.proc(version_cmd).call()
val res = r.out.lines().head.trim

res match {
case version_regex(major, minor, _) => {
List("bitwuzla") ++
/* --incremental argument removed as of 0.1.0 - See NEWS.md */
(if (major.toInt == 0 && minor.toInt == 0) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

could you add a comment to where you found the info for which flags to use?

List("--incremental")
} else {
List()
}) ++
/* --lang option is used to specify smt2 as of 0.3.0 - See NEWS.md and
* https://github.com/bitwuzla/bitwuzla/issues/75 */
(if (major.toInt == 0 && minor.toInt < 3) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

here a comment to the issue or PR or documentation of bitwuzla would be great

List("--smt2")
} else {
List("--lang", "smt2")
})
}
case _ => List("bitwuzla", "--smt2", "--incremental")
}
}
override def name = "bitwuzla-smtlib"
override def supportsConstArrays = false
override def supportsUninterpretedFunctions = false
Expand Down
Loading