diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-28 10:35:17 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-28 10:35:17 -0500 |
| commit | 74c1ad7e4a8e93316b7555ac8a1b88ee777335e2 (patch) | |
| tree | 3f9c1b691a87a8cbbc73cc5bf46d23638d016856 /src/theory/quantifiers/term_util.h | |
| parent | a08914e449c3df26322551a968b4edee12a615f9 (diff) | |
Builtin evaluation functions for sygus (#1991)
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 70f8bbcee..2880713af 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -76,10 +76,6 @@ typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute; struct QuantIdNumAttributeId {}; typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; -/** sygus var num */ -struct SygusVarNumAttributeId {}; -typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute; - /** Attribute to mark Skolems as virtual terms */ struct VirtualTermSkolemAttributeId {}; typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute; |