update the sampler accordingly

vprover · Dec 7, 2023 · f43eb76 · f43eb76
1 parent 1778675
commit f43eb76
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 9 deletions.
diff --git a/samplerFNT.txt b/samplerFNT.txt
@@ -154,9 +154,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
-
 # binary_resolution
 urr=on > br ~cat on:10,off:1
 
@@ -269,6 +266,12 @@ 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
+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
 
 # avatar_split_queue

diff --git a/samplerFOL.txt b/samplerFOL.txt
@@ -190,9 +190,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
@@ -302,6 +299,12 @@ 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
+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
 
 # avatar_split_queue

diff --git a/samplerSMT.txt b/samplerSMT.txt
@@ -216,9 +216,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
@@ -328,6 +325,12 @@ 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
+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
 
 # avatar_split_queue