diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-14 20:41:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-14 20:41:19 +0000 |
commit | 068985035a64d556cbfc2e46af44566c01e0a5e0 (patch) | |
tree | 5c6a9c58eb0d740dec1f651bb7701028ae1beb73 /src/theory/uf | |
parent | 7e289e28e54afa144032048443202a88fa124cb5 (diff) |
Three things:
1. Infrastructure for unit T-conflicts added to SAT proxy
(and also the theory output channel documentation);
previously theories could not communicate unit T-conflicts
with the SAT layer because that layer had an implicit
assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true". These could
conceivably occur in artificial benchmarks in this form:
(let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 744a3d966..ee88df126 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -51,6 +51,11 @@ public: } static RewriteResponse preRewrite(TNode node) { + if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + } return RewriteResponse(REWRITE_DONE, node); } |