diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-18 12:11:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-18 12:11:50 -0500 |
| commit | 6f18015fdcb824f46b969882aa45187b46306e97 (patch) | |
| tree | 8d04dcb3fa263a359886aa156851d4dec3e2c7e8 /src/parser | |
| parent | 382813c77025e05550876bf02f2782b72d6c8927 (diff) | |
Strings API escape sequences (#1245)
* Argument for strings class to specify whether to process escape sequences.
* Change default value on string constructor.
* Make CVC4::String::toString symmetric to the constructor for CVC4::String, document.
* Clang format.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 2 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index eef7ca54d..6337fb5f6 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1978,7 +1978,7 @@ stringTerm[CVC4::Expr& f] /* string literal */ | str[s] - { f = MK_CONST(CVC4::String(s)); } + { f = MK_CONST(CVC4::String(s, true)); } | setsTerm[f] ; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ce1cd1fbd..05faf040e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1031,7 +1031,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] | str[s,false] { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl; - sgt.d_expr = MK_CONST( ::CVC4::String(s) ); + sgt.d_expr = MK_CONST( ::CVC4::String(s, true) ); sgt.d_name = s; sgt.d_gterm_type = SygusGTerm::gterm_op; } @@ -2328,7 +2328,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_CONST( BitVector(binString, 2) ); } | str[s,false] - { expr = MK_CONST( ::CVC4::String(s) ); } + { expr = MK_CONST( ::CVC4::String(s, true) ); } | FP_RNE_TOK { expr = MK_CONST(roundNearestTiesToEven); } | FP_RNA_TOK { expr = MK_CONST(roundNearestTiesToAway); } | FP_RTP_TOK { expr = MK_CONST(roundTowardPositive); } |