From f5e3739358b98d9a6ebc16fbc5aed9edee1483dc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 May 2018 14:50:47 -0500 Subject: [PATCH] Support for str.<= and str.< (#1882) --- src/parser/smt2/smt2.cpp | 2 + src/printer/smt2/smt2_printer.cpp | 5 ++ src/theory/strings/kinds | 6 +- src/theory/strings/theory_strings.cpp | 53 +++++++++------ src/theory/strings/theory_strings.h | 1 + .../strings/theory_strings_preprocess.cpp | 59 ++++++++++++++++- .../strings/theory_strings_preprocess.h | 1 + .../strings/theory_strings_rewriter.cpp | 66 +++++++++++++++++++ src/theory/strings/theory_strings_rewriter.h | 6 ++ .../strings/theory_strings_type_rules.h | 11 ++-- src/util/regexp.cpp | 20 ++++++ src/util/regexp.h | 2 + test/regress/Makefile.tests | 4 ++ .../regress0/strings/code-sat-neg-one.smt2 | 7 ++ .../strings/strings-leq-trans-unsat.smt2 | 14 ++++ .../regress1/strings/strings-lt-len5.smt2 | 9 +++ .../regress1/strings/strings-lt-simple.smt2 | 8 +++ 17 files changed, 248 insertions(+), 26 deletions(-) create mode 100644 test/regress/regress0/strings/code-sat-neg-one.smt2 create mode 100644 test/regress/regress1/strings/strings-leq-trans-unsat.smt2 create mode 100644 test/regress/regress1/strings/strings-lt-len5.smt2 create mode 100644 test/regress/regress1/strings/strings-lt-simple.smt2 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 09dccdfbd..133cc12c1 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -154,6 +154,8 @@ void Smt2::addStringOperators() { addOperator(kind::REGEXP_RANGE, "re.range"); addOperator(kind::REGEXP_LOOP, "re.loop"); addOperator(kind::STRING_CODE, "str.code"); + addOperator(kind::STRING_LT, "str.<"); + addOperator(kind::STRING_LEQ, "str.<="); } void Smt2::addFloatingPointOperators() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2c6a26335..36076ec3c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -521,6 +521,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::STRING_STRREPL: case kind::STRING_PREFIX: case kind::STRING_SUFFIX: + case kind::STRING_LEQ: + case kind::STRING_LT: case kind::STRING_ITOS: case kind::STRING_STOI: case kind::STRING_CODE: @@ -1061,6 +1063,9 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_STRREPL: return "str.replace" ; case kind::STRING_PREFIX: return "str.prefixof" ; case kind::STRING_SUFFIX: return "str.suffixof" ; + case kind::STRING_LEQ: return "str.<="; + case kind::STRING_LT: return "str.<"; + case kind::STRING_CODE: return "str.code"; case kind::STRING_ITOS: return v == smt2_6_1_variant ? "str.from-int" : "int.to.str"; case kind::STRING_STOI: diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 34237f69e..d931e99bc 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -18,6 +18,8 @@ operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr" operator STRING_CHARAT 2 "string charat" operator STRING_STRCTN 2 "string contains" +operator STRING_LT 2 "string less than" +operator STRING_LEQ 2 "string less than or equal" operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" operator STRING_PREFIX 2 "string prefixof" @@ -97,7 +99,9 @@ typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule -typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule +typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule +typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule +typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b77a616b3..3da652457 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -124,6 +124,7 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_STRREPL); getExtTheory()->addFunctionKind(kind::STRING_STRCTN); getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); + getExtTheory()->addFunctionKind(kind::STRING_LEQ); getExtTheory()->addFunctionKind(kind::STRING_CODE); // The kinds we are treating as function application in congruence @@ -133,6 +134,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_CODE); if( options::stringLazyPreproc() ){ d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); + d_equalityEngine.addFunctionKind(kind::STRING_LEQ); d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); d_equalityEngine.addFunctionKind(kind::STRING_ITOS); d_equalityEngine.addFunctionKind(kind::STRING_STOI); @@ -142,6 +144,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); std::vector< Node > nvec; d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); @@ -436,7 +439,8 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI - || k == STRING_STRREPL); + || k == STRING_STRREPL + || k == STRING_LEQ); std::vector< Node > new_nodes; Node res = d_preproc.simplify( n, new_nodes ); Assert( res!=n ); @@ -547,8 +551,9 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Assert(d_normal_forms.find(eqc) != d_normal_forms.end()); if (d_normal_forms[eqc].size() == 1) { - // does it have a code? - if (d_has_str_code) + // does it have a code and the length of these equivalence classes are + // one? + if (d_has_str_code && lts_values[i] == d_one) { EqcInfo* eip = getOrMakeEqcInfo(eqc, false); if (eip && !eip->d_code_term.get().isNull()) @@ -563,7 +568,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) vec.push_back(String::convertCodeToUnsignedInt(cvalue)); Node mv = nm->mkConst(String(vec)); pure_eq_assign[eqc] = mv; - m->getEqualityEngine()->addTerm( mv ); + m->getEqualityEngine()->addTerm(mv); } } pure_eq.push_back(eqc); @@ -579,7 +584,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) //assign a new length if necessary if( !pure_eq.empty() ){ if( lts_values[i].isNull() ){ - unsigned lvalue = 0; + // start with length two (other lengths have special precendence) + unsigned lvalue = 2; while( values_used.find( lvalue )!=values_used.end() ){ lvalue++; } @@ -671,16 +677,22 @@ void TheoryStrings::preRegisterTerm(TNode n) { if( d_pregistered_terms_cache.find(n) == d_pregistered_terms_cache.end() ) { d_pregistered_terms_cache.insert(n); //check for logic exceptions + Kind k = n.getKind(); if( !options::stringExp() ){ - if( n.getKind()==kind::STRING_STRIDOF || - n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_STOI || - n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){ + if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS + || k == kind::STRING_STOI + || k == kind::STRING_STRREPL + || k == kind::STRING_STRCTN + || k == STRING_LEQ) + { std::stringstream ss; - ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp"; + ss << "Term of kind " << k + << " not supported in default mode, try --strings-exp"; throw LogicException(ss.str()); } } - switch( n.getKind() ) { + switch (k) + { case kind::EQUAL: { d_equalityEngine.addTriggerEquality(n); break; @@ -702,7 +714,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { // not belong to this theory. if (options::stringFMF() && (n.isVar() ? d_all_skolems.find(n) == d_all_skolems.end() - : kindToTheoryId(n.getKind()) != THEORY_STRINGS)) + : kindToTheoryId(k) != THEORY_STRINGS)) { d_input_vars.insert(n); } @@ -720,7 +732,9 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } //concat terms do not contribute to theory combination? TODO: verify - if( n.hasOperator() && kindToTheoryId( n.getKind() )==THEORY_STRINGS && n.getKind()!=kind::STRING_CONCAT ){ + if (n.hasOperator() && kindToTheoryId(k) == THEORY_STRINGS + && k != kind::STRING_CONCAT) + { d_functionsTerms.push_back( n ); } } @@ -2218,13 +2232,15 @@ void TheoryStrings::checkNormalForms(){ cmps.pop_back(); for (const Node& c2 : cmps) { - Trace("strings-code-debug") << "Compare codes : " << c1 << " " << c2 - << std::endl; - if (!areDisequal(c1, c2)) + Trace("strings-code-debug") + << "Compare codes : " << c1 << " " << c2 << std::endl; + if (!areDisequal(c1, c2) && !areEqual(c1, d_neg_one)) { + Node eq_no = c1.eqNode(d_neg_one); + Node deq = c1.eqNode(c2).negate(); Node eqn = c1[0].eqNode(c2[0]); - Node eq = c1.eqNode(c2); - Node inj_lem = nm->mkNode(kind::OR, eq.negate(), eqn); + // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y + Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); sendInference(d_empty_vec, inj_lem, "Code_Inj"); } } @@ -3520,9 +3536,8 @@ void TheoryStrings::registerTerm( Node n, int effort ) { d_has_str_code = true; NodeManager* nm = NodeManager::currentNM(); // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 ) - Node neg_one = nm->mkConst(Rational(-1)); Node code_len = mkLength(n[0]).eqNode(d_one); - Node code_eq_neg1 = n.eqNode(nm->mkConst(Rational(-1))); + Node code_eq_neg1 = n.eqNode(d_neg_one); Node code_range = nm->mkNode( kind::AND, nm->mkNode(kind::GEQ, n, d_zero), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 85d2754a8..bd5a797ae 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -196,6 +196,7 @@ private: Node d_false; Node d_zero; Node d_one; + Node d_neg_one; CVC4::Rational RMAXINT; unsigned d_card_size; // Helper functions diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d412eaa33..fac7fccf2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -23,6 +23,8 @@ #include "proof/proof_manager.h" #include "smt/logic_exception.h" +using namespace CVC4; +using namespace CVC4::kind; namespace CVC4 { namespace theory { @@ -30,8 +32,9 @@ namespace strings { StringsPreprocess::StringsPreprocess( context::UserContext* u ){ //Constants - d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + d_empty_str = NodeManager::currentNM()->mkConst(String("")); } StringsPreprocess::~StringsPreprocess(){ @@ -472,6 +475,58 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { ); retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body ); } + else if (t.getKind() == kind::STRING_LEQ) + { + Node ltp = nm->mkSkolem("ltp", nm->booleanType()); + Node k = nm->mkSkolem("k", nm->integerType()); + + std::vector conj; + conj.push_back(nm->mkNode(GEQ, k, d_zero)); + Node substr[2]; + Node code[2]; + for (unsigned r = 0; r < 2; r++) + { + Node ta = t[r]; + Node tb = t[1 - r]; + substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k); + code[r] = + nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one)); + conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta))); + } + conj.push_back(substr[0].eqNode(substr[1])); + std::vector ite_ch; + ite_ch.push_back(ltp); + for (unsigned r = 0; r < 2; r++) + { + ite_ch.push_back(nm->mkNode(LT, code[r], code[1 - r])); + } + conj.push_back(nm->mkNode(ITE, ite_ch)); + + // Intuitively, the reduction says either x and y are equal, or they have + // some (maximal) common prefix after which their characters at position k + // are distinct, and the comparison of their code matches the return value + // of the overall term. + // Notice the below reduction relies on the semantics of str.code being -1 + // for the empty string. In particular, say x = "a" and y = "ab", then the + // reduction below is satisfied for k = 1, since + // str.code(substr( "a", 1, 1 )) = str.code( "" ) = -1 < + // str.code(substr( "ab", 1, 1 )) = str.code( "b" ) = 66 + + // assert: + // IF x=y + // THEN: ltp + // ELSE: k >= 0 AND k <= len( x ) AND k <= len( y ) AND + // substr( x, 0, k ) = substr( y, 0, k ) AND + // IF ltp + // THEN: str.code(substr( x, k, 1 )) < str.code(substr( y, k, 1 )) + // ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 )) + Node assert = + nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj)); + new_nodes.push_back(assert); + + // Thus, str.<=( x, y ) = p_lt + retNode = ltp; + } if( t!=retNode ){ Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 41987265e..d342cba72 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -33,6 +33,7 @@ class StringsPreprocess { //Constants Node d_zero; Node d_one; + Node d_empty_str; //mapping from kinds to UF std::map< Kind, std::map< unsigned, Node > > d_uf; //get UF for node diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index cfd0f6e73..a426c0306 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1176,6 +1176,18 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = rewriteSubstr(node); }else if( node.getKind() == kind::STRING_STRCTN ){ retNode = rewriteContains( node ); + } + else if (node.getKind() == kind::STRING_LT) + { + NodeManager* nm = NodeManager::currentNM(); + // eliminate s < t ---> s != t AND s <= t + retNode = nm->mkNode(AND, + node[0].eqNode(node[1]).negate(), + nm->mkNode(STRING_LEQ, node[0], node[1])); + } + else if (node.getKind() == kind::STRING_LEQ) + { + retNode = rewriteStringLeq(node); }else if( node.getKind()==kind::STRING_STRIDOF ){ retNode = rewriteIndexof( node ); }else if( node.getKind() == kind::STRING_STRREPL ){ @@ -2187,6 +2199,60 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return node; } +Node TheoryStringsRewriter::rewriteStringLeq(Node n) +{ + Assert(n.getKind() == kind::STRING_LEQ); + NodeManager* nm = NodeManager::currentNM(); + if (n[0] == n[1]) + { + Node ret = nm->mkConst(true); + return returnRewrite(n, ret, "str-leq-id"); + } + if (n[0].isConst() && n[1].isConst()) + { + String s = n[0].getConst(); + String t = n[1].getConst(); + Node ret = nm->mkConst(s.isLeq(t)); + return returnRewrite(n, ret, "str-leq-eval"); + } + // empty strings + for (unsigned i = 0; i < 2; i++) + { + if (n[i].isConst() && n[i].getConst().isEmptyString()) + { + Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]); + return returnRewrite(n, ret, "str-leq-empty"); + } + } + + std::vector n1; + getConcat(n[0], n1); + std::vector n2; + getConcat(n[1], n2); + Assert(!n1.empty() && !n2.empty()); + + // constant prefixes + if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0]) + { + String s = n1[0].getConst(); + String t = n2[0].getConst(); + // only need to truncate if s is longer + if (s.size() > t.size()) + { + s = s.prefix(t.size()); + } + // if prefix is not leq, then entire string is not leq + if (!s.isLeq(t)) + { + Node ret = nm->mkConst(false); + return returnRewrite(n, ret, "str-leq-cprefix"); + } + } + + Trace("strings-rewrite-nf") << "No rewrites for : " << n << std::endl; + return n; +} + Node TheoryStringsRewriter::rewritePrefixSuffix(Node n) { Assert(n.getKind() == kind::STRING_PREFIX diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index f7e65f3a9..8befb5e0f 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -103,6 +103,12 @@ private: * Returns the rewritten form of node. */ static Node rewriteReplace(Node node); + /** rewrite string less than or equal + * This is the entry point for post-rewriting terms n of the form + * str.<=( t, s ) + * Returns the rewritten form of n. + */ + static Node rewriteStringLeq(Node n); /** rewrite prefix/suffix * This is the entry point for post-rewriting terms n of the form * str.prefixof( s, t ) / str.suffixof( s, t ) diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index b4629b338..e9e87f29a 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -91,18 +91,21 @@ public: } }; -class StringContainTypeRule { -public: +class StringRelationTypeRule +{ + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting an original string term in string contain"); + throw TypeCheckingExceptionPrivate( + n, "expecting a string term in string relation"); } t = n[1].getType(check); if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain"); + throw TypeCheckingExceptionPrivate( + n, "expecting a string term in string relation"); } } return nodeManager->booleanType(); diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 4cbda5147..bfd9cc3a7 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -298,6 +298,26 @@ std::string String::toString(bool useEscSequences) const { return str; } +bool String::isLeq(const String &y) const +{ + for (unsigned i = 0; i < size(); ++i) + { + if (i >= y.size()) + { + return false; + } + if (d_str[i] > y.d_str[i]) + { + return false; + } + if (d_str[i] < y.d_str[i]) + { + return true; + } + } + return true; +} + bool String::isRepeated() const { if (size() > 1) { unsigned int f = d_str[0]; diff --git a/src/util/regexp.h b/src/util/regexp.h index c8b491475..8b99dfd87 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -131,6 +131,8 @@ class CVC4_PUBLIC String { bool empty() const { return d_str.empty(); } /** is this the empty string? */ bool isEmptyString() const { return empty(); } + /** is less than or equal to string y */ + bool isLeq(const String& y) const; /** Return the length of the string */ std::size_t size() const { return d_str.size(); } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 8584eeca9..cf702ed7c 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -776,6 +776,7 @@ REG0_TESTS = \ regress0/strings/bug002.smt2 \ regress0/strings/bug612.smt2 \ regress0/strings/bug613.smt2 \ + regress0/strings/code-sat-neg-one.smt2 \ regress0/strings/escchar.smt2 \ regress0/strings/escchar_25.smt2 \ regress0/strings/idof-rewrites.smt2 \ @@ -1452,6 +1453,9 @@ REG1_TESTS = \ regress1/strings/str007.smt2 \ regress1/strings/string-unsound-sem.smt2 \ regress1/strings/strings-index-empty.smt2 \ + regress1/strings/strings-leq-trans-unsat.smt2 \ + regress1/strings/strings-lt-len5.smt2 \ + regress1/strings/strings-lt-simple.smt2 \ regress1/strings/strip-endpt-sound.smt2 \ regress1/strings/str-code-sat.smt2 \ regress1/strings/str-code-unsat.smt2 \ diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2 new file mode 100644 index 000000000..c69276a4f --- /dev/null +++ b/test/regress/regress0/strings/code-sat-neg-one.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(assert (not (= x y))) +(assert (= (str.code x) (str.code y))) +(check-sat) diff --git a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 new file mode 100644 index 000000000..de3946ef0 --- /dev/null +++ b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(assert (str.<= x y)) +(assert (str.<= y w)) +(declare-fun xp () String) +(assert (= x (str.++ "G" xp))) +(assert (= w "E")) +(check-sat) diff --git a/test/regress/regress1/strings/strings-lt-len5.smt2 b/test/regress/regress1/strings/strings-lt-len5.smt2 new file mode 100644 index 000000000..aeabfdf75 --- /dev/null +++ b/test/regress/regress1/strings/strings-lt-len5.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun y () String) +(assert (> (str.len y) 5)) +(assert (str.< "ACAAB" y)) +(assert (str.< y "ACAAD")) +(check-sat) diff --git a/test/regress/regress1/strings/strings-lt-simple.smt2 b/test/regress/regress1/strings/strings-lt-simple.smt2 new file mode 100644 index 000000000..e077cf1f7 --- /dev/null +++ b/test/regress/regress1/strings/strings-lt-simple.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun y () String) +(assert (str.< "AC" y)) +(assert (str.< y "AF")) +(check-sat) -- 2.30.2