ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity

[Arith] Support integer in inverse functions (#9134)

Browse Source 
Fixes #9131.

We eliminate inverse functions such as arcsin(x) by replacing them with a fresh skolem sk and adding a range lemma and an equality x = sin(sk). However, x may be an integer term, so we have to be careful about types when constructing the equality. This commit fixes the issue by using the existing helper method mkEquality().

Additionally, the internal type checking example led to an assertion failure decisionLevel() == 0, because the decision trail was not reset after the type exception was thrown. This commit makes the code in SmtDriver more robust to avoid such secondary assertion failures.
This commit is contained in:
Andres Noetzli
2022-09-16 08:00:30 -07:00
committed by GitHub
parent 0070d0ffe2
commit c4be9f5577
4 changed files with 33 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/smt/smt_driver.cpp
View File

@@ -95,6 +95,16 @@ Result SmtDriver::checkSat(const std::vector<Node>& assumptions)
d_smt.getPropEngine()->resetTrail();
throw;
}
catch (const TypeCheckingExceptionPrivate& e)
{
// The exception has been throw during solving, backtrack to reset the
// decision level to the level expected after this method finishes. Note
// that we do not expect type checking exceptions to occur during solving.
// However, if they occur due to a bug, we don't want to additionally cause
// an assertion failure.
d_smt.getPropEngine()->resetTrail();
throw;
}
return result;
}

23
src/theory/arith/operator_elim.cpp
View File

@@ -368,18 +368,19 @@ Node OperatorElim::eliminateOperators(Node node,
}
}
Kind rk =
k == ARCSINE
? SINE
: (k == ARCCOSINE
? COSINE
: (k == ARCTANGENT
? TANGENT
: (k == ARCCOSECANT
? COSECANT
: (k == ARCSECANT ? SECANT : COTANGENT))));
Kind rk;
switch (k)
{
case ARCSINE: rk = SINE; break;
case ARCCOSINE: rk = COSINE; break;
case ARCTANGENT: rk = TANGENT; break;
case ARCCOSECANT: rk = COSECANT; break;
case ARCSECANT: rk = SECANT; break;
case ARCCOTANGENT: rk = COTANGENT; break;
default: Unreachable() << "Unexpected kind " << k;
}
Node invTerm = nm->mkNode(rk, var);
lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
lem = nm->mkNode(AND, rlem, mkEquality(invTerm, node[0]));
if (!cond.isNull())
{
lem = nm->mkNode(IMPLIES, cond, lem);

1
test/regress/cli/CMakeLists.txt
View File

@@ -71,6 +71,7 @@ set(regress_0_tests
regress0/arith/issue8905-pi-to-int.smt2
regress0/arith/issue8872-msum-types.smt2
regress0/arith/issue8872-2-msum-types.smt2
regress0/arith/issue9131-inverse-of-int.smt2
regress0/arith/ite-lift.smt2
regress0/arith/leq.01.smtv1.smt2
regress0/arith/miplib.cvc.smt2

10
test/regress/cli/regress0/arith/issue9131-inverse-of-int.smt2 Normal file
View File

@@ -0,0 +1,10 @@
; COMMAND-LINE: -q
; This is a minimized version of the problem in the original issue. It
; triggered the same type checking exception before the fix (without triggering
; the secondary assertion failure of decisionLevel() == 0.
(set-logic QF_NIRAT)
(declare-const x Int)
(assert (= (to_int (arcsin x)) x))
(set-info :status sat)
(check-sat)