diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-11 15:03:52 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-11 15:03:52 +0200 |
commit | f1f79835adeac5c22fb744c38a83fef01d0002ad (patch) | |
tree | d6f69c1426ee36f8aeba5fbd0a92a008c4f68d7f /src/theory/quantifiers | |
parent | 5ad9f1e8a19d9658a86203fe2db8ad9fb329cd8e (diff) |
Update experimental scripts. Support top-level non-terminals in sygus grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 79199d8b4..60573a7fc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2070,7 +2070,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > } }else{ //print as let term - out << "(let ("; + if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ + out << "(let ("; + } std::vector< Node > subs_lvs; std::vector< Node > new_lvs; for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ @@ -2089,7 +2091,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << ")"; } } - out << ") "; + if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ + out << ") "; + } //print the body Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() ); let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() ); @@ -2104,7 +2108,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > printSygusTerm( new_str, n[i], lvs ); doReplace( body, old_str.str().c_str(), new_str.str().c_str() ); } - out << body << ")"; + out << body; + if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ + out << ")"; + } } return; } |