From 41c805583cad59bd8143737a4f3c331a40eb3212 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Mar 2023 14:22:28 -0500 Subject: [PATCH] Relax assertions in nlt proof checker (#9601) Fixes cvc5/cvc5-projects#530. --- .../arith/nl/transcendental/proof_checker.cpp | 38 +++++++++---------- .../arith/nl/transcendental/sine_solver.cpp | 1 + test/regress/cli/CMakeLists.txt | 1 + .../cli/regress1/nl/proj-issue530.smt2 | 8 ++++ 4 files changed, 29 insertions(+), 19 deletions(-) create mode 100644 test/regress/cli/regress1/nl/proj-issue530.smt2 diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index a9c0807960b..96169857b9b 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -145,7 +145,7 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 4); Assert(args[0].isConst() && args[0].getType().isInteger()); - Assert(args[1].getType().isReal()); + Assert(args[1].getType().isRealOrInt()); Assert(args[2].isConst() && args[2].getType().isRealOrInt()); Assert(args[3].isConst() && args[3].getType().isRealOrInt()); std::uint64_t d = @@ -171,7 +171,7 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 4); Assert(args[0].isConst() && args[0].getType().isInteger()); - Assert(args[1].getType().isReal()); + Assert(args[1].getType().isRealOrInt()); Assert(args[2].isConst() && args[2].getType().isRealOrInt()); Assert(args[3].isConst() && args[3].getType().isRealOrInt()); std::uint64_t d = @@ -198,7 +198,7 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(args.size() == 3); Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].isConst() && args[1].getType().isRealOrInt()); - Assert(args[2].getType().isReal()); + Assert(args[2].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node c = args[1]; @@ -218,7 +218,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 1); - Assert(args[0].getType().isReal()); + Assert(args[0].getType().isRealOrInt()); Node s = nm->mkNode(Kind::SINE, args[0]); return nm->mkNode(AND, nm->mkNode(LEQ, s, one), nm->mkNode(GEQ, s, mone)); } @@ -235,7 +235,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 1); - Assert(args[0].getType().isReal()); + Assert(args[0].getType().isRealOrInt()); Node s1 = nm->mkNode(Kind::SINE, args[0]); Node s2 = nm->mkNode(Kind::SINE, nm->mkNode(Kind::MULT, mone, args[0])); return nm->mkNode(ADD, s1, s2).eqNode(zero); @@ -244,7 +244,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 1); - Assert(args[0].getType().isReal()); + Assert(args[0].getType().isRealOrInt()); Node s = nm->mkNode(Kind::SINE, args[0]); return nm->mkNode( AND, @@ -258,7 +258,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 1); - Assert(args[0].getType().isReal()); + Assert(args[0].getType().isRealOrInt()); Node s = nm->mkNode(Kind::SINE, args[0]); return nm->mkNode( AND, @@ -274,9 +274,9 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 6); Assert(args[0].isConst() && args[0].getType().isInteger()); - Assert(args[1].getType().isReal()); - Assert(args[2].getType().isReal()); - Assert(args[3].getType().isReal()); + Assert(args[1].getType().isRealOrInt()); + Assert(args[2].getType().isRealOrInt()); + Assert(args[3].getType().isRealOrInt()); Assert(args[4].isConst() && args[4].getType().isRealOrInt()); Assert(args[5].isConst() && args[5].getType().isRealOrInt()); std::uint64_t d = @@ -304,9 +304,9 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 5); Assert(args[0].isConst() && args[0].getType().isInteger()); - Assert(args[1].getType().isReal()); - Assert(args[2].getType().isReal()); - Assert(args[3].getType().isReal()); + Assert(args[1].getType().isRealOrInt()); + Assert(args[2].getType().isRealOrInt()); + Assert(args[3].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node t = args[1]; @@ -327,9 +327,9 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 6); Assert(args[0].isConst() && args[0].getType().isInteger()); - Assert(args[1].getType().isReal()); - Assert(args[2].getType().isReal()); - Assert(args[3].getType().isReal()); + Assert(args[1].getType().isRealOrInt()); + Assert(args[2].getType().isRealOrInt()); + Assert(args[3].getType().isRealOrInt()); Assert(args[4].isConst() && args[4].getType().isRealOrInt()); Assert(args[5].isConst() && args[5].getType().isRealOrInt()); std::uint64_t d = @@ -357,9 +357,9 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 5); Assert(args[0].isConst() && args[0].getType().isInteger()); - Assert(args[1].getType().isReal()); - Assert(args[2].getType().isReal()); - Assert(args[3].getType().isReal()); + Assert(args[1].getType().isRealOrInt()); + Assert(args[2].getType().isRealOrInt()); + Assert(args[3].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node t = args[1]; diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index fe7b673a666..52f33d936de 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -225,6 +225,7 @@ void SineSolver::checkInitialRefine() // initial refinements if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end()) { + Trace("nl-ext-debug") << "Process initial refine " << t << std::endl; d_tf_initial_refine[t] = true; Assert(d_data->isPurified(t)); { diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 83da5439344..9a32259f7ef 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2255,6 +2255,7 @@ set(regress_1_tests regress1/nl/proj-issue294.smt2 regress1/nl/proj-issue297.smt2 regress1/nl/proj-issue302.smt2 + regress1/nl/proj-issue530.smt2 regress1/nl/quant-nl.smt2 regress1/nl/red-exp.smt2 regress1/nl/rewriting-sums.smt2 diff --git a/test/regress/cli/regress1/nl/proj-issue530.smt2 b/test/regress/cli/regress1/nl/proj-issue530.smt2 new file mode 100644 index 00000000000..8dbc4f747ab --- /dev/null +++ b/test/regress/cli/regress1/nl/proj-issue530.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :check-proofs true) +(set-option :proof-check eager) +(declare-const x Real) +(assert (= real.pi (/ real.pi (tan (to_real (to_int x)))))) +(assert (= 1 (to_int x))) +(check-sat)