SIMPLY: A compiler from a CSP modeling language to the SMT-LIB format. n this paper we introduce Simply , a compiler from a declarative language for CSP modeling to the standard SMT-LIB format. The current version of Simply is able to generate problem instances falling into the quantifier free linear integer arithmetic logic. The compiler has been developed with the aim of building a system for easy CSP modeling and solving. By taking advantage of the year-over-year increase in performance of SMT solvers, we hope that such a system can serve as an alternative to other decision procedures in many applications. The compiler can also be used for easy SMT benchmark generation
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Ansótegui, Carlos; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (2013)
- Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving constraint satisfaction problems with SAT modulo theories (2012)
- Janičić, Predrag: URSA: a system for uniform reduction to SAT (2012)
- Bofill, Miquel; Suy, Josep; Villaret, Mateu: A system for solving constraint satisfaction problems with SMT (2010)