1 #-----------------------------------------------------------------------------#
2 # Collect libcvc4 source files
8 context/backtrackable.h
11 context/cdhashmap_forward.h
13 context/cdhashset_forward.h
14 context/cdinsert_hashmap.h
15 context/cdinsert_hashmap_forward.h
17 context/cdlist_forward.h
21 context/cdtrail_queue.h
24 context/context_mm.cpp
26 decision/decision_attributes.h
27 decision/decision_engine.cpp
28 decision/decision_engine.h
29 decision/decision_strategy.h
30 decision/justification_heuristic.cpp
31 decision/justification_heuristic.h
39 preprocessing/assertion_pipeline.cpp
40 preprocessing/assertion_pipeline.h
41 preprocessing/passes/apply_substs.cpp
42 preprocessing/passes/apply_substs.h
43 preprocessing/passes/apply_to_const.cpp
44 preprocessing/passes/apply_to_const.h
45 preprocessing/passes/bool_to_bv.cpp
46 preprocessing/passes/bool_to_bv.h
47 preprocessing/passes/bv_abstraction.cpp
48 preprocessing/passes/bv_abstraction.h
49 preprocessing/passes/bv_ackermann.cpp
50 preprocessing/passes/bv_ackermann.h
51 preprocessing/passes/bv_eager_atoms.cpp
52 preprocessing/passes/bv_eager_atoms.h
53 preprocessing/passes/bv_gauss.cpp
54 preprocessing/passes/bv_gauss.h
55 preprocessing/passes/bv_intro_pow2.cpp
56 preprocessing/passes/bv_intro_pow2.h
57 preprocessing/passes/bv_to_bool.cpp
58 preprocessing/passes/bv_to_bool.h
59 preprocessing/passes/extended_rewriter_pass.cpp
60 preprocessing/passes/extended_rewriter_pass.h
61 preprocessing/passes/global_negate.cpp
62 preprocessing/passes/global_negate.h
63 preprocessing/passes/int_to_bv.cpp
64 preprocessing/passes/int_to_bv.h
65 preprocessing/passes/ite_removal.cpp
66 preprocessing/passes/ite_removal.h
67 preprocessing/passes/ite_simp.cpp
68 preprocessing/passes/ite_simp.h
69 preprocessing/passes/miplib_trick.cpp
70 preprocessing/passes/miplib_trick.h
71 preprocessing/passes/nl_ext_purify.cpp
72 preprocessing/passes/nl_ext_purify.h
73 preprocessing/passes/non_clausal_simp.cpp
74 preprocessing/passes/non_clausal_simp.h
75 preprocessing/passes/pseudo_boolean_processor.cpp
76 preprocessing/passes/pseudo_boolean_processor.h
77 preprocessing/passes/quantifier_macros.cpp
78 preprocessing/passes/quantifier_macros.h
79 preprocessing/passes/quantifiers_preprocess.cpp
80 preprocessing/passes/quantifiers_preprocess.h
81 preprocessing/passes/real_to_int.cpp
82 preprocessing/passes/real_to_int.h
83 preprocessing/passes/rewrite.cpp
84 preprocessing/passes/rewrite.h
85 preprocessing/passes/sep_skolem_emp.cpp
86 preprocessing/passes/sep_skolem_emp.h
87 preprocessing/passes/sort_infer.cpp
88 preprocessing/passes/sort_infer.h
89 preprocessing/passes/static_learning.cpp
90 preprocessing/passes/static_learning.h
91 preprocessing/passes/sygus_abduct.cpp
92 preprocessing/passes/sygus_abduct.h
93 preprocessing/passes/sygus_inference.cpp
94 preprocessing/passes/sygus_inference.h
95 preprocessing/passes/symmetry_breaker.cpp
96 preprocessing/passes/symmetry_breaker.h
97 preprocessing/passes/symmetry_detect.cpp
98 preprocessing/passes/symmetry_detect.h
99 preprocessing/passes/synth_rew_rules.cpp
100 preprocessing/passes/synth_rew_rules.h
101 preprocessing/passes/theory_preprocess.cpp
102 preprocessing/passes/theory_preprocess.h
103 preprocessing/passes/unconstrained_simplifier.cpp
104 preprocessing/passes/unconstrained_simplifier.h
105 preprocessing/preprocessing_pass.cpp
106 preprocessing/preprocessing_pass.h
107 preprocessing/preprocessing_pass_context.cpp
108 preprocessing/preprocessing_pass_context.h
109 preprocessing/preprocessing_pass_registry.cpp
110 preprocessing/preprocessing_pass_registry.h
111 preprocessing/util/ite_utilities.cpp
112 preprocessing/util/ite_utilities.h
113 printer/ast/ast_printer.cpp
114 printer/ast/ast_printer.h
115 printer/cvc/cvc_printer.cpp
116 printer/cvc/cvc_printer.h
117 printer/dagification_visitor.cpp
118 printer/dagification_visitor.h
121 printer/smt2/smt2_printer.cpp
122 printer/smt2/smt2_printer.h
123 printer/sygus_print_callback.cpp
124 printer/sygus_print_callback.h
125 printer/tptp/tptp_printer.cpp
126 printer/tptp/tptp_printer.h
127 proof/arith_proof.cpp
129 proof/arith_proof_recorder.cpp
130 proof/arith_proof_recorder.h
131 proof/array_proof.cpp
133 proof/bitvector_proof.cpp
134 proof/bitvector_proof.h
135 proof/clausal_bitvector_proof.cpp
136 proof/clausal_bitvector_proof.h
140 proof/dimacs_printer.cpp
141 proof/dimacs_printer.h
142 proof/drat/drat_proof.cpp
143 proof/drat/drat_proof.h
144 proof/er/er_proof.cpp
146 proof/lemma_proof.cpp
148 proof/lfsc_proof_printer.cpp
149 proof/lfsc_proof_printer.h
150 proof/lrat/lrat_proof.cpp
151 proof/lrat/lrat_proof.h
153 proof/proof_manager.cpp
154 proof/proof_manager.h
155 proof/proof_output_channel.cpp
156 proof/proof_output_channel.h
157 proof/proof_utils.cpp
159 proof/resolution_bitvector_proof.cpp
160 proof/resolution_bitvector_proof.h
162 proof/sat_proof_implementation.h
163 proof/simplify_boolean_node.cpp
164 proof/simplify_boolean_node.h
165 proof/skolemization_manager.cpp
166 proof/skolemization_manager.h
167 proof/theory_proof.cpp
173 prop/bvminisat/bvminisat.cpp
174 prop/bvminisat/bvminisat.h
175 prop/bvminisat/core/Dimacs.h
176 prop/bvminisat/core/Solver.cc
177 prop/bvminisat/core/Solver.h
178 prop/bvminisat/core/SolverTypes.h
179 prop/bvminisat/mtl/Alg.h
180 prop/bvminisat/mtl/Alloc.h
181 prop/bvminisat/mtl/Heap.h
182 prop/bvminisat/mtl/IntTypes.h
183 prop/bvminisat/mtl/Map.h
184 prop/bvminisat/mtl/Queue.h
185 prop/bvminisat/mtl/Sort.h
186 prop/bvminisat/mtl/Vec.h
187 prop/bvminisat/mtl/XAlloc.h
188 prop/bvminisat/simp/SimpSolver.cc
189 prop/bvminisat/simp/SimpSolver.h
190 prop/bvminisat/utils/Options.h
195 prop/cryptominisat.cpp
197 prop/minisat/core/Dimacs.h
198 prop/minisat/core/Solver.cc
199 prop/minisat/core/Solver.h
200 prop/minisat/core/SolverTypes.h
201 prop/minisat/minisat.cpp
202 prop/minisat/minisat.h
203 prop/minisat/mtl/Alg.h
204 prop/minisat/mtl/Alloc.h
205 prop/minisat/mtl/Heap.h
206 prop/minisat/mtl/IntTypes.h
207 prop/minisat/mtl/Map.h
208 prop/minisat/mtl/Queue.h
209 prop/minisat/mtl/Sort.h
210 prop/minisat/mtl/Vec.h
211 prop/minisat/mtl/XAlloc.h
212 prop/minisat/simp/SimpSolver.cc
213 prop/minisat/simp/SimpSolver.h
214 prop/minisat/utils/Options.h
219 prop/sat_solver_factory.cpp
220 prop/sat_solver_factory.h
221 prop/bv_sat_solver_notify.h
222 prop/sat_solver_types.h
223 prop/theory_proxy.cpp
231 smt/logic_exception.h
232 smt/logic_request.cpp
234 smt/managed_ostreams.cpp
235 smt/managed_ostreams.h
238 smt/model_core_builder.cpp
239 smt/model_core_builder.h
242 smt/smt_engine_scope.cpp
243 smt/smt_engine_scope.h
244 smt/smt_statistics_registry.cpp
245 smt/smt_statistics_registry.h
246 smt/term_formula_removal.cpp
247 smt/term_formula_removal.h
249 smt_util/boolean_simplification.cpp
250 smt_util/boolean_simplification.h
251 smt_util/lemma_channels.cpp
252 smt_util/lemma_channels.h
253 smt_util/lemma_input_channel.h
254 smt_util/lemma_output_channel.h
255 smt_util/nary_builder.cpp
256 smt_util/nary_builder.h
257 smt_util/node_visitor.h
258 theory/arith/approx_simplex.cpp
259 theory/arith/approx_simplex.h
260 theory/arith/arith_ite_utils.cpp
261 theory/arith/arith_ite_utils.h
262 theory/arith/arith_msum.cpp
263 theory/arith/arith_msum.h
264 theory/arith/arith_rewriter.cpp
265 theory/arith/arith_rewriter.h
266 theory/arith/arith_static_learner.cpp
267 theory/arith/arith_static_learner.h
268 theory/arith/arith_utilities.h
269 theory/arith/arithvar.cpp
270 theory/arith/arithvar.h
271 theory/arith/attempt_solution_simplex.cpp
272 theory/arith/attempt_solution_simplex.h
273 theory/arith/bound_counts.h
274 theory/arith/callbacks.cpp
275 theory/arith/callbacks.h
276 theory/arith/congruence_manager.cpp
277 theory/arith/congruence_manager.h
278 theory/arith/constraint.cpp
279 theory/arith/constraint.h
280 theory/arith/constraint_forward.h
281 theory/arith/cut_log.cpp
282 theory/arith/cut_log.h
283 theory/arith/delta_rational.cpp
284 theory/arith/delta_rational.h
285 theory/arith/dio_solver.cpp
286 theory/arith/dio_solver.h
287 theory/arith/dual_simplex.cpp
288 theory/arith/dual_simplex.h
289 theory/arith/error_set.cpp
290 theory/arith/error_set.h
291 theory/arith/fc_simplex.cpp
292 theory/arith/fc_simplex.h
293 theory/arith/infer_bounds.cpp
294 theory/arith/infer_bounds.h
295 theory/arith/linear_equality.cpp
296 theory/arith/linear_equality.h
297 theory/arith/matrix.cpp
298 theory/arith/matrix.h
299 theory/arith/nonlinear_extension.cpp
300 theory/arith/nonlinear_extension.h
301 theory/arith/normal_form.cpp
302 theory/arith/normal_form.h
303 theory/arith/partial_model.cpp
304 theory/arith/partial_model.h
305 theory/arith/simplex.cpp
306 theory/arith/simplex.h
307 theory/arith/simplex_update.cpp
308 theory/arith/simplex_update.h
309 theory/arith/soi_simplex.cpp
310 theory/arith/soi_simplex.h
311 theory/arith/tableau.cpp
312 theory/arith/tableau.h
313 theory/arith/tableau_sizes.cpp
314 theory/arith/tableau_sizes.h
315 theory/arith/theory_arith.cpp
316 theory/arith/theory_arith.h
317 theory/arith/theory_arith_private.cpp
318 theory/arith/theory_arith_private.h
319 theory/arith/theory_arith_private_forward.h
320 theory/arith/theory_arith_type_rules.h
321 theory/arith/type_enumerator.h
322 theory/arrays/array_info.cpp
323 theory/arrays/array_info.h
324 theory/arrays/array_proof_reconstruction.cpp
325 theory/arrays/array_proof_reconstruction.h
326 theory/arrays/static_fact_manager.cpp
327 theory/arrays/static_fact_manager.h
328 theory/arrays/theory_arrays.cpp
329 theory/arrays/theory_arrays.h
330 theory/arrays/theory_arrays_rewriter.cpp
331 theory/arrays/theory_arrays_rewriter.h
332 theory/arrays/theory_arrays_type_rules.h
333 theory/arrays/type_enumerator.h
334 theory/arrays/union_find.cpp
335 theory/arrays/union_find.h
338 theory/atom_requests.cpp
339 theory/atom_requests.h
340 theory/booleans/circuit_propagator.cpp
341 theory/booleans/circuit_propagator.h
342 theory/booleans/theory_bool.cpp
343 theory/booleans/theory_bool.h
344 theory/booleans/theory_bool_rewriter.cpp
345 theory/booleans/theory_bool_rewriter.h
346 theory/booleans/theory_bool_type_rules.h
347 theory/booleans/type_enumerator.h
348 theory/builtin/theory_builtin.cpp
349 theory/builtin/theory_builtin.h
350 theory/builtin/theory_builtin_rewriter.cpp
351 theory/builtin/theory_builtin_rewriter.h
352 theory/builtin/theory_builtin_type_rules.h
353 theory/builtin/type_enumerator.cpp
354 theory/builtin/type_enumerator.h
355 theory/bv/abstraction.cpp
356 theory/bv/abstraction.h
357 theory/bv/bitblast/aig_bitblaster.cpp
358 theory/bv/bitblast/aig_bitblaster.h
359 theory/bv/bitblast/bitblast_strategies_template.h
360 theory/bv/bitblast/bitblast_utils.h
361 theory/bv/bitblast/bitblaster.h
362 theory/bv/bitblast/eager_bitblaster.cpp
363 theory/bv/bitblast/eager_bitblaster.h
364 theory/bv/bitblast/lazy_bitblaster.cpp
365 theory/bv/bitblast/lazy_bitblaster.h
366 theory/bv/bv_eager_solver.cpp
367 theory/bv/bv_eager_solver.h
368 theory/bv/bv_inequality_graph.cpp
369 theory/bv/bv_inequality_graph.h
370 theory/bv/bv_quick_check.cpp
371 theory/bv/bv_quick_check.h
372 theory/bv/bv_subtheory.h
373 theory/bv/bv_subtheory_algebraic.cpp
374 theory/bv/bv_subtheory_algebraic.h
375 theory/bv/bv_subtheory_bitblast.cpp
376 theory/bv/bv_subtheory_bitblast.h
377 theory/bv/bv_subtheory_core.cpp
378 theory/bv/bv_subtheory_core.h
379 theory/bv/bv_subtheory_inequality.cpp
380 theory/bv/bv_subtheory_inequality.h
383 theory/bv/theory_bv.cpp
384 theory/bv/theory_bv.h
385 theory/bv/theory_bv_rewrite_rules.h
386 theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
387 theory/bv/theory_bv_rewrite_rules_core.h
388 theory/bv/theory_bv_rewrite_rules_normalization.h
389 theory/bv/theory_bv_rewrite_rules_operator_elimination.h
390 theory/bv/theory_bv_rewrite_rules_simplification.h
391 theory/bv/theory_bv_rewriter.cpp
392 theory/bv/theory_bv_rewriter.h
393 theory/bv/theory_bv_type_rules.h
394 theory/bv/theory_bv_utils.cpp
395 theory/bv/theory_bv_utils.h
396 theory/bv/type_enumerator.h
398 theory/datatypes/datatypes_rewriter.cpp
399 theory/datatypes/datatypes_rewriter.h
400 theory/datatypes/datatypes_sygus.cpp
401 theory/datatypes/datatypes_sygus.h
402 theory/datatypes/sygus_simple_sym.cpp
403 theory/datatypes/sygus_simple_sym.h
404 theory/datatypes/theory_datatypes.cpp
405 theory/datatypes/theory_datatypes.h
406 theory/datatypes/theory_datatypes_type_rules.h
407 theory/datatypes/type_enumerator.cpp
408 theory/datatypes/type_enumerator.h
409 theory/decision_manager.cpp
410 theory/decision_manager.h
411 theory/decision_strategy.cpp
412 theory/decision_strategy.h
415 theory/ext_theory.cpp
417 theory/fp/fp_converter.cpp
418 theory/fp/fp_converter.h
419 theory/fp/theory_fp.cpp
420 theory/fp/theory_fp.h
421 theory/fp/theory_fp_rewriter.cpp
422 theory/fp/theory_fp_rewriter.h
423 theory/fp/theory_fp_type_rules.h
424 theory/fp/type_enumerator.h
425 theory/idl/idl_assertion.cpp
426 theory/idl/idl_assertion.h
427 theory/idl/idl_assertion_db.cpp
428 theory/idl/idl_assertion_db.h
429 theory/idl/idl_model.cpp
430 theory/idl/idl_model.h
431 theory/idl/theory_idl.cpp
432 theory/idl/theory_idl.h
434 theory/logic_info.cpp
436 theory/output_channel.h
437 theory/quantifiers/alpha_equivalence.cpp
438 theory/quantifiers/alpha_equivalence.h
439 theory/quantifiers/anti_skolem.cpp
440 theory/quantifiers/anti_skolem.h
441 theory/quantifiers/bv_inverter.cpp
442 theory/quantifiers/bv_inverter.h
443 theory/quantifiers/bv_inverter_utils.cpp
444 theory/quantifiers/bv_inverter_utils.h
445 theory/quantifiers/candidate_rewrite_database.cpp
446 theory/quantifiers/candidate_rewrite_database.h
447 theory/quantifiers/candidate_rewrite_filter.cpp
448 theory/quantifiers/candidate_rewrite_filter.h
449 theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
450 theory/quantifiers/cegqi/ceg_arith_instantiator.h
451 theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
452 theory/quantifiers/cegqi/ceg_bv_instantiator.h
453 theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
454 theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
455 theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
456 theory/quantifiers/cegqi/ceg_dt_instantiator.h
457 theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
458 theory/quantifiers/cegqi/ceg_epr_instantiator.h
459 theory/quantifiers/cegqi/ceg_instantiator.cpp
460 theory/quantifiers/cegqi/ceg_instantiator.h
461 theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
462 theory/quantifiers/cegqi/inst_strategy_cegqi.h
463 theory/quantifiers/conjecture_generator.cpp
464 theory/quantifiers/conjecture_generator.h
465 theory/quantifiers/dynamic_rewrite.cpp
466 theory/quantifiers/dynamic_rewrite.h
467 theory/quantifiers/ematching/candidate_generator.cpp
468 theory/quantifiers/ematching/candidate_generator.h
469 theory/quantifiers/ematching/ho_trigger.cpp
470 theory/quantifiers/ematching/ho_trigger.h
471 theory/quantifiers/ematching/inst_match_generator.cpp
472 theory/quantifiers/ematching/inst_match_generator.h
473 theory/quantifiers/ematching/inst_strategy_e_matching.cpp
474 theory/quantifiers/ematching/inst_strategy_e_matching.h
475 theory/quantifiers/ematching/instantiation_engine.cpp
476 theory/quantifiers/ematching/instantiation_engine.h
477 theory/quantifiers/ematching/trigger.cpp
478 theory/quantifiers/ematching/trigger.h
479 theory/quantifiers/equality_infer.cpp
480 theory/quantifiers/equality_infer.h
481 theory/quantifiers/equality_query.cpp
482 theory/quantifiers/equality_query.h
483 theory/quantifiers/expr_miner.cpp
484 theory/quantifiers/expr_miner.h
485 theory/quantifiers/expr_miner_manager.cpp
486 theory/quantifiers/expr_miner_manager.h
487 theory/quantifiers/extended_rewrite.cpp
488 theory/quantifiers/extended_rewrite.h
489 theory/quantifiers/first_order_model.cpp
490 theory/quantifiers/first_order_model.h
491 theory/quantifiers/fmf/bounded_integers.cpp
492 theory/quantifiers/fmf/bounded_integers.h
493 theory/quantifiers/fmf/full_model_check.cpp
494 theory/quantifiers/fmf/full_model_check.h
495 theory/quantifiers/fmf/model_builder.cpp
496 theory/quantifiers/fmf/model_builder.h
497 theory/quantifiers/fmf/model_engine.cpp
498 theory/quantifiers/fmf/model_engine.h
499 theory/quantifiers/fun_def_process.cpp
500 theory/quantifiers/fun_def_process.h
501 theory/quantifiers/inst_match.cpp
502 theory/quantifiers/inst_match.h
503 theory/quantifiers/inst_match_trie.cpp
504 theory/quantifiers/inst_match_trie.h
505 theory/quantifiers/inst_propagator.cpp
506 theory/quantifiers/inst_propagator.h
507 theory/quantifiers/inst_strategy_enumerative.cpp
508 theory/quantifiers/inst_strategy_enumerative.h
509 theory/quantifiers/instantiate.cpp
510 theory/quantifiers/instantiate.h
511 theory/quantifiers/lazy_trie.cpp
512 theory/quantifiers/lazy_trie.h
513 theory/quantifiers/local_theory_ext.cpp
514 theory/quantifiers/local_theory_ext.h
515 theory/quantifiers/quant_conflict_find.cpp
516 theory/quantifiers/quant_conflict_find.h
517 theory/quantifiers/quant_epr.cpp
518 theory/quantifiers/quant_epr.h
519 theory/quantifiers/quant_relevance.cpp
520 theory/quantifiers/quant_relevance.h
521 theory/quantifiers/quant_split.cpp
522 theory/quantifiers/quant_split.h
523 theory/quantifiers/quant_util.cpp
524 theory/quantifiers/quant_util.h
525 theory/quantifiers/quantifiers_attributes.cpp
526 theory/quantifiers/quantifiers_attributes.h
527 theory/quantifiers/quantifiers_rewriter.cpp
528 theory/quantifiers/quantifiers_rewriter.h
529 theory/quantifiers/query_generator.cpp
530 theory/quantifiers/query_generator.h
531 theory/quantifiers/relevant_domain.cpp
532 theory/quantifiers/relevant_domain.h
533 theory/quantifiers/rewrite_engine.cpp
534 theory/quantifiers/rewrite_engine.h
535 theory/quantifiers/single_inv_partition.cpp
536 theory/quantifiers/single_inv_partition.h
537 theory/quantifiers/skolemize.cpp
538 theory/quantifiers/skolemize.h
539 theory/quantifiers/solution_filter.cpp
540 theory/quantifiers/solution_filter.h
541 theory/quantifiers/sygus/ce_guided_single_inv.cpp
542 theory/quantifiers/sygus/ce_guided_single_inv.h
543 theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
544 theory/quantifiers/sygus/ce_guided_single_inv_sol.h
545 theory/quantifiers/sygus/cegis.cpp
546 theory/quantifiers/sygus/cegis.h
547 theory/quantifiers/sygus/cegis_unif.cpp
548 theory/quantifiers/sygus/cegis_unif.h
549 theory/quantifiers/sygus/enum_stream_substitution.cpp
550 theory/quantifiers/sygus/enum_stream_substitution.h
551 theory/quantifiers/sygus/sygus_enumerator.cpp
552 theory/quantifiers/sygus/sygus_enumerator.h
553 theory/quantifiers/sygus/sygus_eval_unfold.cpp
554 theory/quantifiers/sygus/sygus_eval_unfold.h
555 theory/quantifiers/sygus/sygus_explain.cpp
556 theory/quantifiers/sygus/sygus_explain.h
557 theory/quantifiers/sygus/sygus_grammar_cons.cpp
558 theory/quantifiers/sygus/sygus_grammar_cons.h
559 theory/quantifiers/sygus/sygus_grammar_norm.cpp
560 theory/quantifiers/sygus/sygus_grammar_norm.h
561 theory/quantifiers/sygus/sygus_grammar_red.cpp
562 theory/quantifiers/sygus/sygus_grammar_red.h
563 theory/quantifiers/sygus/sygus_invariance.cpp
564 theory/quantifiers/sygus/sygus_invariance.h
565 theory/quantifiers/sygus/sygus_module.cpp
566 theory/quantifiers/sygus/sygus_module.h
567 theory/quantifiers/sygus/sygus_pbe.cpp
568 theory/quantifiers/sygus/sygus_pbe.h
569 theory/quantifiers/sygus/sygus_process_conj.cpp
570 theory/quantifiers/sygus/sygus_process_conj.h
571 theory/quantifiers/sygus/sygus_repair_const.cpp
572 theory/quantifiers/sygus/sygus_repair_const.h
573 theory/quantifiers/sygus/sygus_unif.cpp
574 theory/quantifiers/sygus/sygus_unif.h
575 theory/quantifiers/sygus/sygus_unif_io.cpp
576 theory/quantifiers/sygus/sygus_unif_io.h
577 theory/quantifiers/sygus/sygus_unif_rl.cpp
578 theory/quantifiers/sygus/sygus_unif_rl.h
579 theory/quantifiers/sygus/sygus_unif_strat.cpp
580 theory/quantifiers/sygus/sygus_unif_strat.h
581 theory/quantifiers/sygus/synth_conjecture.cpp
582 theory/quantifiers/sygus/synth_conjecture.h
583 theory/quantifiers/sygus/synth_engine.cpp
584 theory/quantifiers/sygus/synth_engine.h
585 theory/quantifiers/sygus/term_database_sygus.cpp
586 theory/quantifiers/sygus/term_database_sygus.h
587 theory/quantifiers/sygus_sampler.cpp
588 theory/quantifiers/sygus_sampler.h
589 theory/quantifiers/term_canonize.cpp
590 theory/quantifiers/term_canonize.h
591 theory/quantifiers/term_database.cpp
592 theory/quantifiers/term_database.h
593 theory/quantifiers/term_enumeration.cpp
594 theory/quantifiers/term_enumeration.h
595 theory/quantifiers/term_util.cpp
596 theory/quantifiers/term_util.h
597 theory/quantifiers/theory_quantifiers.cpp
598 theory/quantifiers/theory_quantifiers.h
599 theory/quantifiers/theory_quantifiers_type_rules.h
600 theory/quantifiers_engine.cpp
601 theory/quantifiers_engine.h
606 theory/rewriter_attributes.h
607 theory/sep/theory_sep.cpp
608 theory/sep/theory_sep.h
609 theory/sep/theory_sep_rewriter.cpp
610 theory/sep/theory_sep_rewriter.h
611 theory/sep/theory_sep_type_rules.h
612 theory/sets/normal_form.h
613 theory/sets/rels_utils.h
614 theory/sets/theory_sets.cpp
615 theory/sets/theory_sets.h
616 theory/sets/theory_sets_private.cpp
617 theory/sets/theory_sets_private.h
618 theory/sets/theory_sets_rels.cpp
619 theory/sets/theory_sets_rels.h
620 theory/sets/theory_sets_rewriter.cpp
621 theory/sets/theory_sets_rewriter.h
622 theory/sets/theory_sets_type_enumerator.h
623 theory/sets/theory_sets_type_rules.h
624 theory/shared_terms_database.cpp
625 theory/shared_terms_database.h
626 theory/sort_inference.cpp
627 theory/sort_inference.h
628 theory/strings/normal_form.cpp
629 theory/strings/normal_form.h
630 theory/strings/regexp_elim.cpp
631 theory/strings/regexp_elim.h
632 theory/strings/regexp_operation.cpp
633 theory/strings/regexp_operation.h
634 theory/strings/regexp_solver.cpp
635 theory/strings/regexp_solver.h
636 theory/strings/skolem_cache.cpp
637 theory/strings/skolem_cache.h
638 theory/strings/theory_strings.cpp
639 theory/strings/theory_strings.h
640 theory/strings/theory_strings_preprocess.cpp
641 theory/strings/theory_strings_preprocess.h
642 theory/strings/theory_strings_rewriter.cpp
643 theory/strings/theory_strings_rewriter.h
644 theory/strings/theory_strings_type_rules.h
645 theory/strings/type_enumerator.h
646 theory/subs_minimize.cpp
647 theory/subs_minimize.h
648 theory/substitutions.cpp
649 theory/substitutions.h
650 theory/term_registration_visitor.cpp
651 theory/term_registration_visitor.h
654 theory/theory_engine.cpp
655 theory/theory_engine.h
656 theory/theory_model.cpp
657 theory/theory_model.h
658 theory/theory_model_builder.cpp
659 theory/theory_model_builder.h
660 theory/theory_registrar.h
661 theory/theory_test_utils.h
662 theory/type_enumerator.h
665 theory/uf/equality_engine.cpp
666 theory/uf/equality_engine.h
667 theory/uf/equality_engine_types.h
668 theory/uf/symmetry_breaker.cpp
669 theory/uf/symmetry_breaker.h
670 theory/uf/theory_uf.cpp
671 theory/uf/theory_uf.h
672 theory/uf/theory_uf_model.cpp
673 theory/uf/theory_uf_model.h
674 theory/uf/theory_uf_rewriter.h
675 theory/uf/theory_uf_strong_solver.cpp
676 theory/uf/theory_uf_strong_solver.h
677 theory/uf/theory_uf_type_rules.h
682 #-----------------------------------------------------------------------------#
683 # Add required include paths for this and all subdirectories.
685 include_directories(include)
686 include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
688 #-----------------------------------------------------------------------------#
689 # IMPORTANT: The order of the theories is important. It affects the order in
690 # which theory solvers are called/initialized internally. For example, strings
691 # depends on arith, quantifiers needs to come as the very last.
692 # See issue https://github.com/CVC4/CVC4/issues/2517 for more details.
695 ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds
696 ${PROJECT_SOURCE_DIR}/src/theory/booleans/kinds
697 ${PROJECT_SOURCE_DIR}/src/theory/uf/kinds
698 ${PROJECT_SOURCE_DIR}/src/theory/arith/kinds
699 ${PROJECT_SOURCE_DIR}/src/theory/bv/kinds
700 ${PROJECT_SOURCE_DIR}/src/theory/fp/kinds
701 ${PROJECT_SOURCE_DIR}/src/theory/arrays/kinds
702 ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds
703 ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
704 ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
705 ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
706 ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds
707 ${PROJECT_SOURCE_DIR}/src/theory/idl/kinds)
709 #-----------------------------------------------------------------------------#
712 add_subdirectory(base)
713 add_subdirectory(expr)
714 add_subdirectory(options)
715 add_subdirectory(parser)
716 add_subdirectory(theory)
717 add_subdirectory(util)
719 #-----------------------------------------------------------------------------#
720 # All sources for libcvc4 are now collected in LIBCVC4_SRCS and (if generated)
721 # LIBCVC4_GEN_SRCS (via libcvc4_add_sources). We can now build libcvc4.
723 set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE)
724 add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS})
725 install(TARGETS cvc4 DESTINATION lib)
727 set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
728 target_compile_definitions(cvc4
731 -D__STDC_LIMIT_MACROS
732 -D__STDC_FORMAT_MACROS
734 # Add libcvc4 dependencies for generated sources.
735 add_dependencies(cvc4 gen-expr gen-gitinfo gen-options gen-tags gen-theory)
737 # Add library/include dependencies
739 target_include_directories(cvc4 PUBLIC ${Valgrind_INCLUDE_DIR})
742 target_link_libraries(cvc4 ${ABC_LIBRARIES})
743 target_include_directories(cvc4 PUBLIC ${ABC_INCLUDE_DIR})
746 target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
747 target_include_directories(cvc4 PUBLIC ${CaDiCaL_INCLUDE_DIR})
750 target_link_libraries(cvc4 ${CLN_LIBRARIES})
751 target_include_directories(cvc4 PUBLIC ${CLN_INCLUDE_DIR})
753 if(USE_CRYPTOMINISAT)
754 target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
755 target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR})
758 target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
759 target_include_directories(cvc4 PUBLIC ${Drat2Er_INCLUDE_DIR})
762 target_link_libraries(cvc4 ${GLPK_LIBRARIES})
763 target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR})
766 target_link_libraries(cvc4 ${LFSC_LIBRARIES})
767 target_include_directories(cvc4 PUBLIC ${LFSC_INCLUDE_DIR})
770 target_include_directories(cvc4 PUBLIC ${SymFPU_INCLUDE_DIR})
773 # Note: When linked statically GMP needs to be linked after CLN since CLN
775 target_link_libraries(cvc4 ${GMP_LIBRARIES})
776 target_include_directories(cvc4 PUBLIC ${GMP_INCLUDE_DIR})
779 # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime).
780 # RT_LIBRARIES should be empty for glibc >= 2.17
781 target_link_libraries(cvc4 ${RT_LIBRARIES})
783 #-----------------------------------------------------------------------------#
784 # Visit main subdirectory after creating target cvc4. For target main, we have
785 # to manually add library dependencies since we can't use
786 # target_link_libraries(...) with object libraries for cmake versions <= 3.12.
787 # Thus, we can only visit main as soon as all dependencies for cvc4 are set up.
789 add_subdirectory(main)
791 #-----------------------------------------------------------------------------#
793 # We define all install commands for all public headers here in one
794 # place so that we can easily remove them as soon as we enforce the new
797 # All (generated) headers that either include cvc4_public.h or
798 # cvc4parser_public.h need to be listed explicitly here.
809 base/modal_exception.h
813 context/cdhashmap_forward.h
814 context/cdhashset_forward.h
815 context/cdinsert_hashmap_forward.h
816 context/cdlist_forward.h
818 include/cvc4/context)
821 include/cvc4_public.h
822 include/cvc4parser_public.h
827 expr/array_store_all.h
828 expr/ascription_type.h
838 expr/uninterpreted_constant.h
839 expr/variable_type_map.h
840 ${CMAKE_CURRENT_BINARY_DIR}/expr/expr.h
841 ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h
842 ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h
846 options/argument_extender.h
847 options/arith_heuristic_pivot_rule.h
848 options/arith_propagation_mode.h
849 options/arith_unate_lemma_mode.h
850 options/datatypes_modes.h
852 options/option_exception.h
854 options/printer_modes.h
855 options/quantifiers_modes.h
856 options/set_language.h
858 options/sygus_out_mode.h
859 options/theoryof_mode.h
861 include/cvc4/options)
865 parser/parser_builder.h
866 parser/parser_exception.h
870 printer/sygus_print_callback.h
872 include/cvc4/printer)
879 smt/logic_exception.h
884 smt_util/lemma_channels.h
885 smt_util/lemma_input_channel.h
886 smt_util/lemma_output_channel.h
888 include/cvc4/smt_util)
894 util/abstract_value.h
902 util/integer_cln_imp.h
903 util/integer_gmp_imp.h
906 util/rational_cln_imp.h
907 util/rational_gmp_imp.h
909 util/resource_manager.h
914 util/unsafe_interrupt_exception.h
915 ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
916 ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
917 ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
921 # Fix include paths for all public headers.
922 # Note: This is a temporary fix until the new C++ API is in place.
923 install(CODE "execute_process(COMMAND
924 ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
925 ${CMAKE_INSTALL_PREFIX})")