diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-21 19:38:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-21 19:38:40 -0500 |
commit | ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 (patch) | |
tree | b241f69ddf7715eb1bfe0753e59ed02a12507da3 /src/parser/smt2/smt2.cpp | |
parent | 5b655946e1c73f511719d0264f92715b063e867f (diff) |
Fix processing of nested Variable construct in sygus let bodies (#2351)
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 778766a61..dfeaca62b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -676,7 +676,10 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, CVC4::Type& ret, bool isNested ){ if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){ - Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl; + Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index + << ", isLet = " + << (sgt.d_gterm_type == SygusGTerm::gterm_let) + << std::endl; Kind oldKind; Kind newKind = kind::UNDEFINED_KIND; //convert to UMINUS if one child of MINUS @@ -684,17 +687,6 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, oldKind = kind::MINUS; newKind = kind::UMINUS; } - /* - //convert to IFF if boolean EQUAL - if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){ - Type ctn = sgt.d_children[0].d_type; - std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn ); - if( it != sygus_to_builtin.end() && it->second.isBoolean() ){ - oldKind = kind::EQUAL; - newKind = kind::IFF; - } - } - */ if( newKind!=kind::UNDEFINED_KIND ){ Expr newExpr = getExprManager()->operatorOf(newKind); Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl; @@ -842,10 +834,15 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){ curr_t = sop.getType(); Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl; - sygus_to_builtin_expr[t] = sop; - //store that term sop has dedicated sygus type t - if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){ - d_sygus_bound_var_type[sop] = t; + // only cache if it is a singleton datatype (has unique expr) + if (ops[sub_dt_index].size() == 1) + { + sygus_to_builtin_expr[t] = sop; + // store that term sop has dedicated sygus type t + if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end()) + { + d_sygus_bound_var_type[sop] = t; + } } }else{ std::vector< Expr > children; |