From a0197709888f34c2fcf786ee72a054e327c2847d Mon Sep 17 00:00:00 2001 From: ntsis Date: Wed, 1 Nov 2023 11:48:35 -0700 Subject: [PATCH] Add partial string support (#327) Added string support for StrLt "str.<", StrLeq "str.<=", StrLen "str.len", StrConcat, "str.++". --- cvc5/include/cvc5_solver.h | 4 +- cvc5/include/cvc5_term.h | 1 + cvc5/src/cvc5_solver.cpp | 65 ++++++++++- cvc5/src/cvc5_sort.cpp | 4 + cvc5/src/cvc5_term.cpp | 7 ++ include/logging_solver.h | 2 + include/logging_term.h | 1 + include/ops.h | 5 + include/printing_solver.h | 3 + include/smtlibparser_maps.h | 6 + include/solver.h | 23 ++++ include/solver_enums.h | 2 + include/sort.h | 1 + include/sort_inference.h | 4 + include/term.h | 5 + src/logging_solver.cpp | 41 ++++++- src/logging_sort.cpp | 5 +- src/logging_term.cpp | 5 + src/ops.cpp | 8 ++ src/printing_solver.cpp | 9 ++ src/smtlib_reader.cpp | 6 +- src/smtlibparser.yy | 8 ++ src/solver_enums.cpp | 2 + src/sort.cpp | 5 + src/sort_inference.cpp | 19 ++++ src/term_translator.cpp | 37 ++++-- tests/CMakeLists.txt | 1 + tests/cvc5/CMakeLists.txt | 1 + tests/cvc5/cvc5-str.cpp | 69 ++++++++++++ tests/cvc5/cvc5_test.cpp | 17 +++ tests/smt2/qf_s/test-ops-SLIA.smt2 | 29 +++++ tests/smt2/qf_s/test-ops.smt2 | 9 ++ tests/smtlib_reader_test_inputs.h | 5 + tests/test-smtlib-reader.cpp | 33 ++++++ tests/test-str.cpp | 174 +++++++++++++++++++++++++++++ 35 files changed, 599 insertions(+), 17 deletions(-) create mode 100644 tests/cvc5/cvc5-str.cpp create mode 100644 tests/smt2/qf_s/test-ops-SLIA.smt2 create mode 100644 tests/smt2/qf_s/test-ops.smt2 create mode 100644 tests/test-str.cpp diff --git a/cvc5/include/cvc5_solver.h b/cvc5/include/cvc5_solver.h index 387f36e58..bca191046 100644 --- a/cvc5/include/cvc5_solver.h +++ b/cvc5/include/cvc5_solver.h @@ -100,6 +100,8 @@ class Cvc5Solver : public AbsSmtSolver Term make_term(bool b) const override; Term make_term(int64_t i, const Sort & sort) const override; + Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const override; + Term make_term(const std::wstring& s, const Sort & sort) const override; Term make_term(const std::string val, const Sort & sort, uint64_t base = 10) const override; @@ -127,7 +129,7 @@ class Cvc5Solver : public AbsSmtSolver // getters for solver-specific objects // for interacting with third-party cvc5-specific software ::cvc5::Solver & get_cvc5_solver() { return solver; }; - + protected: ::cvc5::Solver solver; diff --git a/cvc5/include/cvc5_term.h b/cvc5/include/cvc5_term.h index 78763b7cf..6e6ecb44b 100644 --- a/cvc5/include/cvc5_term.h +++ b/cvc5/include/cvc5_term.h @@ -64,6 +64,7 @@ class Cvc5Term : public AbsTerm bool is_symbolic_const() const override; bool is_value() const override; virtual std::string to_string() override; + virtual std::wstring getStringValue() const override; uint64_t to_int() const override; /** Iterators for traversing the children */ diff --git a/cvc5/src/cvc5_solver.cpp b/cvc5/src/cvc5_solver.cpp index acc3a42b3..c31698ced 100644 --- a/cvc5/src/cvc5_solver.cpp +++ b/cvc5/src/cvc5_solver.cpp @@ -92,8 +92,13 @@ const std::unordered_map primop2kind( { Rotate_Right, ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT }, // Conversion { BV_To_Nat, ::cvc5::Kind::BITVECTOR_TO_NAT }, - // Indexed Op { Int_To_BV, ::cvc5::Kind::INT_TO_BITVECTOR }, + // String Op + { StrLt, ::cvc5::Kind::STRING_LT }, + { StrLeq, ::cvc5::Kind::STRING_LEQ }, + { StrLen, ::cvc5::Kind::STRING_LENGTH }, + { StrConcat, ::cvc5::Kind::STRING_CONCAT }, + // Indexed Op { Select, ::cvc5::Kind::SELECT }, { Store, ::cvc5::Kind::STORE }, { Forall, ::cvc5::Kind::FORALL }, @@ -163,7 +168,7 @@ Term Cvc5Solver::make_term(int64_t i, const Sort & sort) const else if (sk == REAL) { c = solver.mkReal(i); - } + } else if (sk == BV) { // cvc5 uses unsigned integers for mkBitVector @@ -187,6 +192,58 @@ Term Cvc5Solver::make_term(int64_t i, const Sort & sort) const } } +Term Cvc5Solver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const +{ + try + { + SortKind sk = sort->get_sort_kind(); + ::cvc5::Term c; + + if (sk == STRING) + { + c = solver.mkString(s, useEscSequences); + } + else + { + std::string msg = "Can't create a string constant for sort "; + msg += sort->to_string(); + throw IncorrectUsageException(msg.c_str()); + } + + return std::make_shared(c); + } + catch (::cvc5::CVC5ApiException & e) + { + throw IncorrectUsageException(e.what()); + } +} + +Term Cvc5Solver::make_term(const std::wstring& s, const Sort & sort) const +{ + try + { + SortKind sk = sort->get_sort_kind(); + ::cvc5::Term c; + + if (sk == STRING) + { + c = solver.mkString(s); + } + else + { + std::string msg = "Can't create string constant for sort "; + msg += sort->to_string(); + throw IncorrectUsageException(msg.c_str()); + } + + return std::make_shared(c); + } + catch (::cvc5::CVC5ApiException & e) + { + throw IncorrectUsageException(e.what()); + } +} + Term Cvc5Solver::make_term(std::string val, const Sort & sort, uint64_t base) const @@ -478,6 +535,10 @@ Sort Cvc5Solver::make_sort(SortKind sk) const { return std::make_shared(solver.getRealSort()); } + else if (sk == STRING) + { + return std::make_shared(solver.getStringSort()); + } else { std::string msg("Can't create sort with sort constructor "); diff --git a/cvc5/src/cvc5_sort.cpp b/cvc5/src/cvc5_sort.cpp index 732eedb10..c33d4b349 100644 --- a/cvc5/src/cvc5_sort.cpp +++ b/cvc5/src/cvc5_sort.cpp @@ -126,6 +126,10 @@ SortKind Cvc5Sort::get_sort_kind() const { return REAL; } + else if (sort.isString()) + { + return STRING; + } else if (sort.isArray()) { return ARRAY; diff --git a/cvc5/src/cvc5_term.cpp b/cvc5/src/cvc5_term.cpp index dc3a5cd66..76630a6ff 100644 --- a/cvc5/src/cvc5_term.cpp +++ b/cvc5/src/cvc5_term.cpp @@ -104,6 +104,11 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop( { ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT, Rotate_Right }, // Conversion { ::cvc5::Kind::BITVECTOR_TO_NAT, BV_To_Nat }, + // String Op + { ::cvc5::Kind::STRING_LT, StrLt }, + { ::cvc5::Kind::STRING_LEQ, StrLeq }, + { ::cvc5::Kind::STRING_LENGTH, StrLen }, + { ::cvc5::Kind::STRING_CONCAT, StrConcat }, // Indexed Op { ::cvc5::Kind::INT_TO_BITVECTOR, Int_To_BV }, { ::cvc5::Kind::SELECT, Select }, @@ -282,6 +287,8 @@ bool Cvc5Term::is_value() const std::string Cvc5Term::to_string() { return term.toString(); } +std::wstring Cvc5Term::getStringValue() const { return term.getStringValue(); } + uint64_t Cvc5Term::to_int() const { std::string val = term.toString(); diff --git a/include/logging_solver.h b/include/logging_solver.h index 72d4c5c1f..3311ad05d 100644 --- a/include/logging_solver.h +++ b/include/logging_solver.h @@ -57,6 +57,8 @@ class LoggingSolver : public AbsSmtSolver Term make_term(bool b) const override; Term make_term(int64_t i, const Sort & sort) const override; + Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const override; + Term make_term(const std::wstring& s, const Sort & sort) const override; Term make_term(const std::string val, const Sort & sort, uint64_t base = 10) const override; diff --git a/include/logging_term.h b/include/logging_term.h index 79de5210f..e602133dd 100644 --- a/include/logging_term.h +++ b/include/logging_term.h @@ -45,6 +45,7 @@ class LoggingTerm : public AbsTerm Op get_op() const override; Sort get_sort() const override; std::string to_string() override; + std::wstring getStringValue() const override; bool is_symbol() const override; bool is_param() const override; bool is_symbolic_const() const override; diff --git a/include/ops.h b/include/ops.h index d759f58b8..f3bae641a 100644 --- a/include/ops.h +++ b/include/ops.h @@ -98,6 +98,11 @@ enum PrimOp // BitVector Conversion BV_To_Nat, Int_To_BV, + // Strings + StrLt, + StrLeq, + StrLen, + StrConcat, /* Array Theory */ Select, Store, diff --git a/include/printing_solver.h b/include/printing_solver.h index fc8165cdd..9e17a9ed0 100644 --- a/include/printing_solver.h +++ b/include/printing_solver.h @@ -97,6 +97,9 @@ class PrintingSolver : public AbsSmtSolver Term make_term(bool b) const override; Term make_term(int64_t i, const Sort & sort) const override; + Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const override; + Term make_term(const std::wstring& s, const Sort & sort) const override; + Term make_term(const std::string val, const Sort & sort, uint64_t base = 10) const override; diff --git a/include/smtlibparser_maps.h b/include/smtlibparser_maps.h index ace7d7175..0c2f72380 100644 --- a/include/smtlibparser_maps.h +++ b/include/smtlibparser_maps.h @@ -96,6 +96,12 @@ const std::unordered_map> { "repeat", Repeat }, { "rotate_left", Rotate_Left }, { "rotate_right", Rotate_Right } } }, + // Strings + { "S", + { { "str.<", StrLt }, + { "str.<=", StrLeq}, + { "str.len", StrLen}, + { "str.++", StrConcat} } }, // ArraysEx { "A", { diff --git a/include/solver.h b/include/solver.h index cb04200ef..98317fd3b 100644 --- a/include/solver.h +++ b/include/solver.h @@ -210,6 +210,29 @@ class AbsSmtSolver */ virtual Term make_term(int64_t i, const Sort & sort) const = 0; + /* Make a string value term from an `std::string` which may contain SMT-LIB compatible + * escape sequences like `\u1000` or `\u{20}` to encode unicode characters. + * @param s is the value + * @param useEscSequences determines whether escape sequence in `s` should + * be converted to the corresponding unicode character + * @param sort the sort to create + * @return a value term with Sort sort and value s + */ + + virtual Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const{ + throw NotImplementedException("Strings not supported for this solver."); + } + + /* Make a string value term + * @param s is the value + * @param sort the sort to create + * @return a value term with Sort sort and value s + */ + virtual Term make_term(const std::wstring& s, const Sort & sort) const{ + throw NotImplementedException("Strings not supported for this solver."); + } + + /* Make a bit-vector, int, real or (in the future) string value term * @param val the numeric value as a string, or a string value * @param sort the sort to create diff --git a/include/solver_enums.h b/include/solver_enums.h index 74b52b713..ec4c39404 100644 --- a/include/solver_enums.h +++ b/include/solver_enums.h @@ -50,6 +50,8 @@ enum SolverAttribute THEORY_INT, // supports real theory THEORY_REAL, + // supports STR theory + THEORY_STR, // supports array models ARRAY_MODELS, // supports constant arrays diff --git a/include/sort.h b/include/sort.h index f291bae12..a3391dcbe 100644 --- a/include/sort.h +++ b/include/sort.h @@ -38,6 +38,7 @@ enum SortKind BV, INT, REAL, + STRING, FUNCTION, UNINTERPRETED, // an uninterpreted sort constructor (has non-zero arity and takes subsort diff --git a/include/sort_inference.h b/include/sort_inference.h index 32f67cbed..638753788 100644 --- a/include/sort_inference.h +++ b/include/sort_inference.h @@ -173,6 +173,8 @@ bool real_sorts(const SortVec & sorts); bool int_sorts(const SortVec & sorts); +bool string_sorts(const SortVec & sorts); + bool arithmetic_sorts(const SortVec & sorts); bool array_sorts(const SortVec & sorts); @@ -191,6 +193,8 @@ Sort real_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts); Sort int_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts); +Sort string_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts); + Sort ite_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts); Sort extract_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts); diff --git a/include/term.h b/include/term.h index 897d76533..4674bc6f0 100644 --- a/include/term.h +++ b/include/term.h @@ -27,6 +27,7 @@ #include "ops.h" #include "smt_defs.h" #include "sort.h" +#include "exceptions.h" namespace smt { @@ -51,6 +52,10 @@ class AbsTerm virtual Sort get_sort() const = 0; /* to_string in smt2 format */ virtual std::string to_string() = 0; + /* returns the string term as a native string value */ + virtual std::wstring getStringValue() const{ + throw NotImplementedException("Strings not supported for this solver."); + } /* returns true iff this term is a symbol */ virtual bool is_symbol() const = 0; /* returns true iff this term is a parameter (to be bound by a quantifier) */ diff --git a/src/logging_solver.cpp b/src/logging_solver.cpp index b5ec337f7..614a8866f 100644 --- a/src/logging_solver.cpp +++ b/src/logging_solver.cpp @@ -34,7 +34,7 @@ namespace smt { have no Op or children */ const unordered_set supported_sortkinds_for_get_value( - { BOOL, BV, INT, REAL, ARRAY }); + { BOOL, BV, INT, STRING, REAL, ARRAY }); /* LoggingSolver */ @@ -205,6 +205,45 @@ Term LoggingSolver::make_term(int64_t i, const Sort & sort) const return res; } +Term LoggingSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const +{ + shared_ptr lsort = static_pointer_cast(sort); + Term wrapped_res = wrapped_solver->make_term(s, useEscSequences, lsort->wrapped_sort); + Term res = std::make_shared( + wrapped_res, sort, Op(), TermVec{}, next_term_id); + + // check hash table + // lookup modifies term in place and returns true if it's a known term + // i.e. returns existing term and destroying the unnecessary new one + if (!hashtable->lookup(res)) + { + // this is the first time this term was created + hashtable->insert(res); + next_term_id++; + } + + return res; +} + +Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{ + shared_ptr lsort = static_pointer_cast(sort); + Term wrapped_res = wrapped_solver->make_term(s, lsort->wrapped_sort); + Term res = std::make_shared( + wrapped_res, sort, Op(), TermVec{}, next_term_id); + + // check hash table + // lookup modifies term in place and returns true if it's a known term + // i.e. returns existing term and destroying the unnecessary new one + if (!hashtable->lookup(res)) + { + // this is the first time this term was created + hashtable->insert(res); + next_term_id++; + } + + return res; +} + Term LoggingSolver::make_term(const string name, const Sort & sort, uint64_t base) const diff --git a/src/logging_sort.cpp b/src/logging_sort.cpp index 723998c60..2985b6bfd 100644 --- a/src/logging_sort.cpp +++ b/src/logging_sort.cpp @@ -37,7 +37,7 @@ Sort make_uninterpreted_logging_sort(Sort s, Sort make_logging_sort(SortKind sk, Sort s) { - if (sk != BOOL && sk != INT && sk != REAL) + if (sk != BOOL && sk != INT && sk != REAL && sk != STRING) { throw IncorrectUsageException("Can't create sort from " + to_string(sk)); } @@ -135,7 +135,8 @@ bool LoggingSort::compare(const Sort & s) const { case BOOL: case INT: - case REAL: { return true; + case REAL: + case STRING: { return true; } case BV: { return get_width() == s->get_width(); } diff --git a/src/logging_term.cpp b/src/logging_term.cpp index d64a2f9b1..3514285bf 100644 --- a/src/logging_term.cpp +++ b/src/logging_term.cpp @@ -164,6 +164,11 @@ string LoggingTerm::to_string() } } +wstring LoggingTerm::getStringValue() const +{ + return wrapped_term->getStringValue(); +} + bool LoggingTerm::is_symbol() const { // functions, parameters, and symbolic constants are all symbols diff --git a/src/ops.cpp b/src/ops.cpp index 340bc2e4b..2148aa1df 100644 --- a/src/ops.cpp +++ b/src/ops.cpp @@ -85,6 +85,10 @@ const std::unordered_map primop2str( { Rotate_Right, "rotate_right" }, { BV_To_Nat, "bv2nat" }, { Int_To_BV, "int2bv" }, + { StrLt, "str.<"}, + { StrLeq, "str.<="}, + { StrLen, "str.len"}, + { StrConcat, "str.++"}, { Select, "select" }, { Store, "store" }, { Forall, "forall" }, @@ -167,6 +171,10 @@ const std::unordered_map> primop2arity( { Rotate_Right, { 1, 1 } }, { BV_To_Nat, { 1, 1 } }, { Int_To_BV, { 1, 1 } }, + { StrLt, { 2, 2} }, + { StrLeq, { 2, 2} }, + { StrLen, { 1, 1} }, + { StrConcat, { 2, INT_MAX} }, { Select, { 2, 2 } }, { Store, { 3, 3 } }, // to make term traversal easier considering the differences diff --git a/src/printing_solver.cpp b/src/printing_solver.cpp index 5589851f3..db1d3a8aa 100644 --- a/src/printing_solver.cpp +++ b/src/printing_solver.cpp @@ -130,6 +130,15 @@ Term PrintingSolver::make_term(int64_t i, const Sort & sort) const return wrapped_solver->make_term(i, sort); } +Term PrintingSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const +{ + return wrapped_solver->make_term(s, useEscSequences, sort); +} +Term PrintingSolver::make_term(const std::wstring& s, const Sort & sort) const +{ + return wrapped_solver->make_term(s, sort); +} + Term PrintingSolver::make_term(const string name, const Sort & sort, uint64_t base) const diff --git a/src/smtlib_reader.cpp b/src/smtlib_reader.cpp index 1988f6daf..6953877e0 100644 --- a/src/smtlib_reader.cpp +++ b/src/smtlib_reader.cpp @@ -37,7 +37,8 @@ const unordered_map> logic_theory_map( { "NIRA", { "IA", "RA", "IRA" } }, { "NRA", { "RA" } }, { "RDL", { "RA" } }, - { "UF", { "UF" } } }); + { "UF", { "UF" } }, + { "S", { "S" } } }); // maps logic string to vector of associated SortKinds for that logic const unordered_map> logic_sortkind_map( @@ -52,7 +53,8 @@ const unordered_map> logic_sortkind_map( { "NIRA", { INT, REAL } }, { "NRA", { REAL } }, { "RDL", { REAL } }, - { "UF", { FUNCTION } } }); + { "UF", { FUNCTION } }, + { "S", { STRING } } }); SmtLibReader::SmtLibReader(smt::SmtSolver & solver, bool strict) : solver_(solver), diff --git a/src/smtlibparser.yy b/src/smtlibparser.yy index 99e8607a4..74aeb4377 100644 --- a/src/smtlibparser.yy +++ b/src/smtlibparser.yy @@ -350,6 +350,10 @@ atom: } $$ = sym; } + | FLOAT + { + $$ = drv.solver()->make_term($1, drv.solver()->make_sort(smt::REAL)); + } | NAT { $$ = drv.solver()->make_term($1, drv.solver()->make_sort(smt::INT)); @@ -358,6 +362,10 @@ atom: { $$ = $1; } + | QUOTESTRING + { + $$ = drv.solver()->make_term($1, false, drv.solver()->make_sort(smt::STRING)); + } ; bvconst: diff --git a/src/solver_enums.cpp b/src/solver_enums.cpp index a3a77160d..84b774d6a 100644 --- a/src/solver_enums.cpp +++ b/src/solver_enums.cpp @@ -52,6 +52,7 @@ const unordered_map> { CVC5, { TERMITER, THEORY_INT, + THEORY_STR, THEORY_BV, THEORY_REAL, ARRAY_MODELS, @@ -173,6 +174,7 @@ std::ostream & operator<<(std::ostream & o, SolverAttribute a) case TERMITER: o << "TERMITER"; break; case THEORY_INT: o << "THEORY_INT"; break; case THEORY_REAL: o << "THEORY_REAL"; break; + case THEORY_STR: o << "THEORY_STR"; break; case ARRAY_MODELS: o << "ARRAY_MODELS"; break; case CONSTARR: o << "CONSTARR"; break; case FULL_TRANSFER: o << "FULL_TRANSFER"; break; diff --git a/src/sort.cpp b/src/sort.cpp index 5bdd671cf..be9501ab2 100644 --- a/src/sort.cpp +++ b/src/sort.cpp @@ -29,6 +29,7 @@ const std::unordered_map sortkind2str( { BV, "BitVec" }, { INT, "Int" }, { REAL, "Real" }, + { STRING, "String" }, { FUNCTION, "Function" }, { UNINTERPRETED, "Uninterpreted" }, { UNINTERPRETED_CONS, "UninterpretedSortConstructor" }, @@ -71,6 +72,10 @@ std::string AbsSort::to_string() const else if (sk == REAL) { return "Real"; + } + else if (sk == STRING) + { + return "String"; } else if (sk == BV) { diff --git a/src/sort_inference.cpp b/src/sort_inference.cpp index 15d9d3101..7d0b48f84 100644 --- a/src/sort_inference.cpp +++ b/src/sort_inference.cpp @@ -93,6 +93,10 @@ const std::unordered_map> { Rotate_Right, bv_sorts }, { BV_To_Nat, bv_sorts }, { Int_To_BV, int_sorts }, + { StrLt, string_sorts }, + { StrLeq, string_sorts }, + { StrConcat, string_sorts }, + { StrLen, string_sorts }, { Select, check_select_sorts }, { Store, check_store_sorts }, { Forall, check_quantifier_sorts }, @@ -175,6 +179,10 @@ const std::unordered_map< { Rotate_Right, same_sort }, { BV_To_Nat, int_sort }, { Int_To_BV, int_to_bv_sort }, + { StrLt, bool_sort }, + { StrLeq, bool_sort }, + { StrConcat, string_sort }, + { StrLen, int_sort }, { Select, select_sort }, { Store, store_sort }, { Forall, bool_sort }, @@ -462,6 +470,11 @@ bool int_sorts(const SortVec & sorts) return check_sortkind_matches(INT, sorts); }; +bool string_sorts(const SortVec & sorts) +{ + return check_sortkind_matches(STRING, sorts); +}; + bool arithmetic_sorts(const SortVec & sorts) { return check_one_of_sortkinds({ INT, REAL }, sorts); @@ -506,6 +519,12 @@ Sort int_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts) return solver->make_sort(INT); } +Sort string_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts) +{ + return solver->make_sort(STRING); +} + + Sort ite_sort(Op op, const AbsSmtSolver * solver, const SortVec & sorts) { if (sorts[1] != sorts[2]) diff --git a/src/term_translator.cpp b/src/term_translator.cpp index 5f681e3b6..31f6a4ffb 100644 --- a/src/term_translator.cpp +++ b/src/term_translator.cpp @@ -85,7 +85,7 @@ bool uses_uninterp_sort(const smt::Sort & sort) Sort TermTranslator::transfer_sort(const Sort & sort) { SortKind sk = sort->get_sort_kind(); - if ((sk == INT) || (sk == REAL) || (sk == BOOL)) + if ((sk == INT) || (sk == REAL) || (sk == BOOL) || (sk == STRING)) { return solver->make_sort(sk); } @@ -328,8 +328,10 @@ Term TermTranslator::transfer_term(const Term & term, const SortKind sk) Sort sort = solver->make_sort(INT); return cast_term(transferred_term, sort); } - else - { + else if (transferred_sk == STRING){ + Sort sort = solver->make_sort(STRING); + return cast_term(transferred_term, sort); + }else{ string msg("Cannot cast "); msg += transferred_term->to_string() + " to " + smt::to_string(sk); throw IncorrectUsageException(msg); @@ -346,14 +348,24 @@ std::string TermTranslator::infixize_rational(const std::string smtlib) const { } ind_of_up_start += 2; op = "/"; - int ind_of_up_end = smtlib.find_first_of(' ', ind_of_up_start); - assert(ind_of_up_end != std::string::npos); - ind_of_up_end -= 1; + std::string new_up; + int ind_of_up_end; + if (smtlib.substr(ind_of_up_start, 2) == "(-") + { + //std::cout<<"1 "<make_term(posval, sort); + return solver->make_term(Negate, posterm); + } return solver->make_term(mval, sort); } } @@ -434,10 +451,12 @@ Term TermTranslator::value_from_smt2(const std::string val, return solver->make_term(val == "true"); } } - else + else if (sk == STRING){ + return solver->make_term(val, false, sort); + } { throw NotImplementedException( - "Only taking bool, bv, int and real value terms currently."); + "Only taking bool, bv, int, real, str value terms currently."); } } diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 9f964987e..50148d596 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -78,6 +78,7 @@ switch_add_test(test-bv) switch_add_test(test-itp) switch_add_test(test-logging-solver) switch_add_test(test-sorting-network) +switch_add_test(test-str) switch_add_test(test-term-translation) switch_add_test(test-time-limit) switch_add_test(test-unsat-core) diff --git a/tests/cvc5/CMakeLists.txt b/tests/cvc5/CMakeLists.txt index 64b4b5756..725d1eb9b 100644 --- a/tests/cvc5/CMakeLists.txt +++ b/tests/cvc5/CMakeLists.txt @@ -19,6 +19,7 @@ switch_add_cvc5_test(cvc5-interpolants-api) switch_add_cvc5_test(cvc5-transfer) switch_add_cvc5_test(cvc5-neg-numbers) switch_add_cvc5_test(cvc5-printing) +switch_add_cvc5_test(cvc5-str) # Google Test switch_add_cvc5_test(cvc5-term-iter) diff --git a/tests/cvc5/cvc5-str.cpp b/tests/cvc5/cvc5-str.cpp new file mode 100644 index 000000000..58b846348 --- /dev/null +++ b/tests/cvc5/cvc5-str.cpp @@ -0,0 +1,69 @@ +/********************* */ +/*! \file cvc5-str.cpp +** \verbatim +** Top contributors (to current version): +** Nestan Tsiskaridze +** This file is part of the smt-switch project. +** Copyright (c) 2020 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file LICENSE in the top-level source +** directory for licensing information.\endverbatim +** +** \brief +** Tests for strings in the cvc5 backend. +**/ + +#include +#include +#include + +#include "assert.h" +#include "cvc5_factory.h" +#include "smt.h" + +using namespace smt; +using namespace std; + +int main() +{ + SmtSolver s = Cvc5SolverFactory::create(false); + s->set_opt("produce-models", "true"); + s->set_logic("S"); + Sort strsort = s->make_sort(STRING); + Sort intsort = s->make_sort(INT); + + Term zero = s->make_term(0, intsort); + + Term x = s->make_symbol("x", strsort); + Term y = s->make_symbol("y", strsort); + Term z = s->make_symbol("z", strsort); + + Term lenx = s->make_term(StrLen, x); + Term leny = s->make_term(StrLen, y); + Term lenz = s->make_term(StrLen, z); + + Term xy = s->make_term(StrConcat, x, y); + Term yx = s->make_term(StrConcat, y, x); + + //StrLt + s->assert_formula(s->make_term(StrLt, x, y)); + s->assert_formula(s->make_term(StrLt, yx, xy)); + //StrLeq StrConcat + s->assert_formula(s->make_term(StrLeq, z, xy)); + //StrLen + s->assert_formula(s->make_term(Lt, zero, lenz)); + //StrConcat + s->assert_formula(s->make_term(Not, s->make_term(Equal, xy, yx))); + + + + Result r = s->check_sat(); + assert(r.is_sat()); + + cout << "Model Values:" << endl; + for (auto t : TermVec({ x, y, z })) + { + cout << "\t" << t << " = " << s->get_value(t) << endl; + } + return 0; +} diff --git a/tests/cvc5/cvc5_test.cpp b/tests/cvc5/cvc5_test.cpp index 813ce6d6c..9eb9ad4c3 100644 --- a/tests/cvc5/cvc5_test.cpp +++ b/tests/cvc5/cvc5_test.cpp @@ -53,5 +53,22 @@ int main() cout << "\t" << c << endl; } + Term str_a = s->make_term("a", false, s->make_sort(STRING)); + cout << str_a << endl; + Term wstr_b = s->make_term(L"b", s->make_sort(STRING)); + cout << wstr_b << endl; + Term t = s->make_symbol("t", s->make_sort(STRING)); + Term w = s->make_symbol("w", s->make_sort(STRING)); + cout << t->to_string() << endl; + cout << w->to_string() << endl; + Term tw = s->make_term(StrConcat, t, w); + cout << tw->to_string() << endl; + cout << tw << endl; + cout << "Children of " << tw << endl; + for (auto c : tw) + { + cout << "\t" << c << endl; + } + return 0; } diff --git a/tests/smt2/qf_s/test-ops-SLIA.smt2 b/tests/smt2/qf_s/test-ops-SLIA.smt2 new file mode 100644 index 000000000..8e0157221 --- /dev/null +++ b/tests/smt2/qf_s/test-ops-SLIA.smt2 @@ -0,0 +1,29 @@ +(set-logic QF_SLIA) + +(declare-const x String) +(declare-const y String) +(declare-const z String) +(declare-const lenx Int) +(declare-const leny Int) +(declare-const lenz Int) + +(assert (= lenx (str.len x))) +(assert (= leny (str.len y))) + +(declare-const xy String) +(declare-const yx String) + +(assert (= xy (str.++ x y))) +(assert (= yx (str.++ y x))) + +;StrLt +(assert (str.< x y)) +(assert (str.< yx xy)) +;StrLeq StrConcat +(assert (str.<= z xy)) +;StrLen +(assert (< 0 lenz)) +;StrConcat +(assert (not (= xy yx))) + +(check-sat) diff --git a/tests/smt2/qf_s/test-ops.smt2 b/tests/smt2/qf_s/test-ops.smt2 new file mode 100644 index 000000000..5ae550fcc --- /dev/null +++ b/tests/smt2/qf_s/test-ops.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_S) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (not (= x y))) + +(check-sat) + diff --git a/tests/smtlib_reader_test_inputs.h b/tests/smtlib_reader_test_inputs.h index 610a7bedd..0ef4e0070 100644 --- a/tests/smtlib_reader_test_inputs.h +++ b/tests/smtlib_reader_test_inputs.h @@ -33,6 +33,11 @@ const std::unordered_map> qf_uflia_tests({ smt::Result(smt::SAT) } }, }); +const std::unordered_map> qf_s_tests({ + { "test-ops.smt2", { smt::Result(smt::SAT)} }, + { "test-ops-SLIA.smt2", { smt::Result(smt::SAT)} }, +}); + const std::unordered_map> qf_ufbv_tests( { { "test-attr.smt2", { smt::Result(smt::SAT), smt::Result(smt::UNSAT) } }, diff --git a/tests/test-smtlib-reader.cpp b/tests/test-smtlib-reader.cpp index 9161ddc0e..b066a9e4b 100644 --- a/tests/test-smtlib-reader.cpp +++ b/tests/test-smtlib-reader.cpp @@ -83,6 +83,11 @@ class IntReaderTests : public ReaderTests { }; +GTEST_ALLOW_UNINSTANTIATED_PARAMETERIZED_TEST(StrReaderTests); +class StrReaderTests : public ReaderTests +{ +}; + GTEST_ALLOW_UNINSTANTIATED_PARAMETERIZED_TEST(BitVecReaderTests); class BitVecReaderTests : public ReaderTests { @@ -117,6 +122,25 @@ TEST_P(IntReaderTests, QF_UFLIA_Smt2Files) } } +TEST_P(StrReaderTests, QF_S_Smt2Files) +{ + // SMT_SWITCH_DIR is a macro defined at build time + // and should point to the top-level Smt-Switch directory + string test = STRFY(SMT_SWITCH_DIR); + auto testpair = get<1>(GetParam()); + test += "/tests/smt2/qf_s/" + testpair.first; + reader->parse(test); + auto results = reader->get_results(); + auto expected_results = testpair.second; + ASSERT_EQ(results.size(), expected_results.size()); + + size_t size = results.size(); + for (size_t i = 0; i < size; i++) + { + EXPECT_EQ(results[i], expected_results[i]); + } +} + TEST_P(BitVecReaderTests, QF_UFBV_Smt2Files) { // SMT_SWITCH_DIR is a macro defined at build time @@ -182,6 +206,15 @@ INSTANTIATE_TEST_SUITE_P( testing::ValuesIn(qf_uflia_tests.begin(), qf_uflia_tests.end()))); +INSTANTIATE_TEST_SUITE_P( + ParameterizedSolverStrReaderTests, + StrReaderTests, + testing::Combine( + testing::ValuesIn(filter_non_generic_solver_configurations( + { THEORY_INT, THEORY_STR })), + testing::ValuesIn(qf_s_tests.begin(), qf_s_tests.end()))); + + INSTANTIATE_TEST_SUITE_P( ParameterizedSolverBitVecReaderTests, BitVecReaderTests, diff --git a/tests/test-str.cpp b/tests/test-str.cpp new file mode 100644 index 000000000..a81b8a465 --- /dev/null +++ b/tests/test-str.cpp @@ -0,0 +1,174 @@ +/********************* */ +/*! \file test-str.cpp +** \verbatim +** Top contributors (to current version): +** Nestan Tsiskaridze +** This file is part of the smt-switch project. +** Copyright (c) 2020 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file LICENSE in the top-level source +** directory for licensing information.\endverbatim +** +** \brief +** Tests for theory of strings. +**/ + +#include +#include + +#include "available_solvers.h" +#include "gtest/gtest.h" +#include "smt.h" + + +using namespace smt; +using namespace std; + +namespace smt_tests { + +GTEST_ALLOW_UNINSTANTIATED_PARAMETERIZED_TEST(StrTests); +class StrTests : public ::testing::Test, + public ::testing::WithParamInterface +{ + protected: + void SetUp() override + { + s = create_solver(GetParam()); + s->set_opt("produce-models", "true"); + s->set_opt("incremental", "true"); + } + SmtSolver s; +}; + +TEST_P(StrTests, StrChildren) +{ + Sort strsort = s->make_sort(STRING); + + Term t = s->make_symbol("t", strsort); + Term w = s->make_symbol("w", strsort); + Term strA = s->make_term("A", false, strsort); + + EXPECT_TRUE(t->get_op().is_null()); + EXPECT_TRUE(t->is_symbolic_const()); + EXPECT_FALSE(t->is_value()); + EXPECT_TRUE(w->is_symbolic_const()); + EXPECT_FALSE(w->is_value()); + EXPECT_FALSE(strA->is_symbolic_const()); + EXPECT_TRUE(strA->is_value()); + + Term tA = s->make_term(StrConcat, t, strA); + EXPECT_EQ(tA->get_op(), StrConcat); + TermVec children_tA; + for (auto tt : tA) + { + children_tA.push_back(tt); + } + EXPECT_EQ(children_tA[0], t); + EXPECT_EQ(children_tA[1], strA); + + Term tw = s->make_term(StrConcat, t, w); + EXPECT_EQ(tw->get_op(), StrConcat); + TermVec children_tw; + for (auto tt : tw) + { + children_tw.push_back(tt); + } + EXPECT_EQ(children_tw[0], t); + EXPECT_EQ(children_tw[1], w); +} + +TEST_P(StrTests, EqualVars) +{ + Sort str_sort = s->make_sort(STRING); + Term x1 = s->make_symbol("x1", str_sort); + Term x2 = s->make_symbol("x2", str_sort); + s->assert_formula(s->make_term(Equal, x1, x2)); + s->check_sat(); + std::string strx1 = s->get_value(x1)->to_string(); + std::string strx2 = s->get_value(x2)->to_string(); + ASSERT_EQ(strx1, strx2); +} + +TEST_P(StrTests, EqualStrConsts) +{ + Sort str_sort = s->make_sort(STRING); + Term x1 = s->make_term("A", false, str_sort); + Term x2 = s->make_term("A", false, str_sort); + s->check_sat(); + std::string strx1 = s->get_value(x1)->to_string(); + std::string strx2 = s->get_value(x2)->to_string(); + ASSERT_EQ(strx1, strx2); +} + + +TEST_P(StrTests, UseEscSequences) +{ + Sort str_sort = s->make_sort(STRING); + + Term x1 = s->make_term("\\u{0021}", true, str_sort); + Term x2 = s->make_term("\\u2200", true, str_sort); + Term x3 = s->make_term("\\u2102", false, str_sort); + Term x4 = s->make_term("\\u{10}", false, str_sort); + + s->check_sat(); + + std:wstring wchar_u = L"u"; + std::wstring wstrx1 = s->get_value(x1)->getStringValue(); + std::wstring wstrx2 = s->get_value(x2)->getStringValue(); + std::wstring wstrx3 = s->get_value(x3)->getStringValue(); + std::wstring wstrx4 = s->get_value(x4)->getStringValue(); + + assert(wstrx1.find(wchar_u) == std::wstring::npos); + assert(wstrx2.find(wchar_u) == std::wstring::npos); + assert(wstrx3.find(wchar_u) != std::wstring::npos); + assert(wstrx4.find(wchar_u) != std::wstring::npos); +} + + + + +TEST_P(StrTests, EqualVarStrVals) +{ + Sort str_sort = s->make_sort(STRING); + Term x1 = s->make_symbol("x1", str_sort); + Term x2 = s->make_symbol("x2", str_sort); + Term A = s->make_term("A", false, str_sort); + s->assert_formula(s->make_term(Equal, x1, A)); + s->assert_formula(s->make_term(Equal, x2, A)); + s->check_sat(); + std::string strx1 = s->get_value(x1)->to_string(); + std::string strx2 = s->get_value(x2)->to_string(); + ASSERT_EQ(strx1, strx2); +} + +TEST_P(StrTests, EqualWStrConsts) +{ + Sort str_sort = s->make_sort(STRING); + Term x1 = s->make_term(L"A", str_sort); + Term x2 = s->make_term(L"A", str_sort); + s->check_sat(); + std::string strx1 = s->get_value(x1)->to_string(); + std::string strx2 = s->get_value(x2)->to_string(); + ASSERT_EQ(strx1, strx2); +} + +TEST_P(StrTests, EqualVarWStrVals) +{ + Sort str_sort = s->make_sort(STRING); + Term x1 = s->make_symbol("x1", str_sort); + Term x2 = s->make_symbol("x2", str_sort); + Term A = s->make_term(L"A", str_sort); + s->assert_formula(s->make_term(Equal, x1, A)); + s->assert_formula(s->make_term(Equal, x2, A)); + s->check_sat(); + std::string strx1 = s->get_value(x1)->to_string(); + std::string strx2 = s->get_value(x2)->to_string(); + ASSERT_EQ(strx1, strx2); +} + +INSTANTIATE_TEST_SUITE_P( + ParameterizedSolverStrTests, + StrTests, + testing::ValuesIn(filter_solver_configurations({ THEORY_INT, THEORY_STR }))); + +} // namespace smt_tests