src/CMakeLists.txt

   1 #####################
   2 ## CMakeLists.txt
   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.
  10 ##
  11 #-----------------------------------------------------------------------------#
  12 # Collect libcvc4 source files
  13
  14 libcvc4_add_sources(
  15   api/cvc4cpp.cpp
  16   api/cvc4cpp.h
  17   api/cvc4cppkind.h
  18   context/backtrackable.h
  19   context/cddense_set.h
  20   context/cdhashmap.h
  21   context/cdhashmap_forward.h
  22   context/cdhashset.h
  23   context/cdhashset_forward.h
  24   context/cdinsert_hashmap.h
  25   context/cdinsert_hashmap_forward.h
  26   context/cdlist.h
  27   context/cdlist_forward.h
  28   context/cdmaybe.h
  29   context/cdo.h
  30   context/cdqueue.h
  31   context/cdtrail_queue.h
  32   context/context.cpp
  33   context/context.h
  34   context/context_mm.cpp
  35   context/context_mm.h
  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
  42   lib/clock_gettime.c
  43   lib/clock_gettime.h
  44   lib/ffs.c
  45   lib/ffs.h
  46   lib/replacements.h
  47   lib/strtok_r.c
  48   lib/strtok_r.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
 129   printer/printer.cpp
 130   printer/printer.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
 135   proof/clause_id.h
 136   proof/cnf_proof.cpp
 137   proof/cnf_proof.h
 138   proof/proof_manager.cpp
 139   proof/proof_manager.h
 140   proof/sat_proof.h
 141   proof/sat_proof_implementation.h
 142   proof/unsat_core.cpp
 143   proof/unsat_core.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
 163   prop/cadical.cpp
 164   prop/cadical.h
 165   prop/cnf_stream.cpp
 166   prop/cnf_stream.h
 167   prop/cryptominisat.cpp
 168   prop/cryptominisat.h
 169   prop/kissat.cpp
 170   prop/kissat.h
 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
 193   prop/prop_engine.cpp
 194   prop/prop_engine.h
 195   prop/prop_proof_manager.cpp
 196   prop/prop_proof_manager.h
 197   prop/registrar.h
 198   prop/sat_solver.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
 206   prop/theory_proxy.h
 207   smt/abduction_solver.cpp
 208   smt/abduction_solver.h
 209   smt/abstract_values.cpp
 210   smt/abstract_values.h
 211   smt/assertions.cpp
 212   smt/assertions.h
 213   smt/check_models.cpp
 214   smt/check_models.h
 215   smt/command.cpp
 216   smt/command.h
 217   smt/defined_function.h
 218   smt/dump.cpp
 219   smt/dump.h
 220   smt/dump_manager.cpp
 221   smt/dump_manager.h
 222   smt/expand_definitions.cpp
 223   smt/expand_definitions.h
 224   smt/listeners.cpp
 225   smt/listeners.h
 226   smt/logic_exception.h
 227   smt/logic_request.cpp
 228   smt/logic_request.h
 229   smt/interpolation_solver.cpp
 230   smt/interpolation_solver.h
 231   smt/managed_ostreams.cpp
 232   smt/managed_ostreams.h
 233   smt/model.cpp
 234   smt/model.h
 235   smt/model_core_builder.cpp
 236   smt/model_core_builder.h
 237   smt/model_blocker.cpp
 238   smt/model_blocker.h
 239   smt/node_command.cpp
 240   smt/node_command.h
 241   smt/options_manager.cpp
 242   smt/options_manager.h
 243   smt/output_manager.cpp
 244   smt/output_manager.h
 245   smt/quant_elim_solver.cpp
 246   smt/quant_elim_solver.h
 247   smt/preprocessor.cpp
 248   smt/preprocessor.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
 254   smt/proof_manager.h
 255   smt/proof_post_processor.cpp
 256   smt/proof_post_processor.h
 257   smt/set_defaults.cpp
 258   smt/set_defaults.h
 259   smt/smt_engine.cpp
 260   smt/smt_engine.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
 267   smt/smt_mode.cpp
 268   smt/smt_mode.h
 269   smt/smt_solver.cpp
 270   smt/smt_solver.h
 271   smt/smt_statistics_registry.cpp
 272   smt/smt_statistics_registry.h
 273   smt/sygus_solver.cpp
 274   smt/sygus_solver.h
 275   smt/term_formula_removal.cpp
 276   smt/term_formula_removal.h
 277   smt/update_ostream.h
 278   smt/witness_form.cpp
 279   smt/witness_form.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
 445   theory/assertion.cpp
 446   theory/assertion.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
 523   theory/bv/slicer.cpp
 524   theory/bv/slicer.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
 539   theory/care_graph.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
 574   theory/ee_manager.h
 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
 580   theory/evaluator.cpp
 581   theory/evaluator.h
 582   theory/ext_theory.cpp
 583   theory/ext_theory.h
 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
 592   theory/interrupted.h
 593   theory/inference_manager_buffered.cpp
 594   theory/inference_manager_buffered.h
 595   theory/logic_info.cpp
 596   theory/logic_info.h
 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
 806   theory/rep_set.cpp
 807   theory/rep_set.h
 808   theory/rewriter.cpp
 809   theory/rewriter.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
 916   theory/theory.cpp
 917   theory/theory.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
 922   theory/theory_id.cpp
 923   theory/theory_id.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
 944   theory/trust_node.h
 945   theory/trust_substitutions.cpp
 946   theory/trust_substitutions.h
 947   theory/type_enumerator.h
 948   theory/type_set.cpp
 949   theory/type_set.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
 959   theory/uf/eq_proof.h
 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
 974   theory/valuation.cpp
 975   theory/valuation.h
 976 )
 977
 978 #-----------------------------------------------------------------------------#
 979 # Add required include paths for this and all subdirectories.
 980
 981 include_directories(include)
 982 include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
 983
 984 #-----------------------------------------------------------------------------#
 985
 986 set(KINDS_FILES
 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)
