From b2d5fd3f11c68797bbaeb9024414fb1ece2a9c56 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 30 Apr 2014 12:51:02 -0400 Subject: [PATCH] Minor fixes, spelling etc. --- .mailmap | 2 ++ src/theory/bv/theory_bv.h | 4 ++-- src/theory/quantifiers/options | 6 +++--- src/theory/valuation.h | 2 +- 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/.mailmap b/.mailmap index 1560f0272..7cf2a12f0 100644 --- a/.mailmap +++ b/.mailmap @@ -5,6 +5,8 @@ Dejan Jovanovic Francois Bobot Liana Hadarean Andrew Reynolds +Andrew Reynolds +Andrew Reynolds Cesare Tinelli Christopher L. Conway Clark Barrett 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 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; -- 2.30.2