diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 16:43:03 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 16:43:03 +0200 |
| commit | 5ad9f1e8a19d9658a86203fe2db8ad9fb329cd8e (patch) | |
| tree | 4fbad0c7f524ed3cc92a824fd50373b0fdf51e8a | |
| parent | 2f2b368448c3a5e50db46b3ec2cc364ae8959ac1 (diff) | |
Bug fix parsing constant constructor sygus.
| -rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 54938a686..aa56d1f2e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -878,10 +878,11 @@ sygusGTerm[int index, PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor.")); } cargs[index].pop_back(); - Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl; - if( gtermType==2 ){ + Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << ", gterm type=" << sub_gtermType << std::endl; + if( sub_gtermType==2 ){ std::vector< Expr > consts; PARSER_STATE->mkSygusConstantsForType( t, consts ); + Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; for( unsigned i=0; i<consts.size(); i++ ){ std::stringstream ss; ss << consts[i]; @@ -891,6 +892,7 @@ sygusGTerm[int index, cargs[index].push_back( std::vector< CVC4::Type >() ); } }else if( sub_gtermType==3 ){ + Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; for( unsigned i=0; i<sygus_vars.size(); i++ ){ if( sygus_vars[i].getType()==t ){ std::stringstream ss; |