diff options
| -rwxr-xr-x | contrib/run-script-smtcomp2015-application-experimental | 2 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-experimental | 8 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 102 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 103 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 22 | ||||
| -rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 13 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/tl-type.sy | 11 |
9 files changed, 192 insertions, 75 deletions
diff --git a/contrib/run-script-smtcomp2015-application-experimental b/contrib/run-script-smtcomp2015-application-experimental index dac870c75..81d05c774 100755 --- a/contrib/run-script-smtcomp2015-application-experimental +++ b/contrib/run-script-smtcomp2015-application-experimental @@ -36,7 +36,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) runcvc4 --incremental ;; LIA|LRA|NIA|NRA) - runcvc4 --incremental --cbqi + runcvc4 --incremental --cbqi2 ;; QF_BV) runcvc4 --incremental --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental index 8aee209e0..02766943f 100755 --- a/contrib/run-script-smtcomp2015-experimental +++ b/contrib/run-script-smtcomp2015-experimental @@ -67,10 +67,14 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 180 --cbqi --full-saturate-quant + trywith 240 --cbqi2 --full-saturate-quant trywith 60 --full-saturate-quant + trywith 180 --cbqi --cbqi-recurse --full-saturate-quant + trywith 180 --cbqi2 --decision=internal --full-saturate-quant trywith 180 --qcf-tconstraint --full-saturate-quant - finishwith --cbqi --cbqi-recurse --full-saturate-quant + trywith 180 --cbqi --decision=internal --full-saturate-quant + trywith 180 --cbqi --full-saturate-quant + finishwith --cbqi2 --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 600 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index aa56d1f2e..0f020c36e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -496,7 +496,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector< std::vector<Expr> > ops; std::vector< std::vector< std::string > > cnames; std::vector< std::vector< std::vector< CVC4::Type > > > cargs; - bool allow_const = false; + std::vector< bool > allow_const; + std::vector< std::vector< std::string > > unresolved_gterm_sym; bool read_syntax = false; int sygus_dt_index = 0; Type sygus_ret; @@ -609,30 +610,21 @@ sygusCommand returns [CVC4::Command* cmd = NULL] { std::stringstream ss; ss << fun << "_" << name; std::string dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs); + PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym); if(!PARSER_STATE->isUnresolvedType(dname)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); } Type unres_t = PARSER_STATE->mkUnresolvedType(dname); sygus_to_builtin[unres_t] = t; - sygus_dt_index = ops.size()-1; + sygus_dt_index = datatypes.size()-1; Debug("parser-sygus") << "Read sygus grammar " << name << " under function " << fun << "..." << std::endl; } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, allow_const, sygus_ret, -1]+ RPAREN_TOK - RPAREN_TOK - { Debug("parser-sygus") << "Making sygus datatypes..." << std::endl; - for( unsigned i=sygus_dt_index; i<datatypes.size(); i++ ){ - Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl; - if( sorts[i].isNull() ){ - PARSER_STATE->parseError(std::string("Internal error : could not infer builtin sort for nested gterm.")); - } - datatypes[i].setSygus( sorts[i], terms[0], sygus_dt_index==(int)i ? allow_const : false, false ); - PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i] ); - } - PARSER_STATE->popScope(); } + LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sygus_ret, -1]+ RPAREN_TOK + RPAREN_TOK { PARSER_STATE->popScope(); } )+ RPAREN_TOK { read_syntax = true; } )? @@ -640,6 +632,20 @@ sygusCommand returns [CVC4::Command* cmd = NULL] if( !read_syntax ){ //create the default grammar PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars ); + }else{ + Debug("parser-sygus") << "Making sygus datatypes..." << std::endl; + //make unresolved types to recognize + for( unsigned i=0; i<datatypes.size(); i++ ){ + PARSER_STATE->mkUnresolvedType(datatypes[i].getName()); + } + for( unsigned i=0; i<datatypes.size(); i++ ){ + Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl; + if( sorts[i].isNull() ){ + PARSER_STATE->parseError(std::string("Internal error : could not infer builtin sort for nested gterm.")); + } + datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false ); + PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i] ); + } } PARSER_STATE->popScope(); Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl; @@ -739,9 +745,11 @@ sygusGTerm[int index, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool > allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym, std::vector<CVC4::Expr>& sygus_vars, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, - bool& allow_const, CVC4::Type& ret, int gtermType] + CVC4::Type& ret, int gtermType] @declarations { std::string name; Kind k; @@ -751,7 +759,6 @@ sygusGTerm[int index, std::string sname; // 0 builtin operator, 1 defined operator, 2 any constant, 3 any variable, 4 ignore, 5 let, -1 none int sub_gtermType = -1; - bool sub_allow_const = false; Type sub_ret; int sub_dt_index = -1; std::string sub_dname; @@ -759,7 +766,7 @@ sygusGTerm[int index, Expr null_expr; std::vector< Expr > let_vars; int let_start_index = -1; - int let_end_index = -1; + //int let_end_index = -1; int let_end_arg_index = -1; Expr let_func; } @@ -792,21 +799,23 @@ sygusGTerm[int index, std::stringstream ss; ss << datatypes[index].getName() << "_let_var_" << let_vars.size(); sub_dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs ); + PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); sub_dt_index = datatypes.size()-1; sub_ret = null_type; } - sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType] { + sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym, + sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType] { Debug("parser-sygus") << "Process argument #" << let_vars.size() << "..." << std::endl; - Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); cargs[index].back().push_back(tt); } RPAREN_TOK )+ RPAREN_TOK { - let_end_index = datatypes.size(); + //let_end_index = datatypes.size(); let_end_arg_index = cargs[index].back().size(); } | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] - { sub_gtermType = 2; allow_const = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; } + { sub_gtermType = 2; allow_const[index] = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; } | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar variable." << std::endl; } | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] @@ -852,26 +861,28 @@ sygusGTerm[int index, std::stringstream ss; ss << datatypes[index].getName() << "_" << name << "_arg_" << count; sub_dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs ); + PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); sub_dt_index = datatypes.size()-1; sub_ret = null_type; } - ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType] + ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym, + sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType] { Debug("parser-sygus") << "Process argument #" << count << "..." << std::endl; - Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); cargs[index].back().push_back(tt); //add next datatype definition for argument count++; std::stringstream ss; ss << datatypes[index].getName() << "_" << name << "_arg_" << count; sub_dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs ); + PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); sub_dt_index = datatypes.size()-1; sub_ret = null_type; } )* RPAREN_TOK { //pop argument datatype definition - PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs ); + PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); //process constant/variable case if( sub_gtermType==2 || sub_gtermType==3 || sub_gtermType==4 ){ if( !cargs[index].back().empty() ){ @@ -916,7 +927,7 @@ sygusGTerm[int index, //remove datatypes defining body //while( (int)datatypes.size()>let_end_index ){ // Debug("parser-sygus") << "Removing let body datatype " << datatypes[datatypes.size()-1].getName() << std::endl; - // PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs ); + // PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); //} //Debug("parser-sygus") << "Done let body datatypes" << std::endl; }else{ @@ -969,7 +980,8 @@ sygusGTerm[int index, ret = PARSER_STATE->getSort(name); }else{ if( gtermType==-1 ){ - //if we don't know what this symbol is, and it is top level, just ignore it + Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl; + unresolved_gterm_sym[index].push_back(name); }else{ Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved " << name << std::endl; ret = PARSER_STATE->mkUnresolvedType(name); @@ -1783,19 +1795,23 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* a variable */ | symbol[name,CHECK_DECLARED,SYM_VARIABLE] - { const bool isDefinedFunction = - PARSER_STATE->isDefinedFunction(name); - if(PARSER_STATE->isAbstractValue(name)) { - expr = PARSER_STATE->mkAbstractValue(name); - } else if(isDefinedFunction) { - expr = MK_EXPR(CVC4::kind::APPLY, - PARSER_STATE->getFunction(name)); - } else { - expr = PARSER_STATE->getVariable(name); - Type t = PARSER_STATE->getType(name); - if(t.isConstructor() && ConstructorType(t).getArity() == 0) { - // don't require parentheses, immediately turn it into an apply - expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); + { if( PARSER_STATE->sygus() && name[0]=='-' ){ //allow unary minus in sygus + expr = MK_CONST(Rational(name)); + }else{ + const bool isDefinedFunction = + PARSER_STATE->isDefinedFunction(name); + if(PARSER_STATE->isAbstractValue(name)) { + expr = PARSER_STATE->mkAbstractValue(name); + } else if(isDefinedFunction) { + expr = MK_EXPR(CVC4::kind::APPLY, + PARSER_STATE->getFunction(name)); + } else { + expr = PARSER_STATE->getVariable(name); + Type t = PARSER_STATE->getType(name); + if(t.isConstructor() && ConstructorType(t).getArity() == 0) { + // don't require parentheses, immediately turn it into an apply + expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); + } } } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7db87d579..ceab0a779 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -500,7 +500,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ) { Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; - + std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); @@ -512,6 +512,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin ops.push_back(std::vector<Expr>()); std::vector<std::string> cnames; std::vector<std::vector<CVC4::Type> > cargs; + std::vector<std::string> unresolved_gterm_sym; //variables for( unsigned i=0; i<sygus_vars.size(); i++ ){ if( sygus_vars[i].getType()==range ){ @@ -561,7 +562,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin } Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; datatypes.back().setSygus( range, bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym ); sorts.push_back( range ); //Boolean type @@ -597,7 +598,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; Type btype = getExprManager()->booleanType(); datatypes.back().setSygus( btype, bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym ); sorts.push_back( btype ); Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl; @@ -622,12 +623,16 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs ){ + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym ){ sorts.push_back(t); datatypes.push_back(Datatype(dname)); ops.push_back(std::vector<Expr>()); cnames.push_back(std::vector<std::string>()); cargs.push_back(std::vector<std::vector<CVC4::Type> >()); + allow_const.push_back(false); + unresolved_gterm_sym.push_back(std::vector< std::string >()); return true; } @@ -635,12 +640,16 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs ){ + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym ){ sorts.pop_back(); datatypes.pop_back(); ops.pop_back(); cnames.pop_back(); cargs.pop_back(); + allow_const.pop_back(); + unresolved_gterm_sym.pop_back(); return true; } @@ -649,6 +658,8 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) { Type t = sub_ret; @@ -705,7 +716,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl; //otherwise, datatype was unecessary //pop argument datatype definition - popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs ); + popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); } return t; } @@ -870,7 +881,10 @@ 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 ) { + std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, + std::vector<std::string>& unresolved_gterm_sym ) { + Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; + Debug("parser-sygus") << " add constructors..." << std::endl; for( int i=0; i<(int)cnames.size(); i++ ){ bool is_dup = false; //FIXME : should allow multiple operators with different sygus type arguments @@ -899,13 +913,6 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, 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 ); - Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl; Expr let_body; std::vector< Expr > let_args; unsigned let_num_input_args = 0; @@ -914,19 +921,73 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, let_body = it->second; let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() ); let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]]; - Debug("parser-sygus") << " it is a let gterm with body " << let_body << std::endl; } - c.setSygus( ops[i], let_body, let_args, let_num_input_args ); - for( unsigned j=0; j<cargs[i].size(); j++ ){ - std::stringstream sname; - sname << name << "_" << j; - c.addArg(sname.str(), cargs[i][j]); + addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args ); + } + } + Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl; + if( !unresolved_gterm_sym.empty() ){ + std::vector< Type > types; + Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl; + for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){ + Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl; + if( isUnresolvedType(unresolved_gterm_sym[i]) ){ + Debug("parser-sygus") << " it is an unresolved type." << std::endl; + Type t = getSort(unresolved_gterm_sym[i]); + if( std::find( types.begin(), types.end(), t )==types.end() ){ + types.push_back( t ); + //identity element + Type bt = dt.getSygusType(); + Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; + std::stringstream ss; + ss << t << "_x_id"; + Expr let_body = mkBoundVar(ss.str(), bt); + std::vector< Expr > let_args; + let_args.push_back( let_body ); + //make the identity function + Type ft = getExprManager()->mkFunctionType(bt, bt); + std::stringstream ssid; + ssid << unresolved_gterm_sym[i] << "_id"; + Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); + //make the sygus argument list + std::vector< Type > id_carg; + id_carg.push_back( t ); + addSygusDatatypeConstructor( dt, id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 ); + //add to operators + ops.push_back( id_op ); + } + }else{ + Debug("parser-sygus") << " ignore. (likely a free let variable)" << std::endl; } - dt.addConstructor(c); } } + } +void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, + CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) { + + std::string name = dt.getName() + "_" + cname; + std::string testerId("is-"); + testerId.append(name); + checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId ); + Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl; + if( !let_body.isNull() ){ + Debug("parser-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; + } + c.setSygus( op, let_body, let_args, let_num_input_args ); + for( unsigned j=0; j<cargs.size(); j++ ){ + std::stringstream sname; + sname << name << "_" << j; + c.addArg(sname.str(), cargs[j]); + } + dt.addConstructor(c); +} + + // i is index in datatypes/ops // j is index is datatype Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 428977e0b..cfd062457 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -188,19 +188,25 @@ public: std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs ); + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym ); static bool popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs ); + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym ); Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); @@ -223,7 +229,8 @@ public: void defineSygusFuns(); void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, - std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ); + std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, + std::vector<std::string>& unresolved_gterm_sym ); // i is index in datatypes/ops // j is index is datatype @@ -265,6 +272,12 @@ public: name.find_first_not_of("0123456789", 1) != std::string::npos ) { this->Parser::checkDeclaration(name, check, type, notes); return; + }else{ + //it is allowable in sygus + if( sygus() && name[0]=='-' ){ + //do not check anything + return; + } } std::stringstream ss; @@ -304,6 +317,9 @@ private: std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars; void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); + + void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, + CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); void addArithmeticOperators(); diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index a9e6b3a78..d08c92dd9 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1114,12 +1114,13 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node } bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) { - Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << std::endl; TypeNode tn = tst_curr[0].getType(); + Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << " " << tn << std::endl; Node rop = rep_prog.getNumChildren()==0 ? rep_prog : rep_prog.getOperator(); //we can continue if the tester in question is relevant if( std::find( rlv_testers.begin(), rlv_testers.end(), tst_curr )!=rlv_testers.end() ){ unsigned tindex = Datatype::indexOf( tst_curr.getOperator().toExpr() ); + d_tds->registerSygusType( tn ); Node op = d_tds->getArgOp( tn, tindex ); if( op!=rop ){ Trace("sygus-nf-gen-debug") << "mismatch, success." << std::endl; 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; } diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index dc6a1e0d1..abf51d992 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -35,7 +35,8 @@ TESTS = commutative.sy \ no-flat-simp.sy \ twolets2-orig.sy \ let-ringer.sy \ - let-simp.sy + let-simp.sy \ + tl-type.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy new file mode 100644 index 000000000..a8da13742 --- /dev/null +++ b/test/regress/regress0/sygus/tl-type.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-cegqi-si +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int (Term (+ Start Start))) + (Term Int (x 0)))) + +(declare-var x Int) +(constraint (= (f x) (* 3 x))) +(check-synth) + |