From 2679806e54a0b265fae26eb9cf76a5f6a618e963 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 11 May 2015 11:41:48 +0200 Subject: Support for arbitrary constants/variables in Sygus grammars. --- src/theory/quantifiers/term_database.cpp | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'src/theory/quantifiers/term_database.cpp') 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; -- cgit v1.2.3