3 #include "../Formula.h"
30 template<
typename Poly>
40 subs.push_back(
to_pnf(sub, reverse_prefix, used_vars,
false));
46 subs.push_back(
to_pnf(sub, reverse_prefix, used_vars,
true));
57 sub1.push_back(
to_pnf(sub, reverse_prefix, used_vars,
true));
58 sub2.push_back(
to_pnf(sub, reverse_prefix, used_vars,
false));
62 auto lhs =
to_pnf(f, reverse_prefix, used_vars,
false);
87 if (used_vars.contains(v)) {
89 std::stringstream ss; ss << v.name() <<
"_" << new_v.id();
92 new_qvars.insert(new_v);
99 auto subres =
to_pnf(sub, reverse_prefix, used_vars, negated);
100 for (
auto v : new_qvars) {
101 if (subres.variables().find(v) != subres.variables().end()) {
102 reverse_prefix.push_back(std::make_pair(q, v));
113 if (used_vars.contains(v)) {
115 std::stringstream ss; ss << v.name() <<
"_" << new_v.id();
118 sub_aux =
substitute(sub_aux, v, Poly(new_v));
119 new_qvars.insert(new_v);
127 for (
auto v : new_qvars) {
128 if (subres.variables().find(v) != subres.variables().end()) {
129 reverse_prefix.push_back(std::make_pair(q, v));
141 return Formula<Poly>(
FormulaType::ITE, {
to_pnf(f.
condition(), reverse_prefix, used_vars, negated),
to_pnf(f.
first_case(), reverse_prefix, used_vars, negated),
to_pnf(f.
second_case(), reverse_prefix, used_vars, negated)});
150 template<
typename Poly>
151 void free_variables(
const Formula<Poly>& f, boost::container::flat_set<Variable>& current_quantified_vars, boost::container::flat_set<Variable>& free_vars) {
168 if (!current_quantified_vars.contains(v)) {
180 auto old = current_quantified_vars;
183 current_quantified_vars = old;
187 auto old = current_quantified_vars;
190 current_quantified_vars = old;
193 current_quantified_vars = old;
217 template<
typename Poly>
219 boost::container::flat_set<Variable> current_quantified_vars;
220 boost::container::flat_set<Variable> free_vars;
230 template<
typename Poly>
233 boost::container::flat_set<Variable> used_vars =
free_variables(f);
234 auto m =
to_pnf(f, p, used_vars,
false);
236 return std::make_pair(p, m);
239 template<
typename Poly>
242 for (
auto p = prefix.rbegin(); p != prefix.rend(); p++) {
carl is the main namespace for the library.
std::vector< std::pair< Quantifier, carl::Variable > > QuantifierPrefix
void free_variables(const Formula< Poly > &f, boost::container::flat_set< Variable > ¤t_quantified_vars, boost::container::flat_set< Variable > &free_vars)
std::ostream & operator<<(std::ostream &os, const BasicConstraint< Poly > &c)
Prints the given constraint on the given stream.
Formula< Poly > to_formula(const QuantifierPrefix &prefix, const Formula< Poly > &matrix)
std::vector< Formula< Poly > > Formulas
Variable fresh_variable(VariableType vt) noexcept
Coeff substitute(const Monomial &m, const std::map< Variable, Coeff > &substitutions)
Applies the given substitutions to a monomial.
Formula< Poly > to_pnf(const Formula< Poly > &f, QuantifierPrefix &reverse_prefix, boost::container::flat_set< Variable > &used_vars, bool negated=false)
void variables(const BasicConstraint< Pol > &c, carlVariables &vars)
std::set< Variable > Variables
UnivariatePolynomial< Coefficient > reverse(UnivariatePolynomial< Coefficient > &&p)
Reverses the order of the coefficients of this polynomial.
Formula< Pol > connectPrecedingSubformulas(const Formula< Pol > &f)
[Auxiliary method]
void set_name(Variable v, const std::string &name)
Add a name for a given Variable.
static VariablePool & getInstance()
Returns the single instance of this class by reference.
const Formula & subformula() const
const Formula & premise() const
const Formula & conclusion() const
const Formula & quantified_formula() const
const std::vector< carl::Variable > & quantified_variables() const
const Formulas< Pol > & subformulas() const
const Formula & first_case() const
const Formula & second_case() const
const Formula & quantified_aux_formula() const
const Formula & condition() const