projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 874350b) | patch
Allow to use the initial assignment for CAD (#5177)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 1 Oct 2020 16:24:55 +0000 (18:24 +0200)
committerGitHub <noreply@github.com>
Thu, 1 Oct 2020 16:24:55 +0000 (11:24 -0500)
commit25aaeabe85f8c3f2c6701fcd48f00f221f8dfccf
treed05317d4f4aeae7b3f70ea250ca146b00112a1b3tree
parent874350b54bd0f275fa8af7ca7a7af186bde7c030commit | diff
Allow to use the initial assignment for CAD (#5177)

While the CAD subsolver already provided for a way to use the linear model to seed the model search, it was not actually used yet.
This PR now does use it, though it is disabled by a Boolean flag.
src/options/arith_options.toml diff | blob | history
src/theory/arith/nl/cad/cdcac.cpp diff | blob | history
src/theory/arith/nl/cad_solver.cpp diff | blob | history