From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 30 Apr 2014 16:51:02 +0000 (-0400)
Subject: Minor fixes, spelling etc.
X-Git-Tag: cvc5-1.0.0~6799
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fddd187f540cee675368813c0c1d51711a02fdc0;p=cvc5.git

Minor fixes, spelling etc.
---

diff --git a/.mailmap b/.mailmap
index 1560f0272..7cf2a12f0 100644
--- a/.mailmap
+++ b/.mailmap
@@ -5,6 +5,8 @@ Dejan Jovanovic <dejan@cs.nyu.edu> <dejan.jovanovic@gmail.com>
 Francois Bobot <francois@bobot.eu> <francois@bobot.eu>
 Liana Hadarean <lianah@cs.nyu.edu> <lianahady@gmail.com>
 Andrew Reynolds <andrew.j.reynolds@gmail.com> <andrew.j.reynolds@gmail.com>
+Andrew Reynolds <andrew.j.reynolds@gmail.com> <reynolds@laraserver2.epfl.ch>
+Andrew Reynolds <andrew.j.reynolds@gmail.com> <reynolds@larapc05.epfl.ch>
 Cesare Tinelli <cesare-tinelli@uiowa.edu> <cesare-tinelli@uiowa.edu>
 Christopher L. Conway <christopherleeconway@gmail.com> <christopherleeconway@gmail.com>
 Clark Barrett <barrett@cs.nyu.edu> <barrett@cs.nyu.edu>
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 26ed8c296..683f002cf 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -105,7 +105,7 @@ private:
 
 
   /**
-   * Return the uinterpreted function symbol corresponding to division-by-zero
+   * Return the uninterpreted function symbol corresponding to division-by-zero
    * for this particular bit-width
    * @param k should be UREM or UDIV
    * @param width
@@ -121,7 +121,7 @@ private:
   NodeSet d_staticLearnCache;
   
   /**
-   * Maps from bit-vector width to divison-by-zero uninterpreted
+   * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
    */
   __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f8f1744ed..1cdf5e8bd 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -72,10 +72,10 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de
  when to apply instantiation
 option instMaxLevel --inst-max-level=N int :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
- 
+
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
- 
+
 option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 
@@ -105,7 +105,7 @@ option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :def
 option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for mbqi
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
- only add instantiations for one quantifier per round for mbqi 
+ only add instantiations for one quantifier per round for mbqi
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 2462896c7..a9d276f42 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -66,7 +66,7 @@ public:
     d_engine(engine) {
   }
 
-  /*
+  /**
    * Return true if n has an associated SAT literal
    */
   bool isSatLiteral(TNode n) const;