From bee3c7f6840e531bc91d990b98f2b331d1f2f82c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Sep 2019 16:18:06 -0500 Subject: [PATCH] Fix default grammar construction for arrays when no free variables are present (#3225) --- src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 6 ++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/qf_abv.smt2 | 12 ++++++++++++ 3 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/sygus/qf_abv.smt2 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a6b051e58..e7f447ca1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -385,8 +385,9 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, } else if (type.isArray()) { - // TODO #2694 : generate constant array over the first element of the - // constituent type + // generate constant array over the first element of the constituent type + Node c = type.mkGroundTerm(); + ops.push_back(c); } // TODO #1178 : add other missing types } @@ -1032,6 +1033,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( std::vector types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + Trace("sygus-grammar-def") << "...finished" << std::endl; Assert( types.size()==datatypes.size() ); return TypeNode::fromType( types[0] ); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 56010858d..393e21c84 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1696,6 +1696,7 @@ set(regress_1_tests regress1/sygus/planning-unif.sy regress1/sygus/process-10-vars.sy regress1/sygus/qe.sy + regress1/sygus/qf_abv.smt2 regress1/sygus/real-grammar.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy diff --git a/test/regress/regress1/sygus/qf_abv.smt2 b/test/regress/regress1/sygus/qf_abv.smt2 new file mode 100644 index 000000000..b72af20f7 --- /dev/null +++ b/test/regress/regress1/sygus/qf_abv.smt2 @@ -0,0 +1,12 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-info :smt-lib-version 2.6) +(set-logic QF_ABV) +(set-info :status sat) +(declare-fun mem_35_57_4 () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun R_EBX_6_67_3 () (_ BitVec 32)) +(declare-fun R_EBP_0_60_2 () (_ BitVec 32)) +(declare-fun R_ESP_1_58_1 () (_ BitVec 32)) +(assert (let ((?v_0 (bvsub (bvsub R_ESP_1_58_1 (_ bv4 32)) (_ bv4 32)))) (let ((?v_6 (bvadd (bvadd ?v_0 (_ bv4 32)) (_ bv4 32))) (?v_2 (store (store (store (store mem_35_57_4 (bvadd ?v_0 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60_2 (_ bv24 32)))) (bvadd ?v_0 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60_2 (_ bv16 32)))) (bvadd ?v_0 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60_2 (_ bv8 32)))) (bvadd ?v_0 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_60_2)))) (let ((?v_4 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_2 (_ bv134526656 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134526657 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134526658 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134526659 32))) (_ bv24 32)))) (?v_1 (bvsub (bvsub ?v_0 (_ bv4 32)) (_ bv4 32)))) (let ((?v_3 (store (store (store (store ?v_2 (bvadd ?v_1 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_67_3 (_ bv24 32)))) (bvadd ?v_1 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_67_3 (_ bv16 32)))) (bvadd ?v_1 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_67_3 (_ bv8 32)))) (bvadd ?v_1 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_67_3)))) (let ((?v_7 (concat (_ bv0 24) (select ?v_3 ?v_4)))) (let ((?v_5 (store ?v_3 ?v_4 ((_ extract 7 0) (bvadd ?v_7 (_ bv1 32))))) (?v_8 (concat (_ bv0 24) ((_ extract 7 0) ?v_7)))) (let ((?v_9 (bvand (bvsub ?v_8 (_ bv56 32)) (_ bv255 32)))) (let ((?v_10 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_8 (_ bv56 32)) (bvxor ?v_8 ?v_9)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1)))) (= (_ bv1 1) (bvand (ite (not (= (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv3 32)))) (_ bv24 32))) (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv3 32)))) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)) (bvand ((_ extract 0 0) (concat (_ bv0 31) (bvor (bvxor (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr ?v_9 (_ bv7 32)))) (_ bv1 1) (_ bv0 1)) ?v_10) (ite (= ?v_9 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (bvand (bvnot ?v_10) (_ bv1 1)))))))))))))) +(check-sat) +(exit) -- 2.30.2