projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8e476f1) | patch
Infrastructure for tautological literals in nonlinear solver (#3795)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 26 Feb 2020 23:15:02 +0000 (17:15 -0600)
committerGitHub <noreply@github.com>
Wed, 26 Feb 2020 23:15:02 +0000 (17:15 -0600)
commit19392f3e588287b2f0838f90b7e1a6adcf690063
treef5b989f2c5398122b7e7098360be5542ba7e5c69tree
parent8e476f1efeb7f8b3188ea1795ccd27f98f41e4d2commit | diff
Infrastructure for tautological literals in nonlinear solver (#3795)

Work towards CVC4/cvc4-projects#113 and #3783.

This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".

This PR is required for further refactoring of check-model for transcendental functions.
src/expr/node_algorithm.cpp diff | blob | history
src/expr/node_algorithm.h diff | blob | history
src/theory/arith/nl_model.cpp diff | blob | history
src/theory/arith/nl_model.h diff | blob | history
src/theory/arith/nonlinear_extension.cpp diff | blob | history