projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cbd61aa) | patch
(proof-new) arith: dedup literals in flattenImpl (#5320)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 21 Oct 2020 18:40:02 +0000 (11:40 -0700)
committerGitHub <noreply@github.com>
Wed, 21 Oct 2020 18:40:02 +0000 (13:40 -0500)
commite4a3d7e78b72d4a8c6704f346540893bab4e00ef
tree8028371019bf1644a90d37cd9dc71e9b88c8ed8etree
parentcbd61aa8ee07e10846a3e69ea4ba4e42f0a16394commit | diff
(proof-new) arith: dedup literals in flattenImpl (#5320)

TheoryArithPrivte uses flattenImplication to turn implications into
clauses. This commit ensures that said clause does not have duplicate
terms. This is important because when we write proofs related to the
clause, the proof machinery doesn't like duplicates.
src/theory/arith/theory_arith_private.cpp diff | blob | history