summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/inference_manager.cpp12
-rw-r--r--src/theory/strings/inference_manager.h16
-rw-r--r--src/theory/strings/theory_strings.cpp163
-rw-r--r--src/theory/strings/theory_strings.h21
-rw-r--r--src/theory/strings/theory_strings_utils.cpp19
-rw-r--r--src/theory/strings/theory_strings_utils.h5
6 files changed, 157 insertions, 79 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index c9a2bcd70..2b5338a6a 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -16,6 +16,7 @@
#include "expr/kind.h"
#include "options/strings_options.h"
+#include "theory/ext_theory.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings.h"
#include "theory/strings/theory_strings_rewriter.h"
@@ -625,6 +626,17 @@ void InferenceManager::explain(TNode literal,
}
}
}
+void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
+
+void InferenceManager::markCongruent(Node a, Node b)
+{
+ Assert(a.getKind() == b.getKind());
+ ExtTheory* eth = d_parent.getExtTheory();
+ if (eth->hasFunctionKind(a.getKind()))
+ {
+ eth->markCongruent(a, b);
+ }
+}
} // namespace strings
} // namespace theory
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index e052889f6..819e4b98f 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -61,7 +61,8 @@ class TheoryStrings;
* to doPendingLemmas.
*
* It also manages other kinds of interaction with the output channel of the
- * theory of strings, e.g. sendPhaseRequirement.
+ * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
+ * with the extended theory object e.g. markCongruent.
*/
class InferenceManager
{
@@ -249,6 +250,19 @@ class InferenceManager
* the node corresponding to their conjunction.
*/
void explain(TNode literal, std::vector<TNode>& assumptions) const;
+ /**
+ * Set that we are incomplete for the current set of assertions (in other
+ * words, we must answer "unknown" instead of "sat"); this calls the output
+ * channel's setIncomplete method.
+ */
+ void setIncomplete();
+ /**
+ * Mark that terms a and b are congruent in the current context.
+ * This makes a call to markCongruent in the extended theory object of
+ * the parent theory if the kind of a (and b) is owned by the extended
+ * theory.
+ */
+ void markCongruent(Node a, Node b);
private:
/**
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6000489cf..755e6b4df 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2486,26 +2486,25 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
return Node::null();
}
-void TheoryStrings::checkNormalFormsEq()
+void TheoryStrings::checkRegisterTermsPreNormalForm()
{
- if( !options::stringEagerLen() ){
- for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
- Node eqc = d_strings_eqc[i];
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
- while( !eqc_i.isFinished() ) {
- Node n = (*eqc_i);
- if( d_congruent.find( n )==d_congruent.end() ){
- registerTerm( n, 2 );
- }
- ++eqc_i;
+ for (const Node& eqc : d_strings_eqc)
+ {
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+ while (!eqc_i.isFinished())
+ {
+ Node n = (*eqc_i);
+ if (d_congruent.find(n) == d_congruent.end())
+ {
+ registerTerm(n, 2);
}
+ ++eqc_i;
}
}
+}
- if (d_im.hasProcessed())
- {
- return;
- }
+void TheoryStrings::checkNormalFormsEq()
+{
// calculate normal forms for each equivalence class, possibly adding
// splitting lemmas
d_normal_form.clear();
@@ -2819,7 +2818,7 @@ void TheoryStrings::getNormalForms(Node eqc,
if (Trace.isOn("strings-error"))
{
Trace("strings-error") << "Cycle for normal form ";
- printConcat(currv, "strings-error");
+ utils::printConcatTrace(currv, "strings-error");
Trace("strings-error") << "..." << currv[i] << std::endl;
}
Assert(!d_state.areEqual(currv[i], n));
@@ -4176,7 +4175,8 @@ void TheoryStrings::checkNormalFormsDeq()
{
Trace("strings-solve") << "- Verify disequalities are processed for "
<< cols[i][0] << ", normal form : ";
- printConcat(getNormalForm(cols[i][0]).d_nf, "strings-solve");
+ utils::printConcatTrace(getNormalForm(cols[i][0]).d_nf,
+ "strings-solve");
Trace("strings-solve")
<< "... #eql = " << cols[i].size() << std::endl;
}
@@ -4197,9 +4197,11 @@ void TheoryStrings::checkNormalFormsDeq()
if (Trace.isOn("strings-solve"))
{
Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
- printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve");
+ utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf,
+ "strings-solve");
Trace("strings-solve") << " against " << cols[i][k] << " ";
- printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve");
+ utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf,
+ "strings-solve");
Trace("strings-solve") << "..." << std::endl;
}
processDeq(cols[i][j], cols[i][k]);
@@ -4217,54 +4219,67 @@ void TheoryStrings::checkNormalFormsDeq()
}
void TheoryStrings::checkLengthsEqc() {
- if( options::stringLenNorm() ){
- for( unsigned i=0; i<d_strings_eqc.size(); i++ ){
- NormalForm& nfi = getNormalForm(d_strings_eqc[i]);
- Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl;
- //check if there is a length term for this equivalence class
- EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false);
- Node lt = ei ? ei->d_lengthTerm : Node::null();
- if( !lt.isNull() ) {
- Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
- //now, check if length normalization has occurred
- if (ei->d_normalizedLength.get().isNull())
+ for (unsigned i = 0; i < d_strings_eqc.size(); i++)
+ {
+ NormalForm& nfi = getNormalForm(d_strings_eqc[i]);
+ Trace("strings-process-debug")
+ << "Process length constraints for " << d_strings_eqc[i] << std::endl;
+ // check if there is a length term for this equivalence class
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false);
+ Node lt = ei ? ei->d_lengthTerm : Node::null();
+ if (lt.isNull())
+ {
+ Trace("strings-process-debug")
+ << "No length term for eqc " << d_strings_eqc[i] << " "
+ << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl;
+ continue;
+ }
+ Node llt = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, lt);
+ // now, check if length normalization has occurred
+ if (ei->d_normalizedLength.get().isNull())
+ {
+ Node nf = utils::mkNConcat(nfi.d_nf);
+ if (Trace.isOn("strings-process-debug"))
+ {
+ Trace("strings-process-debug")
+ << " normal form is " << nf << " from base " << nfi.d_base
+ << std::endl;
+ Trace("strings-process-debug") << " normal form exp is: " << std::endl;
+ for (const Node& exp : nfi.d_exp)
{
- Node nf = utils::mkNConcat(nfi.d_nf);
- if( Trace.isOn("strings-process-debug") ){
- Trace("strings-process-debug")
- << " normal form is " << nf << " from base " << nfi.d_base
- << std::endl;
- Trace("strings-process-debug") << " normal form exp is: " << std::endl;
- for (const Node& exp : nfi.d_exp)
- {
- Trace("strings-process-debug") << " " << exp << std::endl;
- }
- }
-
- //if not, add the lemma
- std::vector< Node > ant;
- ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end());
- ant.push_back(nfi.d_base.eqNode(lt));
- Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf );
- Node lcr = Rewriter::rewrite( lc );
- Trace("strings-process-debug") << "Rewrote length " << lc << " to " << lcr << std::endl;
- if (!d_state.areEqual(llt, lcr))
- {
- Node eq = llt.eqNode(lcr);
- ei->d_normalizedLength.set(eq);
- d_im.sendInference(ant, eq, "LEN-NORM", true);
- }
- }
- }else{
- Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl;
- if( !options::stringEagerLen() ){
- Node c = utils::mkNConcat(nfi.d_nf);
- registerTerm( c, 3 );
+ Trace("strings-process-debug") << " " << exp << std::endl;
}
}
- //} else {
- // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
- //}
+
+ // if not, add the lemma
+ std::vector<Node> ant;
+ ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end());
+ ant.push_back(nfi.d_base.eqNode(lt));
+ Node lc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nf);
+ Node lcr = Rewriter::rewrite(lc);
+ Trace("strings-process-debug")
+ << "Rewrote length " << lc << " to " << lcr << std::endl;
+ if (!d_state.areEqual(llt, lcr))
+ {
+ Node eq = llt.eqNode(lcr);
+ ei->d_normalizedLength.set(eq);
+ d_im.sendInference(ant, eq, "LEN-NORM", true);
+ }
+ }
+ }
+}
+void TheoryStrings::checkRegisterTermsNormalForms()
+{
+ for (const Node& eqc : d_strings_eqc)
+ {
+ NormalForm& nfi = getNormalForm(eqc);
+ // check if there is a length term for this equivalence class
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
+ Node lt = ei ? ei->d_lengthTerm : Node::null();
+ if (lt.isNull())
+ {
+ Node c = utils::mkNConcat(nfi.d_nf);
+ registerTerm(c, 3);
}
}
}
@@ -4372,13 +4387,6 @@ void TheoryStrings::checkCardinality() {
Trace("strings-card") << "...end check cardinality" << std::endl;
}
-void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
- for( unsigned i=0; i<n.size(); i++ ){
- if( i>0 ) Trace(c) << " ++ ";
- Trace(c) << n[i];
- }
-}
-
//// Finite Model Finding
@@ -4494,10 +4502,12 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
case CHECK_EXTF_EVAL: checkExtfEval(effort); break;
case CHECK_CYCLES: checkCycles(); break;
case CHECK_FLAT_FORMS: checkFlatForms(); break;
+ case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break;
case CHECK_NORMAL_FORMS_EQ: checkNormalFormsEq(); break;
case CHECK_NORMAL_FORMS_DEQ: checkNormalFormsDeq(); break;
case CHECK_CODES: checkCodes(); break;
case CHECK_LENGTH_EQC: checkLengthsEqc(); break;
+ case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
case CHECK_EXTF_REDUCTION: checkExtfReductions(effort); break;
case CHECK_MEMBERSHIP: checkMemberships(); break;
case CHECK_CARDINALITY: checkCardinality(); break;
@@ -4561,15 +4571,20 @@ void TheoryStrings::initializeStrategy()
// do only the above inferences at standard effort, if applicable
step_end[EFFORT_STANDARD] = d_infer_steps.size() - 1;
}
+ if (!options::stringEagerLen())
+ {
+ addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
+ }
addStrategyStep(CHECK_NORMAL_FORMS_EQ);
addStrategyStep(CHECK_EXTF_EVAL, 1);
- if (!options::stringEagerLen())
+ if (!options::stringEagerLen() && options::stringLenNorm())
{
- addStrategyStep(CHECK_LENGTH_EQC);
+ addStrategyStep(CHECK_LENGTH_EQC, 0, false);
+ addStrategyStep(CHECK_REGISTER_TERMS_NF);
}
addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
addStrategyStep(CHECK_CODES);
- if (options::stringEagerLen())
+ if (options::stringEagerLen() && options::stringLenNorm())
{
addStrategyStep(CHECK_LENGTH_EQC);
}
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8e2af8434..990461027 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -68,6 +68,8 @@ enum InferStep
CHECK_CYCLES,
// check flat forms
CHECK_FLAT_FORMS,
+ // check register terms pre-normal forms
+ CHECK_REGISTER_TERMS_PRE_NF,
// check normal forms equalities
CHECK_NORMAL_FORMS_EQ,
// check normal forms disequalities
@@ -76,6 +78,8 @@ enum InferStep
CHECK_CODES,
// check lengths for equivalence classes
CHECK_LENGTH_EQC,
+ // check register terms for normal forms
+ CHECK_REGISTER_TERMS_NF,
// check extended function reductions
CHECK_EXTF_REDUCTION,
// check regular expression memberships
@@ -615,10 +619,6 @@ private:
*/
void registerTerm(Node n, int effort);
- protected:
-
- void printConcat(std::vector<Node>& n, const char* c);
-
// Symbolic Regular Expression
private:
/** regular expression solver module */
@@ -768,6 +768,12 @@ private:
* Must call checkCycles before this function in a strategy.
*/
void checkFlatForms();
+ /** check register terms pre-normal forms
+ *
+ * This calls registerTerm(n,2) on all non-congruent strings in the
+ * equality engine of this class.
+ */
+ void checkRegisterTermsPreNormalForm();
/** check normal forms equalities
*
* This applies an inference schema based on "normal forms". The normal form
@@ -845,6 +851,13 @@ private:
* shown to be helpful.
*/
void checkLengthsEqc();
+ /** check register terms for normal forms
+ *
+ * This calls registerTerm(str.++(t1, ..., tn ), 3) on the normal forms
+ * (t1, ..., tn) of all string equivalence classes { s1, ..., sm } such that
+ * there does not exist a term of the form str.len(si) in the current context.
+ */
+ void checkRegisterTermsNormalForms();
/** check extended function reductions
*
* This adds "reduction" lemmas for each active extended function in this SAT
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 03c2419c4..a564c82e1 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -225,6 +225,25 @@ void getRegexpComponents(Node r, std::vector<Node>& result)
}
}
+void printConcat(std::ostream& out, std::vector<Node>& n)
+{
+ for (unsigned i = 0, nsize = n.size(); i < nsize; i++)
+ {
+ if (i > 0)
+ {
+ out << " ++ ";
+ }
+ out << n[i];
+ }
+}
+
+void printConcatTrace(std::vector<Node>& n, const char* c)
+{
+ std::stringstream ss;
+ printConcat(ss, n);
+ Trace(c) << ss.str();
+}
+
} // namespace utils
} // namespace strings
} // namespace theory
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 2c84bd516..ccdac8edf 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -131,6 +131,11 @@ bool isSimpleRegExp(Node r);
*/
void getRegexpComponents(Node r, std::vector<Node>& result);
+/** Print the vector n as a concatentation term on output stream out */
+void printConcat(std::ostream& out, std::vector<Node>& n);
+/** Print the vector n as a concatentation term on trace given by c */
+void printConcatTrace(std::vector<Node>& n, const char* c);
+
} // namespace utils
} // namespace strings
} // namespace theory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback