From 3614f1c4b8a439ebf785894fa33640fd015aaefa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 5 Mar 2022 13:43:43 -0600 Subject: [PATCH] Make seq.unit robust wrt subtyping (#8209) Fixes cvc5/cvc5-projects#384. Fixes cvc5/cvc5-projects#426. Fixes cvc5/cvc5-projects#427. Fixes cvc5/cvc5-projects#429. Issue cvc5/cvc5-projects#423 still remains, to be addressed in a followup PR. Also fixes issues with subtyping in how sequence constants are printed. Note this solution is required since we are not ready to eliminate arithmetic subtyping in the short term. These changes will be unnecessary when this happens. --- src/CMakeLists.txt | 2 + src/api/cpp/cvc5.cpp | 7 +++ src/expr/node_manager_template.cpp | 12 ++++ src/expr/node_manager_template.h | 9 +++ src/printer/smt2/smt2_printer.cpp | 24 ++++++- .../quantifiers/sygus/sygus_grammar_cons.cpp | 7 ++- src/theory/rewriter.cpp | 5 +- src/theory/sets/singleton_op.cpp | 2 +- src/theory/sets/singleton_op.h | 8 +-- src/theory/sets/theory_sets_type_rules.cpp | 2 +- src/theory/strings/array_core_solver.cpp | 3 +- src/theory/strings/base_solver.cpp | 2 +- src/theory/strings/core_solver.cpp | 2 +- src/theory/strings/eager_solver.cpp | 3 +- src/theory/strings/extf_solver.cpp | 5 ++ src/theory/strings/kinds | 11 +++- src/theory/strings/seq_unit_op.cpp | 50 +++++++++++++++ src/theory/strings/seq_unit_op.h | 63 +++++++++++++++++++ src/theory/strings/sequences_rewriter.cpp | 4 +- src/theory/strings/theory_strings.cpp | 13 ++-- .../strings/theory_strings_preprocess.cpp | 2 +- .../strings/theory_strings_type_rules.cpp | 21 ++++++- src/theory/theory_model.cpp | 1 + test/regress/CMakeLists.txt | 6 ++ .../seq/proj-issue384-2-subtypes.smt2 | 6 ++ .../regress0/seq/proj-issue384-subtypes.smt2 | 7 +++ .../seq/proj-issue427-subtypes-value.smt2 | 9 +++ .../regress0/seq/query0-subtype-skel.smt2 | 7 +++ test/regress/regress0/seq/query1-subtype.smt2 | 11 ++++ test/regress/regress0/seq/query2-subtype.smt2 | 11 ++++ test/unit/api/cpp/solver_black.cpp | 34 ++++++++++ test/unit/theory/sequences_rewriter_white.cpp | 20 +++--- 32 files changed, 335 insertions(+), 34 deletions(-) create mode 100644 src/theory/strings/seq_unit_op.cpp create mode 100644 src/theory/strings/seq_unit_op.h create mode 100644 test/regress/regress0/seq/proj-issue384-2-subtypes.smt2 create mode 100644 test/regress/regress0/seq/proj-issue384-subtypes.smt2 create mode 100644 test/regress/regress0/seq/proj-issue427-subtypes-value.smt2 create mode 100644 test/regress/regress0/seq/query0-subtype-skel.smt2 create mode 100644 test/regress/regress0/seq/query1-subtype.smt2 create mode 100644 test/regress/regress0/seq/query2-subtype.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 94c077ced..7becedad4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1077,6 +1077,8 @@ libcvc5_add_sources( theory/strings/regexp_solver.h theory/strings/rewrites.cpp theory/strings/rewrites.h + theory/strings/seq_unit_op.cpp + theory/strings/seq_unit_op.h theory/strings/sequences_rewriter.cpp theory/strings/sequences_rewriter.h theory/strings/sequences_stats.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 5ffb23e9d..2cfc262c2 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5264,6 +5264,13 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const res = getNodeManager()->mkBag( type, *children[0].d_node, *children[1].d_node); } + else if (kind == api::SEQ_UNIT) + { + // the type of the term is the same as the type of the internal node + // see Term::getSort() + TypeNode type = children[0].d_node->getType(); + res = getNodeManager()->mkSeqUnit(type, *children[0].d_node); + } else { res = d_nodeMgr->mkNode(k, echildren); diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index c62b1af5e..95fbf3c0f 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -32,6 +32,7 @@ #include "expr/type_properties.h" #include "theory/bags/bag_make_op.h" #include "theory/sets/singleton_op.h" +#include "theory/strings/seq_unit_op.h" #include "util/bitvector.h" #include "util/poly_util.h" #include "util/rational.h" @@ -1102,6 +1103,17 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) } } +Node NodeManager::mkSeqUnit(const TypeNode& t, const TNode n) +{ + Assert(n.getType().isSubtypeOf(t)) + << "Invalid operands for mkSeqUnit. The type '" << n.getType() + << "' of node '" << n << "' is not a subtype of '" << t << "'." + << std::endl; + Node op = mkConst(SeqUnitOp(t)); + Node sunit = mkNode(kind::SEQ_UNIT, op, n); + return sunit; +} + Node NodeManager::mkSingleton(const TypeNode& t, const TNode n) { Assert(n.getType().isSubtypeOf(t)) diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index f992b3910..94e746410 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -692,6 +692,15 @@ class NodeManager /** make unique (per Type,Kind) variable. */ Node mkNullaryOperator(const TypeNode& type, Kind k); + /** + * Create a sequence unit from the given element n. + * @param t the element type of the returned sequence. + * Note that the type of n needs to be a subtype of t. + * @param n the single element in the sequence. + * @return a sequence unit constructed from the element n. + */ + Node mkSeqUnit(const TypeNode& t, const TNode n); + /** * Create a singleton set from the given element n. * @param t the element type of the returned set. diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 80bf2b601..535b96d5f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -266,10 +266,12 @@ void Smt2Printer::toStream(std::ostream& out, { const Sequence& sn = n.getConst(); const std::vector& snvec = sn.getVec(); + TypeNode type = n.getType(); + TypeNode elemType = type.getSequenceElementType(); if (snvec.empty()) { out << "(as seq.empty "; - toStreamType(out, n.getType()); + toStreamType(out, type); out << ")"; } else if (snvec.size() > 1) @@ -277,13 +279,17 @@ void Smt2Printer::toStream(std::ostream& out, out << "(seq.++"; for (const Node& snvc : snvec) { - out << " (seq.unit " << snvc << ")"; + out << " (seq.unit "; + toStreamCastToType(out, snvc, toDepth, elemType); + out << ")"; } out << ")"; } else { - out << "(seq.unit " << snvec[0] << ")"; + out << "(seq.unit "; + toStreamCastToType(out, snvec[0], toDepth, elemType); + out << ")"; } break; } @@ -711,6 +717,18 @@ void Smt2Printer::toStream(std::ostream& out, stillNeedToPrintParams = false; break; + // strings + case kind::SEQ_UNIT: + { + out << smtKindString(k, d_variant) << " "; + TypeNode elemType = n.getType().getSequenceElementType(); + toStreamCastToType( + out, n[0], toDepth < 0 ? toDepth : toDepth - 1, elemType); + out << ")"; + return; + } + break; + // sets case kind::SET_SINGLETON: { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1eb722372..983ab6c60 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -938,7 +938,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for seq.unit" << std::endl; std::vector cargsSeqUnit; cargsSeqUnit.push_back(unresElemType); - sdts[i].addConstructor(SEQ_UNIT, cargsSeqUnit); + // lambda x . (seq.unit (seq_unit_op T) x) where T = x.getType() + Node x = nm->mkBoundVar(etype); + Node vars = nm->mkNode(BOUND_VAR_LIST, x); + Node seqUnit = nm->mkSeqUnit(etype, x); + Node lambda = nm->mkNode(LAMBDA, vars, seqUnit); + sdts[i].addConstructor(lambda, "seq.unit", cargsSeqUnit); } } else if (types[i].isArray()) diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 0ed442252..b8d095321 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -331,7 +331,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, #ifdef CVC5_ASSERTIONS RewriteResponse r2 = d_theoryRewriters[newTheoryId]->postRewrite(newNode); - Assert(r2.d_node == newNode) << r2.d_node << " != " << newNode; + Assert(r2.d_node == newNode) + << "Non-idempotent rewriting: " << r2.d_node << " != " << newNode; #endif rewriteStackTop.d_node = newNode; break; @@ -395,6 +396,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, if (rewriteStack.size() == 1) { Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL || rewriteStackTop.d_node.isConst()); + Assert(rewriteStackTop.d_node.getType().isSubtypeOf(node.getType())) + << "Rewriting " << node << " does not preserve type"; return rewriteStackTop.d_node; } diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp index 327df6984..3ad56f2db 100644 --- a/src/theory/sets/singleton_op.cpp +++ b/src/theory/sets/singleton_op.cpp @@ -13,7 +13,7 @@ * A class for singleton operator for sets. */ -#include "singleton_op.h" +#include "theory/sets/singleton_op.h" #include diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h index cde4709d9..05b26d909 100644 --- a/src/theory/sets/singleton_op.h +++ b/src/theory/sets/singleton_op.h @@ -15,8 +15,8 @@ #include "cvc5_public.h" -#ifndef CVC5__SINGLETON_OP_H -#define CVC5__SINGLETON_OP_H +#ifndef CVC5__THEORY__SETS__SINGLETON_OP_H +#define CVC5__THEORY__SETS__SINGLETON_OP_H #include @@ -51,7 +51,7 @@ class SetSingletonOp std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op); /** - * Hash function for the SingletonHashFunction objects. + * Hash function for the SetSingletonOp objects. */ struct SetSingletonOpHashFunction { @@ -60,4 +60,4 @@ struct SetSingletonOpHashFunction } // namespace cvc5 -#endif /* CVC5__SINGLETON_OP_H */ +#endif /* CVC5__THEORY__SETS__SINGLETON_OP_H */ diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index a8a79d5f9..4fd580b24 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -124,7 +124,7 @@ TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager, Assert(n.getKind() == kind::SET_SINGLETON && n.hasOperator() && n.getOperator().getKind() == kind::SET_SINGLETON_OP); - SetSingletonOp op = n.getOperator().getConst(); + const SetSingletonOp& op = n.getOperator().getConst(); TypeNode type1 = op.getType(); if (check) { diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 4be5ec04d..a895b9083 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -74,8 +74,9 @@ void ArrayCoreSolver::checkNth(const std::vector& nthTerms) Node cond1 = nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n[1]); Node cond2 = nm->mkNode(LT, n[1], nm->mkNode(STRING_LENGTH, n[0])); Node cond = nm->mkNode(AND, cond1, cond2); + TypeNode etn = n.getType().getSequenceElementType(); Node body1 = nm->mkNode( - EQUAL, n, nm->mkNode(SEQ_UNIT, nm->mkNode(SEQ_NTH, n[0], n[1]))); + EQUAL, n, nm->mkSeqUnit(etn, nm->mkNode(SEQ_NTH, n[0], n[1]))); Node body2 = nm->mkNode(EQUAL, n, Word::mkEmptyWord(n.getType())); Node lem = nm->mkNode(ITE, cond, body1, body2); sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_EXTRACT); diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index f5864bdd3..3f3c5ed01 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -123,7 +123,7 @@ void BaseSolver::checkInit() { // (seq.unit x) = (seq.unit y) => x=y, or // (seq.unit x) = (seq.unit c) => x=c - Assert(s.getType() == t.getType()); + Assert(s.getType().isComparableTo(t.getType())); d_im.sendInference(exp, s.eqNode(t), InferenceId::STRINGS_UNIT_INJ); } } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index eb02dc178..4bf2406dd 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2014,7 +2014,7 @@ void CoreSolver::processDeq(Node ni, Node nj) Assert(v.getKind() == SEQ_UNIT); vc = v[0]; } - Assert(u[0].getType() == vc.getType()); + Assert(u[0].getType().isComparableTo(vc.getType())); // if already disequal, we are done if (d_state.areDisequal(u[0], vc)) { diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp index 0e5c19658..df10f47a4 100644 --- a/src/theory/strings/eager_solver.cpp +++ b/src/theory/strings/eager_solver.cpp @@ -126,7 +126,8 @@ bool EagerSolver::checkForMergeConflict(Node a, EqcInfo* eb) { Assert(eb != nullptr && ea != nullptr); - Assert(a.getType() == b.getType()); + Assert(a.getType() == b.getType()) + << "bad types for merge " << a << ", " << b; Assert(a.getType().isStringLike() || a.getType().isInteger()); // check prefix, suffix for (size_t i = 0; i < 2; i++) diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 0b789c1a9..101814102 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -294,6 +294,11 @@ void ExtfSolver::checkExtfEval(int effort) // value, say in this example that (str.replace x "A" "B") != "B". std::vector exp; std::vector schildren; + // seq.unit is parameterized + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + schildren.push_back(n.getOperator()); + } bool schanged = false; for (const Node& nc : n) { diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index fcfefbb43..0a17eed02 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -87,7 +87,15 @@ constant CONST_SEQUENCE \ "expr/sequence.h" \ "a sequence of characters" -operator SEQ_UNIT 1 "a sequence of length one" +constant SEQ_UNIT_OP \ + class \ + SeqUnitOp \ + ::cvc5::SeqUnitOpHashFunction \ + "theory/strings/seq_unit_op.h" \ + "operator for sequence units; payload is an instance of the cvc5::SeqUnitOp class" +parameterized SEQ_UNIT SEQ_UNIT_OP 1 \ +"a sequence of length one. First parameter is a SeqUnitOp. Second is a term" + operator SEQ_NTH 2 "The nth element of a sequence" operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)" @@ -183,6 +191,7 @@ typerule STRING_TOLOWER "SimpleTypeRule" ### sequence specific operators typerule CONST_SEQUENCE ::cvc5::theory::strings::ConstSequenceTypeRule +typerule SEQ_UNIT_OP "SimpleTypeRule" typerule SEQ_UNIT ::cvc5::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::cvc5::theory::strings::SeqNthTypeRule typerule SEQ_NTH_TOTAL ::cvc5::theory::strings::SeqNthTypeRule diff --git a/src/theory/strings/seq_unit_op.cpp b/src/theory/strings/seq_unit_op.cpp new file mode 100644 index 000000000..5c29ffe04 --- /dev/null +++ b/src/theory/strings/seq_unit_op.cpp @@ -0,0 +1,50 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A class for sequence unit + */ + +#include "theory/strings/seq_unit_op.h" + +#include + +#include "expr/type_node.h" + +namespace cvc5 { + +std::ostream& operator<<(std::ostream& out, const SeqUnitOp& op) +{ + return out << "(SeqUnitOp " << op.getType() << ')'; +} + +size_t SeqUnitOpHashFunction::operator()(const SeqUnitOp& op) const +{ + return std::hash()(op.getType()); +} + +SeqUnitOp::SeqUnitOp(const TypeNode& elementType) + : d_type(new TypeNode(elementType)) +{ +} + +SeqUnitOp::SeqUnitOp(const SeqUnitOp& op) : d_type(new TypeNode(op.getType())) +{ +} + +const TypeNode& SeqUnitOp::getType() const { return *d_type; } + +bool SeqUnitOp::operator==(const SeqUnitOp& op) const +{ + return getType() == op.getType(); +} + +} // namespace cvc5 diff --git a/src/theory/strings/seq_unit_op.h b/src/theory/strings/seq_unit_op.h new file mode 100644 index 000000000..c8823c99b --- /dev/null +++ b/src/theory/strings/seq_unit_op.h @@ -0,0 +1,63 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A class for sequence unit + */ + +#include "cvc5_public.h" + +#ifndef CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H +#define CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H + +#include + +namespace cvc5 { + +class TypeNode; + +/** + * The class is an operator for kind SEQ_UNIT used to construct sequences + * of length one. It specifies the type of the single element especially when it + * is a constant. e.g. the type of rational 1 is Int, however (seq.unit + * (seq_unit_op Real) 1) is of type (Seq Real), not (Seq Int). Note that the + * type passed to the constructor is the element's type, not the sequence type. + */ +class SeqUnitOp +{ + public: + SeqUnitOp(const TypeNode& elementType); + SeqUnitOp(const SeqUnitOp& op); + + /** return the type of the current object */ + const TypeNode& getType() const; + + bool operator==(const SeqUnitOp& op) const; + + private: + SeqUnitOp(); + /** a pointer to the type of the singleton element */ + std::unique_ptr d_type; +}; /* class SeqUnitOp */ + +std::ostream& operator<<(std::ostream& out, const SeqUnitOp& op); + +/** + * Hash function for the SeqUnitOp objects. + */ +struct SeqUnitOpHashFunction +{ + size_t operator()(const SeqUnitOp& op) const; +}; /* struct SeqUnitOpHashFunction */ + +} // namespace cvc5 + +#endif /* CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H */ diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index d273df30a..cf2df4734 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -3650,7 +3650,9 @@ Node SequencesRewriter::rewriteSeqUnit(Node node) { std::vector seq; seq.push_back(node[0]); - TypeNode stype = node[0].getType(); + // important to take the type according to the operator here, not the + // type of the argument + TypeNode stype = node.getType().getSequenceElementType(); Node ret = nm->mkConst(Sequence(stype, seq)); return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 81733d571..0f1a2f415 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -478,7 +478,8 @@ bool TheoryStrings::collectModelInfoType( argVal = nfe.d_nf[0][0]; } Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; - assignedValue = rewrite(nm->mkNode(SEQ_UNIT, argVal)); + assignedValue = rewrite( + nm->mkSeqUnit(eqc.getType().getSequenceElementType(), argVal)); Trace("strings-model") << "-> assign via seq.unit: " << assignedValue << std::endl; } @@ -504,6 +505,7 @@ bool TheoryStrings::collectModelInfoType( } else if (options().strings.seqArray != options::SeqArrayMode::NONE) { + TypeNode etype = eqc.getType().getSequenceElementType(); // determine skeleton based on the write model, if it exists const std::map& writeModel = d_asolver.getWriteModel(eqc); Trace("strings-model") @@ -531,7 +533,7 @@ bool TheoryStrings::collectModelInfoType( continue; } usedWrites.insert(ivalue); - Node wsunit = nm->mkNode(SEQ_UNIT, w.second); + Node wsunit = nm->mkSeqUnit(etype, w.second); writes.emplace_back(ivalue, wsunit); } // sort based on index value @@ -761,13 +763,14 @@ Node TheoryStrings::mkSkeletonFor(Node c) const Sequence& sn = c.getConst(); const std::vector& snvec = sn.getVec(); std::vector skChildren; + TypeNode etn = c.getType().getSequenceElementType(); for (const Node& snv : snvec) { - TypeNode etn = snv.getType(); + Assert(snv.getType().isSubtypeOf(etn)); Node v = bvm->mkBoundVar(snv, etn); // use a skolem, not a bound variable Node kv = sm->mkPurifySkolem(v, "smv"); - skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); + skChildren.push_back(nm->mkSeqUnit(etn, kv)); } return utils::mkConcat(skChildren, c.getType()); } @@ -789,7 +792,7 @@ Node TheoryStrings::mkSkeletonFromBase(Node r, cacheVals.push_back(nm->mkConst(CONST_RATIONAL, Rational(currIndex))); Node kv = sm->mkSkolemFunction( SkolemFunId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals); - skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); + skChildren.push_back(nm->mkSeqUnit(etn, kv)); cacheVals.pop_back(); } return utils::mkConcat(skChildren, r.getType()); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 56dcbe25c..ff17efa0e 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -513,7 +513,7 @@ Node StringsPreprocess::reduce(Node t, // nodes for the case where `seq.nth` is defined. Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); - Node unit = nm->mkNode(SEQ_UNIT, skt); + Node unit = nm->mkSeqUnit(t.getType(), skt); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, unit, sk2)); // length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index 965fee2b8..d3ab190cc 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -19,6 +19,7 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "options/strings_options.h" +#include "theory/strings/seq_unit_op.h" #include "util/cardinality.h" namespace cvc5 { @@ -325,7 +326,25 @@ TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - return nodeManager->mkSequenceType(n[0].getType(check)); + Assert(n.getKind() == kind::SEQ_UNIT && n.hasOperator() + && n.getOperator().getKind() == kind::SEQ_UNIT_OP); + + const SeqUnitOp& op = n.getOperator().getConst(); + TypeNode otype = op.getType(); + if (check) + { + TypeNode argType = n[0].getType(check); + // the type of the element should be a subtype of the type of the operator + // e.g. (seq.unit (SeqUnitOp Real) 1) where 1 is an Int + if (!argType.isSubtypeOf(otype)) + { + std::stringstream ss; + ss << "The type '" << argType << "' of the element is not a subtype of '" + << otype << "' in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return nodeManager->mkSequenceType(otype); } TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager, diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 37ceccbc2..69e205da1 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -154,6 +154,7 @@ Node TheoryModel::getValue(TNode n) const } Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl << "[model-getvalue] returning " << nn << std::endl; + Assert(nn.getType().isSubtypeOf(n.getType())); return nn; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8d50b53f7..14c8ad1ca 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1164,7 +1164,13 @@ set(regress_0_tests regress0/seq/nth-unit.smt2 regress0/seq/nth-update.smt2 regress0/seq/proj-issue340.smt2 + regress0/seq/proj-issue384-subtypes.smt2 + regress0/seq/proj-issue384-2-subtypes.smt2 + regress0/seq/proj-issue427-subtypes-value.smt2 regress0/seq/quant_len_trigger.smt2 + regress0/seq/query0-subtype-skel.smt2 + regress0/seq/query1-subtype.smt2 + regress0/seq/query2-subtype.smt2 regress0/seq/rev.smt2 regress0/seq/seqa-model-unsound-dd.smt2 regress0/seq/array/array1.smt2 diff --git a/test/regress/regress0/seq/proj-issue384-2-subtypes.smt2 b/test/regress/regress0/seq/proj-issue384-2-subtypes.smt2 new file mode 100644 index 000000000..3781b2c6b --- /dev/null +++ b/test/regress/regress0/seq/proj-issue384-2-subtypes.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_ALL) +(set-info :status sat) +(declare-const x Real) +(check-sat-assuming ((= 0.0 (/ 0.0 x)) (seq.contains (seq.unit x) (seq.rev (seq.unit x))))) diff --git a/test/regress/regress0/seq/proj-issue384-subtypes.smt2 b/test/regress/regress0/seq/proj-issue384-subtypes.smt2 new file mode 100644 index 000000000..c76f7fa88 --- /dev/null +++ b/test/regress/regress0/seq/proj-issue384-subtypes.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :global-declarations true) +(set-option :strings-exp true) +(assert (let ((_let0 (seq.unit real.pi)))(seq.suffixof _let0 (seq.update _let0 (seq.len _let0) _let0)))) +(assert (let ((_let0 real.pi))(let ((_let1 (- _let0)))(let ((_let2 (+ _let1 _let0)))(>= _let1 (* _let2 _let2) _let1))))) +(check-sat) diff --git a/test/regress/regress0/seq/proj-issue427-subtypes-value.smt2 b/test/regress/regress0/seq/proj-issue427-subtypes-value.smt2 new file mode 100644 index 000000000..e3535b33a --- /dev/null +++ b/test/regress/regress0/seq/proj-issue427-subtypes-value.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +; EXPECT: (((seq.unit _x0) (seq.unit 0.0))) +(set-logic ALL) +(set-option :global-declarations true) +(set-option :produce-models true) +(declare-const _x0 Real) +(assert (= _x0 0.0)) +(check-sat) +(get-value ((seq.unit _x0))) diff --git a/test/regress/regress0/seq/query0-subtype-skel.smt2 b/test/regress/regress0/seq/query0-subtype-skel.smt2 new file mode 100644 index 000000000..6eb7c2b9e --- /dev/null +++ b/test/regress/regress0/seq/query0-subtype-skel.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun rrck_19 () (Seq Real)) +(assert (not (= rrck_19 (str.update rrck_19 2 rrck_19)))) +(check-sat) diff --git a/test/regress/regress0/seq/query1-subtype.smt2 b/test/regress/regress0/seq/query1-subtype.smt2 new file mode 100644 index 000000000..6039c62f2 --- /dev/null +++ b/test/regress/regress0/seq/query1-subtype.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp --simplification=none +; EXPECT: sat +(set-logic ALL) +(declare-fun x () (Seq Real)) +(declare-fun y () (Seq Real)) +(declare-fun a () Real) +(declare-fun b () Real) +(assert +(and (= x (seq.unit b)) (= x (str.update y 2 y)) (= x (str.update y 1 x)) (= x (seq.unit 1.0)) (= x (str.update y 1 (as seq.empty (Seq Real))))) +) +(check-sat) diff --git a/test/regress/regress0/seq/query2-subtype.smt2 b/test/regress/regress0/seq/query2-subtype.smt2 new file mode 100644 index 000000000..10928d98f --- /dev/null +++ b/test/regress/regress0/seq/query2-subtype.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp --simplification=none --strings-fmf +; EXPECT: sat +(set-logic ALL) +(declare-fun x () (Seq Real)) +(declare-fun y () (Seq Real)) +(declare-fun a () Real) +(declare-fun b () Real) +(assert +(and (not (= (= x (str.update x 2 (seq.unit 1.0))) (= x (str.update x 2 (str.update x 0 y))))) (not (= b (seq.nth x 2)))) +) +(check-sat) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 15b5accac..0d92b3b54 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -3141,6 +3141,40 @@ TEST_F(TestApiBlackSolver, proj_issue431) slv.checkSat(); ASSERT_THROW(slv.blockModelValues({t103}), CVC5ApiException); } +TEST_F(TestApiBlackSolver, proj_issue426) +{ + Solver slv; + slv.setLogic("ALL"); + slv.setOption("strings-exp", "true"); + slv.setOption("produce-models", "true"); + slv.setOption("produce-assertions", "true"); + Sort s1 = slv.getRealSort(); + Sort s2 = slv.getRoundingModeSort(); + Sort s4 = slv.mkSequenceSort(s1); + Sort s5 = slv.mkArraySort(s4, s4); + Term t4 = slv.mkConst(s1, "_x3"); + Term t5 = slv.mkReal("9192/832927743"); + Term t19 = slv.mkConst(s2, "_x42"); + Term t24 = slv.mkConst(s5, "_x44"); + Term t37 = slv.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE); + slv.checkSat(); + slv.blockModelValues({t24, t19, t4, t37}); + slv.checkSat(); + ASSERT_NO_THROW(slv.getValue({t5})); +} + +TEST_F(TestApiBlackSolver, proj_issue429) +{ + Solver slv; + Sort s1 = slv.getRealSort(); + Term t6 = slv.mkConst(s1, "_x5"); + Term t16 = + slv.mkReal(std::stoll("1696223.9473797265702297792792306581323741")); + Term t111 = slv.mkTerm(Kind::SEQ_UNIT, {t16}); + Term t119 = slv.mkTerm(slv.mkOp(Kind::SEQ_UNIT), {t6}); + Term t126 = slv.mkTerm(Kind::SEQ_PREFIX, {t111, t119}); + slv.checkEntailed({t126}); +} TEST_F(TestApiBlackSolver, proj_issue422) { diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index aee1ee75e..3f41d5ba1 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -235,11 +235,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_nth) static_cast(std::numeric_limits::max()) + 1); Node s01 = d_nodeManager->mkConst(Sequence(intType, {zero, one})); - Node sx = d_nodeManager->mkNode(SEQ_UNIT, x); - Node sy = d_nodeManager->mkNode(SEQ_UNIT, y); - Node sz = d_nodeManager->mkNode(SEQ_UNIT, z); - Node sw = d_nodeManager->mkNode(SEQ_UNIT, w); - Node sv = d_nodeManager->mkNode(SEQ_UNIT, v); + Node sx = d_nodeManager->mkSeqUnit(intType, x); + Node sy = d_nodeManager->mkSeqUnit(intType, y); + Node sz = d_nodeManager->mkSeqUnit(intType, z); + Node sw = d_nodeManager->mkSeqUnit(intType, w); + Node sv = d_nodeManager->mkSeqUnit(intType, v); Node xyz = d_nodeManager->mkNode(STRING_CONCAT, sx, sy, sz); Node wv = d_nodeManager->mkNode(STRING_CONCAT, sw, sv); @@ -435,11 +435,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_update) Node one = d_nodeManager->mkConstInt(1); Node three = d_nodeManager->mkConstInt(3); - Node sx = d_nodeManager->mkNode(SEQ_UNIT, x); - Node sy = d_nodeManager->mkNode(SEQ_UNIT, y); - Node sz = d_nodeManager->mkNode(SEQ_UNIT, z); - Node sw = d_nodeManager->mkNode(SEQ_UNIT, w); - Node sv = d_nodeManager->mkNode(SEQ_UNIT, v); + Node sx = d_nodeManager->mkSeqUnit(intType, x); + Node sy = d_nodeManager->mkSeqUnit(intType, y); + Node sz = d_nodeManager->mkSeqUnit(intType, z); + Node sw = d_nodeManager->mkSeqUnit(intType, w); + Node sv = d_nodeManager->mkSeqUnit(intType, v); Node xyz = d_nodeManager->mkNode(STRING_CONCAT, sx, sy, sz); Node wv = d_nodeManager->mkNode(STRING_CONCAT, sw, sv); -- 2.30.2