From 268dfff597ece230496f897122511fa32bf8a9ce Mon Sep 17 00:00:00 2001
From: Martin Suda <sudam@cs.man.ac.uk>
Date: Mon, 10 Jun 2024 18:45:59 +0200
Subject: [PATCH] updated all other samplers

---
 samplers/samplerFNT.txt |  33 ++++++++---
 samplers/samplerFOL.txt |  11 +++-
 samplers/samplerIND.txt | 122 ++++++++++++++++++++++++++++++----------
 samplers/samplerSMT.txt |  52 +++++++++++------
 4 files changed, 162 insertions(+), 56 deletions(-)

diff --git a/samplers/samplerFNT.txt b/samplers/samplerFNT.txt
index f7787a5412..2306b7fc4f 100644
--- a/samplers/samplerFNT.txt
+++ b/samplers/samplerFNT.txt
@@ -29,7 +29,9 @@ $nm=Z > nm ~cat 0:1
 $nm=NZ > nm ~sgd 0.07,2
 
 # inequality_splitting
-> ins ~cat 0:20,1:4,2:3,3:2,4:1
+> $ins ~cat Z:2,NZ:1
+$ins=Z > ins ~cat 0:1
+$ins=NZ > ins ~sgd 0.4,1
 
 # random_polarities
 > rp ~cat off:3,on:1
@@ -70,8 +72,10 @@ sa!=fmb > awrs ~cat constant:8,decay:1,converge:1
 sa!=fmb  awrs!=constant > awrsf ~ui 1,500
 
 # nongoal_weight_coefficient
-sa!=fmb > nwc ~cat 1:2,2:1
-sa!=fmb nwc!=1 > nwc ~ui 2,15
+sa!=fmb > $nwc ~cat 1:2,666:1
+sa!=fmb $nwc=1 > nwc ~cat 1:1
+sa!=fmb $nwc!=1 > nwc ~uf 0.5,15.0
+# TODO: we will most likely want a new distribution here for ($nwc!=1) just above!
 
 # restrict_nwc_to_goal_constants
 sa!=fmb nwc!=1 > rnwc ~cat off:5,on:1
@@ -130,6 +134,9 @@ sa!=fmb > cond ~cat off:500,on:89,fast:61
 # equational_tautology_removal
 sa!=fmb > etr ~cat off:500,on:30
 
+# instance_redundancy_check
+sa!=fmb > irc ~cat lazy:1,eager:1,off:5
+
 # extensionality_resolution
 sa!=fmb ins=0 > er ~cat off:500,known:25,filter:26
 
@@ -151,6 +158,12 @@ fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
 sa!=fmb $drc=1 > drc ~cat on:643,encompass:554,off:520
 
+# demodulation_precompiled_comparison
+sa!=fmb $drc=1 > dpc ~cat on:1,off:1
+
+# demodulation_only_equational
+sa!=fmb $drc=1 > doe ~cat on:1,off:1
+
 # function_definition_introduction
 sa!=fmb > fdi ~cat 0:100,2:1,4:1,8:1,16:1,32:1,64:1,128:1,256:1,512:1,1024:1
 
@@ -252,13 +265,15 @@ sa!=fmb av=on > alpa ~cat none:300,false:13,true:6,random:4
 sa!=fmb av=on > anc ~cat known:300,all_dependent:38,all:45,none:48
 
 # avatar_turn_off_time_frac
-sa!=fmb av=on > atotf ~cat 1.0:10,0.5:1
-# careful that 1.0 becomes "1" by the ->toFloat->toStr internal transformation
-sa!=fmb atotf!=1 > atotf ~uf 0.0,0.5
+# sa!=fmb av=on > $atotf ~cat 1:10,666:1
+# sa!=fmb av=on $atotf=1 > atotf ~cat 1:1
+# sa!=fmb av=on $atotf!=1 > atotf ~uf 0.0,0.7
+# TODO: leaving out weird timing dependent options
 
 # avatar_flush_period
-sa!=fmb av=on > afp ~cat 0:15,1:1
-sa!=fmb afp!=0 > afp ~cat 1:1,10:1,50:1,300:1,1000:1,2000:1,4000:1,10000:1,40000:1,100000:1,1000000:1
+sa!=fmb av=on > $afp ~cat 0:15,666:1
+sa!=fmb av=on $afp=0 > afp ~cat 0:1
+sa!=fmb av=on $afp!=0 > afp ~cat 1:1,10:1,50:1,300:1,1000:1,2000:1,4000:1,10000:1,40000:1,100000:1,1000000:1
 
 # avatar_flush_quotient
 sa!=fmb afp!=0 > afq ~uf 1.0,3.0
@@ -331,7 +346,7 @@ fmbdsb=on > fmbdsbt ~cat 1:5,2:2,3:1
 # fmb_keep_sbeam_generators
 sa=fmb fmbes=sbeam > fmbksg ~cat off:2,on:1
 
-# fmb_start_size - setting this to values > 1 is making things "finite mode incomplete" (but could save time for some problems)
+# fmb_start_size - setting this to values > 1 is making things "finite model incomplete" (but could save time for some problems)
 sa=fmb > $fmbss ~cat 1:5,666:1
 $fmbss=1 > fmbss ~cat 1:1
 $fmbss=666 > fmbss ~sgd 0.1,1
diff --git a/samplers/samplerFOL.txt b/samplers/samplerFOL.txt
index 8ea60b8bf8..9387522521 100644
--- a/samplers/samplerFOL.txt
+++ b/samplers/samplerFOL.txt
@@ -60,7 +60,7 @@ ss!=off > st ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:
 # SATURATION
 
 # saturation_algorithms
-> sa     ~cat lrs:600,discount:572,otter:236
+> sa ~cat lrs:600,discount:572,otter:236
 
 # literal selection
 > $s_pos ~cat Y:4,N:1
@@ -170,6 +170,9 @@ bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1
 # equational_tautology_removal
 > etr ~cat off:500,on:30
 
+# instance_redundancy_check
+> irc ~cat lazy:1,eager:1,off:5
+
 # extensionality_resolution
 ins=0 > er ~cat off:500,known:25,filter:26
 
@@ -191,6 +194,12 @@ fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
 $drc=1 > drc ~cat encompass:500,on:500,off:354
 
+# demodulation_precompiled_comparison
+$drc=1 > dpc ~cat on:1,off:1
+
+# demodulation_only_equational
+$drc=1 > doe ~cat on:1,off:1
+
 # forward_literal_rewriting
 > flr ~cat off:8,on:1
 
diff --git a/samplers/samplerIND.txt b/samplers/samplerIND.txt
index 9abd78f3ed..e160556262 100644
--- a/samplers/samplerIND.txt
+++ b/samplers/samplerIND.txt
@@ -17,19 +17,21 @@ ep!=off > mep ~cat on:10,off:1
 # general_splitting
 > gsp ~cat off:8,on:1
 
-# inline_let -- this is probably irrelevant on TPTP anyway
-> ile ~cat off:10,on:1
-
 # newcnf
 > newcnf ~cat on:9,off:25
 
+# inline_let -- this is probably irrelevant on TPTP anyway
+newcnf=on > ile ~cat off:10,on:1
+
 # naming
 > $nm ~cat Z:1,NZ:5
 $nm=Z > nm ~cat 0:1
 $nm=NZ > nm ~sgd 0.07,2
 
 # inequality_splitting
-> ins ~cat 0:20,1:4,2:3,3:2,4:1
+> $ins ~cat Z:2,NZ:1
+$ins=Z > ins ~cat 0:1
+$ins=NZ > ins ~sgd 0.4,1
 
 # random_polarities
 > rp ~cat off:3,on:1
@@ -38,7 +40,16 @@ $nm=NZ > nm ~sgd 0.07,2
 > tgt ~cat off:10,ground:6,full:5
 
 # set_of_support
-> sos ~cat off:80,on:17,all:10
+> sos ~cat off:80,on:17,all:10,theory:10
+
+# sos_theory_limit
+sos=theory > sstl ~cat 0:10,1:1,2:1,3:1
+
+# theory_axioms
+> tha ~cat on:10,off:1,some:3
+
+# theory_flattening
+> thf ~cat on:1,off:10
 
 # sine_selection
 > ss ~cat off:1182,included:135,axioms:392
@@ -58,7 +69,7 @@ ss!=off > st ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:
 # SATURATION
 
 # saturation_algorithms
-> sa     ~cat lrs:600,discount:572,otter:236
+> sa ~cat lrs:600,discount:572,otter:236
 
 # literal selection
 > $s_pos ~cat Y:4,N:1
@@ -84,8 +95,11 @@ $ls=on > lsd ~cat 0:20,1:1,5:1,10:1,20:1,50:1,100:1
 sa=lrs > lwlo ~cat off:5,on:1
 
 # lrs_estimate_correction_coef
