From ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 21 Aug 2018 19:38:40 -0500 Subject: [PATCH] Fix processing of nested Variable construct in sygus let bodies (#2351) --- src/parser/smt2/smt2.cpp | 29 +++++----- test/regress/Makefile.tests | 2 + test/regress/regress1/sygus/abv.sy | 61 +++++++++++++++++++++ test/regress/regress1/sygus/let-bug-simp.sy | 22 ++++++++ 4 files changed, 98 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress1/sygus/abv.sy create mode 100644 test/regress/regress1/sygus/let-bug-simp.sy 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; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index e773bf698..f766396a1 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1513,6 +1513,7 @@ REG1_TESTS = \ regress1/strings/type003.smt2 \ regress1/strings/username_checker_min.smt2 \ regress1/sygus/VC22_a.sy \ + regress1/sygus/abv.sy \ regress1/sygus/array_search_2.sy \ regress1/sygus/array_search_5-Q-easy.sy \ regress1/sygus/array_sum_2_5.sy \ @@ -1546,6 +1547,7 @@ REG1_TESTS = \ regress1/sygus/inv-example.sy \ regress1/sygus/inv-unused.sy \ regress1/sygus/large-const-simp.sy \ + regress1/sygus/let-bug-simp.sy \ regress1/sygus/list-head-x.sy \ regress1/sygus/logiccell_help.sy \ regress1/sygus/max.sy \ diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy new file mode 100644 index 000000000..6ce1a011a --- /dev/null +++ b/test/regress/regress1/sygus/abv.sy @@ -0,0 +1,61 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ABV) + +(define-sort AddrSort () (BitVec 32)) +(define-sort ValSort () (BitVec 8)) +(define-sort MemSort () (Array AddrSort ValSort)) + +; Write the value y to index x +(define-fun WriteArr + ; Args + ((x AddrSort) (y ValSort) (arrIn MemSort)) + + ; Return value + MemSort + + ; Function Body + (store arrIn x y) +) + +; Read from index x +(define-fun ReadArr + ; Args + ((x AddrSort) (arrIn MemSort)) + + ; Return value + ValSort + + ; Function Body + (select arrIn x) +) + + +(synth-fun f + ; Args + ((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort)) + + ; Return value + ValSort + + ; Grammar + ( + (StartArray MemSort ( + (WriteArr (Variable AddrSort) (Variable ValSort) StartArray) + (WriteArr (Variable AddrSort) (Variable ValSort) mem))) + + (Start ValSort ( + (let + ((m MemSort StartArray)) + (bvadd + (ReadArr (Variable AddrSort) m) + (ReadArr (Variable AddrSort) m)))))) +) + +(declare-var a (BitVec 8)) +(declare-var b (BitVec 8)) +(declare-var c (BitVec 32)) +(declare-var d (BitVec 32)) +(declare-var e (Array (BitVec 32) (BitVec 8))) +(constraint (=> (not (= c d)) (= (bvadd a b) (f a b c d e)))) +(check-synth) diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy new file mode 100644 index 000000000..d570d5a21 --- /dev/null +++ b/test/regress/regress1/sygus/let-bug-simp.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun f ((x0 Int) (x1 Int)) Bool +( + (StartInt Int (5)) + + (Start Bool ( + (let + ((z Int StartInt)) + (or + (= (Variable Int) z) + (= (Variable Int) z))))) +) +) + +(declare-var a Int) +(declare-var b Int) +(constraint (=> (= a 5) (f a b))) +(constraint (=> (= b 5) (f a b))) +(check-synth) -- 2.30.2