src/CMakeLists.txt

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