1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
/********************* */
/*! \file projections.cpp
** \verbatim
** Top contributors (to current version):
** Gereon Kremer
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implements utilities for CAD projection operators.
**
** Implements utilities for CAD projection operators.
**/
#include "theory/arith/nl/cad/projections.h"
#ifdef CVC4_POLY_IMP
#include "base/check.h"
namespace CVC4 {
namespace theory {
namespace arith {
namespace nl {
namespace cad {
using namespace poly;
void PolyVector::add(const poly::Polynomial& poly, bool assertMain)
{
for (const auto& p : poly::square_free_factors(poly))
{
if (poly::is_constant(p)) continue;
if (assertMain)
{
Assert(main_variable(poly) == main_variable(p));
}
std::vector<poly::Polynomial>::emplace_back(p);
}
}
void PolyVector::reduce()
{
std::sort(begin(), end());
erase(std::unique(begin(), end()), end());
}
void PolyVector::makeFinestSquareFreeBasis()
{
for (std::size_t i = 0, n = size(); i < n; ++i)
{
for (std::size_t j = i + 1; j < n; ++j)
{
Polynomial g = gcd((*this)[i], (*this)[j]);
if (!is_constant(g))
{
(*this)[i] = div((*this)[i], g);
(*this)[j] = div((*this)[j], g);
add(g);
}
}
}
auto it = std::remove_if(
begin(), end(), [](const Polynomial& p) { return is_constant(p); });
erase(it, end());
reduce();
}
void PolyVector::pushDownPolys(PolyVector& down, poly::Variable var)
{
auto it =
std::remove_if(begin(), end(), [&down, &var](const poly::Polynomial& p) {
if (main_variable(p) == var) return false;
down.add(p);
return true;
});
erase(it, end());
}
PolyVector projection_mccallum(const std::vector<Polynomial>& polys)
{
PolyVector res;
for (const auto& p : polys)
{
for (const auto& coeff : coefficients(p))
{
res.add(coeff);
}
res.add(discriminant(p));
}
for (std::size_t i = 0, n = polys.size(); i < n; ++i)
{
for (std::size_t j = i + 1; j < n; ++j)
{
res.add(resultant(polys[i], polys[j]));
}
}
res.reduce();
return res;
}
} // namespace cad
} // namespace nl
} // namespace arith
} // namespace theory
} // namespace CVC4
#endif
|
