Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use rule simplification #93

Open
wants to merge 76 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
76 commits
Select commit Hold shift + click to select a range
dcf53cf
begin to develop the operation-based conversion
gfngfn Jun 15, 2022
9837564
use 'ResultMonad'
gfngfn Jun 15, 2022
3d0f0ed
develop 'decompose_body'
gfngfn Jun 15, 2022
d037f42
develop how to validate rule bodies
gfngfn Jun 15, 2022
055e0c3
develop 'Subst'
gfngfn Jun 15, 2022
d0c1d5c
develop how to extend substitutions
gfngfn Jun 15, 2022
6566652
develop how to extend substitutions and eliminate consumed equality c…
gfngfn Jun 15, 2022
14eebb4
begin to build SQL queries
gfngfn Jun 15, 2022
7333174
build SQL SELECT clauses
gfngfn Jun 15, 2022
3377f93
build SQL FROM clauses and use comparison constraints
gfngfn Jun 15, 2022
d837da0
basically complete 'convert_to_operation_based_sql'
gfngfn Jun 15, 2022
797205e
implement 'sql_of_vterm_new'
gfngfn Jun 16, 2022
89140b0
implement 'sql_vterm_of_arg'
gfngfn Jun 16, 2022
c15194a
refactor 'SqlFromTable'
gfngfn Jun 16, 2022
a88b9f6
use 'colnamtab' and 'symtkey' to implement 'get_column_names_from_table'
gfngfn Jun 16, 2022
187eb3c
begin to add unit tests
gfngfn Jun 16, 2022
61dff32
refactor 'convert_to_operation_based_sql'
gfngfn Jun 22, 2022
7b73c7c
develop tests for 'convert_to_operation_based_sql'
gfngfn Jun 22, 2022
5f290f5
develop tests for 'convert_to_operation_based_sql' (2)
gfngfn Jun 22, 2022
c742437
make cosmetic changes of output SQL queries
gfngfn Jun 22, 2022
5e92a10
refactor tests
gfngfn Jun 22, 2022
321a3b3
refactor tests for running multiple test cases
gfngfn Jun 22, 2022
7c00bde
add a test case '1st rule'
gfngfn Jun 22, 2022
b8da994
add a test case '2nd rule'
gfngfn Jun 22, 2022
2df7b44
slight cosmetic changes
gfngfn Jun 22, 2022
eaf450c
slight cosmetic changes (2)
gfngfn Jun 22, 2022
47d258d
refactor tests about module organization
gfngfn Jun 23, 2022
3bdd426
refactor tests about module organization (by moving tests into 'src/t…
gfngfn Jun 23, 2022
2977bb3
add 'convert_expr_to_operation_based_sql'
gfngfn Jul 1, 2022
e37f90d
develop 'convert_expr_to_operation_based_sql'
gfngfn Jul 1, 2022
4d3ac22
develop how to stringify SQL operations
gfngfn Jul 1, 2022
cdce1e4
update tests for 'convert_expr_to_operation_based_sql'
gfngfn Jul 1, 2022
13792b2
define 'partition_map' instead of using 'List.partition_map' (which i…
gfngfn Jul 14, 2022
24c7819
add 'Ast2sql.show_error'
gfngfn Jul 14, 2022
aa674cc
begin to develop 'Ast2sql.divide_rules_into_groups'
gfngfn Jul 14, 2022
50edf80
begin to generalize 'convert_expr_to_operation_based_sql' using 'divi…
gfngfn Jul 14, 2022
7f03362
slight refactoring and renaming
gfngfn Jul 14, 2022
c34bb58
begin to generalize '{positive,negative}_predicate' for handling delt…
gfngfn Jul 14, 2022
0f8976a
introduce 'delta_environment' for tracking specs of delta predicates
gfngfn Jul 14, 2022
6f6165b
introduce 'combine_delta_column_names'
gfngfn Jul 14, 2022
800e6a9
introduce 'table_environment' and replace 'colnamtab' with it
gfngfn Jul 14, 2022
49b3093
slight fix
gfngfn Jul 14, 2022
f5bb076
introduce 'head_spec' for compiling rules that define views
gfngfn Jul 19, 2022
86ed567
generalize 'divide_rules_into_groups'
gfngfn Jul 19, 2022
f218d92
generalize 'convert_expr_to_operation_based_sql' for 'PredGroup'
gfngfn Jul 19, 2022
dd244d7
generalize 'convert_expr_to_operation_based_sql' for 'PredGroup' (2)
gfngfn Jul 19, 2022
9c4b427
change how to handle rules in 'expr'
gfngfn Jul 20, 2022
679a9ba
introduce 'error_detail', support 'AnonVar', and take view definition…
gfngfn Jul 20, 2022
b6d4778
fix how to output 'FROM' clauses about referring to temporary tables
gfngfn Jul 20, 2022
10ab5fd
fix how to output 'FROM' clauses in subqueries corresponding to negat…
gfngfn Jul 21, 2022
d079522
fix tests
gfngfn Nov 21, 2022
168b133
begin to develop `simplification.ml`
gfngfn Nov 21, 2022
fd13557
develop `convert_{head,body}_rterm` etc.
gfngfn Nov 21, 2022
4966f2e
develop `simplification.ml` slightly
gfngfn Nov 21, 2022
d7767dc
introduce `equation_map` for representing equations internally
gfngfn Nov 21, 2022
f445060
implement `rule_equal`
gfngfn Nov 21, 2022
07ddba7
implement `erase_sole_occurrences`
gfngfn Nov 21, 2022
6f04658
develop `remove_looser_terms`
gfngfn Nov 21, 2022
caa0386
implement `has_contradicting_body` etc.
gfngfn Nov 28, 2022
63dddfd
begin to develop tests for `simplification.ml`
gfngfn Nov 28, 2022
35c4727
slightly develop tests
gfngfn Nov 28, 2022
7b574c9
add a test case and check that it fails
gfngfn Nov 28, 2022
3678c88
fix `remove_looser_{positive,negative}_terms` (and this makes the tes…
gfngfn Nov 28, 2022
8ad1941
add more tests (and confirm that they pass)
gfngfn Nov 30, 2022
5f9daf5
add the interface file `simplification.mli`
gfngfn Dec 8, 2022
9cab7d7
begin to support non-equality constraints
gfngfn Dec 8, 2022
e3b876e
non-equality constraints
gfngfn Dec 8, 2022
6f3da8f
add a test (32) for `Simplification`
gfngfn Dec 15, 2022
1abbcb2
begin to develop `remove_duplicate_rules`
gfngfn Dec 15, 2022
62281bd
begin to develop `are_alpha_equivalent_rules`
gfngfn Dec 15, 2022
adfaba2
implement `are_alpha_equivalent_rules`
gfngfn Dec 26, 2022
ab7d612
use `Simplification.simplify` in `main.ml`
gfngfn Jan 12, 2023
b905583
use `compare` instead of `Int.compare` for keeping support for OCaml …
gfngfn Jan 26, 2023
c845365
remove `Printf.printf` for debugging
gfngfn Jan 26, 2023
f8d85c5
refactor `simplification.ml` for keeping support for OCaml 4.07
gfngfn Feb 2, 2023
64c8a8c
Merge branch 'dev-rule-simplification' into use-rule-simplification
gfngfn Mar 2, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 30 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,12 @@ DIR_GUARD=@mkdir -p $(@D)

#Name of the final executable file to be generated
EX_NAME=birds
TEST_EX_NAME=birds_unit_tests

# source folder
SOURCE_DIR=src
LOGIC_SOURCE_DIR=src/logic
TEST_SOURCE_DIR=src/test

# binary folder for compilation
BIN_DIR=bin
Expand All @@ -17,13 +19,15 @@ RELEASE_DIR = release
LOGIC_RELEASE_DIR = release/logic
OBJ_DIR=${SOURCE_DIR}
LOGIC_OBJ_DIR=${LOGIC_SOURCE_DIR}
TEST_OBJ_DIR=${TEST_SOURCE_DIR}

OCAMLC_FLAGS=-bin-annot -w -26 -I $(OBJ_DIR) -I $(LOGIC_OBJ_DIR)
OCAMLC_FLAGS=-bin-annot -w -26 -I $(OBJ_DIR) -I $(LOGIC_OBJ_DIR) -I $(TEST_OBJ_DIR)
OCAMLOPT_FLAGS=-bin-annot -w -26 -I $(RELEASE_DIR) -I $(LOGIC_RELEASE_DIR)
OCAMLDEP_FLAGS=-I $(SOURCE_DIR) -I $(LOGIC_SOURCE_DIR)
OCAMLDEP_FLAGS=-I $(SOURCE_DIR) -I $(LOGIC_SOURCE_DIR) -I $(TEST_SOURCE_DIR)

#Name of the files that are part of the project
MAIN_FILE=main
TEST_MAIN_FILE=test_main
LOGIC_FILES=\
lib intro formulas prop fol skolem fol_ex\

Expand All @@ -39,17 +43,31 @@ TOP_FILES=\
ast2theorem \
bx\
debugger\
simplification\

TOP_FILES_WITH_MLI=\
parser expr conversion ast2sql ast2theorem\
simplification\

TEST_ONLY_FILES=\
ast2sql_operation_based_conversion_test\
simplification_test\


FILES=\
$(LOGIC_FILES:%=logic/%)\
$(TOP_FILES) \

.PHONY: all release clean depend #annot
TEST_FILES=\
$(FILES)\
$(TEST_ONLY_FILES:%=test/%)\

.PHONY: all release clean depend test #annot
all: $(BIN_DIR)/$(EX_NAME)

test: $(BIN_DIR)/$(TEST_EX_NAME)
./$(BIN_DIR)/$(TEST_EX_NAME)

#Rule for generating the final executable file
$(BIN_DIR)/$(EX_NAME): $(FILES:%=$(OBJ_DIR)/%.cmo) $(OBJ_DIR)/$(MAIN_FILE).cmo
$(DIR_GUARD)
Expand All @@ -60,6 +78,14 @@ $(OBJ_DIR)/$(MAIN_FILE).cmo: $(FILES:%=$(OBJ_DIR)/%.cmo) $(SOURCE_DIR)/$(MAIN_FI
$(DIR_GUARD)
ocamlfind ocamlc $(OCAMLC_FLAGS) -package $(PACKAGES) -thread -o $(OBJ_DIR)/$(MAIN_FILE) -c $(SOURCE_DIR)/$(MAIN_FILE).ml

$(BIN_DIR)/$(TEST_EX_NAME): $(TEST_FILES:%=$(OBJ_DIR)/%.cmo) $(TEST_OBJ_DIR)/$(TEST_MAIN_FILE).cmo
$(DIR_GUARD)
ocamlfind ocamlc $(OCAMLC_FLAGS) -package $(PACKAGES) -thread -linkpkg $(TEST_FILES:%=$(OBJ_DIR)/%.cmo) $(TEST_OBJ_DIR)/$(TEST_MAIN_FILE).cmo -o $(BIN_DIR)/$(TEST_EX_NAME)

$(TEST_OBJ_DIR)/$(TEST_MAIN_FILE).cmo: $(TEST_FILES:%=$(OBJ_DIR)/%.cmo) $(TEST_SOURCE_DIR)/$(TEST_MAIN_FILE).ml
$(DIR_GUARD)
ocamlfind ocamlc $(OCAMLC_FLAGS) -package $(PACKAGES) -thread -o $(TEST_OBJ_DIR)/$(TEST_MAIN_FILE) -c $(TEST_SOURCE_DIR)/$(TEST_MAIN_FILE).ml

#Special rules for creating the lexer and parser
$(SOURCE_DIR)/parser.ml $(SOURCE_DIR)/parser.mli: $(SOURCE_DIR)/parser.mly
ocamlyacc $<
Expand Down Expand Up @@ -91,7 +117,7 @@ $(OBJ_DIR)/%.cmi $(OBJ_DIR)/%.cmo $(OBJ_DIR)/%.cmt: $(SOURCE_DIR)/%.ml
include depend

clean:
rm -r -f $(BIN_DIR)/* $(RELEASE_DIR)/* $(SOURCE_DIR)/parser.mli $(SOURCE_DIR)/parser.ml $(SOURCE_DIR)/lexer.ml $(OBJ_DIR)/*.cmt $(LOGIC_OBJ_DIR)/*.cmt $(OBJ_DIR)/*.cmti $(LOGIC_OBJ_DIR)/*.cmti $(OBJ_DIR)/*.cmo $(LOGIC_OBJ_DIR)/*.cmo $(OBJ_DIR)/*.cmi $(LOGIC_OBJ_DIR)/*.cmi
rm -r -f $(BIN_DIR)/* $(RELEASE_DIR)/* $(SOURCE_DIR)/parser.mli $(SOURCE_DIR)/parser.ml $(SOURCE_DIR)/lexer.ml $(OBJ_DIR)/*.cmt $(LOGIC_OBJ_DIR)/*.cmt $(TEST_OBJ_DIR)/*.cmt $(OBJ_DIR)/*.cmti $(LOGIC_OBJ_DIR)/*.cmti $(TEST_OBJ_DIR)/*.cmti $(OBJ_DIR)/*.cmo $(LOGIC_OBJ_DIR)/*.cmo $(TEST_OBJ_DIR)/*.cmo $(OBJ_DIR)/*.cmi $(LOGIC_OBJ_DIR)/*.cmi $(TEST_OBJ_DIR)/*.cmi

depend:
ocamlfind ocamldep $(OCAMLDEP_FLAGS) $(FILES:%=$(SOURCE_DIR)/%.ml) $(SOURCE_DIR)/lexer.mll $(SOURCE_DIR)/parser.mli |sed -e 's/$(SOURCE_DIR)/$(BIN_DIR)/g' > depend
Expand Down
Loading