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.
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
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
PreprocessingPassResult Rewrite::applyInternal(
AssertionPipeline* assertionsToPreprocess)
-{
+{
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) {
assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i]));
}
--- /dev/null
+/********************* */
+/*! \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<Node> asserts;
+ Node rew = pp.processAssertion(prev, asserts);
+ if (!asserts.empty())
+ {
+ std::vector<Node> 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
--- /dev/null
+/********************* */
+/*! \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 */
#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"
#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"
registerPassInfo("ho-elim", callCtor<HoElim>);
registerPassInfo("fun-def-fmf", callCtor<FunDefFmf>);
registerPassInfo("theory-rewrite-eq", callCtor<TheoryRewriteEq>);
+ registerPassInfo("strings-eager-pp", callCtor<StringsEagerPp>);
}
} // namespace preprocessing
#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"
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);
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())
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;
}
typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
StringsPreprocess::StringsPreprocess(SkolemCache* sc,
- context::UserContext* u,
- SequencesStatistics& stats)
- : d_sc(sc), d_statistics(stats)
+ HistogramStat<Kind>* statReductions)
+ : d_sc(sc), d_statReductions(statReductions)
{
}
Trace("strings-preprocess") << " " << asserts[i] << std::endl;
}
}
- d_statistics.d_reductions << t.getKind();
+ if (d_statReductions != nullptr)
+ {
+ (*d_statReductions) << t.getKind();
+ }
}
else
{
return retNode;
}
-Node StringsPreprocess::simplifyRec(Node t,
- std::vector<Node>& asserts,
- std::map<Node, Node>& visited)
+Node StringsPreprocess::simplifyRec(Node t, std::vector<Node>& asserts)
{
- std::map< Node, Node >::iterator it = visited.find(t);
- if( it!=visited.end() ){
+ std::map<Node, Node>::iterator it = d_visited.find(t);
+ if (it != d_visited.end())
+ {
return it->second;
}else{
Node retNode = t;
cc.push_back( t.getOperator() );
}
for(unsigned i=0; i<t.getNumChildren(); i++) {
- Node s = simplifyRec(t[i], asserts, visited);
+ Node s = simplifyRec(t[i], asserts);
cc.push_back( s );
if( s!=t[i] ) {
changed = true;
}
retNode = simplify(tmp, asserts);
}
- visited[t] = retNode;
+ d_visited[t] = retNode;
return retNode;
}
}
Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
{
- std::map< Node, Node > visited;
std::vector<Node> 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<Node> 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);
return ret;
}
-void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
- std::map< Node, Node > visited;
- for( unsigned i=0; i<vec_node.size(); i++ ){
- Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl;
- //preprocess until fixed point
- std::vector<Node> asserts;
- std::vector<Node> asserts_curr;
- asserts_curr.push_back(vec_node[i]);
- while (!asserts_curr.empty())
- {
- Node curr = asserts_curr.back();
- asserts_curr.pop_back();
- std::vector<Node> 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();
class StringsPreprocess {
public:
StringsPreprocess(SkolemCache* sc,
- context::UserContext* u,
- SequencesStatistics& stats);
+ HistogramStat<Kind>* statReductions = nullptr);
~StringsPreprocess();
/** The reduce routine
*
* asserts.
*/
Node processAssertion(Node t, std::vector<Node>& 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<Node>& 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<Kind>* d_statReductions;
+ /** visited cache */
+ std::map<Node, Node> 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<Node>& asserts,
- std::map<Node, Node>& visited);
+ Node simplifyRec(Node t, std::vector<Node>& asserts);
/**
* Make internal quantified formula with bound variable list bvl and body.
* Internally, we get a node corresponding to marking a quantified formula as
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
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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff