config.properties

# write the outputed saturation into a Datalog file (instead of printing it)
write_output=false

# select the algorithm used for the TGD saturation
# It can be: gsat (default), skolem_sat, simple_sat, ordered_skolem_sat, hyper_sat
saturation_alg=gsat

# force ordered skolem saturation to select a skolem atom in the body
# even if the head atom is maximal (experimental maybe not correct)
ordered_skolemsat_select_skolem_body_atom = false

debug=false

# timeout in seconds
# timeout=30

# are negative constraints included
negative_constraint=true

# change the way variables are renamed in VNF
sorted_vnf=true

# Subsumption method defines the overapproximation of TGD subsumption
# used before the underapproximation, which is always the syntactical subsumption
# exempt in the case "disabled" case
# - disabled        no subsumption is performed
# - min_predicate   the overapproximation is based on a minamal predicate 
# - min_atom        the overapproximation is based on a minamal atom 
# - tree_predicate  the overapproximation is based on an index of predicates 
# - identity        no overapproximation is performed
subsumption_method=tree_predicate

# Simple sat filters the full TGDs it generates 
# such that their body always contains at least a predicate 
# appearing in a non full TGDs head
simple_sat_predicate_filter=true

# skolemization type sets the way to transform 
# the input TGDs to single headed skolemized TGDs
# - NAIVE skolemized first on every universal variable
#         and split the head to form single headed TGDs
#         ex: A(x, y) -> B(y, z) becomes A(x, y) -> B(y, f(x,y))
# - PROJ_ON_FRONTIER introduces a new predicates to project the universal variables
#                    on the frontier variables, then do the naive steps.
#                    ex: A(x, y) -> B(y, z) becomes A(x, y) -> C(y) and C(y) -> B(y, f(y))
skolemization_type=PROJ_ON_FRONTIER

# ========= Evolve-Based algoritm optimizations ========= 

# In order to filter candidates for unification, we used two unification indexes finding
# candidates for unification with a given resp. a left or right input TGD for an evolve inference rule
# By default, each algorithm comes with its best unification indexes, but you can force the use of unification index type using the following parameter
# - DISABLED_INDEX, no index is used 
# - PREDICATE_INDEX, indexes based on the predicates contained in the body or the head
# - ATOM_PATH_INDEX, indexes based on path indexing method defined by Mark E. Stickel (good for Skolem-based algorithm)
# optimization.unification_index_type = ATOM_PATH_INDEX

# In evolved based algorithms, the new TGDs (right and left) are stored 
# in sets :
# - SET, for hashset
# - ORDERED_BY_ATOMS_NB, such that the TGDs with smallest body and largest head come first
# - STACK
optimization.new_tgd_structure = ORDERED_BY_ATOMS_NB

# In evolved based algorithms, the new TGDs can be subsumed by the TGDs outputed by an 
# evolve application on this new TGD and others TGDs. This parameter allows stop to apply evolve
# using this new TGDs, when it is subsumed by one of the outputed TGDs.
optimization.stop_evolving_if_subsumed = true

# True, if the evolving tgd are sorted 
optimization.evolving_tgd_ordering = true

# In evolve-based saturation, if true, the new derived non full TGDs will be discarded,
# if their head do not contains at least a new atom (w.r.t. the evolved non full TGD ),
# whose predicate appears in at least one other TGD body.
optimization.discard_useless_tgd = true

# enable the tautology TGDs to be discarded 
optimization.discard_tautology = true

optimization.apply_structural_transformation = false

optimization.maxPredicate = 15


# ========= Datalog solver options ========= 

# Enable or disable the solver after the saturation process
saturation_only=true

## I-DLV executable and options
solver.name=idlv

# Windows executable
# solver.path=executables/idlv_1.1.6_windows_x86-64.exe

# Linux executable
solver.path=executables/idlv_1.1.6_linux_x86-64
solver.options.grounding=--t --no-facts --check-edb-duplication
solver.options.query=--query

## DLV executable and options
# solver.name=dlv

# Windows executable
# solver.path=executables/dlv.mingw.exe

# Linux executable
# solver.path=executables/dlv.x86-64-linux-elf-static.bin
# solver.options.grounding=-nofacts
# solver.options.query=-silent -FC

## DLV2 executable and options
# solver.name=dlv2

# Windows executable
# solver.path=executables/dlv2-windows.exe

# Linux executable
# solver.path=executables/dlv2-linux
# solver.options.grounding=--t --no-facts --check-edb-duplication
# solver.options.query=--silent --query --mode=idlv

## Execution options
solver.output.to_file=false

# to compute the full grounding/materialisation
solver.full_grounding=true