diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-08-24 04:20:56 +0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-24 01:20:56 +0000 |
commit | 2c35a4fd262a7aa1cc3b953265d327de4eae9f8e (patch) | |
tree | 0ff9aeea76a86ad8fe07a344384de37139efcfdc /src/theory/bv | |
parent | 198e4a9b622bff260cf6b24f67f31fbff11873f2 (diff) |
bv-to-int: more implementations (#7051)
This PR introduces more implementations for the bv-to-int module. Once all implementations are in, this module will be called from the bv-to-int preprocessing pass, and the code there will be deleted.
Here we focus on the translation of nodes without children.
Unit tests are included.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/int_blaster.cpp | 198 | ||||
-rw-r--r-- | src/theory/bv/int_blaster.h | 7 |
2 files changed, 192 insertions, 13 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 |