diff options
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 15 | ||||
| -rw-r--r-- | src/theory/strings/base_solver.cpp | 2 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 54 |
3 files changed, 60 insertions, 11 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 06464af60..b5a8472e6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -271,17 +271,18 @@ void Smt2Printer::toStream(std::ostream& out, toStreamType(out, n.getType()); out << ")"; } - if (snvec.size() > 1) + else if (snvec.size() > 1) { out << "(seq.++"; + for (const Node& snvc : snvec) + { + out << " (seq.unit " << snvc << ")"; + } + out << ")"; } - for (const Node& snvc : snvec) - { - out << " (seq.unit " << snvc << ")"; - } - if (snvec.size() > 1) + else { - out << ")"; + out << "(seq.unit " << snvec[0] << ")"; } break; } diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 00491128a..b25f8f021 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -540,7 +540,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, { Assert(tn.isSequence()); TypeNode etn = tn.getSequenceElementType(); - if (d_state.isFiniteType(etn)) + if (!d_state.isFiniteType(etn)) { // infinite cardinality, we are fine return; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8de43fd55..8912bad3b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -15,7 +15,10 @@ #include "theory/strings/theory_strings.h" +#include "expr/attribute.h" +#include "expr/bound_var_manager.h" #include "expr/kind.h" +#include "expr/sequence.h" #include "options/smt_options.h" #include "options/strings_options.h" #include "options/theory_options.h" @@ -37,6 +40,16 @@ namespace cvc5 { namespace theory { namespace strings { +/** + * Attribute used for making unique (bound variables) which correspond to + * unique element values used in sequence models. See use in collectModelValues + * below. + */ +struct SeqModelVarAttributeId +{ +}; +using SeqModelVarAttribute = expr::Attribute<SeqModelVarAttributeId, Node>; + TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, @@ -355,10 +368,13 @@ bool TheoryStrings::collectModelInfoType( } else { - // otherwise, it is a shared term - argVal = d_valuation.getModelValue(nfe.d_nf[0][0]); + // Otherwise, we use the term itself. We cannot get the model + // value of this term, since it might not be available yet, as + // it may belong to a theory that has not built its model yet. + // Hence, we assign a (non-constant) skeleton (seq.unit argVal). + argVal = nfe.d_nf[0][0]; } - Assert(!argVal.isNull()); + Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal)); pure_eq_assign[eqc] = c; Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") "; @@ -483,6 +499,38 @@ bool TheoryStrings::collectModelInfoType( return false; } c = sel->getCurrent(); + // if we are a sequence with infinite element type + if (tn.isSequence() + && !d_state.isFiniteType(tn.getSequenceElementType())) + { + // Make a skeleton instead. In particular, this means that + // a value: + // (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2)) + // becomes: + // (seq.++ (seq.unit k_0) (seq.unit k_1) (seq.unit k_2)) + // where k_0, k_1, k_2 are fresh integer variables. These + // variables will be assigned values in the standard way by the + // model. This construction is necessary since the strings solver + // must constrain the length of the model of an equivalence class + // (e.g. in this case to length 3); moreover we cannot assign a + // concrete value since it may conflict with other skeletons we + // have assigned, e.g. for the case of (seq.unit argVal) above. + SkolemManager* sm = nm->getSkolemManager(); + BoundVarManager* bvm = nm->getBoundVarManager(); + Assert(c.getKind() == CONST_SEQUENCE); + const Sequence& sn = c.getConst<Sequence>(); + const std::vector<Node>& snvec = sn.getVec(); + std::vector<Node> skChildren; + for (const Node& snv : snvec) + { + TypeNode etn = snv.getType(); + Node v = bvm->mkBoundVar<SeqModelVarAttribute>(snv, etn); + // use a skolem, not a bound variable + Node kv = sm->mkPurifySkolem(v, "smv"); + skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); + } + c = utils::mkConcat(skChildren, tn); + } // increment sel->increment(); } while (m->hasTerm(c)); |