theory_bitvector.h File Reference

#include "theory_core.h"
#include "statistics.h"

Include dependency graph for theory_bitvector.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

• namespace CVC3

Classes

• class CVC3::TheoryBitvector

  Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG). More...
  

Enumerations

• enum CVC3::BVKinds {
    CVC3::BITVECTOR = 8000, CVC3::BVCONST, CVC3::CONCAT, CVC3::EXTRACT,
    CVC3::BOOLEXTRACT, CVC3::LEFTSHIFT, CVC3::CONST_WIDTH_LEFTSHIFT, CVC3::RIGHTSHIFT,
    CVC3::BVSHL, CVC3::BVLSHR, CVC3::BVASHR, CVC3::SX,
    CVC3::BVREPEAT, CVC3::BVZEROEXTEND, CVC3::BVROTL, CVC3::BVROTR,
    CVC3::BVAND, CVC3::BVOR, CVC3::BVXOR, CVC3::BVXNOR,
    CVC3::BVNEG, CVC3::BVNAND, CVC3::BVNOR, CVC3::BVCOMP,
    CVC3::BVUMINUS, CVC3::BVPLUS, CVC3::BVSUB, CVC3::BVMULT,
    CVC3::BVUDIV, CVC3::BVSDIV, CVC3::BVUREM, CVC3::BVSREM,
    CVC3::BVSMOD, CVC3::BVLT, CVC3::BVLE, CVC3::BVGT,
    CVC3::BVGE, CVC3::BVSLT, CVC3::BVSLE, CVC3::BVSGT,
    CVC3::BVSGE, CVC3::INTTOBV, CVC3::BVTOINT, CVC3::BVTYPEPRED
  }

Functions

• Rational CVC3::computeBVConst (const Expr &e)

  computes the integer value of a bitvector constant
  

---

Detailed Description

Author: Vijay Ganesh

Created: Wed May 05 18:34:55 PDT 2004

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file theory_bitvector.h.

---