diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/constraint.cpp | 20 | ||||
-rw-r--r-- | src/theory/arith/constraint.h | 8 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 2 | ||||
-rw-r--r-- | src/theory/arith/options | 3 | ||||
-rw-r--r-- | src/theory/arith/options_handlers.h | 2 |
5 files changed, 17 insertions, 18 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index cf3aeafee..4655ea34e 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -371,8 +371,8 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) { d_database->pushAssertionOrderWatch(this, witness); } -// bool ConstraintValue::isPsuedoConstraint() const { -// return d_proof == d_database->d_psuedoConstraintProof; +// bool ConstraintValue::isPseudoConstraint() const { +// return d_proof == d_database->d_pseudoConstraintProof; // } bool ConstraintValue::isSelfExplaining() const { @@ -486,7 +486,7 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_equalityEngineProof = d_proofs.size(); d_proofs.push_back(NullConstraint); - // d_psuedoConstraintProof = d_proofs.size(); + // d_pseudoConstraintProof = d_proofs.size(); // d_proofs.push_back(NullConstraint); } @@ -833,11 +833,11 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){ } } -// void ConstraintValue::setPsuedoConstraint(){ +// void ConstraintValue::setPseudoConstraint(){ // Assert(truthIsUnknown()); // Assert(!hasLiteral()); -// d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof); +// d_database->pushProofWatch(this, d_database->d_pseudoConstraintProof); // } void ConstraintValue::setEqualityEngineProof(){ @@ -856,7 +856,7 @@ void ConstraintValue::markAsTrue(){ void ConstraintValue::markAsTrue(Constraint imp){ Assert(truthIsUnknown()); Assert(imp->hasProof()); - //Assert(!imp->isPsuedoConstraint()); + //Assert(!imp->isPseudoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(imp); @@ -868,8 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ Assert(truthIsUnknown()); Assert(impA->hasProof()); Assert(impB->hasProof()); - //Assert(!impA->isPsuedoConstraint()); - //Assert(!impB->isPsuedoConstraint()); + //Assert(!impA->isPseudoConstraint()); + //Assert(!impB->isPseudoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(impA); @@ -886,7 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){ for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ Constraint c_i = *i; Assert(c_i->hasProof()); - //Assert(!c_i->isPsuedoConstraint()); + //Assert(!c_i->isPseudoConstraint()); d_database->d_proofs.push_back(c_i); } @@ -903,7 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{ bool ConstraintValue::proofIsEmpty() const{ Assert(hasProof()); bool result = d_database->d_proofs[d_proof] == NullConstraint; - //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint()); + //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint()); Assert((!result) || isSelfExplaining() || hasEqualityEngineProof()); return result; } diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 52aa5a5ce..82023a48b 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -273,7 +273,7 @@ private: */ AssertionOrder _d_assertionOrder; /** - * This is guarenteed to be on the fact queue. + * This is guaranteed to be on the fact queue. * For example if x + y = x + 1 is on the fact queue, then use this */ TNode d_witness; @@ -491,8 +491,8 @@ public: * The explanation is the constant true. * explainInto() does nothing. */ - //void setPsuedoConstraint(); - //bool isPsuedoConstraint() const; + //void setPseudoConstraint(); + //bool isPseudoConstraint() const; /** * Returns a explanation of the constraint that is appropriate for conflicts. @@ -709,7 +709,7 @@ private: * * This is a special proof that is always a member of the list. */ - //ProofId d_psuedoConstraintProof; + //ProofId d_pseudoConstraintProof; typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList; typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList; diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 19a16d558..51c1e5138 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -249,7 +249,7 @@ public: } /** - * Computes a sufficient upperbound to seperate two DeltaRationals. + * Computes a sufficient upperbound to separate two DeltaRationals. * This value is stored in res. * For any rational d such that * 0 < d < res diff --git a/src/theory/arith/options b/src/theory/arith/options index 9e758a0ef..efe594766 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -60,7 +60,6 @@ option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds -/ turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds - +/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds endmodule diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h index 52e7cbf2a..f8f851964 100644 --- a/src/theory/arith/options_handlers.h +++ b/src/theory/arith/options_handlers.h @@ -52,7 +52,7 @@ This decides on kind of propagation arithmetic attempts to do during the search. "; static const std::string heuristicPivotRulesHelp = "\ -This decides on the rule used by simplex during hueristic rounds\n\ +This decides on the rule used by simplex during heuristic rounds\n\ for deciding the next basic variable to select.\n\ Heuristic pivot rules available:\n\ +min\n\ |