SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
AxiomFactory.h
Go to the documentation of this file.
1 /**
2  * Class to create the formulas for axioms.
3  * @author Aklima Zaman
4  * @since 2018-09-24
5  * @version 2018-09-24
6  */
7 
8 #pragma once
9 
10 
11 #include "../dto/VariableCapsule.h"
12 #include <smtrat-common/smtrat-common.h>
13 #include "../Util.h"
14 #include "../../../smtrat-common/model.h"
15 #include "../dto/RationalCapsule.h"
16 
17 namespace smtrat {
18 
19  class AxiomFactory {
20 
21  public:
22  enum AxiomType { ZERO, TANGENT_PLANE, MONOTONICITY, CONGRUENCE, ICP };
23  static FormulasT createFormula(AxiomType axiomType, Model linearizedModel, MonomialMap monomialMap);
24  };
25 
26 }
smtrat::AxiomFactory::createFormula
static FormulasT createFormula(AxiomType axiomType, Model linearizedModel, MonomialMap monomialMap)
Definition: AxiomFactory.cpp:890
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::MonomialMap
std::unordered_map< carl::Variable, carl::Monomial::Arg > MonomialMap
Definition: Util.h:11
smtrat::Model
carl::Model< Rational, Poly > Model
Definition: model.h:13
smtrat::FormulasT
carl::Formulas< Poly > FormulasT
Definition: types.h:39