projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6940f33) | patch
Add finishInit for getInterpol and getAbduct. (#5316)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Wed, 21 Oct 2020 01:28:35 +0000 (20:28 -0500)
committerGitHub <noreply@github.com>
Wed, 21 Oct 2020 01:28:35 +0000 (20:28 -0500)
commite91077d81183c6c54ff0fdad5c6eb160f16c4205
tree764abcca8691c8aaca82066f208e168d8ef45c01tree
parent6940f336d9c63c4844438d6921a38f2c561a4195commit | diff
Add finishInit for getInterpol and getAbduct. (#5316)

This PR removes d_subSolver from SygusInterpol class. findInterpol function now receives the sub-solver as input (possibly through solveInterpolation function). In addition, finishInit is now called for getAbduct and getInterpol functions in smt_engine.cpp.
src/smt/interpolation_solver.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.h diff | blob | history