SMCHR swMATH ID: 9322 Software Authors: Duck, Gregory J. Description: SMCHR: satisfiability modulo constraint handling rules. Constraint handling rules (CHRs) are a high-level rule-based programming language for specification and implementation of constraint solvers. CHR manipulates a global store representing a flat conjunction of constraints. By default, CHR does not support goals with a more complex propositional structure including disjunction, negation, etc., or CHR relies on the host system to provide such features. In this paper we introduce satisfiability modulo constraint handling rules (SMCHR): a tight integration of CHR with a modern Boolean satisfiability (SAT) solver for quantifier-free formulae with an arbitrary propositional structure. SMCHR is essentially a satisfiability modulo theories (SMT) solver where the theory T is implemented in CHR. The execution algorithm of SMCHR is based on lazy clause generation, where a new clause for the SAT solver is generated whenever a rule is applied. We shall also explore the practical aspects of building an SMCHR system, including extending a “built-in” constraint solver supporting equality with unification and justifications. Homepage: http://www.google.de/#sclient=psy&hl=de&source=hp&q=SMCHR Keywords: CHR; satisfiability modulo theories; lazy clause generation Related Software: Smallfoot; CBMC; SLAyer; LLBMC; VeriFast; Predator Cited in: 2 Publications Cited by 3 Authors 2 Duck, Gregory J. 1 Jaffar, Joxan 1 Yap, Roland H. C. Cited in 1 Serial 2 Theory and Practice of Logic Programming Cited in 1 Field 2 Computer science (68-XX) Citations by Year