diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 02:34:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-15 02:34:33 -0500 |
commit | 3f3a0445fe772360d8a2da3069a5f082c031d7f8 (patch) | |
tree | bf78f4bbe23ca8f88cf23aca0f31e0594765799f /src/theory/quantifiers/sygus | |
parent | c808605ef15eb79f9ddc2d1a2b4f6dd052530877 (diff) |
Convert more cases of strings to words (#4206)
Diffstat (limited to 'src/theory/quantifiers/sygus')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 58 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.h | 12 |
4 files changed, 41 insertions, 39 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index fdc8120ff..dfbbdfebf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -97,8 +97,8 @@ Node SygusUnif::constructBestConditional(Node ce, Node SygusUnif::constructBestStringToConcat( const std::vector<Node>& strs, - const std::map<Node, unsigned>& total_inc, - const std::map<Node, std::vector<unsigned>>& incr) + const std::map<Node, size_t>& total_inc, + const std::map<Node, std::vector<size_t>>& incr) { Assert(!strs.empty()); std::vector<Node> strs_tmp = strs; @@ -106,7 +106,7 @@ Node SygusUnif::constructBestStringToConcat( // prefer one that has incremented by more than 0 for (const Node& ns : strs_tmp) { - const std::map<Node, unsigned>::const_iterator iti = total_inc.find(ns); + const std::map<Node, size_t>::const_iterator iti = total_inc.find(ns); if (iti != total_inc.end() && iti->second > 0) { return ns; diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 185a927df..f6e85abcd 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -182,8 +182,8 @@ class SygusUnif */ virtual Node constructBestStringToConcat( const std::vector<Node>& strs, - const std::map<Node, unsigned>& total_inc, - const std::map<Node, std::vector<unsigned> >& incr); + const std::map<Node, size_t>& total_inc, + const std::map<Node, std::vector<size_t>>& incr); //------------------------------ end constructing solutions /** map terms to their sygus size */ std::map<Node, unsigned> d_termToSize; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index dc21107b1..1fc7903fa 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/strings/word.h" #include "util/random.h" #include <math.h> @@ -65,7 +66,7 @@ bool UnifContextIo::updateContext(SygusUnifIo* sui, } bool UnifContextIo::updateStringPosition(SygusUnifIo* sui, - std::vector<unsigned>& pos, + std::vector<size_t>& pos, NodeRole nrole) { Assert(pos.size() == d_str_pos.size()); @@ -106,7 +107,7 @@ void UnifContextIo::initialize(SygusUnifIo* sui) // output type of the examples TypeNode exotn = sui->d_examples_out[0].getType(); - if (exotn.isString()) + if (exotn.isStringLike()) { for (unsigned i = 0; i < sz; i++) { @@ -119,10 +120,10 @@ void UnifContextIo::initialize(SygusUnifIo* sui) void UnifContextIo::getCurrentStrings(SygusUnifIo* sui, const std::vector<Node>& vals, - std::vector<String>& ex_vals) + std::vector<Node>& ex_vals) { bool isPrefix = d_curr_role == role_string_prefix; - String dummy; + Node dummy; for (unsigned i = 0; i < vals.size(); i++) { if (d_vals[i] == sui->d_true) @@ -132,14 +133,16 @@ void UnifContextIo::getCurrentStrings(SygusUnifIo* sui, if (pos_value > 0) { Assert(d_curr_role != role_invalid); - String s = vals[i].getConst<String>(); - Assert(pos_value <= s.size()); - ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value) - : s.prefix(s.size() - pos_value)); + Node s = vals[i]; + size_t sSize = strings::Word::getLength(s); + Assert(pos_value <= sSize); + ex_vals.push_back(isPrefix + ? strings::Word::suffix(s, sSize - pos_value) + : strings::Word::prefix(s, sSize - pos_value)); } else { - ex_vals.push_back(vals[i].getConst<String>()); + ex_vals.push_back(vals[i]); } } else @@ -152,14 +155,14 @@ void UnifContextIo::getCurrentStrings(SygusUnifIo* sui, bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, bool isPrefix, - const std::vector<String>& ex_vals, + const std::vector<Node>& ex_vals, const std::vector<Node>& vals, - std::vector<unsigned>& inc, - unsigned& tot) + std::vector<size_t>& inc, + size_t& tot) { for (unsigned j = 0; j < vals.size(); j++) { - unsigned ival = 0; + size_t ival = 0; if (d_vals[j] == sui->d_true) { // example is active in this context @@ -169,12 +172,12 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, // position return false; } - String mystr = vals[j].getConst<String>(); - ival = mystr.size(); - if (mystr.size() <= ex_vals[j].size()) + ival = strings::Word::getLength(vals[j]); + size_t exjLen = strings::Word::getLength(ex_vals[j]); + if (ival <= exjLen) { - if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival) - : ex_vals[j].rstrncmp(mystr, ival))) + if (!(isPrefix ? strings::Word::strncmp(ex_vals[j], vals[j], ival) + : strings::Word::rstrncmp(ex_vals[j], vals[j], ival))) { Trace("sygus-sui-dt-debug") << "X"; return false; @@ -198,7 +201,7 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, return true; } bool UnifContextIo::isStringSolved(SygusUnifIo* sui, - const std::vector<String>& ex_vals, + const std::vector<Node>& ex_vals, const std::vector<Node>& vals) { for (unsigned j = 0; j < vals.size(); j++) @@ -211,8 +214,7 @@ bool UnifContextIo::isStringSolved(SygusUnifIo* sui, // value is unknown, thus it does not solve return false; } - String mystr = vals[j].getConst<String>(); - if (ex_vals[j] != mystr) + if (ex_vals[j] != vals[j]) { return false; } @@ -889,7 +891,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas) bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) { TypeNode xbt = d_tds->sygusToBuiltinType(e.getType()); - if (xbt.isString()) + if (xbt.isStringLike()) { std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e); if (itx != d_use_str_contains_eexc.end()) @@ -1091,7 +1093,7 @@ Node SygusUnifIo::constructSol( } if (ret_dt.isNull()) { - if (d_tds->sygusToBuiltinType(e.getType()).isString()) + if (d_tds->sygusToBuiltinType(e.getType()).isStringLike()) { // check if a current value that closes all examples // get the term enumerator for this type @@ -1103,7 +1105,7 @@ Node SygusUnifIo::constructSol( EnumCache& ecachet = d_ecache[et]; // get the current examples - std::vector<String> ex_vals; + std::vector<Node> ex_vals; x.getCurrentStrings(this, d_examples_out, ex_vals); Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); @@ -1213,12 +1215,12 @@ Node SygusUnifIo::constructSol( // check if each return value is a prefix/suffix of all open examples if (!retValMod || x.getCurrentRole() == nrole) { - std::map<Node, std::vector<unsigned> > incr; + std::map<Node, std::vector<size_t>> incr; bool isPrefix = nrole == role_string_prefix; - std::map<Node, unsigned> total_inc; + std::map<Node, size_t> total_inc; std::vector<Node> inc_strs; // make the value of the examples - std::vector<String> ex_vals; + std::vector<Node> ex_vals; x.getCurrentStrings(this, d_examples_out, ex_vals); if (Trace.isOn("sygus-sui-dt-debug")) { @@ -1244,7 +1246,7 @@ Node SygusUnifIo::constructSol( TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t); Trace("sygus-sui-dt-debug") << " : "; Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size()); - unsigned tot = 0; + size_t tot = 0; bool exsuccess = x.getStringIncrement(this, isPrefix, ex_vals, diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index da08044bf..06197ce66 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -83,7 +83,7 @@ class UnifContextIo : public UnifContext * role to nrole. */ bool updateStringPosition(SygusUnifIo* sui, - std::vector<unsigned>& pos, + std::vector<size_t>& pos, NodeRole nrole); /** get current strings * @@ -94,7 +94,7 @@ class UnifContextIo : public UnifContext */ void getCurrentStrings(SygusUnifIo* sui, const std::vector<Node>& vals, - std::vector<String>& ex_vals); + std::vector<Node>& ex_vals); /** get string increment * * If this method returns true, then inc and tot are updated such that @@ -107,13 +107,13 @@ class UnifContextIo : public UnifContext */ bool getStringIncrement(SygusUnifIo* sui, bool isPrefix, - const std::vector<String>& ex_vals, + const std::vector<Node>& ex_vals, const std::vector<Node>& vals, - std::vector<unsigned>& inc, - unsigned& tot); + std::vector<size_t>& inc, + size_t& tot); /** returns true if ex_vals[i] = vals[i] for all active indices i. */ bool isStringSolved(SygusUnifIo* sui, - const std::vector<String>& ex_vals, + const std::vector<Node>& ex_vals, const std::vector<Node>& vals); //----------end for CONCAT strategies |