1000
1001 #-----------------------------------------------------------------------------#
1002 # Add subdirectories
1003
1004 add_subdirectory(base)
1005 add_subdirectory(expr)
1006 add_subdirectory(options)
1007 if (NOT BUILD_LIB_ONLY)
1008   add_subdirectory(parser)
1009 endif()
1010 add_subdirectory(theory)
1011 add_subdirectory(util)
1012
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.
1016
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
1020   PUBLIC
1021     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
1022     $<INSTALL_INTERFACE:include>
1023 )
1024
1025 install(TARGETS cvc4
1026   EXPORT cvc4-targets
1027   LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
1028   ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
1029
1030 set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
1031 target_compile_definitions(cvc4
1032   PRIVATE
1033     -D__BUILDING_CVC4LIB
1034     -D__STDC_LIMIT_MACROS
1035     -D__STDC_FORMAT_MACROS
1036 )
1037 # Add libcvc4 dependencies for generated sources.
1038 add_dependencies(cvc4 gen-expr gen-gitinfo gen-options gen-tags gen-theory)
1039
1040 # Add library/include dependencies
1041 if(ENABLE_VALGRIND)
1042   target_include_directories(cvc4 PRIVATE ${Valgrind_INCLUDE_DIR})
1043 endif()
1044 if(USE_ABC)
1045   target_link_libraries(cvc4 ${ABC_LIBRARIES})
1046   target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR})
1047 endif()
1048 if(USE_CADICAL)
1049   target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
1050   target_include_directories(cvc4 PRIVATE ${CaDiCaL_INCLUDE_DIR})
1051 endif()
1052 if(USE_CLN)
1053   target_link_libraries(cvc4 ${CLN_LIBRARIES})
1054   target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
1055 endif()
1056 if(USE_CRYPTOMINISAT)
1057   target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
1058   target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
1059 endif()
1060 if(USE_KISSAT)
1061   target_link_libraries(cvc4 ${Kissat_LIBRARIES})
1062   target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR})
1063 endif()
1064 if(USE_DRAT2ER)
1065   target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
1066   target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
1067 endif()
1068 if(USE_GLPK)
1069   target_link_libraries(cvc4 ${GLPK_LIBRARIES})
1070   target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
1071 endif()
1072 if(USE_LFSC)
1073   target_link_libraries(cvc4 ${LFSC_LIBRARIES})
1074   target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
1075 endif()
1076 if(USE_POLY)
1077   target_link_libraries(cvc4 ${POLY_LIBRARIES})
1078   target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
1079 endif()
1080 if(USE_SYMFPU)
1081   target_include_directories(cvc4
1082     PUBLIC $<BUILD_INTERFACE:${SymFPU_INCLUDE_DIR}>)
1083 endif()
1084
1085 # Note: When linked statically GMP needs to be linked after CLN since CLN
1086 # depends on GMP.
1087 target_link_libraries(cvc4 ${GMP_LIBRARIES})
1088 target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
1089
1090 # Add rt library
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})
1094
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.
1100
1101 if (NOT BUILD_LIB_ONLY)
1102   add_subdirectory(main)
1103 endif()
1104
1105 #-----------------------------------------------------------------------------#
1106 # Note:
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
1109 # C++ API.
1110 #
1111 # All (generated) headers that either include cvc4_public.h or
1112 # cvc4parser_public.h need to be listed explicitly here.
1113 #
1114 install(FILES
1115           api/cvc4cpp.h
1116           api/cvc4cppkind.h
1117         DESTINATION
1118           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/api)
1119 install(FILES
1120           base/configuration.h
1121           base/exception.h
1122           base/listener.h
1123           base/modal_exception.h
1124         DESTINATION
1125           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/base)
1126 install(FILES
1127           context/cdhashmap_forward.h
1128           context/cdhashset_forward.h
1129           context/cdinsert_hashmap_forward.h
1130           context/cdlist_forward.h
1131         DESTINATION
1132           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/context)
1133 install(FILES
1134           include/cvc4.h
1135           include/cvc4_public.h
1136           include/cvc4parser_public.h
1137         DESTINATION
1138           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4)
1139 install(FILES
1140           expr/array_store_all.h
1141           expr/ascription_type.h
1142           expr/emptyset.h
1143           expr/expr_iomanip.h
1144           expr/record.h
1145           expr/sequence.h
1146           expr/symbol_manager.h
1147           expr/symbol_table.h
1148           expr/type.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
1154         DESTINATION
1155           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/expr)
1156 install(FILES
1157           options/language.h
1158           options/option_exception.h
1159           options/options.h
1160           options/printer_modes.h
1161           options/set_language.h
1162         DESTINATION
1163           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/options)
1164 install(FILES
1165           parser/input.h
1166           parser/parser.h
1167           parser/parser_builder.h
1168           parser/parser_exception.h
1169           parser/parse_op.h
1170         DESTINATION
1171           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/parser)
1172 install(FILES
1173         DESTINATION
1174           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/printer)
1175 install(FILES
1176           proof/unsat_core.h
1177         DESTINATION
1178           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/proof)
1179 install(FILES
1180           smt/command.h
1181           smt/logic_exception.h
1182           smt/smt_engine.h
1183         DESTINATION
1184           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/smt)
1185 install(FILES
1186           theory/logic_info.h
1187           theory/theory_id.h
1188         DESTINATION
1189           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/theory)
1190 install(FILES
1191           util/abstract_value.h
1192           util/bitvector.h
1193           util/bool.h
1194           util/cardinality.h
1195           util/divisible.h
1196           util/gmp_util.h
1197           util/hash.h
1198           util/iand.h
1199           util/integer_cln_imp.h
1200           util/integer_gmp_imp.h
1201           util/maybe.h
1202           util/poly_util.h
1203           util/rational_cln_imp.h
1204           util/rational_gmp_imp.h
1205           util/real_algebraic_number_poly_imp.h
1206           util/regexp.h
1207           util/resource_manager.h
1208           util/result.h
1209           util/sexpr.h
1210           util/statistics.h
1211           util/string.h
1212           util/tuple.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
1218         DESTINATION
1219           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/util)
1220
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})")