diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 17:15:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 17:15:02 -0600 |
| commit | 19392f3e588287b2f0838f90b7e1a6adcf690063 (patch) | |
| tree | f5b989f2c5398122b7e7098360be5542ba7e5c69 /src/expr/node_algorithm.h | |
| parent | 8e476f1efeb7f8b3188ea1795ccd27f98f41e4d2 (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.
Diffstat (limited to 'src/expr/node_algorithm.h')
| -rw-r--r-- | src/expr/node_algorithm.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 929e1c5ef..e47029284 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -45,6 +45,13 @@ bool hasSubterm(TNode n, TNode t, bool strict = false); bool hasSubtermMulti(TNode n, TNode t); /** + * @param k The kind of node to check + * @param n The node to search in. + * @return true iff there is a term in n that has kind k + */ +bool hasSubtermKind(Kind k, Node n); + +/** * Check if the node n has a subterm that occurs in t. * @param n The node to search in * @param t The set of subterms to search for |