diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-03 17:13:31 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 17:55:53 -0500 |
| commit | a97891f9cc892fdc261cd4e3d3229ec68f05b45e (patch) | |
| tree | a05c30ddbe81d9dd084a2e024875f829d6f1f3a7 /src/theory/arith | |
| parent | b28a42c3a4fd8c9b079b157ad8ff36e581b60d29 (diff) | |
General pre-release cleanup commit
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
Diffstat (limited to 'src/theory/arith')
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.h | 2 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 1 |
3 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 9d13dccb7..aa2b2a557 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -63,7 +63,7 @@ #include "theory/arith/constraint.h" #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arith/options.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 22fc8d4a7..86de3c1a9 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -71,7 +71,7 @@ #include "theory/arith/constraint.h" #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arith/options.h" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 45e18fe0d..0d3a578a6 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -100,7 +100,6 @@ public: if( check ) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isReal()) { - Message() << lhsType << " : " << n[0] << std::endl; throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); } TypeNode rhsType = n[1].getType(check); |