SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
parser_smtlib.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include <smtrat-common/smtrat-common.h>
4 
5 #include <string>
6 
7 namespace smtrat {
8 
9 /**
10  * Loads the smt2 file specified in filename and returns the formula.
11  * This function ignores most SMT-LIB commands but simply accumulated all asserted formulas.
12  */
13 FormulaT parse_formula(const std::string& filename);
14 
15 }
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::parse_formula
FormulaT parse_formula(const std::string &filename)
Loads the smt2 file specified in filename and returns the formula.
smtrat::FormulaT
carl::Formula< Poly > FormulaT
Definition: types.h:37