projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c7c5e4a
)
Preserve model values for exact sine points (#8188)
author
Andrew Reynolds
<andrew.j.reynolds@gmail.com>
Mon, 28 Feb 2022 22:04:16 +0000
(16:04 -0600)
committer
GitHub
<noreply@github.com>
Mon, 28 Feb 2022 22:04:16 +0000
(16:04 -0600)
Fixes #8182.
src/theory/arith/nl/transcendental/sine_solver.cpp
patch
|
blob
|
history
src/theory/arith/nl/transcendental/sine_solver.h
patch
|
blob
|
history
src/theory/arith/nl/transcendental/transcendental_solver.cpp
patch
|
blob
|
history
test/regress/CMakeLists.txt
patch
|
blob
|
history
test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
[new file with mode: 0644]
patch
|
blob
test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2
[new file with mode: 0644]
patch
|
blob
diff --git
a/src/theory/arith/nl/transcendental/sine_solver.cpp
b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 245665d68dbd8c1a2a991869de9f44891266ed24..8ab36368798ebfbef906bddc13c73f0bf9b9c5fe 100644
(file)
--- a/
src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/
src/theory/arith/nl/transcendental/sine_solver.cpp
@@
-595,6
+595,13
@@
std::pair<Node, Node> SineSolver::getSecantBounds(TNode e,
return bounds;
}
return bounds;
}
+bool SineSolver::hasExactModelValue(TNode n) const
+{
+ Assert(n.getKind() == SINE);
+ Node mv = d_data->d_model.computeAbstractModelValue(n[0]);
+ return d_mpointsSine.find(mv) != d_mpointsSine.end();
+}
+
} // namespace transcendental
} // namespace nl
} // namespace arith
} // namespace transcendental
} // namespace nl
} // namespace arith
diff --git
a/src/theory/arith/nl/transcendental/sine_solver.h
b/src/theory/arith/nl/transcendental/sine_solver.h
index 88ca1b71e1f9a16738baa03f4074ddc90cd01b38..a0589d10898316e4ddc030546c0f413b1a8c9c3b 100644
(file)
--- a/
src/theory/arith/nl/transcendental/sine_solver.h
+++ b/
src/theory/arith/nl/transcendental/sine_solver.h
@@
-108,6
+108,12
@@
class SineSolver : protected EnvObj
unsigned actual_d,
int region);
unsigned actual_d,
int region);
+ /**
+ * Does n of the form sin(x) have an exact model value? This is true if
+ * the model value of x is in the domain of d_mpointsSine.
+ */
+ bool hasExactModelValue(TNode n) const;
+
private:
std::pair<Node, Node> getSecantBounds(TNode e,
TNode c,
private:
std::pair<Node, Node> getSecantBounds(TNode e,
TNode c,
diff --git
a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index ac94be864af1d6df426b96ad05a54813342bd707..262298772cf617836679ef99e4d85a2407a657b5 100644
(file)
--- a/
src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/
src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@
-457,11
+457,18
@@
void TranscendentalSolver::postProcessModel(std::map<Node, Node>& arithModel,
std::unordered_map<Node, Node> trReps;
for (const Node& n : termSet)
{
std::unordered_map<Node, Node> trReps;
for (const Node& n : termSet)
{
- if (isTranscendentalKind(n.getKind()))
+ Kind k = n.getKind();
+ if (!isTranscendentalKind(n.getKind()))
{
{
- Node r = d_astate.getRepresentative(n);
- trReps[r] = n;
+ continue;
+ }
+ // it might have an exact value, in which case there is nothing to do
+ if (k == SINE && d_sineSlv.hasExactModelValue(n))
+ {
+ continue;
}
}
+ Node r = d_astate.getRepresentative(n);
+ trReps[r] = n;
}
if (trReps.empty())
{
}
if (trReps.empty())
{
diff --git
a/test/regress/CMakeLists.txt
b/test/regress/CMakeLists.txt
index 393e191dab80f1e8de2f5eaf0e064452e07a55f4..0d646392fbda78b2378b70ac8d8216c76e817839 100644
(file)
--- a/
test/regress/CMakeLists.txt
+++ b/
test/regress/CMakeLists.txt
@@
-792,6
+792,8
@@
set(regress_0_tests
regress0/nl/nta/issue7938-tf-model.smt2
regress0/nl/nta/issue8147-unc-model.smt2
regress0/nl/nta/issue8160-model-purify.smt2
regress0/nl/nta/issue7938-tf-model.smt2
regress0/nl/nta/issue8147-unc-model.smt2
regress0/nl/nta/issue8160-model-purify.smt2
+ regress0/nl/nta/issue8182-exact-mv-keep.smt2
+ regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
regress0/nl/nta/proj-issue460-pi-value.smt2
regress0/nl/nta/real-pi.smt2
regress0/nl/nta/sin-sym.smt2
regress0/nl/nta/proj-issue460-pi-value.smt2
regress0/nl/nta/real-pi.smt2
regress0/nl/nta/sin-sym.smt2
diff --git a/test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
b/test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
new file mode 100644
(file)
index 0000000..
13088e5
--- /dev/null
+++ b/
test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
@@ -0,0
+1,8
@@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= a (* b (+ (sin a) (/ 1 a)))))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2
b/test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2
new file mode 100644
(file)
index 0000000..
0d71007
--- /dev/null
+++ b/
test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2
@@ -0,0
+1,7
@@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun v () Real)
+(assert (forall ((V Real)) (> 0 (/ 0.0 v))))
+(assert (= 0.0 (* (sin v) (sin 1.0))))
+(check-sat)