src/CMakeLists.txt

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