summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/core_solver.cpp164
-rw-r--r--src/theory/strings/core_solver.h6
-rw-r--r--src/theory/strings/infer_info.cpp1
-rw-r--r--src/theory/strings/infer_info.h4
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/strings/quad-028-2-2-unsat.smt221
6 files changed, 148 insertions, 49 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 9989c89f4..aca43e8c8 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -618,7 +618,7 @@ void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype)
return;
}
// process the normal forms
- processNEqc(normal_forms, stype);
+ processNEqc(eqc, normal_forms, stype);
if (d_im.hasProcessed())
{
return;
@@ -879,81 +879,151 @@ void CoreSolver::getNormalForms(Node eqc,
}
}
Trace("strings-solve") << std::endl;
-
}
} else {
Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
}
-
- //if equivalence class is constant, approximate as containment, infer conflicts
- Node c = d_bsolver.getConstantEqc( eqc );
- if( !c.isNull() ){
- Trace("strings-solve") << "Eqc is constant " << c << std::endl;
- for (unsigned i = 0, size = normal_forms.size(); i < size; i++)
+ }
+}
+
+void CoreSolver::processNEqc(Node eqc,
+ std::vector<NormalForm>& normal_forms,
+ TypeNode stype)
+{
+ if (normal_forms.size() <= 1)
+ {
+ return;
+ }
+ // if equivalence class is constant, approximate as containment, infer
+ // conflicts
+ Node c = d_bsolver.getConstantEqc(eqc);
+ // the possible inferences
+ std::vector<CoreInferInfo> pinfer;
+ // compute normal forms that are effectively unique
+ std::unordered_map<Node, size_t, NodeHashFunction> nfCache;
+ std::vector<size_t> nfIndices;
+ bool hasConstIndex = false;
+ for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++)
+ {
+ NormalForm& nfi = normal_forms[i];
+ Node ni = utils::mkNConcat(nfi.d_nf, stype);
+ if (nfCache.find(ni) == nfCache.end())
+ {
+ // If the equivalence class is entailed to be constant, check
+ // if the normal form cannot be contained in that constant.
+ if (!c.isNull())
{
- NormalForm& nf = normal_forms[i];
int firstc, lastc;
- if (!StringsEntail::canConstantContainList(c, nf.d_nf, firstc, lastc))
+ if (!StringsEntail::canConstantContainList(c, nfi.d_nf, firstc, lastc))
{
- Node n = nf.d_base;
+ Node n = nfi.d_base;
//conflict
Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl;
- //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
+ // conflict, explanation is:
+ // n = base ^ base = c ^ relevant porition of ( n = N[n] )
std::vector< Node > exp;
d_bsolver.explainConstantEqc(n,eqc,exp);
// Notice although not implemented, this can be minimized based on
// firstc/lastc, normal_forms_exp_depend.
- exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
- Node conc = d_false;
- d_im.sendInference(exp, conc, Inference::N_NCTN);
+ exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
+ d_im.sendInference(exp, d_false, Inference::N_NCTN);
+ return;
}
}
+
+ nfCache[ni] = i;
+ if (ni.isConst())
+ {
+ hasConstIndex = true;
+ nfIndices.insert(nfIndices.begin(), i);
+ }
+ else
+ {
+ nfIndices.push_back(i);
+ }
}
}
-}
+ size_t nnfs = nfIndices.size();
+ Trace("strings-solve") << "CoreSolver::processNEqc: " << nnfs << "/"
+ << normal_forms.size() << " normal forms are unique."
+ << std::endl;
-void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
- TypeNode stype)
-{
- //the possible inferences
- std::vector<CoreInferInfo> pinfer;
- // loop over all pairs
- for(unsigned i=0; i<normal_forms.size()-1; i++) {
+ // loop over all pairs
+ for (unsigned i = 0; i < nnfs - 1; i++)
+ {
//unify each normalform[j] with normal_forms[i]
- for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
- NormalForm& nfi = normal_forms[i];
- NormalForm& nfj = normal_forms[j];
+ for (unsigned j = i + 1; j < nnfs; j++)
+ {
+ NormalForm& nfi = normal_forms[nfIndices[i]];
+ NormalForm& nfj = normal_forms[nfIndices[j]];
//ensure that normal_forms[i] and normal_forms[j] are the same modulo equality, add to pinfer if not
Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
if (isNormalFormPair(nfi.d_base, nfj.d_base))
{
Trace("strings-solve") << "Strings: Already cached." << std::endl;
- }else{
- //process the reverse direction first (check for easy conflicts and inferences)
- unsigned rindex = 0;
- nfi.reverse();
- nfj.reverse();
- processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
- nfi.reverse();
- nfj.reverse();
- if (d_im.hasProcessed())
- {
- return;
- }
- //AJR: for less aggressive endpoint inference
- //rindex = 0;
+ continue;
+ }
+ // process the reverse direction first (check for easy conflicts and
+ // inferences)
+ unsigned rindex = 0;
+ nfi.reverse();
+ nfj.reverse();
+ processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
+ nfi.reverse();
+ nfj.reverse();
+ if (d_im.hasProcessed())
+ {
+ break;
+ }
+ // AJR: for less aggressive endpoint inference
+ // rindex = 0;
- unsigned index = 0;
- processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
- if (d_im.hasProcessed())
- {
- return;
- }
+ unsigned index = 0;
+ processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
+ if (d_im.hasProcessed())
+ {
+ break;
+ }
+ }
+ if (hasConstIndex || d_im.hasProcessed())
+ {
+ break;
+ }
+ }
+ if (d_state.isInConflict())
+ {
+ // conflict, we are done
+ return;
+ }
+ // Go back and check for normal form equality conflicts. These take
+ // precedence over any facts and lemmas.
+ for (const std::pair<const Node, size_t>& ni : nfCache)
+ {
+ for (const std::pair<const Node, size_t>& nj : nfCache)
+ {
+ if (ni.first >= nj.first)
+ {
+ // avoid duplicate comparisons
+ continue;
+ }
+ Node eq = ni.first.eqNode(nj.first);
+ eq = Rewriter::rewrite(eq);
+ if (eq == d_false)
+ {
+ std::vector<Node> exp;
+ NormalForm& nfi = normal_forms[ni.second];
+ NormalForm& nfj = normal_forms[nj.second];
+ exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
+ exp.insert(exp.end(), nfj.d_exp.begin(), nfj.d_exp.end());
+ exp.push_back(nfi.d_base.eqNode(nfj.d_base));
+ d_im.sendInference(exp, d_false, Inference::N_EQ_CONF);
+ return;
}
}
}
- if (pinfer.empty())
+ if (d_im.hasProcessed() || pinfer.empty())
{
+ // either already sent a lemma or fact, or there are no possible inferences
return;
}
// now, determine which of the possible inferences we want to add
diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
index 4328b8462..029f1c850 100644
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -275,7 +275,7 @@ class CoreSolver
TypeNode stype);
/** process normalize equivalence class
*
- * This is called when an equivalence class contains a set of terms that
+ * This is called when an equivalence class eqc contains a set of terms that
* have normal forms given by the argument normal_forms. It either
* verifies that all normal forms in this vector are identical, or otherwise
* adds a conflict, lemma, or inference via the sendInference method.
@@ -288,7 +288,9 @@ class CoreSolver
*
* stype is the string-like type of the equivalence class we are processing.
*/
- void processNEqc(std::vector<NormalForm>& normal_forms, TypeNode stype);
+ void processNEqc(Node eqc,
+ std::vector<NormalForm>& normal_forms,
+ TypeNode stype);
/** process simple normal equality
*
* This method is called when two equal terms have normal forms nfi and nfj.
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 9c4ebafa1..e26a49e4e 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -35,6 +35,7 @@ const char* toString(Inference i)
case Inference::F_ENDPOINT_EMP: return "F_ENDPOINT_EMP";
case Inference::F_ENDPOINT_EQ: return "F_ENDPOINT_EQ";
case Inference::F_NCTN: return "F_NCTN";
+ case Inference::N_EQ_CONF: return "N_EQ_CONF";
case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP";
case Inference::N_UNIFY: return "N_UNIFY";
case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ";
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index fca528d1b..5aecf52cb 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -92,6 +92,10 @@ enum class Inference : uint32_t
// Flat form not contained
// x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
F_NCTN,
+ // Normal form equality conflict
+ // x = N[x] ^ y = N[y] ^ x=y => false
+ // where Rewriter::rewrite(N[x]=N[y]) = false.
+ N_EQ_CONF,
// Given two normal forms, infers that the remainder one of them has to be
// empty. For example:
// If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d5174af5e..ea98cf819 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -961,6 +961,7 @@ set(regress_0_tests
regress0/strings/norn-31.smt2
regress0/strings/norn-simp-rew.smt2
regress0/strings/parser-syms.cvc
+ regress0/strings/quad-028-2-2-unsat.smt2
regress0/strings/re.all.smt2
regress0/strings/re-syntax.smt2
regress0/strings/re_diff.smt2
diff --git a/test/regress/regress0/strings/quad-028-2-2-unsat.smt2 b/test/regress/regress0/strings/quad-028-2-2-unsat.smt2
new file mode 100644
index 000000000..2ffe8a7a7
--- /dev/null
+++ b/test/regress/regress0/strings/quad-028-2-2-unsat.smt2
@@ -0,0 +1,21 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Quang Loc Le
+Generated on: 2018-10-22
+Application: Word equations in a decidable fragment
+Target solver: Kepler_22
+Publication: "A decision procedure for string logic with quadratic equations, regular expressions and length constraints" by Q.L. Le and M. He, APLAS 2018.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun x1 () String )
+(declare-fun x2 () String )
+(declare-fun z () String )
+(declare-fun t () String )
+(assert ( =( str.++( str.++( str.++ x1 "abc" ) x2 ) z ) ( str.++( str.++( str.++ x2 "bab" ) x1 ) t ) ) )
+(check-sat)
+
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback