diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 53 |
1 files changed, 41 insertions, 12 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e837980bd..90fc478f8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -683,19 +683,48 @@ void Smt2::defineSygusFuns() { void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) { - for( unsigned i=0; i<cnames.size(); i++ ){ - std::string name = dt.getName() + "_" + cnames[i]; - std::string testerId("is-"); - testerId.append(name); - checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId, ops[i] ); - for( unsigned j=0; j<cargs[i].size(); j++ ){ - std::stringstream sname; - sname << name << "_" << j; - c.addArg(sname.str(), cargs[i][j]); + for( int i=0; i<(int)cnames.size(); i++ ){ + bool is_dup = false; + //FIXME : should allow multiple operators with different sygus type arguments + // for now, just ignore them (introduces incompleteness). + for( int j=0; j<i; j++ ){ + if( ops[i]==ops[j] ){ + is_dup = true; + break; + } + /* + if( ops[i]==ops[j] && cargs[i].size()==cargs[j].size() ){ + is_dup = true; + for( unsigned k=0; k<cargs[i].size(); k++ ){ + if( cargs[i][k]!=cargs[j][k] ){ + is_dup = false; + break; + } + } + } + */ + } + if( is_dup ){ + Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl; + ops.erase( ops.begin() + i, ops.begin() + i + 1 ); + cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 ); + cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 ); + i--; + }else{ + std::string name = dt.getName() + "_" + cnames[i]; + std::string testerId("is-"); + testerId.append(name); + checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId, ops[i] ); + for( unsigned j=0; j<cargs[i].size(); j++ ){ + std::stringstream sname; + sname << name << "_" << j; + c.addArg(sname.str(), cargs[i][j]); + } + Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl; + dt.addConstructor(c); } - dt.addConstructor(c); } } |