From 1a240947cad0dc01e44b94fb9491fa6befbab51a Mon Sep 17 00:00:00 2001 From: ntsis Date: Fri, 25 Aug 2023 09:20:20 -0700 Subject: [PATCH 01/10] Add partial string support --- contrib/setup-cvc5.sh | 7 +++- cvc5/include/cvc5_solver.h | 4 ++- cvc5/src/cvc5_solver.cpp | 64 ++++++++++++++++++++++++++++++++++++- cvc5/src/cvc5_sort.cpp | 4 +++ cvc5/src/cvc5_term.cpp | 6 ++++ include/generic_solver.h | 5 +++ include/logging_solver.h | 2 ++ include/ops.h | 5 +++ include/printing_solver.h | 3 ++ include/smtlibparser_maps.h | 6 ++++ include/solver.h | 22 +++++++++++++ include/sort.h | 1 + include/sort_inference.h | 4 +++ src/generic_solver.cpp | 30 +++++++++++++++++ src/generic_sort.cpp | 8 +++-- src/logging_solver.cpp | 40 +++++++++++++++++++++++ src/ops.cpp | 8 +++++ src/printing_solver.cpp | 9 ++++++ src/smtlib_reader.cpp | 3 +- src/smtlibparser.yy | 8 +++++ src/sort.cpp | 1 + src/sort_inference.cpp | 19 +++++++++++ src/term_translator.cpp | 37 +++++++++++++++------ 23 files changed, 280 insertions(+), 16 deletions(-) diff --git a/contrib/setup-cvc5.sh b/contrib/setup-cvc5.sh index 777ac4eb6..827abaae1 100755 --- a/contrib/setup-cvc5.sh +++ b/contrib/setup-cvc5.sh @@ -26,7 +26,12 @@ if [ ! -d "$DEPS/cvc5" ]; then make -j$NUM_CORES cd $DIR else - echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually." +# echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually." + cd $DEPS + cd cvc5 + cd build + make -j$NUM_CORES + cd $DIR fi if [ -f $DEPS/cvc5/build/src/libcvc5.a ] && [ -f $DEPS/cvc5/build/src/parser/libcvc5parser.a ]; then diff --git a/cvc5/include/cvc5_solver.h b/cvc5/include/cvc5_solver.h index 0932980bb..9f1930662 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/src/cvc5_solver.cpp b/cvc5/src/cvc5_solver.cpp index eb6c77c2c..a84382b26 100644 --- a/cvc5/src/cvc5_solver.cpp +++ b/cvc5/src/cvc5_solver.cpp @@ -94,6 +94,10 @@ const std::unordered_map primop2kind( { BV_To_Nat, ::cvc5::BITVECTOR_TO_NAT }, // Indexed Op { Int_To_BV, ::cvc5::INT_TO_BITVECTOR }, + { StrLt, ::cvc5::STRING_LT }, + { StrLeq, ::cvc5::STRING_LEQ }, + { StrLen, ::cvc5::STRING_LENGTH }, + { StrConcat, ::cvc5::STRING_CONCAT }, { Select, ::cvc5::SELECT }, { Store, ::cvc5::STORE }, { Forall, ::cvc5::FORALL }, @@ -163,7 +167,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 +191,60 @@ 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 constant with string and useEscSequences"; + msg += useEscSequences; + msg += " 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 constant with wstring 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 +536,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 47b37c3e7..968cc9841 100644 --- a/cvc5/src/cvc5_term.cpp +++ b/cvc5/src/cvc5_term.cpp @@ -50,6 +50,7 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop( { ::cvc5::NEG, Negate }, { ::cvc5::MULT, Mult }, { ::cvc5::DIVISION, Div }, + { ::cvc5::INTS_DIVISION, IntDiv }, { ::cvc5::LT, Lt }, { ::cvc5::LEQ, Le }, { ::cvc5::GT, Gt }, @@ -104,6 +105,11 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop( { ::cvc5::BITVECTOR_ROTATE_RIGHT, Rotate_Right }, // Conversion { ::cvc5::BITVECTOR_TO_NAT, BV_To_Nat }, + // String Op + { ::cvc5::STRING_LT, StrLt }, + { ::cvc5::STRING_LEQ, StrLeq }, + { ::cvc5::STRING_LENGTH, StrLen }, + { ::cvc5::STRING_CONCAT, StrConcat }, // Indexed Op { ::cvc5::INT_TO_BITVECTOR, Int_To_BV }, { ::cvc5::SELECT, Select }, diff --git a/include/generic_solver.h b/include/generic_solver.h index ce8cd6532..68f148e8e 100644 --- a/include/generic_solver.h +++ b/include/generic_solver.h @@ -127,6 +127,11 @@ class GenericSolver : public AbsSmtSolver */ Term make_value(bool b) const; Term make_value(int64_t i, const Sort & sort) const; + 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_value(const std::string& s, bool useEscSequences, const Sort & sort) const; + Term make_value(const std::wstring& s, const Sort & sort) const; + Term make_value(const std::string val, const Sort & sort, uint64_t base = 10) const; 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/ops.h b/include/ops.h index 39e3f23a0..8757ebf3f 100644 --- a/include/ops.h +++ b/include/ops.h @@ -97,6 +97,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..60fa8208f 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 + { "STRING", + { { "str.<", StrLt }, + { "str.<=", StrLeq}, + { "str.len", StrLen}, + { "str.++", StrConcat} } }, // ArraysEx { "A", { diff --git a/include/solver.h b/include/solver.h index cb04200ef..9f81ffc52 100644 --- a/include/solver.h +++ b/include/solver.h @@ -210,6 +210,28 @@ class AbsSmtSolver */ virtual Term make_term(int64_t i, const Sort & sort) const = 0; + /* Make a string value term + * @param s is the value + * @param useEscSequences is the useEscSequences in String constructor + * @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/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/src/generic_solver.cpp b/src/generic_solver.cpp index 9ed6f70ea..eb0dea084 100644 --- a/src/generic_solver.cpp +++ b/src/generic_solver.cpp @@ -851,6 +851,36 @@ Term GenericSolver::make_value(int64_t i, const Sort & sort) const } } +Term GenericSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const +{ + Term value_term = make_value(s, useEscSequences, sort); + return store_term(value_term); +} +Term GenericSolver::make_term(const std::wstring& s, const Sort & sort) const +{ + Term value_term = make_value(s, sort); + return store_term(value_term); +} + +Term GenericSolver::make_value(const std::string& s, bool useEscSequences, const Sort & sort) const +{ + SortKind sk = sort->get_sort_kind(); + assert(sk == STRING); + string repr; + repr = std::to_string(s); + Term term = std::make_shared(sort, Op(), TermVec{}, repr); //figure out how to handle useEscSequences + return term; +} +Term GenericSolver::make_value(const std::wstring& s, const Sort & sort) const +{ + SortKind sk = sort->get_sort_kind(); + assert(sk == STRING); + string repr; + repr = std::to_string(s); + Term term = std::make_shared(sort, Op(), TermVec{}, repr); + return term; +} + Term GenericSolver::make_term(const string val, const Sort & sort, uint64_t base) const diff --git a/src/generic_sort.cpp b/src/generic_sort.cpp index f4c0a4c2c..284999005 100644 --- a/src/generic_sort.cpp +++ b/src/generic_sort.cpp @@ -38,7 +38,7 @@ Sort make_uninterpreted_generic_sort(Sort sort_cons, Sort make_generic_sort(SortKind sk) { - 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)); } @@ -217,7 +217,8 @@ bool GenericSort::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(); } @@ -279,7 +280,8 @@ const std::unordered_map sortkind2smtlib( { { ARRAY, "Array" }, { BOOL, "Bool" }, { INT, "Int" }, - { REAL, "Real" }}); + { REAL, "Real" }, + { STRING, "String" }}); std::string to_smtlib(SortKind sk) { diff --git a/src/logging_solver.cpp b/src/logging_solver.cpp index b5ec337f7..8606bcd35 100644 --- a/src/logging_solver.cpp +++ b/src/logging_solver.cpp @@ -205,6 +205,46 @@ 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/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..27dcfa40e 100644 --- a/src/smtlib_reader.cpp +++ b/src/smtlib_reader.cpp @@ -52,7 +52,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/sort.cpp b/src/sort.cpp index 5bdd671cf..acc612f9e 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" }, 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."); } } From 81ac8e8c01e73f3ecd0c554e58d81868e0253d1a Mon Sep 17 00:00:00 2001 From: ntsis Date: Fri, 20 Oct 2023 11:35:16 -0700 Subject: [PATCH 02/10] Add tests for strings --- contrib/setup-cvc5.sh | 7 +- include/smtlibparser_maps.h | 2 +- include/solver_enums.h | 2 + python/smt_switch/enums_dec.pxi | 1 + python/smt_switch/enums_imp.pxi | 4 + src/generic_sort.cpp | 2 + src/logging_solver.cpp | 2 +- src/logging_sort.cpp | 5 +- src/smtlib_reader.cpp | 3 +- src/solver_enums.cpp | 2 + src/sort.cpp | 4 + tests/CMakeLists.txt | 1 + tests/cvc5/CMakeLists.txt | 1 + tests/cvc5/cvc5-str.cpp | 71 +++++++++++++++++ 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-generic-solver.cpp | 63 +++++++++++++++ tests/test-generic-sort.cpp | 11 +++ tests/test-generic-term.cpp | 19 +++++ tests/test-logging-solver.cpp | 39 +++++++++- tests/test-smtlib-reader.cpp | 33 ++++++++ tests/test-str.cpp | 120 +++++++++++++++++++++++++++++ 24 files changed, 439 insertions(+), 13 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/contrib/setup-cvc5.sh b/contrib/setup-cvc5.sh index 827abaae1..777ac4eb6 100755 --- a/contrib/setup-cvc5.sh +++ b/contrib/setup-cvc5.sh @@ -26,12 +26,7 @@ if [ ! -d "$DEPS/cvc5" ]; then make -j$NUM_CORES cd $DIR else -# echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually." - cd $DEPS - cd cvc5 - cd build - make -j$NUM_CORES - cd $DIR + echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually." fi if [ -f $DEPS/cvc5/build/src/libcvc5.a ] && [ -f $DEPS/cvc5/build/src/parser/libcvc5parser.a ]; then diff --git a/include/smtlibparser_maps.h b/include/smtlibparser_maps.h index 60fa8208f..0c2f72380 100644 --- a/include/smtlibparser_maps.h +++ b/include/smtlibparser_maps.h @@ -97,7 +97,7 @@ const std::unordered_map> { "rotate_left", Rotate_Left }, { "rotate_right", Rotate_Right } } }, // Strings - { "STRING", + { "S", { { "str.<", StrLt }, { "str.<=", StrLeq}, { "str.len", StrLen}, 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/python/smt_switch/enums_dec.pxi b/python/smt_switch/enums_dec.pxi index 8c5bb59a0..da007179f 100644 --- a/python/smt_switch/enums_dec.pxi +++ b/python/smt_switch/enums_dec.pxi @@ -43,6 +43,7 @@ cdef extern from "solver_enums.h" namespace "smt": cdef c_SolverAttribute c_TERMITER "smt::TERMITER" cdef c_SolverAttribute c_THEORY_INT "smt::THEORY_INT" cdef c_SolverAttribute c_THEORY_REAL "smt::THEORY_REAL" + cdef c_SolverAttribute c_THEORY_STR "smt::THEORY_STR" cdef c_SolverAttribute c_ARRAY_MODELS "smt::ARRAY_MODELS" cdef c_SolverAttribute c_CONSTARR "smt::CONSTARR" cdef c_SolverAttribute c_FULL_TRANSFER "smt::FULL_TRANSFER" diff --git a/python/smt_switch/enums_imp.pxi b/python/smt_switch/enums_imp.pxi index 8d01eaf0a..92bede9cb 100644 --- a/python/smt_switch/enums_imp.pxi +++ b/python/smt_switch/enums_imp.pxi @@ -163,6 +163,10 @@ cdef SolverAttribute THEORY_REAL = SolverAttribute() THEORY_REAL.sa = c_THEORY_REAL setattr(solverattr, "THEORY_REAL", THEORY_REAL) +cdef SolverAttribute THEORY_STR = SolverAttribute() +THEORY_STR.sa = c_THEORY_STR +setattr(solverattr, "THEORY_STR", THEORY_STR) + cdef SolverAttribute ARRAY_MODELS = SolverAttribute() ARRAY_MODELS.sa = c_ARRAY_MODELS setattr(solverattr, "ARRAY_MODELS", ARRAY_MODELS) diff --git a/src/generic_sort.cpp b/src/generic_sort.cpp index 284999005..b21ad3a96 100644 --- a/src/generic_sort.cpp +++ b/src/generic_sort.cpp @@ -163,6 +163,8 @@ string GenericSort::compute_string() const { return smt::to_smtlib(SortKind::INT); } else if (get_sort_kind() == SortKind::REAL) { return smt::to_smtlib(SortKind::REAL); + } else if (get_sort_kind() == SortKind::STRING) { + return smt::to_smtlib(SortKind::STRING); } else if (get_sort_kind() == SortKind::FUNCTION) { string name = "("; vector domain_sorts = get_domain_sorts(); diff --git a/src/logging_solver.cpp b/src/logging_solver.cpp index 8606bcd35..4c5d7e13b 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 */ 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/smtlib_reader.cpp b/src/smtlib_reader.cpp index 27dcfa40e..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( 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 acc612f9e..be9501ab2 100644 --- a/src/sort.cpp +++ b/src/sort.cpp @@ -72,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/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..84f53d0d1 --- /dev/null +++ b/tests/cvc5/cvc5-str.cpp @@ -0,0 +1,71 @@ +/********************* */ +/*! \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 +** +** +**/ + +#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_opt("strings-exp", "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-generic-solver.cpp b/tests/test-generic-solver.cpp index 94d35cd4e..234b5c8b6 100644 --- a/tests/test-generic-solver.cpp +++ b/tests/test-generic-solver.cpp @@ -158,6 +158,26 @@ void test_int_1(SmtSolver gs) } } +void test_str_1(SmtSolver gs) +{ + Sort str_sort = gs->make_sort(STRING); + cout << "created sort of sort kind " << to_string(STRING) + << ". The sort is: " << str_sort << endl; + + Sort str_sort1 = gs->make_sort(STRING); + assert(str_sort == str_sort1); + + cout << "trying to create a sort in a wrong way" << endl; + try + { + Sort err_sort = gs->make_sort(ARRAY); + } + catch (IncorrectUsageException e) + { + cout << "caught the exception" << endl; + } +} + void test_bv_1(SmtSolver gs) { Sort bv_sort = gs->make_sort(BV, 4); @@ -233,6 +253,33 @@ void test_int_2(SmtSolver gs) gs->pop(1); } +void test_str_2(SmtSolver gs) +{ + Sort str_sort = gs->make_sort(STRING); + Term str_A = gs->make_term("A", str_sort); + Term str_B = gs->make_term("B", str_sort); + cout << "making some constants" << endl; + + Term str_A_equal_B = + gs->make_term(Equal, TermVec({ str_A, str_B })); + + cout << "checking some simple assertions" << endl; + + gs->push(1); + gs->assert_formula(str_A_equal_B); + Result r; + r = gs->check_sat(); + assert(r.is_unsat()); + gs->pop(1); + + gs->push(1); + Term str_A_equal_A = gs->make_term(Equal, TermVec({ str_A, str_A })); + gs->assert_formula(str_A_equal_A); + r = gs->check_sat(); + assert(r.is_sat()); + gs->pop(1); +} + void test_bad_term_1(SmtSolver gs) { cout << "trying to create a badly-sorted term and getting and exception" @@ -498,6 +545,22 @@ void test_int_models(SmtSolver gs) gs->pop(1); } +void test_str_models(SmtSolver gs) +{ + // Testing models + gs->push(1); + Sort str_sort = gs->make_sort(STRING); + Term str_A = gs->make_term("A", str_sort); + Term i1 = gs->make_symbol("i", str_sort); + Term for1 = gs->make_term(Equal, i1, int_zero); + gs->assert_formula(for1); + Result result = gs->check_sat(); + assert(result.is_sat()); + Term val1 = gs->get_value(i1); + Term val2 = gs->get_value(for1); + gs->pop(1); +} + void test_bv_models(SmtSolver gs) { // Testing models diff --git a/tests/test-generic-sort.cpp b/tests/test-generic-sort.cpp index 790365e5d..eacf12e51 100644 --- a/tests/test-generic-sort.cpp +++ b/tests/test-generic-sort.cpp @@ -47,6 +47,14 @@ int main() assert((s1.get_sort_kind()) == (s2.get_sort_kind())); assert(s1.get_sort_kind() == INT); + GenericSort strs1(STRING); + GenericSort strs2(STRING); + assert(strs1.hash() == strs2.hash()); + assert(strs1.to_string() == strs2.to_string()); + assert(strs2.to_string() == strs1.to_string()); + assert((strs1.get_sort_kind()) == (strs2.get_sort_kind())); + assert(strs1.get_sort_kind() == STRING); + Sort int1 = make_generic_sort(INT); Sort int2 = make_generic_sort(INT); assert(int1 == int2); @@ -54,6 +62,9 @@ int main() Sort bv5 = make_generic_sort(BV, 5); assert(bv4 != bv5); assert(bv4 != int1); + Sort str1 = make_generic_sort(STRING); + Sort str2 = make_generic_sort(STRING); + assert(str1 == str2); Sort inttobv4 = make_generic_sort(FUNCTION, int1, bv4); Sort inttobv4_second = make_generic_sort(FUNCTION, int2, bv4); assert(inttobv4 == inttobv4_second); diff --git a/tests/test-generic-term.cpp b/tests/test-generic-term.cpp index 8fe0c0231..d5b89aa1d 100644 --- a/tests/test-generic-term.cpp +++ b/tests/test-generic-term.cpp @@ -57,4 +57,23 @@ int main() { assert(x.is_symbol()); assert(!x.is_param()); assert(x.is_symbolic_const()); + + cout << "Testing a string constant" << endl; + Sort str_sort = make_generic_sort(STRING); + GenericTerm A(str_sort, Op(), {}, "A"); + GenericTerm A_prime(str_sort, Op(), {}, "A"); + assert(A.get_id() == A_prime.get_id()); + assert(A.hash() == A_prime.hash()); + assert(!A.is_symbol()); + assert(!A.is_param()); + assert(!A.is_symbolic_const()); + + cout << "Testing a string variable" << endl; + GenericTerm y(str_sort, Op(), {}, "y", true); + GenericTerm y_prime(str_sort, Op(), {}, "y", true); + assert(y.get_id() == y_prime.get_id()); + assert(y.hash() == y_prime.hash()); + assert(y.is_symbol()); + assert(!y.is_param()); + assert(y.is_symbolic_const()); } diff --git a/tests/test-logging-solver.cpp b/tests/test-logging-solver.cpp index 478e6ce5a..50b5558d3 100644 --- a/tests/test-logging-solver.cpp +++ b/tests/test-logging-solver.cpp @@ -45,15 +45,19 @@ class LoggingTests : public ::testing::Test, bvsort8 = s->make_sort(BV, 8); arraysort = s->make_sort(ARRAY, bvsort4, bvsort8); funsort = s->make_sort(FUNCTION, SortVec{ bvsort4, bvsort8 }); + strsort = s->make_sort(STRING); x = s->make_symbol("x", bvsort4); y = s->make_symbol("y", bvsort4); zero = s->make_term(0, bvsort4); one = s->make_term(1, bvsort4); + t = s->make_symbol("t", strsort); + w = s->make_symbol("w", strsort); + strA = s->make_term("A", false, strsort); } SmtSolver s; - Sort bvsort4, bvsort8, arraysort, funsort; - Term x, y, zero, one; + Sort bvsort4, bvsort8, arraysort, funsort, strsort; + Term x, y, zero, one, t, w, strA; }; TEST_P(LoggingTests, Children) @@ -150,6 +154,37 @@ TEST_P(LoggingTests, Compare) EXPECT_EQ(fxv, fyv); } +TEST_P(LoggingTests, StrChildren) +{ + 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); +} + INSTANTIATE_TEST_SUITE_P( ParameterizedSolverLoggingTests, LoggingTests, 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..50df4c6e1 --- /dev/null +++ b/tests/test-str.cpp @@ -0,0 +1,120 @@ +/********************* */ +/*! \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 constants in 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, 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(); + cout << x1 << " = " << strx1 << endl; + cout << x2 << " = " << strx2 << endl; + 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(); + cout << x1 << " = " << strx1 << endl; + cout << x2 << " = " << strx2 << endl; + ASSERT_EQ(strx1, strx2); +} + +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(); + cout << x1 << " = " << strx1 << endl; + cout << x2 << " = " << strx2 << endl; + 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(); + cout << x1 << " = " << strx1 << endl; + cout << x2 << " = " << strx2 << endl; + 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(); + cout << x1 << " = " << strx1 << endl; + cout << x2 << " = " << strx2 << endl; + ASSERT_EQ(strx1, strx2); +} + +INSTANTIATE_TEST_SUITE_P( + ParameterizedSolverStrTests, + StrTests, + testing::ValuesIn(filter_solver_configurations({ THEORY_INT, THEORY_STR }))); + +} // namespace smt_tests From c0c66ae8da713d00ae8c7cc0e08d7b05837e2a59 Mon Sep 17 00:00:00 2001 From: ntsis Date: Thu, 26 Oct 2023 22:46:23 -0700 Subject: [PATCH 03/10] Add string tests for escape sequences. Make the PR smaller. No support for strings in generic solver in this PR --- cvc5/include/cvc5_term.h | 1 + cvc5/src/cvc5_term.cpp | 3 +- include/generic_term.h | 1 + include/logging_term.h | 1 + include/solver.h | 7 ++-- include/term.h | 2 ++ python/smt_switch/enums_dec.pxi | 1 - python/smt_switch/enums_imp.pxi | 4 --- src/generic_solver.cpp | 22 ++++-------- src/generic_sort.cpp | 10 ++---- src/generic_term.cpp | 5 +++ src/logging_term.cpp | 5 +++ tests/test-generic-solver.cpp | 63 --------------------------------- tests/test-generic-sort.cpp | 11 ------ tests/test-generic-term.cpp | 19 ---------- tests/test-str.cpp | 50 ++++++++++++++++++++------ 16 files changed, 71 insertions(+), 134 deletions(-) diff --git a/cvc5/include/cvc5_term.h b/cvc5/include/cvc5_term.h index 281cba35f..282a84c8e 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() override; uint64_t to_int() const override; /** Iterators for traversing the children */ diff --git a/cvc5/src/cvc5_term.cpp b/cvc5/src/cvc5_term.cpp index 968cc9841..139da9aaa 100644 --- a/cvc5/src/cvc5_term.cpp +++ b/cvc5/src/cvc5_term.cpp @@ -50,7 +50,6 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop( { ::cvc5::NEG, Negate }, { ::cvc5::MULT, Mult }, { ::cvc5::DIVISION, Div }, - { ::cvc5::INTS_DIVISION, IntDiv }, { ::cvc5::LT, Lt }, { ::cvc5::LEQ, Le }, { ::cvc5::GT, Gt }, @@ -282,6 +281,8 @@ bool Cvc5Term::is_value() const std::string Cvc5Term::to_string() { return term.toString(); } +std::wstring Cvc5Term::getStringValue() { return term.getStringValue(); } + uint64_t Cvc5Term::to_int() const { std::string val = term.toString(); diff --git a/include/generic_term.h b/include/generic_term.h index 39f153830..842b2af32 100644 --- a/include/generic_term.h +++ b/include/generic_term.h @@ -47,6 +47,7 @@ class GenericTerm : public AbsTerm Sort get_sort() const override; std::size_t get_id() const override; std::string to_string() override; + std::wstring getStringValue() override; std::size_t hash() const override; bool is_value() const override; uint64_t to_int() const override; diff --git a/include/logging_term.h b/include/logging_term.h index 79de5210f..116486626 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() override; bool is_symbol() const override; bool is_param() const override; bool is_symbolic_const() const override; diff --git a/include/solver.h b/include/solver.h index 9f81ffc52..ed3d1ba59 100644 --- a/include/solver.h +++ b/include/solver.h @@ -210,12 +210,15 @@ class AbsSmtSolver */ virtual Term make_term(int64_t i, const Sort & sort) const = 0; - /* Make a string value term + /* 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 is the useEscSequences in String constructor + * @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."); diff --git a/include/term.h b/include/term.h index 897d76533..91de8c411 100644 --- a/include/term.h +++ b/include/term.h @@ -51,6 +51,8 @@ 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() = 0; /* 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/python/smt_switch/enums_dec.pxi b/python/smt_switch/enums_dec.pxi index da007179f..8c5bb59a0 100644 --- a/python/smt_switch/enums_dec.pxi +++ b/python/smt_switch/enums_dec.pxi @@ -43,7 +43,6 @@ cdef extern from "solver_enums.h" namespace "smt": cdef c_SolverAttribute c_TERMITER "smt::TERMITER" cdef c_SolverAttribute c_THEORY_INT "smt::THEORY_INT" cdef c_SolverAttribute c_THEORY_REAL "smt::THEORY_REAL" - cdef c_SolverAttribute c_THEORY_STR "smt::THEORY_STR" cdef c_SolverAttribute c_ARRAY_MODELS "smt::ARRAY_MODELS" cdef c_SolverAttribute c_CONSTARR "smt::CONSTARR" cdef c_SolverAttribute c_FULL_TRANSFER "smt::FULL_TRANSFER" diff --git a/python/smt_switch/enums_imp.pxi b/python/smt_switch/enums_imp.pxi index 92bede9cb..8d01eaf0a 100644 --- a/python/smt_switch/enums_imp.pxi +++ b/python/smt_switch/enums_imp.pxi @@ -163,10 +163,6 @@ cdef SolverAttribute THEORY_REAL = SolverAttribute() THEORY_REAL.sa = c_THEORY_REAL setattr(solverattr, "THEORY_REAL", THEORY_REAL) -cdef SolverAttribute THEORY_STR = SolverAttribute() -THEORY_STR.sa = c_THEORY_STR -setattr(solverattr, "THEORY_STR", THEORY_STR) - cdef SolverAttribute ARRAY_MODELS = SolverAttribute() ARRAY_MODELS.sa = c_ARRAY_MODELS setattr(solverattr, "ARRAY_MODELS", ARRAY_MODELS) diff --git a/src/generic_solver.cpp b/src/generic_solver.cpp index eb0dea084..dad3c0a32 100644 --- a/src/generic_solver.cpp +++ b/src/generic_solver.cpp @@ -853,32 +853,22 @@ Term GenericSolver::make_value(int64_t i, const Sort & sort) const Term GenericSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const { - Term value_term = make_value(s, useEscSequences, sort); - return store_term(value_term); + throw NotImplementedException("make_term not supported for strings with useEscSequences for this solver."); } + Term GenericSolver::make_term(const std::wstring& s, const Sort & sort) const { - Term value_term = make_value(s, sort); - return store_term(value_term); + throw NotImplementedException("make_term not supported for strings with wstring for this solver."); } Term GenericSolver::make_value(const std::string& s, bool useEscSequences, const Sort & sort) const { - SortKind sk = sort->get_sort_kind(); - assert(sk == STRING); - string repr; - repr = std::to_string(s); - Term term = std::make_shared(sort, Op(), TermVec{}, repr); //figure out how to handle useEscSequences - return term; + throw NotImplementedException("make_value not supported for strings with useEscSequences for this solver."); } + Term GenericSolver::make_value(const std::wstring& s, const Sort & sort) const { - SortKind sk = sort->get_sort_kind(); - assert(sk == STRING); - string repr; - repr = std::to_string(s); - Term term = std::make_shared(sort, Op(), TermVec{}, repr); - return term; + throw NotImplementedException("make_value not supported for strings with wstring for this solver."); } Term GenericSolver::make_term(const string val, diff --git a/src/generic_sort.cpp b/src/generic_sort.cpp index b21ad3a96..f4c0a4c2c 100644 --- a/src/generic_sort.cpp +++ b/src/generic_sort.cpp @@ -38,7 +38,7 @@ Sort make_uninterpreted_generic_sort(Sort sort_cons, Sort make_generic_sort(SortKind sk) { - if (sk != BOOL && sk != INT && sk != REAL && sk!= STRING) + if (sk != BOOL && sk != INT && sk != REAL) { throw IncorrectUsageException("Can't create sort from " + to_string(sk)); } @@ -163,8 +163,6 @@ string GenericSort::compute_string() const { return smt::to_smtlib(SortKind::INT); } else if (get_sort_kind() == SortKind::REAL) { return smt::to_smtlib(SortKind::REAL); - } else if (get_sort_kind() == SortKind::STRING) { - return smt::to_smtlib(SortKind::STRING); } else if (get_sort_kind() == SortKind::FUNCTION) { string name = "("; vector domain_sorts = get_domain_sorts(); @@ -219,8 +217,7 @@ bool GenericSort::compare(const Sort & s) const { case BOOL: case INT: - case REAL: - case STRING: { return true; + case REAL: { return true; } case BV: { return get_width() == s->get_width(); } @@ -282,8 +279,7 @@ const std::unordered_map sortkind2smtlib( { { ARRAY, "Array" }, { BOOL, "Bool" }, { INT, "Int" }, - { REAL, "Real" }, - { STRING, "String" }}); + { REAL, "Real" }}); std::string to_smtlib(SortKind sk) { diff --git a/src/generic_term.cpp b/src/generic_term.cpp index 050129e24..7757908cf 100644 --- a/src/generic_term.cpp +++ b/src/generic_term.cpp @@ -141,6 +141,11 @@ string GenericTerm::to_string() return repr; } +wstring GenericTerm::getStringValue() +{ + throw NotImplementedException("GetStringValue not supported for this solver."); +} + size_t GenericTerm::hash() const { return str_hash(compute_string()); } // check if op is null because a non-value diff --git a/src/logging_term.cpp b/src/logging_term.cpp index d64a2f9b1..89a0024a3 100644 --- a/src/logging_term.cpp +++ b/src/logging_term.cpp @@ -164,6 +164,11 @@ string LoggingTerm::to_string() } } +wstring LoggingTerm::getStringValue() +{ + return wrapped_term->getStringValue(); +} + bool LoggingTerm::is_symbol() const { // functions, parameters, and symbolic constants are all symbols diff --git a/tests/test-generic-solver.cpp b/tests/test-generic-solver.cpp index 234b5c8b6..94d35cd4e 100644 --- a/tests/test-generic-solver.cpp +++ b/tests/test-generic-solver.cpp @@ -158,26 +158,6 @@ void test_int_1(SmtSolver gs) } } -void test_str_1(SmtSolver gs) -{ - Sort str_sort = gs->make_sort(STRING); - cout << "created sort of sort kind " << to_string(STRING) - << ". The sort is: " << str_sort << endl; - - Sort str_sort1 = gs->make_sort(STRING); - assert(str_sort == str_sort1); - - cout << "trying to create a sort in a wrong way" << endl; - try - { - Sort err_sort = gs->make_sort(ARRAY); - } - catch (IncorrectUsageException e) - { - cout << "caught the exception" << endl; - } -} - void test_bv_1(SmtSolver gs) { Sort bv_sort = gs->make_sort(BV, 4); @@ -253,33 +233,6 @@ void test_int_2(SmtSolver gs) gs->pop(1); } -void test_str_2(SmtSolver gs) -{ - Sort str_sort = gs->make_sort(STRING); - Term str_A = gs->make_term("A", str_sort); - Term str_B = gs->make_term("B", str_sort); - cout << "making some constants" << endl; - - Term str_A_equal_B = - gs->make_term(Equal, TermVec({ str_A, str_B })); - - cout << "checking some simple assertions" << endl; - - gs->push(1); - gs->assert_formula(str_A_equal_B); - Result r; - r = gs->check_sat(); - assert(r.is_unsat()); - gs->pop(1); - - gs->push(1); - Term str_A_equal_A = gs->make_term(Equal, TermVec({ str_A, str_A })); - gs->assert_formula(str_A_equal_A); - r = gs->check_sat(); - assert(r.is_sat()); - gs->pop(1); -} - void test_bad_term_1(SmtSolver gs) { cout << "trying to create a badly-sorted term and getting and exception" @@ -545,22 +498,6 @@ void test_int_models(SmtSolver gs) gs->pop(1); } -void test_str_models(SmtSolver gs) -{ - // Testing models - gs->push(1); - Sort str_sort = gs->make_sort(STRING); - Term str_A = gs->make_term("A", str_sort); - Term i1 = gs->make_symbol("i", str_sort); - Term for1 = gs->make_term(Equal, i1, int_zero); - gs->assert_formula(for1); - Result result = gs->check_sat(); - assert(result.is_sat()); - Term val1 = gs->get_value(i1); - Term val2 = gs->get_value(for1); - gs->pop(1); -} - void test_bv_models(SmtSolver gs) { // Testing models diff --git a/tests/test-generic-sort.cpp b/tests/test-generic-sort.cpp index eacf12e51..790365e5d 100644 --- a/tests/test-generic-sort.cpp +++ b/tests/test-generic-sort.cpp @@ -47,14 +47,6 @@ int main() assert((s1.get_sort_kind()) == (s2.get_sort_kind())); assert(s1.get_sort_kind() == INT); - GenericSort strs1(STRING); - GenericSort strs2(STRING); - assert(strs1.hash() == strs2.hash()); - assert(strs1.to_string() == strs2.to_string()); - assert(strs2.to_string() == strs1.to_string()); - assert((strs1.get_sort_kind()) == (strs2.get_sort_kind())); - assert(strs1.get_sort_kind() == STRING); - Sort int1 = make_generic_sort(INT); Sort int2 = make_generic_sort(INT); assert(int1 == int2); @@ -62,9 +54,6 @@ int main() Sort bv5 = make_generic_sort(BV, 5); assert(bv4 != bv5); assert(bv4 != int1); - Sort str1 = make_generic_sort(STRING); - Sort str2 = make_generic_sort(STRING); - assert(str1 == str2); Sort inttobv4 = make_generic_sort(FUNCTION, int1, bv4); Sort inttobv4_second = make_generic_sort(FUNCTION, int2, bv4); assert(inttobv4 == inttobv4_second); diff --git a/tests/test-generic-term.cpp b/tests/test-generic-term.cpp index d5b89aa1d..8fe0c0231 100644 --- a/tests/test-generic-term.cpp +++ b/tests/test-generic-term.cpp @@ -57,23 +57,4 @@ int main() { assert(x.is_symbol()); assert(!x.is_param()); assert(x.is_symbolic_const()); - - cout << "Testing a string constant" << endl; - Sort str_sort = make_generic_sort(STRING); - GenericTerm A(str_sort, Op(), {}, "A"); - GenericTerm A_prime(str_sort, Op(), {}, "A"); - assert(A.get_id() == A_prime.get_id()); - assert(A.hash() == A_prime.hash()); - assert(!A.is_symbol()); - assert(!A.is_param()); - assert(!A.is_symbolic_const()); - - cout << "Testing a string variable" << endl; - GenericTerm y(str_sort, Op(), {}, "y", true); - GenericTerm y_prime(str_sort, Op(), {}, "y", true); - assert(y.get_id() == y_prime.get_id()); - assert(y.hash() == y_prime.hash()); - assert(y.is_symbol()); - assert(!y.is_param()); - assert(y.is_symbolic_const()); } diff --git a/tests/test-str.cpp b/tests/test-str.cpp index 50df4c6e1..404c75037 100644 --- a/tests/test-str.cpp +++ b/tests/test-str.cpp @@ -17,10 +17,14 @@ #include #include +// use this line for printing wstrings +//#include + #include "available_solvers.h" #include "gtest/gtest.h" #include "smt.h" + using namespace smt; using namespace std; @@ -49,8 +53,6 @@ TEST_P(StrTests, EqualVars) s->check_sat(); std::string strx1 = s->get_value(x1)->to_string(); std::string strx2 = s->get_value(x2)->to_string(); - cout << x1 << " = " << strx1 << endl; - cout << x2 << " = " << strx2 << endl; ASSERT_EQ(strx1, strx2); } @@ -62,11 +64,45 @@ TEST_P(StrTests, EqualStrConsts) s->check_sat(); std::string strx1 = s->get_value(x1)->to_string(); std::string strx2 = s->get_value(x2)->to_string(); - cout << x1 << " = " << strx1 << endl; - cout << x2 << " = " << strx2 << endl; ASSERT_EQ(strx1, strx2); } + +TEST_P(StrTests, UseEscSequences) +{ + // use these two lines for printing wstrings + //std::locale::global(std::locale("")); + //std::wcout.imbue(std::locale()); + + 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(); + + + // an example of printing wstrx1 + //std::cout << x1 << " = "; + //std::wcout << wstrx1 << std::endl; + + 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); @@ -78,8 +114,6 @@ TEST_P(StrTests, EqualVarStrVals) s->check_sat(); std::string strx1 = s->get_value(x1)->to_string(); std::string strx2 = s->get_value(x2)->to_string(); - cout << x1 << " = " << strx1 << endl; - cout << x2 << " = " << strx2 << endl; ASSERT_EQ(strx1, strx2); } @@ -91,8 +125,6 @@ TEST_P(StrTests, EqualWStrConsts) s->check_sat(); std::string strx1 = s->get_value(x1)->to_string(); std::string strx2 = s->get_value(x2)->to_string(); - cout << x1 << " = " << strx1 << endl; - cout << x2 << " = " << strx2 << endl; ASSERT_EQ(strx1, strx2); } @@ -107,8 +139,6 @@ TEST_P(StrTests, EqualVarWStrVals) s->check_sat(); std::string strx1 = s->get_value(x1)->to_string(); std::string strx2 = s->get_value(x2)->to_string(); - cout << x1 << " = " << strx1 << endl; - cout << x2 << " = " << strx2 << endl; ASSERT_EQ(strx1, strx2); } From 88a943f5e454e5968bb803d2299551a51ae467c2 Mon Sep 17 00:00:00 2001 From: ntsis Date: Thu, 26 Oct 2023 23:02:20 -0700 Subject: [PATCH 04/10] A bug fix --- include/solver.h | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/include/solver.h b/include/solver.h index ed3d1ba59..86cd09634 100644 --- a/include/solver.h +++ b/include/solver.h @@ -219,21 +219,15 @@ class AbsSmtSolver * @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."); - - } + virtual Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const = 0; /* 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."); - - } + virtual Term make_term(const std::wstring& s, const Sort & sort) const = 0; /* 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 From 1764e7e4ab9d3db602067fd48d265e96c91c47e0 Mon Sep 17 00:00:00 2001 From: ntsis Date: Mon, 30 Oct 2023 22:26:52 -0700 Subject: [PATCH 05/10] Resolve git checks --- cvc5/include/cvc5_term.h | 2 +- cvc5/src/cvc5_term.cpp | 2 +- include/solver.h | 8 ++++++-- include/term.h | 5 ++++- src/logging_term.cpp | 2 +- 5 files changed, 13 insertions(+), 6 deletions(-) diff --git a/cvc5/include/cvc5_term.h b/cvc5/include/cvc5_term.h index 282a84c8e..1c993459c 100644 --- a/cvc5/include/cvc5_term.h +++ b/cvc5/include/cvc5_term.h @@ -64,7 +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() override; + virtual std::wstring getStringValue() const override; uint64_t to_int() const override; /** Iterators for traversing the children */ diff --git a/cvc5/src/cvc5_term.cpp b/cvc5/src/cvc5_term.cpp index 139da9aaa..972117329 100644 --- a/cvc5/src/cvc5_term.cpp +++ b/cvc5/src/cvc5_term.cpp @@ -281,7 +281,7 @@ bool Cvc5Term::is_value() const std::string Cvc5Term::to_string() { return term.toString(); } -std::wstring Cvc5Term::getStringValue() { return term.getStringValue(); } +std::wstring Cvc5Term::getStringValue() const { return term.getStringValue(); } uint64_t Cvc5Term::to_int() const { diff --git a/include/solver.h b/include/solver.h index 86cd09634..98317fd3b 100644 --- a/include/solver.h +++ b/include/solver.h @@ -219,15 +219,19 @@ class AbsSmtSolver * @return a value term with Sort sort and value s */ - virtual Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const = 0; + 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."); + } - virtual Term make_term(const std::wstring& s, const Sort & sort) const = 0; /* 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 diff --git a/include/term.h b/include/term.h index 91de8c411..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 { @@ -52,7 +53,9 @@ class AbsTerm /* to_string in smt2 format */ virtual std::string to_string() = 0; /* returns the string term as a native string value */ - virtual std::wstring getStringValue() = 0; + 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_term.cpp b/src/logging_term.cpp index 89a0024a3..3514285bf 100644 --- a/src/logging_term.cpp +++ b/src/logging_term.cpp @@ -164,7 +164,7 @@ string LoggingTerm::to_string() } } -wstring LoggingTerm::getStringValue() +wstring LoggingTerm::getStringValue() const { return wrapped_term->getStringValue(); } From bbe5eb77c071ffe1915d35cff52b0c566358c331 Mon Sep 17 00:00:00 2001 From: ntsis Date: Mon, 30 Oct 2023 23:18:27 -0700 Subject: [PATCH 06/10] Missed to add to the previous push --- include/logging_term.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/logging_term.h b/include/logging_term.h index 116486626..e602133dd 100644 --- a/include/logging_term.h +++ b/include/logging_term.h @@ -45,7 +45,7 @@ class LoggingTerm : public AbsTerm Op get_op() const override; Sort get_sort() const override; std::string to_string() override; - std::wstring getStringValue() override; + std::wstring getStringValue() const override; bool is_symbol() const override; bool is_param() const override; bool is_symbolic_const() const override; From 3334294a2c2bfb714f9f76aff8b5f87e4cfea6da Mon Sep 17 00:00:00 2001 From: ntsis Date: Mon, 30 Oct 2023 23:54:57 -0700 Subject: [PATCH 07/10] A minor fix --- include/generic_solver.h | 5 ----- include/generic_term.h | 1 - src/generic_solver.cpp | 20 -------------------- src/generic_term.cpp | 5 ----- 4 files changed, 31 deletions(-) diff --git a/include/generic_solver.h b/include/generic_solver.h index 68f148e8e..ce8cd6532 100644 --- a/include/generic_solver.h +++ b/include/generic_solver.h @@ -127,11 +127,6 @@ class GenericSolver : public AbsSmtSolver */ Term make_value(bool b) const; Term make_value(int64_t i, const Sort & sort) const; - 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_value(const std::string& s, bool useEscSequences, const Sort & sort) const; - Term make_value(const std::wstring& s, const Sort & sort) const; - Term make_value(const std::string val, const Sort & sort, uint64_t base = 10) const; diff --git a/include/generic_term.h b/include/generic_term.h index 842b2af32..39f153830 100644 --- a/include/generic_term.h +++ b/include/generic_term.h @@ -47,7 +47,6 @@ class GenericTerm : public AbsTerm Sort get_sort() const override; std::size_t get_id() const override; std::string to_string() override; - std::wstring getStringValue() override; std::size_t hash() const override; bool is_value() const override; uint64_t to_int() const override; diff --git a/src/generic_solver.cpp b/src/generic_solver.cpp index dad3c0a32..9ed6f70ea 100644 --- a/src/generic_solver.cpp +++ b/src/generic_solver.cpp @@ -851,26 +851,6 @@ Term GenericSolver::make_value(int64_t i, const Sort & sort) const } } -Term GenericSolver::make_term(const std::string& s, bool useEscSequences, const Sort & sort) const -{ - throw NotImplementedException("make_term not supported for strings with useEscSequences for this solver."); -} - -Term GenericSolver::make_term(const std::wstring& s, const Sort & sort) const -{ - throw NotImplementedException("make_term not supported for strings with wstring for this solver."); -} - -Term GenericSolver::make_value(const std::string& s, bool useEscSequences, const Sort & sort) const -{ - throw NotImplementedException("make_value not supported for strings with useEscSequences for this solver."); -} - -Term GenericSolver::make_value(const std::wstring& s, const Sort & sort) const -{ - throw NotImplementedException("make_value not supported for strings with wstring for this solver."); -} - Term GenericSolver::make_term(const string val, const Sort & sort, uint64_t base) const diff --git a/src/generic_term.cpp b/src/generic_term.cpp index 7757908cf..050129e24 100644 --- a/src/generic_term.cpp +++ b/src/generic_term.cpp @@ -141,11 +141,6 @@ string GenericTerm::to_string() return repr; } -wstring GenericTerm::getStringValue() -{ - throw NotImplementedException("GetStringValue not supported for this solver."); -} - size_t GenericTerm::hash() const { return str_hash(compute_string()); } // check if op is null because a non-value From 4f8cd82e45b5b5f0c5c3944906df3b2fcb85edd1 Mon Sep 17 00:00:00 2001 From: ntsis Date: Tue, 31 Oct 2023 11:33:38 -0700 Subject: [PATCH 08/10] Move a logging solver test to the string test --- tests/test-logging-solver.cpp | 39 ++--------------------------------- tests/test-str.cpp | 37 +++++++++++++++++++++++++++++++++ 2 files changed, 39 insertions(+), 37 deletions(-) diff --git a/tests/test-logging-solver.cpp b/tests/test-logging-solver.cpp index 50b5558d3..478e6ce5a 100644 --- a/tests/test-logging-solver.cpp +++ b/tests/test-logging-solver.cpp @@ -45,19 +45,15 @@ class LoggingTests : public ::testing::Test, bvsort8 = s->make_sort(BV, 8); arraysort = s->make_sort(ARRAY, bvsort4, bvsort8); funsort = s->make_sort(FUNCTION, SortVec{ bvsort4, bvsort8 }); - strsort = s->make_sort(STRING); x = s->make_symbol("x", bvsort4); y = s->make_symbol("y", bvsort4); zero = s->make_term(0, bvsort4); one = s->make_term(1, bvsort4); - t = s->make_symbol("t", strsort); - w = s->make_symbol("w", strsort); - strA = s->make_term("A", false, strsort); } SmtSolver s; - Sort bvsort4, bvsort8, arraysort, funsort, strsort; - Term x, y, zero, one, t, w, strA; + Sort bvsort4, bvsort8, arraysort, funsort; + Term x, y, zero, one; }; TEST_P(LoggingTests, Children) @@ -154,37 +150,6 @@ TEST_P(LoggingTests, Compare) EXPECT_EQ(fxv, fyv); } -TEST_P(LoggingTests, StrChildren) -{ - 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); -} - INSTANTIATE_TEST_SUITE_P( ParameterizedSolverLoggingTests, LoggingTests, diff --git a/tests/test-str.cpp b/tests/test-str.cpp index 404c75037..0280f7e92 100644 --- a/tests/test-str.cpp +++ b/tests/test-str.cpp @@ -44,6 +44,43 @@ class StrTests : public ::testing::Test, 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); From b19ec1dfc4f29304024f22be273f295dd7615d63 Mon Sep 17 00:00:00 2001 From: ntsis Date: Wed, 1 Nov 2023 10:10:09 -0700 Subject: [PATCH 09/10] Update include/ops.h Co-authored-by: yoni206 --- include/ops.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/ops.h b/include/ops.h index 99e8c4b5c..f3bae641a 100644 --- a/include/ops.h +++ b/include/ops.h @@ -98,7 +98,7 @@ enum PrimOp // BitVector Conversion BV_To_Nat, Int_To_BV, - //Strings + // Strings StrLt, StrLeq, StrLen, From 9a24bc702617e09e166aa7a9e5bbc5d7261abc1e Mon Sep 17 00:00:00 2001 From: ntsis Date: Wed, 1 Nov 2023 10:35:35 -0700 Subject: [PATCH 10/10] Minor changes --- cvc5/src/cvc5_solver.cpp | 9 ++++----- include/ops.h | 2 +- src/logging_solver.cpp | 3 +-- tests/cvc5/cvc5-str.cpp | 6 ++---- tests/test-str.cpp | 17 ++--------------- 5 files changed, 10 insertions(+), 27 deletions(-) diff --git a/cvc5/src/cvc5_solver.cpp b/cvc5/src/cvc5_solver.cpp index 5461ed365..c31698ced 100644 --- a/cvc5/src/cvc5_solver.cpp +++ b/cvc5/src/cvc5_solver.cpp @@ -92,12 +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 }, @@ -204,9 +205,7 @@ Term Cvc5Solver::make_term(const std::string& s, bool useEscSequences, const Sor } else { - std::string msg = "Can't create constant with string and useEscSequences"; - msg += useEscSequences; - msg += " for sort "; + std::string msg = "Can't create a string constant for sort "; msg += sort->to_string(); throw IncorrectUsageException(msg.c_str()); } @@ -232,7 +231,7 @@ Term Cvc5Solver::make_term(const std::wstring& s, const Sort & sort) const } else { - std::string msg = "Can't create constant with wstring for sort "; + std::string msg = "Can't create string constant for sort "; msg += sort->to_string(); throw IncorrectUsageException(msg.c_str()); } diff --git a/include/ops.h b/include/ops.h index 99e8c4b5c..f3bae641a 100644 --- a/include/ops.h +++ b/include/ops.h @@ -98,7 +98,7 @@ enum PrimOp // BitVector Conversion BV_To_Nat, Int_To_BV, - //Strings + // Strings StrLt, StrLeq, StrLen, diff --git a/src/logging_solver.cpp b/src/logging_solver.cpp index 4c5d7e13b..614a8866f 100644 --- a/src/logging_solver.cpp +++ b/src/logging_solver.cpp @@ -205,7 +205,6 @@ 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); @@ -225,6 +224,7 @@ Term LoggingSolver::make_term(const std::string& s, bool useEscSequences, const 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); @@ -244,7 +244,6 @@ Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{ return res; } - Term LoggingSolver::make_term(const string name, const Sort & sort, uint64_t base) const diff --git a/tests/cvc5/cvc5-str.cpp b/tests/cvc5/cvc5-str.cpp index 84f53d0d1..58b846348 100644 --- a/tests/cvc5/cvc5-str.cpp +++ b/tests/cvc5/cvc5-str.cpp @@ -8,10 +8,9 @@ ** 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 @@ -29,7 +28,6 @@ int main() { SmtSolver s = Cvc5SolverFactory::create(false); s->set_opt("produce-models", "true"); - //s->set_opt("strings-exp", "true"); s->set_logic("S"); Sort strsort = s->make_sort(STRING); Sort intsort = s->make_sort(INT); diff --git a/tests/test-str.cpp b/tests/test-str.cpp index 0280f7e92..a81b8a465 100644 --- a/tests/test-str.cpp +++ b/tests/test-str.cpp @@ -9,17 +9,13 @@ ** All rights reserved. See the file LICENSE in the top-level source ** directory for licensing information.\endverbatim ** -** \brief Tests for constants in theory of strings. -** -** +** \brief +** Tests for theory of strings. **/ #include #include -// use this line for printing wstrings -//#include - #include "available_solvers.h" #include "gtest/gtest.h" #include "smt.h" @@ -107,10 +103,6 @@ TEST_P(StrTests, EqualStrConsts) TEST_P(StrTests, UseEscSequences) { - // use these two lines for printing wstrings - //std::locale::global(std::locale("")); - //std::wcout.imbue(std::locale()); - Sort str_sort = s->make_sort(STRING); Term x1 = s->make_term("\\u{0021}", true, str_sort); @@ -126,11 +118,6 @@ TEST_P(StrTests, UseEscSequences) std::wstring wstrx3 = s->get_value(x3)->getStringValue(); std::wstring wstrx4 = s->get_value(x4)->getStringValue(); - - // an example of printing wstrx1 - //std::cout << x1 << " = "; - //std::wcout << wstrx1 << std::endl; - assert(wstrx1.find(wchar_u) == std::wstring::npos); assert(wstrx2.find(wchar_u) == std::wstring::npos); assert(wstrx3.find(wchar_u) != std::wstring::npos);