projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a1e9511) | patch
(cad solver) Use the current model as initial assignment (#4893)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Sun, 16 Aug 2020 00:28:27 +0000 (02:28 +0200)
committerGitHub <noreply@github.com>
Sun, 16 Aug 2020 00:28:27 +0000 (19:28 -0500)
commitf4f7f148082535c23e24a0b92cdf2612f0598072
tree68ae2c80605b49f4320329da1d86d6ebaf3554fbtree
parenta1e951127f7a3af158ca1408e62bd46d5cb065ffcommit | diff
(cad solver) Use the current model as initial assignment (#4893)

This PR implements a first naive way to employ the linear model (obtained from the nonlinear extension) to guide the initial sampling within the cad solver.
src/theory/arith/nl/cad/cdcac.cpp diff | blob | history
src/theory/arith/nl/cad/cdcac.h diff | blob | history