projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d43fe7) | patch
Introduce SyGuS datatype API (#3465)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 15 Nov 2019 22:11:34 +0000 (16:11 -0600)
committerGitHub <noreply@github.com>
Fri, 15 Nov 2019 22:11:34 +0000 (16:11 -0600)
commit5482ab60880e4611354354d863367411a99d540c
treeb284e08e9ee45e009d6952d90964b80944d6296atree
parent7d43fe797c2ec03b76dd55cdb5485fb62d0dfb3acommit | diff
Introduce SyGuS datatype API (#3465)
src/expr/CMakeLists.txt diff | blob | history
src/expr/sygus_datatype.cpp [new file with mode: 0644] blob
src/expr/sygus_datatype.h [new file with mode: 0644] blob
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/sygus_extension.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.h diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_norm.h diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus/type_info.cpp diff | blob | history