diff options
59 files changed, 1248 insertions, 631 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 30cdf15b7..52f46147c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -298,6 +298,7 @@ libcvc4_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.h + theory/arith/nl_lemma_utils.h theory/arith/nl_model.cpp theory/arith/nl_model.h theory/arith/nonlinear_extension.cpp diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2a254328a..31453b618 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -263,6 +263,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {STRING_LEQ, CVC4::Kind::STRING_LEQ}, {STRING_PREFIX, CVC4::Kind::STRING_PREFIX}, {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX}, + {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT}, {STRING_ITOS, CVC4::Kind::STRING_ITOS}, {STRING_STOI, CVC4::Kind::STRING_STOI}, {CONST_STRING, CVC4::Kind::CONST_STRING}, @@ -270,6 +271,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT}, {REGEXP_UNION, CVC4::Kind::REGEXP_UNION}, {REGEXP_INTER, CVC4::Kind::REGEXP_INTER}, + {REGEXP_DIFF, CVC4::Kind::REGEXP_DIFF}, {REGEXP_STAR, CVC4::Kind::REGEXP_STAR}, {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS}, {REGEXP_OPT, CVC4::Kind::REGEXP_OPT}, @@ -277,6 +279,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP}, {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY}, {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA}, + {REGEXP_COMPLEMENT, CVC4::Kind::REGEXP_COMPLEMENT}, /* Quantifiers --------------------------------------------------------- */ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, @@ -526,6 +529,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::STRING_LEQ, STRING_LEQ}, {CVC4::Kind::STRING_PREFIX, STRING_PREFIX}, {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX}, + {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT}, {CVC4::Kind::STRING_ITOS, STRING_ITOS}, {CVC4::Kind::STRING_STOI, STRING_STOI}, {CVC4::Kind::CONST_STRING, CONST_STRING}, @@ -533,6 +537,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT}, {CVC4::Kind::REGEXP_UNION, REGEXP_UNION}, {CVC4::Kind::REGEXP_INTER, REGEXP_INTER}, + {CVC4::Kind::REGEXP_DIFF, REGEXP_DIFF}, {CVC4::Kind::REGEXP_STAR, REGEXP_STAR}, {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS}, {CVC4::Kind::REGEXP_OPT, REGEXP_OPT}, @@ -540,6 +545,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP}, {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, + {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, /* Quantifiers ----------------------------------------------------- */ {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, @@ -1830,9 +1836,9 @@ DatatypeDecl::DatatypeDecl(const Solver* s, bool isCoDatatype) { std::vector<Type> tparams; - for (const Sort& s : params) + for (const Sort& p : params) { - tparams.push_back(*s.d_type); + tparams.push_back(*p.d_type); } d_dtype = std::shared_ptr<CVC4::Datatype>( new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype)); diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 591ff9b1e..eb8575907 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2046,6 +2046,16 @@ enum CVC4_PUBLIC Kind : int32_t */ STRING_SUFFIX, /** + * String is-digit. + * Returns true if string s is digit (it is one of "0", ..., "9"). + * Parameters: 1 + * -[1]: Term of sort String + * Create with: + * mkTerm(Kind kind, Term child1) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_IS_DIGIT, + /** * Integer to string. * If the integer is negative this operator returns the empty string. * Parameters: 1 @@ -2111,6 +2121,15 @@ enum CVC4_PUBLIC Kind : int32_t */ REGEXP_INTER, /** + * Regexp difference. + * Parameters: 2 + * -[1]..[2]: Terms of Regexp sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_DIFF, + /** * Regexp *. * Parameters: 1 * -[1]: Term of sort Regexp @@ -2172,6 +2191,14 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind) */ REGEXP_SIGMA, + /** + * Regexp complement. + * Parameters: 1 + * -[1]: Term of sort RegExp + * Create with: + * mkTerm(Kind kind, Term child1) + */ + REGEXP_COMPLEMENT, #if 0 /* regexp rv (internal use only) */ REGEXP_RV, diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 5f43fb24f..dd5f12b28 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -223,6 +223,41 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ PrettyCheckArgument( !isResolved(), this, "cannot set sygus type to a finalized Datatype"); + // We can be in a case where the only rule specified was + // (Constant T), in which case we have not yet added a constructor. We + // ensure an arbitrary constant is added in this case. We additionally + // add a constant if the grammar has only non-nullary constructors, since this + // ensures the datatype is well-founded (see 3423). + // Notice we only want to do this for sygus datatypes that are user-provided. + // At the moment, the condition !allow_all implies the grammar is + // user-provided and hence may require a default constant. + // TODO (https://github.com/CVC4/cvc4-projects/issues/38): + // In an API for SyGuS, it probably makes more sense for the user to + // explicitly add the "any constant" constructor with a call instead of + // passing a flag. This would make the block of code unnecessary. + if (allow_const && !allow_all) + { + // if i don't already have a constant (0-ary constructor) + bool hasConstant = false; + for (unsigned i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + if ((*this)[i].getNumArgs() == 0) + { + hasConstant = true; + break; + } + } + if (!hasConstant) + { + // add an arbitrary one + Expr op = st.mkGroundTerm(); + std::stringstream cname; + cname << op; + std::vector<Type> cargs; + addSygusConstructor(op, cname.str(), cargs); + } + } + TypeNode stn = TypeNode::fromType(st); Node bvln = Node::fromExpr(bvl); d_internal->setSygus(stn, bvln, allow_const, allow_all); diff --git a/src/expr/node.h b/src/expr/node.h index 4bef8db74..e07499b69 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1368,15 +1368,15 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, nb << getOperator().substitute(node, replacement, cache); } } - for (const Node& n : *this) + for (const_iterator it = begin(), iend = end(); it != iend; ++it) { - if (n == node) + if (*it == node) { nb << replacement; } else { - nb << n.substitute(node, replacement, cache); + nb << (*it).substitute(node, replacement, cache); } } @@ -1435,9 +1435,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, replacementsBegin, replacementsEnd, cache); } - for (const Node& n : *this) + for (const_iterator it = begin(), iend = end(); it != iend; ++it) { - nb << n.substitute( + nb << (*it).substitute( nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache); } Node n = nb; @@ -1483,9 +1483,9 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, // push the operator nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache); } - for (const Node& n : *this) + for (const_iterator it = begin(), iend = end(); it != iend; ++it) { - nb << n.substitute(substitutionsBegin, substitutionsEnd, cache); + nb << (*it).substitute(substitutionsBegin, substitutionsEnd, cache); } Node n = nb; cache[*this] = n; diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 9619e69d1..595adda55 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -129,6 +129,32 @@ bool hasSubtermMulti(TNode n, TNode t) return false; } +bool hasSubtermKind(Kind k, Node n) +{ + std::unordered_set<TNode, TNodeHashFunction> visited; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() == k) + { + return true; + } + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + return false; +} + bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict) { if (t.empty()) diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 929e1c5ef..e47029284 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -45,6 +45,13 @@ bool hasSubterm(TNode n, TNode t, bool strict = false); bool hasSubtermMulti(TNode n, TNode t); /** + * @param k The kind of node to check + * @param n The node to search in. + * @return true iff there is a term in n that has kind k + */ +bool hasSubtermKind(Kind k, Node n); + +/** * Check if the node n has a subterm that occurs in t. * @param n The node to search in * @param t The set of subterms to search for diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index dca61fe48..33ca7bcf2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -240,6 +240,7 @@ tokens { REGEXP_LOOP_TOK = 'RE_LOOP'; REGEXP_EMPTY_TOK = 'RE_EMPTY'; REGEXP_SIGMA_TOK = 'RE_SIGMA'; + REGEXP_COMPLEMENT_TOK = 'RE_COMPLEMENT'; SETS_CARD_TOK = 'CARD'; @@ -1836,23 +1837,8 @@ postfixTerm[CVC4::Expr& f] { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); } ) ( typeAscription[f, t] - { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { - std::vector<CVC4::Expr> v; - Expr e = f.getOperator(); - const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() )); - v.insert(v.end(), f.begin(), f.end()); - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); - } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) { - f = MK_CONST(CVC4::EmptySet(t)); - } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) { - f = EXPR_MANAGER->mkNullaryOperator(t, kind::UNIVERSE_SET); - } else { - if(f.getType() != t) { - PARSER_STATE->parseError("Type ascription not satisfied."); - } - } + { + f = PARSER_STATE->applyTypeAscription(f,t).getExpr(); } )? ; @@ -2060,6 +2046,8 @@ stringTerm[CVC4::Expr& f] { f = MK_EXPR(CVC4::kind::REGEXP_RANGE, f, f2); } | REGEXP_LOOP_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN { f = MK_EXPR(CVC4::kind::REGEXP_LOOP, f, f2, f3); } + | REGEXP_COMPLEMENT_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::REGEXP_COMPLEMENT, f); } | REGEXP_EMPTY_TOK { f = MK_EXPR(CVC4::kind::REGEXP_EMPTY, std::vector<Expr>()); } | REGEXP_SIGMA_TOK diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index 32d583010..a224b2511 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -19,6 +19,7 @@ #include <string> +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/kind.h" @@ -35,6 +36,7 @@ namespace CVC4 { * (2) A string name. * (3) An expression expr. * (4) A type t. + * (5) An operator object. * * Examples: * @@ -66,26 +68,43 @@ struct CVC4_PUBLIC ParseOp Expr d_expr; /** The type associated with the parsed operator, if it exists */ Type d_type; + /** The operator associated with the parsed operator, if it exists */ + api::Op d_op; /* Return true if this is equal to 'p'. */ bool operator==(const ParseOp& p) const { return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr - && d_type == p.d_type; + && d_type == p.d_type && d_op == p.d_op; } }; inline std::ostream& operator<<(std::ostream& os, const ParseOp& p) { + std::stringstream out; + out << "(ParseOp "; if (!p.d_expr.isNull()) { - return os << p.d_expr; + out << " :expr " << p.d_expr; } - else if (p.d_kind != kind::NULL_EXPR) + if (!p.d_op.isNull()) { - return os << p.d_kind; + out << " :op " << p.d_op; } - return os << "ParseOp::unknown"; + if (p.d_kind != kind::NULL_EXPR) + { + out << " :kind " << p.d_kind; + } + if (!p.d_type.isNull()) + { + out << " :type " << p.d_type; + } + if (!p.d_name.empty()) + { + out << " :name " << p.d_name; + } + out << ")"; + return os << out.str(); } } // namespace CVC4 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 663be7f1f..d2577433e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -515,6 +515,78 @@ Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args) return expr; } +api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) +{ + api::Kind k = t.getKind(); + if (k == api::EMPTYSET) + { + t = d_solver->mkEmptySet(s); + } + else if (k == api::UNIVERSE_SET) + { + t = d_solver->mkUniverseSet(s); + } + else if (k == api::SEP_NIL) + { + t = d_solver->mkSepNil(s); + } + else if (k == api::APPLY_CONSTRUCTOR) + { + std::vector<api::Term> children(t.begin(), t.end()); + // apply type ascription to the operator and reconstruct + children[0] = applyTypeAscription(children[0], s); + t = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, children); + } + // !!! temporary until datatypes are refactored in the new API + api::Sort etype = t.getSort(); + if (etype.isConstructor()) + { + api::Sort etype = t.getSort(); + // get the datatype that t belongs to + api::Sort etyped = etype.getConstructorCodomainSort(); + api::Datatype d = etyped.getDatatype(); + // lookup by name + api::DatatypeConstructor dc = d.getConstructor(t.toString()); + + // Type ascriptions only have an effect on the node structure if this is a + // parametric datatype. + if (s.isParametricDatatype()) + { + ExprManager* em = getExprManager(); + // apply type ascription to the operator + Expr e = t.getExpr(); + const DatatypeConstructor& dtc = + Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + t = api::Term(em->mkExpr( + kind::APPLY_TYPE_ASCRIPTION, + em->mkConst( + AscriptionType(dtc.getSpecializedConstructorType(s.getType()))), + e)); + } + // the type of t does not match the sort s by design (constructor type + // vs datatype type), thus we use an alternative check here. + if (t.getSort().getConstructorCodomainSort() != s) + { + std::stringstream ss; + ss << "Type ascription on constructor not satisfied, term " << t + << " expected sort " << s << " but has sort " + << t.getSort().getConstructorCodomainSort(); + parseError(ss.str()); + } + return t; + } + // otherwise, nothing to do + // check that the type is correct + if (t.getSort() != s) + { + std::stringstream ss; + ss << "Type ascription not satisfied, term " << t << " expected sort " << s + << " but has sort " << t.getSort(); + parseError(ss.str()); + } + return t; +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch (type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index 8447eb4dc..d40236208 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -678,6 +678,30 @@ public: */ Expr mkHoApply(Expr expr, std::vector<Expr>& args); + /** Apply type ascription + * + * Return term t with a type ascription applied to it. This is used for + * syntax like (as t T) in smt2 and t::T in the CVC language. This includes: + * - (as emptyset (Set T)) + * - (as univset (Set T)) + * - (as sep.nil T) + * - (cons T) + * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor. + * + * The term to ascribe t is a term whose kind and children (but not type) + * are equivalent to that of the term returned by this method. + * + * Notice that method is not necessarily a cast. In actuality, the above terms + * should be understood as symbols indexed by types. However, SMT-LIB does not + * permit types as indices, so we must use, e.g. (as emptyset (Set T)) + * instead of (_ emptyset (Set T)). + * + * @param t The term to ascribe a type + * @param s The sort to ascribe + * @return Term t with sort s ascribed. + */ + api::Term applyTypeAscription(api::Term t, api::Sort s); + /** * Add an operator to the current legal set. * diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 66831c0c4..caa3e471f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1036,18 +1036,7 @@ sygusGrammar[CVC4::Type & ret, // We can be in a case where the only rule specified was (Variable T) // and there are no variables of type T, in which case this is a bogus // grammar. This results in the error below. - // We can also be in a case where the only rule specified was - // (Constant T), in which case we have not yet added a constructor. We - // ensure an arbitrary constant is added in this case. We additionally - // add a constant if the grammar allows it regardless of whether the - // datatype has other constructors, since this ensures the datatype is - // well-founded (see 3423). - if (aci) - { - Expr c = btt.mkGroundTerm(); - PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres); - } - else if (datatypes[i].getNumConstructors() == 0) + if (datatypes[i].getNumConstructors() == 0) { std::stringstream se; se << "Grouped rule listing for " << datatypes[i].getName() @@ -1931,12 +1920,12 @@ qualIdentifier[CVC4::ParseOp& p] ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { p.d_kind = kind::STORE_ALL; - PARSER_STATE->applyTypeAscription(p, type); + PARSER_STATE->parseOpApplyTypeAscription(p, type); } | identifier[p] sortSymbol[type, CHECK_DECLARED] { - PARSER_STATE->applyTypeAscription(p, type); + PARSER_STATE->parseOpApplyTypeAscription(p, type); } ) RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 8c2b50b04..ff155d0f9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -171,6 +171,7 @@ void Smt2::addStringOperators() { } addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); + addOperator(kind::STRING_IS_DIGIT, "str.is_digit" ); // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -200,6 +201,8 @@ void Smt2::addStringOperators() { addOperator(kind::REGEXP_OPT, "re.opt"); addOperator(kind::REGEXP_RANGE, "re.range"); addOperator(kind::REGEXP_LOOP, "re.loop"); + addOperator(kind::REGEXP_COMPLEMENT, "re.comp"); + addOperator(kind::REGEXP_DIFF, "re.diff"); addOperator(kind::STRING_LT, "str.<"); addOperator(kind::STRING_LEQ, "str.<="); } @@ -754,12 +757,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) warning("Logics in sygus are assumed to contain quantifiers."); warning("Omit QF_ from the logic to avoid this warning."); } - // get unlocked copy, modify, copy and relock - LogicInfo log(d_logic.getUnlockedCopy()); - // enable everything needed for sygus - log.enableSygus(); - d_logic = log; - d_logic.lock(); } // Core theory belongs to every logic @@ -1578,8 +1575,10 @@ InputLanguage Smt2::getLanguage() const return em->getOptions().getInputLanguage(); } -void Smt2::applyTypeAscription(ParseOp& p, Type type) +void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) { + Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type + << std::endl; // (as const (Array T1 T2)) if (p.d_kind == kind::STORE_ALL) { @@ -1612,66 +1611,12 @@ void Smt2::applyTypeAscription(ParseOp& p, Type type) parseError(ss.str()); } } - ExprManager* em = getExprManager(); - Type etype = p.d_expr.getType(); - Kind ekind = p.d_expr.getKind(); Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr; - Trace("parser-qid") << " " << ekind << " " << etype; + Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType(); Trace("parser-qid") << std::endl; - if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype()) - { - // nullary constructors with a type ascription - // could be a parametric constructor or just an overloaded constructor - DatatypeType dtype = static_cast<DatatypeType>(type); - if (dtype.isParametric()) - { - std::vector<Expr> v; - Expr e = p.d_expr.getOperator(); - const DatatypeConstructor& dtc = - Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))), - p.d_expr.getOperator())); - v.insert(v.end(), p.d_expr.begin(), p.d_expr.end()); - p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v); - } - } - else if (etype.isConstructor()) - { - // a non-nullary constructor with a type ascription - DatatypeType dtype = static_cast<DatatypeType>(type); - if (dtype.isParametric()) - { - const DatatypeConstructor& dtc = - Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)]; - p.d_expr = em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))), - p.d_expr); - } - } - else if (ekind == kind::EMPTYSET) - { - Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type - << std::endl; - p.d_expr = em->mkConst(EmptySet(type)); - } - else if (ekind == kind::UNIVERSE_SET) - { - p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET); - } - else if (ekind == kind::SEP_NIL) - { - // We don't want the nil reference to be a constant: for instance, it - // could be of type Int but is not a const rational. However, the - // expression has 0 children. So we convert to a SEP_NIL variable. - p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL); - } - else if (etype != type) - { - parseError("Type ascription not satisfied."); - } + // otherwise, we process the type ascription + p.d_expr = + applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr(); } Expr Smt2::parseOpToExpr(ParseOp& p) diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 954bca314..35ac781f5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -516,7 +516,7 @@ class Smt2 : public Parser * - If p's expression field is set, then we leave p unchanged, check if * that expression has the given type and throw a parse error otherwise. */ - void applyTypeAscription(ParseOp& p, Type type); + void parseOpApplyTypeAscription(ParseOp& p, Type type); /** * This converts a ParseOp to expression, assuming it is a standalone term. * diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 150e41b8f..372df90ce 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -39,9 +39,9 @@ namespace { // TODO: clean this up struct intToBV_stack_element { - TNode node; - bool children_added; - intToBV_stack_element(TNode node) : node(node), children_added(false) {} + TNode d_node; + bool d_children_added; + intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {} }; /* struct intToBV_stack_element */ Node intToBVMakeBinary(TNode n, NodeMap& cache) @@ -54,7 +54,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) { // The current node we are processing intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; NodeMap::iterator find = cache.find(current); if (find != cache.end()) @@ -62,7 +62,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) toVisit.pop_back(); continue; } - if (stackHead.children_added) + if (stackHead.d_children_added) { // Children have been processed, so rebuild this node Node result; @@ -99,7 +99,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) // Mark that we have added the children if any if (current.getNumChildren() > 0) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the children for (TNode::iterator child_it = current.begin(); child_it != current.end(); @@ -138,7 +138,7 @@ Node intToBV(TNode n, NodeMap& cache) { // The current node we are processing intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; // If node is already in the cache we're done, pop from the stack NodeMap::iterator find = cache.find(current); @@ -150,7 +150,7 @@ Node intToBV(TNode n, NodeMap& cache) // Not yet substituted, so process NodeManager* nm = NodeManager::currentNM(); - if (stackHead.children_added) + if (stackHead.d_children_added) { // Children have been processed, so rebuild this node vector<Node> children; @@ -245,7 +245,7 @@ Node intToBV(TNode n, NodeMap& cache) // Mark that we have added the children if any if (current.getNumChildren() > 0) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the children for (TNode::iterator child_it = current.begin(); child_it != current.end(); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 28471de72..886be0cfa 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -84,8 +84,9 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) void Printer::toStreamSygus(std::ostream& out, TNode n) const { // no sygus-specific printing associated with this printer, - // just print the original term - toStream(out, n, -1, false, 1); + // just print the original term, without letification (the fifth argument is + // set to 0). + toStream(out, n, -1, false, 0); } void Printer::toStream(std::ostream& out, const Model& m) const diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c1e8c617f..13a64a2c3 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -666,6 +666,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::REGEXP_OPT: case kind::REGEXP_RANGE: case kind::REGEXP_LOOP: + case kind::REGEXP_COMPLEMENT: case kind::REGEXP_EMPTY: case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break; @@ -1237,6 +1238,7 @@ static string smtKindString(Kind k, Variant v) case kind::REGEXP_OPT: return "re.opt"; case kind::REGEXP_RANGE: return "re.range"; case kind::REGEXP_LOOP: return "re.loop"; + case kind::REGEXP_COMPLEMENT: return "re.comp"; //sep theory case kind::SEP_STAR: return "sep"; @@ -1521,7 +1523,8 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const { out << "("; } - out << dt[cIndex].getSygusOp(); + // print operator without letification (the fifth argument is set to 0). + toStream(out, dt[cIndex].getSygusOp(), -1, false, 0); if (n.getNumChildren() > 0) { for (Node nc : n) @@ -1536,15 +1539,12 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const } } Node p = n.getAttribute(theory::SygusPrintProxyAttribute()); - if (!p.isNull()) + if (p.isNull()) { - out << p; - } - else - { - // cannot convert term to analog, print original - out << n; + p = n; } + // cannot convert term to analog, print original, without letification. + toStream(out, p, -1, false, 0); } static void toStream(std::ostream& out, const AssertCommand* c) diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp index ae1d97c64..92a89a18e 100644 --- a/src/printer/sygus_print_callback.cpp +++ b/src/printer/sygus_print_callback.cpp @@ -78,8 +78,9 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p, sbody = sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + // print to stream without letification std::stringstream body_out; - body_out << sbody; + p->toStream(body_out, sbody, -1, false, 0); // do string substitution Assert(e.getNumChildren() == d_args.size()); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 081e36953..915dc603e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1313,13 +1313,18 @@ void SmtEngine::setDefaults() { { // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; - // we change the logic to incorporate sygus immediately - d_logic = d_logic.getUnlockedCopy(); - d_logic.enableSygus(); - d_logic.lock(); } } + // We now know whether the input is sygus. Update the logic to incorporate + // the theories we need internally for handling sygus problems. + if (is_sygus) + { + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableSygus(); + d_logic.lock(); + } + // sygus core connective requires unsat cores if (options::sygusCoreConnective()) { @@ -3983,6 +3988,8 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) { + SmtScope smts(this); + finalOptionsAreSet(); d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n"; Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); @@ -3991,6 +3998,8 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) { + SmtScope smts(this); + finalOptionsAreSet(); // do nothing (the command is spurious) Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; // don't need to set that the conjecture is stale @@ -4000,6 +4009,8 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id, Expr var, Type type) { + SmtScope smts(this); + finalOptionsAreSet(); d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); @@ -4044,6 +4055,7 @@ void SmtEngine::declareSynthFun(const std::string& id, void SmtEngine::assertSygusConstraint(Expr constraint) { SmtScope smts(this); + finalOptionsAreSet(); d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; @@ -4058,6 +4070,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, const Expr& post) { SmtScope smts(this); + finalOptionsAreSet(); // build invariant constraint // get variables (regular and their respective primed versions) diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h index 58070c0b2..47ed6eff8 100644 --- a/src/smt_util/node_visitor.h +++ b/src/smt_util/node_visitor.h @@ -59,13 +59,15 @@ public: */ struct stack_element { /** The node to be visited */ - TNode node; + TNode d_node; /** The parent of the node */ - TNode parent; + TNode d_parent; /** Have the children been queued up for visitation */ - bool children_added; + bool d_childrenAdded; stack_element(TNode node, TNode parent) - : node(node), parent(parent), children_added(false) {} + : d_node(node), d_parent(parent), d_childrenAdded(false) + { + } };/* struct preprocess_stack_element */ /** @@ -84,20 +86,24 @@ public: while (!toVisit.empty()) { stack_element& stackHead = toVisit.back(); // The current node we are processing - TNode current = stackHead.node; - TNode parent = stackHead.parent; + TNode current = stackHead.d_node; + TNode parent = stackHead.d_parent; if (visitor.alreadyVisited(current, parent)) { // If already visited, we're done toVisit.pop_back(); - } else if (stackHead.children_added) { + } + else if (stackHead.d_childrenAdded) + { // Call the visitor visitor.visit(current, parent); // Done with this node, remove from the stack toVisit.pop_back(); - } else { + } + else + { // Mark that we have added the children - stackHead.children_added = true; + stackHead.d_childrenAdded = true; // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; diff --git a/src/theory/arith/nl_lemma_utils.h b/src/theory/arith/nl_lemma_utils.h new file mode 100644 index 000000000..74886a1fb --- /dev/null +++ b/src/theory/arith/nl_lemma_utils.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file nl_lemma_utils.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utilities for processing lemmas from the non-linear solver + **/ + +#ifndef CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H +#define CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H + +#include <tuple> +#include <vector> +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +/** + * A side effect of adding a lemma in the non-linear solver. This is used + * to specify how the state of the non-linear solver should update. This + * includes: + * - A set of secant points to record (for transcendental secant plane + * inferences). + */ +struct NlLemmaSideEffect +{ + NlLemmaSideEffect() {} + ~NlLemmaSideEffect() {} + /** secant points to add + * + * A member (tf, d, c) in this vector indicates that point c should be added + * to the list of secant points for an application of a transcendental + * function tf for Taylor degree d. This is used for incremental linearization + * for underapproximation (resp. overapproximations) of convex (resp. + * concave) regions of transcendental functions. For details, see + * Cimatti et al., CADE 2017. + */ + std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint; +}; + +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */ diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 929eb4acc..3c1d5f1e9 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -278,6 +278,11 @@ bool NlModel::checkModel(const std::vector<Node>& assertions, std::vector<Node> check_assertions; for (const Node& a : assertions) { + // don't have to check tautological literals + if (d_tautology.find(a) != d_tautology.end()) + { + continue; + } if (d_check_model_solved.find(a) == d_check_model_solved.end()) { Node av = a; @@ -424,6 +429,52 @@ void NlModel::setUsedApproximate() { d_used_approx = true; } bool NlModel::usedApproximate() const { return d_used_approx; } +void NlModel::addTautology(Node n) +{ + // ensure rewritten + n = Rewriter::rewrite(n); + std::unordered_set<TNode, TNodeHashFunction> visited; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() == AND) + { + // children of AND are also implied + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + else + { + // is this an arithmetic literal? + Node atom = cur.getKind() == NOT ? cur[0] : cur; + if ((atom.getKind() == EQUAL && atom[0].getType().isReal()) + || atom.getKind() == LEQ) + { + // Add to tautological literals if it does not contain + // non-linear multiplication. We cannot consider literals + // with non-linear multiplication to be tautological since this + // model object is responsible for checking whether they hold. + // (TODO, cvc4-projects #113: revisit this). + if (!expr::hasSubtermKind(NONLINEAR_MULT, atom)) + { + Trace("nl-taut") << "Tautological literal: " << atom << std::endl; + d_tautology.insert(cur); + } + } + } + } + } while (!visit.empty()); +} + bool NlModel::solveEqualitySimple(Node eq, unsigned d, std::vector<Node>& lemmas) diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h index 354f6f71c..a8746ca2e 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl_model.h @@ -163,6 +163,23 @@ class NlModel void setUsedApproximate(); /** Did we use an approximation during this check? */ bool usedApproximate() const; + /** Set tautology + * + * This states that formula n is a tautology (satisfied in all models). + * We call this on internally generated lemmas. This method computes a + * set of literals that are implied by n, that are hence tautological + * as well, such as: + * l_pi <= real.pi <= u_pi (pi approximations) + * sin(x) = -1*sin(-x) + * where these literals are internally generated for the purposes + * of guiding the models of the linear solver. + * + * TODO (cvc4-projects #113: would be helpful if we could do this even + * more aggressively by ignoring all internally generated literals. + * + * Tautological literals do not need be checked during checkModel. + */ + void addTautology(Node n); //------------------------------ end recording model substitutions and bounds /** print model value, for debugging. @@ -314,6 +331,8 @@ class NlModel std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved; /** did we use an approximation on this call to last-call effort? */ bool d_used_approx; + /** the set of all tautological literals */ + std::unordered_set<Node, NodeHashFunction> d_tautology; }; /* class NlModel */ } // namespace arith diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 65daf8436..2d530d602 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -540,17 +540,38 @@ Node NonlinearExtension::mkMonomialRemFactor( } void NonlinearExtension::sendLemmas(const std::vector<Node>& out, - bool preprocess) + bool preprocess, + std::map<Node, NlLemmaSideEffect>& lemSE) { + std::map<Node, NlLemmaSideEffect>::iterator its; for (const Node& lem : out) { Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; d_containing.getOutputChannel().lemma(lem, false, preprocess); + // process the side effect + its = lemSE.find(lem); + if (its != lemSE.end()) + { + processSideEffect(its->second); + } // add to cache if not preprocess if (!preprocess) { d_lemmas.insert(lem); } + // also indicate this is a tautology + d_model.addTautology(lem); + } +} + +void NonlinearExtension::processSideEffect(const NlLemmaSideEffect& se) +{ + for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint) + { + Node tf = std::get<0>(sp); + unsigned d = std::get<1>(sp); + Node c = std::get<2>(sp); + d_secant_points[tf][d].push_back(c); } } @@ -890,7 +911,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, const std::vector<Node>& xts, std::vector<Node>& lems, std::vector<Node>& lemsPp, - std::vector<Node>& wlems) + std::vector<Node>& wlems, + std::map<Node, NlLemmaSideEffect>& lemSE) { d_ms_vars.clear(); d_ms_proc.clear(); @@ -1262,7 +1284,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } if (options::nlExtTfTangentPlanes()) { - lemmas = checkTranscendentalTangentPlanes(); + lemmas = checkTranscendentalTangentPlanes(lemSE); filterLemmas(lemmas, wlems); } Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." @@ -1297,8 +1319,8 @@ void NonlinearExtension::check(Theory::Effort e) { // If we computed lemmas during collectModelInfo, send them now. if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty()) { - sendLemmas(d_cmiLemmas); - sendLemmas(d_cmiLemmasPp, true); + sendLemmas(d_cmiLemmas, false, d_cmiLemmasSE); + sendLemmas(d_cmiLemmasPp, true, d_cmiLemmasSE); return; } // Otherwise, we will answer SAT. The values that we approximated are @@ -1318,8 +1340,10 @@ void NonlinearExtension::check(Theory::Effort e) { } } -bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems, - std::vector<Node>& mlemsPp) +bool NonlinearExtension::modelBasedRefinement( + std::vector<Node>& mlems, + std::vector<Node>& mlemsPp, + std::map<Node, NlLemmaSideEffect>& lemSE) { // get the assertions std::vector<Node> assertions; @@ -1405,7 +1429,8 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems, if (!false_asserts.empty() || num_shared_wrong_value > 0) { complete_status = num_shared_wrong_value > 0 ? -1 : 0; - checkLastCall(assertions, false_asserts, xts, mlems, mlemsPp, wlems); + checkLastCall( + assertions, false_asserts, xts, mlems, mlemsPp, wlems, lemSE); if (!mlems.empty() || !mlemsPp.empty()) { return true; @@ -1522,10 +1547,11 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel) // run a last call effort check d_cmiLemmas.clear(); d_cmiLemmasPp.clear(); + d_cmiLemmasSE.clear(); if (!d_builtModel.get()) { Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; - modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp); + modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp, d_cmiLemmasSE); } if (d_builtModel.get()) { @@ -3011,7 +3037,8 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { return lemmas; } -std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() +std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes( + std::map<Node, NlLemmaSideEffect>& lemSE) { std::vector<Node> lemmas; Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..." @@ -3051,7 +3078,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() { Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl; unsigned prev = lemmas.size(); - if (!checkTfTangentPlanesFun(tf, d, lemmas)) + if (!checkTfTangentPlanesFun(tf, d, lemmas, lemSE)) { Trace("nl-ext-tftp") << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl; @@ -3069,9 +3096,11 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() return lemmas; } -bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, - unsigned d, - std::vector<Node>& lemmas) +bool NonlinearExtension::checkTfTangentPlanesFun( + Node tf, + unsigned d, + std::vector<Node>& lemmas, + std::map<Node, NlLemmaSideEffect>& lemSE) { Assert(d_model.isRefineableTfFun(tf)); @@ -3257,23 +3286,24 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, Assert(std::find( d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c) == d_secant_points[tf][d].end()); - // insert into the vector - d_secant_points[tf][d].push_back(c); + // Insert into the (temporary) vector. We do not update this vector + // until we are sure this secant plane lemma has been processed. We do + // this by mapping the lemma to a side effect below. + std::vector<Node> spoints = d_secant_points[tf][d]; + spoints.push_back(c); + // sort SortNlModel smv; smv.d_nlm = &d_model; smv.d_isConcrete = true; - std::sort( - d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), smv); + std::sort(spoints.begin(), spoints.end(), smv); // get the resulting index of c unsigned index = - std::find( - d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c) - - d_secant_points[tf][d].begin(); + std::find(spoints.begin(), spoints.end(), c) - spoints.begin(); // bounds are the next closest upper/lower bound values if (index > 0) { - bounds[0] = d_secant_points[tf][d][index - 1]; + bounds[0] = spoints[index - 1]; } else { @@ -3289,9 +3319,9 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, bounds[0] = Rewriter::rewrite(nm->mkNode(MINUS, c, d_one)); } } - if (index < d_secant_points[tf][d].size() - 1) + if (index < spoints.size() - 1) { - bounds[1] = d_secant_points[tf][d][index + 1]; + bounds[1] = spoints[index + 1]; } else { @@ -3310,6 +3340,8 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds[0] << " ... " << bounds[1] << std::endl; + // the secant plane may be conjunction of 1-2 guarded inequalities + std::vector<Node> lemmaConj; for (unsigned s = 0; s < 2; s++) { // compute secant plane @@ -3370,11 +3402,18 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, lem = Rewriter::rewrite(lem); Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl; - // Figure 3 : line 22 - lemmas.push_back(lem); + lemmaConj.push_back(lem); Assert(d_model.computeAbstractModelValue(lem) == d_false); } } + // Figure 3 : line 22 + Assert(!lemmaConj.empty()); + Node lem = + lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj); + lemmas.push_back(lem); + // The side effect says that if lem is added, then we should add the + // secant point c for (tf,d). + lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c)); } return false; } diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 338ae6611..64a601cc5 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -34,6 +34,7 @@ #include "context/context.h" #include "expr/kind.h" #include "expr/node.h" +#include "theory/arith/nl_lemma_utils.h" #include "theory/arith/nl_model.h" #include "theory/arith/theory_arith.h" #include "theory/uf/equality_engine.h" @@ -178,9 +179,13 @@ class NonlinearExtension { * Otherwise, it returns false. In the latter case, the model object d_model * may have information regarding how to construct a model, in the case that * we determined the problem is satisfiable. + * + * The argument lemSE is the "side effect" of the lemmas in mlems and mlemsPp + * (for details, see checkLastCall). */ bool modelBasedRefinement(std::vector<Node>& mlems, - std::vector<Node>& mlemsPp); + std::vector<Node>& mlemsPp, + std::map<Node, NlLemmaSideEffect>& lemSE); /** returns true if the multiset containing the * factors of monomial a is a subset of the multiset * containing the factors of monomial b. @@ -230,13 +235,19 @@ class NonlinearExtension { * output channel as a last resort. In other words, only if we are not * able to establish SAT via a call to checkModel(...) should wlems be * considered. This set typically contains tangent plane lemmas. + * + * The argument lemSE is the "side effect" of the lemmas from the previous + * three calls. If a lemma is mapping to a side effect, it should be + * processed via a call to processSideEffect(...) immediately after the + * lemma is sent (if it is indeed sent on this call to check). */ int checkLastCall(const std::vector<Node>& assertions, const std::vector<Node>& false_asserts, const std::vector<Node>& xts, std::vector<Node>& lems, std::vector<Node>& lemsPp, - std::vector<Node>& wlems); + std::vector<Node>& wlems, + std::map<Node, NlLemmaSideEffect>& lemSE); //---------------------------------------term utilities static bool isArithKind(Kind k); static Node mkLit(Node a, Node b, int status, bool isAbsolute = false); @@ -395,7 +406,11 @@ class NonlinearExtension { /** * Send lemmas in out on the output channel of theory of arithmetic. */ - void sendLemmas(const std::vector<Node>& out, bool preprocess = false); + void sendLemmas(const std::vector<Node>& out, + bool preprocess, + std::map<Node, NlLemmaSideEffect>& lemSE); + /** Process side effect se */ + void processSideEffect(const NlLemmaSideEffect& se); // Returns the NodeMultiset for an existing monomial. const NodeMultiset& getMonomialExponentMap(Node monomial) const; @@ -480,6 +495,8 @@ class NonlinearExtension { */ std::vector<Node> d_cmiLemmas; std::vector<Node> d_cmiLemmasPp; + /** the side effects of the above lemmas */ + std::map<Node, NlLemmaSideEffect> d_cmiLemmasSE; /** * The approximations computed during collectModelInfo. For details, see * NlModel::getModelValueRepair. @@ -872,64 +889,68 @@ class NonlinearExtension { std::vector<Node> checkTranscendentalMonotonic(); /** check transcendental tangent planes - * - * Returns a set of valid theory lemmas, based on - * computing an "incremental linearization" of - * transcendental functions based on the model values - * of transcendental functions and their arguments. - * It is based on Figure 3 of "Satisfiability - * Modulo Transcendental Functions via Incremental - * Linearization" by Cimatti et al., CADE 2017. - * This schema is not terminating in general. - * It is not enabled by default, and can - * be enabled by --nl-ext-tf-tplanes. - * - * Example: - * - * Assume we have a term sin(y) where M( y ) = 1 where M is the current model. - * Note that: - * sin(1) ~= .841471 - * - * The Taylor series and remainder of sin(y) of degree 7 is - * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5 - * R_{7,sin(0),b}( x ) = (-1/5040)*x^7 - * - * This gives us lower and upper bounds : - * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x ) - * ...where note P_u( 1 ) = 4243/5040 ~= .841865 - * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x ) - * ...where note P_l( 1 ) = 4241/5040 ~= .841468 - * - * Assume that M( sin(y) ) > P_u( 1 ). - * Since the concavity of sine in the region 0 < x < PI/2 is -1, - * we add a tangent plane refinement. - * The tangent plane at the point 1 in P_u is - * given by the formula: - * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 ) - * We add the lemma: - * ( 0 < y < PI/2 ) => sin( y ) <= T( y ) - * which is: - * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506) - * - * Assume that M( sin(y) ) < P_u( 1 ). - * Since the concavity of sine in the region 0 < x < PI/2 is -1, - * we add a secant plane refinement for some constants ( l, u ) - * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose - * l = 0 and u = M( PI/2 ) = 150517/47912. - * The secant planes at point 1 for P_l - * are given by the formulas: - * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l ) - * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u ) - * We add the lemmas: - * ( 0 < y < 1 ) => sin( y ) >= S_l( y ) - * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y ) - * which are: - * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y - * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2) - * where c1, c2 are rationals (for brevity, omitted here) - * such that c1 ~= .277 and c2 ~= 2.032. - */ - std::vector<Node> checkTranscendentalTangentPlanes(); + * + * Returns a set of valid theory lemmas, based on + * computing an "incremental linearization" of + * transcendental functions based on the model values + * of transcendental functions and their arguments. + * It is based on Figure 3 of "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017. + * This schema is not terminating in general. + * It is not enabled by default, and can + * be enabled by --nl-ext-tf-tplanes. + * + * Example: + * + * Assume we have a term sin(y) where M( y ) = 1 where M is the current model. + * Note that: + * sin(1) ~= .841471 + * + * The Taylor series and remainder of sin(y) of degree 7 is + * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5 + * R_{7,sin(0),b}( x ) = (-1/5040)*x^7 + * + * This gives us lower and upper bounds : + * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x ) + * ...where note P_u( 1 ) = 4243/5040 ~= .841865 + * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x ) + * ...where note P_l( 1 ) = 4241/5040 ~= .841468 + * + * Assume that M( sin(y) ) > P_u( 1 ). + * Since the concavity of sine in the region 0 < x < PI/2 is -1, + * we add a tangent plane refinement. + * The tangent plane at the point 1 in P_u is + * given by the formula: + * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 ) + * We add the lemma: + * ( 0 < y < PI/2 ) => sin( y ) <= T( y ) + * which is: + * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506) + * + * Assume that M( sin(y) ) < P_u( 1 ). + * Since the concavity of sine in the region 0 < x < PI/2 is -1, + * we add a secant plane refinement for some constants ( l, u ) + * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose + * l = 0 and u = M( PI/2 ) = 150517/47912. + * The secant planes at point 1 for P_l + * are given by the formulas: + * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l ) + * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u ) + * We add the lemmas: + * ( 0 < y < 1 ) => sin( y ) >= S_l( y ) + * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y ) + * which are: + * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y + * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2) + * where c1, c2 are rationals (for brevity, omitted here) + * such that c1 ~= .277 and c2 ~= 2.032. + * + * The argument lemSE is the "side effect" of the lemmas in the return + * value of this function (for details, see checkLastCall). + */ + std::vector<Node> checkTranscendentalTangentPlanes( + std::map<Node, NlLemmaSideEffect>& lemSE); /** check transcendental function refinement for tf * * This method is called by the above method for each refineable @@ -938,9 +959,13 @@ class NonlinearExtension { * * This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental * function application tf for Taylor degree d. It may add a secant or - * tangent plane lemma to lems. + * tangent plane lemma to lems and its side effect (if one exists) + * to lemSE. */ - bool checkTfTangentPlanesFun(Node tf, unsigned d, std::vector<Node>& lems); + bool checkTfTangentPlanesFun(Node tf, + unsigned d, + std::vector<Node>& lems, + std::map<Node, NlLemmaSideEffect>& lemSE); //-------------------------------------------- end lemma schemas }; /* class NonlinearExtension */ diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp index 6054ac603..821c2384c 100644 --- a/src/theory/atom_requests.cpp +++ b/src/theory/atom_requests.cpp @@ -65,15 +65,13 @@ void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toT d_triggerToRequestMap[triggerAtom] = index; } -bool AtomRequests::atom_iterator::done() const { - return index == null_index; -} +bool AtomRequests::atom_iterator::done() const { return d_index == null_index; } void AtomRequests::atom_iterator::next() { - index = requests.d_requests[index].previous; + d_index = d_requests.d_requests[d_index].d_previous; } const AtomRequests::Request& AtomRequests::atom_iterator::get() const { - return requests.d_requests[index].request; + return d_requests.d_requests[d_index].d_request; } diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index 6a3ffe5e9..b96b042af 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -34,24 +34,18 @@ public: /** Which atom and where to send it */ struct Request { /** Atom */ - Node atom; + Node d_atom; /** Where to send it */ - theory::TheoryId toTheory; + theory::TheoryId d_toTheory; - Request(TNode atom, theory::TheoryId toTheory) - : atom(atom), toTheory(toTheory) {} - Request() - : toTheory(theory::THEORY_LAST) - {} + Request(TNode a, theory::TheoryId tt) : d_atom(a), d_toTheory(tt) {} + Request() : d_toTheory(theory::THEORY_LAST) {} bool operator == (const Request& other) const { - return atom == other.atom && toTheory == other.toTheory; - } - - size_t hash() const { - return atom.getId(); + return d_atom == other.d_atom && d_toTheory == other.d_toTheory; } + size_t hash() const { return d_atom.getId(); } }; AtomRequests(context::Context* context); @@ -66,11 +60,14 @@ public: typedef size_t element_index; class atom_iterator { - const AtomRequests& requests; - element_index index; + const AtomRequests& d_requests; + element_index d_index; friend class AtomRequests; atom_iterator(const AtomRequests& requests, element_index start) - : requests(requests), index(start) {} + : d_requests(requests), d_index(start) + { + } + public: /** Is this iterator done */ bool done() const; @@ -97,13 +94,11 @@ private: struct Element { /** Current request */ - Request request; + Request d_request; /** Previous request */ - element_index previous; + element_index d_previous; - Element(const Request& request, element_index previous) - : request(request), previous(previous) - {} + Element(const Request& r, element_index p) : d_request(r), d_previous(p) {} }; /** We index the requests in this vector, it's a list */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 99507245d..94fc1e34c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -622,7 +622,7 @@ int TheoryBV::getReduction(int effort, Node n, Node& nr) } else if (n.getKind() == kind::INT_TO_BITVECTOR) { - nr = utils::eliminateBv2Nat(n); + nr = utils::eliminateInt2Bv(n); return -1; } return 0; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 153f785ca..a7638325c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1382,12 +1382,11 @@ bool RewriteRule<BitwiseSlicing>::applies(TNode node) { if (node[i].getKind() == kind::CONST_BITVECTOR) { BitVector constant = node[i].getConst<BitVector>(); // we do not apply the rule if the constant is all 0s or all 1s - if (constant == BitVector(utils::getSize(node), 0u)) - return false; - - for (unsigned i = 0; i < constant.getSize(); ++i) { - if (!constant.isBitSet(i)) - return true; + if (constant == BitVector(utils::getSize(node), 0u)) return false; + + for (unsigned j = 0, csize = constant.getSize(); j < csize; ++j) + { + if (!constant.isBitSet(j)) return true; } return false; } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index aa3efca19..fecefb8e1 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -211,8 +211,8 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod } }else{ //simplify term - std::map<Node, Node> visited; - getConstraints(n, constraints, visited); + std::map<Node, Node> visitedT; + getConstraints(n, constraints, visitedT); } if( !constraints.empty() && isBool && hasPol ){ //conjoin with current diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 1d1eb9751..11b9bd14b 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -339,7 +339,6 @@ bool Instantiate::addInstantiation( } if (options::trackInstLemmas()) { - bool recorded; if (options::incrementalSolving()) { recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index d1bd5db63..ad281b009 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -823,9 +823,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // "Let W be a subset of D such that S ^ W is unsat." // and uasserts is set to W. uasserts.clear(); - std::unordered_set<Node, NodeHashFunction> queryAsserts; - queryAsserts.insert(d_sc); - getUnsatCore(checkSc, queryAsserts, uasserts); + std::unordered_set<Node, NodeHashFunction> queryAsserts2; + queryAsserts2.insert(d_sc); + getUnsatCore(checkSc, queryAsserts2, uasserts); falseCore = true; } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index dc290d4ba..7c1451771 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -229,9 +229,9 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, // the lemmas must be guarded by the active guard of the enumerator Node g = d_tds->getActiveGuardForEnumerator(e); Assert(!g.isNull()); - for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + for (unsigned k = 0, size = enum_lems.size(); k < size; k++) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + enum_lems[k] = nm->mkNode(OR, g.negate(), enum_lems[k]); } lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index aa1e2627a..965c56ee4 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -25,6 +25,7 @@ operator STRING_STRREPL 3 "string replace" operator STRING_STRREPLALL 3 "string replace all" operator STRING_PREFIX 2 "string prefixof" operator STRING_SUFFIX 2 "string suffixof" +operator STRING_IS_DIGIT 1 "string isdigit, returns true if argument is a string of length one that represents a digit" operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" @@ -63,11 +64,13 @@ operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" operator REGEXP_UNION 2: "regexp union" operator REGEXP_INTER 2: "regexp intersection" +operator REGEXP_DIFF 2: "regexp difference" operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" operator REGEXP_RANGE 2 "regexp range" operator REGEXP_LOOP 2:3 "regexp loop" +operator REGEXP_COMPLEMENT 1 "regexp complement" operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" @@ -80,11 +83,13 @@ typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>" typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>" typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>" typerule REGEXP_INTER "SimpleTypeRuleVar<RRegExp, ARegExp>" +typerule REGEXP_DIFF "SimpleTypeRuleVar<RRegExp, ARegExp>" typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp, AInteger, AOptional<AInteger>>" +typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>" typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>" @@ -100,6 +105,7 @@ typerule STRING_STRREPL "SimpleTypeRule<RString, AString, AString, AString>" typerule STRING_STRREPLALL "SimpleTypeRule<RString, AString, AString, AString>" typerule STRING_PREFIX "SimpleTypeRule<RBool, AString, AString>" typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>" +typerule STRING_IS_DIGIT "SimpleTypeRule<RBool, AString>" typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>" typerule STRING_STOI "SimpleTypeRule<RInteger, AString>" typerule STRING_CODE "SimpleTypeRule<RInteger, AString>" diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 1b2de0eb5..048dc88b6 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -68,9 +68,9 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) visit.pop_back(); it = d_constCache.find(cur); + Kind ck = cur.getKind(); if (it == d_constCache.end()) { - Kind ck = cur.getKind(); if (ck == STRING_TO_REGEXP) { Node tmp = Rewriter::rewrite(cur[0]); @@ -104,7 +104,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) } else if (it->second == RE_C_UNKNOWN) { - RegExpConstType ret = RE_C_CONRETE_CONSTANT; + RegExpConstType ret = ck == REGEXP_COMPLEMENT ? RE_C_CONSTANT : RE_C_CONRETE_CONSTANT; for (const Node& cn : cur) { it = d_constCache.find(cn); @@ -126,7 +126,8 @@ bool RegExpOpr::isRegExpKind(Kind k) return k == REGEXP_EMPTY || k == REGEXP_SIGMA || k == STRING_TO_REGEXP || k == REGEXP_CONCAT || k == REGEXP_UNION || k == REGEXP_INTER || k == REGEXP_STAR || k == REGEXP_PLUS || k == REGEXP_OPT - || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV; + || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV + || k == REGEXP_COMPLEMENT; } // 0-unknown, 1-yes, 2-no @@ -264,6 +265,14 @@ int RegExpOpr::delta( Node r, Node &exp ) { } break; } + case kind::REGEXP_COMPLEMENT: + { + int tmp = delta(r[0], exp); + // flip the result if known + tmp = tmp == 0 ? 0 : (3 - tmp); + exp = exp.isNull() ? exp : exp.negate(); + break; + } default: { Assert(!isRegExpKind(k)); break; @@ -504,6 +513,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { } break; } + case kind::REGEXP_COMPLEMENT: + { + // don't know result + return 0; + break; + } default: { Assert(!isRegExpKind(r.getKind())); return 0; @@ -679,6 +694,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { //Trace("regexp-derive") << "RegExp-derive : REGEXP_LOOP returns /" << mkString(retNode) << "/" << std::endl; break; } + case kind::REGEXP_COMPLEMENT: default: { Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl; Unreachable(); @@ -786,12 +802,13 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) break; } case kind::REGEXP_SIGMA: + case kind::REGEXP_COMPLEMENT: default: { // we do not expect to call this function on regular expressions that // aren't a standard regular expression kind. However, if we do, then // the following code is conservative and says that the current // regular expression can begin with any character. - Assert(k == REGEXP_SIGMA); + Assert(isRegExpKind(k)); // can start with any character Assert(d_lastchar < std::numeric_limits<unsigned>::max()); for (unsigned i = 0; i <= d_lastchar; i++) @@ -1046,6 +1063,12 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes } break; } + case kind::REGEXP_COMPLEMENT: + { + // ~( s in complement(R) ) ---> s in R + conc = nm->mkNode(STRING_IN_REGEXP, s, r[0]); + break; + } default: { Assert(!isRegExpKind(k)); break; @@ -1240,6 +1263,12 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } break; } + case kind::REGEXP_COMPLEMENT: + { + // s in complement(R) ---> ~( s in R ) + conc = nm->mkNode(STRING_IN_REGEXP, s, r[0]).negate(); + break; + } default: { Assert(!isRegExpKind(k)); break; @@ -1305,10 +1334,14 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { if(n == d_emptyRegexp) { r1 = d_emptyRegexp; r2 = d_emptyRegexp; + return; } else if(n == d_emptySingleton) { r1 = d_emptySingleton; r2 = d_emptySingleton; - } else if(n.getKind() == kind::REGEXP_RV) { + } + Kind nk = n.getKind(); + if (nk == REGEXP_RV) + { Assert(n[0].getConst<Rational>() <= Rational(String::maxSize())) << "Exceeded UINT32_MAX in RegExpOpr::convert2"; unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); @@ -1318,7 +1351,9 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { } else { r2 = n; } - } else if(n.getKind() == kind::REGEXP_CONCAT) { + } + else if (nk == REGEXP_CONCAT) + { bool flag = true; std::vector<Node> vr1, vr2; for( unsigned i=0; i<n.getNumChildren(); i++ ) { @@ -1344,7 +1379,9 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { r1 = d_emptySingleton; r2 = n; } - } else if(n.getKind() == kind::REGEXP_UNION) { + } + else if (nk == REGEXP_UNION) + { std::vector<Node> vr1, vr2; for( unsigned i=0; i<n.getNumChildren(); i++ ) { Node t1, t2; @@ -1354,15 +1391,16 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { } r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr1); r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr2); - } else if(n.getKind() == kind::STRING_TO_REGEXP || n.getKind() == kind::REGEXP_SIGMA || n.getKind() == kind::REGEXP_RANGE) { - r1 = d_emptySingleton; - r2 = n; - } else if(n.getKind() == kind::REGEXP_LOOP) { - //TODO:LOOP + } + else if (nk == STRING_TO_REGEXP || nk == REGEXP_SIGMA || nk == REGEXP_RANGE + || nk == REGEXP_COMPLEMENT || nk == REGEXP_LOOP) + { + // this leaves n unchanged r1 = d_emptySingleton; r2 = n; - //Unreachable(); - } else { + } + else + { //is it possible? Unreachable(); } @@ -1541,6 +1579,7 @@ Node RegExpOpr::removeIntersection(Node r) { case REGEXP_CONCAT: case REGEXP_UNION: case REGEXP_STAR: + case REGEXP_COMPLEMENT: { NodeBuilder<> nb(rk); for (const Node& rc : r) @@ -1696,6 +1735,13 @@ std::string RegExpOpr::mkString( Node r ) { retStr += ">"; break; } + case REGEXP_COMPLEMENT: + { + retStr += "^("; + retStr += mkString(r[0]); + retStr += ")"; + break; + } default: { std::stringstream ss; diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 91d5df744..b9dbedba5 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -41,10 +41,13 @@ namespace strings { */ enum RegExpConstType { - // the regular expression doesn't contain variables or re.allchar or re.range + // the regular expression doesn't contain variables or re.comp, + // re.allchar or re.range (call these three operators "non-concrete + // operators"). Notice that re.comp is a non-concrete operator + // since it can be seen as indirectly defined in terms of re.allchar. RE_C_CONRETE_CONSTANT, // the regular expression doesn't contain variables, but may contain - // re.allchar or re.range + // re.comp, re.allchar or re.range RE_C_CONSTANT, // the regular expression may contain variables RE_C_VARIABLE, @@ -122,6 +125,20 @@ class RegExpOpr { /** is k a native operator whose return type is a regular expression? */ static bool isRegExpKind(Kind k); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); + /** + * This method returns 1 if the empty string is in r, 2 if the empty string + * is not in r, or 0 if it is unknown whether the empty string is in r. + * TODO (project #2): refactor the return value of this function. + * + * If this method returns 0, then exp is updated to an explanation that + * would imply that the empty string is in r. + * + * For example, + * - delta( (re.inter (str.to.re x) (re.* "A")) ) returns 0 and sets exp to + * x = "", + * - delta( (re.++ (str.to.re "A") R) ) returns 2, + * - delta( (re.union (re.* "A") R) ) returns 1. + */ int delta( Node r, Node &exp ); int derivativeS( Node r, CVC4::String c, Node &retNode ); Node derivativeSingle( Node r, CVC4::String c ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 339d11dd2..d8bc7f34f 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -25,6 +25,7 @@ #include "theory/arith/arith_msum.h" #include "theory/strings/regexp_operation.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" #include "theory/theory.h" #include "util/integer.h" #include "util/rational.h" @@ -357,20 +358,23 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node) if (!c[0].empty() && !c[1].empty() && c[0].back().isConst() && c[1].back().isConst()) { - String cs[2]; + Node cs[2]; + size_t csl[2]; for (unsigned j = 0; j < 2; j++) { - cs[j] = c[j].back().getConst<String>(); + cs[j] = c[j].back(); + csl[j] = Word::getLength(cs[j]); } - unsigned larger = cs[0].size() > cs[1].size() ? 0 : 1; - unsigned smallerSize = cs[1 - larger].size(); + size_t larger = csl[0] > csl[1] ? 0 : 1; + size_t smallerSize = csl[1 - larger]; if (cs[1 - larger] - == (i == 0 ? cs[larger].suffix(smallerSize) - : cs[larger].prefix(smallerSize))) + == (i == 0 ? Word::suffix(cs[larger], smallerSize) + : Word::prefix(cs[larger], smallerSize))) { - unsigned sizeDiff = cs[larger].size() - smallerSize; - c[larger][c[larger].size() - 1] = nm->mkConst( - i == 0 ? cs[larger].prefix(sizeDiff) : cs[larger].suffix(sizeDiff)); + size_t sizeDiff = csl[larger] - smallerSize; + c[larger][c[larger].size() - 1] = + i == 0 ? Word::prefix(cs[larger], sizeDiff) + : Word::suffix(cs[larger], sizeDiff); c[1 - larger].pop_back(); changed = true; } @@ -393,10 +397,10 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node) for (unsigned i = 0; i < 2; i++) { Node cn = checkEntailHomogeneousString(node[i]); - if (!cn.isNull() && cn.getConst<String>().size() > 0) + if (!cn.isNull() && !Word::isEmpty(cn)) { Assert(cn.isConst()); - Assert(cn.getConst<String>().size() == 1); + Assert(Word::getLength(cn) == 1); unsigned hchar = cn.getConst<String>().front(); // The operands of the concat on each side of the equality without @@ -758,7 +762,8 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) } if(!tmpNode.isConst()) { if(!preNode.isNull()) { - if(preNode.getKind() == kind::CONST_STRING && !preNode.getConst<String>().isEmptyString() ) { + if (preNode.isConst() && !Word::isEmpty(preNode)) + { node_vec.push_back( preNode ); } preNode = Node::null(); @@ -768,11 +773,15 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) if( preNode.isNull() ){ preNode = tmpNode; }else{ - preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode.getConst<String>() ) ); + std::vector<Node> vec; + vec.push_back(preNode); + vec.push_back(tmpNode); + preNode = Word::mkWord(vec); } } } - if( !preNode.isNull() && ( preNode.getKind()!=kind::CONST_STRING || !preNode.getConst<String>().isEmptyString() ) ){ + if (!preNode.isNull() && (!preNode.isConst() || !Word::isEmpty(preNode))) + { node_vec.push_back( preNode ); } @@ -828,7 +837,7 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) } } else if (c.getKind() == STRING_TO_REGEXP && c[0].isConst() - && c[0].getConst<String>().isEmptyString()) + && Word::isEmpty(c[0])) { changed = true; emptyRe = c; @@ -969,9 +978,8 @@ Node TheoryStringsRewriter::rewriteStarRegExp(TNode node) // ((R)*)* ---> R* return returnRewrite(node, node[0], "re-star-nested-star"); } - else if (node[0].getKind() == STRING_TO_REGEXP - && node[0][0].getKind() == CONST_STRING - && node[0][0].getConst<String>().isEmptyString()) + else if (node[0].getKind() == STRING_TO_REGEXP && node[0][0].isConst() + && Word::isEmpty(node[0][0])) { // ("")* ---> "" return returnRewrite(node, node[0], "re-star-empty-string"); @@ -991,8 +999,8 @@ Node TheoryStringsRewriter::rewriteStarRegExp(TNode node) std::vector<Node> node_vec; for (const Node& nc : node[0]) { - if (nc.getKind() == STRING_TO_REGEXP && nc[0].getKind() == CONST_STRING - && nc[0].getConst<String>().isEmptyString()) + if (nc.getKind() == STRING_TO_REGEXP && nc[0].isConst() + && Word::isEmpty(nc[0])) { // can be removed changed = true; @@ -1329,6 +1337,11 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } } } + case REGEXP_COMPLEMENT: + { + return !testConstStringInRegExp(s, index_start, r[0]); + break; + } default: { Assert(!RegExpOpr::isRegExpKind(k)); return false; @@ -1469,7 +1482,13 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { retNode = nm->mkNode(AND, nm->mkNode(LEQ, nm->mkNode(STRING_CODE, r[0]), xcode), nm->mkNode(LEQ, xcode, nm->mkNode(STRING_CODE, r[1]))); - }else if(x != node[0] || r != node[1]) { + } + else if (r.getKind() == REGEXP_COMPLEMENT) + { + retNode = nm->mkNode(STRING_IN_REGEXP, x, r[0]).negate(); + } + else if (x != node[0] || r != node[1]) + { retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r ); } @@ -1560,18 +1579,19 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { Kind nk0 = node[0].getKind(); if( node[0].isConst() ){ - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) ); + retNode = nm->mkConst(Rational(Word::getLength(node[0]))); } else if (nk0 == kind::STRING_CONCAT) { Node tmpNode = node[0]; if(tmpNode.isConst()) { - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) ); + retNode = nm->mkConst(Rational(Word::getLength(tmpNode))); }else if( tmpNode.getKind()==kind::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() ) ) ); + node_vec.push_back( + nm->mkConst(Rational(Word::getLength(tmpNode[i])))); } else { node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) ); } @@ -1644,6 +1664,14 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewritePrefixSuffix(node); } + else if (nk == STRING_IS_DIGIT) + { + // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57 + Node t = nm->mkNode(STRING_CODE, node[0]); + retNode = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConst(Rational(48)), t), + nm->mkNode(LEQ, t, nm->mkConst(Rational(57)))); + } else if (nk == kind::STRING_ITOS) { if(node[0].isConst()) { @@ -1693,6 +1721,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteAndOrRegExp(node); } + else if (nk == REGEXP_DIFF) + { + retNode = nm->mkNode(REGEXP_INTER, node[0],nm->mkNode(REGEXP_COMPLEMENT, node[1])); + } else if (nk == REGEXP_STAR) { retNode = rewriteStarRegExp(node); @@ -1747,7 +1779,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) NodeManager* nm = NodeManager::currentNM(); if (node[0].isConst()) { - if (node[0].getConst<String>().size() == 0) + if (Word::isEmpty(node[0])) { Node ret = node[0]; return returnRewrite(node, ret, "ss-emptystr"); @@ -1762,13 +1794,13 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) { // start beyond the maximum size of strings // thus, it must be beyond the end point of this string - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-const-start-max-oob"); } else if (node[1].getConst<Rational>().sgn() < 0) { // start before the beginning of the string - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-const-start-neg"); } else @@ -1777,7 +1809,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) if (start >= s.size()) { // start beyond the end of the string - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-const-start-oob"); } } @@ -1789,7 +1821,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } else if (node[2].getConst<Rational>().sgn() <= 0) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-const-len-non-pos"); } else @@ -1816,12 +1848,12 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) // if entailed non-positive length or negative start point if (checkEntailArith(zero, node[1], true)) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-start-neg"); } else if (checkEntailArith(zero, node[2])) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-len-non-pos"); } @@ -1847,7 +1879,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) // be empty. if (checkEntailArith(node[1], node[0][2])) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-start-geq-len"); } } @@ -1931,7 +1963,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) Rewriter::rewrite(nm->mkNode(kind::LT, node[1], tot_len)); if (checkEntailArithWithAssumption(n1_lt_tot_len, zero, node[2], false)) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-start-entails-zero-len"); } @@ -1940,7 +1972,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) Rewriter::rewrite(nm->mkNode(kind::LT, zero, node[2])); if (checkEntailArithWithAssumption(non_zero_len, node[1], tot_len, false)) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-non-zero-len-entails-oob"); } @@ -1949,14 +1981,14 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) Rewriter::rewrite(nm->mkNode(kind::GEQ, node[1], zero)); if (checkEntailArithWithAssumption(geq_zero_start, zero, tot_len, false)) { - Node ret = nm->mkConst(String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-geq-zero-start-entails-emp-s"); } // (str.substr s x x) ---> "" if (str.len s) <= 1 if (node[1] == node[2] && checkEntailLengthOne(node[0])) { - Node ret = nm->mkConst(::CVC4::String("")); + Node ret = Word::mkEmptyWord(node.getType()); return returnRewrite(node, ret, "ss-len-one-z-z"); } } @@ -2042,13 +2074,11 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { CVC4::String s = node[0].getConst<String>(); if (node[1].isConst()) { - CVC4::String t = node[1].getConst<String>(); - Node ret = - NodeManager::currentNM()->mkConst(s.find(t) != std::string::npos); + Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos); return returnRewrite(node, ret, "ctn-const"); }else{ Node t = node[1]; - if (s.size() == 0) + if (Word::isEmpty(node[0])) { Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]); @@ -2092,14 +2122,14 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } if (node[1].isConst()) { - CVC4::String t = node[1].getConst<String>(); - if (t.size() == 0) + size_t len = Word::getLength(node[1]); + if (len == 0) { // contains( x, "" ) ---> true Node ret = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, ret, "ctn-rhs-emptystr"); } - else if (t.size() == 1) + else if (len == 1) { // The following rewrites are specific to a single character second // argument of contains, where we can reason that this character is diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 655df7da3..a0ee0d224 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -22,6 +22,16 @@ namespace CVC4 { namespace theory { namespace strings { +Node Word::mkEmptyWord(TypeNode tn) +{ + if (tn.isString()) + { + return mkEmptyWord(CONST_STRING); + } + Unimplemented(); + return Node::null(); +} + Node Word::mkEmptyWord(Kind k) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index e4d10247a..74f50ee9a 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -20,6 +20,7 @@ #include <vector> #include "expr/node.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { @@ -28,7 +29,10 @@ namespace strings { // ------------------------------ for words (string or sequence constants) class Word { -public: + public: + /** make empty constant of type tn */ + static Node mkEmptyWord(TypeNode tn); + /** make empty constant of kind k */ static Node mkEmptyWord(Kind k); @@ -45,9 +49,9 @@ public: static std::size_t find(TNode x, TNode y, std::size_t start = 0); /** - * Return the first position y occurs in x searching from the end of x, or - * std::string::npos otherwise - */ + * Return the first position y occurs in x searching from the end of x, or + * std::string::npos otherwise + */ static std::size_t rfind(TNode x, TNode y, std::size_t start = 0); /** Returns true if y is a prefix of x */ @@ -62,8 +66,9 @@ public: /** Return the substring/subsequence of x starting at index i */ static Node substr(TNode x, std::size_t i); - /** Return the substring/subsequence of x starting at index i with size at most - * j */ + /** Return the substring/subsequence of x starting at index i with size at + * most + * j */ static Node substr(TNode x, std::size_t i, std::size_t j); /** Return the prefix of x of size at most i */ @@ -73,42 +78,43 @@ public: static Node suffix(TNode x, std::size_t i); /** - * Checks if there is any overlap between word x and another word y. This - * corresponds to checking whether one string contains the other and whether a - * substring/subsequence of one is a prefix of the other and vice-versa. - * - * @param x The first string - * @param y The second string - * @return True if there is an overlap, false otherwise - */ + * Checks if there is any overlap between word x and another word y. This + * corresponds to checking whether one string contains the other and whether a + * substring/subsequence of one is a prefix of the other and vice-versa. + * + * @param x The first string + * @param y The second string + * @return True if there is an overlap, false otherwise + */ static bool noOverlapWith(TNode x, TNode y); /** overlap - * - * if overlap returns m>0, - * then the maximal suffix of this string that is a prefix of y is of length m. - * - * For example, if x is "abcdef", then: - * x.overlap("defg") = 3 - * x.overlap("ab") = 0 - * x.overlap("d") = 0 - * x.overlap("bcdefdef") = 5 - */ + * + * if overlap returns m>0, + * then the maximal suffix of this string that is a prefix of y is of length + * m. + * + * For example, if x is "abcdef", then: + * x.overlap("defg") = 3 + * x.overlap("ab") = 0 + * x.overlap("d") = 0 + * x.overlap("bcdefdef") = 5 + */ static std::size_t overlap(TNode x, TNode y); /** reverse overlap - * - * if roverlap returns m>0, - * then the maximal prefix of this word that is a suffix of y is of length m. - * - * For example, if x is "abcdef", then: - * x.roverlap("aaabc") = 3 - * x.roverlap("def") = 0 - * x.roverlap("d") = 0 - * x.roverlap("defabcde") = 5 - * - * Notice that x.overlap(y) = y.roverlap(x) - */ + * + * if roverlap returns m>0, + * then the maximal prefix of this word that is a suffix of y is of length m. + * + * For example, if x is "abcdef", then: + * x.roverlap("aaabc") = 3 + * x.roverlap("def") = 0 + * x.roverlap("d") = 0 + * x.roverlap("defabcde") = 5 + * + * Notice that x.overlap(y) = y.roverlap(x) + */ static std::size_t roverlap(TNode x, TNode y); }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a3c74e7e2..d176b015d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -740,7 +740,7 @@ void TheoryEngine::combineTheories() { // The equality in question (order for no repetition) Node equality = carePair.d_a.eqNode(carePair.d_b); - // EqualityStatus es = getEqualityStatus(carePair.a, carePair.b); + // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b); // Debug("combineTheories") << "TheoryEngine::combineTheories(): " << // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" : // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" : @@ -1453,9 +1453,11 @@ void TheoryEngine::assertFact(TNode literal) AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom); while (!it.done()) { const AtomRequests::Request& request = it.get(); - Node toAssert = polarity ? (Node) request.atom : request.atom.notNode(); + Node toAssert = + polarity ? (Node)request.d_atom : request.d_atom.notNode(); Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl; - assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER); + assertToTheory( + toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER); it.next(); } @@ -1634,8 +1636,8 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; for (unsigned i = 0; i < explanation.size(); ++ i) { - Assert(explanation[i].theory == THEORY_SAT_SOLVER); - all.insert(explanation[i].node); + Assert(explanation[i].d_theory == THEORY_SAT_SOLVER); + all.insert(explanation[i].d_node); } if (all.size() == 0) { @@ -1645,7 +1647,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { if (all.size() == 1) { // All the same, or just one - return explanation[0].node; + return explanation[0].d_node; } NodeBuilder<> conjunction(kind::AND); @@ -1723,10 +1725,11 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain]; - Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node " - << nodeExplainerPair.node - << " is theory: " << nodeExplainerPair.theory << std::endl; - TheoryId explainer = nodeExplainerPair.theory; + Debug("theory::explain") + << "TheoryEngine::getExplanation: explainer for node " + << nodeExplainerPair.d_node + << " is theory: " << nodeExplainerPair.d_theory << std::endl; + TheoryId explainer = nodeExplainerPair.d_theory; // Create the workplace for explanations std::vector<NodeTheoryPair> explanationVector; @@ -2074,31 +2077,42 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; - Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; - + Debug("theory::explain") + << "[i=" << i << "] TheoryEngine::explain(): processing [" + << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from " + << toExplain.d_theory << endl; // If a true constant or a negation of a false constant we can ignore it - if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) { + if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>()) + { ++ i; continue; } - if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) { + if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() + && !toExplain.d_node[0].getConst<bool>()) + { ++ i; continue; } // If from the SAT solver, keep it - if (toExplain.theory == THEORY_SAT_SOLVER) { + if (toExplain.d_theory == THEORY_SAT_SOLVER) + { Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; continue; } // If an and, expand it - if (toExplain.node.getKind() == kind::AND) { - Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << endl; - for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) { - NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp); + if (toExplain.d_node.getKind() == kind::AND) + { + Debug("theory::explain") + << "TheoryEngine::explain(): expanding " << toExplain.d_node + << " got from " << toExplain.d_theory << endl; + for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k) + { + NodeTheoryPair newExplain( + toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); } ++ i; @@ -2110,24 +2124,31 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector if (find != d_propagationMap.end()) { Debug("theory::explain") << "\tTerm was propagated by another theory (theory = " - << getTheoryString((*find).second.theory) << ")" << std::endl; + << getTheoryString((*find).second.d_theory) << ")" << std::endl; // There is some propagation, check if its a timely one - if ((*find).second.timestamp < toExplain.timestamp) { - Debug("theory::explain") << "\tRelevant timetsamp, pushing " - << (*find).second.node << "to index = " << explanationVector.size() << std::endl; + if ((*find).second.d_timestamp < toExplain.d_timestamp) + { + Debug("theory::explain") + << "\tRelevant timetsamp, pushing " << (*find).second.d_node + << "to index = " << explanationVector.size() << std::endl; explanationVector.push_back((*find).second); ++i; PROOF({ - if (toExplain.node != (*find).second.node) { - Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node - << ", toExplain = " << (*find).second.node << std::endl; + if (toExplain.d_node != (*find).second.d_node) + { + Debug("pf::explain") + << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " + << toExplain.d_node << ", toExplain = " << (*find).second.d_node + << std::endl; - if (proofRecipe) { - proofRecipe->addRewriteRule(toExplain.node, (*find).second.node); - } + if (proofRecipe) + { + proofRecipe->addRewriteRule(toExplain.d_node, + (*find).second.d_node); } - }) + } + }) continue; } @@ -2135,21 +2156,27 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // It was produced by the theory, so ask for an explanation Node explanation; - if (toExplain.theory == THEORY_BUILTIN) { - explanation = d_sharedTerms.explain(toExplain.node); + if (toExplain.d_theory == THEORY_BUILTIN) + { + explanation = d_sharedTerms.explain(toExplain.d_node); Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; - } else { - explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + } + else + { + explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); Debug("theory::explain") << "\tTerm was propagated by owner theory: " - << theoryOf(toExplain.theory)->getId() + << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << explanation << std::endl; } - Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; - Assert(explanation != toExplain.node) + Debug("theory::explain") + << "TheoryEngine::explain(): got explanation " << explanation + << " got from " << toExplain.d_theory << endl; + Assert(explanation != toExplain.d_node) << "wasn't sent to you, so why are you explaining it trivially"; // Mark the explanation - NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); + NodeTheoryPair newExplain( + explanation, toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); ++ i; @@ -2160,10 +2187,10 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // If we're expanding the target node of the explanation (this is the // first expansion...), we don't want to add it as a separate proof // step. It is already part of the assertions. - if (!ContainsKey(*inputAssertions, toExplain.node)) + if (!ContainsKey(*inputAssertions, toExplain.d_node)) { - LemmaProofRecipe::ProofStep proofStep(toExplain.theory, - toExplain.node); + LemmaProofRecipe::ProofStep proofStep(toExplain.d_theory, + toExplain.d_node); if (explanation.getKind() == kind::AND) { Node flat = flattenAnd(explanation); @@ -2202,7 +2229,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector if (proofRecipe) { // The remaining literals are the base of the proof for (unsigned k = 0; k < explanationVector.size(); ++k) { - proofRecipe->addBaseAssertion(explanationVector[k].node.negate()); + proofRecipe->addBaseAssertion(explanationVector[k].d_node.negate()); } } }); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a5631059f..1757d7a6d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -60,15 +60,17 @@ class LemmaProofRecipe; * propagations between theories. */ struct NodeTheoryPair { - Node node; - theory::TheoryId theory; - size_t timestamp; - NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0) - : node(node), theory(theory), timestamp(timestamp) {} - NodeTheoryPair() : theory(theory::THEORY_LAST), timestamp() {} + Node d_node; + theory::TheoryId d_theory; + size_t d_timestamp; + NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0) + : d_node(n), d_theory(t), d_timestamp(ts) + { + } + NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {} // Comparison doesn't take into account the timestamp bool operator == (const NodeTheoryPair& pair) const { - return node == pair.node && theory == pair.theory; + return d_node == pair.d_node && d_theory == pair.d_theory; } };/* struct NodeTheoryPair */ @@ -76,8 +78,8 @@ struct NodeTheoryPairHashFunction { NodeHashFunction hashFunction; // Hash doesn't take into account the timestamp size_t operator()(const NodeTheoryPair& pair) const { - uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.node)); - return static_cast<size_t>(fnv1a::fnv1a_64(pair.theory, hash)); + uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node)); + return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash)); } };/* struct NodeTheoryPairHashFunction */ diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index edfaadbb6..e7dc782bb 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -48,10 +48,7 @@ struct RewriteResponse { const RewriteStatus d_status; const Node d_node; - RewriteResponse(RewriteStatus status, Node node) - : d_status(status), d_node(node) - { - } + RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {} }; /* struct RewriteResponse */ /** diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8e0c96ae3..63aa81097 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -24,22 +24,22 @@ namespace theory { namespace eq { EqualityEngine::Statistics::Statistics(std::string name) - : mergesCount(name + "::mergesCount", 0), - termsCount(name + "::termsCount", 0), - functionTermsCount(name + "::functionTermsCount", 0), - constantTermsCount(name + "::constantTermsCount", 0) + : d_mergesCount(name + "::mergesCount", 0), + d_termsCount(name + "::termsCount", 0), + d_functionTermsCount(name + "::functionTermsCount", 0), + d_constantTermsCount(name + "::constantTermsCount", 0) { - smtStatisticsRegistry()->registerStat(&mergesCount); - smtStatisticsRegistry()->registerStat(&termsCount); - smtStatisticsRegistry()->registerStat(&functionTermsCount); - smtStatisticsRegistry()->registerStat(&constantTermsCount); + smtStatisticsRegistry()->registerStat(&d_mergesCount); + smtStatisticsRegistry()->registerStat(&d_termsCount); + smtStatisticsRegistry()->registerStat(&d_functionTermsCount); + smtStatisticsRegistry()->registerStat(&d_constantTermsCount); } EqualityEngine::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&mergesCount); - smtStatisticsRegistry()->unregisterStat(&termsCount); - smtStatisticsRegistry()->unregisterStat(&functionTermsCount); - smtStatisticsRegistry()->unregisterStat(&constantTermsCount); + smtStatisticsRegistry()->unregisterStat(&d_mergesCount); + smtStatisticsRegistry()->unregisterStat(&d_termsCount); + smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount); + smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount); } /** @@ -47,28 +47,31 @@ EqualityEngine::Statistics::~Statistics() { */ struct BfsData { // The current node - EqualityNodeId nodeId; + EqualityNodeId d_nodeId; // The index of the edge we traversed - EqualityEdgeId edgeId; + EqualityEdgeId d_edgeId; // Index in the queue of the previous node. Shouldn't be too much of them, at most the size // of the biggest equivalence class - size_t previousIndex; + size_t d_previousIndex; - BfsData(EqualityNodeId nodeId = null_id, EqualityEdgeId edgeId = null_edge, size_t prev = 0) - : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {} + BfsData(EqualityNodeId nodeId = null_id, + EqualityEdgeId edgeId = null_edge, + size_t prev = 0) + : d_nodeId(nodeId), d_edgeId(edgeId), d_previousIndex(prev) + { + } }; class ScopedBool { - bool& watch; - bool oldValue; -public: - ScopedBool(bool& watch, bool newValue) - : watch(watch), oldValue(watch) { - watch = newValue; - } - ~ScopedBool() { - watch = oldValue; + bool& d_watch; + bool d_oldValue; + + public: + ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch) + { + d_watch = newValue; } + ~ScopedBool() { d_watch = d_oldValue; } }; EqualityEngineNotifyNone EqualityEngine::s_notifyNone; @@ -158,7 +161,10 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { } void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { - Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl; + Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.d_t1Id] + << ", " << d_nodes[candidate.d_t2Id] << ", " + << candidate.d_type << "). reason: " << candidate.d_reason + << std::endl; if (back) { d_propagationQueue.push_back(candidate); } else { @@ -169,7 +175,7 @@ void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) { Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; - ++ d_stats.functionTermsCount; + ++d_stats.d_functionTermsCount; // Get another id for this EqualityNodeId funId = newNode(original); @@ -211,7 +217,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { Debug("equality") << d_name << "::eq::newNode(" << node << ")" << std::endl; - ++ d_stats.termsCount; + ++d_stats.d_termsCount; // Register the new id of the term EqualityNodeId newId = d_nodes.size(); @@ -477,8 +483,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef); // Go through and notify the shared dis-equalities - Theory::Set aTags = aTriggerTerms.tags; - Theory::Set bTags = bTriggerTerms.tags; + Theory::Set aTags = aTriggerTerms.d_tags; + Theory::Set bTags = bTriggerTerms.d_tags; TheoryId aTag = Theory::setPop(aTags); TheoryId bTag = Theory::setPop(bTags); int a_i = 0, b_i = 0; @@ -491,8 +497,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig ++ b_i; } else { // Same tags, notify - EqualityNodeId aSharedId = aTriggerTerms.triggers[a_i++]; - EqualityNodeId bSharedId = bTriggerTerms.triggers[b_i++]; + EqualityNodeId aSharedId = aTriggerTerms.d_triggers[a_i++]; + EqualityNodeId bSharedId = bTriggerTerms.d_triggers[b_i++]; // Propagate if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) { // Store a proof if not there already @@ -533,7 +539,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Assert(triggersFired.empty()); - ++ d_stats.mergesCount; + ++d_stats.d_mergesCount; EqualityNodeId class1Id = class1.getFind(); EqualityNodeId class2Id = class2.getFind(); @@ -562,10 +568,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Trigger set of class 1 TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; - Theory::Set class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).tags; + Theory::Set class1Tags = class1triggerRef == null_set_id + ? 0 + : getTriggerTermSet(class1triggerRef).d_tags; // Trigger set of class 2 TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; - Theory::Set class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).tags; + Theory::Set class2Tags = class2triggerRef == null_set_id + ? 0 + : getTriggerTermSet(class2triggerRef).d_tags; // Disequalities coming from class2 TaggedEqualitiesSet class2disequalitiesToNotify; @@ -600,17 +610,19 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1]; // If the two are not already in the same class - if (otherTrigger.classId != trigger.classId) { - trigger.classId = class1Id; + if (otherTrigger.d_classId != trigger.d_classId) + { + trigger.d_classId = class1Id; // If they became the same, call the trigger - if (otherTrigger.classId == class1Id) { + if (otherTrigger.d_classId == class1Id) + { // Id of the real trigger is half the internal one triggersFired.push_back(currentTrigger); } } // Go to the next trigger - currentTrigger = trigger.nextTrigger; + currentTrigger = trigger.d_nextTrigger; } // Move to the next node @@ -635,17 +647,19 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Get the function application EqualityNodeId funId = useNode.getApplicationId(); Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; - const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; + const FunctionApplication& fun = + d_applications[useNode.getApplicationId()].d_normalized; // If it's interpreted and we can interpret - if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { - // Get the actual term id - TNode term = d_nodes[funId]; - subtermEvaluates(getNodeId(term)); - } - // Check if there is an application with find arguments - EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); - EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); - FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); + if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) + { + // Get the actual term id + TNode term = d_nodes[funId]; + subtermEvaluates(getNodeId(term)); + } + // Check if there is an application with find arguments + EqualityNodeId aNormalized = getEqualityNode(fun.d_a).getFind(); + EqualityNodeId bNormalized = getEqualityNode(fun.d_b).getFind(); + FunctionApplication funNormalized(fun.d_type, aNormalized, bNormalized); ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find != d_applicationLookup.end()) { // Applications fun and the funNormalized can be merged due to congruence @@ -696,14 +710,15 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef); // Initialize the merged set - Theory::Set newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags); + Theory::Set newSetTags = + Theory::setUnion(class1triggers.d_tags, class2triggers.d_tags); EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = 0; int i1 = 0; int i2 = 0; - Theory::Set tags1 = class1triggers.tags; - Theory::Set tags2 = class2triggers.tags; + Theory::Set tags1 = class1triggers.d_tags; + Theory::Set tags2 = class2triggers.d_tags; TheoryId tag1 = Theory::setPop(tags1); TheoryId tag2 = Theory::setPop(tags2); @@ -713,18 +728,21 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect { if (tag1 < tag2) { // copy tag1 - newSetTriggers[newSetTriggersSize++] = class1triggers.triggers[i1++]; + newSetTriggers[newSetTriggersSize++] = + class1triggers.d_triggers[i1++]; tag1 = Theory::setPop(tags1); } else if (tag1 > tag2) { // copy tag2 - newSetTriggers[newSetTriggersSize++] = class2triggers.triggers[i2++]; + newSetTriggers[newSetTriggersSize++] = + class2triggers.d_triggers[i2++]; tag2 = Theory::setPop(tags2); } else { // copy tag1 - EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = class1triggers.triggers[i1++]; + EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = + class1triggers.d_triggers[i1++]; // since they are both tagged notify of merge if (d_performNotify) { - EqualityNodeId tag2id = class2triggers.triggers[i2++]; + EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { return false; } @@ -736,7 +754,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } // Add the new trigger set, if different from previous one - if (class1triggers.tags != class2triggers.tags) { + if (class1triggers.d_tags != class2triggers.d_tags) + { // Add it to the list for backtracking d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; @@ -771,8 +790,8 @@ void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, Equal TriggerId currentTrigger = d_nodeTriggers[currentId]; while (currentTrigger != null_trigger) { Trigger& trigger = d_equalityTriggers[currentTrigger]; - trigger.classId = class2Id; - currentTrigger = trigger.nextTrigger; + trigger.d_classId = class2Id; + currentTrigger = trigger.d_nextTrigger; } // Move to the next node @@ -800,8 +819,10 @@ void EqualityEngine::backtrack() { // Get the ids of the merged classes Equality& eq = d_assertedEqualities[i]; // Undo the merge - if (eq.lhs != null_id) { - undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); + if (eq.d_lhs != null_id) + { + undoMerge( + d_equalityNodes[eq.d_lhs], d_equalityNodes[eq.d_rhs], eq.d_rhs); } } @@ -823,7 +844,7 @@ void EqualityEngine::backtrack() { // Unset the individual triggers for (int i = d_triggerTermSetUpdates.size() - 1, i_end = d_triggerTermSetUpdatesSize; i >= i_end; -- i) { const TriggerSetUpdate& update = d_triggerTermSetUpdates[i]; - d_nodeIndividualTrigger[update.classId] = update.oldValue; + d_nodeIndividualTrigger[update.d_classId] = update.d_oldValue; } d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize); } @@ -832,7 +853,7 @@ void EqualityEngine::backtrack() { // Unlink the triggers from the lists for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) { const Trigger& trigger = d_equalityTriggers[i]; - d_nodeTriggers[trigger.classId] = trigger.nextTrigger; + d_nodeTriggers[trigger.d_classId] = trigger.d_nextTrigger; } // Get rid of the triggers d_equalityTriggers.resize(d_equalityTriggersCount); @@ -860,12 +881,12 @@ void EqualityEngine::backtrack() { Debug("equality") << d_name << "::eq::backtrack(): removing node " << d_nodes[i] << std::endl; d_nodeIds.erase(d_nodes[i]); - const FunctionApplication& app = d_applications[i].original; + const FunctionApplication& app = d_applications[i].d_original; if (!app.isNull()) { // Remove b from use-list - getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.d_b).removeTopFromUseList(d_useListNodes); // Remove a from use-list - getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.d_a).removeTopFromUseList(d_useListNodes); } } @@ -959,8 +980,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, << "Don't ask for stuff I didn't notify you about"; DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; - for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { - + for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i) + { EqualityPair toExplain = d_deducedDisequalityReasons[i]; std::shared_ptr<EqProof> eqpc; @@ -1143,7 +1164,7 @@ void EqualityEngine::getExplanation( // The next node to visit BfsData current = bfsQueue[currentIndex]; - EqualityNodeId currentNode = current.nodeId; + EqualityNodeId currentNode = current.d_nodeId; Debug("equality") << d_name << "::eq::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; @@ -1159,8 +1180,8 @@ void EqualityEngine::getExplanation( const EqualityEdge& edge = d_equalityEdges[currentEdge]; // If not just the backwards edge - if ((currentEdge | 1u) != (current.edgeId | 1u)) { - + if ((currentEdge | 1u) != (current.d_edgeId | 1u)) + { Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; // Did we find the path @@ -1173,7 +1194,7 @@ void EqualityEngine::getExplanation( // Reconstruct the path do { // The current node - currentNode = bfsQueue[currentIndex].nodeId; + currentNode = bfsQueue[currentIndex].d_nodeId; EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); unsigned reasonType = d_equalityEdges[currentEdge].getReasonType(); Node reason = d_equalityEdges[currentEdge].getReason(); @@ -1195,18 +1216,20 @@ void EqualityEngine::getExplanation( case MERGED_THROUGH_CONGRUENCE: { // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl; - const FunctionApplication& f1 = d_applications[currentNode].original; - const FunctionApplication& f2 = d_applications[edgeNode].original; + const FunctionApplication& f1 = + d_applications[currentNode].d_original; + const FunctionApplication& f2 = + d_applications[edgeNode].d_original; Debug("equality") << push; Debug("equality") << "Explaining left hand side equalities" << std::endl; std::shared_ptr<EqProof> eqpc1 = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(f1.a, f2.a, equalities, cache, eqpc1.get()); + getExplanation(f1.d_a, f2.d_a, equalities, cache, eqpc1.get()); Debug("equality") << "Explaining right hand side equalities" << std::endl; std::shared_ptr<EqProof> eqpc2 = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(f1.b, f2.b, equalities, cache, eqpc2.get()); + getExplanation(f1.d_b, f2.d_b, equalities, cache, eqpc2.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); @@ -1214,25 +1237,35 @@ void EqualityEngine::getExplanation( //leave node null for now eqpc->d_node = Node::null(); } else { - if(d_nodes[f1.a].getKind() == kind::APPLY_UF || - d_nodes[f1.a].getKind() == kind::SELECT || - d_nodes[f1.a].getKind() == kind::STORE) { - eqpc->d_node = d_nodes[f1.a]; - } else { - if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) { - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); + if (d_nodes[f1.d_a].getKind() == kind::APPLY_UF + || d_nodes[f1.d_a].getKind() == kind::SELECT + || d_nodes[f1.d_a].getKind() == kind::STORE) + { + eqpc->d_node = d_nodes[f1.d_a]; + } + else + { + if (d_nodes[f1.d_a].getKind() == kind::BUILTIN + && d_nodes[f1.d_a].getConst<Kind>() == kind::SELECT) + { + eqpc->d_node = NodeManager::currentNM()->mkNode( + kind::PARTIAL_SELECT_1, d_nodes[f1.d_b]); // The first child is a PARTIAL_SELECT_0. // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); Assert(eqpc->d_children[0]->d_children.size() == 0); - eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, - d_nodes[f1.b]); - } else { - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, - ProofManager::currentPM()->mkOp(d_nodes[f1.a]), - d_nodes[f1.b]); + eqpc->d_children[0]->d_node = + NodeManager::currentNM()->mkNode( + kind::PARTIAL_SELECT_0, d_nodes[f1.d_b]); + } + else + { + eqpc->d_node = NodeManager::currentNM()->mkNode( + kind::PARTIAL_APPLY_UF, + ProofManager::currentPM()->mkOp(d_nodes[f1.d_a]), + d_nodes[f1.d_b]); } } } @@ -1245,14 +1278,14 @@ void EqualityEngine::getExplanation( // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode; - const FunctionApplication& eq = d_applications[eqId].original; + const FunctionApplication& eq = d_applications[eqId].d_original; Assert(eq.isEquality()) << "Must be an equality"; // Explain why a = b constant Debug("equality") << push; std::shared_ptr<EqProof> eqpc1 = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(eq.a, eq.b, equalities, cache, eqpc1.get()); + getExplanation(eq.d_a, eq.d_b, equalities, cache, eqpc1.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); } @@ -1335,8 +1368,8 @@ void EqualityEngine::getExplanation( } // Go to the previous - currentEdge = bfsQueue[currentIndex].edgeId; - currentIndex = bfsQueue[currentIndex].previousIndex; + currentEdge = bfsQueue[currentIndex].d_edgeId; + currentIndex = bfsQueue[currentIndex].d_previousIndex; //---from Morgan--- if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { @@ -1577,8 +1610,8 @@ void EqualityEngine::propagate() { d_propagationQueue.pop_front(); // Get the representatives - EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind(); - EqualityNodeId t2classId = getEqualityNode(current.t2Id).getFind(); + EqualityNodeId t1classId = getEqualityNode(current.d_t1Id).getFind(); + EqualityNodeId t2classId = getEqualityNode(current.d_t2Id).getFind(); // If already the same, we're done if (t1classId == t2classId) { @@ -1596,7 +1629,8 @@ void EqualityEngine::propagate() { Assert(node2.getFind() == t2classId); // Add the actual equality to the equality graph - addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason); + addGraphEdge( + current.d_t1Id, current.d_t2Id, current.d_type, current.d_reason); // If constants are being merged we're done if (d_isConstant[t1classId] && d_isConstant[t2classId]) { @@ -1642,14 +1676,18 @@ void EqualityEngine::propagate() { } if (mergeInto == t2classId) { - Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; + Debug("equality") << d_name << "::eq::propagate(): merging " + << d_nodes[current.d_t1Id] << " into " + << d_nodes[current.d_t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; if (!merge(node2, node1, triggers)) { d_done = true; } } else { - Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; + Debug("equality") << d_name << "::eq::propagate(): merging " + << d_nodes[current.d_t2Id] << " into " + << d_nodes[current.d_t1Id] << std::endl; d_assertedEqualities.push_back(Equality(t1classId, t2classId)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; if (!merge(node1, node2, triggers)) { @@ -1667,11 +1705,13 @@ void EqualityEngine::propagate() { if (d_performNotify && !d_done) { for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]]; - if (triggerInfo.trigger.getKind() == kind::EQUAL) { + if (triggerInfo.d_trigger.getKind() == kind::EQUAL) + { // Special treatment for disequalities - if (!triggerInfo.polarity) { + if (!triggerInfo.d_polarity) + { // Store that we are propagating a diseauality - TNode equality = triggerInfo.trigger; + TNode equality = triggerInfo.d_trigger; EqualityNodeId original = getNodeId(equality); TNode lhs = equality[0]; TNode rhs = equality[1]; @@ -1685,18 +1725,28 @@ void EqualityEngine::propagate() { d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); } storePropagatedDisequality(THEORY_LAST, lhsId, rhsId); - if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger, + triggerInfo.d_polarity)) + { d_done = true; } } - } else { + } + else + { // Equalities are simple - if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger, + triggerInfo.d_polarity)) + { d_done = true; } } - } else { - if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) { + } + else + { + if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger, + triggerInfo.d_polarity)) + { d_done = true; } } @@ -1776,10 +1826,13 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const if (find != d_applicationLookup.end()) { if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) { if (ensureProof) { - const FunctionApplication original = d_applications[find->second].original; - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.a)); + const FunctionApplication original = + d_applications[find->second].d_original; + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t1Id, original.d_a)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId)); - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b)); + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t2Id, original.d_b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } Debug("equality") << "\t(YES)" << std::endl; @@ -1788,15 +1841,18 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const } // Check the symmetric disequality - std::swap(eqNormalized.a, eqNormalized.b); + std::swap(eqNormalized.d_a, eqNormalized.d_b); find = d_applicationLookup.find(eqNormalized); if (find != d_applicationLookup.end()) { if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) { if (ensureProof) { - const FunctionApplication original = d_applications[find->second].original; - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.a)); + const FunctionApplication original = + d_applications[find->second].d_original; + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t2Id, original.d_a)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId)); - nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b)); + nonConst->d_deducedDisequalityReasons.push_back( + EqualityPair(t1Id, original.d_b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } Debug("equality") << "\t(YES)" << std::endl; @@ -1875,7 +1931,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Get the existing set TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); // Initialize the new set for copy/insert - newSetTags = Theory::setInsert(tag, triggerSet.tags); + newSetTags = Theory::setInsert(tag, triggerSet.d_tags); newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; @@ -1886,7 +1942,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) tags = Theory::setRemove(current, tags); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = - current == tag ? eqNodeId : triggerSet.triggers[i++]; + current == tag ? eqNodeId : triggerSet.d_triggers[i++]; } } else { // Setup a singleton @@ -1920,11 +1976,11 @@ TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const EqualityNodeId classId = getEqualityNode(t).getFind(); const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]); unsigned i = 0; - Theory::Set tags = triggerSet.tags; + Theory::Set tags = triggerSet.d_tags; while (Theory::setPop(tags) != tag) { ++ i; } - return d_nodes[triggerSet.triggers[i]]; + return d_nodes[triggerSet.d_triggers[i]]; } void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) { @@ -1938,9 +1994,12 @@ void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, // If an equality over constants we merge to false if (funNormalized.isEquality()) { - if (funNormalized.a == funNormalized.b) { + if (funNormalized.d_a == funNormalized.d_b) + { enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null())); - } else if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) { + } + else if (d_isConstant[funNormalized.d_a] && d_isConstant[funNormalized.d_b]) + { enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } @@ -1988,9 +2047,9 @@ EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(Theory::Set d_triggerDatabaseSize = d_triggerDatabaseSize + size; // Copy the information TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef); - newSet.tags = newSetTags; + newSet.d_tags = newSetTags; for (unsigned i = 0; i < newSetTriggersSize; ++i) { - newSet.triggers[i] = newSetTriggers[i]; + newSet.d_triggers[i] = newSetTriggers[i]; } // Return the new reference return newTriggerSetRef; @@ -2055,19 +2114,20 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size()); #ifdef CVC4_ASSERTIONS // Check that the reasons are valid - for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { + for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i) + { Assert( getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind()); } #endif if (Debug.isOn("equality::disequality")) { - for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { + for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i) + { TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first]; TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second]; Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(): because " << lhs << " == " << rhs << std::endl; } - } // Store for backtracking @@ -2089,7 +2149,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // The class we are looking for, shouldn't have any of the tags we are looking for already set Assert(d_nodeIndividualTrigger[classId] == null_set_id || Theory::setIntersection( - getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, + getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags, inputTags) == 0); @@ -2117,14 +2177,15 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI Debug("equality::trigger") << d_name << "::getDisequalities() : checking " << d_nodes[funId] << std::endl; - const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original; + const FunctionApplication& fun = + d_applications[useListNode.getApplicationId()].d_original; // If it's an equality asserted to false, we do the work if (fun.isEquality() && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { // Get the other equality member bool lhs = false; - EqualityNodeId toCompare = fun.b; + EqualityNodeId toCompare = fun.d_b; if (toCompare == currentId) { - toCompare = fun.a; + toCompare = fun.d_a; lhs = true; } // Representative of the other member @@ -2145,7 +2206,8 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // Tags of the other gey TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); // We only care if there are things in inputTags that is also in toCompareTags - Theory::Set commonTags = Theory::setIntersection(inputTags, toCompareTriggerSet.tags); + Theory::Set commonTags = + Theory::setIntersection(inputTags, toCompareTriggerSet.d_tags); if (commonTags) { out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs)); } @@ -2178,14 +2240,17 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger for (; !d_done && it != it_end; ++ it) { // The information about the equality that is asserted to false const TaggedEquality& disequalityInfo = *it; - const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); - Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags); + const TriggerTermSet& disequalityTriggerSet = + getTriggerTermSet(disequalityInfo.d_triggerSetRef); + Theory::Set commonTags = + Theory::setIntersection(disequalityTriggerSet.d_tags, tags); Assert(commonTags); // This is the actual function - const FunctionApplication& fun = d_applications[disequalityInfo.equalityId].original; + const FunctionApplication& fun = + d_applications[disequalityInfo.d_equalityId].d_original; // Figure out who we are comparing to in the original equality - EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b; - EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a; + EqualityNodeId toCompare = disequalityInfo.d_lhs ? fun.d_a : fun.d_b; + EqualityNodeId myCompare = disequalityInfo.d_lhs ? fun.d_b : fun.d_a; if (getEqualityNode(toCompare).getFind() == getEqualityNode(myCompare).getFind()) { // We're propagating a != a, which means we're inconsistent, just bail and let it go into // a regular conflict @@ -2203,7 +2268,8 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger if (!hasPropagatedDisequality(myRep, tagRep)) { d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep)); d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); - d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); + d_deducedDisequalityReasons.push_back( + EqualityPair(disequalityInfo.d_equalityId, d_falseId)); } // Store the propagation storePropagatedDisequality(currentTag, myRep, tagRep); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 73d8bd4e9..041625568 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -211,13 +211,13 @@ public: /** Statistics about the equality engine instance */ struct Statistics { /** Total number of merges */ - IntStat mergesCount; + IntStat d_mergesCount; /** Number of terms managed by the system */ - IntStat termsCount; + IntStat d_termsCount; /** Number of function terms managed by the system */ - IntStat functionTermsCount; + IntStat d_functionTermsCount; /** Number of constant terms managed by the system */ - IntStat constantTermsCount; + IntStat d_constantTermsCount; Statistics(std::string name); @@ -300,12 +300,14 @@ private: */ struct Equality { /** Left hand side of the equality */ - EqualityNodeId lhs; + EqualityNodeId d_lhs; /** Right hand side of the equality */ - EqualityNodeId rhs; + EqualityNodeId d_rhs; /** Equality constructor */ - Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id) - : lhs(lhs), rhs(rhs) {} + Equality(EqualityNodeId l = null_id, EqualityNodeId r = null_id) + : d_lhs(l), d_rhs(r) + { + } };/* struct EqualityEngine::Equality */ /** The ids of the classes we have merged */ @@ -402,12 +404,15 @@ private: */ struct Trigger { /** The current class id of the LHS of the trigger */ - EqualityNodeId classId; + EqualityNodeId d_classId; /** Next trigger for class */ - TriggerId nextTrigger; + TriggerId d_nextTrigger; - Trigger(EqualityNodeId classId = null_id, TriggerId nextTrigger = null_trigger) - : classId(classId), nextTrigger(nextTrigger) {} + Trigger(EqualityNodeId classId = null_id, + TriggerId nextTrigger = null_trigger) + : d_classId(classId), d_nextTrigger(nextTrigger) + { + } };/* struct EqualityEngine::Trigger */ /** @@ -573,14 +578,17 @@ private: /** Set of trigger terms */ struct TriggerTermSet { /** Set of theories in this set */ - Theory::Set tags; + Theory::Set d_tags; /** The trigger terms */ - EqualityNodeId triggers[0]; + EqualityNodeId d_triggers[0]; /** Returns the theory tags */ - Theory::Set hasTrigger(TheoryId tag) const { return Theory::setContains(tag, tags); } + Theory::Set hasTrigger(TheoryId tag) const + { + return Theory::setContains(tag, d_tags); + } /** Returns a trigger by tag */ EqualityNodeId getTrigger(TheoryId tag) const { - return triggers[Theory::setIndex(tag, tags)]; + return d_triggers[Theory::setIndex(tag, d_tags)]; } };/* struct EqualityEngine::TriggerTermSet */ @@ -618,10 +626,13 @@ private: context::CDO<DefaultSizeType> d_triggerDatabaseSize; struct TriggerSetUpdate { - EqualityNodeId classId; - TriggerTermSetRef oldValue; - TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) - : classId(classId), oldValue(oldValue) {} + EqualityNodeId d_classId; + TriggerTermSetRef d_oldValue; + TriggerSetUpdate(EqualityNodeId classId = null_id, + TriggerTermSetRef oldValue = null_set_id) + : d_classId(classId), d_oldValue(oldValue) + { + } };/* struct EqualityEngine::TriggerSetUpdate */ /** @@ -693,14 +704,18 @@ private: */ struct TaggedEquality { /** Id of the equality */ - EqualityNodeId equalityId; + EqualityNodeId d_equalityId; /** TriggerSet reference for the class of one of the sides */ - TriggerTermSetRef triggerSetRef; + TriggerTermSetRef d_triggerSetRef; /** Is trigger equivalent to the lhs (rhs otherwise) */ - bool lhs; + bool d_lhs; - TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true) - : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {} + TaggedEquality(EqualityNodeId equalityId = null_id, + TriggerTermSetRef triggerSetRef = null_set_id, + bool lhs = true) + : d_equalityId(equalityId), d_triggerSetRef(triggerSetRef), d_lhs(lhs) + { + } }; /** A map from equivalence class id's to tagged equalities */ diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 402b21a02..0e6d283fe 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -109,11 +109,14 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { * additional information. */ struct MergeCandidate { - EqualityNodeId t1Id, t2Id; - unsigned type; - TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason) - : t1Id(x), t2Id(y), type(type), reason(reason) + EqualityNodeId d_t1Id, d_t2Id; + unsigned d_type; + TNode d_reason; + MergeCandidate(EqualityNodeId x, + EqualityNodeId y, + unsigned type, + TNode reason) + : d_t1Id(x), d_t2Id(y), d_type(type), d_reason(reason) {} }; @@ -121,10 +124,13 @@ struct MergeCandidate { * Just an index into the reasons array, and the number of merges to consume. */ struct DisequalityReasonRef { - DefaultSizeType mergesStart; - DefaultSizeType mergesEnd; - DisequalityReasonRef(DefaultSizeType mergesStart = 0, DefaultSizeType mergesEnd = 0) - : mergesStart(mergesStart), mergesEnd(mergesEnd) {} + DefaultSizeType d_mergesStart; + DefaultSizeType d_mergesEnd; + DisequalityReasonRef(DefaultSizeType mergesStart = 0, + DefaultSizeType mergesEnd = 0) + : d_mergesStart(mergesStart), d_mergesEnd(mergesEnd) + { + } }; /** @@ -289,41 +295,38 @@ enum FunctionApplicationType { */ struct FunctionApplication { /** Type of application */ - FunctionApplicationType type; + FunctionApplicationType d_type; /** The actual application elements */ - EqualityNodeId a, b; + EqualityNodeId d_a, d_b; /** Construct an application */ - FunctionApplication(FunctionApplicationType type = APP_EQUALITY, EqualityNodeId a = null_id, EqualityNodeId b = null_id) - : type(type), a(a), b(b) {} + FunctionApplication(FunctionApplicationType type = APP_EQUALITY, + EqualityNodeId a = null_id, + EqualityNodeId b = null_id) + : d_type(type), d_a(a), d_b(b) + { + } /** Equality of two applications */ bool operator == (const FunctionApplication& other) const { - return type == other.type && a == other.a && b == other.b; + return d_type == other.d_type && d_a == other.d_a && d_b == other.d_b; } /** Is this a null application */ - bool isNull() const { - return a == null_id || b == null_id; - } + bool isNull() const { return d_a == null_id || d_b == null_id; } /** Is this an equality */ - bool isEquality() const { - return type == APP_EQUALITY; - } + bool isEquality() const { return d_type == APP_EQUALITY; } /** Is this an interpreted application (equality is special, i.e. not interpreted) */ - bool isInterpreted() const { - return type == APP_INTERPRETED; - } - + bool isInterpreted() const { return d_type == APP_INTERPRETED; } }; struct FunctionApplicationHashFunction { size_t operator () (const FunctionApplication& app) const { size_t hash = 0; - hash = 0x9e3779b9 + app.a; - hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2); + hash = 0x9e3779b9 + app.d_a; + hash ^= 0x9e3779b9 + app.d_b + (hash << 6) + (hash >> 2); return hash; } }; @@ -333,14 +336,15 @@ struct FunctionApplicationHashFunction { * we keep both the original, and the normalized version. */ struct FunctionApplicationPair { - FunctionApplication original; - FunctionApplication normalized; + FunctionApplication d_original; + FunctionApplication d_normalized; FunctionApplicationPair() {} - FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized) - : original(original), normalized(normalized) {} - bool isNull() const { - return original.isNull(); + FunctionApplicationPair(const FunctionApplication& original, + const FunctionApplication& normalized) + : d_original(original), d_normalized(normalized) + { } + bool isNull() const { return d_original.isNull(); } }; /** @@ -348,12 +352,14 @@ struct FunctionApplicationPair { */ struct TriggerInfo { /** The trigger itself */ - Node trigger; + Node d_trigger; /** Polarity of the trigger */ - bool polarity; - TriggerInfo() : polarity(false) {} + bool d_polarity; + TriggerInfo() : d_polarity(false) {} TriggerInfo(Node trigger, bool polarity) - : trigger(trigger), polarity(polarity) {} + : d_trigger(trigger), d_polarity(polarity) + { + } }; } // namespace eq diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3fe4321d0..7be085d48 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -898,6 +898,7 @@ set(regress_0_tests regress0/strings/code-eval.smt2 regress0/strings/code-perf.smt2 regress0/strings/code-sat-neg-one.smt2 + regress0/strings/complement-simple.smt2 regress0/strings/escchar.smt2 regress0/strings/escchar_25.smt2 regress0/strings/hconst-092618.smt2 @@ -905,6 +906,7 @@ set(regress_0_tests regress0/strings/idof-sem.smt2 regress0/strings/ilc-like.smt2 regress0/strings/indexof-sym-simp.smt2 + regress0/strings/is_digit_simple.smt2 regress0/strings/issue1189.smt2 regress0/strings/issue2958.smt2 regress0/strings/issue3440.smt2 @@ -920,6 +922,7 @@ set(regress_0_tests regress0/strings/parser-syms.cvc regress0/strings/re.all.smt2 regress0/strings/re-syntax.smt2 + regress0/strings/re_diff.smt2 regress0/strings/regexp-native-simple.cvc regress0/strings/regexp_inclusion.smt2 regress0/strings/regexp_inclusion_reduction.smt2 @@ -1310,6 +1313,7 @@ set(regress_1_tests regress1/nl/issue3300-approx-sqrt-witness.smt2 regress1/nl/issue3441.smt2 regress1/nl/issue3617.smt2 + regress1/nl/issue3647.smt2 regress1/nl/issue3656.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 @@ -1661,6 +1665,7 @@ set(regress_1_tests regress1/strings/cmu-inc-nlpp-071516.smt2 regress1/strings/cmu-substr-rw.smt2 regress1/strings/code-sequence.smt2 + regress1/strings/complement-test.smt2 regress1/strings/crash-1019.smt2 regress1/strings/csp-prefix-exp-bug.smt2 regress1/strings/double-replace.smt2 @@ -1924,7 +1929,6 @@ set(regress_2_tests regress2/arith/prp-13-24.smt2 regress2/arith/pursuit-safety-11.smtv1.smt2 regress2/arith/pursuit-safety-12.smtv1.smt2 - regress2/arith/real2int-test.smt2 regress2/arith/sc-7.base.cvc.smtv1.smt2 regress2/arith/uart-8.base.cvc.smtv1.smt2 regress2/auflia-fuzz06.smtv1.smt2 @@ -2339,6 +2343,8 @@ set(regression_disabled_tests regress2/arith/arith-int-098.cvc regress2/arith/miplib-opt1217--27.smt2 regress2/arith/miplib-pp08a-3000.smt2 + # timeout on debug + regress2/arith/real2int-test.smt2 regress2/bug396.smt2 regress2/nl/dumortier-050317.smt2 regress2/nl/nt-lemmas-bad.smt2 diff --git a/test/regress/regress0/strings/complement-simple.smt2 b/test/regress/regress0/strings/complement-simple.smt2 new file mode 100644 index 000000000..c19699448 --- /dev/null +++ b/test/regress/regress0/strings/complement-simple.smt2 @@ -0,0 +1,5 @@ +(set-logic SLIA) +(set-info :status sat) +(declare-fun x () String) +(assert (str.in.re x (re.comp (str.to.re "ABC")))) +(check-sat) diff --git a/test/regress/regress0/strings/is_digit_simple.smt2 b/test/regress/regress0/strings/is_digit_simple.smt2 new file mode 100644 index 000000000..d95a22078 --- /dev/null +++ b/test/regress/regress0/strings/is_digit_simple.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(assert (str.is_digit "0")) +(assert (str.is_digit "7")) +(assert (not (str.is_digit "A"))) +(assert (not (str.is_digit ""))) + +(check-sat) diff --git a/test/regress/regress0/strings/re_diff.smt2 b/test/regress/regress0/strings/re_diff.smt2 new file mode 100644 index 000000000..d63731acb --- /dev/null +++ b/test/regress/regress0/strings/re_diff.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in_re x (re.diff (re.* (str.to_re "A")) re.none))) +(assert (or (not (str.in_re x (re.* (str.to_re "A")))) (str.in_re y (re.diff (re.* (str.to_re "B")) re.all)))) + +(check-sat) diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index 1b060637a..d506dd5b2 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --uf-ho ; EXPECT: unsat -(set-logic LIA) +(set-logic UFLIA) (declare-fun uf (Int) Int) diff --git a/test/regress/regress1/bv/issue3654.smt2 b/test/regress/regress1/bv/issue3654.smt2 index 59c11456f..a1e2f8b87 100644 --- a/test/regress/regress1/bv/issue3654.smt2 +++ b/test/regress/regress1/bv/issue3654.smt2 @@ -1,4 +1,4 @@ -; COMMAND_LINE: --ext-rew-prep +; COMMAND-LINE: --ext-rew-prep ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress1/bv/issue3776.smt2 b/test/regress/regress1/bv/issue3776.smt2 index 215f3e253..30c034c70 100644 --- a/test/regress/regress1/bv/issue3776.smt2 +++ b/test/regress/regress1/bv/issue3776.smt2 @@ -1,4 +1,4 @@ -; COMMAND_LINE: --rewrite-divk +; COMMAND-LINE: --rewrite-divk ; EXPECT: sat (set-logic QF_BVLIA) (declare-fun t () Int) diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2 new file mode 100644 index 000000000..0fc0f55f9 --- /dev/null +++ b/test/regress/regress1/nl/issue3647.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models --produce-models --decision=internal +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (distinct (sin 1.0) 0.0)) +(check-sat) diff --git a/test/regress/regress1/strings/complement-test.smt2 b/test/regress/regress1/strings/complement-test.smt2 new file mode 100644 index 000000000..1fcbdc2c3 --- /dev/null +++ b/test/regress/regress1/strings/complement-test.smt2 @@ -0,0 +1,12 @@ +(set-logic SLIA) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(assert (= x (str.++ "AB" y))) +(assert (or (= y "C") (= y (str.++ "D" z)) (= (str.len y) 10))) +(assert (str.in.re x + (re.inter + (re.comp (str.to.re "AB")) + (re.comp (re.++ (str.to.re "AB") (re.range "A" "E") (re.* re.allchar)))))) +(check-sat) diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy index eee7956f4..45d49e75b 100644 --- a/test/regress/regress1/sygus/constant-bool-si-all.sy +++ b/test/regress/regress1/sygus/constant-bool-si-all.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status -(set-logic SAT) +(set-logic LIA) (synth-fun f () Bool) (synth-fun g () Bool) (synth-fun h () Bool) diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy index 7229dea2e..e20520a4a 100644 --- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy +++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete -(set-logic SAT) +(set-logic LIA) (synth-fun u ((x Int)) Int) (synth-fun f () Bool) (synth-fun g () Bool) diff --git a/test/regress/regress1/sygus/issue3802-default-consts.sy b/test/regress/regress1/sygus/issue3802-default-consts.sy index 10daee6ec..e07365052 100644 --- a/test/regress/regress1/sygus/issue3802-default-consts.sy +++ b/test/regress/regress1/sygus/issue3802-default-consts.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) (synth-fun f () Bool diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy index b9731de0f..66880eafa 100644 --- a/test/regress/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) +; COMMAND-LINE: --sygus-out=status --uf-ho +(set-logic UFLIA) (declare-fun uf ( Int ) Int) (synth-fun f ((x Int) (y Int)) Bool ((Start Bool (true false diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy index bf1cd1576..282bc122c 100644 --- a/test/regress/regress1/sygus/tester.sy +++ b/test/regress/regress1/sygus/tester.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status -(set-logic SLIA) +(set-logic DTSLIA) (declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool)))) (define-fun isA ((i DT)) Bool ((_ is A) i) ) |