Skip to content

Commit 70af9ce

Browse files
Moving refined_string_type to util
This is a more appropriate location for this module since it's used both in the preprocessing of goto-programs and the string solver.
1 parent 3a2e210 commit 70af9ce

File tree

5 files changed

+5
-6
lines changed

5 files changed

+5
-6
lines changed

src/goto-programs/string_refine_preprocess.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,9 @@ Date: September 2016
1414
#include <util/pointer_offset_size.h>
1515
#include <util/prefix.h>
1616
#include <util/string_expr.h>
17+
#include <util/refined_string_type.h>
1718
#include <util/fresh_symbol.h>
1819
#include <goto-programs/class_identifier.h>
19-
// TODO: refined_string_type should be moved to util
20-
#include <solvers/refinement/refined_string_type.h>
2120
#include <java_bytecode/java_types.h>
2221

2322
#include "string_refine_preprocess.h"

src/solvers/refinement/string_constraint.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Romain Brenguier, [email protected]
1515

1616
#include <langapi/language_ui.h>
1717
#include <solvers/refinement/bv_refinement.h>
18-
#include <solvers/refinement/refined_string_type.h>
18+
#include <util/refined_string_type.h>
1919

2020
class string_constraintt: public exprt
2121
{

src/solvers/refinement/string_constraint_generator.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Romain Brenguier, [email protected]
1414
#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
1515

1616
#include <util/string_expr.h>
17-
#include <solvers/refinement/refined_string_type.h>
17+
#include <util/refined_string_type.h>
1818
#include <solvers/refinement/string_constraint.h>
1919

2020
class string_constraint_generatort

src/solvers/refinement/refined_string_type.h renamed to src/util/refined_string_type.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ Author: Romain Brenguier, [email protected]
1010
1111
\*******************************************************************/
1212

13-
#ifndef CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
14-
#define CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
13+
#ifndef CPROVER_UTIL_REFINED_STRING_TYPE_H
14+
#define CPROVER_UTIL_REFINED_STRING_TYPE_H
1515

1616
#include <util/std_types.h>
1717
#include <util/std_expr.h>

0 commit comments

Comments
 (0)