diff options
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 618 |
1 files changed, 602 insertions, 16 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 500900bb1..e1e03bd97 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,17 +1,603 @@ -#add_subdirectory(base) +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/git_versioninfo.cpp.in + ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp +) + +set(cvc4_src_files + ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp + api/cvc4cpp.cpp + api/cvc4cpp.h + api/cvc4cppkind.h + context/backtrackable.h + context/cddense_set.h + context/cdhashmap.h + context/cdhashmap_forward.h + context/cdhashset.h + context/cdhashset_forward.h + context/cdinsert_hashmap.h + context/cdinsert_hashmap_forward.h + context/cdlist.h + context/cdlist_forward.h + context/cdmaybe.h + context/cdo.h + context/cdqueue.h + context/cdtrail_queue.h + context/context.cpp + context/context.h + context/context_mm.cpp + context/context_mm.h + decision/decision_attributes.h + decision/decision_engine.cpp + decision/decision_engine.h + decision/decision_strategy.h + decision/justification_heuristic.cpp + decision/justification_heuristic.h + preprocessing/passes/apply_substs.cpp + preprocessing/passes/apply_substs.h + preprocessing/passes/bool_to_bv.cpp + preprocessing/passes/bool_to_bv.h + preprocessing/passes/bv_abstraction.cpp + preprocessing/passes/bv_abstraction.h + preprocessing/passes/bv_ackermann.cpp + preprocessing/passes/bv_ackermann.h + preprocessing/passes/bv_gauss.cpp + preprocessing/passes/bv_gauss.h + preprocessing/passes/bv_intro_pow2.cpp + preprocessing/passes/bv_intro_pow2.h + preprocessing/passes/bv_to_bool.cpp + preprocessing/passes/bv_to_bool.h + preprocessing/passes/int_to_bv.cpp + preprocessing/passes/int_to_bv.h + preprocessing/passes/pseudo_boolean_processor.cpp + preprocessing/passes/pseudo_boolean_processor.h + preprocessing/passes/real_to_int.cpp + preprocessing/passes/real_to_int.h + preprocessing/passes/rewrite.cpp + preprocessing/passes/rewrite.h + preprocessing/passes/sep_skolem_emp.cpp + preprocessing/passes/sep_skolem_emp.h + preprocessing/passes/static_learning.cpp + preprocessing/passes/static_learning.h + preprocessing/passes/symmetry_breaker.cpp + preprocessing/passes/symmetry_breaker.h + preprocessing/passes/symmetry_detect.cpp + preprocessing/passes/symmetry_detect.h + preprocessing/passes/synth_rew_rules.cpp + preprocessing/passes/synth_rew_rules.h + preprocessing/preprocessing_pass.cpp + preprocessing/preprocessing_pass.h + preprocessing/preprocessing_pass_context.cpp + preprocessing/preprocessing_pass_context.h + preprocessing/preprocessing_pass_registry.cpp + preprocessing/preprocessing_pass_registry.h + printer/ast/ast_printer.cpp + printer/ast/ast_printer.h + printer/cvc/cvc_printer.cpp + printer/cvc/cvc_printer.h + printer/dagification_visitor.cpp + printer/dagification_visitor.h + printer/printer.cpp + printer/printer.h + printer/smt2/smt2_printer.cpp + printer/smt2/smt2_printer.h + printer/sygus_print_callback.cpp + printer/sygus_print_callback.h + printer/tptp/tptp_printer.cpp + printer/tptp/tptp_printer.h + proof/arith_proof.cpp + proof/arith_proof.h + proof/array_proof.cpp + proof/array_proof.h + proof/bitvector_proof.cpp + proof/bitvector_proof.h + proof/clause_id.h + proof/cnf_proof.cpp + proof/cnf_proof.h + proof/lemma_proof.cpp + proof/lemma_proof.h + proof/proof.h + proof/proof_manager.cpp + proof/proof_manager.h + proof/proof_output_channel.cpp + proof/proof_output_channel.h + proof/proof_utils.cpp + proof/proof_utils.h + proof/sat_proof.h + proof/sat_proof_implementation.h + proof/simplify_boolean_node.cpp + proof/simplify_boolean_node.h + proof/skolemization_manager.cpp + proof/skolemization_manager.h + proof/theory_proof.cpp + proof/theory_proof.h + proof/uf_proof.cpp + proof/uf_proof.h + proof/unsat_core.cpp + proof/unsat_core.h + prop/cadical.cpp + prop/cadical.h + prop/cnf_stream.cpp + prop/cnf_stream.h + prop/cryptominisat.cpp + prop/cryptominisat.h + prop/prop_engine.cpp + prop/prop_engine.h + prop/registrar.h + prop/sat_solver.h + prop/sat_solver_factory.cpp + prop/sat_solver_factory.h + prop/sat_solver_types.h + prop/theory_proxy.cpp + prop/theory_proxy.h + smt/command.cpp + smt/command.h + smt/command_list.cpp + smt/command_list.h + smt/dump.cpp + smt/dump.h + smt/logic_exception.h + smt/logic_request.cpp + smt/logic_request.h + smt/managed_ostreams.cpp + smt/managed_ostreams.h + smt/model.cpp + smt/model.h + smt/smt_engine.cpp + smt/smt_engine.h + smt/smt_engine_check_proof.cpp + smt/smt_engine_scope.cpp + smt/smt_engine_scope.h + smt/smt_statistics_registry.cpp + smt/smt_statistics_registry.h + smt/term_formula_removal.cpp + smt/term_formula_removal.h + smt/update_ostream.h + theory/arith/approx_simplex.cpp + theory/arith/approx_simplex.h + theory/arith/arith_ite_utils.cpp + theory/arith/arith_ite_utils.h + theory/arith/arith_msum.cpp + theory/arith/arith_msum.h + theory/arith/arith_rewriter.cpp + theory/arith/arith_rewriter.h + theory/arith/arith_static_learner.cpp + theory/arith/arith_static_learner.h + theory/arith/arith_utilities.h + theory/arith/arithvar.cpp + theory/arith/arithvar.h + theory/arith/attempt_solution_simplex.cpp + theory/arith/attempt_solution_simplex.h + theory/arith/bound_counts.h + theory/arith/callbacks.cpp + theory/arith/callbacks.h + theory/arith/congruence_manager.cpp + theory/arith/congruence_manager.h + theory/arith/constraint.cpp + theory/arith/constraint.h + theory/arith/constraint_forward.h + theory/arith/cut_log.cpp + theory/arith/cut_log.h + theory/arith/delta_rational.cpp + theory/arith/delta_rational.h + theory/arith/dio_solver.cpp + theory/arith/dio_solver.h + theory/arith/dual_simplex.cpp + theory/arith/dual_simplex.h + theory/arith/error_set.cpp + theory/arith/error_set.h + theory/arith/fc_simplex.cpp + theory/arith/fc_simplex.h + theory/arith/infer_bounds.cpp + theory/arith/infer_bounds.h + theory/arith/linear_equality.cpp + theory/arith/linear_equality.h + theory/arith/matrix.cpp + theory/arith/matrix.h + theory/arith/nonlinear_extension.cpp + theory/arith/nonlinear_extension.h + theory/arith/normal_form.cpp + theory/arith/normal_form.h + theory/arith/partial_model.cpp + theory/arith/partial_model.h + theory/arith/simplex.cpp + theory/arith/simplex.h + theory/arith/simplex_update.cpp + theory/arith/simplex_update.h + theory/arith/soi_simplex.cpp + theory/arith/soi_simplex.h + theory/arith/tableau.cpp + theory/arith/tableau.h + theory/arith/tableau_sizes.cpp + theory/arith/tableau_sizes.h + theory/arith/theory_arith.cpp + theory/arith/theory_arith.h + theory/arith/theory_arith_private.cpp + theory/arith/theory_arith_private.h + theory/arith/theory_arith_private_forward.h + theory/arith/theory_arith_type_rules.h + theory/arith/type_enumerator.h + theory/arrays/array_info.cpp + theory/arrays/array_info.h + theory/arrays/array_proof_reconstruction.cpp + theory/arrays/array_proof_reconstruction.h + theory/arrays/static_fact_manager.cpp + theory/arrays/static_fact_manager.h + theory/arrays/theory_arrays.cpp + theory/arrays/theory_arrays.h + theory/arrays/theory_arrays_rewriter.cpp + theory/arrays/theory_arrays_rewriter.h + theory/arrays/theory_arrays_type_rules.h + theory/arrays/type_enumerator.h + theory/arrays/union_find.cpp + theory/arrays/union_find.h + theory/assertion.cpp + theory/assertion.h + theory/atom_requests.cpp + theory/atom_requests.h + theory/booleans/circuit_propagator.cpp + theory/booleans/circuit_propagator.h + theory/booleans/theory_bool.cpp + theory/booleans/theory_bool.h + theory/booleans/theory_bool_rewriter.cpp + theory/booleans/theory_bool_rewriter.h + theory/booleans/theory_bool_type_rules.h + theory/booleans/type_enumerator.h + theory/builtin/theory_builtin.cpp + theory/builtin/theory_builtin.h + theory/builtin/theory_builtin_rewriter.cpp + theory/builtin/theory_builtin_rewriter.h + theory/builtin/theory_builtin_type_rules.h + theory/builtin/type_enumerator.cpp + theory/builtin/type_enumerator.h + theory/bv/abstraction.cpp + theory/bv/abstraction.h + theory/bv/bitblast/aig_bitblaster.cpp + theory/bv/bitblast/aig_bitblaster.h + theory/bv/bitblast/bitblast_strategies_template.h + theory/bv/bitblast/bitblast_utils.h + theory/bv/bitblast/bitblaster.h + theory/bv/bitblast/eager_bitblaster.cpp + theory/bv/bitblast/eager_bitblaster.h + theory/bv/bitblast/lazy_bitblaster.cpp + theory/bv/bitblast/lazy_bitblaster.h + theory/bv/bv_eager_solver.cpp + theory/bv/bv_eager_solver.h + theory/bv/bv_inequality_graph.cpp + theory/bv/bv_inequality_graph.h + theory/bv/bv_quick_check.cpp + theory/bv/bv_quick_check.h + theory/bv/bv_subtheory.h + theory/bv/bv_subtheory_algebraic.cpp + theory/bv/bv_subtheory_algebraic.h + theory/bv/bv_subtheory_bitblast.cpp + theory/bv/bv_subtheory_bitblast.h + theory/bv/bv_subtheory_core.cpp + theory/bv/bv_subtheory_core.h + theory/bv/bv_subtheory_inequality.cpp + theory/bv/bv_subtheory_inequality.h + theory/bv/slicer.cpp + theory/bv/slicer.h + theory/bv/theory_bv.cpp + theory/bv/theory_bv.h + theory/bv/theory_bv_rewrite_rules.h + theory/bv/theory_bv_rewrite_rules_constant_evaluation.h + theory/bv/theory_bv_rewrite_rules_core.h + theory/bv/theory_bv_rewrite_rules_normalization.h + theory/bv/theory_bv_rewrite_rules_operator_elimination.h + theory/bv/theory_bv_rewrite_rules_simplification.h + theory/bv/theory_bv_rewriter.cpp + theory/bv/theory_bv_rewriter.h + theory/bv/theory_bv_type_rules.h + theory/bv/theory_bv_utils.cpp + theory/bv/theory_bv_utils.h + theory/bv/type_enumerator.h + theory/care_graph.h + theory/datatypes/datatypes_rewriter.cpp + theory/datatypes/datatypes_rewriter.h + theory/datatypes/datatypes_sygus.cpp + theory/datatypes/datatypes_sygus.h + theory/datatypes/sygus_simple_sym.cpp + theory/datatypes/sygus_simple_sym.h + theory/datatypes/theory_datatypes.cpp + theory/datatypes/theory_datatypes.h + theory/datatypes/theory_datatypes_type_rules.h + theory/datatypes/type_enumerator.cpp + theory/datatypes/type_enumerator.h + theory/evaluator.cpp + theory/evaluator.h + theory/ext_theory.cpp + theory/ext_theory.h + theory/fp/fp_converter.cpp + theory/fp/fp_converter.h + theory/fp/theory_fp.cpp + theory/fp/theory_fp.h + theory/fp/theory_fp_rewriter.cpp + theory/fp/theory_fp_rewriter.h + theory/fp/theory_fp_type_rules.h + theory/fp/type_enumerator.h + theory/idl/idl_assertion.cpp + theory/idl/idl_assertion.h + theory/idl/idl_assertion_db.cpp + theory/idl/idl_assertion_db.h + theory/idl/idl_model.cpp + theory/idl/idl_model.h + theory/idl/theory_idl.cpp + theory/idl/theory_idl.h + theory/interrupted.h + theory/ite_utilities.cpp + theory/ite_utilities.h + theory/logic_info.cpp + theory/logic_info.h + theory/output_channel.h + theory/quantifiers/alpha_equivalence.cpp + theory/quantifiers/alpha_equivalence.h + theory/quantifiers/anti_skolem.cpp + theory/quantifiers/anti_skolem.h + theory/quantifiers/bv_inverter.cpp + theory/quantifiers/bv_inverter.h + theory/quantifiers/candidate_rewrite_database.cpp + theory/quantifiers/candidate_rewrite_database.h + theory/quantifiers/candidate_rewrite_filter.cpp + theory/quantifiers/candidate_rewrite_filter.h + theory/quantifiers/cegqi/ceg_arith_instantiator.cpp + theory/quantifiers/cegqi/ceg_arith_instantiator.h + theory/quantifiers/cegqi/ceg_bv_instantiator.cpp + theory/quantifiers/cegqi/ceg_bv_instantiator.h + theory/quantifiers/cegqi/ceg_dt_instantiator.cpp + theory/quantifiers/cegqi/ceg_dt_instantiator.h + theory/quantifiers/cegqi/ceg_epr_instantiator.cpp + theory/quantifiers/cegqi/ceg_epr_instantiator.h + theory/quantifiers/cegqi/ceg_instantiator.cpp + theory/quantifiers/cegqi/ceg_instantiator.h + theory/quantifiers/cegqi/inst_strategy_cbqi.cpp + theory/quantifiers/cegqi/inst_strategy_cbqi.h + theory/quantifiers/conjecture_generator.cpp + theory/quantifiers/conjecture_generator.h + theory/quantifiers/dynamic_rewrite.cpp + theory/quantifiers/dynamic_rewrite.h + theory/quantifiers/ematching/candidate_generator.cpp + theory/quantifiers/ematching/candidate_generator.h + theory/quantifiers/ematching/ho_trigger.cpp + theory/quantifiers/ematching/ho_trigger.h + theory/quantifiers/ematching/inst_match_generator.cpp + theory/quantifiers/ematching/inst_match_generator.h + theory/quantifiers/ematching/inst_strategy_e_matching.cpp + theory/quantifiers/ematching/inst_strategy_e_matching.h + theory/quantifiers/ematching/instantiation_engine.cpp + theory/quantifiers/ematching/instantiation_engine.h + theory/quantifiers/ematching/trigger.cpp + theory/quantifiers/ematching/trigger.h + theory/quantifiers/equality_infer.cpp + theory/quantifiers/equality_infer.h + theory/quantifiers/equality_query.cpp + theory/quantifiers/equality_query.h + theory/quantifiers/extended_rewrite.cpp + theory/quantifiers/extended_rewrite.h + theory/quantifiers/first_order_model.cpp + theory/quantifiers/first_order_model.h + theory/quantifiers/fmf/ambqi_builder.cpp + theory/quantifiers/fmf/ambqi_builder.h + theory/quantifiers/fmf/bounded_integers.cpp + theory/quantifiers/fmf/bounded_integers.h + theory/quantifiers/fmf/full_model_check.cpp + theory/quantifiers/fmf/full_model_check.h + theory/quantifiers/fmf/model_builder.cpp + theory/quantifiers/fmf/model_builder.h + theory/quantifiers/fmf/model_engine.cpp + theory/quantifiers/fmf/model_engine.h + theory/quantifiers/fun_def_process.cpp + theory/quantifiers/fun_def_process.h + theory/quantifiers/global_negate.cpp + theory/quantifiers/global_negate.h + theory/quantifiers/inst_match.cpp + theory/quantifiers/inst_match.h + theory/quantifiers/inst_match_trie.cpp + theory/quantifiers/inst_match_trie.h + theory/quantifiers/inst_propagator.cpp + theory/quantifiers/inst_propagator.h + theory/quantifiers/inst_strategy_enumerative.cpp + theory/quantifiers/inst_strategy_enumerative.h + theory/quantifiers/instantiate.cpp + theory/quantifiers/instantiate.h + theory/quantifiers/lazy_trie.cpp + theory/quantifiers/lazy_trie.h + theory/quantifiers/local_theory_ext.cpp + theory/quantifiers/local_theory_ext.h + theory/quantifiers/macros.cpp + theory/quantifiers/macros.h + theory/quantifiers/quant_conflict_find.cpp + theory/quantifiers/quant_conflict_find.h + theory/quantifiers/quant_epr.cpp + theory/quantifiers/quant_epr.h + theory/quantifiers/quant_relevance.cpp + theory/quantifiers/quant_relevance.h + theory/quantifiers/quant_split.cpp + theory/quantifiers/quant_split.h + theory/quantifiers/quant_util.cpp + theory/quantifiers/quant_util.h + theory/quantifiers/quantifiers_attributes.cpp + theory/quantifiers/quantifiers_attributes.h + theory/quantifiers/quantifiers_rewriter.cpp + theory/quantifiers/quantifiers_rewriter.h + theory/quantifiers/relevant_domain.cpp + theory/quantifiers/relevant_domain.h + theory/quantifiers/rewrite_engine.cpp + theory/quantifiers/rewrite_engine.h + theory/quantifiers/single_inv_partition.cpp + theory/quantifiers/single_inv_partition.h + theory/quantifiers/skolemize.cpp + theory/quantifiers/skolemize.h + theory/quantifiers/sygus/ce_guided_conjecture.cpp + theory/quantifiers/sygus/ce_guided_conjecture.h + theory/quantifiers/sygus/ce_guided_instantiation.cpp + theory/quantifiers/sygus/ce_guided_instantiation.h + theory/quantifiers/sygus/ce_guided_single_inv.cpp + theory/quantifiers/sygus/ce_guided_single_inv.h + theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp + theory/quantifiers/sygus/ce_guided_single_inv_sol.h + theory/quantifiers/sygus/cegis.cpp + theory/quantifiers/sygus/cegis.h + theory/quantifiers/sygus/cegis_unif.cpp + theory/quantifiers/sygus/cegis_unif.h + theory/quantifiers/sygus/sygus_eval_unfold.cpp + theory/quantifiers/sygus/sygus_eval_unfold.h + theory/quantifiers/sygus/sygus_explain.cpp + theory/quantifiers/sygus/sygus_explain.h + theory/quantifiers/sygus/sygus_grammar_cons.cpp + theory/quantifiers/sygus/sygus_grammar_cons.h + theory/quantifiers/sygus/sygus_grammar_norm.cpp + theory/quantifiers/sygus/sygus_grammar_norm.h + theory/quantifiers/sygus/sygus_grammar_red.cpp + theory/quantifiers/sygus/sygus_grammar_red.h + theory/quantifiers/sygus/sygus_invariance.cpp + theory/quantifiers/sygus/sygus_invariance.h + theory/quantifiers/sygus/sygus_module.cpp + theory/quantifiers/sygus/sygus_module.h + theory/quantifiers/sygus/sygus_pbe.cpp + theory/quantifiers/sygus/sygus_pbe.h + theory/quantifiers/sygus/sygus_process_conj.cpp + theory/quantifiers/sygus/sygus_process_conj.h + theory/quantifiers/sygus/sygus_repair_const.cpp + theory/quantifiers/sygus/sygus_repair_const.h + theory/quantifiers/sygus/sygus_unif.cpp + theory/quantifiers/sygus/sygus_unif.h + theory/quantifiers/sygus/sygus_unif_io.cpp + theory/quantifiers/sygus/sygus_unif_io.h + theory/quantifiers/sygus/sygus_unif_rl.cpp + theory/quantifiers/sygus/sygus_unif_rl.h + theory/quantifiers/sygus/sygus_unif_strat.cpp + theory/quantifiers/sygus/sygus_unif_strat.h + theory/quantifiers/sygus/term_database_sygus.cpp + theory/quantifiers/sygus/term_database_sygus.h + theory/quantifiers/sygus_inference.cpp + theory/quantifiers/sygus_inference.h + theory/quantifiers/sygus_sampler.cpp + theory/quantifiers/sygus_sampler.h + theory/quantifiers/term_database.cpp + theory/quantifiers/term_database.h + theory/quantifiers/term_enumeration.cpp + theory/quantifiers/term_enumeration.h + theory/quantifiers/term_util.cpp + theory/quantifiers/term_util.h + theory/quantifiers/theory_quantifiers.cpp + theory/quantifiers/theory_quantifiers.h + theory/quantifiers/theory_quantifiers_type_rules.h + theory/quantifiers_engine.cpp + theory/quantifiers_engine.h + theory/rep_set.cpp + theory/rep_set.h + theory/rewriter.cpp + theory/rewriter.h + theory/rewriter_attributes.h + theory/sep/theory_sep.cpp + theory/sep/theory_sep.h + theory/sep/theory_sep_rewriter.cpp + theory/sep/theory_sep_rewriter.h + theory/sep/theory_sep_type_rules.h + theory/sets/normal_form.h + theory/sets/rels_utils.h + theory/sets/theory_sets.cpp + theory/sets/theory_sets.h + theory/sets/theory_sets_private.cpp + theory/sets/theory_sets_private.h + theory/sets/theory_sets_rels.cpp + theory/sets/theory_sets_rels.h + theory/sets/theory_sets_rewriter.cpp + theory/sets/theory_sets_rewriter.h + theory/sets/theory_sets_type_enumerator.h + theory/sets/theory_sets_type_rules.h + theory/shared_terms_database.cpp + theory/shared_terms_database.h + theory/sort_inference.cpp + theory/sort_inference.h + theory/strings/regexp_operation.cpp + theory/strings/regexp_operation.h + theory/strings/theory_strings.cpp + theory/strings/theory_strings.h + theory/strings/theory_strings_preprocess.cpp + theory/strings/theory_strings_preprocess.h + theory/strings/theory_strings_rewriter.cpp + theory/strings/theory_strings_rewriter.h + theory/strings/theory_strings_type_rules.h + theory/strings/type_enumerator.h + theory/substitutions.cpp + theory/substitutions.h + theory/term_registration_visitor.cpp + theory/term_registration_visitor.h + theory/theory.cpp + theory/theory.h + theory/theory_engine.cpp + theory/theory_engine.h + theory/theory_model.cpp + theory/theory_model.h + theory/theory_model_builder.cpp + theory/theory_model_builder.h + theory/theory_registrar.h + theory/theory_test_utils.h + theory/type_enumerator.h + theory/type_set.cpp + theory/type_set.h + theory/uf/equality_engine.cpp + theory/uf/equality_engine.h + theory/uf/equality_engine_types.h + theory/uf/symmetry_breaker.cpp + theory/uf/symmetry_breaker.h + theory/uf/theory_uf.cpp + theory/uf/theory_uf.h + theory/uf/theory_uf_model.cpp + theory/uf/theory_uf_model.h + theory/uf/theory_uf_rewriter.h + theory/uf/theory_uf_strong_solver.cpp + theory/uf/theory_uf_strong_solver.h + theory/uf/theory_uf_type_rules.h + theory/unconstrained_simplifier.cpp + theory/unconstrained_simplifier.h + theory/valuation.cpp + theory/valuation.h +) + +# Generated in theory/ +set(cvc4_gen_src_files + theory/rewriter_tables.h + theory/theory_traits.h + theory/type_enumerator.cpp +) +# Since these files are generated in a different CMakeLists.txt we have to +# tell cmake that the files are generated. +set_source_files_properties(${cvc4_gen_src_files} PROPERTIES GENERATED TRUE) + +add_library(cvc4 SHARED ${cvc4_src_files} ${cvc4_gen_src_files}) +set_target_properties(cvc4 + PROPERTIES + COMPILE_DEFINITIONS + __BUILDING_CVC4LIB + __STDC_LIMIT_MACROS + __STDC_FORMAT_MACROS +) +add_dependencies(cvc4 gen-theory-files) +target_link_libraries(cvc4 + base bvminisat expr minisat options smtutil util replacements + ${LIBRARIES} +) + +# TODO: if proofs: libsignatures + +include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) +include_directories(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) +include_directories(include ${CMAKE_CURRENT_BINARY_DIR}/include) +include_directories(options ${CMAKE_CURRENT_BINARY_DIR}/options) + +add_subdirectory(base) #add_subdirectory(bindings) -#add_subdirectory(compat) -#add_subdirectory(context) -#add_subdirectory(decision) -#add_subdirectory(expr) -#add_subdirectory(lib) -#add_subdirectory(main) -#add_subdirectory(options) -#add_subdirectory(parser) -#add_subdirectory(printer) -#add_subdirectory(proof) -#add_subdirectory(prop) -#add_subdirectory(smt) -#add_subdirectory(smt_util) -#add_subdirectory(theory) -#add_subdirectory(util) +add_subdirectory(compat) +add_subdirectory(expr) +add_subdirectory(lib) +add_subdirectory(main) +add_subdirectory(options) +add_subdirectory(parser) +add_subdirectory(prop/bvminisat) +add_subdirectory(prop/minisat) +add_subdirectory(smt_util) +add_subdirectory(theory) +add_subdirectory(util) + |