diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/expr/node_manager.cpp | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a9be51418..ebf78f541 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -780,6 +780,13 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } +Node NodeManager::mkBooleanTermVariable() { + Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE); + n.setAttribute(TypeAttr(), booleanType()); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ |