BarcelogicTools

Barcelogic for SMT is an efficient implementation of the DPLL(T) framework [Ganzingeretal2004CAV, Nieuwenhuisetal2005LPAR]. A DPLL(T) system consists of a general DPLL(X) engine, very similar in nature to a SAT solver, whose parameter X can be instantiated with a solver for a theory T. Once the DPLL(X) engine has been implemented, this approach becomes extremely flexible: new theories can be dealt with by simply plugging in new theory solvers. These solvers only must be able to deal with conjunctions of theory literals and conform to a minimal and simple interface [Ganzingeretal2004CAV]. Currently, Barcelogic for SMT supports difference logic over the integers of the reals, equality with uninterpreted function symbols (EUF) and the interpreted function symbols predecessor and successor, or combinations of these theories. The input formulas given to the system have to be in the SMT-LIB format.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 7 articles , 1 standard article )

Showing results 1 to 7 of 7.
Sorted by year (citations)

  1. Brummayer, Robert; Biere, Armin: Lemmas on demand for the extensional theory of arrays (2009)
  2. Faure, Germain; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric: SAT modulo the theory of linear arithmetic: Exact, inexact and commercial solvers (2008)
  3. Tveretina, Olga; Wesselink, Wieger: EufDPLL -- a tool to check satisfiability of equality logic formulas (2008)
  4. Lev-Ami, Tal; Weidenbach, Christoph; Reps, Thomas; Sagiv, Mooly: Labelled clauses (2007)
  5. Seshia, Sanjit A.; Subramani, K.; Bryant, Randal E.: On solving Boolean combinations of UTVPI constraints. (2007)
  6. Sheini, Hossein M.; Sakallah, Karem A.: A progressive simplifier for satisfiability modulo theories (2006)
  7. Nieuwenhuis, Robert; Oliveras, Albert: Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools (2005)