Fix several spelling errors (#2231)

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index c0946c86a3ded7c7fe8aabc193aa7ba8248cab33..7bfe8d59286a52c816a72b46fd15a319375df61e 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -501,7 +501,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "intial splits on zero for all variables"
+  help       = "initial splits on zero for all variables"
 
 [[option]]
   name       = "nlExtTfTaylorDegree"

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 8d71e2f65a964f39472d204af899ab83e7b4e3c9..740c2e5e675b6f008d0a3fb864a3e0925cb53afd 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -138,7 +138,7 @@ Solver::Solver(CVC4::context::Context* c) :
   , ca                 ()
 
   // even though these are temporaries and technically should be set
-  // before calling, lets intialize them. this will reduces chances of
+  // before calling, lets initialize them. this will reduces chances of
   // non-determinism in portfolio (parallel) solver if variables are
   // being (incorrectly) used without initialization.
   , seen(),  analyze_stack(), analyze_toclear(), add_tmp()

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 748bf12da27843a6d04cb1d4722e36973b2fa066..c33e2c6b7d8346dc09cdbd877de2ccb9e9edc872 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -173,7 +173,7 @@ class FirstOrderModel : public TheoryModel
   std::map<Node, std::map<Node, int> > d_quant_var_id;
   /** process initialize model for term */
   virtual void processInitializeModelForTerm(Node n) = 0;
-  /** process intialize quantifier */
+  /** process initialize quantifier */
   virtual void processInitializeQuantifier(Node q) {}
   /** process initialize */
   virtual void processInitialize(bool ispre) = 0;

diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index f094b94907db4be5adb362302b0b3b0fcd21b3bc..ce4186eb27264fd1fbf369874818e6b126e52087 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -77,7 +77,7 @@ class Cegis : public SygusModule
    */
   Node d_base_body;
   //----------------------------------cegis-implementation-specific
-  /** do cegis-implementation-specific intialization for this class */
+  /** do cegis-implementation-specific initialization for this class */
   virtual bool processInitialize(Node n,
                                  const std::vector<Node>& candidates,
                                  std::vector<Node>& lemmas);

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 48fca53f57e5ab3a8f41ac02245a7afe107bbd20..858a83bce5d83583e60aeb36de071da2dccb6558 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -236,7 +236,7 @@ class CegisUnif : public Cegis
   Node getNextDecisionRequest(unsigned& priority) override;
 
  private:
-  /** do cegis-implementation-specific intialization for this class */
+  /** do cegis-implementation-specific initialization for this class */
   bool processInitialize(Node n,
                          const std::vector<Node>& candidates,
                          std::vector<Node>& lemmas) override;

diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index 4efc171d330f2a399987eed877d4dabbfcfd13c0..3f18a65d649873b9c94385674199c1d7d19ee81a 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -65,7 +65,7 @@ class TermRecBuild
   /** get the i^th child of the active term */
   Node getChild(unsigned i);
   /** build the (modified) version of the term
-   * we intialized via the call to init().
+   * we initialized via the call to init().
    */
   Node build(unsigned p = 0);
 

diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 0134b3a86c652cc5dde67f0eba0db98a0d1fea7d..f90c6ebd0a534be5e48469853cf7ddc22374efac 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -50,7 +50,7 @@ namespace quantifiers {
  * For example, say the grammar for f is:
  *   A = 0 | 1 | x | y | A+A | ite( B, A, A )
  *   B = A <= A
- * If we call intialize( tds, f, 5 ), this class will generate 5 random sample
+ * If we call initialize( tds, f, 5 ), this class will generate 5 random sample
  * points for (x,y), say (0,0), (1,1), (0,1), (1,0), (2,2). The return values
  * of successive calls to registerTerm are listed below.
  *   registerTerm( 0 ) -> 0
@@ -281,7 +281,7 @@ class SygusSampler : public LazyTrieEvaluator
   std::map<Node, std::vector<TypeNode> > d_var_sygus_types;
   /** map from constants to sygus types that include them */
   std::map<Node, std::vector<TypeNode> > d_const_sygus_types;
-  /** register sygus type, intializes the above two data structures */
+  /** register sygus type, initializes the above two data structures */
   void registerSygusType(TypeNode tn);
 };