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
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
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;
{ 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; }
)?
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;
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;
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;
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;
}
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]
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() ){
//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{
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);
/* 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);
+ }
}
}
}
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();
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 ){
}
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
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;
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;
}
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;
}
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;
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;
}
}
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
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;
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,
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 );
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
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;
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();
}
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;
}
}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++ ){
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() );
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;
}
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) \
--- /dev/null
+; 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)
+
projects / cvc5.git / commitdiff