windows build fix for UINT32_MAX

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 3167734ee4a987203b1298d23383f50c381ccde8..1b040f71c1d75b7706df1bfd913e7dee79cd7b5d 100644 (file)
--- 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 8a603e6df62962b72e2b2da30d8fe859cf436a0c..f6de1b129b2a772866cd10b3f201fb680a5c2f55 100644 (file)
--- 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;
                                                }