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() {
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:
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:
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"
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
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
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);
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 );
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 );
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())
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);
//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++;
}
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;
// 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);
}
}
}
//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 );
}
}
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");
}
}
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),
Node d_false;
Node d_zero;
Node d_one;
+ Node d_neg_one;
CVC4::Rational RMAXINT;
unsigned d_card_size;
// Helper functions
#include "proof/proof_manager.h"
#include "smt/logic_exception.h"
+using namespace CVC4;
+using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
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(){
);
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<Node> 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<Node> 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;
//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
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 ){
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>();
+ String t = n[1].getConst<String>();
+ 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<String>().isEmptyString())
+ {
+ Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
+ return returnRewrite(n, ret, "str-leq-empty");
+ }
+ }
+
+ std::vector<Node> n1;
+ getConcat(n[0], n1);
+ std::vector<Node> 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>();
+ String t = n2[0].getConst<String>();
+ // 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
* 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 )
}
};
-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();
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];
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(); }
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 \
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 \
--- /dev/null
+(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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff