projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9547af1) | patch
Remove "inUnsatCore" flag throughout (#6964)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 3 Aug 2021 01:21:04 +0000 (20:21 -0500)
committerGitHub <noreply@github.com>
Tue, 3 Aug 2021 01:21:04 +0000 (01:21 +0000)
commit6b55bf59675fcdaab4c8dbf70a8a74ebb1f990e9
tree5a3b4b8dff3f72acff78988ef7dd8def6597038btree
parent9547af1fb7fa26d6a3299ede363fc2faaae85908commit | diff
Remove "inUnsatCore" flag throughout (#6964)

The internal solver no longer cares about what assertions are named / are in the unsat core.

This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces.

This eliminates another external use of `getSmtEngine`.
14 files changed:
src/parser/smt2/Smt2.g diff | blob | history
src/parser/tptp/Tptp.g diff | blob | history
src/parser/tptp/tptp.cpp diff | blob | history
src/parser/tptp/tptp.h diff | blob | history
src/smt/assertions.cpp diff | blob | history
src/smt/assertions.h diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/command.h diff | blob | history
src/smt/quant_elim_solver.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/smt_solver.cpp diff | blob | history
src/smt/smt_solver.h diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history