-sa=lrs > lecc ~cat 1:10,666:1
-lecc!=1 > lecc ~uf 0.5,2.0
+# > $lecc ~cat 1:1
+# sa=lrs > $lecc ~cat 1:10,666:1
+# sa=lrs $lecc=1 > lecc ~cat 1.0:1
+# sa=lrs $lecc!=1 > lecc ~uf 0.5,2.0
+# TODO: leaving out weird timing dependent options
 
 # age_weight_ratio_shape
 > awrs ~cat constant:8,decay:1,converge:1
@@ -94,8 +108,16 @@ lecc!=1 > lecc ~uf 0.5,2.0
 awrs!=constant > awrsf ~ui 1,500
 
 # nongoal_weight_coefficient
-> nwc ~cat 1:2,2:1
-nwc!=1 > nwc ~ui 2,15
+> $nwc ~cat 1:2,666:1
+$nwc=1 > nwc ~cat 1:1
+$nwc!=1 > nwc ~uf 0.5,15.0
+# TODO: we will most likely want a new distribution here for ($nwc!=1) just above!
+
+# increased_numeral_weight
+> inw ~cat off:5,on:1
+
+# introduced_symbol_precedence
+> isp ~cat top:10,bottom:1
 
 # restrict_nwc_to_goal_constants
 nwc!=1 > rnwc ~cat off:5,on:1
@@ -160,12 +182,12 @@ bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1
 # condensation
 > cond ~cat off:500,on:89,fast:61
 
-# demodulation_redundancy_check
-> drc ~cat encompass:500,on:500,off:354
-
 # equational_tautology_removal
 > etr ~cat off:500,on:30
 
+# instance_redundancy_check
+> irc ~cat lazy:1,eager:1,off:5
+
 # extensionality_resolution
 ins=0 > er ~cat off:500,known:25,filter:26
 
@@ -181,6 +203,18 @@ er!=off > erml ~cat 0:3,2:1,3:1
 # forward_demodulation
 > fd ~cat all:500,off:41,preordered:168
 
+# demodulation_redundancy_check
+> $drc ~cat 0:1
+fd!=off > $drc ~cat 1:1
+bd!=off > $drc ~cat 1:1
+$drc=1 > drc ~cat encompass:500,on:500,off:354
+
+# demodulation_precompiled_comparison
+$drc=1 > dpc ~cat on:1,off:1
+
+# demodulation_only_equational
+$drc=1 > doe ~cat on:1,off:1
+
 # forward_literal_rewriting
 > flr ~cat off:8,on:1
 
@@ -190,9 +224,6 @@ er!=off > erml ~cat 0:3,2:1,3:1
 # inner_rewriting
 > irw ~cat off:165,on:6
 
-# unit_resulting_resolution
-> urr ~cat off:1200,ec_only:162,on:340
-
 # SINE LEVELS and shit
 
 # sine_to_age
@@ -247,9 +278,19 @@ $s2a=on > s2agt ~cat 0:7,5:1,10:1,15:1,20:1,30:1,50:1,100:1
 # sine_to_age_tolerance
 $s2a=on > s2at ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:15,5.0:50,5.5:10,6.0:30,7.0:20
 
-# AVATAR
+# AVATAR - main
 > av ~cat on:15,off:4
 
+# SAT SOLVER
+
+# sat_solver
+av=on > sas ~cat minisat:1,z3:1
+
+# sat_fallback_for_smt
+av=on sas=z3 > sffsmt ~cat off:5,on:1
+
+# AVATAR - rest
+
 # avatar_add_complementary
 av=on > aac ~cat none:147,ground:600
 
@@ -257,7 +298,7 @@ av=on > aac ~cat none:147,ground:600
 av=on > abs ~cat on:63,off:300
 
 # avatar_congruence_closure
-av=on > acc ~cat off:600,model:24,on:58
+av=on sas!=z3 > acc ~cat off:600,model:24,on:58
 
 # cc_unsat_cores
 acc!=off > ccuc ~cat first:1,small_ones:1,all:3
@@ -282,13 +323,15 @@ av=on > alpa ~cat none:300,false:13,true:6,random:4
 av=on > anc ~cat known:300,all_dependent:38,all:45,none:48
 
 # avatar_turn_off_time_frac
