projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6d37c13) | patch
Single invocation module for counterexample guided quantifier instantiation --cegqi...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 2 Feb 2015 16:42:31 +0000 (17:42 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 2 Feb 2015 16:42:31 +0000 (17:42 +0100)
commit8deb9d980d7b0e281a0190539b756896a487c451
treece0bfe29b53cc16c8854fa6833f2dda3b9122c6ftree
parent6d37c136a251b957197269aeb389a9f1ae07e620commit | diff
Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring.  Do not apply exhaustive tester inference for sygus datatypes.
13 files changed:
src/Makefile.am diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp [new file with mode: 0644] blob
src/theory/quantifiers/ce_guided_single_inv.h [new file with mode: 0644] blob
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history