diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 11:41:48 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 11:41:48 +0200 |
commit | 2679806e54a0b265fae26eb9cf76a5f6a618e963 (patch) | |
tree | 5de4f159ee57db57366dfab70f7b2640a578b734 /src/theory | |
parent | a0cb1add6db449c64c6ca63bc219761c8bc4a4de (diff) |
Support for arbitrary constants/variables in Sygus grammars.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6c32ccb4a..62eb78679 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1586,16 +1586,18 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) { const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); Node sc; - int carg = getOpArg( tn, c ); - if( carg!=-1 ){ - sc = Node::fromExpr( dt[carg].getSygusOp() ); + // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy + if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){ + Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); + SygusProxyAttribute spa; + k.setAttribute(spa,c); + sc = k; }else{ - //TODO - if( !options::cegqiSingleInvReconstructConst() ){ - Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); - SygusProxyAttribute spa; - k.setAttribute(spa,c); - sc = k; + int carg = getOpArg( tn, c ); + if( carg!=-1 ){ + sc = Node::fromExpr( dt[carg].getSygusOp() ); + }else{ + //TODO } } d_builtin_const_to_sygus[tn][c] = sc; |