-av=on > atotf ~cat 1.0:10,0.5:1
-# careful that 1.0 becomes "1" by the ->toFloat->toStr internal transformation
-atotf!=1 > atotf ~uf 0.0,0.5
+# av=on > $atotf ~cat 1:10,666:1
+# av=on $atotf=1 > atotf ~cat 1:1
+# av=on $atotf!=1 > atotf ~uf 0.0,0.7
+# TODO: leaving out weird timing dependent options
 
 # avatar_flush_period
-av=on > afp ~cat 0:15,1:1
-afp!=0 > afp ~cat 1:1,10:1,50:1,300:1,1000:1,2000:1,4000:1,10000:1,40000:1,100000:1,1000000:1
+av=on > $afp ~cat 0:15,666:1
+av=on $afp=0 > afp ~cat 0:1
+av=on $afp!=0 > afp ~cat 1:1,10:1,50:1,300:1,1000:1,2000:1,4000:1,10000:1,40000:1,100000:1,1000000:1
 
 # avatar_flush_quotient
 afp!=0 > afq ~uf 1.0,3.0
@@ -299,11 +342,11 @@ av=on > nicw ~cat off:600,on:76
 # split_at_activation
 av=on > sac ~cat off:3,on:1
 
-# sat_solver (NOTE: requires compiling with Z3)
-av=on > sas ~cat minisat:10,z3:3
+# BACK TO PREPROCESSING
 
-# sat_fallback_for_smt
-sas=z3 > sffsmt ~cat off:10,on:1
+# unit_resulting_resolution
+av=on  > urr ~cat off:1200,ec_only:162,on:300,full:40
+av=off > urr ~cat off:1200,ec_only:162,on:340
 
 # AVATAR SPLIT QUEUE
 
@@ -336,7 +379,7 @@ gs=on av=on > gsaa ~cat off:30,from_current:11,full_model:3
 
 > uhcvi ~cat off:1,on:1
 
-# GOAL GUESSING - useful for indution on SMTLIB problems (without assert-not)
+# GOAL GUESSING - useful for induction on SMTLIB problems (without assert-not)
 
 # guess_the_goal
 > gtg ~cat off:10,all:1,exists_top:1,exists_all:1,exists_sym:1,position:1
@@ -344,6 +387,23 @@ gs=on av=on > gsaa ~cat off:30,from_current:11,full_model:3
 # guess_the_goal_limit
 gtg!=off > gtgl ~ui 1,5
 
+# THEORY SPLIT QUEUE
+
+# theory_split_queue
+> thsq ~cat off:10,on:1
+
+# theory_split_queue_layered_arrangement
+thsq=on > thsql ~cat on:11,off:3
+
+# theory_split_queue_cutoffs
+thsq=on > thsqc ~cat 0:1,8:1,16:2,32:5,64:5,128:2
+
+# theory_split_queue_ratios
+thsq=on > thsqr ~u2r -3;3;,
+
+# theory_split_queue_expected_ratio_denom
+thsq=on > thsqd ~cat 2:1,4:1,8:7,32:5,64:2,128:1
+
 # INDUCTION (focusing on structural)
 
 # induction
@@ -460,5 +520,9 @@ thi!=off > thigen ~cat off:1,on:1
 thi!=off > thitd ~cat off:1,on:1
 
 # unification_with_abstraction
-> uwa ~cat off:5,interpreted_only:1,one_side_interpreted:1,one_side_constant:1,all:1,ground:1
+> uwa ~cat off:5,interpreted_only:1,one_side_interpreted:1,one_side_constant:1,all:1,ground:1,func_ext:1,ac1:1,ac2:1
+
+# unification_with_abstraction_postpro
+> uwa_fpi ~cat off:5,on:1
+
 
diff --git a/samplers/samplerSMT.txt b/samplers/samplerSMT.txt
index 2b7516fd9c..f60a21bb88 100644
--- a/samplers/samplerSMT.txt
+++ b/samplers/samplerSMT.txt
@@ -32,7 +32,9 @@ $nm=Z > nm ~cat 0:1
 $nm=NZ > nm ~sgd 0.07,2
 
 # inequality_splitting
-> ins ~cat 0:20,1:4,2:3,3:2,4:1
+> $ins ~cat Z:2,NZ:1
+$ins=Z > ins ~cat 0:1
+$ins=NZ > ins ~sgd 0.4,1
 
 # random_polarities
 > rp ~cat off:3,on:1
@@ -96,8 +98,11 @@ $ls=on > lsd ~cat 0:20,1:1,5:1,10:1,20:1,50:1,100:1
 sa=lrs > lwlo ~cat off:5,on:1
 
 # lrs_estimate_correction_coef
