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
=================
}
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());
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]));
}
}
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) {
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) {
/** 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();
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));
/** 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;
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;
}
../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 \
../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 \
** \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
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;
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;
** \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
QF_NIA,
QF_NRA,
QF_RDL,
+ QF_S, // nonstandard (for string theory)
QF_SAT,
QF_UF,
QF_UFIDL,
THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
THEORY_REALS,
THEORY_REALS_INTS,
+ THEORY_STRINGS,
THEORY_QUANTIFIERS
};
** \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
: 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) ); }
)*
@declarations {
CVC4::Kind k;
std::string s;
+ std::vector<unsigned int> s_vec;
}
: INTEGER_LITERAL
{ sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
{ 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)
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
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
;
| 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
;
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 |.
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:
addBitvectorOperators();
break;
+ case THEORY_STRINGS:
+ defineType("String", getExprManager()->stringType());
+ addStringOperators();
+ break;
+
case THEORY_QUANTIFIERS:
break;
addTheory(THEORY_BITVECTORS);
}
+ if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
+ addTheory(THEORY_STRINGS);
+ }
+
if(d_logic.isQuantified()) {
addTheory(THEORY_QUANTIFIERS);
}
THEORY_REALS,
THEORY_REALS_INTS,
THEORY_QUANTIFIERS,
+ THEORY_STRINGS
};
private:
void addBitvectorOperators();
+ void addStringOperators();
+
};/* class Smt2 */
}/* CVC4::parser namespace */
-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
@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 \
"::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
}
};/* 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) {
** \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
ss << "DT";
++seen;
}
+ if(d_theories[THEORY_STRINGS]) {
+ ss << "S";
+ ++seen;
+ }
if(d_theories[THEORY_ARITH]) {
if(isDifferenceLogic()) {
ss << (areIntegersUsed() ? "I" : "");
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;
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/strings
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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
--- /dev/null
+# 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
--- /dev/null
+#
+# 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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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);
+}
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
util_model.h \
util_model.cpp \
sort_inference.h \
- sort_inference.cpp
+ sort_inference.cpp \
+ regexp.h
libstatistics_la_SOURCES = \
statistics_registry.h \
--- /dev/null
+/********************* */
+/*! \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 */
regress/regress0/unconstrained \
regress/regress0/decision \
regress/regress0/fmf \
+ regress/regress0/strings \
regress/regress1 \
regress/regress2 \
regress/regress3
-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
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/strings
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
--- /dev/null
+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:
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
+
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
+ info.disableTheory(THEORY_STRINGS);
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
projects / cvc5.git / commitdiff