projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: edd69cb) | patch
Make nonlinear extension (more) deterministic (#4996)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 3 Sep 2020 13:39:58 +0000 (15:39 +0200)
committerGitHub <noreply@github.com>
Thu, 3 Sep 2020 13:39:58 +0000 (15:39 +0200)
commit337f8b791943e9b6b9a234f4f5422cf173342dd9
tree52250ac0a79463eb52fa617c6c34e958ee91ebf3tree
parentedd69cb2570692f36bf26b658e967c317ebc048ecommit | diff
Make nonlinear extension (more) deterministic (#4996)

This PR tries to make the nonlinear extension more deterministic by keeping the order of input assertion (instead of taking them from a hash set). This makes the ordering somewhat more robust against varying node ids, which proved to be a problem for debugging...
Also adds a few logging messages at interesting places.
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/engine_output_channel.cpp diff | blob | history