diff options
43 files changed, 2852 insertions, 44 deletions
@@ -14,6 +14,7 @@ Changes since 1.2 resolved. * New :command-verbosity SMT option to silence success and error messages on a per-command basis. API changes to Command infrastructure to support. +* A new theory of strings. Currently, only word equations are supported. Changes since 1.1 ================= diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 1ac277667..2b552684a 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1066,8 +1066,8 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { - bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF"; - bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF"; + bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF"; + bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF"; CVC4::CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); CVC4::CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator()); @@ -1197,7 +1197,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, CVC4::CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); for(unsigned k = 0; k < selectors[i][j].size(); ++k) { if(types[i][j][k].getType().isString()) { - ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<string>())); + ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<CVC4::String>().toString())); } else { ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k])); } @@ -1307,12 +1307,12 @@ Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) { } Expr ValidityChecker::stringExpr(const std::string& str) { - return d_em->mkConst(str); + return d_em->mkConst(CVC4::String(str)); } Expr ValidityChecker::idExpr(const std::string& name) { // represent as a string expr, CVC4 doesn't have id exprs - return d_em->mkConst(name); + return d_em->mkConst(CVC4::String(name)); } Expr ValidityChecker::listExpr(const std::vector<Expr>& kids) { @@ -1333,21 +1333,21 @@ Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) { Expr ValidityChecker::listExpr(const std::string& op, const std::vector<Expr>& kids) { - return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), vector<CVC4::Expr>(kids.begin(), kids.end())); + return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(CVC4::String(op)), vector<CVC4::Expr>(kids.begin(), kids.end())); } Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1) { - return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), e1); + return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(CVC4::String(op)), e1); } Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1, const Expr& e2) { - return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), e1, e2); + return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(CVC4::String(op)), e1, e2); } Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1, const Expr& e2, const Expr& e3) { - return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), e1, e2, e3); + return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(CVC4::String(op)), e1, e2, e3); } void ValidityChecker::printExpr(const Expr& e) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index a65655501..31f6d75d9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -683,6 +683,9 @@ public: /** Get the (singleton) type for strings. */ inline TypeNode stringType(); + /** Get the (singleton) type for RegExp. */ + inline TypeNode regexpType(); + /** Get the bound var list type. */ inline TypeNode boundVarListType(); @@ -1030,6 +1033,11 @@ inline TypeNode NodeManager::stringType() { return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE)); } +/** Get the (singleton) type for regexps. */ +inline TypeNode NodeManager::regexpType() { + return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE)); +} + /** Get the bound var list type. */ inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 061e73fc9..322f7ad92 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -554,6 +554,9 @@ public: /** Get the constituent types of a symbolic expression type */ std::vector<TypeNode> getSExprTypes() const; + /** Is this a regexp type */ + bool isRegExp() const; + /** Is this a bit-vector type */ bool isBitVector() const; @@ -842,6 +845,12 @@ inline bool TypeNode::isString() const { getConst<TypeConstant>() == STRING_TYPE; } +/** Is this a regexp type */ +inline bool TypeNode::isRegExp() const { + return getKind() == kind::TYPE_CONSTANT && + getConst<TypeConstant>() == REGEXP_TYPE; +} + inline bool TypeNode::isArray() const { return getKind() == kind::ARRAY_TYPE; } diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 670718e4e..5b0894680 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -23,6 +23,8 @@ OPTIONS_FILES_SRCS = \ ../theory/quantifiers/options.h \ ../theory/rewriterules/options.cpp \ ../theory/rewriterules/options.h \ + ../theory/strings/options.cpp \ + ../theory/strings/options.h \ ../prop/options.cpp \ ../prop/options.h \ ../proof/options.cpp \ @@ -82,6 +84,8 @@ nodist_liboptions_la_SOURCES = \ ../theory/quantifiers/options.h \ ../theory/rewriterules/options.cpp \ ../theory/rewriterules/options.h \ + ../theory/strings/options.cpp \ + ../theory/strings/options.h \ ../prop/options.cpp \ ../prop/options.h \ ../proof/options.cpp \ diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 41b0523bd..c9bbd3860 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: Christopher L. Conway - ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Clark Barrett + ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Clark Barrett, Tianyi Liang ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -39,6 +39,7 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne logicMap["QF_NIA"] = QF_NIA; logicMap["QF_NRA"] = QF_NRA; logicMap["QF_RDL"] = QF_RDL; + logicMap["QF_S"] = QF_S; logicMap["QF_SAT"] = QF_SAT; logicMap["QF_UF"] = QF_UF; logicMap["QF_UFIDL"] = QF_UFIDL; @@ -180,6 +181,10 @@ void Smt1::setLogic(const std::string& name) { d_logic = toLogic(name); switch(d_logic) { + case QF_S: + throw ParserException("Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2."); + break; + case QF_AX: addTheory(THEORY_ARRAYS_EX); break; diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index d6961371a..f96a4e810 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: Christopher L. Conway - ** Minor contributors (to current version): Clark Barrett + ** Minor contributors (to current version): Clark Barrett, Tianyi Liang ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -52,6 +52,7 @@ public: QF_NIA, QF_NRA, QF_RDL, + QF_S, // nonstandard (for string theory) QF_SAT, QF_UF, QF_UFIDL, @@ -82,6 +83,7 @@ public: THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX, THEORY_REALS, THEORY_REALS_INTS, + THEORY_STRINGS, THEORY_QUANTIFIERS }; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a6a2aa58c..74434f499 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Christopher L. Conway ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds, Francois Bobot + ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds, Francois Bobot, Tianyi Liang ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -452,7 +452,7 @@ extendedCommand[CVC4::Command*& cmd] : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } { /* open a scope to keep the UnresolvedTypes contained */ PARSER_STATE->pushScope(true); } - LPAREN_TOK /* parametric sorts */ + LPAREN_TOK /* parametric sorts */ ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { sorts.push_back( PARSER_STATE->mkSort(name) ); } )* @@ -697,6 +697,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] @declarations { CVC4::Kind k; std::string s; + std::vector<unsigned int> s_vec; } : INTEGER_LITERAL { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } @@ -704,6 +705,13 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } | str[s] { sexpr = SExpr(s); } +// | LPAREN_TOK STRCST_TOK +// ( INTEGER_LITERAL { +// s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 ); +// } )* RPAREN_TOK +// { +// sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) ); +// } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) @@ -757,6 +765,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::hash_set<std::string, StringHashFunction> names; std::vector< std::pair<std::string, Expr> > binders; Type type; + std::string s; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -1011,6 +1020,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } + | str[s] + { expr = MK_CONST( ::CVC4::String(s) ); } + // NOTE: Theory constants go here ; @@ -1222,6 +1234,17 @@ builtinOp[CVC4::Kind& kind] | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } + | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } + | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } + | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } + | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } + | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } + | REOR_TOK { $kind = CVC4::kind::REGEXP_OR; } + | REINTER_TOK { $kind = CVC4::kind::REGEXP_INTER; } + | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; } + | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } + | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; } + // NOTE: Theory operators go here ; @@ -1579,6 +1602,19 @@ BVSLE_TOK : 'bvsle'; BVSGT_TOK : 'bvsgt'; BVSGE_TOK : 'bvsge'; +//STRING +STRCST_TOK : 'str.const'; +STRCON_TOK : 'str.++'; +STRLEN_TOK : 'str.len'; +STRINRE_TOK : 'str.in.re'; +STRTORE_TOK : 'str.to.re'; +RECON_TOK : 're.++'; +REOR_TOK : 're.or'; +REINTER_TOK : 're.inter'; +RESTAR_TOK : 're.*'; +REPLUS_TOK : 're.+'; +REOPT_TOK : 're.opt'; + /** * A sequence of printable ASCII characters (except backslash) that starts * and ends with | and does not otherwise contain |. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7a1fdf174..db242d101 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -86,6 +86,12 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_ROTATE_RIGHT); } +void Smt2::addStringOperators() { + addOperator(kind::STRING_CONCAT); + addOperator(kind::STRING_LENGTH); + //addOperator(kind::STRING_IN_REGEXP); +} + void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_CORE: @@ -135,6 +141,11 @@ void Smt2::addTheory(Theory theory) { addBitvectorOperators(); break; + case THEORY_STRINGS: + defineType("String", getExprManager()->stringType()); + addStringOperators(); + break; + case THEORY_QUANTIFIERS: break; @@ -180,6 +191,10 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); } + if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { + addTheory(THEORY_STRINGS); + } + if(d_logic.isQuantified()) { addTheory(THEORY_QUANTIFIERS); } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 3f1d3b087..cc46efe07 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -44,6 +44,7 @@ public: THEORY_REALS, THEORY_REALS_INTS, THEORY_QUANTIFIERS, + THEORY_STRINGS }; private: @@ -127,6 +128,8 @@ private: void addBitvectorOperators(); + void addStringOperators(); + };/* class Smt2 */ }/* CVC4::parser namespace */ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 2df698da4..860075aa8 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl +SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl strings DIST_SUBDIRS = $(SUBDIRS) example noinst_LTLIBRARIES = libtheory.la @@ -61,7 +61,8 @@ libtheory_la_LIBADD = \ @builddir@/datatypes/libdatatypes.la \ @builddir@/quantifiers/libquantifiers.la \ @builddir@/rewriterules/librewriterules.la \ - @builddir@/idl/libidl.la + @builddir@/idl/libidl.la \ + @builddir@/strings/libstrings.la EXTRA_DIST = \ logic_info.i \ diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 6a6fb2e31..b51feea6d 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -326,23 +326,6 @@ well-founded SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -# These will eventually move to a theory of strings. -# -# For now these are unbounded strings over a fixed, finite alphabet -# (this may change). -sort STRING_TYPE \ - Cardinality::INTEGERS \ - well-founded \ - "NodeManager::currentNM()->mkConst(::std::string())" \ - "string" \ - "String type" -constant CONST_STRING \ - ::std::string \ - ::CVC4::StringHashFunction \ - "util/hash.h" \ - "a string of characters" -typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule - typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index a04f9f88a..c7143bdeb 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -146,14 +146,6 @@ public: } };/* class AbstractValueTypeRule */ -class StringConstantTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::CONST_STRING); - return nodeManager->stringType(); - } -};/* class StringConstantTypeRule */ - class LambdaTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 008618342..d74f36069 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic + ** Minor contributors (to current version): Dejan Jovanovic, Tianyi Liang ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -105,6 +105,10 @@ std::string LogicInfo::getLogicString() const { ss << "DT"; ++seen; } + if(d_theories[THEORY_STRINGS]) { + ss << "S"; + ++seen; + } if(d_theories[THEORY_ARITH]) { if(isDifferenceLogic()) { ss << (areIntegersUsed() ? "I" : ""); @@ -177,6 +181,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableTheory(THEORY_ARRAY); ++p; } + if(*p == 'S') { + // Strings requires arith for length constraints, + // and UF for equality (?) + enableTheory(THEORY_STRINGS); + enableTheory(THEORY_UF); + enableTheory(THEORY_ARITH); + enableIntegers(); + arithOnlyLinear(); + ++p; + } if(!strncmp(p, "UF", 2)) { enableTheory(THEORY_UF); p += 2; diff --git a/src/theory/strings/Makefile b/src/theory/strings/Makefile new file mode 100644 index 000000000..e92c24ab7 --- /dev/null +++ b/src/theory/strings/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/strings + +include $(topdir)/Makefile.subdir diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am new file mode 100644 index 000000000..15bd04b88 --- /dev/null +++ b/src/theory/strings/Makefile.am @@ -0,0 +1,17 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libstrings.la + +libstrings_la_SOURCES = \ + theory_strings.h \ + theory_strings.cpp \ + theory_strings_rewriter.h \ + theory_strings_rewriter.cpp \ + theory_strings_type_rules.h \ + type_enumerator.h + +EXTRA_DIST = \ + kinds diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds new file mode 100644 index 000000000..814276a7c --- /dev/null +++ b/src/theory/strings/kinds @@ -0,0 +1,105 @@ +# kinds [for strings theory] +# + +theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" + +properties check parametric propagate + +rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h" + +typechecker "theory/strings/theory_strings_type_rules.h" + + +operator STRING_CONCAT 2: "string concat" + +operator STRING_IN_REGEXP 2 "membership" + +operator STRING_LENGTH 1 "string length" + +#sort CHAR_TYPE \ +# Cardinality::INTEGERS \ +# well-founded \ +# "NodeManager::currentNM()->mkConst(::CVC4::String())" \ +# "util/regexp.h" \ +# "String type" + +sort STRING_TYPE \ + Cardinality::INTEGERS \ + well-founded \ + "NodeManager::currentNM()->mkConst(::CVC4::String())" \ + "util/regexp.h" \ + "String type" + +sort REGEXP_TYPE \ + Cardinality::INTEGERS \ + well-founded \ + "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \ + "util/regexp.h" \ + "RegExp type" + +enumerator STRING_TYPE \ + "::CVC4::theory::strings::StringEnumerator" \ + "theory/strings/type_enumerator.h" + +#enumerator REGEXP_TYPE \ +# "::CVC4::theory::strings::RegExpEnumerator" \ +# "theory/strings/type_enumerator.h" + +constant CONST_STRING \ + ::CVC4::String \ + ::CVC4::strings::StringHashFunction \ + "util/regexp.h" \ + "a string of characters" + +constant CONST_REGEXP \ + ::CVC4::RegExp \ + ::CVC4::RegExpHashFunction \ + "util/regexp.h" \ + "a regular expression" + +typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule +typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule + +# equal equal / less than / output +operator STRING_TO_REGEXP 1 "convert string to regexp" +operator REGEXP_CONCAT 2: "regexp concat" +operator REGEXP_OR 2: "regexp or" +operator REGEXP_INTER 2: "regexp intersection" +operator REGEXP_STAR 1 "regexp *" +operator REGEXP_PLUS 1 "regexp +" +operator REGEXP_OPT 1 "regexp ?" + +#constant REGEXP_EMPTY \ +# ::CVC4::RegExp \ +# ::CVC4::RegExpHashFunction \ +# "util/string.h" \ +# "a regexp contains nothing" + +#constant REGEXP_ALL \ +# ::CVC4::RegExp \ +# ::CVC4::RegExpHashFunction \ +# "util/string.h" \ +# "a regexp contains all strings" + +#constant REGEXP_SIGMA \ +# ::CVC4::RegExp \ +# ::CVC4::RegExpHashFunction \ +# "util/string.h" \ +# "a regexp contains an arbitrary charactor" + +typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule +typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule +typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule +typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule +typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule +typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule + +typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule + + +typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule +typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule + +typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule + +endtheory diff --git a/src/theory/strings/options b/src/theory/strings/options new file mode 100644 index 000000000..c90d654b1 --- /dev/null +++ b/src/theory/strings/options @@ -0,0 +1,11 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module STRINGS "theory/strings/options.h" Strings theory + +option stringCharCardinality str-cardinality --str-cardinality=N int16_t :default 256 :read-write + the cardinality of the characters used by the theory of string, default 256 + +endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp new file mode 100644 index 000000000..33bee4135 --- /dev/null +++ b/src/theory/strings/theory_strings.cpp @@ -0,0 +1,1285 @@ +/********************* */ +/*! \file theory_strings.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: Tianyi Liang, Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the theory of strings. + ** + ** Implementation of the theory of strings. + **/ + + +#include "theory/strings/theory_strings.h" +#include "theory/valuation.h" +#include "expr/kind.h" +#include "theory/rewriter.h" +#include "expr/command.h" +#include "theory/model.h" +#include "smt/logic_exception.h" +#include "theory/strings/options.h" +#include <cmath> + +using namespace std; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace strings { + +TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, qe), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"), + d_conflict( c, false ), + d_infer(c), + d_infer_exp(c), + d_nf_pairs(c), + d_ind_map1(c), + d_ind_map2(c), + d_ind_map_exp(c), + d_ind_map_lemma(c) +{ + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); + d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); + d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); + + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + d_true = NodeManager::currentNM()->mkConst( true ); + d_false = NodeManager::currentNM()->mkConst( false ); +} + +TheoryStrings::~TheoryStrings() { + +} + +void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + +void TheoryStrings::addSharedTerm(TNode t) { + Debug("strings") << "TheoryStrings::addSharedTerm(): " + << t << " " << t.getType().isBoolean() << endl; + d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS); + Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl; +} + +void TheoryStrings::propagate(Effort e) +{ + // direct propagation now +} + +bool TheoryStrings::propagate(TNode literal) { + Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl; + // If already in conflict, no more propagation + if (d_conflict) { + Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl; + return false; + } + Trace("strings-prop") << "strPropagate " << literal << std::endl; + // Propagate out + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; + } + return ok; +} + +/** explain */ +void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){ + Debug("strings-explain") << "Explain " << literal << std::endl; + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); + } +} + +Node TheoryStrings::explain( TNode literal ){ + std::vector< TNode > assumptions; + explain( literal, assumptions ); + if( assumptions.empty() ){ + return NodeManager::currentNM()->mkConst( true ); + }else if( assumptions.size()==1 ){ + return assumptions[0]; + }else{ + return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); + } +} + +///////////////////////////////////////////////////////////////////////////// +// MODEL GENERATION +///////////////////////////////////////////////////////////////////////////// + + +void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { + /* + // Generate model + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ) { + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + Node cst = ei ? ei->d_const_term : Node::null(); + if( !cst.isNull() ){ + //print out + Trace("strings-model-debug") << cst << std::endl; + }else{ + //is there a length term? + // is there a value for it? if so, assign a constant via enumerator + // otherwise: error + //otherwise: assign a new unique length, then assign a constant via enumerator + } + }else{ + //should be length eqc + //if no constant, error + } + + ++eqcs_i; + } +*/ + //TODO: not done +} + +///////////////////////////////////////////////////////////////////////////// +// MAIN SOLVER +///////////////////////////////////////////////////////////////////////////// + +void TheoryStrings::preRegisterTerm(TNode n) { + Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl; + //collectTerms( n ); + switch (n.getKind()) { + case kind::EQUAL: + d_equalityEngine.addTriggerEquality(n); + break; + case kind::STRING_IN_REGEXP: + d_equalityEngine.addTriggerPredicate(n); + break; + default: + if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) { + Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); + Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, zero); + Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl; + d_out->lemma(n_len_geq_zero); + } + if (n.getType().isBoolean()) { + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerPredicate(n); + } else { + // Function applications/predicates + d_equalityEngine.addTerm(n); + } + break; + } +} + +void TheoryStrings::dealPositiveWordEquation(TNode n) { + Trace("strings-pwe") << "Deal Positive Word Equation: " << n << endl; + Node node = n; + + // length left = length right + //Node n_left = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]); + //Node n_right = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[1]); + if(node[0].getKind() == kind::CONST_STRING) { + } else if(node[0].getKind() == kind::STRING_CONCAT) { + } +} + +void TheoryStrings::check(Effort e) { + bool polarity; + TNode atom; + + // Trace("strings-process") << "Theory of strings, check : " << e << std::endl; + Trace("strings-check") << "Theory of strings, check : " << e << std::endl; + while ( !done() && !d_conflict) + { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Trace("strings-assertion") << "get assertion: " << fact << endl; + + polarity = fact.getKind() != kind::NOT; + atom = polarity ? fact : fact[0]; + if (atom.getKind() == kind::EQUAL) { + //head + //if(atom[0].getKind() == kind::CONST_STRING) { + //if(atom[1].getKind() == kind::STRING_CONCAT) { + //} + //} + //tail + d_equalityEngine.assertEquality(atom, polarity, fact); + } else { + d_equalityEngine.assertPredicate(atom, polarity, fact); + } + switch(atom.getKind()) { + case kind::EQUAL: + if(polarity) { + //if(atom[0].isString() && atom[1].isString()) { + //dealPositiveWordEquation(atom); + //} + } else { + // TODO: Word Equation negaitive + } + break; + case kind::STRING_IN_REGEXP: + // TODO: membership + break; + default: + //possibly error + break; + } + } + doPendingFacts(); + + + bool addedLemma = false; + if( e == EFFORT_FULL && !d_conflict ) { + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + //EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); + //get the constant for the equivalence class + //int c_len = ...; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + + //if n is concat, and + //if n has not instantiatied the concat..length axiom + //then, add lemma + if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){ + if( d_length_inst.find(n)==d_length_inst.end() ){ + d_length_inst[n] = true; + Trace("strings-debug") << "get n: " << n << endl; + Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); + eq = Rewriter::rewrite(eq); + Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl; + d_out->lemma(eq); + Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node lsum; + if( n.getKind() == kind::STRING_CONCAT ){ + //add lemma + std::vector<Node> node_vec; + for( unsigned i=0; i<n.getNumChildren(); i++ ) { + Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } + lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); + }else{ + //add lemma + lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) ); + } + Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); + ceq = Rewriter::rewrite(ceq); + Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl; + d_out->lemma(ceq); + addedLemma = true; + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + if( !addedLemma ){ + addedLemma = checkNormalForms(); + if(!d_conflict && !addedLemma) { + addedLemma = checkCardinality(); + if( !d_conflict && !addedLemma ){ + addedLemma = checkInductiveEquations(); + } + } + } + } + Trace("strings-process") << "Theory of strings, done check : " << e << std::endl; +} + +TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) { + +} + +TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) { + std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc ); + if( eqc_i==d_eqc_info.end() ){ + if( doMake ){ + EqcInfo* ei = new EqcInfo( getSatContext() ); + d_eqc_info[eqc] = ei; + return ei; + }else{ + return NULL; + } + }else{ + return (*eqc_i).second; + } +} + + +/** Conflict when merging two constants */ +void TheoryStrings::conflict(TNode a, TNode b){ + Node conflictNode; + if (a.getKind() == kind::CONST_BOOLEAN) { + conflictNode = explain( a.iffNode(b) ); + } else { + conflictNode = explain( a.eqNode(b) ); + } + Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + d_out->conflict( conflictNode ); + d_conflict = true; +} + +/** called when a new equivalance class is created */ +void TheoryStrings::eqNotifyNewClass(TNode t){ + if( t.getKind() == kind::CONST_STRING ){ + EqcInfo * ei =getOrMakeEqcInfo( t, true ); + ei->d_const_term = t; + } + if( t.getKind() == kind::STRING_LENGTH ){ + Trace("strings-debug") << "New length eqc : " << t << std::endl; + Node r = d_equalityEngine.getRepresentative(t[0]); + EqcInfo * ei = getOrMakeEqcInfo( r, true ); + ei->d_length_term = t[0]; + } +} + +/** called when two equivalance classes will merge */ +void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ + EqcInfo * e2 = getOrMakeEqcInfo(t2, false); + if( e2 ){ + EqcInfo * e1 = getOrMakeEqcInfo( t1 ); + //add information from e2 to e1 + if( !e2->d_const_term.get().isNull() ){ + e1->d_const_term.set( e2->d_const_term ); + } + if( !e2->d_length_term.get().isNull() ){ + e1->d_length_term.set( e2->d_length_term ); + } + if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { + e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); + } + } + if( hasTerm( d_zero ) ){ + Node leqc; + if( areEqual(d_zero, t1) ){ + leqc = t2; + }else if( areEqual(d_zero, t2) ){ + leqc = t1; + } + if( !leqc.isNull() ){ + //scan equivalence class to see if we apply + eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + if( n.getKind()==kind::STRING_LENGTH ){ + if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){ + Trace("strings-debug") << "Processing possible inference." << n << std::endl; + //apply the rule length(n[0])==0 => n[0] == "" + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString ); + d_pending.push_back( eq ); + Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero ); + d_pending_exp[eq] = eq_exp; + Trace("strings-infer") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + } + } + ++eqc_i; + } + } + } +} + +/** called when two equivalance classes have merged */ +void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) { + +} + +/** called when two equivalance classes are disequal */ +void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + +} + +void TheoryStrings::computeCareGraph(){ + Theory::computeCareGraph(); +} + +void TheoryStrings::doPendingFacts() { + int i=0; + while( !d_conflict && i<(int)d_pending.size() ){ + Node fact = d_pending[i]; + Node exp = d_pending_exp[ fact ]; + Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl; + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.assertEquality( atom, polarity, exp ); + }else{ + d_equalityEngine.assertPredicate( atom, polarity, exp ); + } + i++; + } + d_pending.clear(); + d_pending_exp.clear(); +} + +void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, + std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) { + // EqcItr + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + Trace("strings-process") << "Process term " << n << std::endl; + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { + std::vector<Node> nf_n; + std::vector<Node> nf_exp_n; + if( n.getKind() == kind::CONST_STRING ){ + if( n!=d_emptyString ) { + nf_n.push_back( n ); + } + } else if( n.getKind() == kind::STRING_CONCAT ) { + for( unsigned i=0; i<n.getNumChildren(); i++ ) { + Node nr = d_equalityEngine.getRepresentative( n[i] ); + std::vector< Node > nf_temp; + std::vector< Node > nf_exp_temp; + Trace("strings-process") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return; + } + if( nf.size()!=1 || nf[0]!=d_emptyString ) { + for( unsigned r=0; r<nf_temp.size(); r++ ) { + Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT ); + } + nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() ); + } + nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() ); + if( nr!=n[i] ) { + nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); + } + } + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + } + /* should we add these? + else { + //var/sk? + std::vector<Node> nf_n; + std::vector<Node> nf_exp_n; + nf_n.push_back(n); + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + }*/ + ++eqc_i; + } + + // Test the result + if( !normal_forms.empty() ) { + Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; + for( unsigned i=0; i<normal_forms.size(); i++ ) { + Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : "; + for( unsigned j=0; j<normal_forms[i].size(); j++ ) { + if(j>0) Trace("strings-solve") << ", "; + Trace("strings-solve") << normal_forms[i][j]; + } + Trace("strings-solve") << std::endl; + Trace("strings-solve") << " Explanation is : "; + if(normal_forms_exp[i].size() == 0) { + Trace("strings-solve") << "NONE"; + } else { + for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) { + if(j>0) Trace("strings-solve") << " AND "; + Trace("strings-solve") << normal_forms_exp[i][j]; + } + } + Trace("strings-solve") << std::endl; + } + } +} +//nf_exp is conjunction +void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { + Trace("strings-process") << "Process equivalence class " << eqc << std::endl; + if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){ + //nf.push_back( eqc ); + if( eqc.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; i<eqc.getNumChildren(); i++ ){ + nf.push_back( eqc[i] ); + } + }else{ + nf.push_back( eqc ); + } + Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; + } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){ + //do nothing + Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl; + } else { + visited.push_back( eqc ); + if(d_normal_forms.find(eqc)==d_normal_forms.end() ){ + //phi => t = s1 * ... * sn + // normal form for each non-variable term in this eqc (s1...sn) + std::vector< std::vector< Node > > normal_forms; + // explanation for each normal form (phi) + std::vector< std::vector< Node > > normal_forms_exp; + // record terms for each normal form (t) + std::vector< Node > normal_form_src; + //Get Normal Forms + getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return; + } + + unsigned i = 0; + //unify each normal form > 0 with normal_forms[0] + for( unsigned j=1; j<normal_forms.size(); j++ ) { + std::vector< Node > loop_eqs_x; + std::vector< Node > loop_eqs_y; + std::vector< Node > loop_eqs_z; + std::vector< Node > loop_exps; + Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl; + if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){ + Trace("strings-solve") << "Already normalized (in cache)." << std::endl; + }else{ + Trace("strings-solve") << "Not in cache." << std::endl; + //the current explanation for why the prefix is equal + std::vector< Node > curr_exp; + curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); + curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); + curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); + //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality + unsigned index_i = 0; + unsigned index_j = 0; + bool success; + do + { + success = false; + //if we are at the end + if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { + if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){ + //we're done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //add loop equations that we've accumulated + for( unsigned r=0; r<loop_eqs_x.size(); r++ ){ + addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r] ); + } + }else{ + //the remainder must be empty + unsigned k = index_i==normal_forms[i].size() ? j : i; + unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; + while(!d_conflict && index_k<normal_forms[k].size()) { + //can infer that this string must be empty + Node eq_exp; + if( curr_exp.empty() ) { + eq_exp = NodeManager::currentNM()->mkConst(true); + } else if( curr_exp.size() == 1 ) { + eq_exp = curr_exp[0]; + } else { + eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp ); + } + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); + Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + //d_equalityEngine.assertEquality( eq, true, eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + index_k++; + } + } + }else { + Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl; + if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){ + Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl; + //terms are equal, continue + if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){ + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i], + normal_forms[j][index_j]); + Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; + curr_exp.push_back(eq); + } + index_j++; + index_i++; + success = true; + }else{ + EqcInfo * ei = getOrMakeEqcInfo( normal_forms[i][index_i] ); + Node length_term_i = ei->d_length_term; + if( length_term_i.isNull()) { + //typically shouldnt be necessary + length_term_i = normal_forms[i][index_i]; + } + length_term_i = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_i ); + EqcInfo * ej = getOrMakeEqcInfo( normal_forms[j][index_j] ); + Node length_term_j = ej->d_length_term; + if( length_term_j.isNull()) { + length_term_j = normal_forms[j][index_j]; + } + length_term_j = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_j ); + //check if length(normal_forms[i][index]) == length(normal_forms[j][index]) + if( areEqual(length_term_i, length_term_j) ){ + Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl; + //length terms are equal, merge equivalence classes if not already done so + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); + std::vector< Node > temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j )); + Node eq_exp = temp_exp.empty() ? NodeManager::currentNM()->mkConst(true) : + temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); + Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + //d_equalityEngine.assertEquality( eq, true, eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + return; + }else{ + Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl; + bool sendLemma = false; + Node loop_x; + Node loop_y; + Node loop_z; + Node conc; + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + //check for loops + Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; + int has_loop[2] = { -1, -1 }; + for( unsigned r=0; r<2; r++ ){ + int index = (r==0 ? index_i : index_j); + int other_index = (r==0 ? index_j : index_i ); + int n_index = (r==0 ? i : j); + int other_n_index = (r==0 ? j : i); + if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { + for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){ + if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){ + has_loop[r] = lp; + break; + } + } + } + } + if( has_loop[0]!=-1 || has_loop[1]!=-1 ){ + int loop_n_index = has_loop[0]!=-1 ? i : j; + int other_n_index = has_loop[0]!=-1 ? j : i; + int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1]; + int index = has_loop[0]!=-1 ? index_i : index_j; + int other_index = has_loop[0]!=-1 ? index_j : index_i; + Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index]; + Trace("strings-loop") << " ... " << normal_forms[other_n_index][other_index] << std::endl; + //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp + //check if + //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] = y * z + // and + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y + // for some y,z,k + int found_size_y = -1; + for( int size_y = 0; size_y<(loop_index-index); size_y++ ){ + int size_z = (loop_index-index)-size_y; + bool success = true; + //check for z + for( int r = 0; r<size_z; r++ ){ + if( other_index+1+r >= (int)normal_forms[other_n_index].size() || + normal_forms[other_n_index][other_index+1+r]!=normal_forms[loop_n_index][index+size_y+r] ) { + success = false; + break; + } + } + //check for y + if( success ){ + for( int r=0; r<size_y; r++ ){ + if( other_index+1+r >= (int)normal_forms[other_n_index].size() || + normal_forms[other_n_index][other_index+1+size_y+r]!=normal_forms[loop_n_index][index+r] ) { + success = false; + break; + } + } + if( success ){ + found_size_y = size_y; + break; + } + } + } + if( found_size_y==-1 ){ + //need to break + Node sk_y= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + + sendLemma = true; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + //t1 * ... * tn = y * z + std::vector< Node > c1c; + //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] + for( int r=index; r<=loop_index-1; r++ ) { + c1c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc1 = c1c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c1c ) : + c1c.size()==1 ? c1c[0] : d_emptyString; + conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + std::vector< Node > c2c; + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] + for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { + c2c.push_back( normal_forms[other_n_index][r] ); + } + Node left2 = c2c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c2c ) : + c2c.size()==1 ? c2c[0] : d_emptyString; + std::vector< Node > c3c; + c3c.push_back( sk_z ); + c3c.push_back( sk_y ); + //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] + for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { + c3c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c3c ) ); + Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); + //Node sk_y_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_y_len, zero); + //Node sk_z_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_z_len, zero); + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, sk_y_len_geq_zero, sk_z_len_geq_zero ); + loop_x = normal_forms[other_n_index][other_index]; + loop_y = sk_y; + loop_z = sk_z; + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + } else { + // x = (yz)*y + Trace("strings-loop") << "We have that " << normal_forms[loop_n_index][loop_index] << " = ("; + loop_eqs_x.push_back( normal_forms[loop_n_index][loop_index] ); + for( unsigned r=0; r<2; r++ ){ + //print y + std::vector< Node > yc; + for( int rr = 0; rr<found_size_y; rr++ ){ + if( rr>0 ) Trace("strings-loop") << "."; + Trace("strings-loop") << normal_forms[loop_n_index][index+rr]; + yc.push_back( normal_forms[loop_n_index][index+rr] ); + } + if( r==0 ){ + loop_eqs_y.push_back( mkConcat( yc ) ); + Trace("strings-loop") <<".."; + //print z + int found_size_z = (loop_index-index)-found_size_y; + std::vector< Node > zc; + for( int rr = 0; rr<found_size_z; rr++ ){ + if( rr>0 ) Trace("strings-loop") << "."; + Trace("strings-loop") << normal_forms[loop_n_index][index+found_size_y+rr]; + zc.push_back( normal_forms[loop_n_index][index+found_size_y+rr] ); + } + Trace("strings-loop") << ")*"; + loop_eqs_z.push_back( mkConcat( zc ) ); + } + } + Trace("strings-loop") << std::endl; + if( loop_n_index==(int)i ){ + index_j += (loop_index+1)-index_i; + index_i = loop_index+1; + }else{ + index_i += (loop_index+1)-index_j; + index_j = loop_index+1; + } + success = true; + std::vector< Node > empty_vec; + loop_exps.push_back( mkExplain( antec, empty_vec ) ); + } + }else{ + Trace("strings-loop") << "No loops detected." << std::endl; + if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || + normal_forms[j][index_j].getKind() == kind::CONST_STRING) { + Node const_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[i][index_i] : normal_forms[j][index_j]; + Node other_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[j][index_j] : normal_forms[i][index_i]; + if( other_str.getKind() == kind::CONST_STRING ) { + unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size(); + if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) { + //same prefix + //k is the index of the string that is shorter + int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j; + int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j; + int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i; + int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i; + Node remainderStr = NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(len_short) ); + Trace("strings-solve-debug") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; + normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); + normal_forms[l][index_l] = normal_forms[k][index_k]; + success = true; + } else { + //curr_exp is conflict + sendLemma = true; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + } + } else { + Assert( other_str.getKind()!=kind::STRING_CONCAT ); + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); + //split the string + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); + // |sk| >= 0 + Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); + //Node sk_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_len, zero); + + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); + Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + sendLemma = true; + } + }else{ + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + antec.push_back( ldeq ); + }else{ + antec_new_lits.push_back(ldeq); + } + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); + Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + sendLemma = true; + // |sk| > 0 + Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); + Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, zero); + Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + //d_out->lemma(sk_gt_zero); + d_lemma_cache.push_back( sk_gt_zero ); + } + } + Trace("strings-solve-debug2") << "sendLemma/success : " << sendLemma << " " << success << std::endl; + if( sendLemma ){ + Node ant = mkExplain( antec, antec_new_lits ); + if( conc.isNull() ){ + d_out->conflict(ant); + Trace("strings-conflict") << "Strings conflict : " << ant << std::endl; + d_conflict = true; + }else{ + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); + Trace("strings-lemma") << "Strings compare lemma : " << lem << std::endl; + //d_out->lemma(lem); + d_lemma_cache.push_back( lem ); + } + if( !loop_y.isNull() ){ + addInductiveEquation( loop_x, loop_y, loop_z, ant ); + } + return; + } + } + } + } + }while(success); + } + } + + //construct the normal form + if( normal_forms.empty() ){ + Trace("strings-solve-debug2") << "construct the normal form" << std::endl; + nf.push_back( eqc ); + } else { + Trace("strings-solve-debug2") << "just take the first normal form" << std::endl; + //just take the first normal form + nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() ); + nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() ); + if( eqc!=normal_form_src[0] ){ + nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) ); + } + Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl; + } + //if( visited.empty() ){ + //TODO : cache? + //} + d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() ); + d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() ); + Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl; + }else{ + Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl; + nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() ); + nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() ); + } + visited.pop_back(); + } +} +bool TheoryStrings::hasTerm( Node a ){ + return d_equalityEngine.hasTerm( a ); +} + +bool TheoryStrings::areEqual( Node a, Node b ){ + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areEqual( a, b ); + }else{ + return false; + } +} + +void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { + //Trace("strings-debug") << "add normal form pair. " << n1 << " " << n2 << std::endl; + if( !isNormalFormPair( n1, n2 ) ){ + NodeList* lst; + NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); + if( nf_i == d_nf_pairs.end() ){ + if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){ + addNormalFormPair( n2, n1 ); + return; + } + lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_nf_pairs.insertDataFromContextMemory( n1, lst ); + }else{ + lst = (*nf_i).second; + } + lst->push_back( n2 ); + } +} +bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) { + //TODO: modulo equality? + return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 ); +} +bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { + //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; + NodeList* lst; + NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); + if( nf_i != d_nf_pairs.end() ){ + lst = (*nf_i).second; + for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) { + Node n = *i; + if( n==n2 ){ + return true; + } + } + } + return false; +} + +void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) { + Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl; + + NodeListMap::iterator itr_x_y = d_ind_map1.find(x); + NodeList* lst1; + NodeList* lst2; + NodeList* lste; + NodeList* lstl; + if( itr_x_y == d_ind_map1.end() ) { + // add x->y + lst1 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map1.insertDataFromContextMemory( x, lst1 ); + // add x->z + lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map2.insertDataFromContextMemory( x, lst2 ); + // add x->exp + lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map_exp.insertDataFromContextMemory( x, lste ); + // add x->hasLemma false + lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map_lemma.insertDataFromContextMemory( x, lstl ); + } else { + //TODO: x in (yz)*y (exp) vs x in (y1 z1)*y1 (exp1) + lst1 = (*itr_x_y).second; + lst2 = (*d_ind_map2.find(x)).second; + lste = (*d_ind_map_exp.find(x)).second; + lstl = (*d_ind_map_lemma.find(x)).second; + Trace("strings-solve-debug") << "Already in maps " << x << " = (" << lst1 << " " << lst2 << ")* " << lst1 << std::endl; + Trace("strings-solve-debug") << "... with exp = " << lste << std::endl; + } + lst1->push_back( y ); + lst2->push_back( z ); + lste->push_back( exp ); +} + +Node TheoryStrings::mkConcat( std::vector< Node >& c ) { + return c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); +} + +Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { + std::vector< TNode > antec_exp; + for( unsigned i=0; i<a.size(); i++ ){ + Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl; + //assert + if(a[i].getKind() == kind::EQUAL) { + //assert( hasTerm(a[i][0]) ); + //assert( hasTerm(a[i][1]) ); + Assert( areEqual(a[i][0], a[i][1]) ); + } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){ + Assert( hasTerm(a[i][0][0]) ); + Assert( hasTerm(a[i][0][1]) ); + Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) ); + } + explain(a[i], antec_exp); + Trace("strings-solve-debug") << "Done." << std::endl; + } + for( unsigned i=0; i<an.size(); i++ ){ + antec_exp.push_back(an[i]); + } + Node ant; + if( antec_exp.empty() ) { + ant = NodeManager::currentNM()->mkConst(true); + } else if( antec_exp.size()==1 ) { + ant = antec_exp[0]; + } else { + ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp ); + } + return ant; +} + +bool TheoryStrings::checkNormalForms() { + Trace("strings-process") << "Normalize equivalence classes...." << std::endl; + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs2_i.isFinished() ){ + Node eqc = (*eqcs2_i); + //if (eqc.getType().isString()) { + eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + Trace("strings-eqc") << "Eqc( " << eqc << " ) : "; + while( !eqc2_i.isFinished() ) { + Trace("strings-eqc") << (*eqc2_i) << " "; + ++eqc2_i; + } + Trace("strings-eqc") << std::endl; + //} + ++eqcs2_i; + } + + bool addedFact = false; + do { + //calculate normal forms for each equivalence class, possibly adding splitting lemmas + d_normal_forms.clear(); + d_normal_forms_exp.clear(); + std::map< Node, Node > nf_to_eqc; + std::map< Node, Node > eqc_to_exp; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + d_lemma_cache.clear(); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + Trace("strings-process") << "Verify normal forms are the same for " << eqc << std::endl; + std::vector< Node > visited; + std::vector< Node > nf; + std::vector< Node > nf_exp; + normalizeEquivalenceClass(eqc, visited, nf, nf_exp); + if( d_conflict ){ + return true; + }else if ( d_pending.empty() && d_lemma_cache.empty() ){ + Node nf_term; + if( nf.size()==0 ){ + nf_term = d_emptyString; + }else if( nf.size()==1 ) { + nf_term = nf[0]; + } else { + nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf ); + } + nf_term = Rewriter::rewrite( nf_term ); + Trace("strings-debug") << "Make nf_term_exp..." << std::endl; + Node nf_term_exp = nf_exp.empty() ? NodeManager::currentNM()->mkConst(true) : + nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp ); + if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){ + //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; + //two equivalence classes have same normal form, merge + Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] ); + Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl; + //d_equalityEngine.assertEquality( eq, true, eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + }else{ + nf_to_eqc[nf_term] = eqc; + eqc_to_exp[eqc] = nf_term_exp; + } + } + Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl; + } + ++eqcs_i; + } + addedFact = !d_pending.empty(); + doPendingFacts(); + if( !d_conflict ){ + for( unsigned i=0; i<d_lemma_cache.size(); i++ ){ + Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl; + d_out->lemma( d_lemma_cache[i] ); + } + if( !d_lemma_cache.empty() ){ + d_lemma_cache.clear(); + return true; + } + } + } while (!d_conflict && addedFact); + return false; +} + +bool TheoryStrings::checkCardinality() { + int cardinality = options::stringCharCardinality(); + Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl; + + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + unsigned leqc_counter = 0; + std::map< Node, unsigned > eqc_to_leqc; + std::map< unsigned, Node > leqc_to_eqc; + std::map< unsigned, std::vector< Node > > eqc_to_strings; + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); + Node lt = ei->d_length_term; + if( !lt.isNull() ){ + lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + Node r = d_equalityEngine.getRepresentative( lt ); + if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ + eqc_to_leqc[r] = leqc_counter; + leqc_to_eqc[leqc_counter] = r; + leqc_counter++; + } + eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc ); + }else{ + eqc_to_strings[leqc_counter].push_back( eqc ); + leqc_counter++; + } + } + ++eqcs_i; + } + for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){ + Node lr = leqc_to_eqc[it->first]; + Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << it->second.size() << std::endl; + // size > c^k + double k = std::log( it->second.size() ) / log((double) cardinality); + unsigned int int_k = (unsigned int)k; + Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + //double c_k = pow ( (double)cardinality, (double)lr ); + if( it->second.size() > 1 ) { + bool allDisequal = true; + for( std::vector< Node >::iterator itr1 = it->second.begin(); + itr1 != it->second.end(); ++itr1) { + for( std::vector< Node >::iterator itr2 = itr1 + 1; + itr2 != it->second.end(); ++itr2) { + if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) { + allDisequal = false; + // add split lemma + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, *itr1, *itr2 ); + Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq ); + Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq ); + Trace("strings-lemma") << "Strings split lemma : " << lemma_or << std::endl; + d_out->lemma(lemma_or); + return true; + } + } + } + if(allDisequal) { + EqcInfo* ei = getOrMakeEqcInfo( lr, true ); + Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ei->d_cardinality_lem_k << std::endl; + if( int_k > ei->d_cardinality_lem_k.get() ){ + //add cardinality lemma + Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, it->second ); + std::vector< Node > vec_node; + vec_node.push_back( dist ); + for( std::vector< Node >::iterator itr1 = it->second.begin(); + itr1 != it->second.end(); ++itr1) { + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); + if( len!=lr ){ + Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len ); + vec_node.push_back( len_eq_lr ); + } + } + Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node ); + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, it->second[0] ); + Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node ); + Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons ); + Trace("strings-lemma") << "Strings cardinaliry lemma : " << lemma << std::endl; + d_out->lemma(lemma); + ei->d_cardinality_lem_k.set( k ); + return true; + } + } + } + } + return false; +} + +bool TheoryStrings::checkInductiveEquations() { + bool hasEq = false; + Trace("strings-ind") << "We are sat, with these inductive equations : " << std::endl; + for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ + Node x = (*it).first; + NodeList* lst1 = (*it).second; + NodeList* lst2 = (*d_ind_map2.find(x)).second; + NodeList* lste = (*d_ind_map_exp.find(x)).second; + NodeList* lstl = (*d_ind_map_lemma.find(x)).second; + NodeList::const_iterator i1 = lst1->begin(); + NodeList::const_iterator i2 = lst2->begin(); + NodeList::const_iterator ie = lste->begin(); + NodeList::const_iterator il = lstl->begin(); + while( i1!=lst1->end() ){ + Node y = *i1; + Node z = *i2; + Node exp = *ie; + Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << "..." << z << " )* " << y << std::endl; + if( il==lstl->end() ) { + Trace("strings-ind") << "Add length lemma..." << std::endl; + Node lemma_len; + if( y.getKind()!=kind::STRING_CONCAT || z.getKind()!=kind::STRING_CONCAT ) { + Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); + Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); + lemma_len = NodeManager::currentNM()->mkNode( kind::GEQ, len_x, len_y ); + } else { + // both constants + Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); + Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" ); + Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); + Node len_z = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, z ); + Node len_y_plus_len_z = NodeManager::currentNM()->mkNode( kind::PLUS, len_y, len_z ); + Node y_p_z_t_a = NodeManager::currentNM()->mkNode( kind::MULT, len_y_plus_len_z, sk ); + Node y_p_z_t_a_p_y = NodeManager::currentNM()->mkNode( kind::PLUS, y_p_z_t_a, len_y ); + lemma_len = NodeManager::currentNM()->mkNode( kind::EQUAL, y_p_z_t_a_p_y, len_x ); + Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero ); + lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero ); + } + lemma_len = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len ); + Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl; + d_out->lemma(lemma_len); + lstl->push_back( d_true ); + return true; + } + + ++i1; + ++i2; + ++ie; + ++il; + hasEq = true; + } + } + if( hasEq ){ + d_out->setIncomplete(); + } + return false; +} + + + + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h new file mode 100644 index 000000000..a6644b8bb --- /dev/null +++ b/src/theory/strings/theory_strings.h @@ -0,0 +1,222 @@ +/********************* */ +/*! \file theory_strings.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory of strings + ** + ** Theory of strings. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H +#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** + * Decision procedure for strings. + * + */ + +class TheoryStrings : public Theory { + typedef context::CDChunkList<Node> NodeList; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; + public: + + TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + ~TheoryStrings(); + + void setMasterEqualityEngine(eq::EqualityEngine* eq); + + std::string identify() const { return std::string("TheoryStrings"); } + + + public: + + void propagate(Effort e); + bool propagate(TNode literal); + void explain( TNode literal, std::vector<TNode>& assumptions ); + Node explain( TNode literal ); + + + // NotifyClass for equality engine + class NotifyClass : public eq::EqualityEngineNotify { + TheoryStrings& d_str; + public: + NotifyClass(TheoryStrings& t_str): d_str(t_str) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_str.propagate(equality); + } else { + // We use only literal triggers so taking not is safe + return d_str.propagate(equality.notNode()); + } + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + return d_str.propagate(predicate); + } else { + return d_str.propagate(predicate.notNode()); + } + } + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; + if (value) { + return d_str.propagate(t1.eqNode(t2)); + } else { + return d_str.propagate(t1.eqNode(t2).notNode()); + } + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_str.conflict(t1, t2); + } + void eqNotifyNewClass(TNode t) { + Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + d_str.eqNotifyNewClass(t); + } + void eqNotifyPreMerge(TNode t1, TNode t2) { + Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + d_str.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) { + Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + d_str.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + d_str.eqNotifyDisequal(t1, t2, reason); + } + };/* class TheoryStrings::NotifyClass */ + + private: + /** The notify class */ + NotifyClass d_notify; + /** Equaltity engine */ + eq::EqualityEngine d_equalityEngine; + /** Are we in conflict */ + context::CDO<bool> d_conflict; + + Node d_emptyString; + Node d_true; + Node d_false; + Node d_zero; + //list of pairs of nodes to merge + std::map< Node, Node > d_pending_exp; + std::vector< Node > d_pending; + std::vector< Node > d_lemma_cache; + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + /** inferences */ + NodeList d_infer; + NodeList d_infer_exp; + //map of pairs of terms that have the same normal form + NodeListMap d_nf_pairs; + void addNormalFormPair( Node n1, Node n2 ); + bool isNormalFormPair( Node n1, Node n2 ); + bool isNormalFormPair2( Node n1, Node n2 ); + + NodeListMap d_ind_map1; + NodeListMap d_ind_map2; + NodeListMap d_ind_map_exp; + NodeListMap d_ind_map_lemma; + void addInductiveEquation( Node x, Node y, Node z, Node exp ); + + ///////////////////////////////////////////////////////////////////////////// + // MODEL GENERATION + ///////////////////////////////////////////////////////////////////////////// + public: + + void collectModelInfo(TheoryModel* m, bool fullModel); + + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// + + public: + + void shutdown() { } + + ///////////////////////////////////////////////////////////////////////////// + // MAIN SOLVER + ///////////////////////////////////////////////////////////////////////////// + private: + void dealPositiveWordEquation(TNode n); + void addSharedTerm(TNode n); + + private: + class EqcInfo + { + public: + EqcInfo( context::Context* c ); + ~EqcInfo(){} + //constant in this eqc + context::CDO< Node > d_const_term; + context::CDO< Node > d_length_term; + context::CDO< unsigned > d_cardinality_lem_k; + }; + /** map from representatives to information necessary for equivalence classes */ + std::map< Node, EqcInfo* > d_eqc_info; + EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); + //maintain which concat terms have the length lemma instantiatied + std::map< Node, bool > d_length_inst; + private: + std::map< Node, std::vector< Node > > d_normal_forms; + std::map< Node, std::vector< Node > > d_normal_forms_exp; + void getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, + std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); + void normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); + bool areLengthsEqual( Node n1, Node n2 ); //TODO + + bool checkNormalForms(); + bool checkCardinality(); + bool checkInductiveEquations(); + public: + void preRegisterTerm(TNode n); + void check(Effort e); + + /** Conflict when merging two constants */ + void conflict(TNode a, TNode b); + /** called when a new equivalance class is created */ + void eqNotifyNewClass(TNode t); + /** called when two equivalance classes will merge */ + void eqNotifyPreMerge(TNode t1, TNode t2); + /** called when two equivalance classes have merged */ + void eqNotifyPostMerge(TNode t1, TNode t2); + /** called when two equivalence classes are made disequal */ + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); +protected: + /** compute care graph */ + void computeCareGraph(); + + //do pending merges + void doPendingFacts(); + + /** mkConcat **/ + Node mkConcat( std::vector< Node >& c ); + /** mkExplain **/ + Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); +};/* class TheoryStrings */ + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp new file mode 100644 index 000000000..412135675 --- /dev/null +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -0,0 +1,156 @@ +/********************* */ +/*! \file theory_strings_rewriter.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the theory of strings. + ** + ** Implementation of the theory of strings. + **/ +#include "theory/strings/theory_strings_rewriter.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +Node TheoryStringsRewriter::rewriteConcatString(TNode node) { + Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl; + Node retNode = node; + std::vector<Node> node_vec; + Node preNode = Node::null(); + for(unsigned int i=0; i<node.getNumChildren(); ++i) { + Node tmpNode = node[i]; + if(node[i].getKind() == kind::STRING_CONCAT) { + tmpNode = rewriteConcatString(node[i]); + if(tmpNode.getKind() == kind::STRING_CONCAT) { + unsigned int j=0; + if(!preNode.isNull()) { + if(tmpNode[0].isConst()) { + preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode[0].getConst<String>() ) ); + node_vec.push_back( preNode ); + preNode = Node::null(); + ++j; + } else { + node_vec.push_back( preNode ); + preNode = Node::null(); + node_vec.push_back( tmpNode[0] ); + ++j; + } + } + for(; j<tmpNode.getNumChildren() - 1; ++j) { + node_vec.push_back( tmpNode[j] ); + } + tmpNode = tmpNode[j]; + } + } + if(!tmpNode.isConst()) { + if(preNode != Node::null()) { + if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().toString()=="" ) { + preNode = Node::null(); + } else { + node_vec.push_back( preNode ); + preNode = Node::null(); + } + } + node_vec.push_back( tmpNode ); + } else { + if(preNode.isNull()) { + preNode = tmpNode; + } else { + preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode.getConst<String>() ) ); + } + } + } + if(preNode != Node::null()) { + node_vec.push_back( preNode ); + } + if(node_vec.size() > 1) { + retNode = NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, node_vec); + } else { + retNode = node_vec[0]; + } + Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl; + return retNode; +} + +RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { + Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; + Node retNode = node; + + if(node.getKind() == kind::STRING_CONCAT) { + retNode = rewriteConcatString(node); + } else if(node.getKind() == kind::EQUAL) { + Node leftNode = node[0]; + if(node[0].getKind() == kind::STRING_CONCAT) { + leftNode = rewriteConcatString(node[0]); + } + Node rightNode = node[1]; + if(node[1].getKind() == kind::STRING_CONCAT) { + rightNode = rewriteConcatString(node[1]); + } + + if(leftNode == rightNode) { + retNode = NodeManager::currentNM()->mkConst(true); + } else if(leftNode.isConst() && rightNode.isConst()) { + retNode = NodeManager::currentNM()->mkConst(false); + } else if(leftNode > rightNode) { + retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, rightNode, leftNode); + } else if( leftNode != node[0] || rightNode != node[1]) { + retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode); + } + } else if(node.getKind() == kind::STRING_IN_REGEXP) { + Node leftNode = node[0]; + if(node[0].getKind() == kind::STRING_CONCAT) { + leftNode = rewriteConcatString(node[0]); + } + // TODO: right part + Node rightNode = node[1]; + // merge + if( leftNode != node[0] || rightNode != node[1]) { + retNode = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, leftNode, rightNode); + } + } else if(node.getKind() == kind::STRING_LENGTH) { + if(node[0].isConst()) { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) ); + } else if(node[0].getKind() == kind::STRING_CONCAT) { + Node tmpNode = rewriteConcatString(node[0]); + if(tmpNode.isConst()) { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) ); + } else { + // it has to be string concat + std::vector<Node> node_vec; + for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) { + if(tmpNode[i].isConst()) { + node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) ); + } else { + node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) ); + } + } + retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); + } + } + } + + Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, retNode); +} + +RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { + Node retNode = node; + Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl; + + if(node.getKind() == kind::STRING_CONCAT) { + retNode = rewriteConcatString(node); + } + + Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; + return RewriteResponse(REWRITE_DONE, retNode); +} diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h new file mode 100644 index 000000000..3bccd91de --- /dev/null +++ b/src/theory/strings/theory_strings_rewriter.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file theory_strings_rewriter.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H +#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H + +#include "theory/rewriter.h" +#include "theory/type_enumerator.h" +#include "expr/attribute.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +class TheoryStringsRewriter { + +public: + static Node rewriteConcatString(TNode node); + + static RewriteResponse postRewrite(TNode node); + + static RewriteResponse preRewrite(TNode node); + + static inline void init() {} + static inline void shutdown() {} + +};/* class TheoryStringsRewriter */ + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H */ diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h new file mode 100644 index 000000000..bf284ea7b --- /dev/null +++ b/src/theory/strings/theory_strings_type_rules.h @@ -0,0 +1,220 @@ +/********************* */ +/*! \file theory_strings_type_rules.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Typing and cardinality rules for the theory of arrays + ** + ** Typing and cardinality rules for the theory of arrays. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H +#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H + +namespace CVC4 { +namespace theory { +namespace strings { + +class StringConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return nodeManager->stringType(); + } +}; + +class StringConcatTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat"); + } + } + return nodeManager->stringType(); + } +}; + +class StringLengthTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ){ + TypeNode t = n[0].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length"); + } + } + return nodeManager->integerType(); + } +}; + +class RegExpConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return nodeManager->regexpType(); + } +}; + +class RegExpConcatTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + } + return nodeManager->regexpType(); + } +}; + +class RegExpOrTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + } + return nodeManager->regexpType(); + } +}; + +class RegExpInterTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + } + return nodeManager->regexpType(); + } +}; + +class RegExpStarTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many regexp"); + } + + return nodeManager->regexpType(); + } +}; + +class RegExpPlusTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many regexp"); + } + + return nodeManager->regexpType(); + } +}; + +class RegExpOptTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many regexp"); + } + + return nodeManager->regexpType(); + } +}; + +class StringToRegExpTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many terms"); + } + + return nodeManager->regexpType(); + } +}; + +class StringInRegExpTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms"); + } + ++it; + t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many terms"); + } + + return nodeManager->booleanType(); + } +}; + + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */ diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h new file mode 100644 index 000000000..3ab9df0cd --- /dev/null +++ b/src/theory/strings/type_enumerator.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \file type_enumerator.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Enumerators for strings + ** + ** Enumerators for strings. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H +#define __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H + +#include <sstream> + +#include "util/regexp.h" +#include "theory/type_enumerator.h" +#include "expr/type_node.h" +#include "expr/kind.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> { + unsigned d_int; + +public: + + StringEnumerator(TypeNode type) throw(AssertionException) : + TypeEnumeratorBase<StringEnumerator>(type), + d_int(0) { + Assert(type.getKind() == kind::TYPE_CONSTANT && + type.getConst<TypeConstant>() == STRING_TYPE); + } + + Node operator*() throw() { + std::stringstream ss; + ss << d_int; + return NodeManager::currentNM()->mkConst( ::CVC4::String( ss.str() ) ); + } + + StringEnumerator& operator++() throw() { + d_int++; + return *this; + } + + bool isFinished() throw() { + return false; + } + +};/* class StringEnumerator */ + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 59c69889b..156288600 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -88,7 +88,8 @@ libutil_la_SOURCES = \ util_model.h \ util_model.cpp \ sort_inference.h \ - sort_inference.cpp + sort_inference.cpp \ + regexp.h libstatistics_la_SOURCES = \ statistics_registry.h \ diff --git a/src/util/regexp.h b/src/util/regexp.h new file mode 100644 index 000000000..debb57e4c --- /dev/null +++ b/src/util/regexp.h @@ -0,0 +1,336 @@ +/********************* */ +/*! \file regexp.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__REGEXP_H +#define __CVC4__REGEXP_H + +#include <iostream> +#include <string> +//#include "util/exception.h" +//#include "util/integer.h" +#include "util/hash.h" + +namespace CVC4 { + +class CVC4_PUBLIC Char { + +private: + unsigned int d_char; + +public: + Char() {} + + Char(const unsigned int c) + : d_char(c) {} + + ~Char() {} + + Char& operator =(const Char& y) { + if(this != &y) d_char = y.d_char; + return *this; + } + + bool operator ==(const Char& y) const { + return d_char == y.d_char ; + } + + bool operator !=(const Char& y) const { + return d_char != y.d_char ; + } + + bool operator <(const Char& y) const { + return d_char < y.d_char; + } + + bool operator >(const Char& y) const { + return d_char > y.d_char ; + } + + bool operator <=(const Char& y) const { + return d_char <= y.d_char; + } + + bool operator >=(const Char& y) const { + return d_char >= y.d_char ; + } + + /* + * Convenience functions + */ + std::string toString() const { + std::string str = "1"; + str[0] = (char) d_char; + return str; + } + + unsigned size() const { + return 1; + } + + const char* c_str() const { + return toString().c_str(); + } +};/* class Char */ + +namespace strings { + +struct CharHashFunction { + size_t operator()(const ::CVC4::Char& c) const { + return __gnu_cxx::hash<const char*>()(c.toString().c_str()); + } +};/* struct CharHashFunction */ + +} + +inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const Char& c) { + return os << "\"" << c.toString() << "\""; +} + +class CVC4_PUBLIC String { + +private: + std::vector<unsigned int> d_str; + + bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const { + if(a.size() != b.size()) return false; + else { + for(unsigned int i=0; i<a.size(); ++i) + if(a[i] != b[i]) return false; + return true; + } + } + +public: + String() {} + + String(const std::string &s) { + for(unsigned int i=0; i<s.size(); ++i) { + d_str.push_back( (unsigned int)s[i] ); + } + } + + String(const char* s) { + for(unsigned int i=0,len=strlen(s); i<len; ++i) { + d_str.push_back( (unsigned int)s[i] ); + } + } + + String(const std::vector<unsigned int> &s) : d_str(s) { } + + ~String() {} + + String& operator =(const String& y) { + if(this != &y) d_str = y.d_str; + return *this; + } + + bool operator ==(const String& y) const { + return isVecSame(d_str, y.d_str); + } + + bool operator !=(const String& y) const { + return ! ( isVecSame(d_str, y.d_str) ); + } + + String concat (const String& other) const { + std::vector<unsigned int> ret_vec(d_str); + ret_vec.insert( ret_vec.end(), other.d_str.begin(), other.d_str.end() ); + return String(ret_vec); + } + + bool operator <(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size(); + else { + for(unsigned int i=0; i<d_str.size(); ++i) + if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i]; + + return false; + } + } + + bool operator >(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size(); + else { + for(unsigned int i=0; i<d_str.size(); ++i) + if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i]; + + return false; + } + } + + bool operator <=(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size(); + else { + for(unsigned int i=0; i<d_str.size(); ++i) + if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i]; + + return true; + } + } + + bool operator >=(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size(); + else { + for(unsigned int i=0; i<d_str.size(); ++i) + if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i]; + + return true; + } + } + + bool strncmp(const String &y, unsigned int n) const { + for(unsigned int i=0; i<n; ++i) + if(d_str[i] != y.d_str[i]) return false; + return true; + } + + /* + * Convenience functions + */ + std::string toString() const { + std::string str; + for(unsigned int i=0; i<d_str.size(); ++i) { + str += (char)d_str[i]; + } + return str; + } + + unsigned size() const { + return d_str.size(); + } + + String substr(unsigned i) const { + std::vector<unsigned int> ret_vec; + std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; + //for(unsigned k=0; k<i; k++) ++itr; + ret_vec.insert(ret_vec.end(), itr, d_str.end()); + return String(ret_vec); + } + String substr(unsigned i, unsigned j) const { + std::vector<unsigned int> ret_vec; + std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; + //for(unsigned k=0; k<i; k++) ++itr; + //std::vector<unsigned int>::const_iterator itr2 = itr; + //for(unsigned k=0; k<j; k++) ++itr2; + ret_vec.insert( ret_vec.end(), itr, itr + j ); + return String(ret_vec); + } +};/* class String */ + +namespace strings { + +struct StringHashFunction { + size_t operator()(const ::CVC4::String& s) const { + return __gnu_cxx::hash<const char*>()(s.toString().c_str()); + } +};/* struct StringHashFunction */ + +} + +inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const String& s) { + return os << "\"" << s.toString() << "\""; +} + +class CVC4_PUBLIC RegExp { + +private: + std::string d_str; + +public: + RegExp() {} + + RegExp(const std::string s) + : d_str(s) {} + + ~RegExp() {} + + RegExp& operator =(const RegExp& y) { + if(this != &y) d_str = y.d_str; + return *this; + } + + bool operator ==(const RegExp& y) const { + return d_str == y.d_str ; + } + + bool operator !=(const RegExp& y) const { + return d_str != y.d_str ; + } + + String concat (const RegExp& other) const { + return String(d_str + other.d_str); + } + + bool operator <(const RegExp& y) const { + return d_str < y.d_str; + } + + bool operator >(const RegExp& y) const { + return d_str > y.d_str ; + } + + bool operator <=(const RegExp& y) const { + return d_str <= y.d_str; + } + + bool operator >=(const RegExp& y) const { + return d_str >= y.d_str ; + } + + /* + * Convenience functions + */ + + size_t hash() const { + unsigned int h = 1; + + for (size_t i = 0; i < d_str.length(); ++i) { + h = (h << 5) + d_str[i]; + } + + return h; + } + + std::string toString() const { + return d_str; + } + + unsigned size() const { + return d_str.size(); + } +};/* class String */ + +/** + * Hash function for the RegExp constants. + */ +struct CVC4_PUBLIC RegExpHashFunction { + inline size_t operator()(const RegExp& s) const { + return s.hash(); + } +};/* struct RegExpHashFunction */ + +inline std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const RegExp& s) { + return os << s.toString(); +} +}/* CVC4 namespace */ + +#endif /* __CVC4__STRING_H */ diff --git a/test/Makefile.am b/test/Makefile.am index 1ac00eb82..104d40ab1 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -55,6 +55,7 @@ subdirs_to_check = \ regress/regress0/unconstrained \ regress/regress0/decision \ regress/regress0/fmf \ + regress/regress0/strings \ regress/regress1 \ regress/regress2 \ regress/regress3 diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 082662a1e..80c377972 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf -DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings +DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings BINARY = cvc4 LOG_COMPILER = @srcdir@/../run_regression diff --git a/test/regress/regress0/strings/Makefile b/test/regress/regress0/strings/Makefile new file mode 100644 index 000000000..1c399b3e4 --- /dev/null +++ b/test/regress/regress0/strings/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/strings + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am new file mode 100644 index 000000000..37da1091e --- /dev/null +++ b/test/regress/regress0/strings/Makefile.am @@ -0,0 +1,47 @@ +SUBDIRS = . + +BINARY = cvc4 +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + cardinality.smt2 \ + str001.smt2 \ + str002.smt2 \ + str003.smt2 \ + str004.smt2 \ + str005.smt2 \ + loop001.smt2 +# loop002.smt2 \ +# loop003.smt2 \ +# loop004.smt2 \ +# loop005.smt2 \ +# loop006.smt2 + +FAILING_TESTS = + +EXTRA_DIST = $(TESTS) + + +# and make sure to distribute it +EXTRA_DIST += + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2 new file mode 100644 index 000000000..5c4771d71 --- /dev/null +++ b/test/regress/regress0/strings/cardinality.smt2 @@ -0,0 +1,23 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(set-option :str-cardinality 2) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun i () Int) + +(assert (= i 1)) +(assert (= (str.len x) i)) +(assert (= (str.len y) i)) +(assert (= (str.len z) i)) +(assert (= (str.len w) 2)) + +(assert (not (= x y))) +(assert (not (= x z))) +(assert (not (= z y))) + + +(check-sat) diff --git a/test/regress/regress0/strings/loop001.smt2 b/test/regress/regress0/strings/loop001.smt2 new file mode 100644 index 000000000..11460b335 --- /dev/null +++ b/test/regress/regress0/strings/loop001.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun w1 () String) +(declare-fun w2 () String) + +(assert (= (str.++ x "a") (str.++ "b" x))) + +(check-sat) diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2 new file mode 100644 index 000000000..a47b959f5 --- /dev/null +++ b/test/regress/regress0/strings/loop002.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +; EXIT: 10 +; +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun w1 () String) +(declare-fun w2 () String) + +(assert (= (str.++ x "ba") (str.++ "ab" x))) + +(check-sat) diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2 new file mode 100644 index 000000000..a535f7583 --- /dev/null +++ b/test/regress/regress0/strings/loop003.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +; EXIT: 10 +; +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun w1 () String) +(declare-fun w2 () String) + +(assert (= (str.++ x "aaaae") (str.++ "eaaaa" x))) + +(check-sat) diff --git a/test/regress/regress0/strings/loop004.smt2 b/test/regress/regress0/strings/loop004.smt2 new file mode 100644 index 000000000..7b39bf2d3 --- /dev/null +++ b/test/regress/regress0/strings/loop004.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +; EXIT: 10 +; +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun w1 () String) +(declare-fun w2 () String) + +(assert (= (str.++ x y z) (str.++ y z x))) + +(check-sat) diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 new file mode 100644 index 000000000..ec294b9bb --- /dev/null +++ b/test/regress/regress0/strings/loop005.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +; EXIT: 10 +; +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun w1 () String) +(declare-fun w2 () String) + +(assert (= (str.++ x y z) (str.++ x z y))) +(assert (= (str.++ x w z) (str.++ x z w))) +(assert (not (= y w))) +(assert (> (str.len z) 0)) + +(check-sat) diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2 new file mode 100644 index 000000000..8c3690c61 --- /dev/null +++ b/test/regress/regress0/strings/loop006.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +; EXIT: 10 +; +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(declare-fun w1 () String) +(declare-fun w2 () String) + +(assert (= (str.++ x y z) (str.++ x z y))) + +(check-sat) diff --git a/test/regress/regress0/strings/str001.smt2 b/test/regress/regress0/strings/str001.smt2 new file mode 100644 index 000000000..8ae10edbe --- /dev/null +++ b/test/regress/regress0/strings/str001.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun xx () String) +(declare-fun yy () String) +(declare-fun zz () String) +(declare-fun ww () String) +(declare-fun pp () String) +(declare-fun qq () String) + +(assert (= (str.++ xx yy zz) (str.++ ww qq))) +(assert (= ww (str.++ xx pp))) +(assert (= yy pp)) +(assert (not (= zz qq))) + +(check-sat) diff --git a/test/regress/regress0/strings/str002.smt2 b/test/regress/regress0/strings/str002.smt2 new file mode 100644 index 000000000..98b3e1e00 --- /dev/null +++ b/test/regress/regress0/strings/str002.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun xx () String) +(declare-fun yy () String) +(declare-fun zz () String) +(declare-fun ww () String) +(declare-fun pp () String) +(declare-fun qq () String) + +; assoc +(assert (or (= xx (str.++ yy "aa")) (= zz (str.++ yy "aa")) +)) +(assert (and (not (= (str.++ xx "bb") (str.++ yy "aa" "bb"))) + (not (= (str.++ zz "bb") (str.++ yy "aa" "bb"))) +)) + +(check-sat) diff --git a/test/regress/regress0/strings/str003.smt2 b/test/regress/regress0/strings/str003.smt2 new file mode 100644 index 000000000..c88e1233e --- /dev/null +++ b/test/regress/regress0/strings/str003.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun xx () String) +(declare-fun yy () String) +(declare-fun zz () String) +(declare-fun ww () String) +(declare-fun pp () String) +(declare-fun qq () String) + +(assert (= "ab" (str.++ "a" xx))) +(assert (not (= xx yy))) +(assert (= "b" yy)) + +(check-sat) diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2 new file mode 100644 index 000000000..d4763adee --- /dev/null +++ b/test/regress/regress0/strings/str004.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun xx () String) +(declare-fun yy () String) +(declare-fun zz () String) +(declare-fun ww () String) +(declare-fun pp () String) +(declare-fun qq () String) + +; Morgan says it needs length bound +(assert (> (str.len yy) (str.len xx))) +(assert (= xx (str.++ xx yy))) + +(check-sat) diff --git a/test/regress/regress0/strings/str005.smt2 b/test/regress/regress0/strings/str005.smt2 new file mode 100644 index 000000000..4916b1df4 --- /dev/null +++ b/test/regress/regress0/strings/str005.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun xx () String) +(declare-fun yy () String) +(declare-fun zz () String) +(declare-fun ww () String) +(declare-fun pp () String) +(declare-fun qq () String) + +; common postfix +;(assert (= (str.++ xx "aa") (str.++ xx "bb"))) + +(assert (= (str.len yy) 0)) +(assert (not (= yy ""))) + +(check-sat) + diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 39d8aadb1..8f9417966 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -511,6 +511,7 @@ public: info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); + info.disableTheory(THEORY_STRINGS); info.arithOnlyLinear(); info.disableIntegers(); info.lock(); |