Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.
This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.
This makes us safer in several places related to double SYMM steps.
if (isSym)
{
- d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
+ if (pgc->getRule() == PfRule::SYMM)
+ {
+ d_manager->updateNode(cur, pgc->getChildren()[0].get());
+ }
+ else
+ {
+ d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
+ }
}
else
{
if (pf == nullptr)
{
Trace("cdproof") << "...fresh make symm" << std::endl;
- std::shared_ptr<ProofNode> psym =
- d_manager->mkNode(PfRule::SYMM, pschild, args, fact);
+ std::shared_ptr<ProofNode> psym = d_manager->mkSymm(pfs, fact);
Assert(psym != nullptr);
d_nodes.insert(fact, psym);
return psym;
{
return true;
}
- else if (rule == PfRule::SYMM)
+ else if (rule != PfRule::SYMM)
{
- const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
- Assert(pc.size() == 1);
- return pc[0]->getRule() == PfRule::ASSUME;
+ return false;
}
- return false;
+ pn = ProofNodeManager::cancelDoubleSymm(pn);
+ rule = pn->getRule();
+ if (rule == PfRule::ASSUME)
+ {
+ return true;
+ }
+ else if (rule != PfRule::SYMM)
+ {
+ return false;
+ }
+ const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
+ Assert(pc.size() == 1);
+ return pc[0]->getRule() == PfRule::ASSUME;
}
bool CDProof::isSame(TNode f, TNode g)
return mkNode(PfRule::ASSUME, {}, {fact}, fact);
}
+std::shared_ptr<ProofNode> ProofNodeManager::mkSymm(
+ std::shared_ptr<ProofNode> child, Node expected)
+{
+ if (child->getRule() == PfRule::SYMM)
+ {
+ Assert(expected.isNull()
+ || child->getChildren()[0]->getResult() == expected);
+ return child->getChildren()[0];
+ }
+ return mkNode(PfRule::SYMM, {child}, {}, expected);
+}
+
std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
{
// use SYMM if possible
if (aMatch == aeqSym)
{
- updateNode(pfs.get(), PfRule::SYMM, children, {});
+ if (pfaa->getRule() == PfRule::SYMM)
+ {
+ updateNode(pfs.get(), pfaa->getChildren()[0].get());
+ }
+ else
+ {
+ updateNode(pfs.get(), PfRule::SYMM, children, {});
+ }
}
else
{
{
Assert(pn != nullptr);
Assert(pnr != nullptr);
+ if (pn == pnr)
+ {
+ // same node, no update necessary
+ return true;
+ }
if (pn->getResult() != pnr->getResult())
{
return false;
ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
std::shared_ptr<ProofNode> ProofNodeManager::clone(
- std::shared_ptr<ProofNode> pn)
+ std::shared_ptr<ProofNode> pn) const
{
const ProofNode* orig = pn.get();
std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited;
{
it = visited.find(cp.get());
Assert(it != visited.end());
- Assert(it->second != nullptr);
+ // if we encounter nullptr here, then this child is currently being
+ // traversed at a higher level, hence this corresponds to a cyclic
+ // proof.
+ if (it->second == nullptr)
+ {
+ Unreachable() << "Cyclic proof encountered when cloning a proof node";
+ }
cchildren.push_back(it->second);
}
cloned = std::make_shared<ProofNode>(
return visited[orig];
}
+ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn)
+{
+ while (pn->getRule() == PfRule::SYMM)
+ {
+ std::shared_ptr<ProofNode> pnc = pn->getChildren()[0];
+ if (pnc->getRule() == PfRule::SYMM)
+ {
+ pn = pnc->getChildren()[0].get();
+ }
+ else
+ {
+ break;
+ }
+ }
+ return pn;
+}
+
bool ProofNodeManager::updateNodeInternal(
ProofNode* pn,
PfRule id,
* @return The ASSUME proof of fact.
*/
std::shared_ptr<ProofNode> mkAssume(Node fact);
+ /**
+ * Make symm, which accounts for whether the child is already a SYMM
+ * node, in which case we return its child.
+ */
+ std::shared_ptr<ProofNode> mkSymm(std::shared_ptr<ProofNode> child,
+ Node expected = Node::null());
/**
* Make transitivity proof, where children contains one or more proofs of
* equalities that form an ordered chain. In other words, the vector children
* @param pn The proof node to clone
* @return the cloned proof node.
*/
- std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn);
+ std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn) const;
+ /**
+ * Cancel double SYMM. Returns a proof node that is not a double application
+ * of SYMM, e.g. for (SYMM (SYMM (r P))), this returns (r P) where r != SYMM.
+ */
+ static ProofNode* cancelDoubleSymm(ProofNode* pn);
private:
/** The (optional) proof checker */
regress2/strings/issue6639-replace-re-all.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
+ regress2/strings/proof-fail-083021-delta.smt2
regress2/strings/range-perf.smt2
regress2/strings/repl-repl-i-no-push.smt2
regress2/strings/repl-repl.smt2
--- /dev/null
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x Bool)
+(declare-const x1 Int)
+(declare-fun s () String)
+(assert (ite (str.prefixof "-" (str.substr s 0 1)) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) true))
+(assert (not (<= (- (str.len s) 1 (+ 1 1) 1) 3)))
+(assert (ite x true (> 1 (str.len (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (= 0 (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s 1 x1)) 1)))) true))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (not (<= (str.to_int (str.substr s 0 (+ 1 1))) 255)))
+(check-sat)
projects / cvc5.git / commitdiff