• SMT-LIB

  • Referenced in 182 articles [sw04103]
  • SMT-LIB was created with the expectation that the availability of common standards...
  • MathSAT5

  • Referenced in 44 articles [sw09569]
  • tool. It supports most of the SMT-LIB theories and their combinations, and provides many...
  • SMTtoTPTP

  • Referenced in 5 articles [sw13650]
  • from proof problems written in the SMT-LIB format into the TPTP TFF format ... SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function ... SMTtoTPTP is useful for, e.g., making SMT-LIB problems available to TPTP system developers...
  • SIMPLY

  • Referenced in 5 articles [sw11807]
  • modeling language to the SMT-LIB format. n this paper we introduce Simply , a compiler ... modeling to the standard SMT-LIB format. The current version of Simply is able...
  • raSAT

  • Referenced in 7 articles [sw15206]
  • linux. raSAT accepts inequality problems in SMT-LIB format (.smt2) (including...
  • CLSAT

  • Referenced in 5 articles [sw08416]
  • clsat = SMT-LIB format parser + CNF converter + SAT solver + QF_IDL solver...
  • jSMTLIB

  • Referenced in 2 articles [sw19842]
  • adapter tools for SMT-LIBv2. The SMT-LIB standard defines an input format and response ... understand and apply the newly revised SMT-LIB format; the tutorial also describes fine points ... SMT-LIB format which, along with a compliance suite, will be useful to SMT implementors ... older solvers, such as Simplify, as SMT-LIB compliant tools...
  • fzn2smt

  • Referenced in 4 articles [sw13501]
  • FlatZinc language to the standard SMT-LIB language version 1.2. SMT stands for Satisfiability Modulo...
  • SONOLAR

  • Referenced in 2 articles [sw26291]
  • logic formulas. The solver supports the SMT-LIB format including the following logics: Bit vectors ... supports the symbols described in the SMT-LIB theory for floting point numbers. Since ... SMT-LIB logic names are yet to be defined for this theory, the logics...
  • JavaSMT

  • Referenced in 1 article [sw18525]
  • tools rely on SMT solving. The SMT-LIB initiative defines a common format for communication ... formula introspection are not supported by SMT-LIB directly. Additionally, using SMT-LIB for communication...
  • ARGO-LIB

  • Referenced in 2 articles [sw02619]
  • generic platform for decision procedures. ARGO-LIB is a C++ library that provides support ... decision procedures. This platform follows the SMT-LIB initiative which aims at establishing a library...
  • PySMT

  • Referenced in 1 article [sw19843]
  • native solvers, or by wrapping any SMT-Lib complaint solver, Dump your problems ... SMT-Lib format, and more...
  • SMT-Exec

  • Referenced in 1 article [sw13589]
  • solver execution service provided by the SMT-LIB initiative for the benefit ... similar interface, SMT-Exec permits members of the SMT community: to upload new solvers ... configurable experiments over available solvers and SMT-LIB benchmarks; and to view the results...
  • Z34Bio

  • Referenced in 1 article [sw25444]
  • studies which we make available as SMT-LIB benchmarks, to enable comparison of different analysis...
  • Boolector

  • Referenced in 27 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors...
  • z3

  • Referenced in 496 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • StarExec

  • Referenced in 35 articles [sw08839]
  • StarExec: Starexec is a cross community logic solving...
  • CVC4

  • Referenced in 104 articles [sw09485]
  • CVC4 is an efficient open-source automatic theorem...