diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-18 14:21:13 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-18 14:21:13 +0200 |
commit | eee182ae7479d688aec42f630d2aa6b2636cc2f9 (patch) | |
tree | 5eb86c02e8702173e863b774c9ba1df724034fcd /src/parser | |
parent | 1aaf70f23d8f2061e5c05ca98d12deea06494a25 (diff) |
More work mixing UF and sygus.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 |
2 files changed, 11 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4e5c27e3d..cfcc7df99 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -396,6 +396,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support push command."); } } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { @@ -425,6 +426,7 @@ command returns [CVC4::Command* cmd = NULL] } } ) | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support pop command."); } } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n > PARSER_STATE->scopeLevel()) { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7e621f56b..d3af9143a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -344,6 +344,8 @@ void Smt2::setLogic(std::string name) { name = "UFLIRA"; } else if(name == "BV") { name = "UFBV"; + } else if(name == "ALL_SUPPORTED") { + //no change } else { std::stringstream ss; ss << "Unknown SyGuS background logic `" << name << "'"; @@ -513,7 +515,7 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) } void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){ - if( range.isInteger() || range.isBitVector() || range.isDatatype() ){ + if( !range.isBoolean() ){ if( std::find( types.begin(), types.end(), range )==types.end() ){ Debug("parser-sygus") << "...will make grammar for " << range << std::endl; types.push_back( range ); @@ -534,9 +536,9 @@ void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::m void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) { - if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ - parseError("No default grammar for type."); - } + //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ + // parseError("No default grammar for type."); + //} startIndex = -1; Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; @@ -628,6 +630,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin cargs.push_back( std::vector< CVC4::Type >() ); for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){ Type crange = ((SelectorType)dt[k][j].getType()).getRangeType(); + //Assert( type_to_unres.find(crange)!=type_to_unres.end() ); cargs.back().push_back( type_to_unres[crange] ); } } @@ -645,6 +648,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin ops[i].push_back( sels[types[i]][j].getSelector() ); cnames.push_back( sels[types[i]][j].getName() ); cargs.push_back( std::vector< CVC4::Type >() ); + //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() ); cargs.back().push_back( type_to_unres[arg_type] ); } } @@ -1324,6 +1328,7 @@ void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std:: CVC4::DatatypeConstructor c(name, testerId ); c.setSygus( op, let_body, let_args, let_num_input_args ); for( unsigned j=0; j<cargs.size(); j++ ){ + Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl; std::stringstream sname; sname << name << "_" << j; c.addArg(sname.str(), cargs[j]); |