summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/base_solver.cpp38
-rw-r--r--src/theory/strings/infer_proof_cons.cpp5
-rw-r--r--src/theory/strings/infer_proof_cons.h5
-rw-r--r--src/theory/strings/inference_manager.cpp15
-rw-r--r--src/theory/strings/inference_manager.h9
-rw-r--r--src/theory/strings/kinds4
-rw-r--r--src/theory/strings/regexp_enumerator.cpp49
-rw-r--r--src/theory/strings/regexp_enumerator.h59
-rw-r--r--src/theory/strings/regexp_solver.cpp5
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback