projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a08f9d1) | patch
Add option --snorm-infer-eq to infer equalities based on normalization in ArithCongru...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 14 Apr 2016 16:38:51 +0000 (11:38 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 14 Apr 2016 16:38:51 +0000 (11:38 -0500)
commit4ce7a09a02bdcdf456d2028b3b4365c981a031f2
tree1dce3580517f717d263ab8969b95a351ffe497c1tree
parenta08f9d1f33c110ded40ee395d328de1fac087463commit | diff
Add option --snorm-infer-eq to infer equalities based on normalization in ArithCongruenceManager at standard effort (disabled by default).
src/options/arith_options diff | blob | history
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history