diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/base_solver.cpp | 38 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.h | 5 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 15 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.h | 9 | ||||
-rw-r--r-- | src/theory/strings/kinds | 4 | ||||
-rw-r--r-- | src/theory/strings/regexp_enumerator.cpp | 49 | ||||
-rw-r--r-- | src/theory/strings/regexp_enumerator.h | 59 | ||||
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 5 |
9 files changed, 178 insertions, 11 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index b675d2444..9396e3e87 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -17,6 +17,7 @@ #include "theory/strings/base_solver.h" #include "expr/sequence.h" +#include "options/quantifiers_options.h" #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" @@ -539,8 +540,41 @@ void BaseSolver::checkCardinalityType(TypeNode tn, // infinite cardinality, we are fine return; } - // TODO (cvc4-projects #23): how to handle sequence for finite types? - return; + // we check the cardinality class of the type, assuming that FMF is + // disabled. + if (isCardinalityClassFinite(etn.getCardinalityClass(), false)) + { + Cardinality c = etn.getCardinality(); + bool smallCardinality = false; + if (!c.isLargeFinite()) + { + Integer ci = c.getFiniteCardinality(); + if (ci.fitsUnsignedInt()) + { + smallCardinality = true; + typeCardSize = ci.toUnsignedInt(); + } + } + if (!smallCardinality) + { + // if it is large finite, then there is no way we could have + // constructed that many terms in memory, hence there is nothing + // to do. + return; + } + } + else + { + Assert(options().quantifiers.finiteModelFind); + // we are in a case where the cardinality of the type is infinite + // if not FMF, and finite given the Env's option value for FMF. In this + // case, FMF must be true, and the cardinality is finite and dynamic + // (i.e. it depends on the model's finite interpretation for uninterpreted + // sorts). We do not know how to handle this case, we set incomplete. + // TODO (cvc4-projects #23): how to handle sequence for finite types? + d_im.setIncomplete(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY); + return; + } } // for each collection for (unsigned i = 0, csize = cols.size(); i < csize; ++i) diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 34597c8be..5eba8663a 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -59,6 +59,11 @@ void InferProofCons::notifyFact(const InferInfo& ii) d_lazyFactMap.insert(ii.d_conc, iic); } +void InferProofCons::notifyLemma(const InferInfo& ii) +{ + d_lazyFactMap[ii.d_conc] = std::make_shared<InferInfo>(ii); +} + bool InferProofCons::addProofTo(CDProof* pf, Node conc, InferenceId infer, diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 110d231cf..02b266fd7 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -69,6 +69,11 @@ class InferProofCons : public ProofGenerator * only for facts that are explained. */ void notifyFact(const InferInfo& ii); + /** + * Same as above, but always overwrites. This is used for lemmas and + * conflicts, which do not necessarily have unique conclusions. + */ + void notifyLemma(const InferInfo& ii); /** * This returns the proof for fact. This is required for using this class as diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 0e971fc54..1f531a97c 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -42,7 +42,8 @@ InferenceManager::InferenceManager(Env& env, d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) + d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr), + d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -279,12 +280,12 @@ void InferenceManager::processConflict(const InferInfo& ii) { Assert(!d_state.isInConflict()); // setup the fact to reproduce the proof in the call below - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } // make the trust node - TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get()); + TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get()); Assert(tconf.getKind() == TrustNodeKind::CONFLICT); Trace("strings-assert") << "(assert (not " << tconf.getNode() << ")) ; conflict " << ii.getId() << std::endl; @@ -335,11 +336,11 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) } // ensure that the proof generator is ready to explain the final conclusion // of the lemma (ii.d_conc). - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } - TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get()); + TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get()); Trace("strings-pending") << "Process pending lemma : " << tlem.getNode() << std::endl; diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 49f10d7cb..9f4cd1986 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -249,8 +249,15 @@ class InferenceManager : public InferenceManagerBuffered ExtTheory& d_extt; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; - /** Conversion from inferences to proofs */ + /** Conversion from inferences to proofs for facts */ std::unique_ptr<InferProofCons> d_ipc; + /** + * Conversion from inferences to proofs for lemmas and conflicts. This is + * separate from the above proof generator to avoid rare cases where the + * conclusion of a lemma is a duplicate of the conclusion of another lemma, + * or is a fact in the current equality engine. + */ + std::unique_ptr<InferProofCons> d_ipcl; /** Common constants */ Node d_true; Node d_false; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index aa95ef2f8..9faa935e1 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -56,6 +56,10 @@ enumerator STRING_TYPE \ "::cvc5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" +enumerator REGEXP_TYPE \ + "::cvc5::theory::strings::RegExpEnumerator" \ + "theory/strings/regexp_enumerator.h" + constant CONST_STRING \ class \ String \ diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp new file mode 100644 index 000000000..261d0008e --- /dev/null +++ b/src/theory/strings/regexp_enumerator.cpp @@ -0,0 +1,49 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of enumerator for regular expressions. + */ + +#include "theory/strings/regexp_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase<RegExpEnumerator>(type), d_senum(type, tep) +{ +} + +RegExpEnumerator::RegExpEnumerator(const RegExpEnumerator& enumerator) + : TypeEnumeratorBase<RegExpEnumerator>(enumerator.getType()), + d_senum(enumerator.d_senum) +{ +} + +Node RegExpEnumerator::operator*() +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STRING_TO_REGEXP, *d_senum); +} + +RegExpEnumerator& RegExpEnumerator::operator++() +{ + ++d_senum; + return *this; +} + +bool RegExpEnumerator::isFinished() { return d_senum.isFinished(); } + +} // namespace strings +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/strings/regexp_enumerator.h b/src/theory/strings/regexp_enumerator.h new file mode 100644 index 000000000..289c8b046 --- /dev/null +++ b/src/theory/strings/regexp_enumerator.h @@ -0,0 +1,59 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Enumerators for regular expressions. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H +#define CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H + +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/strings/type_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +/** + * Simple regular expression enumerator, generates only singleton language + * regular expressions from a string enumeration, in other words: + * (str.to_re s1) ... (str.to_re sn) .... + * where s1 ... sn ... is the enumeration for strings. + */ +class RegExpEnumerator : public TypeEnumeratorBase<RegExpEnumerator> +{ + public: + RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + RegExpEnumerator(const RegExpEnumerator& enumerator); + ~RegExpEnumerator() {} + /** get the current term */ + Node operator*() override; + /** increment */ + RegExpEnumerator& operator++() override; + /** is this enumerator finished? */ + bool isFinished() override; + + private: + /** underlying string enumerator */ + StringEnumerator d_senum; +}; + +} // namespace strings +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 614a5e6e0..898c0f1b7 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -546,7 +546,10 @@ bool RegExpSolver::checkPDerivative( { std::vector<Node> noExplain; noExplain.push_back(atom); - noExplain.push_back(x.eqNode(d_emptyString)); + if (x != d_emptyString) + { + noExplain.push_back(x.eqNode(d_emptyString)); + } std::vector<Node> iexp = nf_exp; iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF); |