~ubuntu-branches/ubuntu/wily/acl2/wily

; transforms a bit-vector v into a bit-vector of len n, if n is bigger then v's length. if not, returns the last n bits of v (v is considered in big-endian representation)

130

131

(defun bv-to-n (v n)

132

(if (and (bvp v)

133

(integerp n)

134

(<= 0 n))

135

(if (>= n (len v))

136

(append (make-list (- n (len v)) :initial-element 0) v)

137

(nthcdr (- (len v) n) v))

138

nil))

139

140

141

;and between two bit-vectors with the same length

142

143

(defun bv-a (x y)

144

(if (and (bvp x) (bvp y)

145

(equal (len x) (len y)))

146

(if (endp x) nil

147

(cons (b-and (car x) (car y))

148

(bv-a (cdr x) (cdr y))))

149

nil))

150

151

152

153

;and between two bit-vectors with arbitrary length

154

155

(defun binary-bv-and (x y)

156

(if (and (bvp x) (bvp y))

157

(if (<= (len x) (len y))

158

(bv-a (bv-to-n x (len y)) y)

159

(bv-a x (bv-to-n y (len x))))

160

nil))

161

162

163

(defun bv-and-macro (lst)

164

(if (consp lst)

165

(if (consp (cdr lst))

166

(list 'binary-bv-and (car lst)

167

(bv-and-macro (cdr lst)))

168

(car lst))

169

nil))

170

171

(defmacro bv-and (&rest args)

172

(bv-and-macro args))

173

174

175

176

;or between two bit-vectors with the same length

177

178

(defun bv-o (x y)

179

(if (and (bvp x) (bvp y)

180

(equal (len x) (len y)))

181

(if (endp x) nil

182

(cons (b-or (car x) (car y))

183

(bv-o (cdr x) (cdr y))))

184

nil))

185

186

;or between two bit-vectors with arbitrary length

187

188

(defun binary-bv-or (x y)

189

(if (and (bvp x) (bvp y))

190

(if (<= (len x) (len y))

191

(bv-o (bv-to-n x (len y)) y)

192

(bv-o x (bv-to-n y (len x))))

193

nil))

194

195

(defun bv-or-macro (lst)

196

(if (consp lst)

197

(if (consp (cdr lst))

198

(list 'binary-bv-or (car lst)

199

(bv-or-macro (cdr lst)))

200

(car lst))

201

nil))

202

203

(defmacro bv-or (&rest args)

204

(bv-or-macro args))

205

206

207

208

;xor between two bit-vectors with the same length

209

210

(defun bv-xo (x y)

211

(if (and (bvp x) (bvp y)

212

(equal (len x) (len y)))

213

(if (endp x) nil

214

(cons (b-xor (car x) (car y))

215

(bv-xo (cdr x) (cdr y))))

216

nil))

217

218

219

220

;xor between two bit-vectors with arbitrary length

221

222

(defun binary-bv-xor (x y)

223

(if (and (bvp x) (bvp y))

224

(if (<= (len x) (len y))

225

(bv-xo (bv-to-n x (len y)) y)

226

(bv-xo x (bv-to-n y (len x))))

227

nil))

228

229

(defun bv-xor-macro (lst)

230

(if (consp lst)

231

(if (consp (cdr lst))

232

(list 'binary-bv-xor (car lst)

233

(bv-xor-macro (cdr lst)))

234

(car lst))

235

nil))

236

237

(defmacro bv-xor (&rest args)

238

(bv-xor-macro args))

239

240

241

; not of a bit-vector x

242

243

(defun bv-not (x)

244

(if (bvp x)

245

(if (endp x)

246

nil

247

(cons (b-not (car x)) (bv-not (cdr x))))

248

nil))

249

250

251

252

; addition modulo (2 pow i) of two bit-vectors x and y

253

254

(defun binary-plus (i x y )

255

(if (and (bvp x) (<= 0 (bv-int-big-endian x))

256

(<= (bv-int-big-endian x) (expt 2 i))

257

(bvp y) (<= 0 (bv-int-big-endian y))

258

(<= (bv-int-big-endian y) (expt 2 i))

259

(integerp i) (<= 0 i))

260

(bv-to-n (int-bv-big-endian (mod (+ (bv-int-big-endian x)

261

(bv-int-big-endian y)) (expt 2 i))) i)

262

nil))

263

264

265

(defun plus-macro (i lst )

266

(if (and (consp lst) (integerp i) (<= 0 i))

267

(if (consp (cdr lst))

268

(list 'binary-plus i (car lst)

269

(plus-macro i (cdr lst) ))

270

(car lst))

271

nil))

272

273

(defmacro plus (i &rest args )

274

(plus-macro i args ))

275

276

;auxiliary shift operations

277

278

(defun << (x n w)

279

(if (and (wordp x w )

280

(integerp n)

281

(<= 0 n) (integerp w)

282

(<= 0 w)

283

(<= n w))

284

(cond ((zp n) x)

285

((endp x ) nil)

286

(t (append (nthcdr n x) (make-list n :initial-element 0) )))

287

nil))

288

289

;ACL2 !>(<< '(1 1 1 1) 2 4)

290

;(1 1 0 0)

291

292

293

(defun >> ( x n w)

294

(if (and (wordp x w)

295

(integerp n)

296

(<= 0 n)(integerp w)

297

(<= 0 w)

298

(<= n w))

299

(cond ((zp n) x)

300

((endp x ) nil)

301

(t (append (make-list n :initial-element 0) (firstn (- (len x) n) x) ) ))

302

nil))

303

304

;ACL2 !>(>> '(1 1 1 1) 2 4)

305

;(0 0 1 1)

306

307

;right shift of x with n elements on w bits

308

309

(defun shr (n x w)

310

(if (and (wordp x w)

311

(integerp n)

312

(<= 0 n)(integerp w)

313

(<= 0 w)

314

(<= n w))

315

(>> x n w) nil))

316

317

318

;rotate right (circular right shift) of x with n elements on w bits

319

320

(defun rotr (n x w)

321

(if (and (wordp x w)

322

(integerp n)

323

(<= 0 n)(integerp w)

324

(<= 0 w)

325

(<= n w))

326

(bv-or (>> x n w) (<< x (- w n) w)) nil))

327

328

;rotate left (circular left shift) of x with n elements on w bits

329

330

(defun rotl (n x w)

331

(if (and (wordp x w)

332

(integerp n)

333

(<= 0 n)(integerp w)

334

(<= 0 w)

335

(<= n w))

336

(bv-or (<< x n w) (>> x (- w n) w)) nil))

Older »