From: Andrew Reynolds Date: Fri, 15 Jan 2021 21:19:43 +0000 (-0600) Subject: Implement --no-strings-lazy-pp as a preprocessing pass (#5777) X-Git-Tag: cvc5-1.0.0~2377 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=de79f1ad325036ca90be9144a74606310b5dab9b;p=cvc5.git Implement --no-strings-lazy-pp as a preprocessing pass (#5777) This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally. Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6f5647e9a..dd944f929 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -68,6 +68,8 @@ libcvc4_add_sources( preprocessing/passes/bv_to_int.h preprocessing/passes/extended_rewriter_pass.cpp preprocessing/passes/extended_rewriter_pass.h + preprocessing/passes/foreign_theory_rewrite.cpp + preprocessing/passes/foreign_theory_rewrite.h preprocessing/passes/fun_def_fmf.cpp preprocessing/passes/fun_def_fmf.h preprocessing/passes/global_negate.cpp @@ -102,8 +104,8 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h - preprocessing/passes/foreign_theory_rewrite.cpp - preprocessing/passes/foreign_theory_rewrite.h + preprocessing/passes/strings_eager_pp.cpp + preprocessing/passes/strings_eager_pp.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/synth_rew_rules.cpp diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index b4a353862..b8c9498e1 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -31,7 +31,7 @@ Rewrite::Rewrite(PreprocessingPassContext* preprocContext) PreprocessingPassResult Rewrite::applyInternal( AssertionPipeline* assertionsToPreprocess) -{ +{ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i])); } diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp new file mode 100644 index 000000000..69cb8914c --- /dev/null +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -0,0 +1,59 @@ +/********************* */ +/*! \file strings_eager_pp.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The strings eager preprocess utility + **/ + +#include "preprocessing/passes/strings_eager_pp.h" + +#include "theory/strings/theory_strings_preprocess.h" +#include "theory/rewriter.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +StringsEagerPp::StringsEagerPp(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "strings-eager-pp"){}; + +PreprocessingPassResult StringsEagerPp::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + theory::strings::SkolemCache skc(false); + theory::strings::StringsPreprocess pp(&skc); + for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts; + ++i) + { + Node prev = (*assertionsToPreprocess)[i]; + std::vector asserts; + Node rew = pp.processAssertion(prev, asserts); + if (!asserts.empty()) + { + std::vector conj; + conj.push_back(rew); + conj.insert(conj.end(), asserts.begin(), asserts.end()); + rew = nm->mkAnd(conj); + } + if (prev != rew) + { + assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew)); + } + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h new file mode 100644 index 000000000..299260c61 --- /dev/null +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -0,0 +1,45 @@ +/********************* */ +/*! \file strings_eager_pp.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The strings eager preprocess utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H +#define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * Eliminate all extended string functions in the input problem using + * reductions to bounded string quantifiers. + */ +class StringsEagerPp : public PreprocessingPass +{ + public: + StringsEagerPp(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index da09f6363..f14b8b4a7 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -33,6 +33,7 @@ #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/bv_to_int.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#include "preprocessing/passes/foreign_theory_rewrite.h" #include "preprocessing/passes/fun_def_fmf.h" #include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/ho_elim.h" @@ -50,7 +51,7 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" -#include "preprocessing/passes/foreign_theory_rewrite.h" +#include "preprocessing/passes/strings_eager_pp.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/synth_rew_rules.h" #include "preprocessing/passes/theory_preprocess.h" @@ -153,6 +154,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("ho-elim", callCtor); registerPassInfo("fun-def-fmf", callCtor); registerPassInfo("theory-rewrite-eq", callCtor); + registerPassInfo("strings-eager-pp", callCtor); } } // namespace preprocessing diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 6d6c81e3c..0c01abbbb 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -24,6 +24,7 @@ #include "options/quantifiers_options.h" #include "options/sep_options.h" #include "options/smt_options.h" +#include "options/strings_options.h" #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -243,7 +244,10 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["fun-def-fmf"]->apply(&assertions); } } - + if (!options::stringLazyPreproc()) + { + d_passes["strings-eager-pp"]->apply(&assertions); + } if (options::sortInference() || options::ufssFairnessMonotone()) { d_passes["sort-inference"]->apply(&assertions); diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 7e416d132..352da5ac8 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -43,7 +43,7 @@ ExtfSolver::ExtfSolver(SolverState& s, d_csolver(cs), d_extt(et), d_statistics(statistics), - d_preproc(d_termReg.getSkolemCache(), s.getUserContext(), statistics), + d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions), d_hasExtf(s.getSatContext(), false), d_extfInferCache(s.getSatContext()), d_reduced(s.getUserContext()) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3189b297a..eec59685a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1032,31 +1032,6 @@ TrustNode TheoryStrings::ppRewrite(TNode atom) atomRet = ret.getNode(); } } - if( !options::stringLazyPreproc() ){ - //eager preprocess here - std::vector< Node > new_nodes; - StringsPreprocess* p = d_esolver.getPreprocess(); - Node pret = p->processAssertion(atomRet, new_nodes); - if (pret != atomRet) - { - Trace("strings-ppr") << " rewrote " << atomRet << " -> " << pret - << ", with " << new_nodes.size() << " lemmas." - << std::endl; - for (const Node& lem : new_nodes) - { - Trace("strings-ppr") << " lemma : " << lem << std::endl; - ++(d_statistics.d_lemmasEagerPreproc); - d_out->lemma(lem); - } - atomRet = pret; - // Don't support proofs yet, thus we must return nullptr. This is the - // case even if we had proven the elimination via regexp elimination - // above. - ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr); - }else{ - Assert(new_nodes.empty()); - } - } return ret; } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1a46b26f5..f0afe5f26 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -41,9 +41,8 @@ struct QInternalVarAttributeId typedef expr::Attribute QInternalVarAttribute; StringsPreprocess::StringsPreprocess(SkolemCache* sc, - context::UserContext* u, - SequencesStatistics& stats) - : d_sc(sc), d_statistics(stats) + HistogramStat* statReductions) + : d_sc(sc), d_statReductions(statReductions) { } @@ -938,7 +937,10 @@ Node StringsPreprocess::simplify(Node t, std::vector& asserts) Trace("strings-preprocess") << " " << asserts[i] << std::endl; } } - d_statistics.d_reductions << t.getKind(); + if (d_statReductions != nullptr) + { + (*d_statReductions) << t.getKind(); + } } else { @@ -948,12 +950,11 @@ Node StringsPreprocess::simplify(Node t, std::vector& asserts) return retNode; } -Node StringsPreprocess::simplifyRec(Node t, - std::vector& asserts, - std::map& visited) +Node StringsPreprocess::simplifyRec(Node t, std::vector& asserts) { - std::map< Node, Node >::iterator it = visited.find(t); - if( it!=visited.end() ){ + std::map::iterator it = d_visited.find(t); + if (it != d_visited.end()) + { return it->second; }else{ Node retNode = t; @@ -968,7 +969,7 @@ Node StringsPreprocess::simplifyRec(Node t, cc.push_back( t.getOperator() ); } for(unsigned i=0; i& asserts) { - std::map< Node, Node > visited; std::vector asserts_curr; - Node ret = simplifyRec(n, asserts_curr, visited); + Node ret = simplifyRec(n, asserts_curr); while (!asserts_curr.empty()) { Node curr = asserts_curr.back(); asserts_curr.pop_back(); std::vector asserts_tmp; - curr = simplifyRec(curr, asserts_tmp, visited); + curr = simplifyRec(curr, asserts_tmp); asserts_curr.insert( asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end()); asserts.push_back(curr); @@ -1003,38 +1003,6 @@ Node StringsPreprocess::processAssertion(Node n, std::vector& asserts) return ret; } -void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ - std::map< Node, Node > visited; - for( unsigned i=0; i asserts; - std::vector asserts_curr; - asserts_curr.push_back(vec_node[i]); - while (!asserts_curr.empty()) - { - Node curr = asserts_curr.back(); - asserts_curr.pop_back(); - std::vector asserts_tmp; - curr = simplifyRec(curr, asserts_tmp, visited); - asserts_curr.insert( - asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end()); - asserts.push_back(curr); - } - Node res = asserts.size() == 1 - ? asserts[0] - : NodeManager::currentNM()->mkNode(kind::AND, asserts); - if( res!=vec_node[i] ){ - res = Rewriter::rewrite( res ); - if (options::unsatCores() && !options::proofNew()) - { - ProofManager::currentPM()->addDependence(res, vec_node[i]); - } - vec_node[i] = res; - } - } -} - Node StringsPreprocess::mkForallInternal(Node bvl, Node body) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 124a09a4c..b156a5f5e 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -41,8 +41,7 @@ namespace strings { class StringsPreprocess { public: StringsPreprocess(SkolemCache* sc, - context::UserContext* u, - SequencesStatistics& stats); + HistogramStat* statReductions = nullptr); ~StringsPreprocess(); /** The reduce routine * @@ -79,27 +78,20 @@ class StringsPreprocess { * asserts. */ Node processAssertion(Node t, std::vector& asserts); - /** - * Replaces all formulas t in vec_node with an equivalent formula t' that - * contains no free instances of extended functions (that is, extended - * functions may only appear beneath quantifiers). This applies simplifyRec - * on each assertion in vec_node until a fixed point is reached. - */ - void processAssertions(std::vector& vec_node); private: /** pointer to the skolem cache used by this class */ SkolemCache* d_sc; /** Reference to the statistics for the theory of strings/sequences. */ - SequencesStatistics& d_statistics; + HistogramStat* d_statReductions; + /** visited cache */ + std::map d_visited; /** * Applies simplify to all top-level extended function subterms of t. New * assertions created in this reduction are added to asserts. The argument * visited stores a cache of previous results. */ - Node simplifyRec(Node t, - std::vector& asserts, - std::map& visited); + Node simplifyRec(Node t, std::vector& asserts); /** * Make internal quantified formula with bound variable list bvl and body. * Internally, we get a node corresponding to marking a quantified formula as diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a2e070daf..e2af099d7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1101,6 +1101,10 @@ set(regress_0_tests regress0/strings/issue5384-double-conflict.smt2 regress0/strings/issue5428-re-diff-assoc.smt2 regress0/strings/issue5542-strings-seq-mix.smt2 + regress0/strings/issue5608-eager-pp.smt2 + regress0/strings/issue5745-eager-pp.smt2 + regress0/strings/issue5767-eager-pp.smt2 + regress0/strings/issue5771-eager-pp.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 @@ -1988,6 +1992,7 @@ set(regress_1_tests regress1/strings/issue5330.smt2 regress1/strings/issue5330_2.smt2 regress1/strings/issue5374-proxy-i.smt2 + regress1/strings/issue5406-eager-pp.smt2 regress1/strings/issue5483-pp-leq.smt2 regress1/strings/issue5510-re-consume.smt2 regress1/strings/issue5520-re-consume.smt2 diff --git a/test/regress/regress0/strings/issue5608-eager-pp.smt2 b/test/regress/regress0/strings/issue5608-eager-pp.smt2 new file mode 100644 index 000000000..a1a166277 --- /dev/null +++ b/test/regress/regress0/strings/issue5608-eager-pp.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-strings-lazy-pp -i +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_SLIA) +(declare-fun v6 () Bool) +(declare-fun str6 () String) +(assert (and v6 (str.in_re (str.replace str6 (str.from_int 12) str6) (str.to_re str6)))) +(check-sat) +(check-sat) +(assert (not v6)) +(check-sat) diff --git a/test/regress/regress0/strings/issue5745-eager-pp.smt2 b/test/regress/regress0/strings/issue5745-eager-pp.smt2 new file mode 100644 index 000000000..b869a9ded --- /dev/null +++ b/test/regress/regress0/strings/issue5745-eager-pp.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-strings-lazy-pp +; EXPECT: sat +(set-logic ALL) +(declare-fun i0 () Int) +(declare-fun str4 () String) +(assert (= str4 (str.substr str4 (mod i0 2) 1))) +(assert (not (= "" str4))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5767-eager-pp.smt2 b/test/regress/regress0/strings/issue5767-eager-pp.smt2 new file mode 100644 index 000000000..5e4d29d5a --- /dev/null +++ b/test/regress/regress0/strings/issue5767-eager-pp.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-strings-lazy-pp -q +; EXPECT: sat +(set-logic ALL) +(declare-fun s () String) +(assert (xor (= (str.at s (div 0 0)) "A") (= (div 0 (str.len s)) 0))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5771-eager-pp.smt2 b/test/regress/regress0/strings/issue5771-eager-pp.smt2 new file mode 100644 index 000000000..c3049e72f --- /dev/null +++ b/test/regress/regress0/strings/issue5771-eager-pp.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-strings-lazy-pp +; EXPECT: sat +(set-logic ALL) +(declare-fun a () Int) +(assert (str.suffixof "B" (str.from_code a))) +(check-sat) diff --git a/test/regress/regress1/strings/issue5406-eager-pp.smt2 b/test/regress/regress1/strings/issue5406-eager-pp.smt2 new file mode 100644 index 000000000..9ea7310fe --- /dev/null +++ b/test/regress/regress1/strings/issue5406-eager-pp.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --no-strings-lazy-pp -i +; EXPECT: unsat +(set-logic QF_S) +(declare-fun _substvar_18_ () String) +(set-option :strings-lazy-pp false) +(declare-fun str2 () String) +(declare-fun str3 () String) +(declare-fun str9 () String) +(declare-fun str10 () String) +(assert (not (str.prefixof str3 str9))) +(push 1) +(assert (= str3 str2 str10 str9 _substvar_18_)) +(check-sat)