carl  25.02
Computer ARithmetic Library
Visit.h
Go to the documentation of this file.
1 #pragma once
2 
3 namespace carl {
4 
5 
6 /**
7  * Recursively calls func on every subformula.
8  * @param formula Formula to visit.
9  * @param func Function to call.
10  */
11 template<typename Pol, typename Visitor>
12 void visit(const Formula<Pol>& formula, /*std::function<void(const Formula<Pol>&)>&*/ Visitor func) {
13  switch (formula.type()) {
14  case AND:
15  case OR:
16  case IFF:
17  case XOR:
18  case IMPLIES:
19  case ITE:
20  for (const auto& cur: formula.subformulas()) visit(cur, func);
21  break;
22  case NOT:
23  visit(formula.subformula(), func);
24  break;
25  case BOOL:
26  case CONSTRAINT:
27  case VARCOMPARE:
28  case VARASSIGN:
29  case BITVECTOR:
30  case TRUE:
31  case FALSE:
32  case UEQ:
33  break;
34  case EXISTS:
35  case FORALL:
36  visit(formula.quantified_formula(), func);
37  break;
38  case AUX_EXISTS:
39  visit(formula.quantified_formula(), func);
40  visit(formula.quantified_aux_formula(), func);
41  break;
42  }
43  func(formula);
44 }
45 /**
46  * Recursively calls func on every subformula and return a new formula.
47  * On every call of func, the passed formula is replaced by the result.
48  * @param formula Formula to visit.
49  * @param func Function to call.
50  * @return New formula.
51  */
52 template<typename Pol, typename Visitor>
53 Formula<Pol> visit_result(const Formula<Pol>& formula, /*std::function<Formula<Pol>(const Formula<Pol>&)>&*/ Visitor func) {
54  Formula<Pol> newFormula = formula;
55  switch (formula.type()) {
56  case AND:
57  case OR:
58  case IFF:
59  case XOR: {
61  bool changed = false;
62  for (const auto& cur: formula.subformulas()) {
63  Formula newCur = visit_result(cur, func);
64  if (newCur != cur) changed = true;
65  newSubformulas.push_back(newCur);
66  }
67  if (changed) {
68  newFormula = Formula(formula.type(), std::move(newSubformulas));
69  }
70  break;
71  }
72  case NOT: {
73  Formula<Pol> cur = visit_result(formula.subformula(), func);
74  if (cur != formula.subformula()) {
75  newFormula = !cur;
76  }
77  break;
78  }
79  case IMPLIES: {
80  Formula<Pol> prem = visit_result(formula.premise(), func);
81  Formula<Pol> conc = visit_result(formula.conclusion(), func);
82  if ((prem != formula.premise()) || (conc != formula.conclusion())) {
83  newFormula = Formula(IMPLIES, {prem, conc});
84  }
85  break;
86  }
87  case ITE: {
88  Formula<Pol> cond = visit_result(formula.condition(), func);
89  Formula<Pol> fCase = visit_result(formula.first_case(), func);
90  Formula<Pol> sCase = visit_result(formula.second_case(), func);
91  if ((cond != formula.condition()) || (fCase != formula.first_case()) || (sCase != formula.second_case())) {
92  newFormula = Formula(ITE, {cond, fCase, sCase});
93  }
94  break;
95  }
96  case BOOL:
97  case CONSTRAINT:
98  case VARCOMPARE:
99  case VARASSIGN:
100  case BITVECTOR:
101  case TRUE:
102  case FALSE:
103  case UEQ:
104  break;
105  case EXISTS:
106  case FORALL: {
107  Formula<Pol> sub = visit_result(formula.quantified_formula(), func);
108  if (sub != formula.quantified_formula()) {
109  newFormula = Formula<Pol>(formula.type(), formula.quantified_variables(), sub);
110  }
111  break;
112  }
113  case AUX_EXISTS: {
114  Formula<Pol> sub = visit_result(formula.quantified_formula(), func);
115  Formula<Pol> sub_aux = visit_result(formula.quantified_aux_formula(), func);
116  if (sub != formula.quantified_formula() || sub_aux != formula.quantified_aux_formula()) {
117  newFormula = Formula<Pol>(formula.type(), formula.quantified_variables(), sub_aux, sub);
118  }
119  break;
120  }
121  }
122  return func(newFormula);
123 }
124 
125 
126 }
carl is the main namespace for the library.
@ CONSTRAINT
@ BITVECTOR
@ VARCOMPARE
@ AUX_EXISTS
@ VARASSIGN
std::vector< Formula< Poly > > Formulas
void visit(const Formula< Pol > &formula, Visitor func)
Recursively calls func on every subformula.
Definition: Visit.h:12
Formula< Pol > visit_result(const Formula< Pol > &formula, Visitor func)
Recursively calls func on every subformula and return a new formula.
Definition: Visit.h:53
Represent an SMT formula, which can be an atom for some background theory or a boolean combination of...
Definition: Formula.h:47
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
const Formula & condition() const
Definition: Formula.h:362