summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/arith_entail.cpp8
-rw-r--r--src/theory/strings/base_solver.cpp7
-rw-r--r--src/theory/strings/infer_proof_cons.cpp11
-rw-r--r--src/theory/strings/normal_form.cpp9
-rw-r--r--src/theory/strings/term_registry.cpp10
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp10
6 files changed, 20 insertions, 35 deletions
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index cc2c7a2e6..3c58767b3 100644
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -15,6 +15,7 @@
#include "theory/strings/arith_entail.h"
#include "expr/attribute.h"
+#include "expr/node_algorithm.h"
#include "theory/arith/arith_msum.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_utils.h"
@@ -555,6 +556,8 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
{
Assert(assumption.getKind() == kind::EQUAL);
Assert(Rewriter::rewrite(assumption) == assumption);
+ Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
+ << ", strict=" << strict << std::endl;
// Find candidates variables to compute substitutions for
std::unordered_set<Node, NodeHashFunction> candVars;
@@ -615,8 +618,11 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
// Could not solve for v
return false;
}
+ Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> "
+ << solution << std::endl;
- a = a.substitute(TNode(v), TNode(solution));
+ // use capture avoiding substitution
+ a = expr::substituteCaptureAvoiding(a, v, solution);
return check(a, strict);
}
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index d33a7f902..451c01f8c 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -638,9 +638,8 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
ei->d_cardinalityLemK.set(int_k + 1);
if (!cons.isConst() || !cons.getConst<bool>())
{
- std::vector<Node> emptyVec;
d_im.sendInference(
- emptyVec, expn, cons, Inference::CARDINALITY, true);
+ expn, expn, cons, Inference::CARDINALITY, false, true);
return;
}
}
@@ -675,7 +674,7 @@ Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
}
if (!bei.d_exp.isNull())
{
- exp.push_back(bei.d_exp);
+ utils::flattenOp(AND, bei.d_exp, exp);
}
if (!bei.d_base.isNull())
{
@@ -695,7 +694,7 @@ Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp)
Assert(!bei.d_bestContent.isNull());
if (!bei.d_exp.isNull())
{
- exp.push_back(bei.d_exp);
+ utils::flattenOp(AND, bei.d_exp, exp);
}
if (!bei.d_base.isNull())
{
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index c5275cc43..66f71bf14 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -878,17 +878,6 @@ void InferProofCons::convert(Inference infer,
ps.d_rule = PfRule::STRING_TRUST;
// add to stats
d_statistics.d_inferencesNoPf << infer;
- if (options::proofNewPedantic() > 0)
- {
- std::stringstream serr;
- serr << "InferProofCons::convert: Failed " << infer
- << (isRev ? " :rev " : " ") << conc << std::endl;
- for (const Node& ec : exp)
- {
- serr << " e: " << ec << std::endl;
- }
- Unhandled() << serr.str();
- }
}
if (Trace.isOn("strings-ipc-debug"))
{
diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 372b07f56..7724b5137 100644
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -83,6 +83,7 @@ void NormalForm::addToExplanation(Node exp,
unsigned new_val,
unsigned new_rev_val)
{
+ Assert(!exp.isConst());
if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end())
{
d_exp.push_back(exp);
@@ -177,11 +178,9 @@ void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
Trace("strings-explain-prefix")
<< "Included " << curr_exp.size() << " / "
<< (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl;
- if (nfi.d_base != nfj.d_base)
- {
- Node eq = nfi.d_base.eqNode(nfj.d_base);
- curr_exp.push_back(eq);
- }
+ // add explanation for why they are equal
+ Node eq = nfi.d_base.eqNode(nfj.d_base);
+ curr_exp.push_back(eq);
}
} // namespace strings
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 76230bcff..8274b7dc0 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -462,11 +462,6 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma(
Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
<< std::endl;
Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
- if (options::proofNewPedantic() > 0)
- {
- Unhandled() << "Unhandled lemma Strings::Lemma SK-GEQ-ONE : "
- << len_geq_one << std::endl;
- }
return TrustNode::mkTrustLemma(len_geq_one, nullptr);
}
@@ -476,11 +471,6 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma(
Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
<< std::endl;
Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
- if (options::proofNewPedantic() > 0)
- {
- Unhandled() << "Unhandled lemma Strings::Lemma SK-ONE : " << len_one
- << std::endl;
- }
return TrustNode::mkTrustLemma(len_one, nullptr);
}
Assert(s == LENGTH_SPLIT);
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a8c1a6573..936f60ed2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -875,7 +875,7 @@ Node StringsPreprocess::reduce(Node t,
{
Node ltp = sc->mkTypedSkolemCached(
nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp");
- Node k = nm->mkSkolem("k", nm->integerType());
+ Node k = SkolemCache::mkIndexVar(t);
std::vector<Node> conj;
conj.push_back(nm->mkNode(GEQ, k, zero));
@@ -899,6 +899,8 @@ Node StringsPreprocess::reduce(Node t,
}
conj.push_back(nm->mkNode(ITE, ite_ch));
+ Node conjn = nm->mkNode(
+ EXISTS, nm->mkNode(BOUND_VAR_LIST, k), nm->mkNode(AND, conj));
// Intuitively, the reduction says either x and y are equal, or they have
// some (maximal) common prefix after which their characters at position k
// are distinct, and the comparison of their code matches the return value
@@ -912,13 +914,13 @@ Node StringsPreprocess::reduce(Node t,
// assert:
// IF x=y
// THEN: ltp
- // ELSE: k >= 0 AND k <= len( x ) AND k <= len( y ) AND
+ // ELSE: exists k.
+ // k >= 0 AND k <= len( x ) AND k <= len( y ) AND
// substr( x, 0, k ) = substr( y, 0, k ) AND
// IF ltp
// THEN: str.code(substr( x, k, 1 )) < str.code(substr( y, k, 1 ))
// ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 ))
- Node assert =
- nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj));
+ Node assert = nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, conjn);
asserts.push_back(assert);
// Thus, str.<=( x, y ) = ltp
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback