SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
to_formula.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include <smtrat-common/types.h>
4 #include <smtrat-coveringng/types.h>
5 
6 namespace smtrat::qe::coverings::util {
7 
8 FormulaT to_formula_true_only(const cadcells::datastructures::PolyPool& pool, const covering_ng::ParameterTree& tree);
9 
10 FormulaT to_formula_alternate(const cadcells::datastructures::PolyPool& pool, const covering_ng::ParameterTree& tree);
11 
12 } // namespace smtrat::qe::coverings
smtrat::qe::coverings::util::to_formula_alternate
FormulaT to_formula_alternate(const cadcells::datastructures::PolyPool &pool, const covering_ng::ParameterTree &tree, bool positive)
Definition: to_formula.cpp:63
smtrat::qe::coverings::util::to_formula_true_only
FormulaT to_formula_true_only(const cadcells::datastructures::PolyPool &pool, const covering_ng::ParameterTree &tree)
Definition: to_formula.cpp:40
smtrat::FormulaT
carl::Formula< Poly > FormulaT
Definition: types.h:37