From: ajreynol Date: Thu, 11 Jun 2015 16:13:37 +0000 (+0200) Subject: Avoid naming conflicts in sygus, refactor. Add missing regression. Detect Start... X-Git-Tag: cvc5-1.0.0~6293 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aaabd78a7573bf03068ca1bf4aa1389627f11326;p=cvc5.git Avoid naming conflicts in sygus, refactor. Add missing regression. Detect Start grammar. Add regression. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ffa2994fc..11ddf2a15 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -503,6 +503,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Type sygus_ret; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr; + int startIndex = -1; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -606,26 +607,34 @@ sygusCommand returns [CVC4::Command* cmd = NULL] sortSymbol[range,CHECK_DECLARED] ( LPAREN_TOK ( LPAREN_TOK - symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); } + symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] { std::stringstream ss; ss << fun << "_" << name; + if( name=="Start" ){ + startIndex = datatypes.size(); + } std::string dname = ss.str(); PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym); + Type unres_t; if(!PARSER_STATE->isUnresolvedType(dname)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); + unres_t = PARSER_STATE->mkUnresolvedType(dname); + }else{ + unres_t = PARSER_STATE->getSort(dname); } - Type unres_t = PARSER_STATE->mkUnresolvedType(dname); sygus_to_builtin[unres_t] = t; sygus_dt_index = datatypes.size()-1; - Debug("parser-sygus") << "Read sygus grammar " << name << " under function " << fun << "..." << std::endl; + Debug("parser-sygus") << "--- Read sygus grammar " << name << " under function " << fun << "..." << std::endl; + Debug("parser-sygus") << " type to resolve " << unres_t << std::endl; + Debug("parser-sygus") << " builtin type " << t << 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, 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 )+ RPAREN_TOK { read_syntax = true; } )? @@ -634,10 +643,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] //create the default grammar PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars ); }else{ + //swap index if necessary Debug("parser-sygus") << "Making sygus datatypes..." << std::endl; - //make unresolved types to recognize for( unsigned i=0; imkUnresolvedType(datatypes[i].getName()); + Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl; } for( unsigned i=0; imkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin ); } + //only care about datatypes/sorts/ops past here + if( startIndex>0 ){ + // PARSER_STATE->swapSygusStart( startIndex, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); + CVC4::Datatype tmp_dt = datatypes[0]; + Type tmp_sort = sorts[0]; + std::vector< Expr > tmp_ops; + tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); + datatypes[0] = datatypes[startIndex]; + sorts[0] = sorts[startIndex]; + ops[0].clear(); + ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() ); + datatypes[startIndex] = tmp_dt; + sorts[startIndex] = tmp_sort; + ops[startIndex].clear(); + ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() ); + } } PARSER_STATE->popScope(); Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl; @@ -798,7 +823,7 @@ sygusGTerm[int index, Expr v = PARSER_STATE->mkBoundVar(sname,t); let_vars.push_back( v ); std::stringstream ss; - ss << datatypes[index].getName() << "_let_var_" << let_vars.size(); + ss << datatypes[index].getName() << "_" << ops[index].size() << "_lv_" << let_vars.size(); sub_dname = ss.str(); PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); sub_dt_index = datatypes.size()-1; @@ -860,7 +885,7 @@ sygusGTerm[int index, //add datatype definition for argument count++; std::stringstream ss; - ss << datatypes[index].getName() << "_" << name << "_arg_" << count; + ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count; sub_dname = ss.str(); PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); sub_dt_index = datatypes.size()-1; @@ -875,7 +900,7 @@ sygusGTerm[int index, //add next datatype definition for argument count++; std::stringstream ss; - ss << datatypes[index].getName() << "_" << name << "_arg_" << count; + ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count; sub_dname = ss.str(); PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); sub_dt_index = datatypes.size()-1; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 17bedf115..47022da3e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -653,7 +653,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, unresolved_gterm_sym.pop_back(); return true; } - + Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector >& ops, @@ -927,6 +927,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, Expr v = mkBoundVar(ss.str(), bt); let_args.push_back( v ); fsorts.push_back( bt ); + Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl; } //make the let_body std::vector< Expr > children; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 50f755fef..dbef0494a 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -37,7 +37,8 @@ TESTS = commutative.sy \ let-ringer.sy \ let-simp.sy \ tl-type.sy \ - dup-op.sy + dup-op.sy \ + nflat-fwd.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy new file mode 100644 index 000000000..dbf415986 --- /dev/null +++ b/test/regress/regress0/sygus/dup-op.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-cegqi-si +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ Con Con) (+ Start Start) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) (* 2 x))) +(check-synth) + diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy new file mode 100644 index 000000000..0f9d46215 --- /dev/null +++ b/test/regress/regress0/sygus/nflat-fwd.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) (* 2 x))) +(check-synth) +