The Model-Validation Track Post-Processor
The SMT Competition Model-Validation Track post-processor script takes as input
a satisfiable SMT-LIB v2 problem that has a
(set-option :produce-models true)command and exactly one
(check-sat)command followed by one
the model returned by an SMT solver having the following structure:
sat (model (define-fun <var> () <type> <const>) ... )
<var> is the name of a bit-vector or boolean variable occurring in
the original problem,
<type> is the Boolean or bit-vector type of the
<const> is a constant value of the appropriate type.
The model validator uses pySMT to validate the model by substituting the model in the original formula and checking that is simplifies to True.
The validator will output
VALID if the model is a full model that satisfies
the input problem, and
INVALID followed by the reason if the model validation
did not succeed. It will output
UNKNOWN if the input model is empty.
ModelValidator.py script uses the pySMT pySMT
version packaged in this repository (pysmt.tar.xz). To run use
PYTHONPATH="pysmt" python2 ModelValidator.py.
See the pySMT documentation
for more information about pySMT.
ModelValidator.py [-h] --smt2 SMT2 --model MODEL
Alternatively (and on StarExec), you can use the provided wrapper script process.model-validation-track, which requires that the provided pySMT version is unpacked into the same directory as the script.
./process.model-validation-track SMT2 MODEL