1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
/********************* */
/*! \file smt_solver.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The solver for SMT queries in an SmtEngine.
**/
#include "cvc4_private.h"
#ifndef CVC4__SMT__SMT_SOLVER_H
#define CVC4__SMT__SMT_SOLVER_H
#include <vector>
#include "expr/node.h"
#include "theory/logic_info.h"
#include "util/result.h"
namespace CVC4 {
class SmtEngine;
class TheoryEngine;
class ResourceManager;
namespace prop {
class PropEngine;
}
namespace smt {
class Assertions;
class SmtEngineState;
class Preprocessor;
class SmtEngineStatistics;
/**
* A solver for SMT queries.
*
* This class manages the initialization of the theory engine and propositional
* engines and implements the method for checking satisfiability of the current
* set of assertions.
*
* Notice that this class is only conceptually responsible for running
* check-sat commands and an interface for sending formulas to the underlying
* classes. It does not implement any query techniques beyond getting the result
* (unsat/sat/unknown) of check-sat calls. More detailed information (e.g.
* models) can be queries using other classes that examine the state of the
* TheoryEngine directly, which can be accessed via getTheoryEngine.
*/
class SmtSolver
{
public:
SmtSolver(SmtEngine& smt,
SmtEngineState& state,
ResourceManager* rm,
Preprocessor& pp,
SmtEngineStatistics& stats);
~SmtSolver();
/**
* Create theory engine, prop engine based on the logic info.
*/
void finishInit(const LogicInfo& logicInfo);
/** Reset all assertions, global declarations, etc. */
void resetAssertions();
/**
* Interrupt a running query. This can be called from another thread
* or from a signal handler. Throws a ModalException if the SmtSolver
* isn't currently in a query.
*/
void interrupt();
/**
* This is called by the destructor of SmtEngine, just before destroying the
* PropEngine, TheoryEngine, and DecisionEngine (in that order). It
* is important because there are destruction ordering issues
* between PropEngine and Theory.
*/
void shutdown();
/**
* Check satisfiability (used to check satisfiability and entailment)
* in SmtEngine. This is done via adding assumptions (when necessary) to
* assertions as, preprocessing and pushing assertions into the prop engine
* of this class, and checking for satisfiability via the prop engine.
*
* @param as The object managing the assertions in SmtEngine. This class
* maintains a current set of (unprocessed) assertions which are pushed
* into the internal members of this class (TheoryEngine and PropEngine)
* during this call.
* @param assumptions The assumptions for this check-sat call, which are
* temporary assertions.
* @param inUnsatCore Whether assumptions are in the unsat core.
* @param isEntailmentCheck Whether this is an entailment check (assumptions
* are negated in this case).
*/
Result checkSatisfiability(Assertions& as,
const std::vector<Node>& assumptions,
bool inUnsatCore,
bool isEntailmentCheck);
/**
* Process the assertions that have been asserted in as. This moves the set of
* assertions that have been buffered into as, preprocesses them, pushes them
* into the SMT solver, and clears the buffer.
*/
void processAssertions(Assertions& as);
//------------------------------------------ access methods
/** Get a pointer to the TheoryEngine owned by this solver. */
TheoryEngine* getTheoryEngine();
/** Get a pointer to the PropEngine owned by this solver. */
prop::PropEngine* getPropEngine();
//------------------------------------------ end access methods
private:
/** Reference to the parent SMT engine */
SmtEngine& d_smt;
/** Reference to the state of the SmtEngine */
SmtEngineState& d_state;
/** Pointer to a resource manager (owned by SmtEngine) */
ResourceManager* d_rm;
/** Reference to the preprocessor of SmtEngine */
Preprocessor& d_pp;
/** Reference to the statistics of SmtEngine */
SmtEngineStatistics& d_stats;
/** The theory engine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
/** The propositional engine */
std::unique_ptr<prop::PropEngine> d_propEngine;
};
} // namespace smt
} // namespace CVC4
#endif /* CVC4__SMT__SMT_SOLVER_H */
|
