diff options
| -rw-r--r-- | src/theory/bv/int_blaster.cpp | 198 | ||||
| -rw-r--r-- | src/theory/bv/int_blaster.h | 7 | ||||
| -rw-r--r-- | test/unit/theory/theory_bv_int_blaster_white.cpp | 78 |
3 files changed, 269 insertions, 14 deletions
diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 9da9d1c2b..02fdb4e05 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -16,6 +16,7 @@ #include "theory/bv/int_blaster.h" #include <cmath> +#include <sstream> #include <string> #include <unordered_map> #include <vector> @@ -26,6 +27,7 @@ #include "options/option_exception.h" #include "options/uf_options.h" #include "theory/rewriter.h" +#include "util/bitvector.h" #include "util/iand.h" #include "util/rational.h" @@ -185,7 +187,7 @@ Node IntBlaster::intBlast(Node n, return d_intblastCache[n].get(); } -Node IntBlaster::unsignedToSigned(Node n, uint64_t bw) { return Node(); } +Node IntBlaster::uts(Node n, uint64_t bw) { return Node(); } Node IntBlaster::translateWithChildren( Node original, @@ -201,20 +203,202 @@ Node IntBlaster::translateNoChildren(Node original, std::vector<Node>& lemmas, std::map<Node, Node>& skolems) { - return Node(); -} + Trace("int-blaster-debug") + << "translating leaf: " << original << "; of type: " << original.getType() + << std::endl; + + // The result of the translation + Node translation; + + // The translation is done differently for variables (bound or free) and + // constants (values) + Assert(original.isVar() || original.isConst()); + if (original.isVar()) + { + if (original.getType().isBitVector()) + { + // For bit-vector variables, we create fresh integer variables. + if (original.getKind() == kind::BOUND_VARIABLE) + { + // Range constraints for the bound integer variables are not added now. + // they will be added once the quantifier itself is handled. + std::stringstream ss; + ss << original; + translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType()); + } + else + { + // original is a bit-vector variable (symbolic constant). + // Either we translate it to a fresh integer variable, + // or we translate it to (bv2nat original). + // In the former case, we must include range lemmas, while in the + // latter we don't. + // This is determined by the option bv-to-int-fresh-vars. + // The variables intCast and bvCast are used for models: + // even if we introduce a fresh variable, + // it is associated with intCast (which is (bv2nat original)). + // bvCast is either ( (_ nat2bv k) original) or just original. + Node intCast = castToType(original, d_nm->integerType()); + Node bvCast; + if (d_introduceFreshIntVars) + { + // we introduce a fresh variable, add range constraints, and save the + // connection between original and the new variable via intCast + translation = d_nm->getSkolemManager()->mkPurifySkolem( + intCast, + "__intblast__var", + "Variable introduced in intblasting for " + original.toString()); + uint64_t bvsize = original.getType().getBitVectorSize(); + addRangeConstraint(translation, bvsize, lemmas); + // put new definition of old variable in skolems + bvCast = castToType(translation, original.getType()); + } + else + { + // we just translate original to (bv2nat original) + translation = intCast; + // no need to do any casting back to bit-vector in this case. + bvCast = original; + } -Node IntBlaster::defineBVUFAsIntUF(Node bvUF, Node intUF) { return Node(); } + // add bvCast to skolems if it is not already there. + if (skolems.find(original) == skolems.end()) + { + skolems[original] = bvCast; + } + else + { + Assert(skolems[original] == bvCast); + } + } + } + else if (original.getType().isFunction()) + { + // translate function symbol + translation = translateFunctionSymbol(original, skolems); + } + else + { + // leave other variables intact + translation = original; + } + } + else + { + // original is a constant (value) + if (original.getKind() == kind::CONST_BITVECTOR) + { + // Bit-vector constants are transformed into their integer value. + BitVector constant(original.getConst<BitVector>()); + Integer c = constant.toInteger(); + translation = d_nm->mkConst<Rational>(c); + } + else + { + // Other constants stay the same. + translation = original; + } + } + return translation; +} Node IntBlaster::translateFunctionSymbol(Node bvUF, std::map<Node, Node>& skolems) { - return Node(); + // construct the new function symbol. + Node intUF; + + // old and new types of domain and result + TypeNode tn = bvUF.getType(); + TypeNode bvRange = tn.getRangeType(); + std::vector<TypeNode> bvDomain = tn.getArgTypes(); + std::vector<TypeNode> intDomain; + + // if the original range is a bit-vector sort, + // the new range should be an integer sort. + // Otherwise, we keep the original range. + // Similarly for the domain sorts. + TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange; + for (const TypeNode& d : bvDomain) + { + intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d); + } + + // create the new function symbol as a skolem + std::ostringstream os; + os << "__intblast_fun_" << bvUF << "_int"; + SkolemManager* sm = d_nm->getSkolemManager(); + intUF = sm->mkDummySkolem( + os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function"); + + // add definition of old function symbol to skolems. + + // formal arguments of the lambda expression. + std::vector<Node> args; + + // arguments to be passed in the application. + std::vector<Node> achildren; + achildren.push_back(intUF); + + // iterate the arguments, cast BV arguments to integers + int i = 0; + for (const TypeNode& d : bvDomain) + { + // Each bit-vector argument is casted to a natural number + // Other arguments are left intact. + Node fresh_bound_var = d_nm->mkBoundVar(d); + args.push_back(fresh_bound_var); + Node castedArg = args[i]; + if (d.isBitVector()) + { + castedArg = castToType(castedArg, d_nm->integerType()); + } + achildren.push_back(castedArg); + i++; + } + + // create the lambda expression, and add it to skolems + Node app = d_nm->mkNode(kind::APPLY_UF, achildren); + Node body = castToType(app, bvRange); + Node bvlist = d_nm->mkNode(kind::BOUND_VAR_LIST, args); + Node result = d_nm->mkNode(kind::LAMBDA, bvlist, body); + if (skolems.find(bvUF) == skolems.end()) + { + skolems[bvUF] = result; + } + return intUF; } bool IntBlaster::childrenTypesChanged(Node n) { return true; } -Node IntBlaster::castToType(Node n, TypeNode tn) { return Node(); } +Node IntBlaster::castToType(Node n, TypeNode tn) +{ + // If there is no reason to cast, return the + // original node. + if (n.getType().isSubtypeOf(tn)) + { + return n; + } + // We only case int to bv or vice verse. + Assert((n.getType().isBitVector() && tn.isInteger()) + || (n.getType().isInteger() && tn.isBitVector())); + Trace("int-blaster") << "castToType from " << n.getType() << " to " << tn + << std::endl; + + // casting integers to bit-vectors + if (n.getType().isInteger()) + { + Assert(tn.isBitVector()); + unsigned bvsize = tn.getBitVectorSize(); + Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); + return d_nm->mkNode(intToBVOp, n); + } + + // casting bit-vectors to ingers + Assert(n.getType().isBitVector()); + Assert(tn.isInteger()); + return d_nm->mkNode(kind::BITVECTOR_TO_NAT, n); +} Node IntBlaster::reconstructNode(Node originalNode, TypeNode resultType, @@ -235,6 +419,4 @@ Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode) return Node(); } -Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) { return Node(); } - } // namespace cvc5 diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index 444eb88a7..e98ae149e 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -151,9 +151,6 @@ class IntBlaster /** Adds a constraint that encodes bitwise and */ void addBitwiseConstraint(Node bitwiseConstraint, std::vector<Node>& lemmas); - /** Returns a node that represents the bitwise negation of n. */ - Node createBVNotNode(Node n, uint64_t bvsize); - /** * Whenever we introduce an integer variable that represents a bit-vector * variable, we need to guard the range of the newly introduced variable. @@ -240,7 +237,7 @@ class IntBlaster * A useful utility function. * if n is an integer and tn is bit-vector, * applies the IntToBitVector operator on n. - * if n is a vit-vector and tn is integer, + * if n is a bit-vector and tn is integer, * applies BitVector_TO_NAT operator. * Otherwise, keeps n intact. */ @@ -284,7 +281,7 @@ class IntBlaster * binary representation of n is the same as the * signed binary representation of m. */ - Node unsignedToSigned(Node n, uint64_t bvsize); + Node uts(Node n, uint64_t bvsize); /** * Performs the actual translation to integers for nodes diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 1e19b14b4..b17ccf342 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -17,11 +17,12 @@ #include <memory> #include <vector> +#include "context/context.h" +#include "options/options.h" #include "test_smt.h" #include "theory/bv/int_blaster.h" #include "util/bitvector.h" #include "util/rational.h" - namespace cvc5 { using namespace kind; @@ -43,5 +44,80 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit Node d_true; Node d_one; }; + +TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_constants) +{ + // place holders for lemmas and skolem + std::vector<Node> lemmas; + std::map<Node, Node> skolems; + + // bit-vector constant representing the integer 7, with 4 bits + BitVector c1(4, Integer(7)); + Node bv7_4 = d_nodeManager->mkConst<BitVector>(c1); + + // translating it to integers should yield 7. + IntBlaster intBlaster( + d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, false); + Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); + Node seven = d_nodeManager->mkConst(Rational(7)); + ASSERT_EQ(seven, result); + + // translating integer constants should not change them + result = intBlaster.translateNoChildren(seven, lemmas, skolems); + ASSERT_EQ(seven, result); +} + +TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_symbolic_constant) +{ + // place holders for lemmas and skolem + std::vector<Node> lemmas; + std::map<Node, Node> skolems; + + // bit-vector variable + TypeNode bvType = d_nodeManager->mkBitVectorType(4); + Node bv = d_nodeManager->mkVar("bv1", bvType); + + // translating it to integers should yield an integer variable. + IntBlaster intBlaster( + d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + Node result = intBlaster.translateNoChildren(bv, lemmas, skolems); + ASSERT_TRUE(result.isVar() && result.getType().isInteger()); + + // translating integer variables should not change them + Node resultSquared = intBlaster.translateNoChildren(result, lemmas, skolems); + ASSERT_EQ(resultSquared, result); +} + +TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_uf) +{ + // place holders for lemmas and skolem + std::vector<Node> lemmas; + std::map<Node, Node> skolems; + + // uf from integers and bit-vectors to Bools + std::vector<TypeNode> domain; + TypeNode bvType = d_nodeManager->mkBitVectorType(4); + TypeNode intType = d_nodeManager->integerType(); + domain.push_back(intType); + domain.push_back(bvType); + TypeNode range = d_nodeManager->booleanType(); + TypeNode funType = d_nodeManager->mkFunctionType(domain, range); + Node f = d_nodeManager->mkVar("f", funType); + + // translating it to integers should yield an Int x Int -> Bool function + IntBlaster intBlaster( + d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + Node result = intBlaster.translateNoChildren(f, lemmas, skolems); + TypeNode resultType = result.getType(); + std::vector<TypeNode> resultDomain = resultType.getArgTypes(); + TypeNode resultRange = resultType.getRangeType(); + ASSERT_TRUE(result.isVar()); + ASSERT_TRUE(resultType.isFunction()); + ASSERT_TRUE(resultDomain.size() == 2); + ASSERT_TRUE(resultDomain[0].isInteger()); + ASSERT_TRUE(resultDomain[1].isInteger()); + ASSERT_TRUE(resultRange.isBoolean()); +} + } // namespace test } // namespace cvc5 |