From 49e18991f04032e1b0c266aa768ef767b5bc2b1d Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 1 Apr 2014 08:16:22 -0500 Subject: [PATCH] windows build fix for UINT32_MAX --- src/theory/strings/theory_strings_preprocess.cpp | 5 +++-- 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 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 using namespace std; using namespace CVC4; @@ -481,13 +482,13 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { bool flag = false; std::string stmp = node[0].getConst().getNumerator().toString(); if(node.getKind() == kind::STRING_U16TOS) { - CVC4::Rational r1(65536); + CVC4::Rational r1(UINT16_MAX); CVC4::Rational r2 = node[0].getConst(); 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(); 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; } -- 2.30.2