From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 1 Apr 2014 13:16:22 +0000 (-0500)
Subject: windows build fix for UINT32_MAX
X-Git-Tag: cvc5-1.0.0~6989
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3fd6359ae7ea9137133d61f20ac7e43668cd7bab;p=cvc5.git

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 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;
 						}