Fix default grammar construction for arrays when no free variables are present ...

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index a6b051e58703433dec0e7a60ad8240411881815c..e7f447ca1da19b17de282862dedff2dfd12ffff4 100644 (file)
--- 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<DatatypeType> 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 56010858ddb064574c38d774985271627cd9a3f7..393e21c84fbe9f006ccda7ea1e174ebff3b9046c 100644 (file)
--- 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 (file)
index 0000000..b72af20
--- /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)