From: yoni206 Date: Tue, 31 Aug 2021 16:45:48 +0000 (+0300) Subject: bv-to-int-module: implementations and stubs for translating operators (#7086) X-Git-Tag: cvc5-1.0.0~1314 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70baef755ad939040c9a670da224512eb076f61b;p=cvc5.git bv-to-int-module: implementations and stubs for translating operators (#7086) This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs. A unit test is added with sanity checks for all implemented operators. --- diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 02fdb4e05..5b9e0bfc4 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -26,6 +26,7 @@ #include "expr/skolem_manager.h" #include "options/option_exception.h" #include "options/uf_options.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" #include "util/iand.h" @@ -34,6 +35,13 @@ namespace cvc5 { using namespace cvc5::theory; +namespace { + +// A helper function to compute 2^b as a Rational +Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); } + +} // namespace + IntBlaster::IntBlaster(context::Context* c, options::SolveBVAsIntMode mode, uint64_t granularity, @@ -65,11 +73,24 @@ void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint, Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); } -Node IntBlaster::maxInt(uint64_t k) { return Node(); } +Node IntBlaster::maxInt(uint64_t k) +{ + Assert(k > 0); + Rational max_value = intpow2(k) - 1; + return d_nm->mkConst(max_value); +} -Node IntBlaster::pow2(uint64_t k) { return Node(); } +Node IntBlaster::pow2(uint64_t k) +{ + Assert(k >= 0); + return d_nm->mkConst(intpow2(k)); +} -Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); } +Node IntBlaster::modpow2(Node n, uint64_t exponent) +{ + Node p2 = d_nm->mkConst(intpow2(exponent)); + return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); +} Node IntBlaster::makeBinary(Node n) { @@ -194,8 +215,350 @@ Node IntBlaster::translateWithChildren( const std::vector& translated_children, std::vector& lemmas) { - Node binarized = makeBinary(original); - // continue to process the binarized version + // The translation of the original node is determined by the kind of + // the node. + kind::Kind_t oldKind = original.getKind(); + + // Some BV operators were eliminated before this point. + Assert(oldKind != kind::BITVECTOR_SDIV); + Assert(oldKind != kind::BITVECTOR_SREM); + Assert(oldKind != kind::BITVECTOR_SMOD); + Assert(oldKind != kind::BITVECTOR_XNOR); + Assert(oldKind != kind::BITVECTOR_NAND); + Assert(oldKind != kind::BITVECTOR_SUB); + Assert(oldKind != kind::BITVECTOR_REPEAT); + Assert(oldKind != kind::BITVECTOR_ROTATE_RIGHT); + Assert(oldKind != kind::BITVECTOR_ROTATE_LEFT); + Assert(oldKind != kind::BITVECTOR_COMP); + Assert(oldKind != kind::BITVECTOR_SGT); + Assert(oldKind != kind::BITVECTOR_SLE); + Assert(oldKind != kind::BITVECTOR_SGE); + Assert(oldKind != kind::EXISTS); + + // BV division by zero was eliminated before this point. + Assert(oldKind != kind::BITVECTOR_UDIV + || !(original[1].isConst() + && original[1].getConst().getValue().isZero())); + + // Store the translated node + Node returnNode; + + // Translate according to the kind of the original node. + switch (oldKind) + { + case kind::BITVECTOR_ADD: + { + Assert(original.getNumChildren() == 2); + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createBVAddNode( + translated_children[0], translated_children[1], bvsize); + break; + } + case kind::BITVECTOR_MULT: + { + Assert(original.getNumChildren() == 2); + uint64_t bvsize = original[0].getType().getBitVectorSize(); + Node mult = d_nm->mkNode(kind::MULT, translated_children); + Node p2 = pow2(bvsize); + returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2); + break; + } + case kind::BITVECTOR_UDIV: + { + // we use an ITE for the case where the second operand is 0. + uint64_t bvsize = original[0].getType().getBitVectorSize(); + Node pow2BvSize = pow2(bvsize); + Node divNode = + d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children); + returnNode = d_nm->mkNode( + kind::ITE, + d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), + d_nm->mkNode(kind::MINUS, pow2BvSize, d_one), + divNode); + break; + } + case kind::BITVECTOR_UREM: + { + // we use an ITE for the case where the second operand is 0. + Node modNode = + d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children); + returnNode = d_nm->mkNode( + kind::ITE, + d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), + translated_children[0], + modNode); + break; + } + case kind::BITVECTOR_NOT: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createBVNotNode(translated_children[0], bvsize); + break; + } + case kind::BITVECTOR_NEG: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createBVNegNode(translated_children[0], bvsize); + break; + } + case kind::BITVECTOR_TO_NAT: + { + // In this case, we already translated the child to integer. + // The result is simply the translated child. + returnNode = translated_children[0]; + break; + } + case kind::INT_TO_BITVECTOR: + { + // In this case we take the original integer, + // modulo 2 to the power of the bit-width + returnNode = + modpow2(translated_children[0], + original.getOperator().getConst().d_size); + break; + } + case kind::BITVECTOR_OR: + { + Assert(translated_children.size() == 2); + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createBVOrNode( + translated_children[0], translated_children[1], bvsize, lemmas); + break; + } + case kind::BITVECTOR_XOR: + { + Assert(translated_children.size() == 2); + uint64_t bvsize = original[0].getType().getBitVectorSize(); + // Based on Hacker's Delight section 2-2 equation n: + // x xor y = x|y - x&y + Node bvor = createBVOrNode( + translated_children[0], translated_children[1], bvsize, lemmas); + Node bvand = createBVAndNode( + translated_children[0], translated_children[1], bvsize, lemmas); + returnNode = createBVSubNode(bvor, bvand, bvsize); + break; + } + case kind::BITVECTOR_AND: + { + Assert(translated_children.size() == 2); + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createBVAndNode( + translated_children[0], translated_children[1], bvsize, lemmas); + break; + } + case kind::BITVECTOR_SHL: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createShiftNode(translated_children, bvsize, true); + break; + } + case kind::BITVECTOR_LSHR: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = createShiftNode(translated_children, bvsize, false); + break; + } + case kind::BITVECTOR_ASHR: + { + /* From SMT-LIB2: + * (bvashr s t) abbreviates + * (ite (= ((_ extract |m-1| |m-1|) s) #b0) + * (bvlshr s t) + * (bvnot (bvlshr (bvnot s) t))) + * + * Equivalently: + * (bvashr s t) abbreviates + * (ite (bvult s 100000...) + * (bvlshr s t) + * (bvnot (bvlshr (bvnot s) t))) + * + */ + // signed_min is 100000... + uint64_t bvsize = original[0].getType().getBitVectorSize(); + Node signed_min = pow2(bvsize - 1); + Node condition = + d_nm->mkNode(kind::LT, translated_children[0], signed_min); + Node thenNode = createShiftNode(translated_children, bvsize, false); + std::vector children = { + createBVNotNode(translated_children[0], bvsize), + translated_children[1]}; + Node elseNode = + createBVNotNode(createShiftNode(children, bvsize, false), bvsize); + returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode); + break; + } + case kind::BITVECTOR_ITE: + { + // Lifted to a boolean ite. + Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one); + returnNode = d_nm->mkNode( + kind::ITE, cond, translated_children[1], translated_children[2]); + break; + } + case kind::BITVECTOR_ZERO_EXTEND: + { + // zero extension does not change the integer translation. + returnNode = translated_children[0]; + break; + } + case kind::BITVECTOR_SIGN_EXTEND: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = + createSignExtendNode(translated_children[0], + bvsize, + bv::utils::getSignExtendAmount(original)); + break; + } + case kind::BITVECTOR_CONCAT: + { + // (concat a b) translates to a*2^k+b, k being the bitwidth of b. + uint64_t bvsizeRight = original[1].getType().getBitVectorSize(); + Node pow2BvSizeRight = pow2(bvsizeRight); + Node a = + d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight); + Node b = translated_children[1]; + returnNode = d_nm->mkNode(kind::PLUS, a, b); + break; + } + case kind::BITVECTOR_EXTRACT: + { + // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1} + // original = a[i:j] + uint64_t i = bv::utils::getExtractHigh(original); + uint64_t j = bv::utils::getExtractLow(original); + Assert(i >= j); + Node div = d_nm->mkNode( + kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j)); + returnNode = modpow2(div, i - j + 1); + break; + } + case kind::EQUAL: + { + returnNode = d_nm->mkNode(kind::EQUAL, translated_children); + break; + } + case kind::BITVECTOR_ULT: + { + returnNode = d_nm->mkNode(kind::LT, translated_children); + break; + } + case kind::BITVECTOR_SLT: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = d_nm->mkNode(kind::LT, + uts(translated_children[0], bvsize), + uts(translated_children[1], bvsize)); + break; + } + case kind::BITVECTOR_ULE: + { + returnNode = d_nm->mkNode(kind::LEQ, translated_children); + break; + } + case kind::BITVECTOR_UGT: + { + returnNode = d_nm->mkNode(kind::GT, translated_children); + break; + } + case kind::BITVECTOR_UGE: + { + returnNode = d_nm->mkNode(kind::GEQ, translated_children); + break; + } + case kind::BITVECTOR_ULTBV: + { + returnNode = d_nm->mkNode(kind::ITE, + d_nm->mkNode(kind::LT, translated_children), + d_one, + d_zero); + break; + } + case kind::BITVECTOR_SLTBV: + { + uint64_t bvsize = original[0].getType().getBitVectorSize(); + returnNode = + d_nm->mkNode(kind::ITE, + d_nm->mkNode(kind::LT, + uts(translated_children[0], bvsize), + uts(translated_children[1], bvsize)), + d_one, + d_zero); + break; + } + case kind::ITE: + { + returnNode = d_nm->mkNode(oldKind, translated_children); + break; + } + case kind::APPLY_UF: + { + /** + * higher order logic allows comparing between functions + * The translation does not support this, + * as the translated functions may be different outside + * of the bounds that were relevant for the original + * bit-vectors. + */ + if (childrenTypesChanged(original) && options::ufHo()) + { + throw OptionException("bv-to-int does not support higher order logic "); + } + // Insert the translated application term to the cache + returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children); + // Add range constraints if necessary. + // If the original range was a BV sort, the original application of + // the function must be within the range determined by the + // bitwidth. + if (original.getType().isBitVector()) + { + addRangeConstraint( + returnNode, original.getType().getBitVectorSize(), lemmas); + } + break; + } + case kind::BOUND_VAR_LIST: + { + returnNode = d_nm->mkNode(oldKind, translated_children); + break; + } + case kind::FORALL: + { + returnNode = translateQuantifiedFormula(original); + break; + } + default: + { + // first, verify that we haven't missed + // any bv operator + Assert(theory::kindToTheoryId(oldKind) != THEORY_BV); + + // In the default case, we have reached an operator that we do not + // translate directly to integers. The children whose types have + // changed from bv to int should be adjusted back to bv and then + // this term is reconstructed. + TypeNode resultingType; + if (original.getType().isBitVector()) + { + resultingType = d_nm->integerType(); + } + else + { + resultingType = original.getType(); + } + Node reconstruction = + reconstructNode(original, resultingType, translated_children); + returnNode = reconstruction; + break; + } + } + Trace("int-blaster-debug") << "original: " << original << std::endl; + Trace("int-blaster-debug") << "returnNode: " << returnNode << std::endl; + return returnNode; +} + +Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) +{ return Node(); } @@ -419,4 +782,53 @@ Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode) return Node(); } +Node IntBlaster::createBVAndNode(Node x, + Node y, + uint64_t bvsize, + std::vector& lemmas) +{ + return Node(); +} + +Node IntBlaster::createBVOrNode(Node x, + Node y, + uint64_t bvsize, + std::vector& lemmas) +{ + // Based on Hacker's Delight section 2-2 equation h: + // x+y = x|y + x&y + // from which we deduce: + // x|y = x+y - x&y + Node plus = createBVAddNode(x, y, bvsize); + Node bvand = createBVAndNode(x, y, bvsize, lemmas); + return createBVSubNode(plus, bvand, bvsize); +} + +Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize) +{ + Node minus = d_nm->mkNode(kind::MINUS, x, y); + Node p2 = pow2(bvsize); + return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2); +} + +Node IntBlaster::createBVAddNode(Node x, Node y, uint64_t bvsize) +{ + Node plus = d_nm->mkNode(kind::PLUS, x, y); + Node p2 = pow2(bvsize); + return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2); +} + +Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize) +{ + // Based on Hacker's Delight section 2-2 equation a: + // -x = ~x+1 + Node p2 = pow2(bvsize); + return d_nm->mkNode(kind::MINUS, p2, n); +} + +Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) +{ + return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n); +} + } // namespace cvc5 diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index e98ae149e..1b4d5cdd6 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -74,6 +74,11 @@ namespace cvc5 { ** Tr(a=b) = Tr(a)=Tr(b) ** Tr((bvult a b)) = Tr(a) < Tr(b) ** Similar transformations are done for bvule, bvugt, and bvuge. +** Tr((bvslt a b)) = Tr(uts(a)) < Tr(uts(b)), +** where uts is a function that transforms unsigned +** to signed representations. See more details +** in the documentation of the function uts. +** Similar transformations are done for the remaining comparators. ** ** Bit-vector operators that are not listed above are either ** eliminated using the BV rewriter, @@ -151,6 +156,35 @@ class IntBlaster /** Adds a constraint that encodes bitwise and */ void addBitwiseConstraint(Node bitwiseConstraint, std::vector& lemmas); + /** Returns a node that represents the bitwise negation of n. */ + Node createBVNotNode(Node n, uint64_t bvsize); + + /** Returns a node that represents the arithmetic negation of n. */ + Node createBVNegNode(Node n, uint64_t bvsize); + + /** Returns a node that represents the bitwise and of x and y, based on the + * provided option. */ + Node createBVAndNode(Node x, + Node y, + uint64_t bvsize, + std::vector& lemmas); + + /** Returns a node that represents the bitwise or of x and y, by translation + * to sum and bitwise and. */ + Node createBVOrNode(Node x, + Node y, + uint64_t bvsize, + std::vector& lemmas); + + /** Returns a node that represents the sum of x and y. */ + Node createBVAddNode(Node x, Node y, uint64_t bvsize); + + /** Returns a node that represents the difference of x and y. */ + Node createBVSubNode(Node x, Node y, uint64_t bvsize); + + /** Returns a node that represents the signed extension of x by amount. */ + Node createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount); + /** * Whenever we introduce an integer variable that represents a bit-vector * variable, we need to guard the range of the newly introduced variable. diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index b17ccf342..f76305db6 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -21,6 +21,7 @@ #include "options/options.h" #include "test_smt.h" #include "theory/bv/int_blaster.h" +#include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" #include "util/rational.h" namespace cvc5 { @@ -45,7 +46,7 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit Node d_one; }; -TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_constants) +TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) { // place holders for lemmas and skolem std::vector lemmas; @@ -67,7 +68,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_constants) ASSERT_EQ(seven, result); } -TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_symbolic_constant) +TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) { // place holders for lemmas and skolem std::vector lemmas; @@ -88,7 +89,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_symbolic_constant) ASSERT_EQ(resultSquared, result); } -TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_uf) +TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) { // place holders for lemmas and skolem std::vector lemmas; @@ -119,5 +120,129 @@ TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_uf) ASSERT_TRUE(resultRange.isBoolean()); } +/** Check all cases of the translation. + * This is a sanity check, that noly verifies + * the expected type, and that there were no + * failures. + */ +TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) +{ + // place holders for lemmas and skolem + std::vector lemmas; + std::map skolems; + IntBlaster intBlaster( + d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + + // bit-vector variables + TypeNode bvType = d_nodeManager->mkBitVectorType(4); + Node v1 = d_nodeManager->mkVar("v1", bvType); + Node v2 = d_nodeManager->mkVar("v2", bvType); + + // translated integer variables + Node i1 = intBlaster.translateNoChildren(v1, lemmas, skolems); + Node i2 = intBlaster.translateNoChildren(v2, lemmas, skolems); + + // if original is BV, result should be Int. + // Otherwise, they should have the same type. + Node original; + Node result; + + // sum + original = d_nodeManager->mkNode(BITVECTOR_ADD, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // multiplication + original = d_nodeManager->mkNode(BITVECTOR_MULT, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // division 1 + original = d_nodeManager->mkNode(BITVECTOR_UDIV, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // division 2 + original = d_nodeManager->mkNode(BITVECTOR_UREM, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // bit-wise negation + original = d_nodeManager->mkNode(BITVECTOR_NOT, v1); + result = intBlaster.translateWithChildren(original, {i1}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // arithmetic negation + original = d_nodeManager->mkNode(BITVECTOR_NEG, v1); + result = intBlaster.translateWithChildren(original, {i1}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // bv2nat + original = d_nodeManager->mkNode(BITVECTOR_TO_NAT, v1); + result = intBlaster.translateWithChildren(original, {i1}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // int2bv + Node intToBVOp = d_nodeManager->mkConst(IntToBitVector(4)); + original = d_nodeManager->mkNode(intToBVOp, i1); + result = intBlaster.translateWithChildren(original, {i1}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // zero extend + Node zeroExtOp = + d_nodeManager->mkConst(BitVectorZeroExtend(4)); + original = d_nodeManager->mkNode(zeroExtOp, v1); + result = intBlaster.translateWithChildren(original, {i1}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // extract + BV ITE + Node extract = theory::bv::utils::mkExtract(v1, 0, 0); + original = d_nodeManager->mkNode(BITVECTOR_ITE, extract, v2, v1); + Node intExtract = intBlaster.translateWithChildren(extract, {i1}, lemmas); + result = + intBlaster.translateWithChildren(original, {intExtract, i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + ASSERT_TRUE(intExtract.getType().isInteger()); + + // concat + original = d_nodeManager->mkNode(BITVECTOR_CONCAT, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // predicates + original = d_nodeManager->mkNode(EQUAL, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isBoolean()); + + original = d_nodeManager->mkNode(BITVECTOR_ULT, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isBoolean()); + + original = d_nodeManager->mkNode(BITVECTOR_ULE, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isBoolean()); + + original = d_nodeManager->mkNode(BITVECTOR_UGT, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isBoolean()); + + original = d_nodeManager->mkNode(BITVECTOR_UGE, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isBoolean()); + + // BVULT with a BV result + original = d_nodeManager->mkNode(BITVECTOR_ULTBV, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // function application + TypeNode funType = d_nodeManager->mkFunctionType({bvType}, bvType); + Node f = d_nodeManager->mkVar("f", funType); + Node g = intBlaster.translateNoChildren(f, lemmas, skolems); + original = d_nodeManager->mkNode(APPLY_UF, f, v1); + result = intBlaster.translateWithChildren(original, {g, i1}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); +} + } // namespace test } // namespace cvc5