diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-04-01 08:16:22 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-04-01 08:24:46 -0500 |
| commit | 3fd6359ae7ea9137133d61f20ac7e43668cd7bab (patch) | |
| tree | f9242ea3ff657da46267cf8ac0fffa6708ef4010 /src/theory | |
| parent | 9af3f271937cb9389f8e5b8f1b302f48bc6cdd9a (diff) | |
windows build fix for UINT32_MAX
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 5 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 9 |
2 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 3167734ee..1b040f71c 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -18,6 +18,7 @@ #include "expr/kind.h" #include "theory/strings/options.h" #include "smt/logic_exception.h" +#include <stdint.h> namespace CVC4 { namespace theory { @@ -248,11 +249,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero); if(t.getKind()==kind::STRING_U16TOS) { - nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(65536) ), t[0])); + nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0])); Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp); new_nodes.push_back(lencond); } else if(t.getKind()==kind::STRING_U32TOS) { - nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(4294967296) ), t[0])); + nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0])); Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp); new_nodes.push_back(lencond); } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 8a603e6df..f6de1b129 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -16,6 +16,7 @@ #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/options.h" #include "smt/logic_exception.h" +#include <stdint.h> using namespace std; using namespace CVC4; @@ -481,13 +482,13 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { bool flag = false; std::string stmp = node[0].getConst<Rational>().getNumerator().toString(); if(node.getKind() == kind::STRING_U16TOS) { - CVC4::Rational r1(65536); + CVC4::Rational r1(UINT16_MAX); CVC4::Rational r2 = node[0].getConst<Rational>(); if(r2>r1) { flag = true; } } else if(node.getKind() == kind::STRING_U32TOS) { - CVC4::Rational r1(4294967296); + CVC4::Rational r1(UINT32_MAX); CVC4::Rational r2 = node[0].getConst<Rational>(); if(r2>r1) { flag = true; @@ -512,12 +513,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { bool flag = false; CVC4::Rational r2(stmp.c_str()); if(node.getKind() == kind::STRING_U16TOS) { - CVC4::Rational r1(65536); + CVC4::Rational r1(UINT16_MAX); if(r2>r1) { flag = true; } } else if(node.getKind() == kind::STRING_U32TOS) { - CVC4::Rational r1(4294967296); + CVC4::Rational r1(UINT32_MAX); if(r2>r1) { flag = true; } |