diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 17 | ||||
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 22 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 35 |
10 files changed, 102 insertions, 32 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index fe6764297..4469f0fe9 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -244,14 +244,21 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; return ret; } - Kind ok = getOperatorKindForSygusBuiltin(op); - if (schildren.size() == 1 && ok == kind::UNDEFINED_KIND) + Kind ok = NodeManager::operatorToKind(op); + if (ok != UNDEFINED_KIND) + { + ret = NodeManager::currentNM()->mkNode(ok, schildren); + Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; + return ret; + } + Kind tok = getOperatorKindForSygusBuiltin(op); + if (schildren.size() == 1 && tok == kind::UNDEFINED_KIND) { ret = schildren[0]; } else { - ret = NodeManager::currentNM()->mkNode(ok, schildren); + ret = NodeManager::currentNM()->mkNode(tok, schildren); } Trace("dt-sygus-util") << "...return " << ret << std::endl; return ret; diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 908bef92c..2d2e9ce30 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -276,11 +276,7 @@ CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) { - ExtendedRewriter* er = nullptr; - if (options::synthRrPrepExtRew()) - { - er = &d_ext_rewrite; - } + ExtendedRewriter* er = &d_ext_rewrite; Node nr; if (er == nullptr) { diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 0e8542826..67aa8688c 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -77,7 +77,8 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, // check is ground. Node squery = convertToSkolem(query); NodeManager* nm = NodeManager::currentNM(); - if (options::sygusExprMinerCheckTimeout.wasSetByUser()) + if (options::sygusExprMinerCheckTimeout.wasSetByUser() + || options::sygusRewSynthInput()) { // To support a separate timeout for the subsolver, we need to create // a separate ExprManager with its own options. This requires that @@ -89,6 +90,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, checker.reset(new SmtEngine(&em)); checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); + checker->setOption("sygus-rr-synth-input", false); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); } @@ -96,8 +98,9 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, { std::stringstream msg; msg << "Unable to export " << squery - << " but exporting expressions is required for " - "--sygus-rr-synth-check-timeout."; + << " but exporting expressions is " + "required for an expression " + "miner check."; throw OptionException(msg.str()); } needExport = true; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 2e7f0cc02..06f041d93 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -198,6 +198,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, Node lem = nm->mkNode( OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])); lems.push_back(lem); + addedEvalLemmas = true; Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index f9c10e33e..972d07af7 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -95,8 +95,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf * registerEvalPtAtSize on the output channel of d_qe. */ void registerEvalPts(const std::vector<Node>& eis, Node e); - /** Retrieves active guard for enumerator */ - Node getActiveGuardForEnumerator(Node e); private: /** reference to quantifier engine */ @@ -109,9 +107,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf bool d_initialized; /** null node */ Node d_null; - /** map from condition enumerators to active guards (in case they are - * enumerated indepedently of the return values) */ - std::map<Node, Node> d_enum_to_active_guard; /** information per initialized type */ class StrategyPtInfo { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index eadbf766a..47c701cf6 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -126,21 +126,18 @@ Node CegGrammarConstructor::process(Node q, preGrammarType = preGrammarType.getRangeType(); } } - Node sfvl = getSygusVarList(sf); - // sfvl may be null for constant synthesis functions - Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl; // the actual sygus datatype we will use (normalized below) TypeNode tn; std::stringstream ss; ss << sf; - if (preGrammarType.isDatatype() - && static_cast<DatatypeType>(preGrammarType.toType()) - .getDatatype() - .isSygus()) + Node sfvl; + if (preGrammarType.isDatatype() && preGrammarType.getDatatype().isSygus()) { + sfvl = Node::fromExpr(preGrammarType.getDatatype().getSygusVarList()); tn = preGrammarType; }else{ + sfvl = getSygusVarList(sf); // check which arguments are irrelevant std::unordered_set<unsigned> arg_irrelevant; d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant); @@ -156,6 +153,9 @@ Node CegGrammarConstructor::process(Node q, tn = mkSygusDefaultType( preGrammarType, sfvl, ss.str(), extra_cons, exc_cons, term_irlv); } + // sfvl may be null for constant synthesis functions + Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " + << sfvl << std::endl; // normalize type SygusGrammarNorm sygus_norm(d_qe); @@ -367,6 +367,10 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, ops.push_back(nm->mkConst(true)); ops.push_back(nm->mkConst(false)); } + else if (type.isString()) + { + ops.push_back(nm->mkConst(String(""))); + } // TODO #1178 : add other missing types } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 022031bef..0c5b67656 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -108,6 +108,12 @@ public: * functions-to-synthesize of sygus conjecture q. */ static bool hasSyntaxRestrictions(Node q); + /** + * Make the builtin constants for type "type" that should be included in a + * sygus grammar, add them to vector ops. + */ + static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops); + private: /** reference to quantifier engine */ QuantifiersEngine * d_qe; @@ -124,8 +130,6 @@ public: //---------------- grammar construction // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres); - // make the builtin constants for type type that should be included in a sygus grammar - static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops); // collect the list of types that depend on type range static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); /** helper function for function mkSygusDefaultType diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index b014a30c6..b5dea4c38 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -158,12 +158,21 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm, Node sygus_op = Node::fromExpr(cons.getSygusOp()); Trace("sygus-grammar-normalize-debug") << ".....operator is " << sygus_op << std::endl; - Node exp_sop_n = Node::fromExpr( - smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr())); + Node exp_sop_n = sygus_op; + // Only expand definitions if the operator is not constant, since calling + // expandDefinitions on them should be a no-op. This check ensures we don't + // try to expand e.g. bitvector extract operators, whose type is undefined, + // and thus should not be passed to expandDefinitions. + if (!sygus_op.isConst()) + { + exp_sop_n = Node::fromExpr( + smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr())); + } + // get the kind for the operator. + Kind ok = NodeManager::operatorToKind(exp_sop_n); // if it is a builtin operator, convert to total version if necessary - if (exp_sop_n.getKind() == kind::BUILTIN) + if (ok != UNDEFINED_KIND) { - Kind ok = NodeManager::operatorToKind(sygus_op); Kind nk = getEliminateKind(ok); if (nk != ok) { diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 8ea26fca9..0310e4620 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -104,18 +104,21 @@ Node RegExpElimination::eliminateConcat(Node atom) // prev_end stores the current (symbolic) index in x that we are // searching. Node prev_end = d_zero; + // the symbolic index we start searching, for each child in sep_children. + std::vector<Node> prev_ends; unsigned gap_minsize_end = gap_minsize.back(); bool gap_exact_end = gap_exact.back(); std::vector<Node> non_greedy_find_vars; for (unsigned i = 0, size = sep_children.size(); i < size; i++) { - Node sc = sep_children[i]; if (gap_minsize[i] > 0) { // the gap to this child is at least gap_minsize[i] prev_end = nm->mkNode(PLUS, prev_end, nm->mkConst(Rational(gap_minsize[i]))); } + prev_ends.push_back(prev_end); + Node sc = sep_children[i]; Node lensc = nm->mkNode(STRING_LENGTH, sc); if (gap_exact[i]) { @@ -169,7 +172,6 @@ Node RegExpElimination::eliminateConcat(Node atom) Node lenSc = nm->mkNode(STRING_LENGTH, sc); Node loc = nm->mkNode(MINUS, lenx, nm->mkNode(PLUS, lenSc, cEnd)); Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc)); - conj.push_back(scc); // We also must ensure that we fit. This constraint is necessary in // addition to the constraint above. Take this example: // x in (re.++ "A" _ (re.* _) "B" _) ---> @@ -182,9 +184,23 @@ Node RegExpElimination::eliminateConcat(Node atom) // would have been the case than "ABB" would be a model for x, where // the second constraint refers to the third position, and the third // constraint refers to the second position. + // + // With respect to the above example, the following is an optimization. + // For that example, we instead produce: + // x in (re.++ "A" _ (re.* _) "B" _) ---> + // substr( x, 0, 1 ) = "A" ^ // find "A" + // substr( x, len(x)-2, 1 ) = "B" ^ // "B" is at end - 2 + // 2 <= len( x ) - 2 + // The intuition is that above, there are two constraints that insist + // that "B" is found, whereas we only need one. The last constraint + // above says that the "B" we find at end-2 can be found >=1 after + // the "A". + conj.pop_back(); Node fit = nm->mkNode(gap_exact[sep_children.size() - 1] ? EQUAL : LEQ, - nm->mkNode(MINUS, prev_end, lenSc), + prev_ends.back(), loc); + + conj.push_back(scc); conj.push_back(fit); } else if (gap_minsize_end > 0) diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b2778298a..00a711a31 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1610,6 +1610,33 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-len-non-pos"); } + if (node[0].getKind() == STRING_SUBSTR) + { + // (str.substr (str.substr x a b) c d) ---> "" if c >= b + // + // Note that this rewrite can be generalized to: + // + // (str.substr x a b) ---> "" if a >= (str.len x) + // + // This can be done when we generalize our entailment methods to + // accept an optional context. Then we could conjecture that + // (str.substr x a b) rewrites to "" and do a case analysis: + // + // - a < 0 or b < 0 (the result is trivially empty in these cases) + // - a >= (str.len x) assuming that { a >= 0, b >= 0 } + // + // For example, for (str.substr (str.substr x a a) a a), we could + // then deduce that under those assumptions, "a" is an + // over-approximation of the length of (str.substr x a a), which + // then allows us to reason that the result of the whole term must + // be empty. + if (checkEntailArith(node[1], node[0][2])) + { + Node ret = nm->mkConst(::CVC4::String("")); + return returnRewrite(node, ret, "ss-start-geq-len"); + } + } + std::vector<Node> n1; getConcat(node[0], n1); @@ -1673,6 +1700,14 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) Node ret = nm->mkConst(::CVC4::String("")); return returnRewrite(node, ret, "ss-start-entails-zero-len"); } + + // (str.substr s x x) ---> "" if (str.len s) <= 1 + Node one = nm->mkConst(CVC4::Rational(1)); + if (node[1] == node[2] && checkEntailArith(one, tot_len)) + { + Node ret = nm->mkConst(::CVC4::String("")); + return returnRewrite(node, ret, "ss-len-one-z-z"); + } } if (!curr.isNull()) { |