projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 640a076) | patch
preprocessing context: Add wrapper for model substitutions. (#6370)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 15 Apr 2021 21:57:53 +0000 (14:57 -0700)
committerGitHub <noreply@github.com>
Thu, 15 Apr 2021 21:57:53 +0000 (21:57 +0000)
commitb7dcbee6f351c22ca3454d706d5773d01dd806fa
treeeef642fd1c9818ac32dd4dff7e13edfff6ff352ctree
parent640a07690826d4bbd87398949091b94b32e35c7acommit | diff
preprocessing context: Add wrapper for model substitutions. (#6370)

Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.

Fixes #5473.
src/preprocessing/passes/bv_eager_atoms.cpp diff | blob | history
src/preprocessing/passes/miplib_trick.cpp diff | blob | history
src/preprocessing/passes/non_clausal_simp.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/datatypes/v3l60006.cvc diff | blob | history
test/regress/regress0/issue5473.smt2 [new file with mode: 0644] blob