1 ###############################################################################
2 # Top contributors (to current version):
3 # Mathias Preiner, Andrew Reynolds, Gereon Kremer
5 # This file is part of the cvc5 project.
7 # Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 # in the top-level source directory and their institutional affiliations.
9 # All rights reserved. See the file COPYING in the top-level source
10 # directory for licensing information.
11 # #############################################################################
13 # The build system configuration.
16 # Collect libcvc5 source files
22 decision/assertion_list.cpp
23 decision/assertion_list.h
24 decision/decision_attributes.h
25 decision/decision_engine.cpp
26 decision/decision_engine.h
27 decision/decision_engine_old.cpp
28 decision/decision_engine_old.h
29 decision/decision_strategy.h
30 decision/justification_heuristic.cpp
31 decision/justification_heuristic.h
32 decision/justification_strategy.cpp
33 decision/justification_strategy.h
34 decision/justify_info.cpp
35 decision/justify_info.h
36 decision/justify_stack.cpp
37 decision/justify_stack.h
38 decision/justify_stats.cpp
39 decision/justify_stats.h
47 omt/bitvector_optimizer.cpp
48 omt/bitvector_optimizer.h
49 omt/integer_optimizer.cpp
50 omt/integer_optimizer.h
53 options/decision_weight.h
58 options/managed_streams.cpp
59 options/managed_streams.h
60 options/option_exception.cpp
61 options/option_exception.h
62 options/options_handler.cpp
63 options/options_handler.h
64 options/options_listener.h
65 options/options_public.h
66 preprocessing/assertion_pipeline.cpp
67 preprocessing/assertion_pipeline.h
68 preprocessing/learned_literal_manager.cpp
69 preprocessing/learned_literal_manager.h
70 preprocessing/passes/ackermann.cpp
71 preprocessing/passes/ackermann.h
72 preprocessing/passes/apply_substs.cpp
73 preprocessing/passes/apply_substs.h
74 preprocessing/passes/bool_to_bv.cpp
75 preprocessing/passes/bool_to_bv.h
76 preprocessing/passes/bv_eager_atoms.cpp
77 preprocessing/passes/bv_eager_atoms.h
78 preprocessing/passes/bv_gauss.cpp
79 preprocessing/passes/bv_gauss.h
80 preprocessing/passes/bv_intro_pow2.cpp
81 preprocessing/passes/bv_intro_pow2.h
82 preprocessing/passes/bv_to_bool.cpp
83 preprocessing/passes/bv_to_bool.h
84 preprocessing/passes/bv_to_int.cpp
85 preprocessing/passes/bv_to_int.h
86 preprocessing/passes/extended_rewriter_pass.cpp
87 preprocessing/passes/extended_rewriter_pass.h
88 preprocessing/passes/foreign_theory_rewrite.cpp
89 preprocessing/passes/foreign_theory_rewrite.h
90 preprocessing/passes/fun_def_fmf.cpp
91 preprocessing/passes/fun_def_fmf.h
92 preprocessing/passes/global_negate.cpp
93 preprocessing/passes/global_negate.h
94 preprocessing/passes/ho_elim.cpp
95 preprocessing/passes/ho_elim.h
96 preprocessing/passes/int_to_bv.cpp
97 preprocessing/passes/int_to_bv.h
98 preprocessing/passes/ite_removal.cpp
99 preprocessing/passes/ite_removal.h
100 preprocessing/passes/ite_simp.cpp
101 preprocessing/passes/ite_simp.h
102 preprocessing/passes/learned_rewrite.cpp
103 preprocessing/passes/learned_rewrite.h
104 preprocessing/passes/miplib_trick.cpp
105 preprocessing/passes/miplib_trick.h
106 preprocessing/passes/nl_ext_purify.cpp
107 preprocessing/passes/nl_ext_purify.h
108 preprocessing/passes/non_clausal_simp.cpp
109 preprocessing/passes/non_clausal_simp.h
110 preprocessing/passes/pseudo_boolean_processor.cpp
111 preprocessing/passes/pseudo_boolean_processor.h
112 preprocessing/passes/quantifiers_preprocess.cpp
113 preprocessing/passes/quantifiers_preprocess.h
114 preprocessing/passes/real_to_int.cpp
115 preprocessing/passes/real_to_int.h
116 preprocessing/passes/rewrite.cpp
117 preprocessing/passes/rewrite.h
118 preprocessing/passes/sep_skolem_emp.cpp
119 preprocessing/passes/sep_skolem_emp.h
120 preprocessing/passes/sort_infer.cpp
121 preprocessing/passes/sort_infer.h
122 preprocessing/passes/static_learning.cpp
123 preprocessing/passes/static_learning.h
124 preprocessing/passes/strings_eager_pp.cpp
125 preprocessing/passes/strings_eager_pp.h
126 preprocessing/passes/sygus_inference.cpp
127 preprocessing/passes/sygus_inference.h
128 preprocessing/passes/synth_rew_rules.cpp
129 preprocessing/passes/synth_rew_rules.h
130 preprocessing/passes/theory_preprocess.cpp
131 preprocessing/passes/theory_preprocess.h
132 preprocessing/passes/theory_rewrite_eq.cpp
133 preprocessing/passes/theory_rewrite_eq.h
134 preprocessing/passes/unconstrained_simplifier.cpp
135 preprocessing/passes/unconstrained_simplifier.h
136 preprocessing/preprocessing_pass.cpp
137 preprocessing/preprocessing_pass.h
138 preprocessing/preprocessing_pass_context.cpp
139 preprocessing/preprocessing_pass_context.h
140 preprocessing/preprocessing_pass_registry.cpp
141 preprocessing/preprocessing_pass_registry.h
142 preprocessing/util/ite_utilities.cpp
143 preprocessing/util/ite_utilities.h
144 printer/ast/ast_printer.cpp
145 printer/ast/ast_printer.h
146 printer/let_binding.cpp
147 printer/let_binding.h
150 printer/smt2/smt2_printer.cpp
151 printer/smt2/smt2_printer.h
152 printer/tptp/tptp_printer.cpp
153 printer/tptp/tptp_printer.h
154 proof/annotation_proof_generator.cpp
155 proof/annotation_proof_generator.h
156 proof/assumption_proof_generator.cpp
157 proof/assumption_proof_generator.h
158 proof/buffered_proof_generator.cpp
159 proof/buffered_proof_generator.h
160 proof/conv_proof_generator.cpp
161 proof/conv_proof_generator.h
162 proof/conv_seq_proof_generator.cpp
163 proof/conv_seq_proof_generator.h
165 proof/dot/dot_printer.cpp
166 proof/dot/dot_printer.h
167 proof/eager_proof_generator.cpp
168 proof/eager_proof_generator.h
171 proof/lazy_proof_chain.cpp
172 proof/lazy_proof_chain.h
173 proof/lazy_tree_proof_generator.cpp
174 proof/lazy_tree_proof_generator.h
175 proof/lfsc/lfsc_list_sc_node_converter.cpp
176 proof/lfsc/lfsc_list_sc_node_converter.h
177 proof/lfsc/lfsc_node_converter.cpp
178 proof/lfsc/lfsc_node_converter.h
179 proof/lfsc/lfsc_post_processor.cpp
180 proof/lfsc/lfsc_post_processor.h
181 proof/lfsc/lfsc_printer.cpp
182 proof/lfsc/lfsc_printer.h
183 proof/lfsc/lfsc_print_channel.cpp
184 proof/lfsc/lfsc_print_channel.h
185 proof/lfsc/lfsc_util.cpp
186 proof/lfsc/lfsc_util.h
193 proof/proof_checker.cpp
194 proof/proof_checker.h
195 proof/proof_ensure_closed.cpp
196 proof/proof_ensure_closed.h
197 proof/proof_generator.cpp
198 proof/proof_generator.h
199 proof/proof_letify.cpp
203 proof/proof_node_algorithm.cpp
204 proof/proof_node_algorithm.h
205 proof/proof_node_to_sexpr.cpp
206 proof/proof_node_to_sexpr.h
207 proof/proof_node_manager.cpp
208 proof/proof_node_manager.h
209 proof/proof_node_updater.cpp
210 proof/proof_node_updater.h
214 proof/proof_step_buffer.cpp
215 proof/proof_step_buffer.h
218 proof/theory_proof_step_buffer.cpp
219 proof/theory_proof_step_buffer.h
222 proof/alethe/alethe_nosubtype_node_converter.cpp
223 proof/alethe/alethe_nosubtype_node_converter.h
224 proof/alethe/alethe_node_converter.cpp
225 proof/alethe/alethe_node_converter.h
226 proof/alethe/alethe_post_processor.cpp
227 proof/alethe/alethe_post_processor.h
228 proof/alethe/alethe_printer.h
229 proof/alethe/alethe_printer.cpp
230 proof/alethe/alethe_proof_rule.cpp
231 proof/alethe/alethe_proof_rule.h
236 prop/cryptominisat.cpp
240 prop/opt_clauses_manager.cpp
241 prop/opt_clauses_manager.h
242 prop/proof_cnf_stream.cpp
243 prop/proof_cnf_stream.h
244 prop/minisat/core/Dimacs.h
245 prop/minisat/core/Solver.cc
246 prop/minisat/core/Solver.h
247 prop/minisat/core/SolverTypes.h
248 prop/minisat/minisat.cpp
249 prop/minisat/minisat.h
250 prop/minisat/mtl/Alg.h
251 prop/minisat/mtl/Alloc.h
252 prop/minisat/mtl/Heap.h
253 prop/minisat/mtl/IntTypes.h
254 prop/minisat/mtl/Map.h
255 prop/minisat/mtl/Queue.h
256 prop/minisat/mtl/Sort.h
257 prop/minisat/mtl/Vec.h
258 prop/minisat/mtl/XAlloc.h
259 prop/minisat/simp/SimpSolver.cc
260 prop/minisat/simp/SimpSolver.h
261 prop/minisat/utils/Options.h
262 prop/proof_post_processor.cpp
263 prop/proof_post_processor.h
266 prop/prop_proof_manager.cpp
267 prop/prop_proof_manager.h
270 prop/sat_proof_manager.cpp
271 prop/sat_proof_manager.h
272 prop/sat_solver_factory.cpp
273 prop/sat_solver_factory.h
274 prop/sat_solver_types.cpp
275 prop/sat_solver_types.h
276 prop/skolem_def_manager.cpp
277 prop/skolem_def_manager.h
278 prop/theory_proxy.cpp
280 prop/zero_level_learner.cpp
281 prop/zero_level_learner.h
282 smt/abduction_solver.cpp
283 smt/abduction_solver.h
284 smt/abstract_values.cpp
285 smt/abstract_values.h
292 smt/difficulty_post_processor.cpp
293 smt/difficulty_post_processor.h
298 smt/expand_definitions.cpp
299 smt/expand_definitions.h
302 smt/logic_exception.h
303 smt/interpolation_solver.cpp
304 smt/interpolation_solver.h
307 smt/model_core_builder.cpp
308 smt/model_core_builder.h
309 smt/model_blocker.cpp
311 smt/optimization_solver.cpp
312 smt/optimization_solver.h
313 smt/quant_elim_solver.cpp
314 smt/quant_elim_solver.h
317 smt/preprocess_proof_generator.cpp
318 smt/preprocess_proof_generator.h
319 smt/print_benchmark.cpp
320 smt/print_benchmark.h
321 smt/process_assertions.cpp
322 smt/process_assertions.h
323 smt/proof_manager.cpp
325 smt/proof_final_callback.cpp
326 smt/proof_final_callback.h
327 smt/proof_post_processor.cpp
328 smt/proof_post_processor.h
331 smt/solver_engine.cpp
333 smt/solver_engine_scope.cpp
334 smt/solver_engine_scope.h
335 smt/solver_engine_state.cpp
336 smt/solver_engine_state.h
337 smt/solver_engine_stats.cpp
338 smt/solver_engine_stats.h
343 smt/smt_statistics_registry.cpp
344 smt/smt_statistics_registry.h
347 smt/term_formula_removal.cpp
348 smt/term_formula_removal.h
349 smt/unsat_core_manager.cpp
350 smt/unsat_core_manager.h
353 smt_util/boolean_simplification.cpp
354 smt_util/boolean_simplification.h
355 theory/arith/approx_simplex.cpp
356 theory/arith/approx_simplex.h
357 theory/arith/arith_evaluator.cpp
358 theory/arith/arith_evaluator.h
359 theory/arith/arith_ite_utils.cpp
360 theory/arith/arith_ite_utils.h
361 theory/arith/arith_msum.cpp
362 theory/arith/arith_msum.h
363 theory/arith/arith_poly_norm.cpp
364 theory/arith/arith_poly_norm.h
365 theory/arith/arith_preprocess.cpp
366 theory/arith/arith_preprocess.h
367 theory/arith/arith_rewriter.cpp
368 theory/arith/arith_rewriter.h
369 theory/arith/arith_state.cpp
370 theory/arith/arith_state.h
371 theory/arith/arith_static_learner.cpp
372 theory/arith/arith_static_learner.h
373 theory/arith/arith_utilities.cpp
374 theory/arith/arith_utilities.h
375 theory/arith/arithvar.cpp
376 theory/arith/arithvar.h
377 theory/arith/attempt_solution_simplex.cpp
378 theory/arith/attempt_solution_simplex.h
379 theory/arith/bound_counts.h
380 theory/arith/bound_inference.cpp
381 theory/arith/bound_inference.h
382 theory/arith/branch_and_bound.cpp
383 theory/arith/branch_and_bound.h
384 theory/arith/callbacks.cpp
385 theory/arith/callbacks.h
386 theory/arith/congruence_manager.cpp
387 theory/arith/congruence_manager.h
388 theory/arith/constraint.cpp
389 theory/arith/constraint.h
390 theory/arith/constraint_forward.h
391 theory/arith/cut_log.cpp
392 theory/arith/cut_log.h
393 theory/arith/delta_rational.cpp
394 theory/arith/delta_rational.h
395 theory/arith/dio_solver.cpp
396 theory/arith/dio_solver.h
397 theory/arith/dual_simplex.cpp
398 theory/arith/dual_simplex.h
399 theory/arith/equality_solver.cpp
400 theory/arith/equality_solver.h
401 theory/arith/error_set.cpp
402 theory/arith/error_set.h
403 theory/arith/fc_simplex.cpp
404 theory/arith/fc_simplex.h
405 theory/arith/infer_bounds.cpp
406 theory/arith/infer_bounds.h
407 theory/arith/inference_manager.cpp
408 theory/arith/inference_manager.h
409 theory/arith/linear_equality.cpp
410 theory/arith/linear_equality.h
411 theory/arith/matrix.cpp
412 theory/arith/matrix.h
413 theory/arith/nl/cad_solver.cpp
414 theory/arith/nl/cad_solver.h
415 theory/arith/nl/cad/cdcac.cpp
416 theory/arith/nl/cad/cdcac.h
417 theory/arith/nl/cad/cdcac_utils.cpp
418 theory/arith/nl/cad/cdcac_utils.h
419 theory/arith/nl/cad/constraints.cpp
420 theory/arith/nl/cad/constraints.h
421 theory/arith/nl/cad/lazard_evaluation.cpp
422 theory/arith/nl/cad/lazard_evaluation.h
423 theory/arith/nl/cad/projections.cpp
424 theory/arith/nl/cad/projections.h
425 theory/arith/nl/cad/proof_checker.cpp
426 theory/arith/nl/cad/proof_checker.h
427 theory/arith/nl/cad/proof_generator.cpp
428 theory/arith/nl/cad/proof_generator.h
429 theory/arith/nl/cad/variable_ordering.cpp
430 theory/arith/nl/cad/variable_ordering.h
431 theory/arith/nl/equality_substitution.cpp
432 theory/arith/nl/equality_substitution.h
433 theory/arith/nl/ext/constraint.cpp
434 theory/arith/nl/ext/constraint.h
435 theory/arith/nl/ext/factoring_check.cpp
436 theory/arith/nl/ext/factoring_check.h
437 theory/arith/nl/ext/monomial.cpp
438 theory/arith/nl/ext/monomial.h
439 theory/arith/nl/ext/monomial_bounds_check.cpp
440 theory/arith/nl/ext/monomial_bounds_check.h
441 theory/arith/nl/ext/monomial_check.cpp
442 theory/arith/nl/ext/monomial_check.h
443 theory/arith/nl/ext/ext_state.cpp
444 theory/arith/nl/ext/ext_state.h
445 theory/arith/nl/ext/proof_checker.cpp
446 theory/arith/nl/ext/proof_checker.h
447 theory/arith/nl/ext/split_zero_check.cpp
448 theory/arith/nl/ext/split_zero_check.h
449 theory/arith/nl/ext/tangent_plane_check.cpp
450 theory/arith/nl/ext/tangent_plane_check.h
451 theory/arith/nl/ext_theory_callback.cpp
452 theory/arith/nl/ext_theory_callback.h
453 theory/arith/nl/iand_solver.cpp
454 theory/arith/nl/iand_solver.h
455 theory/arith/nl/icp/candidate.cpp
456 theory/arith/nl/icp/candidate.h
457 theory/arith/nl/icp/contraction_origins.cpp
458 theory/arith/nl/icp/contraction_origins.h
459 theory/arith/nl/icp/icp_solver.cpp
460 theory/arith/nl/icp/icp_solver.h
461 theory/arith/nl/icp/intersection.cpp
462 theory/arith/nl/icp/intersection.h
463 theory/arith/nl/iand_utils.cpp
464 theory/arith/nl/iand_utils.h
465 theory/arith/nl/nl_lemma_utils.cpp
466 theory/arith/nl/nl_lemma_utils.h
467 theory/arith/nl/nl_model.cpp
468 theory/arith/nl/nl_model.h
469 theory/arith/nl/nonlinear_extension.cpp
470 theory/arith/nl/nonlinear_extension.h
471 theory/arith/nl/poly_conversion.cpp
472 theory/arith/nl/poly_conversion.h
473 theory/arith/nl/pow2_solver.cpp
474 theory/arith/nl/pow2_solver.h
475 theory/arith/nl/stats.cpp
476 theory/arith/nl/stats.h
477 theory/arith/nl/strategy.cpp
478 theory/arith/nl/strategy.h
479 theory/arith/nl/transcendental/exponential_solver.cpp
480 theory/arith/nl/transcendental/exponential_solver.h
481 theory/arith/nl/transcendental/proof_checker.cpp
482 theory/arith/nl/transcendental/proof_checker.h
483 theory/arith/nl/transcendental/sine_solver.cpp
484 theory/arith/nl/transcendental/sine_solver.h
485 theory/arith/nl/transcendental/taylor_generator.cpp
486 theory/arith/nl/transcendental/taylor_generator.h
487 theory/arith/nl/transcendental/transcendental_solver.cpp
488 theory/arith/nl/transcendental/transcendental_solver.h
489 theory/arith/nl/transcendental/transcendental_state.cpp
490 theory/arith/nl/transcendental/transcendental_state.h
491 theory/arith/normal_form.cpp
492 theory/arith/normal_form.h
493 theory/arith/operator_elim.cpp
494 theory/arith/operator_elim.h
495 theory/arith/partial_model.cpp
496 theory/arith/partial_model.h
497 theory/arith/pp_rewrite_eq.cpp
498 theory/arith/pp_rewrite_eq.h
499 theory/arith/proof_checker.cpp
500 theory/arith/proof_checker.h
501 theory/arith/rewriter/node_utils.cpp
502 theory/arith/rewriter/node_utils.h
503 theory/arith/rewriter/ordering.h
504 theory/arith/rewrites.cpp
505 theory/arith/rewrites.h
506 theory/arith/simplex.cpp
507 theory/arith/simplex.h
508 theory/arith/simplex_update.cpp
509 theory/arith/simplex_update.h
510 theory/arith/soi_simplex.cpp
511 theory/arith/soi_simplex.h
512 theory/arith/tableau.cpp
513 theory/arith/tableau.h
514 theory/arith/tableau_sizes.cpp
515 theory/arith/tableau_sizes.h
516 theory/arith/theory_arith.cpp
517 theory/arith/theory_arith.h
518 theory/arith/theory_arith_private.cpp
519 theory/arith/theory_arith_private.h
520 theory/arith/theory_arith_type_rules.cpp
521 theory/arith/theory_arith_type_rules.h
522 theory/arith/type_enumerator.h
523 theory/arrays/array_info.cpp
524 theory/arrays/array_info.h
525 theory/arrays/inference_manager.cpp
526 theory/arrays/inference_manager.h
527 theory/arrays/proof_checker.cpp
528 theory/arrays/proof_checker.h
529 theory/arrays/skolem_cache.cpp
530 theory/arrays/skolem_cache.h
531 theory/arrays/theory_arrays.cpp
532 theory/arrays/theory_arrays.h
533 theory/arrays/theory_arrays_rewriter.cpp
534 theory/arrays/theory_arrays_rewriter.h
535 theory/arrays/theory_arrays_type_rules.cpp
536 theory/arrays/theory_arrays_type_rules.h
537 theory/arrays/type_enumerator.h
538 theory/arrays/type_enumerator.cpp
539 theory/arrays/union_find.cpp
540 theory/arrays/union_find.h
543 theory/atom_requests.cpp
544 theory/atom_requests.h
545 theory/bags/bag_make_op.cpp
546 theory/bags/bag_make_op.h
547 theory/bags/bags_rewriter.cpp
548 theory/bags/bags_rewriter.h
549 theory/bags/bag_solver.cpp
550 theory/bags/bag_solver.h
551 theory/bags/bag_reduction.cpp
552 theory/bags/bag_reduction.h
553 theory/bags/bags_statistics.cpp
554 theory/bags/bags_statistics.h
555 theory/bags/bags_utils.cpp
556 theory/bags/bags_utils.h
557 theory/bags/card_solver.cpp
558 theory/bags/card_solver.h
559 theory/bags/infer_info.cpp
560 theory/bags/infer_info.h
561 theory/bags/inference_generator.cpp
562 theory/bags/inference_generator.h
563 theory/bags/inference_manager.cpp
564 theory/bags/inference_manager.h
565 theory/bags/rewrites.cpp
566 theory/bags/rewrites.h
567 theory/bags/solver_state.cpp
568 theory/bags/solver_state.h
569 theory/bags/strategy.cpp
570 theory/bags/strategy.h
571 theory/bags/term_registry.cpp
572 theory/bags/term_registry.h
573 theory/bags/theory_bags.cpp
574 theory/bags/theory_bags.h
575 theory/bags/theory_bags_type_enumerator.cpp
576 theory/bags/theory_bags_type_enumerator.h
577 theory/bags/theory_bags_type_rules.h
578 theory/bags/theory_bags_type_rules.cpp
579 theory/booleans/circuit_propagator.cpp
580 theory/booleans/circuit_propagator.h
581 theory/booleans/proof_circuit_propagator.cpp
582 theory/booleans/proof_circuit_propagator.h
583 theory/booleans/proof_checker.cpp
584 theory/booleans/proof_checker.h
585 theory/booleans/theory_bool.cpp
586 theory/booleans/theory_bool.h
587 theory/booleans/theory_bool_rewriter.cpp
588 theory/booleans/theory_bool_rewriter.h
589 theory/booleans/theory_bool_type_rules.cpp
590 theory/booleans/theory_bool_type_rules.h
591 theory/booleans/type_enumerator.h
592 theory/builtin/proof_checker.cpp
593 theory/builtin/proof_checker.h
594 theory/builtin/theory_builtin.cpp
595 theory/builtin/theory_builtin.h
596 theory/builtin/theory_builtin_rewriter.cpp
597 theory/builtin/theory_builtin_rewriter.h
598 theory/builtin/theory_builtin_type_rules.cpp
599 theory/builtin/theory_builtin_type_rules.h
600 theory/builtin/type_enumerator.cpp
601 theory/builtin/type_enumerator.h
602 theory/bv/bitblast/bitblast_proof_generator.cpp
603 theory/bv/bitblast/bitblast_proof_generator.h
604 theory/bv/bitblast/bitblast_strategies_template.h
605 theory/bv/bitblast/bitblast_utils.h
606 theory/bv/bitblast/bitblaster.h
607 theory/bv/bitblast/node_bitblaster.cpp
608 theory/bv/bitblast/node_bitblaster.h
609 theory/bv/bitblast/proof_bitblaster.cpp
610 theory/bv/bitblast/proof_bitblaster.h
611 theory/bv/bv_solver.h
612 theory/bv/bv_solver_bitblast.cpp
613 theory/bv/bv_solver_bitblast.h
614 theory/bv/bv_solver_bitblast_internal.cpp
615 theory/bv/bv_solver_bitblast_internal.h
616 theory/bv/int_blaster.cpp
617 theory/bv/int_blaster.h
618 theory/bv/proof_checker.cpp
619 theory/bv/proof_checker.h
620 theory/bv/theory_bv.cpp
621 theory/bv/theory_bv.h
622 theory/bv/theory_bv_rewrite_rules.h
623 theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
624 theory/bv/theory_bv_rewrite_rules_core.h
625 theory/bv/theory_bv_rewrite_rules_normalization.h
626 theory/bv/theory_bv_rewrite_rules_operator_elimination.h
627 theory/bv/theory_bv_rewrite_rules_simplification.h
628 theory/bv/theory_bv_rewriter.cpp
629 theory/bv/theory_bv_rewriter.h
630 theory/bv/theory_bv_type_rules.cpp
631 theory/bv/theory_bv_type_rules.h
632 theory/bv/theory_bv_utils.cpp
633 theory/bv/theory_bv_utils.h
634 theory/bv/type_enumerator.h
636 theory/combination_care_graph.cpp
637 theory/combination_care_graph.h
638 theory/combination_engine.cpp
639 theory/combination_engine.h
640 theory/datatypes/datatypes_rewriter.cpp
641 theory/datatypes/datatypes_rewriter.h
642 theory/datatypes/inference.cpp
643 theory/datatypes/inference.h
644 theory/datatypes/inference_manager.cpp
645 theory/datatypes/inference_manager.h
646 theory/datatypes/infer_proof_cons.cpp
647 theory/datatypes/infer_proof_cons.h
648 theory/datatypes/proof_checker.cpp
649 theory/datatypes/proof_checker.h
650 theory/datatypes/sygus_datatype_utils.cpp
651 theory/datatypes/sygus_datatype_utils.h
652 theory/datatypes/sygus_extension.cpp
653 theory/datatypes/sygus_extension.h
654 theory/datatypes/sygus_simple_sym.cpp
655 theory/datatypes/sygus_simple_sym.h
656 theory/datatypes/theory_datatypes.cpp
657 theory/datatypes/theory_datatypes.h
658 theory/datatypes/theory_datatypes_type_rules.cpp
659 theory/datatypes/theory_datatypes_type_rules.h
660 theory/datatypes/theory_datatypes_utils.cpp
661 theory/datatypes/theory_datatypes_utils.h
662 theory/datatypes/tuple_project_op.cpp
663 theory/datatypes/tuple_project_op.h
664 theory/datatypes/tuple_utils.cpp
665 theory/datatypes/tuple_utils.h
666 theory/datatypes/type_enumerator.cpp
667 theory/datatypes/type_enumerator.h
668 theory/decision_manager.cpp
669 theory/decision_manager.h
670 theory/decision_strategy.cpp
671 theory/decision_strategy.h
672 theory/difficulty_manager.cpp
673 theory/difficulty_manager.h
674 theory/ee_manager.cpp
676 theory/ee_manager_central.cpp
677 theory/ee_manager_central.h
678 theory/ee_manager_distributed.cpp
679 theory/ee_manager_distributed.h
680 theory/ee_setup_info.h
681 theory/engine_output_channel.cpp
682 theory/engine_output_channel.h
685 theory/ext_theory.cpp
687 theory/fp/fp_word_blaster.cpp
688 theory/fp/fp_word_blaster.h
689 theory/fp/fp_expand_defs.cpp
690 theory/fp/fp_expand_defs.h
691 theory/fp/theory_fp.cpp
692 theory/fp/theory_fp.h
693 theory/fp/theory_fp_rewriter.cpp
694 theory/fp/theory_fp_rewriter.h
695 theory/fp/theory_fp_type_rules.h
696 theory/fp/theory_fp_type_rules.cpp
697 theory/fp/type_enumerator.h
699 theory/incomplete_id.cpp
700 theory/incomplete_id.h
701 theory/inference_id.cpp
702 theory/inference_id.h
703 theory/inference_id_proof_annotator.cpp
704 theory/inference_id_proof_annotator.h
705 theory/inference_manager_buffered.cpp
706 theory/inference_manager_buffered.h
707 theory/logic_info.cpp
709 theory/model_manager.cpp
710 theory/model_manager.h
711 theory/model_manager_distributed.cpp
712 theory/model_manager_distributed.h
713 theory/output_channel.cpp
714 theory/output_channel.h
715 theory/quantifiers/alpha_equivalence.cpp
716 theory/quantifiers/alpha_equivalence.h
717 theory/quantifiers/bv_inverter.cpp
718 theory/quantifiers/bv_inverter.h
719 theory/quantifiers/bv_inverter_utils.cpp
720 theory/quantifiers/bv_inverter_utils.h
721 theory/quantifiers/candidate_rewrite_database.cpp
722 theory/quantifiers/candidate_rewrite_database.h
723 theory/quantifiers/candidate_rewrite_filter.cpp
724 theory/quantifiers/candidate_rewrite_filter.h
725 theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
726 theory/quantifiers/cegqi/ceg_arith_instantiator.h
727 theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
728 theory/quantifiers/cegqi/ceg_bv_instantiator.h
729 theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
730 theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
731 theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
732 theory/quantifiers/cegqi/ceg_dt_instantiator.h
733 theory/quantifiers/cegqi/ceg_instantiator.cpp
734 theory/quantifiers/cegqi/ceg_instantiator.h
735 theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
736 theory/quantifiers/cegqi/inst_strategy_cegqi.h
737 theory/quantifiers/cegqi/nested_qe.cpp
738 theory/quantifiers/cegqi/nested_qe.h
739 theory/quantifiers/cegqi/vts_term_cache.cpp
740 theory/quantifiers/cegqi/vts_term_cache.h
741 theory/quantifiers/conjecture_generator.cpp
742 theory/quantifiers/conjecture_generator.h
743 theory/quantifiers/dynamic_rewrite.cpp
744 theory/quantifiers/dynamic_rewrite.h
745 theory/quantifiers/ematching/candidate_generator.cpp
746 theory/quantifiers/ematching/candidate_generator.h
747 theory/quantifiers/ematching/ho_trigger.cpp
748 theory/quantifiers/ematching/ho_trigger.h
749 theory/quantifiers/ematching/im_generator.cpp
750 theory/quantifiers/ematching/im_generator.h
751 theory/quantifiers/ematching/inst_match_generator.cpp
752 theory/quantifiers/ematching/inst_match_generator.h
753 theory/quantifiers/ematching/inst_match_generator_multi.cpp
754 theory/quantifiers/ematching/inst_match_generator_multi.h
755 theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
756 theory/quantifiers/ematching/inst_match_generator_multi_linear.h
757 theory/quantifiers/ematching/inst_match_generator_simple.cpp
758 theory/quantifiers/ematching/inst_match_generator_simple.h
759 theory/quantifiers/ematching/inst_strategy.cpp
760 theory/quantifiers/ematching/inst_strategy.h
761 theory/quantifiers/ematching/inst_strategy_e_matching.cpp
762 theory/quantifiers/ematching/inst_strategy_e_matching.h
763 theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
764 theory/quantifiers/ematching/inst_strategy_e_matching_user.h
765 theory/quantifiers/ematching/instantiation_engine.cpp
766 theory/quantifiers/ematching/instantiation_engine.h
767 theory/quantifiers/ematching/pattern_term_selector.cpp
768 theory/quantifiers/ematching/pattern_term_selector.h
769 theory/quantifiers/ematching/relational_match_generator.cpp
770 theory/quantifiers/ematching/relational_match_generator.h
771 theory/quantifiers/ematching/trigger.cpp
772 theory/quantifiers/ematching/trigger.h
773 theory/quantifiers/ematching/trigger_database.cpp
774 theory/quantifiers/ematching/trigger_database.h
775 theory/quantifiers/ematching/trigger_term_info.cpp
776 theory/quantifiers/ematching/trigger_term_info.h
777 theory/quantifiers/ematching/trigger_trie.cpp
778 theory/quantifiers/ematching/trigger_trie.h
779 theory/quantifiers/ematching/var_match_generator.cpp
780 theory/quantifiers/ematching/var_match_generator.h
781 theory/quantifiers/entailment_check.cpp
782 theory/quantifiers/entailment_check.h
783 theory/quantifiers/equality_query.cpp
784 theory/quantifiers/equality_query.h
785 theory/quantifiers/expr_miner.cpp
786 theory/quantifiers/expr_miner.h
787 theory/quantifiers/expr_miner_manager.cpp
788 theory/quantifiers/expr_miner_manager.h
789 theory/quantifiers/extended_rewrite.cpp
790 theory/quantifiers/extended_rewrite.h
791 theory/quantifiers/first_order_model.cpp
792 theory/quantifiers/first_order_model.h
793 theory/quantifiers/fmf/bounded_integers.cpp
794 theory/quantifiers/fmf/bounded_integers.h
795 theory/quantifiers/fmf/first_order_model_fmc.cpp
796 theory/quantifiers/fmf/first_order_model_fmc.h
797 theory/quantifiers/fmf/full_model_check.cpp
798 theory/quantifiers/fmf/full_model_check.h
799 theory/quantifiers/fmf/model_builder.cpp
800 theory/quantifiers/fmf/model_builder.h
801 theory/quantifiers/fmf/model_engine.cpp
802 theory/quantifiers/fmf/model_engine.h
803 theory/quantifiers/fun_def_evaluator.cpp
804 theory/quantifiers/fun_def_evaluator.h
805 theory/quantifiers/ho_term_database.cpp
806 theory/quantifiers/ho_term_database.h
807 theory/quantifiers/index_trie.cpp
808 theory/quantifiers/index_trie.h
809 theory/quantifiers/inst_match.cpp
810 theory/quantifiers/inst_match.h
811 theory/quantifiers/inst_match_trie.cpp
812 theory/quantifiers/inst_match_trie.h
813 theory/quantifiers/inst_strategy_enumerative.cpp
814 theory/quantifiers/inst_strategy_enumerative.h
815 theory/quantifiers/inst_strategy_pool.cpp
816 theory/quantifiers/inst_strategy_pool.h
817 theory/quantifiers/instantiate.cpp
818 theory/quantifiers/instantiate.h
819 theory/quantifiers/instantiation_list.cpp
820 theory/quantifiers/instantiation_list.h
821 theory/quantifiers/lazy_trie.cpp
822 theory/quantifiers/lazy_trie.h
823 theory/quantifiers/master_eq_notify.cpp
824 theory/quantifiers/master_eq_notify.h
825 theory/quantifiers/proof_checker.cpp
826 theory/quantifiers/proof_checker.h
827 theory/quantifiers/quant_bound_inference.cpp
828 theory/quantifiers/quant_bound_inference.h
829 theory/quantifiers/quant_conflict_find.cpp
830 theory/quantifiers/quant_conflict_find.h
831 theory/quantifiers/quant_relevance.cpp
832 theory/quantifiers/quant_relevance.h
833 theory/quantifiers/quant_rep_bound_ext.cpp
834 theory/quantifiers/quant_rep_bound_ext.h
835 theory/quantifiers/quant_split.cpp
836 theory/quantifiers/quant_split.h
837 theory/quantifiers/quant_util.cpp
838 theory/quantifiers/quant_util.h
839 theory/quantifiers/quant_module.cpp
840 theory/quantifiers/quant_module.h
841 theory/quantifiers/quantifiers_attributes.cpp
842 theory/quantifiers/quantifiers_attributes.h
843 theory/quantifiers/quantifiers_inference_manager.cpp
844 theory/quantifiers/quantifiers_inference_manager.h
845 theory/quantifiers/quantifiers_macros.cpp
846 theory/quantifiers/quantifiers_macros.h
847 theory/quantifiers/quantifiers_modules.cpp
848 theory/quantifiers/quantifiers_modules.h
849 theory/quantifiers/quantifiers_preprocess.cpp
850 theory/quantifiers/quantifiers_preprocess.h
851 theory/quantifiers/quantifiers_registry.cpp
852 theory/quantifiers/quantifiers_registry.h
853 theory/quantifiers/quantifiers_rewriter.cpp
854 theory/quantifiers/quantifiers_rewriter.h
855 theory/quantifiers/quantifiers_state.cpp
856 theory/quantifiers/quantifiers_state.h
857 theory/quantifiers/quantifiers_statistics.cpp
858 theory/quantifiers/quantifiers_statistics.h
859 theory/quantifiers/query_generator.cpp
860 theory/quantifiers/query_generator.h
861 theory/quantifiers/query_generator_unsat.cpp
862 theory/quantifiers/query_generator_unsat.h
863 theory/quantifiers/relevant_domain.cpp
864 theory/quantifiers/relevant_domain.h
865 theory/quantifiers/single_inv_partition.cpp
866 theory/quantifiers/single_inv_partition.h
867 theory/quantifiers/skolemize.cpp
868 theory/quantifiers/skolemize.h
869 theory/quantifiers/solution_filter.cpp
870 theory/quantifiers/solution_filter.h
871 theory/quantifiers/term_pools.cpp
872 theory/quantifiers/term_pools.h
873 theory/quantifiers/term_tuple_enumerator.cpp
874 theory/quantifiers/term_tuple_enumerator.h
875 theory/quantifiers/sygus/ce_guided_single_inv.cpp
876 theory/quantifiers/sygus/ce_guided_single_inv.h
877 theory/quantifiers/sygus/cegis.cpp
878 theory/quantifiers/sygus/cegis.h
879 theory/quantifiers/sygus/cegis_core_connective.cpp
880 theory/quantifiers/sygus/cegis_core_connective.h
881 theory/quantifiers/sygus/cegis_unif.cpp
882 theory/quantifiers/sygus/cegis_unif.h
883 theory/quantifiers/sygus/enum_val_generator.h
884 theory/quantifiers/sygus/example_eval_cache.cpp
885 theory/quantifiers/sygus/example_eval_cache.h
886 theory/quantifiers/sygus/example_infer.cpp
887 theory/quantifiers/sygus/example_infer.h
888 theory/quantifiers/sygus/example_min_eval.cpp
889 theory/quantifiers/sygus/example_min_eval.h
890 theory/quantifiers/sygus/enum_stream_substitution.cpp
891 theory/quantifiers/sygus/enum_stream_substitution.h
892 theory/quantifiers/sygus/enum_value_manager.cpp
893 theory/quantifiers/sygus/enum_value_manager.h
894 theory/quantifiers/sygus/example_infer.cpp
895 theory/quantifiers/sygus/example_infer.h
896 theory/quantifiers/sygus/example_min_eval.cpp
897 theory/quantifiers/sygus/example_min_eval.h
898 theory/quantifiers/sygus/rcons_obligation.cpp
899 theory/quantifiers/sygus/rcons_obligation.h
900 theory/quantifiers/sygus/rcons_type_info.cpp
901 theory/quantifiers/sygus/rcons_type_info.h
902 theory/quantifiers/sygus/sygus_abduct.cpp
903 theory/quantifiers/sygus/sygus_abduct.h
904 theory/quantifiers/sygus/sygus_enumerator.cpp
905 theory/quantifiers/sygus/sygus_enumerator.h
906 theory/quantifiers/sygus/sygus_enumerator_callback.cpp
907 theory/quantifiers/sygus/sygus_enumerator_callback.h
908 theory/quantifiers/sygus/sygus_eval_unfold.cpp
909 theory/quantifiers/sygus/sygus_eval_unfold.h
910 theory/quantifiers/sygus/sygus_explain.cpp
911 theory/quantifiers/sygus/sygus_explain.h
912 theory/quantifiers/sygus/sygus_grammar_cons.cpp
913 theory/quantifiers/sygus/sygus_grammar_cons.h
914 theory/quantifiers/sygus/sygus_grammar_norm.cpp
915 theory/quantifiers/sygus/sygus_grammar_norm.h
916 theory/quantifiers/sygus/sygus_grammar_red.cpp
917 theory/quantifiers/sygus/sygus_grammar_red.h
918 theory/quantifiers/sygus/sygus_interpol.cpp
919 theory/quantifiers/sygus/sygus_interpol.h
920 theory/quantifiers/sygus/sygus_invariance.cpp
921 theory/quantifiers/sygus/sygus_invariance.h
922 theory/quantifiers/sygus/sygus_module.cpp
923 theory/quantifiers/sygus/sygus_module.h
924 theory/quantifiers/sygus/sygus_pbe.cpp
925 theory/quantifiers/sygus/sygus_pbe.h
926 theory/quantifiers/sygus/sygus_process_conj.cpp
927 theory/quantifiers/sygus/sygus_process_conj.h
928 theory/quantifiers/sygus/sygus_qe_preproc.cpp
929 theory/quantifiers/sygus/sygus_qe_preproc.h
930 theory/quantifiers/sygus/sygus_random_enumerator.cpp
931 theory/quantifiers/sygus/sygus_random_enumerator.h
932 theory/quantifiers/sygus/sygus_reconstruct.cpp
933 theory/quantifiers/sygus/sygus_reconstruct.h
934 theory/quantifiers/sygus/sygus_repair_const.cpp
935 theory/quantifiers/sygus/sygus_repair_const.h
936 theory/quantifiers/sygus/sygus_stats.cpp
937 theory/quantifiers/sygus/sygus_stats.h
938 theory/quantifiers/sygus/sygus_unif.cpp
939 theory/quantifiers/sygus/sygus_unif.h
940 theory/quantifiers/sygus/sygus_unif_io.cpp
941 theory/quantifiers/sygus/sygus_unif_io.h
942 theory/quantifiers/sygus/sygus_unif_rl.cpp
943 theory/quantifiers/sygus/sygus_unif_rl.h
944 theory/quantifiers/sygus/sygus_unif_strat.cpp
945 theory/quantifiers/sygus/sygus_unif_strat.h
946 theory/quantifiers/sygus/sygus_utils.cpp
947 theory/quantifiers/sygus/sygus_utils.h
948 theory/quantifiers/sygus/synth_conjecture.cpp
949 theory/quantifiers/sygus/synth_conjecture.h
950 theory/quantifiers/sygus/synth_engine.cpp
951 theory/quantifiers/sygus/synth_engine.h
952 theory/quantifiers/sygus/synth_verify.cpp
953 theory/quantifiers/sygus/synth_verify.h
954 theory/quantifiers/sygus/template_infer.cpp
955 theory/quantifiers/sygus/template_infer.h
956 theory/quantifiers/sygus/term_database_sygus.cpp
957 theory/quantifiers/sygus/term_database_sygus.h
958 theory/quantifiers/sygus/type_info.cpp
959 theory/quantifiers/sygus/type_info.h
960 theory/quantifiers/sygus/type_node_id_trie.cpp
961 theory/quantifiers/sygus/type_node_id_trie.h
962 theory/quantifiers/sygus/transition_inference.cpp
963 theory/quantifiers/sygus/transition_inference.h
964 theory/quantifiers/sygus_inst.cpp
965 theory/quantifiers/sygus_inst.h
966 theory/quantifiers/sygus_sampler.cpp
967 theory/quantifiers/sygus_sampler.h
968 theory/quantifiers/term_database.cpp
969 theory/quantifiers/term_database.h
970 theory/quantifiers/term_enumeration.cpp
971 theory/quantifiers/term_enumeration.h
972 theory/quantifiers/term_pools.cpp
973 theory/quantifiers/term_pools.h
974 theory/quantifiers/term_registry.cpp
975 theory/quantifiers/term_registry.h
976 theory/quantifiers/term_util.cpp
977 theory/quantifiers/term_util.h
978 theory/quantifiers/theory_quantifiers.cpp
979 theory/quantifiers/theory_quantifiers.h
980 theory/quantifiers/theory_quantifiers_type_rules.cpp
981 theory/quantifiers/theory_quantifiers_type_rules.h
982 theory/quantifiers_engine.cpp
983 theory/quantifiers_engine.h
984 theory/relevance_manager.cpp
985 theory/relevance_manager.h
990 theory/rewriter_attributes.h
991 theory/sep/theory_sep.cpp
992 theory/sep/theory_sep.h
993 theory/sep/theory_sep_rewriter.cpp
994 theory/sep/theory_sep_rewriter.h
995 theory/sep/theory_sep_type_rules.cpp
996 theory/sep/theory_sep_type_rules.h
997 theory/sets/cardinality_extension.cpp
998 theory/sets/cardinality_extension.h
999 theory/sets/inference_manager.cpp
1000 theory/sets/inference_manager.h
1001 theory/sets/normal_form.h
1002 theory/sets/rels_utils.cpp
1003 theory/sets/rels_utils.h
1004 theory/sets/singleton_op.cpp
1005 theory/sets/singleton_op.h
1006 theory/sets/skolem_cache.cpp
1007 theory/sets/skolem_cache.h
1008 theory/sets/solver_state.cpp
1009 theory/sets/solver_state.h
1010 theory/sets/term_registry.cpp
1011 theory/sets/term_registry.h
1012 theory/sets/theory_sets.cpp
1013 theory/sets/theory_sets.h
1014 theory/sets/theory_sets_private.cpp
1015 theory/sets/theory_sets_private.h
1016 theory/sets/theory_sets_rels.cpp
1017 theory/sets/theory_sets_rels.h
1018 theory/sets/theory_sets_rewriter.cpp
1019 theory/sets/theory_sets_rewriter.h
1020 theory/sets/theory_sets_type_enumerator.cpp
1021 theory/sets/theory_sets_type_enumerator.h
1022 theory/sets/theory_sets_type_rules.cpp
1023 theory/sets/theory_sets_type_rules.h
1024 theory/shared_solver.cpp
1025 theory/shared_solver.h
1026 theory/shared_solver_distributed.cpp
1027 theory/shared_solver_distributed.h
1028 theory/shared_terms_database.cpp
1029 theory/shared_terms_database.h
1030 theory/skolem_lemma.cpp
1031 theory/skolem_lemma.h
1032 theory/smt_engine_subsolver.cpp
1033 theory/smt_engine_subsolver.h
1034 theory/sort_inference.cpp
1035 theory/sort_inference.h
1036 theory/strings/array_solver.cpp
1037 theory/strings/array_solver.h
1038 theory/strings/array_core_solver.cpp
1039 theory/strings/array_core_solver.h
1040 theory/strings/arith_entail.cpp
1041 theory/strings/arith_entail.h
1042 theory/strings/base_solver.cpp
1043 theory/strings/base_solver.h
1044 theory/strings/core_solver.cpp
1045 theory/strings/core_solver.h
1046 theory/strings/eager_solver.cpp
1047 theory/strings/eager_solver.h
1048 theory/strings/extf_solver.cpp
1049 theory/strings/extf_solver.h
1050 theory/strings/eqc_info.cpp
1051 theory/strings/eqc_info.h
1052 theory/strings/infer_info.cpp
1053 theory/strings/infer_info.h
1054 theory/strings/infer_proof_cons.cpp
1055 theory/strings/infer_proof_cons.h
1056 theory/strings/inference_manager.cpp
1057 theory/strings/inference_manager.h
1058 theory/strings/normal_form.cpp
1059 theory/strings/normal_form.h
1060 theory/strings/proof_checker.cpp
1061 theory/strings/proof_checker.h
1062 theory/strings/regexp_enumerator.cpp
1063 theory/strings/regexp_enumerator.h
1064 theory/strings/regexp_elim.cpp
1065 theory/strings/regexp_elim.h
1066 theory/strings/regexp_entail.cpp
1067 theory/strings/regexp_entail.h
1068 theory/strings/regexp_operation.cpp
1069 theory/strings/regexp_operation.h
1070 theory/strings/regexp_solver.cpp
1071 theory/strings/regexp_solver.h
1072 theory/strings/rewrites.cpp
1073 theory/strings/rewrites.h
1074 theory/strings/sequences_rewriter.cpp
1075 theory/strings/sequences_rewriter.h
1076 theory/strings/sequences_stats.cpp
1077 theory/strings/sequences_stats.h
1078 theory/strings/skolem_cache.cpp
1079 theory/strings/skolem_cache.h
1080 theory/strings/solver_state.cpp
1081 theory/strings/solver_state.h
1082 theory/strings/strategy.cpp
1083 theory/strings/strategy.h
1084 theory/strings/strings_entail.cpp
1085 theory/strings/strings_entail.h
1086 theory/strings/strings_fmf.cpp
1087 theory/strings/strings_fmf.h
1088 theory/strings/strings_rewriter.cpp
1089 theory/strings/strings_rewriter.h
1090 theory/strings/theory_strings.cpp
1091 theory/strings/theory_strings.h
1092 theory/strings/theory_strings_preprocess.cpp
1093 theory/strings/theory_strings_preprocess.h
1094 theory/strings/theory_strings_type_rules.cpp
1095 theory/strings/theory_strings_type_rules.h
1096 theory/strings/theory_strings_utils.cpp
1097 theory/strings/theory_strings_utils.h
1098 theory/strings/term_registry.cpp
1099 theory/strings/term_registry.h
1100 theory/strings/type_enumerator.cpp
1101 theory/strings/type_enumerator.h
1102 theory/strings/word.cpp
1103 theory/strings/word.h
1104 theory/subs_minimize.cpp
1105 theory/subs_minimize.h
1106 theory/substitutions.cpp
1107 theory/substitutions.h
1108 theory/term_registration_visitor.cpp
1109 theory/term_registration_visitor.h
1112 theory/theory_engine.cpp
1113 theory/theory_engine.h
1114 theory/theory_engine_proof_generator.cpp
1115 theory/theory_engine_proof_generator.h
1116 theory/theory_id.cpp
1118 theory/theory_eq_notify.h
1119 theory/theory_inference.cpp
1120 theory/theory_inference.h
1121 theory/theory_inference_manager.cpp
1122 theory/theory_inference_manager.h
1123 theory/theory_model.cpp
1124 theory/theory_model.h
1125 theory/theory_model_builder.cpp
1126 theory/theory_model_builder.h
1127 theory/theory_preprocessor.cpp
1128 theory/theory_preprocessor.h
1129 theory/theory_rewriter.cpp
1130 theory/theory_rewriter.h
1131 theory/theory_state.cpp
1132 theory/theory_state.h
1133 theory/trust_substitutions.cpp
1134 theory/trust_substitutions.h
1135 theory/type_enumerator.h
1138 theory/uf/cardinality_extension.cpp
1139 theory/uf/cardinality_extension.h
1140 theory/uf/equality_engine.cpp
1141 theory/uf/equality_engine.h
1142 theory/uf/equality_engine_iterator.cpp
1143 theory/uf/equality_engine_iterator.h
1144 theory/uf/equality_engine_notify.h
1145 theory/uf/equality_engine_types.h
1146 theory/uf/eq_proof.cpp
1147 theory/uf/eq_proof.h
1148 theory/uf/function_const.cpp
1149 theory/uf/function_const.h
1150 theory/uf/lambda_lift.cpp
1151 theory/uf/lambda_lift.h
1152 theory/uf/proof_checker.cpp
1153 theory/uf/proof_checker.h
1154 theory/uf/proof_equality_engine.cpp
1155 theory/uf/proof_equality_engine.h
1156 theory/uf/ho_extension.cpp
1157 theory/uf/ho_extension.h
1158 theory/uf/lambda_lift.cpp
1159 theory/uf/lambda_lift.h
1160 theory/uf/symmetry_breaker.cpp
1161 theory/uf/symmetry_breaker.h
1162 theory/uf/theory_uf.cpp
1163 theory/uf/theory_uf.h
1164 theory/uf/theory_uf_model.cpp
1165 theory/uf/theory_uf_model.h
1166 theory/uf/theory_uf_rewriter.cpp
1167 theory/uf/theory_uf_rewriter.h
1168 theory/uf/theory_uf_type_rules.cpp
1169 theory/uf/theory_uf_type_rules.h
1170 theory/uf/type_enumerator.cpp
1171 theory/uf/type_enumerator.h
1172 theory/valuation.cpp
1176 #-----------------------------------------------------------------------------#
1177 # Add required include paths for this and all subdirectories.
1179 include_directories(include)
1180 include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
1182 #-----------------------------------------------------------------------------#
1183 # Take care of options
1185 check_python_module("toml")
1187 set(options_toml_files
1188 options/arith_options.toml
1189 options/arrays_options.toml
1190 options/base_options.toml
1191 options/booleans_options.toml
1192 options/builtin_options.toml
1193 options/bv_options.toml
1194 options/datatypes_options.toml
1195 options/decision_options.toml
1196 options/expr_options.toml
1197 options/fp_options.toml
1198 options/main_options.toml
1199 options/parser_options.toml
1200 options/printer_options.toml
1201 options/proof_options.toml
1202 options/prop_options.toml
1203 options/quantifiers_options.toml
1204 options/sep_options.toml
1205 options/sets_options.toml
1206 options/smt_options.toml
1207 options/strings_options.toml
1208 options/theory_options.toml
1209 options/uf_options.toml
1211 string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
1212 string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files})
1213 list(APPEND options_gen_cpp_files "options/options.cpp" "options/options_public.cpp" "main/options.cpp")
1214 list(APPEND options_gen_h_files "options/options.h")
1216 libcvc5_add_sources(GENERATED ${options_gen_cpp_files} ${options_gen_h_files})
1218 list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
1220 set(options_gen_doc_files "")
1224 options_gen_doc_files
1225 "${CMAKE_BINARY_DIR}/docs/options_generated.rst"
1229 # The mkoptions.py script only updates its output files if their content would
1230 # actually change. This mechanism makes sure that running the script does not
1231 # automatically trigger a full rebuild, but only a rebuild of those parts that
1232 # include files that did actually change.
1233 # This approach also means that the output files (which gen-options used to
1234 # depend on) may not actually be updated and thus cmake would keep re-running
1235 # mkoptions.py over and over again.
1236 # We thus have an artificial options.stamp file that mkoptions.py always writes
1237 # to, and can thus be used to communicate that all options files have been
1241 options/options.stamp
1243 ${CMAKE_COMMAND} -E make_directory ${CMAKE_CURRENT_BINARY_DIR}/options
1245 ${PYTHON_EXECUTABLE}
1246 ${CMAKE_CURRENT_LIST_DIR}/options/mkoptions.py
1247 ${CMAKE_CURRENT_LIST_DIR}
1249 ${CMAKE_CURRENT_BINARY_DIR}
1252 ${options_gen_cpp_files} ${options_gen_h_files} ${options_gen_doc_files}
1254 options/mkoptions.py
1255 ${options_toml_files}
1256 main/options_template.cpp
1257 options/module_template.h
1258 options/module_template.cpp
1259 options/options_public_template.cpp
1260 options/options_template.h
1261 options/options_template.cpp
1264 add_custom_target(gen-options DEPENDS options/options.stamp)
1267 #-----------------------------------------------------------------------------#
1270 ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds
1271 ${PROJECT_SOURCE_DIR}/src/theory/booleans/kinds
1272 ${PROJECT_SOURCE_DIR}/src/theory/uf/kinds
1273 ${PROJECT_SOURCE_DIR}/src/theory/arith/kinds
1274 ${PROJECT_SOURCE_DIR}/src/theory/bv/kinds
1275 ${PROJECT_SOURCE_DIR}/src/theory/fp/kinds
1276 ${PROJECT_SOURCE_DIR}/src/theory/arrays/kinds
1277 ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds
1278 ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
1279 ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
1280 ${PROJECT_SOURCE_DIR}/src/theory/bags/kinds
1281 ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
1282 ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds)
1284 #-----------------------------------------------------------------------------#
1285 # Add subdirectories
1287 add_subdirectory(base)
1288 add_subdirectory(context)
1289 add_subdirectory(expr)
1290 add_subdirectory(parser)
1291 add_subdirectory(theory)
1292 add_subdirectory(util)
1294 #-----------------------------------------------------------------------------#
1295 # All sources for libcvc5 are now collected in LIBCVC5_SRCS and (if generated)
1296 # LIBCVC5_GEN_SRCS (via libcvc5_add_sources). We can now build libcvc5.
1298 set_source_files_properties(${LIBCVC5_GEN_SRCS} PROPERTIES GENERATED TRUE)
1300 # First build the object library
1301 add_library(cvc5-obj OBJECT ${LIBCVC5_SRCS} ${LIBCVC5_GEN_SRCS})
1302 target_compile_definitions(cvc5-obj PRIVATE -D__BUILDING_CVC5LIB -Dcvc5_obj_EXPORTS)
1303 set_target_properties(cvc5-obj PROPERTIES POSITION_INDEPENDENT_CODE ON)
1304 # add_dependencies() is necessary for cmake versions before 3.21
1305 add_dependencies(cvc5-obj cvc5base cvc5context)
1306 # Add libcvc5 dependencies for generated sources.
1307 add_dependencies(cvc5-obj gen-expr gen-versioninfo gen-options gen-tags gen-theory)
1309 add_library(cvc5 $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
1311 set_target_properties(cvc5 PROPERTIES OUTPUT_NAME cvc5)
1313 # Link the shared library
1314 target_include_directories(cvc5
1316 $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
1317 $<INSTALL_INTERFACE:include>
1319 install(TARGETS cvc5
1321 LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
1322 ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
1325 include(GenerateExportHeader)
1326 generate_export_header(cvc5-obj BASE_NAME cvc5)
1328 # Add library/include dependencies
1329 add_dependencies(cvc5-obj GMP)
1330 target_include_directories(cvc5-obj PRIVATE ${GMP_INCLUDE_DIR})
1331 if(BUILD_SHARED_LIBS)
1332 target_link_libraries(cvc5 PRIVATE GMP)
1334 target_link_libraries(cvc5 PUBLIC GMP)
1338 # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime).
1339 # RT_LIBRARIES should be empty for glibc >= 2.17
1340 target_link_libraries(cvc5 PRIVATE ${RT_LIBRARIES})
1343 target_include_directories(cvc5-obj PUBLIC ${Valgrind_INCLUDE_DIR})
1346 add_dependencies(cvc5-obj CaDiCaL)
1347 target_include_directories(cvc5-obj PRIVATE ${CaDiCaL_INCLUDE_DIR})
1348 target_link_libraries(cvc5 PRIVATE CaDiCaL)
1351 add_dependencies(cvc5-obj CLN)
1352 target_include_directories(cvc5-obj PRIVATE ${CLN_INCLUDE_DIR})
1353 target_link_libraries(cvc5 PRIVATE CLN)
1355 if(USE_CRYPTOMINISAT)
1356 add_dependencies(cvc5-obj CryptoMiniSat)
1357 target_include_directories(cvc5-obj PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
1358 target_link_libraries(cvc5 PRIVATE CryptoMiniSat)
1361 add_dependencies(cvc5-obj Kissat)
1362 target_include_directories(cvc5-obj PRIVATE ${Kissat_INCLUDE_DIR})
1363 target_link_libraries(cvc5 PRIVATE Kissat)
1366 target_include_directories(cvc5-obj PRIVATE ${GLPK_INCLUDE_DIR})
1367 target_link_libraries(cvc5 PRIVATE ${GLPK_LIBRARIES})
1370 add_dependencies(cvc5-obj Polyxx)
1371 target_include_directories(cvc5-obj PRIVATE ${Poly_INCLUDE_DIR})
1372 if(BUILD_SHARED_LIBS)
1373 target_link_libraries(cvc5 PRIVATE Polyxx)
1375 target_link_libraries(cvc5 PUBLIC Polyxx)
1379 add_dependencies(cvc5-obj CoCoA)
1380 target_include_directories(cvc5-obj PRIVATE ${CoCoA_INCLUDE_DIR})
1381 target_link_libraries(cvc5 PRIVATE CoCoA)
1384 add_dependencies(cvc5-obj SymFPU)
1385 target_include_directories(cvc5-obj PRIVATE ${SymFPU_INCLUDE_DIR})
1386 target_link_libraries(cvc5 PRIVATE SymFPU)
1388 #-----------------------------------------------------------------------------#
1389 # Visit main subdirectory after creating target cvc5. For target main, we have
1390 # to manually add library dependencies since we can't use
1391 # target_link_libraries(...) with object libraries for cmake versions <= 3.12.
1392 # Thus, we can only visit main as soon as all dependencies for cvc5 are set up.
1394 add_subdirectory(main)
1396 #-----------------------------------------------------------------------------#
1397 # Install public API headers
1403 ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/)
1405 ${CMAKE_CURRENT_BINARY_DIR}/cvc5_export.h
1407 ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/)
1409 # Fix include paths for all public headers.
1410 # Note: This is a temporary fix until the new C++ API is in place.
1411 install(CODE "execute_process(COMMAND
1412 ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
1413 ${CMAKE_INSTALL_PREFIX})")