Add partial string support #327

ntsis · 2023-08-25T16:35:28Z

Added string support for StrLt "str.<", StrLeq "str.<=", StrLen "str.len", StrConcat, "str.++".

Also, added support for IntDiv, ::cvc5::INTS_DIVISION, FLOAT parsing, and made changes to TermTranslator::infixize_rational.

yoni206

Thanks for doing this! We have been wanting this for a while...
Some general comments:

We don't have a strict clang-format policy, we still some lines look too long, it is better to try keep it under 80 characters per line. Also, clang-formatting of course wouldn't hurt (but not necessary).
You might want to split this PR to 2 PRs -- the string related stuff and the other stuff. But up to you.
While the implementation generally looks fine to me, it is really hard to tell if it works without tests. It would be great if you could add tests that exercise every function that you've implemented. You can find examples in the tests directory.

yoni206 · 2023-08-25T17:41:19Z

contrib/setup-cvc5.sh

+#    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


I am not sure this is what we want to do.
If the directory already exists, then this would probably mean that cvc5 is already built in it, no?

yoni206 · 2023-08-25T17:46:09Z

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


This comment is not very clear. What is the string constructor? And what does useEscSequences mean? It might be the case that this documentation line is too specific to cvc5, while it should be more general.

include/solver.h

yoni206 · 2023-08-25T17:48:31Z

include/solver.h

+   */  
+  virtual Term make_term(const std::wstring& s, const Sort & sort) const{
+        throw NotImplementedException("Strings not supported for this solver.");
+


Suggested change

yoni206 · 2023-08-25T17:56:39Z

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 },


I wonder -- integer division is already tested, including with cvc5:

smt-switch/tests/test-int.cpp

Line 49 in f2d7d3d

Term div = s->make_term(IntDiv, five, two);

How come we need to add it now?

include/ops.h

yoni206 · 2023-08-25T18:00:00Z

src/generic_solver.cpp

+{
+  Term value_term = make_value(s, useEscSequences, sort);
+  return store_term(value_term);
+}


Suggested change

}

}

yoni206 · 2023-08-25T18:01:29Z

src/generic_solver.cpp

+  assert(sk == STRING);
+  string repr;
+  repr = std::to_string(s);
+  Term term = std::make_shared<GenericTerm>(sort, Op(), TermVec{}, repr); //figure out how to handle useEscSequences


Is this figured out yet? :)
If not -- what exactly is the issue?
If so, the comment can be removed.

yoni206 · 2023-08-25T18:02:18Z

src/generic_solver.cpp

+  SortKind sk = sort->get_sort_kind();
+  assert(sk == STRING);
+  string repr;
+  repr = std::to_string(s);


Will that always work? Is it always possible to convert a wstring to a string?

…t for strings in generic solver in this PR

…o add-strings The changes are caused by resolving conflict with main.

yoni206

Looks great, a few final minor comments.

yoni206 · 2023-11-01T08:14:12Z

cvc5/src/cvc5_solver.cpp

+      std::string msg = "Can't create constant with string and useEscSequences";
+      msg += useEscSequences;


Suggested change

std::string msg = "Can't create constant with string and useEscSequences";

msg += useEscSequences;

std::string msg = "Can't create a string constant

yoni206 · 2023-11-01T08:14:43Z

cvc5/src/cvc5_solver.cpp

