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
|
/********************* */
/*! \file preprocessor.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Justin Xu
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 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 preprocessor of the SmtEngine.
**/
#include "cvc4_private.h"
#ifndef CVC4__SMT__PREPROCESSOR_H
#define CVC4__SMT__PREPROCESSOR_H
#include <memory>
#include "smt/expand_definitions.h"
#include "smt/process_assertions.h"
#include "theory/booleans/circuit_propagator.h"
namespace CVC5 {
namespace preprocessing {
class PreprocessingPassContext;
}
namespace smt {
class AbstractValues;
class PreprocessProofGenerator;
/**
* The preprocessor module of an SMT engine.
*
* This class is responsible for:
* (1) preprocessing the set of assertions from input before they are sent to
* the SMT solver,
* (2) implementing methods for expanding and simplifying formulas. The latter
* takes into account the substitutions inferred by this class.
*/
class Preprocessor
{
public:
Preprocessor(SmtEngine& smt,
context::UserContext* u,
AbstractValues& abs,
SmtEngineStatistics& stats);
~Preprocessor();
/**
* Finish initialization
*/
void finishInit();
/**
* Process the assertions that have been asserted in argument as. Returns
* true if no conflict was discovered while preprocessing them.
*/
bool process(Assertions& as);
/**
* Clear learned literals from the Boolean propagator.
*/
void clearLearnedLiterals();
/**
* Cleanup, which deletes the processing passes owned by this module. This
* is required to be done explicitly so that passes are deleted before the
* objects they refer to in the SmtEngine destructor.
*/
void cleanup();
/**
* Simplify a formula without doing "much" work. Does not involve
* the SAT Engine in the simplification, but uses the current
* definitions, assertions, and the current partial model, if one
* has been constructed. It also involves theory normalization.
*
* @param n The node to simplify
* @return The simplified term.
*/
Node simplify(const Node& n);
/**
* Expand the definitions in a term or formula n. No other
* simplification or normalization is done.
*
* @param n The node to expand
* @param expandOnly if true, then the expandDefinitions function of
* TheoryEngine is not called on subterms of n.
* @return The expanded term.
*/
Node expandDefinitions(const Node& n, bool expandOnly = false);
/** Same as above, with a cache of previous results. */
Node expandDefinitions(
const Node& n,
std::unordered_map<Node, Node, NodeHashFunction>& cache,
bool expandOnly = false);
/**
* Set proof node manager. Enables proofs in this preprocessor.
*/
void setProofGenerator(PreprocessProofGenerator* pppg);
private:
/** A copy of the current context */
context::Context* d_context;
/** Reference to the parent SmtEngine */
SmtEngine& d_smt;
/** Reference to the abstract values utility */
AbstractValues& d_absValues;
/**
* A circuit propagator for non-clausal propositional deduction.
*/
theory::booleans::CircuitPropagator d_propagator;
/**
* User-context-dependent flag of whether any assertions have been processed.
*/
context::CDO<bool> d_assertionsProcessed;
/** The preprocessing pass context */
std::unique_ptr<preprocessing::PreprocessingPassContext> d_ppContext;
/** Expand definitions module, responsible for expanding definitions */
ExpandDefs d_exDefs;
/**
* Process assertions module, responsible for implementing the preprocessing
* passes.
*/
ProcessAssertions d_processor;
/** Proof node manager */
ProofNodeManager* d_pnm;
};
} // namespace smt
} // namespace CVC5
#endif
|
