From 6476c8c75ed7fd584b5afa658dd2c8ba277c59e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 6 Nov 2020 13:47:22 -0600 Subject: (proof-new) Miscellaneous changes to strings for proofs (#5362) This includes all minor remaining changes from proof-new for strings that were not merged to master. This includes mostly minor changes to make proofs pass, including reordering assertions. It also removes some non-standard pedantic checks as these are now subsumed by standard ones. It also makes the strings rewriter slightly more safe when checking arithmetic entailment under assumptions. This code used substitution, which was not safe when quantifiers were involved. This is replaced by capture avoiding substitution here. --- src/theory/strings/term_registry.cpp | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'src/theory/strings/term_registry.cpp') 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); -- cgit v1.2.3