+    }    
+    else
+    {
+      std::string msg = "Can't create constant with wstring for sort ";


Suggested change

std::string msg = "Can't create constant with wstring for sort ";

std::string msg = "Can't create string constant for sort ";

yoni206 · 2023-11-01T08:17:24Z

cvc5/src/cvc5_solver.cpp

      // Indexed Op
      { Int_To_BV, ::cvc5::Kind::INT_TO_BITVECTOR },
+      { StrLt, ::cvc5::Kind::STRING_LT },
+      { StrLeq, ::cvc5::Kind::STRING_LEQ },
+      { StrLen, ::cvc5::Kind::STRING_LENGTH }, 
+      { StrConcat, ::cvc5::Kind::STRING_CONCAT },


Suggested change

// Indexed Op

{ Int_To_BV, ::cvc5::Kind::INT_TO_BITVECTOR },

{ StrLt, ::cvc5::Kind::STRING_LT },

{ StrLeq, ::cvc5::Kind::STRING_LEQ },

{ StrLen, ::cvc5::Kind::STRING_LENGTH },

{ StrConcat, ::cvc5::Kind::STRING_CONCAT },

// String Op

{ StrLt, ::cvc5::Kind::STRING_LT },

{ StrLeq, ::cvc5::Kind::STRING_LEQ },

{ StrLen, ::cvc5::Kind::STRING_LENGTH },

{ StrConcat, ::cvc5::Kind::STRING_CONCAT },

// Indexed Op

{ Int_To_BV, ::cvc5::Kind::INT_TO_BITVECTOR },

yoni206 · 2023-11-01T08:19:20Z

src/logging_solver.cpp

+
+  return res;
+}
+Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{


Suggested change

Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{

Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{

yoni206 · 2023-11-01T08:21:00Z

tests/cvc5/cvc5-str.cpp

+** directory for licensing information.\endverbatim
+**
+** \brief
+**


Suggested change

**

** Tests for strings in the cvc5 backend.

yoni206 · 2023-11-01T08:21:37Z

tests/cvc5/cvc5-str.cpp

+{
+  SmtSolver s = Cvc5SolverFactory::create(false);
+  s->set_opt("produce-models", "true");
+  //s->set_opt("strings-exp", "true");


Suggested change

//s->set_opt("strings-exp", "true");

yoni206 · 2023-11-01T08:23:30Z

tests/test-str.cpp

+// use this line for printing wstrings
+//#include <locale>


Suggested change

// use this line for printing wstrings

//#include <locale>

yoni206 · 2023-11-01T08:24:05Z

tests/test-str.cpp

+  // an example of printing wstrx1
+  //std::cout << x1 << " = "; 
+  //std::wcout << wstrx1 << std::endl;


Suggested change

// an example of printing wstrx1

//std::cout << x1 << " = ";

//std::wcout << wstrx1 << std::endl;

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

…o add-strings Minor change

yoni206 · 2023-11-01T18:48:27Z

Added string support for StrLt "str.<", StrLeq "str.<=", StrLen "str.len", StrConcat, "str.++".

Add partial string support

1a24094

yoni206 requested changes Aug 25, 2023

View reviewed changes

ntsis added 9 commits October 20, 2023 11:35

Add tests for strings

81ac8e8

Add string tests for escape sequences. Make the PR smaller. No suppor…

c0c66ae

…t for strings in generic solver in this PR

A bug fix

88a943f

Merge branch 'master' into add-strings

c0f950f

Resolve git checks

1764e7e

Merge branch 'add-strings' of https://github.com/ntsis/smt-switch int…

8627d1e

…o add-strings The changes are caused by resolving conflict with main.

Missed to add to the previous push

bbe5eb7

A minor fix

3334294

Move a logging solver test to the string test

4f8cd82

yoni206 requested changes Nov 1, 2023

View reviewed changes

ntsis and others added 3 commits November 1, 2023 10:10

Update include/ops.h

b19ec1d

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

Minor changes

9a24bc7

Merge branch 'add-strings' of https://github.com/ntsis/smt-switch int…

b312a48

…o add-strings Minor change

yoni206 approved these changes Nov 1, 2023

View reviewed changes

yoni206 merged commit a019770 into stanford-centaur:master Nov 1, 2023
10 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add partial string support #327

Add partial string support #327

ntsis commented Aug 25, 2023

yoni206 left a comment

yoni206 Aug 25, 2023

yoni206 Aug 25, 2023

yoni206 Aug 25, 2023

yoni206 Aug 25, 2023

yoni206 Aug 25, 2023

yoni206 Aug 25, 2023

yoni206 Aug 25, 2023

yoni206 left a comment

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 Nov 1, 2023

yoni206 commented Nov 1, 2023

		std::string msg = "Can't create constant with string and useEscSequences";
		msg += useEscSequences;

	std::string msg = "Can't create constant with string and useEscSequences";
	msg += useEscSequences;
	std::string msg = "Can't create a string constant

	std::string msg = "Can't create constant with wstring for sort ";
	std::string msg = "Can't create string constant for sort ";

	Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{

	Term LoggingSolver::make_term(const std::wstring& s, const Sort & sort) const{

	// an example of printing wstrx1
	//std::cout << x1 << " = ";
	//std::wcout << wstrx1 << std::endl;

Add partial string support #327

Add partial string support #327

Conversation

ntsis commented Aug 25, 2023

yoni206 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yoni206 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yoni206 commented Nov 1, 2023