z3verificationsmtformal-verificationsat

SMT solver with custom theories?


I'm looking at doing some verification work where I've got regular tree grammars as an underlying theory.

Z3 lets you define your own stuff with uninterpreted functions, but that doesn't tend to work well any time your decision procedures are recursive. They used to allow for plugins but that has been depricated, I think.

I'm wondering, does anybody have a recommendation of a decent SMT solver that allows you to write decision procedures for custom theories?


Solution

  • There are several options given that most reasonable SMT solvers are open source you can integrate theory solvers in any detail depending on how much time and energy you have to spend.

    Again, I would say that for a first version you should get pretty far with an external integration where you let the SMT solver deal with propositional SAT and uninterpreted functions (and arithmetic if you need this). You can then ask the solver for a model and add theory axioms back until the propositional model you get back from the solver aligns with your theory (or you get UNSAT). Not all assignments in the propositional model are going to be relevant. You can minimize the number of assignments you consider by applying dual propagation (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/29_niemetz.pdf).