Narrow sygus search space based on NNF and rewriting constant arguments.
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 22 Jan 2015 16:09:29 +0000 (17:09 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 22 Jan 2015 16:09:29 +0000 (17:09 +0100)
commit732dc4232ccf62d9b4a3ddf49fcfbd56efabcd41
treeb421689667af1b212d41c9b3c1c04cfc7cb11405
parentd9d13027f1f1e3cc462dc5885dfd0b529bf57512
Narrow sygus search space based on NNF and rewriting constant arguments.
src/smt/smt_engine.cpp
src/theory/bv/options
src/theory/datatypes/datatypes_sygus.cpp
src/theory/datatypes/datatypes_sygus.h
src/theory/quantifiers/ce_guided_instantiation.cpp