From 7225f8f14ea0de0eca4c49ec3a2616196074d4d3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 May 2020 10:20:34 -0500 Subject: Normal form equality conflicts and uniqueness check (#4497) This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false. It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting. --- src/theory/strings/core_solver.cpp | 164 +++++++++++++++------ src/theory/strings/core_solver.h | 6 +- src/theory/strings/infer_info.cpp | 1 + src/theory/strings/infer_info.h | 4 + test/regress/CMakeLists.txt | 1 + .../regress0/strings/quad-028-2-2-unsat.smt2 | 21 +++ 6 files changed, 148 insertions(+), 49 deletions(-) create mode 100644 test/regress/regress0/strings/quad-028-2-2-unsat.smt2 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& 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 pinfer; + // compute normal forms that are effectively unique + std::unordered_map nfCache; + std::vector 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& normal_forms, - TypeNode stype) -{ - //the possible inferences - std::vector pinfer; - // loop over all pairs - for(unsigned i=0; i& ni : nfCache) + { + for (const std::pair& 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 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& normal_forms, TypeNode stype); + void processNEqc(Node eqc, + std::vector& 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) -- cgit v1.2.3