CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
qbf_quantor.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_QBF_QBF_QUANTOR_H
11#define CPROVER_SOLVERS_QBF_QBF_QUANTOR_H
12
13#include "qdimacs_cnf.h"
14
16{
17public:
18 explicit qbf_quantort(message_handlert &message_handler);
19 ~qbf_quantort() override;
20
21 std::string solver_text() const override;
22 virtual resultt prop_solve();
23 tvt l_get(literalt a) const override;
24};
25
26#endif // CPROVER_SOLVERS_QBF_QBF_QUANTOR_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
virtual resultt prop_solve()
tvt l_get(literalt a) const override
~qbf_quantort() override
std::string solver_text() const override
Definition threeval.h:20
resultt
The result of goto verifying.
Definition properties.h:45