projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2070474) | patch
Converting defined functions and let expressions from Sygus grammars to lambdas ...
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Thu, 23 Nov 2017 03:56:35 +0000 (21:56 -0600)
committerGitHub <noreply@github.com>
Thu, 23 Nov 2017 03:56:35 +0000 (21:56 -0600)
commitc9ae6b9812e737ae7932df91fa5f334d6d2588d4
tree61ac786790c044b88cf8589cc588e77760fe22e8tree
parent20704741e4609055d61e010b6981c6916d28019acommit | diff
Converting defined functions and let expressions from Sygus grammars to lambdas (#1403)

This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed.

The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
src/expr/datatype.cpp diff | blob | history
src/expr/datatype.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/quantifiers/sygus_grammar_norm.cpp diff | blob | history
src/theory/quantifiers/sygus_grammar_norm.h diff | blob | history