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
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Morgan Deters, Justin Xu
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* The preprocessor of the SmtEngine.
*/
#include "cvc5_private.h"
#ifndef CVC5__SMT__PREPROCESSOR_H
#define CVC5__SMT__PREPROCESSOR_H
#include <memory>
#include "smt/expand_definitions.h"
#include "smt/process_assertions.h"
#include "theory/booleans/circuit_propagator.h"
namespace cvc5 {
class Env;
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,
Env& env,
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
* @return The expanded term.
*/
Node expandDefinitions(const Node& n);
/** Same as above, with a cache of previous results. */
Node expandDefinitions(
const Node& n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
/**
* Set proof node manager. Enables proofs in this preprocessor.
*/
void setProofGenerator(PreprocessProofGenerator* pppg);
private:
/** Reference to the parent SmtEngine */
SmtEngine& d_smt;
/** Reference to the env */
Env& d_env;
/** 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
|
