projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2fb903e) | patch
Support model cores via option --produce-model-cores. (#2407)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 11 Sep 2018 18:08:00 +0000 (13:08 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 11 Sep 2018 18:08:00 +0000 (11:08 -0700)
commit64c48c4d3b4c26b0ba28ab1ab11ef2314ca0cbee
treeece6319150e855d2b0850f7508d9e3ee080b7f03tree
parent2fb903ed7309fd97c848b03f6587c9d0604efd24commit | diff
Support model cores via option --produce-model-cores. (#2407)

This adds support for model cores, fixes #1233.

It includes some minor cleanup and additions to utility functions.
17 files changed:
src/Makefile.am diff | blob | history
src/options/smt_options.toml diff | blob | history
src/printer/printer.cpp diff | blob | history
src/smt/model.h diff | blob | history
src/smt/model_core_builder.cpp [new file with mode: 0644] blob
src/smt/model_core_builder.h [new file with mode: 0644] blob
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/theory_bv_utils.cpp diff | blob | history
src/theory/bv/theory_bv_utils.h diff | blob | history
src/theory/quantifiers/term_util.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history
src/theory/subs_minimize.cpp [new file with mode: 0644] blob
src/theory/subs_minimize.h [new file with mode: 0644] blob
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress0/model-core.smt2 [new file with mode: 0644] blob