diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-20 14:52:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-20 14:52:31 -0500 |
commit | 78373c7f5fe93b7e8bbea10e3924f24d25a618ac (patch) | |
tree | b3bd84e3d2154a4835679c71c028e87dbe1e2665 /src/theory/quantifiers/term_util.h | |
parent | fc0a5dcc002b12f075681d53e87cca1ddfbd479d (diff) |
Make Sygus conjectures higher-order (#1244)
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.
* Minor fix
* Fix bug in Node::hasBoundVar for non-ground operators.
* Add regression.
* Address review.
* Apply clang format.
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
-rw-r--r-- | src/theory/quantifiers/term_util.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 2360c5bfb..a0b3b8ec2 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -73,8 +73,9 @@ struct SygusProxyAttributeId {}; typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute; // attribute for associating a synthesis function with a first order variable -struct SygusSynthFunAttributeId {}; -typedef expr::Attribute<SygusSynthFunAttributeId, Node> SygusSynthFunAttribute; +struct SygusSynthGrammarAttributeId {}; +typedef expr::Attribute<SygusSynthGrammarAttributeId, Node> + SygusSynthGrammarAttribute; // attribute for associating a variable list with a synth fun struct SygusSynthFunVarListAttributeId {}; |