diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-16 15:15:03 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-13 18:32:39 -0400 |
commit | 14776d0aeb833a7e728a27af6ef545f20b495f7f (patch) | |
tree | eccc91e0be00cfb9af7d757aae3dd07479c256fb /src/theory/arith | |
parent | 09fc93244e10b4450592b4ede151873142d54b34 (diff) |
Documentation fixes, some code typo fixes, file perms, other minor things.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/approx_simplex.h | 4 | ||||
-rw-r--r-- | src/theory/arith/bound_counts.h | 17 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/options | 18 | ||||
-rw-r--r-- | src/theory/arith/simplex_update.h | 2 |
5 files changed, 30 insertions, 13 deletions
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 175e56f8e..a34c8981d 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -24,7 +24,7 @@ public: /** * If glpk is enabled, return a subclass that can do something. - * If glpk is disabled, return a sublass that does nothing. + * If glpk is disabled, return a subclass that does nothing. */ static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars); ApproximateSimplex(); @@ -52,7 +52,7 @@ public: virtual ApproxResult solveMIP() = 0; virtual Solution extractMIP() const = 0; - /** UTILIES FOR DEALING WITH ESTIMATES */ + /** UTILITIES FOR DEALING WITH ESTIMATES */ static const double SMALL_FIXED_DELTA; static const double TOLERENCE; diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 1ee6ada06..49c1a94ce 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file bound_counts.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 1ebbe49e0..7cd202e53 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -22,7 +22,7 @@ using namespace std; namespace CVC4 { -namespace theory{ +namespace theory { namespace arith { bool Variable::isDivMember(Node n){ diff --git a/src/theory/arith/options b/src/theory/arith/options index 57ef3d1b9..43b582bc8 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -56,7 +56,7 @@ option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bo turns on the preprocessing step of attempting to infer bounds on miplib problems /turns off the preprocessing step of attempting to infer bounds on miplib problems -option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned :default 1 +option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1 do substitution for miplib 'tmp' vars if defined in <= N eliminated vars option doCutAllBounded --cut-all-bounded bool :default false :read-write @@ -67,11 +67,11 @@ option maxCutsInContext --maxCutsInContext unsigned :default 65535 maximum cuts in a given context before signalling a restart option revertArithModels --revert-arith-models-on-unsat bool :default false - Revert the arithmetic model to a known safe model on unsat if one is cached + revert the arithmetic model to a known safe model on unsat if one is cached option havePenalties --fc-penalties bool :default false :read-write turns on degenerate pivot penalties -/ turns off degenerate pivot penalties +/turns off degenerate pivot penalties option useFC --use-fcsimplex bool :default false :read-write use focusing and converging simplex (FMCAD 2013 submission) @@ -80,25 +80,25 @@ option useSOI --use-soi bool :default false :read-write use sum of infeasibility simplex (FMCAD 2013 submission) option restrictedPivots --restrict-pivots bool :default true :read-write - have a pivot cap for simplex at effort levels below fullEffort. + have a pivot cap for simplex at effort levels below fullEffort option collectPivots --collect-pivot-stats bool :default false :read-write collect the pivot history option fancyFinal --fancy-final bool :default false :read-write - Tuning how final check works for really hard problems. + tuning how final check works for really hard problems option exportDioDecompositions --dio-decomps bool :default false :read-write - Let skolem variables for integer divisibility constraints leak from the dio solver. + let skolem variables for integer divisibility constraints leak from the dio solver option newProp --new-prop bool :default false :read-write - Use the new row propagation system + use the new row propagation system option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write - Rows shorter than this are propagated as clauses + rows shorter than this are propagated as clauses option soiQuickExplain --soi-qe bool :default false :read-write - Use quick explain to minimize the sum of infeasibility conflicts. + use quick explain to minimize the sum of infeasibility conflicts option rewriteDivk rewrite-divk --rewrite-divk bool :default false rewrite division and mod when by a constant into linear terms diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 516586568..64aa193dd 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -318,7 +318,7 @@ private: } /** - * Determines the appropraite WitnessImprovement for the update. + * Determines the appropriate WitnessImprovement for the update. * useBlands breaks ties for degenerate pivots. * * This is safe if: |