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
--- /dev/null
+/********************* */
+/*! \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<Node> 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<Node>& vars)
+{
+ if (d_inputVarLsum.get().isNull() && !vars.empty())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> 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
--- /dev/null
+/********************* */
+/*! \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<Node, NodeHashFunction> 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<Node>& 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<Node> d_inputVarLsum;
+ };
+ /** an instance of the above class */
+ std::unique_ptr<StringSumLengthDecisionStrategy> 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 */
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();
// 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<Node> 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;
}
}
}
}
- // 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
}
}
}
+ // register with finite model finding
+ if (options::stringFMF())
+ {
+ d_stringsFmf.preRegisterTerm(n);
+ }
}
}
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<Node>& vars)
-{
- if (d_input_var_lsum.get().isNull() && !vars.empty())
- {
- NodeManager* nm = NodeManager::currentNM();
- std::vector<Node> 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;
#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"
#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"
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<Node>& 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<Node> d_input_var_lsum;
- };
- /** an instance of the above class */
- std::unique_ptr<StringSumLengthDecisionStrategy> d_sslds;
+ /** Strings finite model finding decision strategy */
+ StringsFmf d_stringsFmf;
public:
// ppRewrite
projects / cvc5.git / commitdiff