3 ## Top contributors (to current version):
4 ## Mathias Preiner, Andrew Reynolds, Gereon Kremer
5 ## This file is part of the CVC4 project.
6 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
7 ## in the top-level source directory and their institutional affiliations.
8 ## All rights reserved. See the file COPYING in the top-level source
9 ## directory for licensing information.
11 #-----------------------------------------------------------------------------#
12 # Collect libcvc4 source files
18 context/backtrackable.h
21 context/cdhashmap_forward.h
23 context/cdhashset_forward.h
24 context/cdinsert_hashmap.h
25 context/cdinsert_hashmap_forward.h
27 context/cdlist_forward.h
31 context/cdtrail_queue.h
34 context/context_mm.cpp
36 decision/decision_attributes.h
37 decision/decision_engine.cpp
38 decision/decision_engine.h
39 decision/decision_strategy.h
40 decision/justification_heuristic.cpp
41 decision/justification_heuristic.h
49 preprocessing/assertion_pipeline.cpp
50 preprocessing/assertion_pipeline.h
51 preprocessing/passes/ackermann.cpp
52 preprocessing/passes/ackermann.h
53 preprocessing/passes/apply_substs.cpp
54 preprocessing/passes/apply_substs.h
55 preprocessing/passes/bool_to_bv.cpp
56 preprocessing/passes/bool_to_bv.h
57 preprocessing/passes/bv_abstraction.cpp
58 preprocessing/passes/bv_abstraction.h
59 preprocessing/passes/bv_eager_atoms.cpp
60 preprocessing/passes/bv_eager_atoms.h
61 preprocessing/passes/bv_gauss.cpp
62 preprocessing/passes/bv_gauss.h
63 preprocessing/passes/bv_intro_pow2.cpp
64 preprocessing/passes/bv_intro_pow2.h
65 preprocessing/passes/bv_to_bool.cpp
66 preprocessing/passes/bv_to_bool.h
67 preprocessing/passes/bv_to_int.cpp
68 preprocessing/passes/bv_to_int.h
69 preprocessing/passes/extended_rewriter_pass.cpp
70 preprocessing/passes/extended_rewriter_pass.h
71 preprocessing/passes/fun_def_fmf.cpp
72 preprocessing/passes/fun_def_fmf.h
73 preprocessing/passes/global_negate.cpp
74 preprocessing/passes/global_negate.h
75 preprocessing/passes/ho_elim.cpp
76 preprocessing/passes/ho_elim.h
77 preprocessing/passes/int_to_bv.cpp
78 preprocessing/passes/int_to_bv.h
79 preprocessing/passes/ite_removal.cpp
80 preprocessing/passes/ite_removal.h
81 preprocessing/passes/ite_simp.cpp
82 preprocessing/passes/ite_simp.h
83 preprocessing/passes/miplib_trick.cpp
84 preprocessing/passes/miplib_trick.h
85 preprocessing/passes/nl_ext_purify.cpp
86 preprocessing/passes/nl_ext_purify.h
87 preprocessing/passes/non_clausal_simp.cpp
88 preprocessing/passes/non_clausal_simp.h
89 preprocessing/passes/pseudo_boolean_processor.cpp
90 preprocessing/passes/pseudo_boolean_processor.h
91 preprocessing/passes/quantifier_macros.cpp
92 preprocessing/passes/quantifier_macros.h
93 preprocessing/passes/quantifiers_preprocess.cpp
94 preprocessing/passes/quantifiers_preprocess.h
95 preprocessing/passes/real_to_int.cpp
96 preprocessing/passes/real_to_int.h
97 preprocessing/passes/rewrite.cpp
98 preprocessing/passes/rewrite.h
99 preprocessing/passes/sep_skolem_emp.cpp
100 preprocessing/passes/sep_skolem_emp.h
101 preprocessing/passes/sort_infer.cpp
102 preprocessing/passes/sort_infer.h
103 preprocessing/passes/static_learning.cpp
104 preprocessing/passes/static_learning.h
105 preprocessing/passes/sygus_inference.cpp
106 preprocessing/passes/sygus_inference.h
107 preprocessing/passes/synth_rew_rules.cpp
108 preprocessing/passes/synth_rew_rules.h
109 preprocessing/passes/theory_preprocess.cpp
110 preprocessing/passes/theory_preprocess.h
111 preprocessing/passes/unconstrained_simplifier.cpp
112 preprocessing/passes/unconstrained_simplifier.h
113 preprocessing/preprocessing_pass.cpp
114 preprocessing/preprocessing_pass.h
115 preprocessing/preprocessing_pass_context.cpp
116 preprocessing/preprocessing_pass_context.h
117 preprocessing/preprocessing_pass_registry.cpp
118 preprocessing/preprocessing_pass_registry.h
119 preprocessing/util/ite_utilities.cpp
120 preprocessing/util/ite_utilities.h
121 printer/ast/ast_printer.cpp
122 printer/ast/ast_printer.h
123 printer/cvc/cvc_printer.cpp
124 printer/cvc/cvc_printer.h
125 printer/dagification_visitor.cpp
126 printer/dagification_visitor.h
127 printer/let_binding.cpp
128 printer/let_binding.h
131 printer/smt2/smt2_printer.cpp
132 printer/smt2/smt2_printer.h
133 printer/tptp/tptp_printer.cpp
134 printer/tptp/tptp_printer.h
138 proof/proof_manager.cpp
139 proof/proof_manager.h
141 proof/sat_proof_implementation.h
144 prop/bv_sat_solver_notify.h
145 prop/bvminisat/bvminisat.cpp
146 prop/bvminisat/bvminisat.h
147 prop/bvminisat/core/Dimacs.h
148 prop/bvminisat/core/Solver.cc
149 prop/bvminisat/core/Solver.h
150 prop/bvminisat/core/SolverTypes.h
151 prop/bvminisat/mtl/Alg.h
152 prop/bvminisat/mtl/Alloc.h
153 prop/bvminisat/mtl/Heap.h
154 prop/bvminisat/mtl/IntTypes.h
155 prop/bvminisat/mtl/Map.h
156 prop/bvminisat/mtl/Queue.h
157 prop/bvminisat/mtl/Sort.h
158 prop/bvminisat/mtl/Vec.h
159 prop/bvminisat/mtl/XAlloc.h
160 prop/bvminisat/simp/SimpSolver.cc
161 prop/bvminisat/simp/SimpSolver.h
162 prop/bvminisat/utils/Options.h
167 prop/cryptominisat.cpp
171 prop/proof_cnf_stream.cpp
172 prop/proof_cnf_stream.h
173 prop/minisat/core/Dimacs.h
174 prop/minisat/core/Solver.cc
175 prop/minisat/core/Solver.h
176 prop/minisat/core/SolverTypes.h
177 prop/minisat/minisat.cpp
178 prop/minisat/minisat.h
179 prop/minisat/mtl/Alg.h
180 prop/minisat/mtl/Alloc.h
181 prop/minisat/mtl/Heap.h
182 prop/minisat/mtl/IntTypes.h
183 prop/minisat/mtl/Map.h
184 prop/minisat/mtl/Queue.h
185 prop/minisat/mtl/Sort.h
186 prop/minisat/mtl/Vec.h
187 prop/minisat/mtl/XAlloc.h
188 prop/minisat/simp/SimpSolver.cc
189 prop/minisat/simp/SimpSolver.h
190 prop/minisat/utils/Options.h
191 prop/proof_post_processor.cpp
192 prop/proof_post_processor.h
195 prop/prop_proof_manager.cpp
196 prop/prop_proof_manager.h
199 prop/sat_proof_manager.cpp
200 prop/sat_proof_manager.h
201 prop/sat_solver_factory.cpp
202 prop/sat_solver_factory.h
203 prop/sat_solver_types.cpp
204 prop/sat_solver_types.h
205 prop/theory_proxy.cpp
207 smt/abduction_solver.cpp
208 smt/abduction_solver.h
209 smt/abstract_values.cpp
210 smt/abstract_values.h
217 smt/defined_function.h
222 smt/expand_definitions.cpp
223 smt/expand_definitions.h
226 smt/logic_exception.h
227 smt/logic_request.cpp
229 smt/interpolation_solver.cpp
230 smt/interpolation_solver.h
231 smt/managed_ostreams.cpp
232 smt/managed_ostreams.h
235 smt/model_core_builder.cpp
236 smt/model_core_builder.h
237 smt/model_blocker.cpp
241 smt/options_manager.cpp
242 smt/options_manager.h
243 smt/output_manager.cpp
245 smt/quant_elim_solver.cpp
246 smt/quant_elim_solver.h
249 smt/preprocess_proof_generator.cpp
250 smt/preprocess_proof_generator.h
251 smt/process_assertions.cpp
252 smt/process_assertions.h
253 smt/proof_manager.cpp
255 smt/proof_post_processor.cpp
256 smt/proof_post_processor.h
261 smt/smt_engine_scope.cpp
262 smt/smt_engine_scope.h
263 smt/smt_engine_state.cpp
264 smt/smt_engine_state.h
265 smt/smt_engine_stats.cpp
266 smt/smt_engine_stats.h
271 smt/smt_statistics_registry.cpp
272 smt/smt_statistics_registry.h
275 smt/term_formula_removal.cpp
276 smt/term_formula_removal.h
280 smt_util/boolean_simplification.cpp
281 smt_util/boolean_simplification.h
282 smt_util/nary_builder.cpp
283 smt_util/nary_builder.h
284 theory/arith/approx_simplex.cpp
285 theory/arith/approx_simplex.h
286 theory/arith/arith_ite_utils.cpp
287 theory/arith/arith_ite_utils.h
288 theory/arith/arith_lemma.cpp
289 theory/arith/arith_lemma.h
290 theory/arith/arith_msum.cpp
291 theory/arith/arith_msum.h
292 theory/arith/arith_preprocess.cpp
293 theory/arith/arith_preprocess.h
294 theory/arith/arith_rewriter.cpp
295 theory/arith/arith_rewriter.h
296 theory/arith/arith_state.cpp
297 theory/arith/arith_state.h
298 theory/arith/arith_static_learner.cpp
299 theory/arith/arith_static_learner.h
300 theory/arith/arith_utilities.cpp
301 theory/arith/arith_utilities.h
302 theory/arith/arithvar.cpp
303 theory/arith/arithvar.h
304 theory/arith/attempt_solution_simplex.cpp
305 theory/arith/attempt_solution_simplex.h
306 theory/arith/bound_counts.h
307 theory/arith/bound_inference.cpp
308 theory/arith/bound_inference.h
309 theory/arith/callbacks.cpp
310 theory/arith/callbacks.h
311 theory/arith/congruence_manager.cpp
312 theory/arith/congruence_manager.h
313 theory/arith/constraint.cpp
314 theory/arith/constraint.h
315 theory/arith/constraint_forward.h
316 theory/arith/cut_log.cpp
317 theory/arith/cut_log.h
318 theory/arith/delta_rational.cpp
319 theory/arith/delta_rational.h
320 theory/arith/dio_solver.cpp
321 theory/arith/dio_solver.h
322 theory/arith/dual_simplex.cpp
323 theory/arith/dual_simplex.h
324 theory/arith/error_set.cpp
325 theory/arith/error_set.h
326 theory/arith/fc_simplex.cpp
327 theory/arith/fc_simplex.h
328 theory/arith/infer_bounds.cpp
329 theory/arith/infer_bounds.h
330 theory/arith/inference_id.cpp
331 theory/arith/inference_id.h
332 theory/arith/inference_manager.cpp
333 theory/arith/inference_manager.h
334 theory/arith/linear_equality.cpp
335 theory/arith/linear_equality.h
336 theory/arith/matrix.cpp
337 theory/arith/matrix.h
338 theory/arith/nl/cad_solver.cpp
339 theory/arith/nl/cad_solver.h
340 theory/arith/nl/cad/cdcac.cpp
341 theory/arith/nl/cad/cdcac.h
342 theory/arith/nl/cad/cdcac_utils.cpp
343 theory/arith/nl/cad/cdcac_utils.h
344 theory/arith/nl/cad/constraints.cpp
345 theory/arith/nl/cad/constraints.h
346 theory/arith/nl/cad/projections.cpp
347 theory/arith/nl/cad/projections.h
348 theory/arith/nl/cad/variable_ordering.cpp
349 theory/arith/nl/cad/variable_ordering.h
350 theory/arith/nl/ext/constraint.cpp
351 theory/arith/nl/ext/constraint.h
352 theory/arith/nl/ext/factoring_check.cpp
353 theory/arith/nl/ext/factoring_check.h
354 theory/arith/nl/ext/monomial.cpp
355 theory/arith/nl/ext/monomial.h
356 theory/arith/nl/ext/monomial_bounds_check.cpp
357 theory/arith/nl/ext/monomial_bounds_check.h
358 theory/arith/nl/ext/monomial_check.cpp
359 theory/arith/nl/ext/monomial_check.h
360 theory/arith/nl/ext/ext_state.cpp
361 theory/arith/nl/ext/ext_state.h
362 theory/arith/nl/ext/split_zero_check.cpp
363 theory/arith/nl/ext/split_zero_check.h
364 theory/arith/nl/ext/tangent_plane_check.cpp
365 theory/arith/nl/ext/tangent_plane_check.h
366 theory/arith/nl/ext_theory_callback.cpp
367 theory/arith/nl/ext_theory_callback.h
368 theory/arith/nl/iand_solver.cpp
369 theory/arith/nl/iand_solver.h
370 theory/arith/nl/icp/candidate.cpp
371 theory/arith/nl/icp/candidate.h
372 theory/arith/nl/icp/contraction_origins.cpp
373 theory/arith/nl/icp/contraction_origins.h
374 theory/arith/nl/icp/icp_solver.cpp
375 theory/arith/nl/icp/icp_solver.h
376 theory/arith/nl/icp/intersection.cpp
377 theory/arith/nl/icp/intersection.h
378 theory/arith/nl/iand_table.cpp
379 theory/arith/nl/iand_table.h
380 theory/arith/nl/nl_lemma_utils.cpp
381 theory/arith/nl/nl_lemma_utils.h
382 theory/arith/nl/nl_model.cpp
383 theory/arith/nl/nl_model.h
384 theory/arith/nl/nonlinear_extension.cpp
385 theory/arith/nl/nonlinear_extension.h
386 theory/arith/nl/poly_conversion.cpp
387 theory/arith/nl/poly_conversion.h
388 theory/arith/nl/stats.cpp
389 theory/arith/nl/stats.h
390 theory/arith/nl/strategy.cpp
391 theory/arith/nl/strategy.h
392 theory/arith/nl/transcendental/exponential_solver.cpp
393 theory/arith/nl/transcendental/exponential_solver.h
394 theory/arith/nl/transcendental/sine_solver.cpp
395 theory/arith/nl/transcendental/sine_solver.h
396 theory/arith/nl/transcendental/taylor_generator.cpp
397 theory/arith/nl/transcendental/taylor_generator.h
398 theory/arith/nl/transcendental/transcendental_solver.cpp
399 theory/arith/nl/transcendental/transcendental_solver.h
400 theory/arith/nl/transcendental/transcendental_state.cpp
401 theory/arith/nl/transcendental/transcendental_state.h
402 theory/arith/normal_form.cpp
403 theory/arith/normal_form.h
404 theory/arith/operator_elim.cpp
405 theory/arith/operator_elim.h
406 theory/arith/partial_model.cpp
407 theory/arith/partial_model.h
408 theory/arith/proof_checker.cpp
409 theory/arith/proof_checker.h
410 theory/arith/proof_macros.h
411 theory/arith/rewrites.cpp
412 theory/arith/rewrites.h
413 theory/arith/simplex.cpp
414 theory/arith/simplex.h
415 theory/arith/simplex_update.cpp
416 theory/arith/simplex_update.h
417 theory/arith/soi_simplex.cpp
418 theory/arith/soi_simplex.h
419 theory/arith/tableau.cpp
420 theory/arith/tableau.h
421 theory/arith/tableau_sizes.cpp
422 theory/arith/tableau_sizes.h
423 theory/arith/theory_arith.cpp
424 theory/arith/theory_arith.h
425 theory/arith/theory_arith_private.cpp
426 theory/arith/theory_arith_private.h
427 theory/arith/theory_arith_type_rules.h
428 theory/arith/type_enumerator.h
429 theory/arrays/array_info.cpp
430 theory/arrays/array_info.h
431 theory/arrays/inference_manager.cpp
432 theory/arrays/inference_manager.h
433 theory/arrays/proof_checker.cpp
434 theory/arrays/proof_checker.h
435 theory/arrays/skolem_cache.cpp
436 theory/arrays/skolem_cache.h
437 theory/arrays/theory_arrays.cpp
438 theory/arrays/theory_arrays.h
439 theory/arrays/theory_arrays_rewriter.cpp
440 theory/arrays/theory_arrays_rewriter.h
441 theory/arrays/theory_arrays_type_rules.h
442 theory/arrays/type_enumerator.h
443 theory/arrays/union_find.cpp
444 theory/arrays/union_find.h
447 theory/atom_requests.cpp
448 theory/atom_requests.h
449 theory/bags/bags_rewriter.cpp
450 theory/bags/bags_rewriter.h
451 theory/bags/bags_statistics.cpp
452 theory/bags/bags_statistics.h
453 theory/bags/inference_manager.cpp
454 theory/bags/inference_manager.h
455 theory/bags/make_bag_op.cpp
456 theory/bags/make_bag_op.h
457 theory/bags/normal_form.cpp
458 theory/bags/normal_form.h
459 theory/bags/rewrites.cpp
460 theory/bags/rewrites.h
461 theory/bags/solver_state.cpp
462 theory/bags/solver_state.h
463 theory/bags/term_registry.cpp
464 theory/bags/term_registry.h
465 theory/bags/theory_bags.cpp
466 theory/bags/theory_bags.h
467 theory/bags/theory_bags_type_enumerator.cpp
468 theory/bags/theory_bags_type_enumerator.h
469 theory/bags/theory_bags_type_rules.h
470 theory/booleans/circuit_propagator.cpp
471 theory/booleans/circuit_propagator.h
472 theory/booleans/proof_circuit_propagator.cpp
473 theory/booleans/proof_circuit_propagator.h
474 theory/booleans/proof_checker.cpp
475 theory/booleans/proof_checker.h
476 theory/booleans/theory_bool.cpp
477 theory/booleans/theory_bool.h
478 theory/booleans/theory_bool_rewriter.cpp
479 theory/booleans/theory_bool_rewriter.h
480 theory/booleans/theory_bool_type_rules.h
481 theory/booleans/type_enumerator.h
482 theory/builtin/proof_checker.cpp
483 theory/builtin/proof_checker.h
484 theory/builtin/theory_builtin.cpp
485 theory/builtin/theory_builtin.h
486 theory/builtin/theory_builtin_rewriter.cpp
487 theory/builtin/theory_builtin_rewriter.h
488 theory/builtin/theory_builtin_type_rules.cpp
489 theory/builtin/theory_builtin_type_rules.h
490 theory/builtin/type_enumerator.cpp
491 theory/builtin/type_enumerator.h
492 theory/bv/abstraction.cpp
493 theory/bv/abstraction.h
494 theory/bv/bitblast/aig_bitblaster.cpp
495 theory/bv/bitblast/aig_bitblaster.h
496 theory/bv/bitblast/bitblast_strategies_template.h
497 theory/bv/bitblast/bitblast_utils.h
498 theory/bv/bitblast/bitblaster.h
499 theory/bv/bitblast/eager_bitblaster.cpp
500 theory/bv/bitblast/eager_bitblaster.h
501 theory/bv/bitblast/lazy_bitblaster.cpp
502 theory/bv/bitblast/lazy_bitblaster.h
503 theory/bv/bv_eager_solver.cpp
504 theory/bv/bv_eager_solver.h
505 theory/bv/bv_inequality_graph.cpp
506 theory/bv/bv_inequality_graph.h
507 theory/bv/bv_quick_check.cpp
508 theory/bv/bv_quick_check.h
509 theory/bv/bv_solver.h
510 theory/bv/bv_solver_lazy.cpp
511 theory/bv/bv_solver_lazy.h
512 theory/bv/bv_solver_simple.cpp
513 theory/bv/bv_solver_simple.h
514 theory/bv/bv_subtheory.h
515 theory/bv/bv_subtheory_algebraic.cpp
516 theory/bv/bv_subtheory_algebraic.h
517 theory/bv/bv_subtheory_bitblast.cpp
518 theory/bv/bv_subtheory_bitblast.h
519 theory/bv/bv_subtheory_core.cpp
520 theory/bv/bv_subtheory_core.h
521 theory/bv/bv_subtheory_inequality.cpp
522 theory/bv/bv_subtheory_inequality.h
525 theory/bv/theory_bv.cpp
526 theory/bv/theory_bv.h
527 theory/bv/theory_bv_rewrite_rules.h
528 theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
529 theory/bv/theory_bv_rewrite_rules_core.h
530 theory/bv/theory_bv_rewrite_rules_normalization.h
531 theory/bv/theory_bv_rewrite_rules_operator_elimination.h
532 theory/bv/theory_bv_rewrite_rules_simplification.h
533 theory/bv/theory_bv_rewriter.cpp
534 theory/bv/theory_bv_rewriter.h
535 theory/bv/theory_bv_type_rules.h
536 theory/bv/theory_bv_utils.cpp
537 theory/bv/theory_bv_utils.h
538 theory/bv/type_enumerator.h
540 theory/combination_care_graph.cpp
541 theory/combination_care_graph.h
542 theory/combination_engine.cpp
543 theory/combination_engine.h
544 theory/datatypes/datatypes_rewriter.cpp
545 theory/datatypes/datatypes_rewriter.h
546 theory/datatypes/inference.cpp
547 theory/datatypes/inference.h
548 theory/datatypes/inference_manager.cpp
549 theory/datatypes/inference_manager.h
550 theory/datatypes/infer_proof_cons.cpp
551 theory/datatypes/infer_proof_cons.h
552 theory/datatypes/proof_checker.cpp
553 theory/datatypes/proof_checker.h
554 theory/datatypes/sygus_datatype_utils.cpp
555 theory/datatypes/sygus_datatype_utils.h
556 theory/datatypes/sygus_extension.cpp
557 theory/datatypes/sygus_extension.h
558 theory/datatypes/sygus_simple_sym.cpp
559 theory/datatypes/sygus_simple_sym.h
560 theory/datatypes/theory_datatypes.cpp
561 theory/datatypes/theory_datatypes.h
562 theory/datatypes/theory_datatypes_type_rules.h
563 theory/datatypes/theory_datatypes_utils.cpp
564 theory/datatypes/theory_datatypes_utils.h
565 theory/datatypes/type_enumerator.cpp
566 theory/datatypes/type_enumerator.h
567 theory/decision_manager.cpp
568 theory/decision_manager.h
569 theory/decision_strategy.cpp
570 theory/decision_strategy.h
571 theory/eager_proof_generator.cpp
572 theory/eager_proof_generator.h
573 theory/ee_manager.cpp
575 theory/ee_manager_distributed.cpp
576 theory/ee_manager_distributed.h
577 theory/ee_setup_info.h
578 theory/engine_output_channel.cpp
579 theory/engine_output_channel.h
582 theory/ext_theory.cpp
584 theory/fp/fp_converter.cpp
585 theory/fp/fp_converter.h
586 theory/fp/theory_fp.cpp
587 theory/fp/theory_fp.h
588 theory/fp/theory_fp_rewriter.cpp
589 theory/fp/theory_fp_rewriter.h
590 theory/fp/theory_fp_type_rules.h
591 theory/fp/type_enumerator.h
593 theory/inference_manager_buffered.cpp
594 theory/inference_manager_buffered.h
595 theory/logic_info.cpp
597 theory/model_manager.cpp
598 theory/model_manager.h
599 theory/model_manager_distributed.cpp
600 theory/model_manager_distributed.h
601 theory/output_channel.cpp
602 theory/output_channel.h
603 theory/quantifiers/alpha_equivalence.cpp
604 theory/quantifiers/alpha_equivalence.h
605 theory/quantifiers/anti_skolem.cpp
606 theory/quantifiers/anti_skolem.h
607 theory/quantifiers/bv_inverter.cpp
608 theory/quantifiers/bv_inverter.h
609 theory/quantifiers/bv_inverter_utils.cpp
610 theory/quantifiers/bv_inverter_utils.h
611 theory/quantifiers/candidate_rewrite_database.cpp
612 theory/quantifiers/candidate_rewrite_database.h
613 theory/quantifiers/candidate_rewrite_filter.cpp
614 theory/quantifiers/candidate_rewrite_filter.h
615 theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
616 theory/quantifiers/cegqi/ceg_arith_instantiator.h
617 theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
618 theory/quantifiers/cegqi/ceg_bv_instantiator.h
619 theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
620 theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
621 theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
622 theory/quantifiers/cegqi/ceg_dt_instantiator.h
623 theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
624 theory/quantifiers/cegqi/ceg_epr_instantiator.h
625 theory/quantifiers/cegqi/ceg_instantiator.cpp
626 theory/quantifiers/cegqi/ceg_instantiator.h
627 theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
628 theory/quantifiers/cegqi/inst_strategy_cegqi.h
629 theory/quantifiers/cegqi/nested_qe.cpp
630 theory/quantifiers/cegqi/nested_qe.h
631 theory/quantifiers/cegqi/vts_term_cache.cpp
632 theory/quantifiers/cegqi/vts_term_cache.h
633 theory/quantifiers/conjecture_generator.cpp
634 theory/quantifiers/conjecture_generator.h
635 theory/quantifiers/dynamic_rewrite.cpp
636 theory/quantifiers/dynamic_rewrite.h
637 theory/quantifiers/ematching/candidate_generator.cpp
638 theory/quantifiers/ematching/candidate_generator.h
639 theory/quantifiers/ematching/ho_trigger.cpp
640 theory/quantifiers/ematching/ho_trigger.h
641 theory/quantifiers/ematching/inst_match_generator.cpp
642 theory/quantifiers/ematching/inst_match_generator.h
643 theory/quantifiers/ematching/inst_strategy_e_matching.cpp
644 theory/quantifiers/ematching/inst_strategy_e_matching.h
645 theory/quantifiers/ematching/instantiation_engine.cpp
646 theory/quantifiers/ematching/instantiation_engine.h
647 theory/quantifiers/ematching/trigger.cpp
648 theory/quantifiers/ematching/trigger.h
649 theory/quantifiers/equality_infer.cpp
650 theory/quantifiers/equality_infer.h
651 theory/quantifiers/equality_query.cpp
652 theory/quantifiers/equality_query.h
653 theory/quantifiers/expr_miner.cpp
654 theory/quantifiers/expr_miner.h
655 theory/quantifiers/expr_miner_manager.cpp
656 theory/quantifiers/expr_miner_manager.h
657 theory/quantifiers/extended_rewrite.cpp
658 theory/quantifiers/extended_rewrite.h
659 theory/quantifiers/first_order_model.cpp
660 theory/quantifiers/first_order_model.h
661 theory/quantifiers/fmf/bounded_integers.cpp
662 theory/quantifiers/fmf/bounded_integers.h
663 theory/quantifiers/fmf/full_model_check.cpp
664 theory/quantifiers/fmf/full_model_check.h
665 theory/quantifiers/fmf/model_builder.cpp
666 theory/quantifiers/fmf/model_builder.h
667 theory/quantifiers/fmf/model_engine.cpp
668 theory/quantifiers/fmf/model_engine.h
669 theory/quantifiers/fun_def_evaluator.cpp
670 theory/quantifiers/fun_def_evaluator.h
671 theory/quantifiers/inst_match.cpp
672 theory/quantifiers/inst_match.h
673 theory/quantifiers/inst_match_trie.cpp
674 theory/quantifiers/inst_match_trie.h
675 theory/quantifiers/inst_strategy_enumerative.cpp
676 theory/quantifiers/inst_strategy_enumerative.h
677 theory/quantifiers/sygus_inst.cpp
678 theory/quantifiers/sygus_inst.h
679 theory/quantifiers/instantiate.cpp
680 theory/quantifiers/instantiate.h
681 theory/quantifiers/lazy_trie.cpp
682 theory/quantifiers/lazy_trie.h
683 theory/quantifiers/proof_checker.cpp
684 theory/quantifiers/proof_checker.h
685 theory/quantifiers/quant_conflict_find.cpp
686 theory/quantifiers/quant_conflict_find.h
687 theory/quantifiers/quant_epr.cpp
688 theory/quantifiers/quant_epr.h
689 theory/quantifiers/quant_relevance.cpp
690 theory/quantifiers/quant_relevance.h
691 theory/quantifiers/quant_rep_bound_ext.cpp
692 theory/quantifiers/quant_rep_bound_ext.h
693 theory/quantifiers/quant_split.cpp
694 theory/quantifiers/quant_split.h
695 theory/quantifiers/quant_util.cpp
696 theory/quantifiers/quant_util.h
697 theory/quantifiers/quantifiers_attributes.cpp
698 theory/quantifiers/quantifiers_attributes.h
699 theory/quantifiers/quantifiers_modules.cpp
700 theory/quantifiers/quantifiers_modules.h
701 theory/quantifiers/quantifiers_rewriter.cpp
702 theory/quantifiers/quantifiers_rewriter.h
703 theory/quantifiers/quantifiers_state.cpp
704 theory/quantifiers/quantifiers_state.h
705 theory/quantifiers/query_generator.cpp
706 theory/quantifiers/query_generator.h
707 theory/quantifiers/relevant_domain.cpp
708 theory/quantifiers/relevant_domain.h
709 theory/quantifiers/single_inv_partition.cpp
710 theory/quantifiers/single_inv_partition.h
711 theory/quantifiers/skolemize.cpp
712 theory/quantifiers/skolemize.h
713 theory/quantifiers/solution_filter.cpp
714 theory/quantifiers/solution_filter.h
715 theory/quantifiers/sygus/ce_guided_single_inv.cpp
716 theory/quantifiers/sygus/ce_guided_single_inv.h
717 theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
718 theory/quantifiers/sygus/ce_guided_single_inv_sol.h
719 theory/quantifiers/sygus/cegis.cpp
720 theory/quantifiers/sygus/cegis.h
721 theory/quantifiers/sygus/cegis_core_connective.cpp
722 theory/quantifiers/sygus/cegis_core_connective.h
723 theory/quantifiers/sygus/cegis_unif.cpp
724 theory/quantifiers/sygus/cegis_unif.h
725 theory/quantifiers/sygus/example_eval_cache.cpp
726 theory/quantifiers/sygus/example_eval_cache.h
727 theory/quantifiers/sygus/example_infer.cpp
728 theory/quantifiers/sygus/example_infer.h
729 theory/quantifiers/sygus/example_min_eval.cpp
730 theory/quantifiers/sygus/example_min_eval.h
731 theory/quantifiers/sygus/enum_stream_substitution.cpp
732 theory/quantifiers/sygus/enum_stream_substitution.h
733 theory/quantifiers/sygus/example_infer.cpp
734 theory/quantifiers/sygus/example_infer.h
735 theory/quantifiers/sygus/example_min_eval.cpp
736 theory/quantifiers/sygus/example_min_eval.h
737 theory/quantifiers/sygus/sygus_abduct.cpp
738 theory/quantifiers/sygus/sygus_abduct.h
739 theory/quantifiers/sygus/sygus_enumerator.cpp
740 theory/quantifiers/sygus/sygus_enumerator.h
741 theory/quantifiers/sygus/sygus_enumerator_basic.cpp
742 theory/quantifiers/sygus/sygus_enumerator_basic.h
743 theory/quantifiers/sygus/sygus_eval_unfold.cpp
744 theory/quantifiers/sygus/sygus_eval_unfold.h
745 theory/quantifiers/sygus/sygus_explain.cpp
746 theory/quantifiers/sygus/sygus_explain.h
747 theory/quantifiers/sygus/sygus_grammar_cons.cpp
748 theory/quantifiers/sygus/sygus_grammar_cons.h
749 theory/quantifiers/sygus/sygus_grammar_norm.cpp
750 theory/quantifiers/sygus/sygus_grammar_norm.h
751 theory/quantifiers/sygus/sygus_grammar_red.cpp
752 theory/quantifiers/sygus/sygus_grammar_red.h
753 theory/quantifiers/sygus/sygus_interpol.cpp
754 theory/quantifiers/sygus/sygus_interpol.h
755 theory/quantifiers/sygus/sygus_invariance.cpp
756 theory/quantifiers/sygus/sygus_invariance.h
757 theory/quantifiers/sygus/sygus_module.cpp
758 theory/quantifiers/sygus/sygus_module.h
759 theory/quantifiers/sygus/sygus_pbe.cpp
760 theory/quantifiers/sygus/sygus_pbe.h
761 theory/quantifiers/sygus/sygus_process_conj.cpp
762 theory/quantifiers/sygus/sygus_process_conj.h
763 theory/quantifiers/sygus/sygus_qe_preproc.cpp
764 theory/quantifiers/sygus/sygus_qe_preproc.h
765 theory/quantifiers/sygus/sygus_repair_const.cpp
766 theory/quantifiers/sygus/sygus_repair_const.h
767 theory/quantifiers/sygus/sygus_stats.cpp
768 theory/quantifiers/sygus/sygus_stats.h
769 theory/quantifiers/sygus/sygus_unif.cpp
770 theory/quantifiers/sygus/sygus_unif.h
771 theory/quantifiers/sygus/sygus_unif_io.cpp
772 theory/quantifiers/sygus/sygus_unif_io.h
773 theory/quantifiers/sygus/sygus_unif_rl.cpp
774 theory/quantifiers/sygus/sygus_unif_rl.h
775 theory/quantifiers/sygus/sygus_unif_strat.cpp
776 theory/quantifiers/sygus/sygus_unif_strat.h
777 theory/quantifiers/sygus/synth_conjecture.cpp
778 theory/quantifiers/sygus/synth_conjecture.h
779 theory/quantifiers/sygus/synth_engine.cpp
780 theory/quantifiers/sygus/synth_engine.h
781 theory/quantifiers/sygus/template_infer.cpp
782 theory/quantifiers/sygus/template_infer.h
783 theory/quantifiers/sygus/term_database_sygus.cpp
784 theory/quantifiers/sygus/term_database_sygus.h
785 theory/quantifiers/sygus/type_info.cpp
786 theory/quantifiers/sygus/type_info.h
787 theory/quantifiers/sygus/type_node_id_trie.cpp
788 theory/quantifiers/sygus/type_node_id_trie.h
789 theory/quantifiers/sygus/transition_inference.cpp
790 theory/quantifiers/sygus/transition_inference.h
791 theory/quantifiers/sygus_sampler.cpp
792 theory/quantifiers/sygus_sampler.h
793 theory/quantifiers/term_database.cpp
794 theory/quantifiers/term_database.h
795 theory/quantifiers/term_enumeration.cpp
796 theory/quantifiers/term_enumeration.h
797 theory/quantifiers/term_util.cpp
798 theory/quantifiers/term_util.h
799 theory/quantifiers/theory_quantifiers.cpp
800 theory/quantifiers/theory_quantifiers.h
801 theory/quantifiers/theory_quantifiers_type_rules.h
802 theory/quantifiers_engine.cpp
803 theory/quantifiers_engine.h
804 theory/relevance_manager.cpp
805 theory/relevance_manager.h
810 theory/rewriter_attributes.h
811 theory/sep/theory_sep.cpp
812 theory/sep/theory_sep.h
813 theory/sep/theory_sep_rewriter.cpp
814 theory/sep/theory_sep_rewriter.h
815 theory/sep/theory_sep_type_rules.h
816 theory/sets/cardinality_extension.cpp
817 theory/sets/cardinality_extension.h
818 theory/sets/inference_manager.cpp
819 theory/sets/inference_manager.h
820 theory/sets/normal_form.h
821 theory/sets/rels_utils.h
822 theory/sets/singleton_op.cpp
823 theory/sets/singleton_op.h
824 theory/sets/skolem_cache.cpp
825 theory/sets/skolem_cache.h
826 theory/sets/solver_state.cpp
827 theory/sets/solver_state.h
828 theory/sets/term_registry.cpp
829 theory/sets/term_registry.h
830 theory/sets/theory_sets.cpp
831 theory/sets/theory_sets.h
832 theory/sets/theory_sets_private.cpp
833 theory/sets/theory_sets_private.h
834 theory/sets/theory_sets_rels.cpp
835 theory/sets/theory_sets_rels.h
836 theory/sets/theory_sets_rewriter.cpp
837 theory/sets/theory_sets_rewriter.h
838 theory/sets/theory_sets_type_enumerator.cpp
839 theory/sets/theory_sets_type_enumerator.h
840 theory/sets/theory_sets_type_rules.h
841 theory/shared_solver.cpp
842 theory/shared_solver.h
843 theory/shared_solver_distributed.cpp
844 theory/shared_solver_distributed.h
845 theory/shared_terms_database.cpp
846 theory/shared_terms_database.h
847 theory/smt_engine_subsolver.cpp
848 theory/smt_engine_subsolver.h
849 theory/sort_inference.cpp
850 theory/sort_inference.h
851 theory/strings/arith_entail.cpp
852 theory/strings/arith_entail.h
853 theory/strings/base_solver.cpp
854 theory/strings/base_solver.h
855 theory/strings/core_solver.cpp
856 theory/strings/core_solver.h
857 theory/strings/extf_solver.cpp
858 theory/strings/extf_solver.h
859 theory/strings/eqc_info.cpp
860 theory/strings/eqc_info.h
861 theory/strings/infer_info.cpp
862 theory/strings/infer_info.h
863 theory/strings/infer_proof_cons.cpp
864 theory/strings/infer_proof_cons.h
865 theory/strings/inference_manager.cpp
866 theory/strings/inference_manager.h
867 theory/strings/normal_form.cpp
868 theory/strings/normal_form.h
869 theory/strings/proof_checker.cpp
870 theory/strings/proof_checker.h
871 theory/strings/regexp_elim.cpp
872 theory/strings/regexp_elim.h
873 theory/strings/regexp_entail.cpp
874 theory/strings/regexp_entail.h
875 theory/strings/regexp_operation.cpp
876 theory/strings/regexp_operation.h
877 theory/strings/regexp_solver.cpp
878 theory/strings/regexp_solver.h
879 theory/strings/rewrites.cpp
880 theory/strings/rewrites.h
881 theory/strings/sequences_rewriter.cpp
882 theory/strings/sequences_rewriter.h
883 theory/strings/sequences_stats.cpp
884 theory/strings/sequences_stats.h
885 theory/strings/skolem_cache.cpp
886 theory/strings/skolem_cache.h
887 theory/strings/solver_state.cpp
888 theory/strings/solver_state.h
889 theory/strings/strategy.cpp
890 theory/strings/strategy.h
891 theory/strings/strings_entail.cpp
892 theory/strings/strings_entail.h
893 theory/strings/strings_fmf.cpp
894 theory/strings/strings_fmf.h
895 theory/strings/strings_rewriter.cpp
896 theory/strings/strings_rewriter.h
897 theory/strings/theory_strings.cpp
898 theory/strings/theory_strings.h
899 theory/strings/theory_strings_preprocess.cpp
900 theory/strings/theory_strings_preprocess.h
901 theory/strings/theory_strings_type_rules.h
902 theory/strings/theory_strings_utils.cpp
903 theory/strings/theory_strings_utils.h
904 theory/strings/term_registry.cpp
905 theory/strings/term_registry.h
906 theory/strings/type_enumerator.cpp
907 theory/strings/type_enumerator.h
908 theory/strings/word.cpp
909 theory/strings/word.h
910 theory/subs_minimize.cpp
911 theory/subs_minimize.h
912 theory/substitutions.cpp
913 theory/substitutions.h
914 theory/term_registration_visitor.cpp
915 theory/term_registration_visitor.h
918 theory/theory_engine.cpp
919 theory/theory_engine.h
920 theory/theory_engine_proof_generator.cpp
921 theory/theory_engine_proof_generator.h
924 theory/theory_eq_notify.h
925 theory/theory_inference.cpp
926 theory/theory_inference.h
927 theory/theory_inference_manager.cpp
928 theory/theory_inference_manager.h
929 theory/theory_model.cpp
930 theory/theory_model.h
931 theory/theory_model_builder.cpp
932 theory/theory_model_builder.h
933 theory/theory_preprocessor.cpp
934 theory/theory_preprocessor.h
935 theory/theory_proof_step_buffer.cpp
936 theory/theory_proof_step_buffer.h
937 theory/theory_rewriter.cpp
938 theory/theory_rewriter.h
939 theory/theory_registrar.h
940 theory/theory_state.cpp
941 theory/theory_state.h
942 theory/theory_test_utils.h
943 theory/trust_node.cpp
945 theory/trust_substitutions.cpp
946 theory/trust_substitutions.h
947 theory/type_enumerator.h
950 theory/uf/cardinality_extension.cpp
951 theory/uf/cardinality_extension.h
952 theory/uf/equality_engine.cpp
953 theory/uf/equality_engine.h
954 theory/uf/equality_engine_iterator.cpp
955 theory/uf/equality_engine_iterator.h
956 theory/uf/equality_engine_notify.h
957 theory/uf/equality_engine_types.h
958 theory/uf/eq_proof.cpp
960 theory/uf/proof_checker.cpp
961 theory/uf/proof_checker.h
962 theory/uf/proof_equality_engine.cpp
963 theory/uf/proof_equality_engine.h
964 theory/uf/ho_extension.cpp
965 theory/uf/ho_extension.h
966 theory/uf/symmetry_breaker.cpp
967 theory/uf/symmetry_breaker.h
968 theory/uf/theory_uf.cpp
969 theory/uf/theory_uf.h
970 theory/uf/theory_uf_model.cpp
971 theory/uf/theory_uf_model.h
972 theory/uf/theory_uf_rewriter.h
973 theory/uf/theory_uf_type_rules.h
978 #-----------------------------------------------------------------------------#
979 # Add required include paths for this and all subdirectories.
981 include_directories(include)
982 include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
984 #-----------------------------------------------------------------------------#
987 ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds
988 ${PROJECT_SOURCE_DIR}/src/theory/booleans/kinds
989 ${PROJECT_SOURCE_DIR}/src/theory/uf/kinds
990 ${PROJECT_SOURCE_DIR}/src/theory/arith/kinds
991 ${PROJECT_SOURCE_DIR}/src/theory/bv/kinds
992 ${PROJECT_SOURCE_DIR}/src/theory/fp/kinds
993 ${PROJECT_SOURCE_DIR}/src/theory/arrays/kinds
994 ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds
995 ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
996 ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
997 ${PROJECT_SOURCE_DIR}/src/theory/bags/kinds
998 ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
999 ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds)
1001 #-----------------------------------------------------------------------------#
1002 # Add subdirectories
1004 add_subdirectory(base)
1005 add_subdirectory(expr)
1006 add_subdirectory(options)
1007 if (NOT BUILD_LIB_ONLY)
1008 add_subdirectory(parser)
1010 add_subdirectory(theory)
1011 add_subdirectory(util)
1013 #-----------------------------------------------------------------------------#
1014 # All sources for libcvc4 are now collected in LIBCVC4_SRCS and (if generated)
1015 # LIBCVC4_GEN_SRCS (via libcvc4_add_sources). We can now build libcvc4.
1017 set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE)
1018 add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS})
1019 target_include_directories(cvc4
1021 $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
1022 $<INSTALL_INTERFACE:include>
1025 install(TARGETS cvc4
1027 LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
1028 ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
1030 set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
1031 target_compile_definitions(cvc4
1033 -D__BUILDING_CVC4LIB
1034 -D__STDC_LIMIT_MACROS
1035 -D__STDC_FORMAT_MACROS
1037 # Add libcvc4 dependencies for generated sources.
1038 add_dependencies(cvc4 gen-expr gen-gitinfo gen-options gen-tags gen-theory)
1040 # Add library/include dependencies
1042 target_include_directories(cvc4 PRIVATE ${Valgrind_INCLUDE_DIR})
1045 target_link_libraries(cvc4 ${ABC_LIBRARIES})
1046 target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR})
1049 target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
1050 target_include_directories(cvc4 PRIVATE ${CaDiCaL_INCLUDE_DIR})
1053 target_link_libraries(cvc4 ${CLN_LIBRARIES})
1054 target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
1056 if(USE_CRYPTOMINISAT)
1057 target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
1058 target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
1061 target_link_libraries(cvc4 ${Kissat_LIBRARIES})
1062 target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR})
1065 target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
1066 target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
1069 target_link_libraries(cvc4 ${GLPK_LIBRARIES})
1070 target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
1073 target_link_libraries(cvc4 ${LFSC_LIBRARIES})
1074 target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
1077 target_link_libraries(cvc4 ${POLY_LIBRARIES})
1078 target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
1081 target_include_directories(cvc4
1082 PUBLIC $<BUILD_INTERFACE:${SymFPU_INCLUDE_DIR}>)
1085 # Note: When linked statically GMP needs to be linked after CLN since CLN
1087 target_link_libraries(cvc4 ${GMP_LIBRARIES})
1088 target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
1091 # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime).
1092 # RT_LIBRARIES should be empty for glibc >= 2.17
1093 target_link_libraries(cvc4 ${RT_LIBRARIES})
1095 #-----------------------------------------------------------------------------#
1096 # Visit main subdirectory after creating target cvc4. For target main, we have
1097 # to manually add library dependencies since we can't use
1098 # target_link_libraries(...) with object libraries for cmake versions <= 3.12.
1099 # Thus, we can only visit main as soon as all dependencies for cvc4 are set up.
1101 if (NOT BUILD_LIB_ONLY)
1102 add_subdirectory(main)
1105 #-----------------------------------------------------------------------------#
1107 # We define all install commands for all public headers here in one
1108 # place so that we can easily remove them as soon as we enforce the new
1111 # All (generated) headers that either include cvc4_public.h or
1112 # cvc4parser_public.h need to be listed explicitly here.
1118 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/api)
1120 base/configuration.h
1123 base/modal_exception.h
1125 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/base)
1127 context/cdhashmap_forward.h
1128 context/cdhashset_forward.h
1129 context/cdinsert_hashmap_forward.h
1130 context/cdlist_forward.h
1132 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/context)
1135 include/cvc4_public.h
1136 include/cvc4parser_public.h
1138 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4)
1140 expr/array_store_all.h
1141 expr/ascription_type.h
1146 expr/symbol_manager.h
1149 expr/uninterpreted_constant.h
1150 expr/variable_type_map.h
1151 ${CMAKE_CURRENT_BINARY_DIR}/expr/expr.h
1152 ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h
1153 ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h
1155 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/expr)
1158 options/option_exception.h
1160 options/printer_modes.h
1161 options/set_language.h
1163 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/options)
1167 parser/parser_builder.h
1168 parser/parser_exception.h
1171 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/parser)
1174 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/printer)
1178 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/proof)
1181 smt/logic_exception.h
1184 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/smt)
1189 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/theory)
1191 util/abstract_value.h
1199 util/integer_cln_imp.h
1200 util/integer_gmp_imp.h
1203 util/rational_cln_imp.h
1204 util/rational_gmp_imp.h
1205 util/real_algebraic_number_poly_imp.h
1207 util/resource_manager.h
1213 util/unsafe_interrupt_exception.h
1214 ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
1215 ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
1216 ${CMAKE_CURRENT_BINARY_DIR}/util/real_algebraic_number.h
1217 ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint_literal_symfpu.h
1219 ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/util)
1221 # Fix include paths for all public headers.
1222 # Note: This is a temporary fix until the new C++ API is in place.
1223 install(CODE "execute_process(COMMAND
1224 ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
1225 ${CMAKE_INSTALL_PREFIX})")