diff options
Diffstat (limited to 'src/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 96 |
1 files changed, 36 insertions, 60 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index fe38ddf71..773acf67e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -19,7 +19,7 @@ AM_CPPFLAGS = \ -I@builddir@ -I@srcdir@/include -I@srcdir@ -I@top_srcdir@/proofs/lfsc_checker AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main +SUBDIRS = lib base options util expr smt_util prop/minisat prop/bvminisat . parser compat bindings main # The THEORIES list has been moved to Makefile.theories include @top_srcdir@/src/Makefile.theories @@ -33,6 +33,7 @@ nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp libcvc4_la_SOURCES = \ git_versioninfo.cpp \ svn_versioninfo.cpp \ + context/backtrackable.h \ context/context.cpp \ context/context.h \ context/context_mm.cpp \ @@ -56,20 +57,16 @@ libcvc4_la_SOURCES = \ context/stacking_map.h \ context/stacking_vector.h \ context/cddense_set.h \ - decision/decision_mode.h \ - decision/decision_mode.cpp \ + decision/decision_attributes.h \ decision/decision_engine.h \ decision/decision_engine.cpp \ decision/decision_strategy.h \ decision/justification_heuristic.h \ decision/justification_heuristic.cpp \ - decision/options_handlers.h \ printer/printer.h \ printer/printer.cpp \ printer/dagification_visitor.h \ printer/dagification_visitor.cpp \ - printer/modes.h \ - printer/modes.cpp \ printer/ast/ast_printer.h \ printer/ast/ast_printer.cpp \ printer/smt1/smt1_printer.h \ @@ -80,7 +77,6 @@ libcvc4_la_SOURCES = \ printer/cvc/cvc_printer.cpp \ printer/tptp/tptp_printer.h \ printer/tptp/tptp_printer.cpp \ - printer/options_handlers.h \ proof/proof.h \ proof/sat_proof.h \ proof/sat_proof.cpp \ @@ -90,6 +86,8 @@ libcvc4_la_SOURCES = \ proof/theory_proof.cpp \ proof/proof_manager.h \ proof/proof_manager.cpp \ + proof/unsat_core.cpp \ + proof/unsat_core.h \ prop/registrar.h \ prop/prop_engine.cpp \ prop/prop_engine.h \ @@ -106,31 +104,29 @@ libcvc4_la_SOURCES = \ smt/smt_engine.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ + smt/smt_options_handler.cpp \ + smt/smt_options_handler.h \ smt/smt_engine_scope.cpp \ smt/smt_engine_scope.h \ smt/command_list.cpp \ smt/command_list.h \ - smt/modal_exception.h \ smt/boolean_terms.h \ smt/boolean_terms.cpp \ smt/logic_exception.h \ smt/logic_request.h \ smt/logic_request.cpp \ - smt/simplification_mode.h \ - smt/simplification_mode.cpp \ - smt/options_handlers.h \ - theory/decision_attributes.h \ theory/logic_info.h \ theory/logic_info.cpp \ theory/output_channel.h \ theory/interrupted.h \ + theory/sort_inference.cpp \ + theory/sort_inference.h \ theory/type_enumerator.h \ theory/theory_engine.h \ theory/theory_engine.cpp \ theory/theory_test_utils.h \ theory/theory.h \ theory/theory.cpp \ - theory/theoryof_mode.h \ theory/theory_registrar.h \ theory/rewriter.h \ theory/rewriter_attributes.h \ @@ -155,7 +151,6 @@ libcvc4_la_SOURCES = \ theory/rep_set.cpp \ theory/atom_requests.h \ theory/atom_requests.cpp \ - theory/options_handlers.h \ theory/uf/theory_uf.h \ theory/uf/theory_uf.cpp \ theory/uf/theory_uf_type_rules.h \ @@ -169,7 +164,6 @@ libcvc4_la_SOURCES = \ theory/uf/theory_uf_strong_solver.cpp \ theory/uf/theory_uf_model.h \ theory/uf/theory_uf_model.cpp \ - theory/uf/options_handlers.h \ theory/bv/theory_bv_utils.h \ theory/bv/theory_bv_utils.cpp \ theory/bv/type_enumerator.h \ @@ -211,9 +205,6 @@ libcvc4_la_SOURCES = \ theory/bv/bv_quick_check.cpp \ theory/bv/bv_subtheory_algebraic.h \ theory/bv/bv_subtheory_algebraic.cpp \ - theory/bv/options_handlers.h \ - theory/bv/bitblast_mode.h \ - theory/bv/bitblast_mode.cpp \ theory/bv/bitblast_utils.h \ theory/bv/bvintropow2.h \ theory/bv/bvintropow2.cpp \ @@ -241,7 +232,6 @@ libcvc4_la_SOURCES = \ theory/datatypes/datatypes_sygus.cpp \ theory/sets/expr_patterns.h \ theory/sets/normal_form.h \ - theory/sets/options_handlers.h \ theory/sets/scrutinize.h \ theory/sets/term_info.h \ theory/sets/theory_sets.cpp \ @@ -289,8 +279,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/inst_match.cpp \ theory/quantifiers/model_engine.h \ theory/quantifiers/model_engine.cpp \ - theory/quantifiers/modes.cpp \ - theory/quantifiers/modes.h \ theory/quantifiers/term_database.h \ theory/quantifiers/term_database.cpp \ theory/quantifiers/first_order_model.h \ @@ -345,7 +333,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quant_equality_engine.cpp \ theory/quantifiers/ceg_instantiator.h \ theory/quantifiers/ceg_instantiator.cpp \ - theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ theory/arith/arithvar.h \ @@ -404,17 +391,10 @@ libcvc4_la_SOURCES = \ theory/arith/theory_arith_private.cpp \ theory/arith/dio_solver.h \ theory/arith/dio_solver.cpp \ - theory/arith/arith_heuristic_pivot_rule.h \ - theory/arith/arith_heuristic_pivot_rule.cpp \ - theory/arith/arith_unate_lemma_mode.h \ - theory/arith/arith_unate_lemma_mode.cpp \ - theory/arith/arith_propagation_mode.h \ - theory/arith/arith_propagation_mode.cpp \ theory/arith/pseudoboolean_proc.h \ theory/arith/pseudoboolean_proc.cpp \ theory/arith/cut_log.h \ theory/arith/cut_log.cpp \ - theory/arith/options_handlers.h \ theory/booleans/type_enumerator.h \ theory/booleans/theory_bool.h \ theory/booleans/theory_bool.cpp \ @@ -423,9 +403,6 @@ libcvc4_la_SOURCES = \ theory/booleans/theory_bool_rewriter.cpp \ theory/booleans/circuit_propagator.h \ theory/booleans/circuit_propagator.cpp \ - theory/booleans/boolean_term_conversion_mode.h \ - theory/booleans/boolean_term_conversion_mode.cpp \ - theory/booleans/options_handlers.h \ theory/fp/theory_fp.h \ theory/fp/theory_fp.cpp \ theory/fp/theory_fp_rewriter.h \ @@ -433,15 +410,16 @@ libcvc4_la_SOURCES = \ theory/fp/theory_fp_type_rules.h nodist_libcvc4_la_SOURCES = \ - smt/smt_options.cpp \ theory/rewriter_tables.h \ theory/theory_traits.h \ theory/type_enumerator.cpp libcvc4_la_LIBADD = \ + @builddir@/base/libbase.la \ @builddir@/options/liboptions.la \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ + @builddir@/smt_util/libsmtutil.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/prop/bvminisat/libbvminisat.la if CVC4_PROOF @@ -484,42 +462,40 @@ CLEANFILES = \ $(top_builddir)/src/.subdirs EXTRA_DIST = \ + Makefile.theories \ + cvc4.i \ + include/cvc4.h \ + include/cvc4_private.h \ include/cvc4_private_library.h \ + include/cvc4_public.h \ include/cvc4parser_private.h \ include/cvc4parser_public.h \ - include/cvc4_private.h \ - include/cvc4_public.h \ - include/cvc4.h \ - cvc4.i \ mksubdirs \ - Makefile.theories \ - smt/smt_options_template.cpp \ - smt/modal_exception.i \ smt/logic_exception.i \ smt/smt_engine.i \ - theory/logic_info.i \ - theory/rewriter_tables_template.h \ - theory/theory_traits_template.h \ - theory/type_enumerator_template.cpp \ - theory/mktheorytraits \ - theory/mkrewriter \ - theory/uf/kinds \ - theory/bv/kinds \ - theory/idl/kinds \ - theory/builtin/kinds \ - theory/datatypes/kinds \ - theory/sets/kinds \ - theory/strings/kinds \ - theory/arrays/kinds \ - theory/quantifiers/kinds \ + proof/unsat_core.i \ theory/arith/kinds \ + theory/arrays/kinds \ theory/booleans/kinds \ - theory/example/ecdata.h \ + theory/builtin/kinds \ + theory/bv/kinds \ + theory/datatypes/kinds \ theory/example/ecdata.cpp \ - theory/example/theory_uf_tim.h \ + theory/example/ecdata.h \ theory/example/theory_uf_tim.cpp \ + theory/example/theory_uf_tim.h \ theory/fp/kinds \ - theory/fp/options_handlers.h + theory/idl/kinds \ + theory/logic_info.i \ + theory/mkrewriter \ + theory/mktheorytraits \ + theory/quantifiers/kinds \ + theory/rewriter_tables_template.h \ + theory/sets/kinds \ + theory/strings/kinds \ + theory/theory_traits_template.h \ + theory/type_enumerator_template.cpp \ + theory/uf/kinds svn_versioninfo.cpp: svninfo $(AM_V_GEN)( \ @@ -581,7 +557,7 @@ install-data-local: (echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo util/tls.h; \ + echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ @@ -614,7 +590,7 @@ uninstall-local: -(echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo util/tls.h; \ + echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ |