projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 03541f4) | patch
Refactor sygus_util to TermDb. Initial work on solution reconstruction into syntax...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 4 Feb 2015 12:29:28 +0000 (13:29 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 4 Feb 2015 12:29:28 +0000 (13:29 +0100)
commit97e30c1089e42b668a914472b986f2d986190fc6
treec2072c1db332ba61268f23fd67959d134a2f2373tree
parent03541f4faeb820539ac25f06f1e64adc7aedca6fcommit | diff
Refactor sygus_util to TermDb.  Initial work on solution reconstruction into syntax for single inv properties.
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/datatypes/theory_datatypes.h diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history