diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-15 15:19:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-15 15:19:43 -0600 |
commit | de79f1ad325036ca90be9144a74606310b5dab9b (patch) | |
tree | ff025f0ccc846073327b1ad823eb9d255f4a8843 /src/theory | |
parent | eb6155c5f078a26b7cdddddad6e209fad0f825f8 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 25 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 60 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 18 |
4 files changed, 20 insertions, 85 deletions
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<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) { } @@ -938,7 +937,10 @@ Node StringsPreprocess::simplify(Node t, std::vector<Node>& 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<Node>& asserts) 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; @@ -968,7 +969,7 @@ Node StringsPreprocess::simplifyRec(Node 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; @@ -980,22 +981,21 @@ Node StringsPreprocess::simplifyRec(Node t, } 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); @@ -1003,38 +1003,6 @@ Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts) 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(); 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<Kind>* statReductions = nullptr); ~StringsPreprocess(); /** The reduce routine * @@ -79,27 +78,20 @@ class StringsPreprocess { * 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 |