-sa=lrs > lecc ~cat 1:10,666:1
-lecc!=1 > lecc ~uf 0.5,2.0
+# > $lecc ~cat 1:1
+# sa=lrs > $lecc ~cat 1:10,666:1
+# sa=lrs $lecc=1 > lecc ~cat 1.0:1
+# sa=lrs $lecc!=1 > lecc ~uf 0.5,2.0
+# TODO: leaving out weird timing dependent options
 
 # age_weight_ratio_shape
 > awrs ~cat constant:8,decay:1,converge:1
@@ -106,8 +111,10 @@ lecc!=1 > lecc ~uf 0.5,2.0
 awrs!=constant > awrsf ~ui 1,500
 
 # nongoal_weight_coefficient
-> nwc ~cat 1:2,2:1
-nwc!=1 > nwc ~ui 2,15
+> $nwc ~cat 1:2,666:1
+$nwc=1 > nwc ~cat 1:1
+$nwc!=1 > nwc ~uf 0.5,15.0
+# TODO: we will most likely want a new distribution here for ($nwc!=1) just above!
 
 # increased_numeral_weight
 > inw ~cat off:5,on:1
@@ -181,6 +188,9 @@ bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1
 # equational_tautology_removal
 > etr ~cat off:500,on:30
 
+# instance_redundancy_check
+> irc ~cat lazy:1,eager:1,off:5
+
 # extensionality_resolution
 ins=0 > er ~cat off:500,known:25,filter:26
 
@@ -197,10 +207,16 @@ er!=off > erml ~cat 0:3,2:1,3:1
 > fd ~cat all:500,off:41,preordered:168
 
 # demodulation_redundancy_check
-> $set_drc ~cat N:1
-fd!=off > $set_drc ~cat Y:1
-bd!=off > $set_drc ~cat Y:1
-$set_drc=Y > drc ~cat encompass:500,on:500,off:354
+> $drc ~cat 0:1
+fd!=off > $drc ~cat 1:1
+bd!=off > $drc ~cat 1:1
+$drc=1 > drc ~cat encompass:500,on:500,off:354
+
+# demodulation_precompiled_comparison
+$drc=1 > dpc ~cat on:1,off:1
+
+# demodulation_only_equational
+$drc=1 > doe ~cat on:1,off:1
 
 # forward_literal_rewriting
 > flr ~cat off:8,on:1
@@ -310,13 +326,15 @@ av=on > alpa ~cat none:300,false:13,true:6,random:4
 av=on > anc ~cat known:300,all_dependent:38,all:45,none:48
 
 # avatar_turn_off_time_frac
-av=on > atotf ~cat 1.0:10,0.5:1
-# careful that 1.0 becomes "1" by the ->toFloat->toStr internal transformation
-atotf!=1 > atotf ~uf 0.0,0.5
+# av=on > $atotf ~cat 1:10,666:1
+# av=on $atotf=1 > atotf ~cat 1:1
+# av=on $atotf!=1 > atotf ~uf 0.0,0.7
+# TODO: leaving out weird timing dependent options
 
 # avatar_flush_period
-av=on > afp ~cat 0:15,1:1
-afp!=0 > afp ~cat 1:1,10:1,50:1,300:1,1000:1,2000:1,4000:1,10000:1,40000:1,100000:1,1000000:1
+av=on > $afp ~cat 0:15,666:1
+av=on $afp=0 > afp ~cat 0:1
+av=on $afp!=0 > afp ~cat 1:1,10:1,50:1,300:1,1000:1,2000:1,4000:1,10000:1,40000:1,100000:1,1000000:1
 
 # avatar_flush_quotient
 afp!=0 > afq ~uf 1.0,3.0
@@ -327,9 +345,6 @@ av=on > nicw ~cat off:600,on:76
 # split_at_activation
 av=on > sac ~cat off:3,on:1
 
-# TODO: consider enabling this for vampire_z3 compiles!
-# av=on > sas ~cat minisat:10,z3:1
-
 # BACK TO PREPROCESSING
 
 # unit_resulting_resolution
@@ -394,6 +409,9 @@ thsq=on > thsqd ~cat 2:1,4:1,8:7,32:5,64:2,128:1
 
 # TERM ALGEBRA REASONINING
 
+# term_algebra_exhaustiveness_axiom
+> taea ~cat off:1,on:1
+
 # term_algebra_acyclicity
 > tac ~cat off:3,axiom:1,rule:1,light:1