projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 624b03d) | patch
Allow non-value model values (#8076)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 7 Feb 2022 20:56:34 +0000 (12:56 -0800)
committerGitHub <noreply@github.com>
Mon, 7 Feb 2022 20:56:34 +0000 (20:56 +0000)
commit5eb347630fcccf038a8fae15946e35600bcc91ae
treed4d5c35773f95e07a4f6a1d986e7cbea3fa83373tree
parent624b03d3826f790bf1354276a974b5f76afe14c8commit | diff
Allow non-value model values (#8076)

We previously required model values to be "values", i.e., constants or constant-like stuff like real algebraic numbers or lambdas. This is an inherent problem for, e.g, transcendental models: the simplest model for a transcendental problem may legitimately be 3 * PI or PI + exp(3). This PR removes this restriction, only requiring that values are rewritten.
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/exp-in-model.smt2 [new file with mode: 0644] blob