diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-30 12:51:02 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:38 -0400 |
| commit | fddd187f540cee675368813c0c1d51711a02fdc0 (patch) | |
| tree | be6b4f6bdc731e13068d82cc31f32ccfa53bd4ab | |
| parent | 95028e5424d08d2c921e6bb77320685e7161e736 (diff) | |
Minor fixes, spelling etc.
| -rw-r--r-- | .mailmap | 2 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/options | 6 | ||||
| -rw-r--r-- | src/theory/valuation.h | 2 |
4 files changed, 8 insertions, 6 deletions
@@ -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; |