From 5b05e467710e07bbfa27d4a2417ec27b336c245d Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 18 Dec 2020 07:01:58 -0800 Subject: [PATCH] Bugfix: proofs for props of non-normal arith lits (#5702) Arith has a normal form for literals, which the rewriter computes. Nonetheless, arith sometimes gets (and ultimately propagates) non-normal literals. It normalizes them internally and goes about its business. However, when asked for an explanation, it must prove the non-normal literal, rather than the normal one. Also includes a regression for the bug, courtesy of Andy. Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu --- src/theory/arith/constraint.cpp | 13 ++++++++----- src/theory/arith/constraint.h | 11 ++++++++++- src/theory/arith/theory_arith_private.cpp | 4 ++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/arith/non-normal.smt2 | 16 ++++++++++++++++ 5 files changed, 37 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/arith/non-normal.smt2 diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 03d9c50e9..c1db8e55a 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1507,7 +1507,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){ return externalExplain(b, AssertionOrderSentinel); } -TrustNode Constraint::externalExplainForPropagation() const +TrustNode Constraint::externalExplainForPropagation(TNode lit) const { Assert(hasProof()); Assert(!isAssumption()); @@ -1517,6 +1517,9 @@ TrustNode Constraint::externalExplainForPropagation() const Node n = safeConstructNary(nb); if (d_database->isProofEnabled()) { + // Check that the literal we're explaining via this constraint actually + // matches the constraint's canonical literal. + Assert(Rewriter::rewrite(lit) == getLiteral()); std::vector assumptions; if (n.getKind() == Kind::AND) { @@ -1526,18 +1529,18 @@ TrustNode Constraint::externalExplainForPropagation() const { assumptions.push_back(n); } - if (getProofLiteral() != getLiteral()) + if (getProofLiteral() != lit) { pfFromAssumptions = d_database->d_pnm->mkNode( - PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {getLiteral()}); + PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {lit}); } auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions); return d_database->d_pfGen->mkTrustedPropagation( - getLiteral(), safeConstructNary(Kind::AND, assumptions), pf); + lit, safeConstructNary(Kind::AND, assumptions), pf); } else { - return TrustNode::mkTrustPropExp(getLiteral(), n); + return TrustNode::mkTrustPropExp(lit, n); } } diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 952879182..70b2cad20 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -601,8 +601,17 @@ class Constraint { * hasEqualityEngineProof(). * * All return conjuncts were asserted before this constraint. + * + * Requires the given node to rewrite to the canonical literal for this + * constraint. + * + * @params n the literal to prove + * n must rewrite to the constraint's canonical literal + * + * @returns a trust node of the form: + * (=> explanation n) */ - TrustNode externalExplainForPropagation() const; + TrustNode externalExplainForPropagation(TNode n) const; /** * Explain the constraint and its negation in terms of assertions. diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ce0445d1f..d1068c6ac 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3848,12 +3848,12 @@ TrustNode TheoryArithPrivate::explain(TNode n) TrustNode exp; if(c != NullConstraint){ Assert(!c->isAssumption()); - exp = c->externalExplainForPropagation(); + exp = c->externalExplainForPropagation(n); Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl; }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){ c = d_assertionsThatDoNotMatchTheirLiterals[n]; if(!c->isAssumption()){ - exp = c->externalExplainForPropagation(); + exp = c->externalExplainForPropagation(n); Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl; }else{ Debug("arith::explain") << "this is a strange mismatch" << n << endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d185049e0..2c480da3a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -68,6 +68,7 @@ set(regress_0_tests regress0/arith/mod-simp.smt2 regress0/arith/mod.01.smt2 regress0/arith/mult.01.smt2 + regress0/arith/non-normal.smt2 regress0/arr1.smt2 regress0/arr1.smtv1.smt2 regress0/arr2.smtv1.smt2 diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2 new file mode 100644 index 000000000..389bd6d2b --- /dev/null +++ b/test/regress/regress0/arith/non-normal.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --proof-new-eager-checking +; EXPECT: sat +(set-logic QF_UFLRA) +(declare-fun v1 () Real) +(declare-fun v2 () Real) +(declare-fun f1 (Real) Real) +(declare-fun f0 (Real Real) Real) +(declare-fun p0 (Real Real) Bool) +(assert +(ite + (or (= 0.0 v2) (> 1 (ite (< (- (- v1)) 1.0) 1.0 (ite (p0 0.0 v1) 0.0 1.0)))) + (= 0.0 (ite (= 1.0 (f1 0.0)) 0.0 (f1 1.0))) + (and + (= 1.0 (ite (= 0.0 (f1 1.0)) v2 (- 1.0))) + (=> (not (p0 0.0 (- (- (- v2))))) (= 1.0 (ite (= 1.0 v2) (ite (= 0 (f0 0.0 1.0)) 1.0 (f0 0.0 (- v2 (- v1)))) 0.0)))))) +(check-sat) -- 2.30.2