From 4b580ea3876055f701b13e67e0e4e78abbe47674 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Nov 2017 15:20:37 -0500 Subject: (Refactor) Split term util (#1303) * Fix some documentation. * Move model basis out of term db. * Moving * Finished moving. * Document Skolemize and term enumeration. * Minor * Model basis to first order model. * Change function name. * Minor * Clang format. * Minor * Format * Minor * Format * Address review. --- src/Makefile.am | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Makefile.am') diff --git a/src/Makefile.am b/src/Makefile.am index d370a73bc..e8910e182 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -424,6 +424,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/relevant_domain.h \ theory/quantifiers/rewrite_engine.cpp \ theory/quantifiers/rewrite_engine.h \ + theory/quantifiers/skolemize.cpp \ + theory/quantifiers/skolemize.h \ theory/quantifiers/sygus_grammar_cons.cpp \ theory/quantifiers/sygus_grammar_cons.h \ theory/quantifiers/sygus_process_conj.cpp \ @@ -434,6 +436,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/term_database.h \ theory/quantifiers/term_database_sygus.cpp \ theory/quantifiers/term_database_sygus.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 \ -- cgit v1.2.3