diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-02 08:33:49 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-02 08:33:49 -0500 |
| commit | 5401565e7622f9ee6b07abb68e1a9378cb9876a8 (patch) | |
| tree | 6aec7ada59563bdd8ecad7b78dbe4ab6d3014a3c /src/expr/node_manager.h | |
| parent | 5266e8e075ed222598449cb7bc058e095077d3ae (diff) | |
(proof-new) Updates to skolem manager interface (#4664)
Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c3435f445..098ff8eea 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -550,8 +550,10 @@ public: SKOLEM_DEFAULT = 0, /**< default behavior */ SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */ - SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ - }; + SKOLEM_IS_GLOBAL = 4, /**< global vars appear in models even after a pop */ + SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ + }; /* enum SkolemFlags */ + /** * Create a skolem constant with the given name, type, and comment. * |