From 12bad5f9c981dd1a328dd769176e87e39a041f91 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Aug 2019 13:56:39 -0500 Subject: [PATCH] Support default sygus grammar for strings (#3148) --- .../sygus/ce_guided_single_inv.cpp | 16 ++++++++-- .../quantifiers/sygus/sygus_grammar_cons.cpp | 31 +++++++++++++++++++ test/regress/CMakeLists.txt | 2 ++ .../regress1/sygus/strings-no-syntax.sy | 13 ++++++++ .../regress2/sygus/strings-no-syntax-len.sy | 13 ++++++++ 5 files changed, 72 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/sygus/strings-no-syntax.sy create mode 100644 test/regress/regress2/sygus/strings-no-syntax-len.sy diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 00d040af5..3fbb4eaee 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -363,17 +363,27 @@ void CegSingleInv::finishInit(bool syntaxRestricted) d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end()); Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl; - if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){ + // check whether we can handle this quantified formula + CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv); + if( statuspresolve( d_single_inv ); } - }else{ + } + if( !d_single_invocation ) + { d_single_inv = Node::null(); Trace("cegqi-si") << "Formula is not single invocation." << std::endl; if (options::cegqiSingleInvAbort()) { std::stringstream ss; - ss << "Property is not single invocation." << std::endl; + ss << "Property is not handled by single invocation." << std::endl; throw LogicException(ss.str()); } } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index bcd0d709e..bb8da59da 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -420,6 +420,12 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( collectSygusGrammarTypesFor( TypeNode::fromType(arrayType.getConstituentType()), types); } + else if (range.isString() ) + { + // theory of strings shares the integer type + TypeNode intType = NodeManager::currentNM()->integerType(); + collectSygusGrammarTypesFor(intType,types); + } } } } @@ -670,6 +676,31 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( weights[i].push_back(-1); } } + else if (types[i].isString()) + { + // concatenation + ops[i].push_back(nm->operatorOf(STRING_CONCAT).toExpr()); + cnames[i].push_back(kindToString(STRING_CONCAT)); + cargs[i].push_back(std::vector()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); + // length + TypeNode intType = nm->integerType(); + Assert(std::find(types.begin(),types.end(),intType)!=types.end()); + unsigned i_intType = std::distance( + types.begin(), + std::find(types.begin(), + types.end(), + intType)); + ops[i_intType].push_back(nm->operatorOf(STRING_LENGTH).toExpr()); + cnames[i_intType].push_back(kindToString(STRING_LENGTH)); + cargs[i_intType].push_back(std::vector()); + cargs[i_intType].back().push_back(unres_t); + pcs[i_intType].push_back(nullptr); + weights[i_intType].push_back(-1); + } else if (types[i].isArray()) { ArrayType arrayType = static_cast(types[i].toType()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 99b464d09..19e5fa899 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1696,6 +1696,7 @@ set(regress_1_tests regress1/sygus/real-grammar.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy + regress1/sygus/strings-no-syntax.sy regress1/sygus/strings-concat-3-args.sy regress1/sygus/strings-double-rec.sy regress1/sygus/strings-small.sy @@ -1833,6 +1834,7 @@ set(regress_2_tests regress2/sygus/process-10-vars-2fun.sy regress2/sygus/process-arg-invariance.sy regress2/sygus/real-grammar-neg.sy + regress2/sygus/strings-no-syntax-len.sy regress2/sygus/three.sy regress2/sygus/vcb.sy regress2/typed_v1l50016-simp.cvc diff --git a/test/regress/regress1/sygus/strings-no-syntax.sy b/test/regress/regress1/sygus/strings-no-syntax.sy new file mode 100644 index 000000000..4959d6fe1 --- /dev/null +++ b/test/regress/regress1/sygus/strings-no-syntax.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun f ((x String) (y String)) String) + +(declare-var x String) +(declare-var y String) + +(constraint (>= (str.len (f x y)) (str.len x))) +(constraint (>= (str.len (f x y)) (str.len y))) + +(check-synth) diff --git a/test/regress/regress2/sygus/strings-no-syntax-len.sy b/test/regress/regress2/sygus/strings-no-syntax-len.sy new file mode 100644 index 000000000..22048f1ec --- /dev/null +++ b/test/regress/regress2/sygus/strings-no-syntax-len.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun f ((x String)) Int) + +(declare-var x String) +(constraint (>= (f (str.++ "A" x)) (f x))) +(constraint (= (f "A") 2)) +(constraint (= (f "BB") 4)) +(constraint (= (f "BCB") 6)) + +(check-synth) -- 2.30.2