Clingo
Loading...
Searching...
No Matches
program.hh
1#pragma once
2
3#include <clingo/input/statement.hh>
4
5#include <clingo/core/logger.hh>
6
7#include <clingo/util/enum.hh>
8#include <clingo/util/ordered_map.hh>
9#include <clingo/util/ordered_set.hh>
10
11#include <forward_list>
12
13namespace CppClingo::Input {
14
17
21enum class ProjectionMode : uint8_t {
22 disabled = 0,
23 anonymous = 1,
24 pure = 2,
25};
26
28enum class ProfileFlags : uint8_t {
29 off = 0,
30 detailed = 1,
31 step = 2,
32 accu = 4,
33};
36
46
49
52
62 std::vector<Stm const *> srcs;
65};
67using ProgramPartVec = std::vector<ProgramPart>;
68
71 public:
73 void add(SymbolStore &store, Stm stm);
74
76 void clear();
77
79 [[nodiscard]] auto empty() const -> bool;
80
82 void mark(SymbolCollector &gc) const;
83
85 void join(UnprocessedProgram const &other);
86
88 [[nodiscard]] auto parts() const -> ProgramPartVec const & { return parts_; }
90 [[nodiscard]] auto meta_stms() const -> StmVec const & { return meta_stms_; }
91
92 private:
93 ProgramPartVec parts_;
94 StmVec meta_stms_;
95};
96
102enum class ComponentType : uint8_t {
103 positive = 1,
104 single_pass = 2,
105};
108
129
131using Components = std::vector<std::vector<Component>>;
132
135 public:
137 virtual ~DependencyBuilder() = default;
139 void param(ProgramParam const &param) { do_param(param); }
141 void meta(std::vector<Stm> const &stms) { do_meta(stms); }
143 void fact(std::vector<Symbol> const &facts) { do_fact(facts); }
145 [[nodiscard]] auto components(Components const &comps) -> bool { return do_components(comps); }
146
147 private:
148 virtual void do_param(ProgramParam const &param) = 0;
149 virtual void do_meta(std::vector<Stm> const &stms) = 0;
150 virtual void do_fact(SymbolVec const &facts) = 0;
151 [[nodiscard]] virtual auto do_components(Components const &comps) -> bool = 0;
152};
153
155class Program {
156 public:
160 Program(RewriteOptions opts) : opts_{opts} {}
165 void join(Logger &log, SymbolStore &store, UnprocessedProgram const &prg);
169 template <class F> void visit_stms(SymbolStore &store, F fun) const {
170 for (auto const &stm : script_stms_) {
171 fun(stm);
172 }
173 if (default_parts_) {
174 fun(*default_parts_);
175 }
176 for (auto const &stm : defined_stms_) {
177 fun(stm);
178 }
179 for (auto const &[id, sym] : const_map_) {
180 fun(Stm{StmConst{sym.first.loc(), sym.first.type(), sym.first.name(),
181 TermSymbol{location(sym.first.value()), *sym.second}}});
182 }
183 for (auto const &stm : thy_stms_) {
184 fun(stm);
185 }
186 for (auto const &stm : meta_stms_) {
187 fun(stm);
188 }
189 for (auto const &[sig, part] : parts_) {
190 auto pum = param_map_(store, part);
191 auto loc = part.part.loc();
192 auto ids = SharedStringArray{pum.begin(), pum.end(), [](auto const &x) { return *x.second; }};
193 fun(StmProgram{loc, *sig.first, std::move(ids)});
194 for (auto const &fact : part.facts) {
195 fun(Stm{StmRule{loc, HdLitSimple{LitSymbolic{loc, Sign::none, TermSymbol{loc, fact}}}, BdLitArray{}}});
196 }
197 for (auto const &stm : part.stms) {
198 if (auto unmapped = unmap_(store, pum, stm); unmapped) {
199 fun(std::move(unmapped).value());
200 } else {
201 fun(stm);
202 }
203 }
204 }
205 }
207 auto meta_stms() -> StmVec const & { return meta_stms_; }
208
210 [[nodiscard]] auto analyze(SymbolStore &store, ProgramParamVec const &params, DependencyBuilder &bld) -> bool;
211
213 void mark(SymbolCollector &gc) const;
214
216 void check(Logger &log);
217
219 [[nodiscard]] auto theory_directives() const -> TheorySigVec;
220
222 [[nodiscard]] auto const_map() const -> ConstMap const & { return const_map_; };
223
225 void mark_sig(Input::Sig const &sig);
226
228 [[nodiscard]] auto default_parts() -> std::optional<StmParts> & { return default_parts_; }
229
231 [[nodiscard]] auto profile() const -> ProfileFlags { return opts_.profile; }
232
233 private:
237 using Signature = std::pair<SharedString, size_t>;
244
246 [[nodiscard]] static auto param_map_(SymbolStore &store, ProgramPart const &part) -> ParamUnmap;
248 [[nodiscard]] static auto unmap_(SymbolStore &store, ParamUnmap const &pum, Stm const &stm) -> std::optional<Stm>;
249
250 void fill_source(ProgramPart &part);
251
253 RewriteOptions opts_;
255 StmVec meta_stms_;
257 std::vector<StmScript> script_stms_;
259 std::vector<StmDefined> defined_stms_;
261 std::vector<StmTheory> thy_stms_;
263 std::optional<StmParts> default_parts_;
265 PartMap parts_;
267 std::forward_list<Stm> sources_;
269 std::forward_list<Stm>::iterator last_source_ = sources_.before_begin();
271 ConstMap const_map_;
273 SharedSigSet provide_;
277 size_t depend_offset_ = 0;
278};
279
281
282} // namespace CppClingo::Input
Interface to process a rewritten and analyzed input program.
Definition program.hh:134
auto components(Components const &comps) -> bool
Add components.
Definition program.hh:145
void param(ProgramParam const &param)
Add parts to ground.
Definition program.hh:139
void fact(std::vector< Symbol > const &facts)
Add facts.
Definition program.hh:143
virtual ~DependencyBuilder()=default
Default destructor.
void meta(std::vector< Stm > const &stms)
Add meta statements.
Definition program.hh:141
A single literal in a rule head.
Definition head_literal.hh:15
Literal representing a symbolic literal.
Definition literal.hh:104
A program consisting of parts.
Definition program.hh:155
void check(Logger &log)
Check program and emit diagnostics.
Program(RewriteOptions opts)
Initialize a program with a rewrite level.
Definition program.hh:160
void mark(SymbolCollector &gc) const
Mark symbols occurring in the program.
auto analyze(SymbolStore &store, ProgramParamVec const &params, DependencyBuilder &bld) -> bool
Prepare the statements in a program for grounding.
auto profile() const -> ProfileFlags
Check whether profiling is enabled.
Definition program.hh:231
void join(Logger &log, SymbolStore &store, UnprocessedProgram const &prg)
Join with the given unprocessed program.
void mark_sig(Input::Sig const &sig)
Mark the given signature as provided.
auto const_map() const -> ConstMap const &
Get the constants in the program.
Definition program.hh:222
auto theory_directives() const -> TheorySigVec
Get a sorted vector of all signatures of theory directives in the program.
auto default_parts() -> std::optional< StmParts > &
Get the default parts.
Definition program.hh:228
auto meta_stms() -> StmVec const &
Get the meta statements in the program.
Definition program.hh:207
void visit_stms(SymbolStore &store, F fun) const
Visit all the statements in the program.
Definition program.hh:169
A const statement.
Definition statement.hh:728
auto loc() const -> Location const &
The location of the statement.
Definition statement.hh:741
A program statement.
Definition statement.hh:690
A rule.
Definition statement.hh:16
Term representing a symbol.
Definition term.hh:123
Program grouping unprocessed statements.
Definition program.hh:70
void add(SymbolStore &store, Stm stm)
Add a statement.
void mark(SymbolCollector &gc) const
Mark symbols occurring in the program.
void clear()
Reset the program to its initial state removing all added statements.
auto meta_stms() const -> StmVec const &
Meta statements.
Definition program.hh:90
auto empty() const -> bool
Check if the program is empty.
void join(UnprocessedProgram const &other)
Join with another unprocessed program.
auto parts() const -> ProgramPartVec const &
Unprocessed statements.
Definition program.hh:88
Simple logger to report message to stderr or via a callback.
Definition logger.hh:63
Helper class to mark owned symbols.
Definition symbol.hh:429
A store for symbols.
Definition symbol.hh:454
auto begin() const noexcept -> const_iterator
Get an iterator pointing to the beginning of the array.
Definition immutable_array.hh:117
std::vector< Symbol > SymbolVec
A vector of symbols.
Definition symbol.hh:220
std::vector< TheorySig > TheorySigVec
A vector of theory atom signatures.
Definition core.hh:184
@ none
No sign.
@ sig
Check if term is a signature.
ComponentType
The type of a component.
Definition program.hh:102
std::vector< ProgramPart > ProgramPartVec
Statements grouped by parts.
Definition program.hh:67
std::vector< std::vector< Component > > Components
The list of components in groundable order.
Definition program.hh:131
Util::ordered_map< SharedString, SharedString > ParamUnmap
Map from parameters to their replacements.
Definition program.hh:51
ProfileFlags
Flags to control how profiling information is output.
Definition program.hh:28
Util::ordered_map< SharedString, std::pair< StmConst, SharedSymbol > > ConstMap
Map from identifiers to constants.
Definition program.hh:48
ProjectionMode
Enumeration to select variables to project.
Definition program.hh:21
@ positive
The component does not contain a negative cycle.
@ single_pass
The component can be grounded in one pass.
@ accu
Output accumulated profiling information.
@ step
Output profiling information for each step.
@ detailed
Output detailed profiling information.
@ disabled
Disable projection.
@ anonymous
Only project anonymous variables.
@ pure
Project pure variables.
std::vector< ProgramParam > ProgramParamVec
A list of program params.
Definition statement.hh:761
std::variant< StmRule, StmTheory, StmOptimize, StmWeakConstraint, StmShow, StmShowNothing, StmShowSig, StmProject, StmProjectSig, StmDefined, StmExternal, StmEdge, StmHeuristic, StmScript, StmInclude, StmProgram, StmConst, StmParts, StmComment > Stm
Variant of available statements.
Definition statement.hh:828
std::vector< Stm > StmVec
A vector of statements.
Definition statement.hh:830
std::pair< SharedString, std::vector< SharedSymbol > > ProgramParam
Concrete symbols for a program statement.
Definition statement.hh:759
Util::ordered_set< SharedSig > SharedSigSet
A set of predicate signatures.
Definition term.hh:44
std::tuple< String, size_t, bool > Sig
The signature of a predicate.
Definition term.hh:40
tsl::hopscotch_set< Key, Hash, KeyEqual, Allocator, NeighborhoodSize, StoreHash, GrowthPolicy > unordered_set
Alias for unordered sets.
Definition unordered_set.hh:16
tsl::ordered_map< Key, T, Hash, KeyEqual, Allocator, ValueTypeContainer, IndexType > ordered_map
Alias for ordered maps.
Definition ordered_map.hh:16
#define CLINGO_ENABLE_BITSET_ENUM(E,...)
Opt-in macro for enabling bit operations for a given enum type.
Definition enum.hh:18
A refined component.
Definition program.hh:116
Util::ordered_map< Term const *, Util::ordered_set< Term const * > > incomplete
This vector captures literals that are not yet complete.
Definition program.hh:125
ComponentType type
The type of the component.
Definition program.hh:127
std::vector< Stm const * > stms
The statements in the component.
Definition program.hh:119
Util::unordered_set< std::tuple< String, size_t, bool > > depend
The literals a component depends on.
Definition program.hh:123
std::vector< Stm const * > srcs
The (optional) source statements in the component.
Definition program.hh:121
A program part.
Definition program.hh:54
StmVec stms
The statements in the program part.
Definition program.hh:60
SymbolVec facts
The facts in the program part.
Definition program.hh:64
std::vector< Stm const * > srcs
The source index of the statement at the corresponding index.
Definition program.hh:62
ProgramPart(StmProgram part)
Construct a program part.
Definition program.hh:56
StmProgram part
The (first) program part statement that introduced the part.
Definition program.hh:58
Options to configure rewriting.
Definition program.hh:38
ProjectionMode project_mode
The projection mode.
Definition program.hh:40
bool project_anonymous
Whether to project anonymous variables in negative literals.
Definition program.hh:42
ProfileFlags profile
Whether to profile the grounding process.
Definition program.hh:44