CVC3  2.4.1
theory_bitvector Directory Reference

Files

file  bitvector_exception.h [code]
 An exception thrown by the bitvector decision procedure.
 
file  bitvector_expr_value.h [code]
 Subclasses of ExprValue for bit-vector expressions.
 
file  bitvector_proof_rules.h [code]
 Arithmetic proof rules.
 
file  bitvector_theorem_producer.cpp [code]
 
file  bitvector_theorem_producer.h [code]
 TRUSTED implementation of bitvector proof rules.
 
file  theory_bitvector.cpp [code]