carl  25.02
Computer ARithmetic Library
PNF.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "../Formula.h"
4 #include "Substitution.h"
5 #include "aux.h"
6 
7 namespace carl {
8 
9 enum class Quantifier {
10  EXISTS,
11  FORALL,
12  FREE
13 };
14 inline std::ostream& operator<<(std::ostream& os, const Quantifier& type) {
15  switch (type) {
16  case Quantifier::EXISTS:
17  os << "exists";
18  return os;
19  case Quantifier::FORALL:
20  os << "forall";
21  return os;
22  case Quantifier::FREE:
23  os << "free";
24  return os;
25  }
26 }
27 
28 using QuantifierPrefix = std::vector<std::pair<Quantifier, carl::Variable>>;
29 
30 template<typename Poly>
31 Formula<Poly> to_pnf(const Formula<Poly>& f, QuantifierPrefix& reverse_prefix, boost::container::flat_set<Variable>& used_vars, bool negated = false) {
32  switch (f.type()) {
33  case FormulaType::AND:
34  case FormulaType::IFF:
35  case FormulaType::OR:
36  case FormulaType::XOR: {
37  if (!negated) {
38  Formulas<Poly> subs;
39  for (auto& sub : f.subformulas()) {
40  subs.push_back(to_pnf(sub, reverse_prefix, used_vars, false));
41  }
42  return Formula<Poly>(f.type(), std::move(subs));
43  } else if (f.type() == FormulaType::AND || f.type() == FormulaType::OR) {
44  Formulas<Poly> subs;
45  for (auto& sub : f.subformulas()) {
46  subs.push_back(to_pnf(sub, reverse_prefix, used_vars, true));
47  }
48  if (f.type() == FormulaType::AND) {
49  return Formula<Poly>(FormulaType::OR, std::move(subs));
50  } else {
51  return Formula<Poly>(FormulaType::AND, std::move(subs));
52  }
53  } else if (f.type() == FormulaType::IFF) {
54  Formulas<Poly> sub1;
55  Formulas<Poly> sub2;
56  for (auto& sub : f.subformulas()) {
57  sub1.push_back(to_pnf(sub, reverse_prefix, used_vars, true));
58  sub2.push_back(to_pnf(sub, reverse_prefix, used_vars, false));
59  }
60  return Formula<Poly>(FormulaType::AND, {Formula<Poly>(FormulaType::OR, std::move(sub1)), Formula<Poly>(FormulaType::OR, std::move(sub2))});
61  } else if (f.type() == FormulaType::XOR) {
62  auto lhs = to_pnf(f, reverse_prefix, used_vars, false);
63  auto rhs = to_pnf(formula::aux::connectPrecedingSubformulas(f), reverse_prefix, used_vars, false);
64  return Formula<Poly>(FormulaType::IFF, std::vector<Formula<Poly>>({lhs, rhs}));
65  }
66  assert(false);
67  }
68  case FormulaType::BOOL:
70  case FormulaType::FALSE:
71  case FormulaType::UEQ:
73  case FormulaType::TRUE:
76  if (negated)
77  return f.negated();
78  else
79  return f;
80  }
82  case FormulaType::FORALL: {
85  carl::Variables new_qvars;
86  for (auto v : f.quantified_variables()) {
87  if (used_vars.contains(v)) {
88  auto new_v = fresh_variable(v.type());
89  std::stringstream ss; ss << v.name() << "_" << new_v.id();
90  VariablePool::getInstance().set_name(new_v, ss.str());
91  sub = substitute(sub, v, Poly(new_v));
92  new_qvars.insert(new_v);
93  } else {
94  used_vars.insert(v);
95  new_qvars.insert(v);
96  }
97  }
98 
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));
103  }
104  }
105  return subres;
106  }
111  carl::Variables new_qvars;
112  for (auto v : f.quantified_variables()) {
113  if (used_vars.contains(v)) {
114  auto new_v = fresh_variable(v.type());
115  std::stringstream ss; ss << v.name() << "_" << new_v.id();
116  VariablePool::getInstance().set_name(new_v, ss.str());
117  sub = substitute(sub, v, Poly(new_v));
118  sub_aux = substitute(sub_aux, v, Poly(new_v));
119  new_qvars.insert(new_v);
120  } else {
121  used_vars.insert(v);
122  new_qvars.insert(v);
123  }
124  }
125 
126  auto subres = carl::Formula(carl::FormulaType::AND, sub_aux, to_pnf(sub, reverse_prefix, used_vars, negated));
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));
130  }
131  }
132  return subres;
133  }
135  if (negated) {
136  return Formula<Poly>(FormulaType::AND, {to_pnf(f.premise(), reverse_prefix, used_vars, false), to_pnf(f.conclusion(), reverse_prefix, used_vars, true)});
137  } else {
138  return Formula<Poly>(FormulaType::OR, {to_pnf(f.premise(), reverse_prefix, used_vars, true), to_pnf(f.conclusion(), reverse_prefix, used_vars, false)});
139  }
140  case FormulaType::ITE:
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)});
142  case FormulaType::NOT:
143  return to_pnf(f.subformula(), reverse_prefix, used_vars, !negated);
144  default:
145  assert(false);
147  }
148 }
149 
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) {
152  switch (f.type()) {
153  case FormulaType::AND:
154  case FormulaType::IFF:
155  case FormulaType::OR:
156  case FormulaType::XOR: {
157  for (auto& sub : f.subformulas()) {
158  free_variables(sub, current_quantified_vars, free_vars);
159  }
160  break;
161  }
162  case FormulaType::BOOL:
165  case FormulaType::UEQ:
167  for (auto v : variables(f)) {
168  if (!current_quantified_vars.contains(v)) {
169  free_vars.insert(v);
170  }
171  }
172  break;
173  }
174  case FormulaType::VARASSIGN: {
175  assert(false);
176  break;
177  }
178  case FormulaType::EXISTS:
179  case FormulaType::FORALL: {
180  auto old = current_quantified_vars;
181  current_quantified_vars.insert(f.quantified_variables().begin(), f.quantified_variables().end());
182  free_variables(f.quantified_formula(), current_quantified_vars, free_vars);
183  current_quantified_vars = old;
184  break;
185  }
187  auto old = current_quantified_vars;
188  current_quantified_vars.insert(f.quantified_variables().begin(), f.quantified_variables().end());
189  free_variables(f.quantified_formula(), current_quantified_vars, free_vars);
190  current_quantified_vars = old;
191  current_quantified_vars.insert(f.quantified_variables().begin(), f.quantified_variables().end());
192  free_variables(f.quantified_aux_formula(), current_quantified_vars, free_vars);
193  current_quantified_vars = old;
194  break;
195  }
197  free_variables(f.premise(), current_quantified_vars, free_vars);
198  free_variables(f.conclusion(), current_quantified_vars, free_vars);
199  break;
200  case FormulaType::ITE:
201  free_variables(f.condition(), current_quantified_vars, free_vars);
202  free_variables(f.first_case(), current_quantified_vars, free_vars);
203  free_variables(f.second_case(), current_quantified_vars, free_vars);
204  break;
205  case FormulaType::NOT:
206  free_variables(f.subformula(), current_quantified_vars, free_vars);
207  break;
208  case FormulaType::FALSE:
209  case FormulaType::TRUE: {
210  break;
211  }
212  default:
213  assert(false);
214  }
215 }
216 
217 template<typename Poly>
219  boost::container::flat_set<Variable> current_quantified_vars;
220  boost::container::flat_set<Variable> free_vars;
221  free_variables(f, current_quantified_vars, free_vars);
222  return free_vars;
223 }
224 
225 /**
226  * Transforms this formula to its equivalent in prenex normal form.
227  * @param negated Used for internal recursion.
228  * @return A pair of the prefix and the matrix.
229  */
230 template<typename Poly>
231 std::pair<QuantifierPrefix, Formula<Poly>> to_pnf(const Formula<Poly>& f) {
233  boost::container::flat_set<Variable> used_vars = free_variables(f);
234  auto m = to_pnf(f, p, used_vars, false);
235  std::reverse(p.begin(), p.end());
236  return std::make_pair(p, m);
237 }
238 
239 template<typename Poly>
240 inline Formula<Poly> to_formula(const QuantifierPrefix& prefix, const Formula<Poly>& matrix) {
241  Formula<Poly> res = matrix;
242  for (auto p = prefix.rbegin(); p != prefix.rend(); p++) {
243  assert(p->first != Quantifier::FREE);
244  res = Formula<Poly>(p->first == Quantifier::EXISTS ? FormulaType::EXISTS : FormulaType::FORALL, std::vector<Variable>({p->second}), res);
245  }
246  return res;
247 }
248 
249 } // namespace carl
carl is the main namespace for the library.
@ CONSTRAINT
@ BITVECTOR
@ VARCOMPARE
@ AUX_EXISTS
@ VARASSIGN
std::vector< std::pair< Quantifier, carl::Variable > > QuantifierPrefix
Definition: PNF.h:28
Quantifier
Definition: PNF.h:9
void free_variables(const Formula< Poly > &f, boost::container::flat_set< Variable > &current_quantified_vars, boost::container::flat_set< Variable > &free_vars)
Definition: PNF.h:151
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)
Definition: PNF.h:240
std::vector< Formula< Poly > > Formulas
Variable fresh_variable(VariableType vt) noexcept
Definition: VariablePool.h:179
Coeff substitute(const Monomial &m, const std::map< Variable, Coeff > &substitutions)
Applies the given substitutions to a monomial.
Definition: Substitution.h:19
Formula< Poly > to_pnf(const Formula< Poly > &f, QuantifierPrefix &reverse_prefix, boost::container::flat_set< Variable > &used_vars, bool negated=false)
Definition: PNF.h:31
void variables(const BasicConstraint< Pol > &c, carlVariables &vars)
std::set< Variable > Variables
Definition: Common.h:18
UnivariatePolynomial< Coefficient > reverse(UnivariatePolynomial< Coefficient > &&p)
Reverses the order of the coefficients of this polynomial.
Formula< Pol > connectPrecedingSubformulas(const Formula< Pol > &f)
[Auxiliary method]
Definition: aux.h:13
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.
Definition: Singleton.h:45
const Formula & subformula() const
Definition: Formula.h:335
const Formula & premise() const
Definition: Formula.h:344
const Formula & conclusion() const
Definition: Formula.h:353
const Formula & quantified_formula() const
Definition: Formula.h:402
const std::vector< carl::Variable > & quantified_variables() const
Definition: Formula.h:389
const Formulas< Pol > & subformulas() const
Definition: Formula.h:422
const Formula & first_case() const
Definition: Formula.h:371
const Formula & second_case() const
Definition: Formula.h:380
const Formula & quantified_aux_formula() const
Definition: Formula.h:412
FormulaType type() const
Definition: Formula.h:262
Formula negated() const
Definition: Formula.h:316
const Formula & condition() const
Definition: Formula.h:362