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 | |
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')
-rw-r--r-- | src/theory/output_channel.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 5 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index b25bf503d..a9722690b 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -72,7 +72,9 @@ public: * @param n - a conflict at the current decision level. This should * be an AND-kinded node of literals that are TRUE in the current * assignment and are in conflict (i.e., at least one must be - * assigned false). + * assigned false), or else a literal by itself (in the case of a + * unit conflict) which is assigned TRUE (and T-conflicting) in the + * current assignment. * * @param safe - whether it is safe to be interrupted */ 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); } |