From 4cd199a554bd6a5247ab8143e1a3fb2d7eff88f3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Sep 2021 13:03:38 -0500 Subject: [PATCH] Add extensionality option for strings disequalities (#7229) Towards the strings array solver. Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled. --- src/options/strings_options.toml | 8 ++++ src/theory/inference_id.cpp | 2 + src/theory/inference_id.h | 4 ++ src/theory/strings/core_solver.cpp | 59 +++++++++++++++++++++++++++++- src/theory/strings/core_solver.h | 14 +++++++ src/theory/strings/skolem_cache.h | 3 ++ 6 files changed, 89 insertions(+), 1 deletion(-) diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 90e363f28..d46e5055e 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -182,3 +182,11 @@ name = "Strings Theory" type = "bool" default = "true" help = "perform eager context-dependent evaluation for applications of string kinds" + +[[option]] + name = "stringsDeqExt" + category = "regular" + long = "strings-deq-ext" + type = "bool" + default = "false" + help = "use extensionality for string disequalities" diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 7bb87819e..fce867688 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -397,6 +397,8 @@ const char* toString(InferenceId i) case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ"; case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP"; case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP"; + case InferenceId::STRINGS_DEQ_EXTENSIONALITY: + return "STRINGS_DEQ_EXTENSIONALITY"; case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY"; case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ"; case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 4c6140872..3def963ea 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -673,6 +673,10 @@ enum class InferenceId // is unknown, we apply the inference: // len(s) != len(t) V len(s) = len(t) STRINGS_DEQ_LENGTH_SP, + // Disequality extensionality + // x != y => ( seq.len(x) != seq.len(y) or + // ( seq.nth(x, d) != seq.nth(y, d) ^ 0 <= d < seq.len(x) ) ) + STRINGS_DEQ_EXTENSIONALITY, //-------------------- codes solver // str.to_code( v ) = rewrite( str.to_code(c) ) // where v is the proxy variable for c. diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 98a0e819c..2dfc73756 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -47,7 +47,8 @@ CoreSolver::CoreSolver(Env& env, d_im(im), d_termReg(tr), d_bsolver(bs), - d_nfPairs(context()) + d_nfPairs(context()), + d_extDeq(userContext()) { d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -2080,6 +2081,12 @@ void CoreSolver::processDeq(Node ni, Node nj) return; } + if (options::stringsDeqExt()) + { + processDeqExtensionality(ni, nj); + return; + } + nfi = nfni.d_nf; nfj = nfnj.d_nf; @@ -2441,6 +2448,56 @@ bool CoreSolver::processSimpleDeq(std::vector& nfi, return false; } +void CoreSolver::processDeqExtensionality(Node n1, Node n2) +{ + // hash based on equality + Node eq = n1 < n2 ? n1.eqNode(n2) : n2.eqNode(n1); + NodeSet::const_iterator it = d_extDeq.find(eq); + if (it != d_extDeq.end()) + { + // already processed + return; + } + d_extDeq.insert(eq); + + NodeManager* nm = NodeManager::currentNM(); + SkolemCache* sc = d_termReg.getSkolemCache(); + TypeNode intType = nm->integerType(); + Node k = sc->mkTypedSkolemCached( + intType, n1, n2, SkolemCache::SK_DEQ_DIFF, "diff"); + Node deq = eq.negate(); + Node ss1, ss2; + if (n1.getType().isString()) + { + // substring of length 1 + ss1 = nm->mkNode(STRING_SUBSTR, n1, k, d_one); + ss2 = nm->mkNode(STRING_SUBSTR, n2, k, d_one); + } + else + { + // as an optimization, for sequences, use seq.nth + ss1 = nm->mkNode(SEQ_NTH, n1, k); + ss2 = nm->mkNode(SEQ_NTH, n2, k); + } + // disequality between nth/substr + Node conc1 = ss1.eqNode(ss2).negate(); + + // The skolem k is in the bounds of at least + // one string/sequence + Node len1 = nm->mkNode(STRING_LENGTH, n1); + Node len2 = nm->mkNode(STRING_LENGTH, n2); + Node conc2 = nm->mkNode(LEQ, d_zero, k); + Node conc3 = nm->mkNode(LT, k, len1); + Node lenDeq = nm->mkNode(EQUAL, len1, len2).negate(); + + std::vector concs = {conc1, conc2, conc3}; + 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) ) ) + d_im.sendInference( + {deq}, conc, InferenceId::STRINGS_DEQ_EXTENSIONALITY, false, true); +} + void CoreSolver::addNormalFormPair( Node n1, Node n2 ){ if (n1>n2) { diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index 35d37ce12..adf17de4d 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -19,6 +19,7 @@ #ifndef CVC5__THEORY__STRINGS__CORE_SOLVER_H #define CVC5__THEORY__STRINGS__CORE_SOLVER_H +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" #include "smt/env_obj.h" @@ -81,6 +82,7 @@ class CoreSolver : protected EnvObj { friend class InferenceManager; using NodeIntMap = context::CDHashMap; + using NodeSet = context::CDHashSet; public: CoreSolver(Env& env, @@ -469,6 +471,16 @@ class CoreSolver : protected EnvObj Node nj, size_t& index, bool isRev); + /** + * Process disequality by extensionality. If necessary, this may result + * in inferences that follow from this disequality of the form: + * (not (= n1 n2)) => (not (= k1 k2)) + * where k1, k2 are either strings of length one or elements of a sequence. + * + * @param n1 The first string in the disequality + * @param n2 The second string in the disequality + */ + void processDeqExtensionality(Node n1, Node n2); //--------------------------end for checkNormalFormsDeq /** The solver state object */ @@ -522,6 +534,8 @@ class CoreSolver : protected EnvObj * the argument number of the t1 ... tn they were generated from. */ std::map > d_flat_form_index; + /** Set of equalities for which we have applied extensionality. */ + NodeSet d_extDeq; }; /* class CoreSolver */ } // namespace strings diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index f0376dbc6..dabe333ae 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -149,6 +149,9 @@ class SkolemCache // forall s, n. // k(s, n) is some undefined value of sort U SK_NTH, + // Diff index for disequalities + // a != b => substr(a,k,1) != substr(b,k,1) + SK_DEQ_DIFF }; /** * Returns a skolem of type string that is cached for (a,b,id) and has -- 2.30.2