diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 10 |
5 files changed, 22 insertions, 22 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index c063245a5..bb6dfe40b 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -516,7 +516,7 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { } void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0); @@ -537,7 +537,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_SUB && node.getNumChildren() == 2 && bits.size() == 0); @@ -555,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_NEG); Bits a; @@ -633,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid } void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); Bits a, b; @@ -649,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); Bits a, b; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index a5a9b9a7e..24d6b300b 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_subtheory_eq_bitblast.cpp +/*! \file bv_subtheory_bitblast.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: dejan + ** Original author: dejan + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 0a8f046b7..324921f9a 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_subtheory_eq_bitblast.h +/*! \file bv_subtheory_bitblast.h ** \verbatim - ** Original author: lianah - ** Major contributors: dejan + ** Original author: dejan + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 8cbf99ae9..005be88a8 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_bv_rewrite_rules_core.h +/*! \file theory_bv_rewrite_rules_constant_evaluation.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): + ** Major contributors: barrett + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 506570ed2..48df9492d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_bv_rewrite_rules_core.h +/*! \file theory_bv_rewrite_rules_operator_elimination.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): + ** Major contributors: barrett + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -65,7 +65,7 @@ bool RewriteRule<SgtEliminate>::applies(TNode node) { template<> Node RewriteRule<SgtEliminate>::apply(TNode node) { - BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl; TNode a = node[0]; TNode b = node[1]; Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a); |