void CoreSolver::processDeq(Node ni, Node nj)
{
- // If using the sequence update solver, we always apply extensionality.
- // This is required for model soundness currently, although we could
- // investigate determining cases where the disequality is already
- // satisfied (for optimization).
- if (options().strings.seqArray != options::SeqArrayMode::NONE)
- {
- processDeqExtensionality(ni, nj);
- return;
- }
NodeManager* nm = NodeManager::currentNM();
NormalForm& nfni = getNormalForm(ni);
NormalForm& nfnj = getNormalForm(nj);
return;
}
- if (options().strings.stringsDeqExt)
- {
- processDeqExtensionality(ni, nj);
- return;
- }
-
nfi = nfni.d_nf;
nfj = nfnj.d_nf;
Node conc = nm->mkNode(OR, lenDeq, nm->mkAnd(concs));
// A != B => ( seq.len(A) != seq.len(B) or
// ( seq.nth(A, d) != seq.nth(B, d) ^ 0 <= d < seq.len(A) ) )
+ // Note that we take A != B verbatim, and do not explain it.
d_im.sendInference(
- {deq}, conc, InferenceId::STRINGS_DEQ_EXTENSIONALITY, false, true);
+ {deq}, {deq}, conc, InferenceId::STRINGS_DEQ_EXTENSIONALITY, false, true);
}
void CoreSolver::addNormalFormPair( Node n1, Node n2 ){
const context::CDList<Node>& deqs = d_state.getDisequalityList();
NodeManager* nm = NodeManager::currentNM();
+ Trace("str-deq") << "Process disequalites..." << std::endl;
+ std::vector<Node> relevantDeqs;
//for each pair of disequal strings, must determine whether their lengths are equal or disequal
for (const Node& eq : deqs)
{
+ Trace("str-deq") << "- disequality " << eq << std::endl;
Node n[2];
for( unsigned i=0; i<2; i++ ){
n[i] = ee->getRepresentative( eq[i] );
lt[i] = nm->mkNode(STRING_LENGTH, eq[i]);
}
}
- if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1]))
+ if (d_state.areEqual(lt[0], lt[1]))
+ {
+ // if they have equal lengths, we must process the disequality below
+ relevantDeqs.push_back(eq);
+ Trace("str-deq") << "...relevant" << std::endl;
+ }
+ else if (!d_state.areDisequal(lt[0], lt[1]))
{
d_im.sendSplit(lt[0], lt[1], InferenceId::STRINGS_DEQ_LENGTH_SP);
+ Trace("str-deq") << "...split" << std::endl;
+ }
+ else
+ {
+ Trace("str-deq") << "...disequal length" << std::endl;
}
}
+ else
+ {
+ Trace("str-deq") << "...congruent" << std::endl;
+ }
}
if (d_im.hasProcessed())
// added splitting lemma above
return;
}
- // otherwise, look at pairs of equivalence classes with equal lengths
- std::map<TypeNode, std::vector<std::vector<Node> > > colsT;
- std::map<TypeNode, std::vector<Node> > ltsT;
- d_state.separateByLength(d_strings_eqc, colsT, ltsT);
- for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& ct : colsT)
+ for (const Node& eq : relevantDeqs)
{
- std::vector<std::vector<Node> >& cols = ct.second;
- for( unsigned i=0; i<cols.size(); i++ ){
- if (cols[i].size() > 1 && !d_im.hasPendingLemma())
- {
- if (Trace.isOn("strings-solve"))
- {
- Trace("strings-solve") << "- Verify disequalities are processed for "
- << cols[i][0] << ", normal form : ";
- utils::printConcatTrace(getNormalForm(cols[i][0]).d_nf, "strings-solve");
- Trace("strings-solve")
- << "... #eql = " << cols[i].size() << std::endl;
- }
- //must ensure that normal forms are disequal
- for( unsigned j=0; j<cols[i].size(); j++ ){
- for( unsigned k=(j+1); k<cols[i].size(); k++ ){
- //for strings that are disequal, but have the same length
- if (cols[i][j].isConst() && cols[i][k].isConst())
- {
- // if both are constants, they should be distinct, and its trivial
- Assert(cols[i][j] != cols[i][k]);
- }
- else if (d_state.areDisequal(cols[i][j], cols[i][k]))
- {
- Assert(!d_state.isInConflict());
- if (Trace.isOn("strings-solve"))
- {
- Trace("strings-solve") << "- Compare " << cols[i][j] << ", nf ";
- utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf,
- "strings-solve");
- Trace("strings-solve") << " against " << cols[i][k] << ", nf ";
- utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf,
- "strings-solve");
- Trace("strings-solve") << "..." << std::endl;
- }
- processDeq(cols[i][j], cols[i][k]);
- if (d_im.hasProcessed())
- {
- return;
- }
- }
- }
- }
- }
+ Assert(!d_state.isInConflict());
+ // If using the sequence update solver, we always apply extensionality.
+ // This is required for model soundness currently, although we could
+ // investigate determining cases where the disequality is already
+ // satisfied (for optimization).
+ if (options().strings.stringsDeqExt
+ || options().strings.seqArray != options::SeqArrayMode::NONE)
+ {
+ processDeqExtensionality(eq[0], eq[1]);
+ continue;
+ }
+ // the method below requires representatives
+ Node n[2];
+ for (size_t i = 0; i < 2; i++)
+ {
+ n[i] = ee->getRepresentative(eq[i]);
+ }
+ if (Trace.isOn("strings-solve"))
+ {
+ Trace("strings-solve") << "- Compare " << n[0] << ", nf ";
+ utils::printConcatTrace(getNormalForm(n[0]).d_nf, "strings-solve");
+ Trace("strings-solve") << " against " << n[1] << ", nf ";
+ utils::printConcatTrace(getNormalForm(n[1]).d_nf, "strings-solve");
+ Trace("strings-solve") << "..." << std::endl;
+ }
+ processDeq(n[0], n[1]);
+ if (d_im.hasProcessed())
+ {
+ return;
}
}
}
bool TheoryStrings::preNotifyFact(
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
- // this is only required for internal facts, others are already registered
- if (isInternal && atom.getKind() == EQUAL)
+ if (atom.getKind() == EQUAL)
{
- // We must ensure these terms are registered. We register eagerly here for
- // performance reasons. Alternatively, terms could be registered at full
- // effort in e.g. BaseSolver::init.
- for (const Node& t : atom)
+ // this is only required for internal facts, others are already registered
+ if (isInternal)
+ {
+ // We must ensure these terms are registered. We register eagerly here for
+ // performance reasons. Alternatively, terms could be registered at full
+ // effort in e.g. BaseSolver::init.
+ for (const Node& t : atom)
+ {
+ d_termReg.registerTerm(t, 0);
+ }
+ }
+ // store disequalities between strings that occur as literals
+ if (!pol && atom[0].getType().isStringLike())
{
- d_termReg.registerTerm(t, 0);
+ d_state.addDisequality(atom[0], atom[1]);
}
}
return false;
}
}
-void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
-{
- if (t1.getType().isStringLike())
- {
- // store disequalities between strings, may need to check if their lengths
- // are equal/disequal
- d_state.addDisequality(t1, t2);
- }
-}
-
void TheoryStrings::addCarePairs(TNodeTrie* t1,
TNodeTrie* t2,
unsigned arity,
projects / cvc5.git / commitdiff