projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3520346) | patch
Fixes for sygus inference (#2238)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 6 Aug 2018 23:55:29 +0000 (18:55 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Mon, 6 Aug 2018 23:55:29 +0000 (16:55 -0700)
commit79121aeeb03bf70323208d5059e23dfb62a83903
tree11d96cd290f59f506d039de3df008d97ed8451e8tree
parent352034696fdce868452d097d155f195ea1fa949ccommit | diff
Fixes for sygus inference (#2238)

This includes:
- Enabling sygus-specific options in SmtEngine::setDefaults,
- Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks),
- Treating free constants as functions to synthesize
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/sygus_inference.cpp diff | blob | history