From: Andrew Reynolds Date: Sat, 8 Feb 2020 05:16:12 +0000 (-0600) Subject: Split strings finite model finding strategy (#3727) X-Git-Tag: cvc5-1.0.0~3668 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f9b6b57255d38fa9bee6b66dae3b8932703135a;p=cvc5.git Split strings finite model finding strategy (#3727) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5bb239bd5..81328831a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -690,6 +690,8 @@ libcvc4_add_sources( theory/strings/skolem_cache.h theory/strings/solver_state.cpp theory/strings/solver_state.h + theory/strings/strings_fmf.cpp + theory/strings/strings_fmf.h theory/strings/theory_strings.cpp theory/strings/theory_strings.h theory/strings/theory_strings_preprocess.cpp diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp new file mode 100644 index 000000000..8ca6d2de1 --- /dev/null +++ b/src/theory/strings/strings_fmf.cpp @@ -0,0 +1,124 @@ +/********************* */ +/*! \file strings_fmf.cpp + ** \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 Implementation of a finite model finding decision strategy for + ** strings. + **/ + +#include "theory/strings/strings_fmf.h" + +using namespace std; +using namespace CVC4::context; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +StringsFmf::StringsFmf(context::Context* c, + context::UserContext* u, + Valuation valuation, + SkolemCache& skc) + : d_sslds(nullptr), + d_satContext(c), + d_userContext(u), + d_valuation(valuation), + d_skCache(skc), + d_inputVars(u) +{ +} + +StringsFmf::~StringsFmf() {} + +void StringsFmf::preRegisterTerm(TNode n) +{ + if (!n.getType().isString()) + { + return; + } + Kind k = n.getKind(); + // Our decision strategy will minimize the length of this term if it is a + // variable but not an internally generated Skolem, or a term that does + // not belong to this theory. + if (n.isVar() ? !d_skCache.isSkolem(n) : kindToTheoryId(k) != THEORY_STRINGS) + { + d_inputVars.insert(n); + Trace("strings-dstrat-reg") << "input variable: " << n << std::endl; + } +} + +void StringsFmf::presolve() +{ + d_sslds.reset(new StringSumLengthDecisionStrategy( + d_satContext, d_userContext, d_valuation)); + Trace("strings-dstrat-reg") + << "presolve: register decision strategy." << std::endl; + std::vector inputVars; + for (NodeSet::const_iterator itr = d_inputVars.begin(); + itr != d_inputVars.end(); + ++itr) + { + inputVars.push_back(*itr); + } + d_sslds->initialize(inputVars); +} + +DecisionStrategy* StringsFmf::getDecisionStrategy() const +{ + return d_sslds.get(); +} + +StringsFmf::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy( + context::Context* c, context::UserContext* u, Valuation valuation) + : DecisionStrategyFmf(c, valuation), d_inputVarLsum(u) +{ +} + +bool StringsFmf::StringSumLengthDecisionStrategy::isInitialized() +{ + return !d_inputVarLsum.get().isNull(); +} + +void StringsFmf::StringSumLengthDecisionStrategy::initialize( + const std::vector& vars) +{ + if (d_inputVarLsum.get().isNull() && !vars.empty()) + { + NodeManager* nm = NodeManager::currentNM(); + std::vector sum; + for (const Node& v : vars) + { + sum.push_back(nm->mkNode(STRING_LENGTH, v)); + } + Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum); + d_inputVarLsum.set(sumn); + } +} + +Node StringsFmf::StringSumLengthDecisionStrategy::mkLiteral(unsigned i) +{ + if (d_inputVarLsum.get().isNull()) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); + Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConst(Rational(i))); + Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl; + return lit; +} +std::string StringsFmf::StringSumLengthDecisionStrategy::identify() const +{ + return std::string("string_sum_len"); +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h new file mode 100644 index 000000000..375a100ff --- /dev/null +++ b/src/theory/strings/strings_fmf.h @@ -0,0 +1,123 @@ +/********************* */ +/*! \file strings_fmf.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 A finite model finding decision strategy for strings. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__STRINGS_FMF_H +#define CVC4__THEORY__STRINGS__STRINGS_FMF_H + +#include "context/cdhashset.h" +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/decision_strategy.h" +#include "theory/strings/skolem_cache.h" +#include "theory/valuation.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** Strings finite model finding + * + * This class manages the creation of a decision strategy that bounds the + * sum of lengths of terms of type string. + */ +class StringsFmf +{ + typedef context::CDHashSet NodeSet; + + public: + StringsFmf(context::Context* c, + context::UserContext* u, + Valuation valuation, + SkolemCache& skc); + ~StringsFmf(); + /** preRegister term + * + * This determines if the term n should be added to d_inputVars, the set + * of terms of type string whose length we are minimizing with this decision + * strategy. + */ + void preRegisterTerm(TNode n); + /** presolve + * + * This initializes a (new copy) of the decision strategy d_sslds. + */ + void presolve(); + /** + * Get the decision strategy, valid after a call to presolve in the duration + * of a check-sat call. + */ + DecisionStrategy* getDecisionStrategy() const; + + private: + /** String sum of lengths decision strategy + * + * This decision strategy enforces that len(x_1) + ... + len(x_k) <= n + * for a minimal natural number n, where x_1, ..., x_n is the list of + * input variables of the problem of type String. + * + * This decision strategy is enabled by option::stringsFmf(). + */ + class StringSumLengthDecisionStrategy : public DecisionStrategyFmf + { + public: + StringSumLengthDecisionStrategy(context::Context* c, + context::UserContext* u, + Valuation valuation); + /** make literal */ + Node mkLiteral(unsigned i) override; + /** identify */ + std::string identify() const override; + /** is initialized */ + bool isInitialized(); + /** initialize */ + void initialize(const std::vector& vars); + + /* + * Do not hide the zero-argument version of initialize() inherited from the + * base class + */ + using DecisionStrategyFmf::initialize; + + private: + /** + * User-context-dependent node corresponding to the sum of the lengths of + * input variables of type string + */ + context::CDO d_inputVarLsum; + }; + /** an instance of the above class */ + std::unique_ptr d_sslds; + /** The SAT search context for the theory of strings. */ + context::Context* d_satContext; + /** The user level assertion context for the theory of strings. */ + context::UserContext* d_userContext; + /** The valuation object */ + Valuation d_valuation; + /** reference to the skolem cache */ + SkolemCache& d_skCache; + /** + * The set of terms of type string whose length we are minimizing + * with this decision strategy. + */ + NodeSet d_inputVars; +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__STRINGS_FMF_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 33bde3162..197f7ac4c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -84,11 +84,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_bsolver(c, u, d_state, d_im), d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver), d_regexp_solver(*this, d_state, d_im, c, u), - d_input_vars(u), - d_input_var_lsum(u), - d_cardinality_lits(u), - d_curr_cardinality(c, 0), - d_sslds(nullptr), + d_stringsFmf(c, u, valuation, d_sk_cache), d_strategy_init(false) { setupExtTheory(); @@ -405,25 +401,15 @@ void TheoryStrings::presolve() { // if strings fmf is enabled, register the strategy if (options::stringFMF()) { - d_sslds.reset(new StringSumLengthDecisionStrategy( - getSatContext(), getUserContext(), d_valuation)); - Trace("strings-dstrat-reg") - << "presolve: register decision strategy." << std::endl; - std::vector inputVars; - for (NodeSet::const_iterator itr = d_input_vars.begin(); - itr != d_input_vars.end(); - ++itr) - { - inputVars.push_back(*itr); - } - d_sslds->initialize(inputVars); + d_stringsFmf.presolve(); // This strategy is local to a check-sat call, since we refresh the strategy // on every call to presolve. getDecisionManager()->registerStrategy( DecisionManager::STRAT_STRINGS_SUM_LENGTHS, - d_sslds.get(), + d_stringsFmf.getDecisionStrategy(), DecisionManager::STRAT_SCOPE_LOCAL_SOLVE); } + Debug("strings-presolve") << "Finished presolve" << std::endl; } @@ -749,17 +735,6 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } } - // if finite model finding is enabled, - // then we minimize the length of this term if it is a variable - // but not an internally generated Skolem, or a term that does - // not belong to this theory. - if (options::stringFMF() - && (n.isVar() ? !d_sk_cache.isSkolem(n) - : kindToTheoryId(k) != THEORY_STRINGS)) - { - d_input_vars.insert(n); - Trace("strings-dstrat-reg") << "input variable: " << n << std::endl; - } d_equalityEngine.addTerm(n); } else if (tn.isBoolean()) { // Get triggered for both equal and dis-equal @@ -783,6 +758,11 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } } + // register with finite model finding + if (options::stringFMF()) + { + d_stringsFmf.preRegisterTerm(n); + } } } @@ -1932,52 +1912,6 @@ void TheoryStrings::checkCardinality() { Trace("strings-card") << "...end check cardinality" << std::endl; } - -//// Finite Model Finding - -TheoryStrings::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy( - context::Context* c, context::UserContext* u, Valuation valuation) - : DecisionStrategyFmf(c, valuation), d_input_var_lsum(u) -{ -} - -bool TheoryStrings::StringSumLengthDecisionStrategy::isInitialized() -{ - return !d_input_var_lsum.get().isNull(); -} - -void TheoryStrings::StringSumLengthDecisionStrategy::initialize( - const std::vector& vars) -{ - if (d_input_var_lsum.get().isNull() && !vars.empty()) - { - NodeManager* nm = NodeManager::currentNM(); - std::vector sum; - for (const Node& v : vars) - { - sum.push_back(nm->mkNode(STRING_LENGTH, v)); - } - Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum); - d_input_var_lsum.set(sumn); - } -} - -Node TheoryStrings::StringSumLengthDecisionStrategy::mkLiteral(unsigned i) -{ - if (d_input_var_lsum.get().isNull()) - { - return Node::null(); - } - NodeManager* nm = NodeManager::currentNM(); - Node lit = nm->mkNode(LEQ, d_input_var_lsum.get(), nm->mkConst(Rational(i))); - Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl; - return lit; -} -std::string TheoryStrings::StringSumLengthDecisionStrategy::identify() const -{ - return std::string("string_sum_len"); -} - Node TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; Node atomElim; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 5e00f9416..960d3ceaa 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -23,7 +23,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/node_trie.h" -#include "theory/decision_manager.h" #include "theory/strings/base_solver.h" #include "theory/strings/core_solver.h" #include "theory/strings/infer_info.h" @@ -34,6 +33,7 @@ #include "theory/strings/regexp_solver.h" #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" +#include "theory/strings/strings_fmf.h" #include "theory/strings/theory_strings_preprocess.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -461,51 +461,8 @@ private: RegExpSolver d_regexp_solver; /** regular expression elimination module */ RegExpElimination d_regexp_elim; - - // Finite Model Finding - private: - NodeSet d_input_vars; - context::CDO< Node > d_input_var_lsum; - context::CDHashMap< int, Node > d_cardinality_lits; - context::CDO< int > d_curr_cardinality; - /** String sum of lengths decision strategy - * - * This decision strategy enforces that len(x_1) + ... + len(x_k) <= n - * for a minimal natural number n, where x_1, ..., x_n is the list of - * input variables of the problem of type String. - * - * This decision strategy is enabled by option::stringsFmf(). - */ - class StringSumLengthDecisionStrategy : public DecisionStrategyFmf - { - public: - StringSumLengthDecisionStrategy(context::Context* c, - context::UserContext* u, - Valuation valuation); - /** make literal */ - Node mkLiteral(unsigned i) override; - /** identify */ - std::string identify() const override; - /** is initialized */ - bool isInitialized(); - /** initialize */ - void initialize(const std::vector& vars); - - /* - * Do not hide the zero-argument version of initialize() inherited from the - * base class - */ - using DecisionStrategyFmf::initialize; - - private: - /** - * User-context-dependent node corresponding to the sum of the lengths of - * input variables of type string - */ - context::CDO d_input_var_lsum; - }; - /** an instance of the above class */ - std::unique_ptr d_sslds; + /** Strings finite model finding decision strategy */ + StringsFmf d_stringsFmf; public: // ppRewrite