summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-07-29 16:08:45 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-07-29 16:08:45 -0400
commitda9eec6aa0fc0f6c29f2c3fdb08bd45ba9c27808 (patch)
treedca1b2fb1d1c213a94d5b2902aed4a24895aae3f /src/theory/bv
parentbc3db83a6856016c9c838fbabdd29f962aa60769 (diff)
Fix numerous compiler warnings on various platforms
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/bitblaster.cpp4
-rw-r--r--src/theory/bv/bitblaster.h3
2 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 47aac4370..d17dd588f 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -178,7 +178,7 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
}
-/**
+/*
* Asserts the clauses corresponding to the atom to the Sat Solver
* by turning on the marker literal (i.e. setting it to false)
* @param node the atom to be asserted
@@ -444,6 +444,8 @@ bool Bitblaster::hasValue(TNode a) {
* or null if the value is completely unassigned.
*
* @param a
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
*
* @return
*/
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 83efc05b0..6fab0369c 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -152,13 +152,14 @@ public:
* Adds a constant value for each bit-blasted variable in the model.
*
* @param m the model
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
*/
void collectModelInfo(TheoryModel* m, bool fullModel);
/**
* Stores the variable (or non-bv term) and its corresponding bits.
*
* @param var
- * @param bits
*/
void storeVariable(TNode var) {
d_variables.insert(var);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback