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.
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
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);
#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"
}
}
+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))
/** 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.
{
const Sequence& sn = n.getConst<Sequence>();
const std::vector<Node>& 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)
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;
}
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:
{
Trace("sygus-grammar-def") << "...add for seq.unit" << std::endl;
std::vector<TypeNode> 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())
#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;
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;
}
* A class for singleton operator for sets.
*/
-#include "singleton_op.h"
+#include "theory/sets/singleton_op.h"
#include <iostream>
#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 <memory>
std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op);
/**
- * Hash function for the SingletonHashFunction objects.
+ * Hash function for the SetSingletonOp objects.
*/
struct SetSingletonOpHashFunction
{
} // namespace cvc5
-#endif /* CVC5__SINGLETON_OP_H */
+#endif /* CVC5__THEORY__SETS__SINGLETON_OP_H */
Assert(n.getKind() == kind::SET_SINGLETON && n.hasOperator()
&& n.getOperator().getKind() == kind::SET_SINGLETON_OP);
- SetSingletonOp op = n.getOperator().getConst<SetSingletonOp>();
+ const SetSingletonOp& op = n.getOperator().getConst<SetSingletonOp>();
TypeNode type1 = op.getType();
if (check)
{
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);
{
// (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);
}
}
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))
{
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++)
// value, say in this example that (str.replace x "A" "B") != "B".
std::vector<Node> exp;
std::vector<Node> schildren;
+ // seq.unit is parameterized
+ if (n.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ schildren.push_back(n.getOperator());
+ }
bool schanged = false;
for (const Node& nc : n)
{
"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)"
### sequence specific operators
typerule CONST_SEQUENCE ::cvc5::theory::strings::ConstSequenceTypeRule
+typerule SEQ_UNIT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule SEQ_UNIT ::cvc5::theory::strings::SeqUnitTypeRule
typerule SEQ_NTH ::cvc5::theory::strings::SeqNthTypeRule
typerule SEQ_NTH_TOTAL ::cvc5::theory::strings::SeqNthTypeRule
--- /dev/null
+/******************************************************************************
+ * 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 <iostream>
+
+#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<TypeNode>()(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
--- /dev/null
+/******************************************************************************
+ * 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 <memory>
+
+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<TypeNode> 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 */
{
std::vector<Node> 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);
}
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;
}
}
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<Node, Node>& writeModel = d_asolver.getWriteModel(eqc);
Trace("strings-model")
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
const Sequence& sn = c.getConst<Sequence>();
const std::vector<Node>& snvec = sn.getVec();
std::vector<Node> skChildren;
+ TypeNode etn = c.getType().getSequenceElementType();
for (const Node& snv : snvec)
{
- TypeNode etn = snv.getType();
+ Assert(snv.getType().isSubtypeOf(etn));
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));
+ skChildren.push_back(nm->mkSeqUnit(etn, kv));
}
return utils::mkConcat(skChildren, c.getType());
}
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());
// 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);
#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 {
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<SeqUnitOp>();
+ 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,
}
Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
<< "[model-getvalue] returning " << nn << std::endl;
+ Assert(nn.getType().isSubtypeOf(n.getType()));
return nn;
}
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
--- /dev/null
+; 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)))))
--- /dev/null
+(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)
--- /dev/null
+; 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)))
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
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)
{
static_cast<uint64_t>(std::numeric_limits<uint32_t>::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);
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);
projects / cvc5.git / commitdiff