diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:35:47 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:35:47 -0500 |
commit | 0e513c05b2e0ae3b8e2d08514ccb8007258f963b (patch) | |
tree | 0b0b458a1a3d6415f4b7ff1f298fcd443cbb37fb /src/expr | |
parent | f3590092818d9eab9d961ea602093029ff472a85 (diff) |
Separate sygus term utilities to new file, minor cleanup from last commit.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index e45ca49e0..0c844f92d 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -114,6 +114,10 @@ bool NodeTemplate<ref_count>::hasBoundVar() { hasBv = (*i).hasBoundVar(); } if( !hasBv ){ + //FIXME : this is a hack to handle synthesis conjectures + // the issue is that we represent second-order quantification in synthesis conjectures via a Node: + // exists x forall y P[f,y], where x is a dummy variable that maps to f through attribute SygusSynthFunVarListAttributeId + // when asked whether a node has a bound variable, we want to treat f as if it were a bound (second-order) variable. -AJR if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){ hasBv = true; } |