From 1600b1140b62c9b1c3564960a7f630808863afac Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Sun, 7 Jun 2026 10:05:55 +0200 Subject: [PATCH 1/7] Attempt to fix error related to not fool eliminating type quantifiers in the lazy cnf-on-the-fly case --- Kernel/Formula.cpp | 23 +++++++++++++++++++++++ Kernel/Formula.hpp | 1 + Kernel/HOL/Convert.cpp | 13 +------------ Shell/FOOLElimination.cpp | 16 ++++++++++++++++ 4 files changed, 41 insertions(+), 12 deletions(-) diff --git a/Kernel/Formula.cpp b/Kernel/Formula.cpp index 8e19bd173..e5a4b81fc 100644 --- a/Kernel/Formula.cpp +++ b/Kernel/Formula.cpp @@ -451,6 +451,29 @@ Formula* Formula::quantify(Formula* f) return f; } +/** removes the leading universal quantifiers from a formula */ +Formula* Formula::removeUniversalTypePrenex(Formula* f) +{ + while (f->connective() == FORALL) { + auto vars = f->vars(); + // get rid of current universal type prenex + while (vars && vars->head().second == AtomicSort::superSort()) { + vars = vars->tail(); + } + // if there was none, return original formula + if (vars == f->vars()) { + break; + } + // if there are vars remaining, we return a new formula + if (vars) { + return new QuantifiedFormula(FORALL, vars, f->qarg()); + } + // otherwise we recurse + f = f->qarg(); + } + return f; +} + /** * Return formula equal to @b cl diff --git a/Kernel/Formula.hpp b/Kernel/Formula.hpp index e212d0d5f..21b3660db 100644 --- a/Kernel/Formula.hpp +++ b/Kernel/Formula.hpp @@ -87,6 +87,7 @@ class Formula static Formula* fromClause(Clause* cl,bool closed = true); static Formula* quantify(Formula* f); + static Formula* removeUniversalTypePrenex(Formula* f); static Formula* trueFormula(); static Formula* falseFormula(); diff --git a/Kernel/HOL/Convert.cpp b/Kernel/HOL/Convert.cpp index dbc2bbdd4..4f20f41d6 100644 --- a/Kernel/HOL/Convert.cpp +++ b/Kernel/HOL/Convert.cpp @@ -175,16 +175,5 @@ TermList HOL::convert::toNameless(TermList term) { TermList HOL::convert::toNameless(Formula* formula) { - // remove leading universal type quantifiers - if (formula->connective() == FORALL) { - auto vars = formula->vars(); - while (vars && vars->head().second == AtomicSort::superSort()) { - vars = vars->tail(); - } - if (vars != formula->vars()) { - auto f = formula->qarg(); - formula = vars ? new QuantifiedFormula(FORALL, vars, f) : f; - } - } - return formulaToNameless(formula, {}); + return formulaToNameless(Formula::removeUniversalTypePrenex(formula), {}); } diff --git a/Shell/FOOLElimination.cpp b/Shell/FOOLElimination.cpp index ebfe78ba0..16412be98 100644 --- a/Shell/FOOLElimination.cpp +++ b/Shell/FOOLElimination.cpp @@ -170,6 +170,22 @@ FormulaUnit* FOOLElimination::apply(FormulaUnit* unit) { env.options->cnfOnTheFly() != Options::CNFOnTheFly::OFF && (env.options->cnfOnTheFly() != Options::CNFOnTheFly::CONJ_EAGER || !isConjecture); + // proxification fails in HOL::convert::toNameless for formulas that contain + // non-prenex type quantifiers, so we simply override this decision for them + if (env.higherOrder() && proxify) { + auto qf = Formula::removeUniversalTypePrenex(formula); + if (iterTraits(vi(new SubformulaIterator(qf))).any([](Formula* f) { + // quantified formulas with any type variable + // TODO remove leading forall block as in HOL::convert::toNameless + return (f->connective() == FORALL || f->connective() == EXISTS) && + iterTraits(Kernel::VSList::Iterator(f->vars())).any([](auto kv) { + return kv.second == AtomicSort::superSort(); + }); + })) { + proxify = false; + } + } + Formula* processedFormula = proxify ? convertToProxified(formula) : process(formula); if (formula == processedFormula) { return rectifiedUnit; From 8514064691cbea4b31b9befcc33ed24b3fea8a8d Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Sun, 7 Jun 2026 10:38:17 +0200 Subject: [PATCH 2/7] Disable fmb for now in HO sampler --- samplers/samplerHOL.smp | 227 +++++++++++++++++----------------------- 1 file changed, 94 insertions(+), 133 deletions(-) diff --git a/samplers/samplerHOL.smp b/samplers/samplerHOL.smp index 8a17fe354..19c3888a8 100644 --- a/samplers/samplerHOL.smp +++ b/samplers/samplerHOL.smp @@ -62,12 +62,11 @@ intent=unsat ss!=off > st ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:1 # SATURATION # saturation_algorithms -intent=unsat ep=off > sa ~cat fmb:10,lrs:600,discount:572,otter:236 -intent=unsat ep!=off > sa ~cat lrs:600,discount:572,otter:236 -intent=sat > sa ~cat fmb:22,otter:60,discount:28 +intent=unsat > sa ~cat lrs:600,discount:572,otter:236 +intent=sat > sa ~cat otter:60,discount:28 # set_of_support -intent=unsat sa!=fmb > sos ~cat off:80,on:17,all:10 +intent=unsat > sos ~cat off:80,on:17,all:10 # lrs_first_time_check > $lftc ~cat N:5,Y:1 @@ -75,29 +74,29 @@ sa=lrs $lftc=Y > lftc ~ui 5,95 # literal selection > $s_pos ~cat Y:4,N:1 -intent=unsat sa!=fmb $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50,1002:141,1003:14,1004:23,1010:145,1011:357,1666:50 -intent=unsat sa!=fmb $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50,-1002:141,-1003:14,-1004:23,-1010:145,-1011:357,-1666:50 +intent=unsat $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50,1002:141,1003:14,1004:23,1010:145,1011:357,1666:50 +intent=unsat $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50,-1002:141,-1003:14,-1004:23,-1010:145,-1011:357,-1666:50 -intent=sat sa!=fmb $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50 -intent=sat sa!=fmb $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50 +intent=sat $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50 +intent=sat $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50 # lookahaed_delay > $ls ~cat off:1 -sa!=fmb s=11 > $ls ~cat on:1 -sa!=fmb s=-11 > $ls ~cat on:1 -sa!=fmb s=1011 > $ls ~cat on:1 -sa!=fmb s=-1011 > $ls ~cat on:1 +s=11 > $ls ~cat on:1 +s=-11 > $ls ~cat on:1 +s=1011 > $ls ~cat on:1 +s=-1011 > $ls ~cat on:1 -sa!=fmb $ls=on > lsd ~cat 0:20,1:1,5:1,10:1,20:1,50:1,100:1 +$ls=on > lsd ~cat 0:20,1:1,5:1,10:1,20:1,50:1,100:1 # age_weight_ratio -sa!=fmb > $awr ~cat A:1,W:1,AW:98 -sa!=fmb $awr=A > awr ~set 1:0 -sa!=fmb $awr=W > awr ~set 0:1 -sa!=fmb $awr=AW > awr ~u2r -10;4;: +> $awr ~cat A:1,W:1,AW:98 +$awr=A > awr ~set 1:0 +$awr=W > awr ~set 0:1 +$awr=AW > awr ~u2r -10;4;: # random_awr -sa!=fmb > rawr ~cat on:4,off:1 +> rawr ~cat on:4,off:1 # lrs_weight_limit_only sa=lrs > lwlo ~cat off:5,on:1 @@ -113,19 +112,19 @@ sa=lrs > lrd ~cat off:1,on:1 # TODO: leaving out weird timing dependent options # nongoal_weight_coefficient -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 +> $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! # restrict_nwc_to_goal_constants -sa!=fmb nwc!=1 > rnwc ~cat off:5,on:1 +nwc!=1 > rnwc ~cat off:5,on:1 # literal_maximality_aftercheck -sa!=fmb > lma ~cat off:500,on:83 +> lma ~cat off:500,on:83 # POSITIVE LITERAL SPLIT QUEUE -sa!=fmb > plsq ~cat off:4,on:1 +> plsq ~cat off:4,on:1 # positive_literal_split_queue_layered_arrangement plsq=on > plsql ~cat on:66,off:162 @@ -139,132 +138,132 @@ plsq=on > plsqr ~u2r -5;7;, # INFERENCES # superposition (don't turn this off at home!) -intent=unsat sa!=fmb > sup ~cat on:100,off:1 +intent=unsat > sup ~cat on:100,off:1 # simultaneous_superposition -sa!=fmb sup=on > sims ~cat on:50,off:1 +sup=on > sims ~cat on:50,off:1 # superposition_from_variables -intent=unsat sa!=fmb sup=on > sfv ~cat on:38,off:1 +intent=unsat sup=on > sfv ~cat on:38,off:1 # code_tree_subsumption -sa!=fmb > cts ~cat on:3,off:1 +> cts ~cat on:3,off:1 # forward_subsumption -sa!=fmb > fs ~cat on:500,off:31 +> fs ~cat on:500,off:31 # forward_subsumption_resolution -sa!=fmb fs=off > fsr ~cat off:1 -sa!=fmb fs=on > fsr ~cat on:500,off:193 +fs=off > fsr ~cat off:1 +fs=on > fsr ~cat on:500,off:193 # forward_subsumption_demodulation -sa!=fmb > fsd ~cat off:500,on:90 +> fsd ~cat off:500,on:90 # forward_subsumption_demodulation_max_matches -sa!=fmb fsd=on > fsdmm ~cat 0:10,1:3,2:2,3:1 +fsd=on > fsdmm ~cat 0:10,1:3,2:2,3:1 # backward_demodulation -sa!=fmb > bd ~cat all:500,off:245,preordered:91 +> bd ~cat all:500,off:245,preordered:91 # backward_subsumption -sa!=fmb fs!=off > bs ~cat off:500,unit_only:74,on:64 +fs!=off > bs ~cat off:500,unit_only:74,on:64 # backward_subsumption_resolution -sa!=fmb > bsr ~cat off:500,unit_only:118,on:75 +> bsr ~cat off:500,unit_only:118,on:75 # backward_subsumption_demodulation -sa!=fmb > bsd ~cat off:500,on:74 +> bsd ~cat off:500,on:74 # backward_subsumption_demodulation_max_matches -sa!=fmb bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1 +bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1 # condensation -sa!=fmb > cond ~cat off:500,on:89,fast:61 +> cond ~cat off:500,on:89,fast:61 # equational_tautology_removal -sa!=fmb > etr ~cat off:500,on:30 +> etr ~cat off:500,on:30 # extensionality_resolution -sa!=fmb ins=0 > er ~cat off:500,known:25,filter:26 +ins=0 > er ~cat off:500,known:25,filter:26 # extensionality_allow_pos_eq -sa!=fmb er=filter > eape ~cat off:3,on:1 +er=filter > eape ~cat off:3,on:1 # extensionality_max_length -sa!=fmb er!=off > erml ~cat 0:3,2:1,3:1 +er!=off > erml ~cat 0:3,2:1,3:1 # fool_paramodulation -sa!=fmb > foolp ~cat off:10,on:1 +> foolp ~cat off:10,on:1 # forward_demodulation -sa!=fmb > fd ~cat all:500,off:41,preordered:168 +> 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 -intent=unsat sa!=fmb $drc=1 > drc ~cat encompass:500,ordering:500,off:354 -intent=sat sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554 +intent=unsat $drc=1 > drc ~cat encompass:500,ordering:500,off:354 +intent=sat $drc=1 > drc ~cat ordering:643,encompass:554 # forward_demodulation_term_ordering_diagrams -sa!=fmb fd!=off > fdtod ~cat on:1,off:1 +fd!=off > fdtod ~cat on:1,off:1 # demodulation_only_equational -sa!=fmb $drc=1 > doe ~cat on:1,off:1 +$drc=1 > doe ~cat on:1,off:1 # forward_ground_joinability -sa!=fmb > fgj ~cat on:1,off:1 +> fgj ~cat on:1,off:1 # forward_literal_rewriting -intent=unsat sa!=fmb > flr ~cat off:8,on:1 +intent=unsat > flr ~cat off:8,on: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 +> fdi ~cat 0:100,2:1,4:1,8:1,16:1,32:1,64:1,128:1,256:1,512:1,1024:1 # inner_rewriting -sa!=fmb > irw ~cat off:165,on:6 +> irw ~cat off:165,on:6 # subsumption_equality_resolution -sa!=fmb > ser ~cat off:9,on:1 +> ser ~cat off:9,on:1 # SINE LEVELS and shit # sine_to_age -sa!=fmb > s2a ~cat off:2,on:1 +> s2a ~cat off:2,on:1 # sine_level_split_queue -sa!=fmb > slsq ~cat off:5,on:1 +> slsq ~cat off:5,on:1 # sine_level_split_queue_layered_arrangement -sa!=fmb slsq=on > slsql ~cat on:1,off:1 +slsq=on > slsql ~cat on:1,off:1 # sine_level_split_queue_cutoffs -sa!=fmb slsq=on > slsqc ~cat 0:10,1:10,2:6,3:3,4:1 +slsq=on > slsqc ~cat 0:10,1:10,2:6,3:3,4:1 # sine_level_split_queue_ratios -sa!=fmb slsq=on > slsqr ~u2r -5;2;, +slsq=on > slsqr ~u2r -5;2;, # ORDERING # term_ordering -sa!=fmb > to ~cat kbo:13,lpo:4 +> to ~cat kbo:13,lpo:4 # symbol_precedence -sa!=fmb > sp ~cat arity:100,const_min:72,frequency:130,const_frequency:49,reverse_frequency:55,reverse_arity:72,weighted_frequency:24,unary_first:28,occurrence:82,unary_frequency:14,const_max:18 +> sp ~cat arity:100,const_min:72,frequency:130,const_frequency:49,reverse_frequency:55,reverse_arity:72,weighted_frequency:24,unary_first:28,occurrence:82,unary_frequency:14,const_max:18 # symbol_precedence_boost -sa!=fmb > spb ~cat none:200,units:78,goal:91,goal_then_units:93,non_intro:14,intro:12 +> spb ~cat none:200,units:78,goal:91,goal_then_units:93,non_intro:14,intro:12 # kbo_max_zero -sa!=fmb to=kbo > kmz ~cat off:200,on:1 +to=kbo > kmz ~cat off:200,on:1 # kbo_weight_scheme -sa!=fmb to=kbo > kws ~cat const:50,inv_arity_squared:6,precedence:28,arity_squared:1,inv_arity:5,inv_frequency:8,frequency:2 +to=kbo > kws ~cat const:50,inv_arity_squared:6,precedence:28,arity_squared:1,inv_arity:5,inv_frequency:8,frequency:2 # literal_comparison_mode -intent=unsat sa!=fmb > lcm ~cat standard:500,reverse:66,predicate:51 -intent=sat sa!=fmb > lcm ~cat standard:500,reverse:66,predicate:51 +intent=unsat > lcm ~cat standard:500,reverse:66,predicate:51 +intent=sat > lcm ~cat standard:500,reverse:66,predicate:51 # sine_to_pred_levels -sa!=fmb lcm=standard > s2pl ~cat off:50,on:2,no:3 +lcm=standard > s2pl ~cat off:50,on:2,no:3 # SINE LEVELS - configure (must come after sine_to_age & slsq & s2pl) @@ -283,54 +282,53 @@ $s2a=on > s2agt ~cat 0:7,5:1,10:1,15:1,20:1,30:1,50:1,100:1 $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 -sa!=fmb > av ~cat on:15,off:4 +> av ~cat on:15,off:4 # partial_redundancy_check -sa!=fmb > prc ~cat on:3,off:5 +> prc ~cat on:3,off:5 # partial_redundancy_ordering_constraints -sa!=fmb prc=on > proc ~cat on:1,off:1 +prc=on > proc ~cat on:1,off:1 # partial_redundancy_avatar_constraints -sa!=fmb av=on prc=on > prac ~cat on:1,off:1 +av=on prc=on > prac ~cat on:1,off:1 # partial_redundancy_literal_constraints -sa!=fmb prc=on > prlc ~cat on:1,off:1 +prc=on > prlc ~cat on:1,off:1 # sat_solver -sa!=fmb $has_z3=true av=on > sas ~cat minisat:10,cadical:7,z3:3 -sa!=fmb $has_z3!=true av=on > sas ~cat minisat:10,cadical:7 -sa=fmb > sas ~cat minisat:7,cadical:10 +$has_z3=true av=on > sas ~cat minisat:10,cadical:7,z3:3 +$has_z3!=true av=on > sas ~cat minisat:10,cadical:7 # avatar_add_complementary -sa!=fmb av=on > aac ~cat none:147,ground:600 +av=on > aac ~cat none:147,ground:600 # avatar_congruence_closure -sa!=fmb sas!=z3 av=on > acc ~cat off:600,on:58 +sas!=z3 av=on > acc ~cat off:600,on:58 # avatar_minimize_model -sa!=fmb av=on > amm ~cat on:600,off:69 +av=on > amm ~cat on:600,off:69 # avatar_delete_deactivated -sa!=fmb av=on > add ~cat on:300,large:55,off:8 +av=on > add ~cat on:300,large:55,off:8 # avatar_literal_polarity_advice -sa!=fmb av=on > alpa ~cat none:300,false:13,true:6,random:4 +av=on > alpa ~cat none:300,false:13,true:6,random:4 # avatar_nonsplittable_components -sa!=fmb av=on > anc ~cat known:300,all_dependent:38,all:45,none:48 +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: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 +# 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 # nonliterals_in_clause_weight -sa!=fmb av=on > nicw ~cat off:600,on:76 +av=on > nicw ~cat off:600,on:76 # split_at_activation -sa!=fmb av=on > sac ~cat off:3,on:1 +av=on > sac ~cat off:3,on:1 # Michael's clause cleaving TODO # intent=sat av=on > cm ~cat on:1 @@ -338,67 +336,30 @@ sa!=fmb av=on > sac ~cat off:3,on:1 # BACK TO INFERENCES # unit_resulting_resolution -sa!=fmb av=on > urr ~cat off:1200,ec_only:162,on:300,full:40 -sa!=fmb av=off > urr ~cat off:1200,ec_only:162,on:340 +av=on > urr ~cat off:1200,ec_only:162,on:300,full:40 +av=off > urr ~cat off:1200,ec_only:162,on:340 # binary_resolution -intent=unsat sa!=fmb > br ~cat on:8,off:1 -intent=sat sa!=fmb urr=on > br ~cat on:10,off:1 +intent=unsat > br ~cat on:8,off:1 +intent=sat urr=on > br ~cat on:10,off:1 # AVATAR SPLIT QUEUE # avatar_split_queue -sa!=fmb av=on > avsq ~cat off:5,on:1 +av=on > avsq ~cat off:5,on:1 # avatar_split_queue_layered_arrangement -sa!=fmb avsq=on > avsql ~cat off:4,on:1 +avsq=on > avsql ~cat off:4,on:1 # avatar_split_queue_cutoffs -sa!=fmb avsq=on > avsqc ~cat 0:80,1:30,2:20,3:20,4:10,5:5 +avsq=on > avsqc ~cat 0:80,1:30,2:20,3:20,4:10,5:5 # avatar_split_queue_ratios -sa!=fmb avsq=on > avsqr ~u2r -5;3;, +avsq=on > avsqr ~u2r -5;3;, # GLOBAL SUBSUMPTION # global_subsumption -sa!=fmb > gs ~cat off:5,on:1 - -# FMB options - -# TODO: a candidate for hardwiring "on" (go an collect the data) -# fmb_use_simplifying_solver -sa=fmb sas=minisat > fmbuss ~cat off:1,on:5 - -# fmb_enumeration_strategy (TODO: in the multi-sorted setting, sbeam makes only sense with intent=sat) -$has_z3=true sa=fmb > fmbes ~cat sbeam:1,smt:1,contour:1 -$has_z3!=true sa=fmb > fmbes ~cat sbeam:1,contour:1 - -# fmb_size_weight_ratio -fmbes=contour > fmbswr ~ui 0,5 - -# fmb_adjust_sorts -sa=fmb fmbes!=contour > fmbas ~cat group:36,predicate:4,expand:4,off:1,function:1 -sa=fmb fmbes=contour > fmbas ~cat group:36,predicate:4,off:1,function:1 - -# fmb_detect_sort_bounds -sa=fmb fmbas!=predicate fmbas!=function > fmbdsb ~cat off:5,on:1 - -# fmb_detect_sort_bounds_time_limit -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 model incomplete" (but could save time for some problems) -intent=sat sa=fmb > $fmbss ~cat 1:5,666:1 -intent=sat sa=fmb $fmbss=1 > fmbss ~cat 1:1 -intent=sat sa=fmb $fmbss=666 > fmbss ~sgd 0.1,1 - -# fmb_symmetry_symbol_order -sa=fmb > fmbsso ~cat occurrence:22,input_usage:1,preprocessed_usage:1 - -# fmb_symmetry_ratio -sa=fmb > fmbsr ~uf 1.0,2.5 +> gs ~cat off:5,on:1 # HIGHER ORDER STUFF @@ -471,7 +432,7 @@ func_ext!=axiom > pe ~cat off:20,on:1 > inj ~cat off:4,on:1 # higher order split queue -sa!=fmb > hsq ~cat off:10,on:1 +> hsq ~cat off:10,on:1 hsq=on > hsql ~cat off:1,on:4 hsq=on > hsqc ~cat 0:80,1:30,2:20,3:20,4:10,5:5 hsq=on > hsqr ~u2r -5;3;, From 53217d2cb79b7bc195f81be2d740320d5fe12d42 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Mon, 8 Jun 2026 16:45:31 +0200 Subject: [PATCH 3/7] Add assertion to ensure all shared terms are appified; fix definition introduction --- Indexing/TermSharing.cpp | 2 ++ Inferences/DefinitionIntroduction.cpp | 46 +++++++++++++++++++-------- Kernel/HOL/HOL.hpp | 2 +- Kernel/RobSubstitution.cpp | 2 +- Kernel/Term.hpp | 2 +- 5 files changed, 38 insertions(+), 16 deletions(-) diff --git a/Indexing/TermSharing.cpp b/Indexing/TermSharing.cpp index e79a068ff..3aa0f7b02 100644 --- a/Indexing/TermSharing.cpp +++ b/Indexing/TermSharing.cpp @@ -133,6 +133,8 @@ void TermSharing::computeAndSetSharedTermData(Term* t) t->setHasLambda(hasLambda); t->setInterpretedConstantsPresence(hasInterpretedConstants); + ASS_REP(!env.higherOrder() || t->isApplication() || t->isLambdaTerm() || !t->numTermArguments(), "HO term " + t->toString() + " is not appified"); + //poly function works for mono as well, but is slow //it is fine to use for debug ASS_REP(_wellSortednessCheckingDisabled || SortHelper::areImmediateSortsValidPoly(t), t->toString()); diff --git a/Inferences/DefinitionIntroduction.cpp b/Inferences/DefinitionIntroduction.cpp index 34e6fa851..9cff2d008 100644 --- a/Inferences/DefinitionIntroduction.cpp +++ b/Inferences/DefinitionIntroduction.cpp @@ -14,6 +14,7 @@ #include "DefinitionIntroduction.hpp" #include "Kernel/Clause.hpp" +#include "Kernel/HOL/HOL.hpp" #include "Kernel/TermIterators.hpp" #include "Kernel/InferenceStore.hpp" #include "Lib/Metaiterators.hpp" @@ -111,9 +112,10 @@ void DefinitionIntroduction::introduceDefinitionFor(Term *t) { SortHelper::collectVariableSorts(t, domain_sorts); // reformat data - std::vector domain_sort_vector; + TermStack domain_sort_vector; std::vector variables; - unsigned term_arity = 0, sort_arity = 0; + TermStack term_variables; + unsigned term_arity = 0, type_arity = 0; // OperatorType expects a canonically-renamed type Renaming sort_rename; @@ -121,7 +123,7 @@ void DefinitionIntroduction::introduceDefinitionFor(Term *t) { // first, sort variables for(auto [x, sort] : iterTraits(domain_sorts.items())) if(sort == AtomicSort::superSort()) { - sort_arity++; + type_arity++; variables.emplace_back(x, false); sort_rename.getOrBind(x); } @@ -129,20 +131,38 @@ void DefinitionIntroduction::introduceDefinitionFor(Term *t) { for(auto [x, sort] : iterTraits(domain_sorts.items())) if(sort != AtomicSort::superSort()) { term_arity++; - variables.emplace_back(x, false); - domain_sort_vector.push_back(sort_rename.apply(sort)); + if constexpr (higherOrder) { + term_variables.emplace(x, false); + } else { + variables.emplace_back(x, false); + } + domain_sort_vector.push(sort_rename.apply(sort)); } // create the equation - unsigned functor = env.signature->addFreshFunction(term_arity + sort_arity, "sF"); - OperatorType *type = OperatorType::getFunctionType( - term_arity, - domain_sort_vector.data(), - sort_rename.apply(range_sort), - sort_arity - ); + unsigned functor; + OperatorType* type; + if constexpr (higherOrder) { + functor = env.signature->addFreshFunction(type_arity, "sF"); + auto sort = AtomicSort::arrowSort(domain_sort_vector, sort_rename.apply(range_sort), /*fromTop=*/true); + type = OperatorType::getConstantsType(sort, type_arity); + } else { + functor = env.signature->addFreshFunction(type_arity + term_arity, "sF"); + type = OperatorType::getFunctionType( + term_arity, + domain_sort_vector.begin(), + sort_rename.apply(range_sort), + type_arity + ); + } env.signature->getFunction(functor)->setType(type); - Term *def = Term::create(functor, sort_arity + term_arity, variables.data()); + Term *def; + if constexpr (higherOrder) { + TermList head(Term::create(functor, type_arity, variables.data())); + def = HOL::create::app(head, term_variables, /*fromTop=*/false).term(); + } else { + def = Term::create(functor, type_arity + term_arity, variables.data()); + } Literal *eq = Literal::createEquality(true, TermList(def), TermList(t), range_sort); // record definition diff --git a/Kernel/HOL/HOL.hpp b/Kernel/HOL/HOL.hpp index 9dd06fc62..008ee7241 100644 --- a/Kernel/HOL/HOL.hpp +++ b/Kernel/HOL/HOL.hpp @@ -95,7 +95,7 @@ namespace HOL::create { TermList app(TermList s1, TermList s2, TermList arg1, TermList arg2, bool shared = true); // With head h and a stack or arguments (a1,...an) from bottom to top, we get h @ an @ ... @ a1 // with fromTop = true, while h @ a1 @ ... @ an with fromTop = false. - // TODO I think due to the default fromTop==true, some call sites might be wrong, double check + // TODO(HOL): I think due to the default fromTop==true, some call sites might be wrong, double check TermList app(TermList sort, TermList head, const TermStack& terms, bool fromTop = true); TermList app(TermList head, const TermStack& terms, bool fromTop = true); diff --git a/Kernel/RobSubstitution.cpp b/Kernel/RobSubstitution.cpp index 8286b04aa..96192ef24 100644 --- a/Kernel/RobSubstitution.cpp +++ b/Kernel/RobSubstitution.cpp @@ -350,7 +350,7 @@ bool RobSubstitution::unify(TermSpec s, TermSpec t) localBD.drop(); } - DEBUG_UNIFY(0, *this) + DEBUG_UNIFY(0, *this, " (", mismatch ? "fail" : "success", ")"); return !mismatch; } diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp index 1b78670e0..a12138fdd 100644 --- a/Kernel/Term.hpp +++ b/Kernel/Term.hpp @@ -1051,7 +1051,7 @@ class AtomicSort // With a stack (s1,...sn) from bottom to top, we get s1 -> (... -> sn) with fromTop = true, // while sn -> (... -> s1) with fromTop = false. - // TODO check also this, some call sites might be wrong + // TODO(HOL): check also this, some call sites might be wrong static TermList arrowSort(const TermStack& domSorts, TermList range, bool fromTop = false); static TermList arrowSort(TermList s1, TermList s2); static TermList arrowSort(unsigned size, const TermList* types, TermList range); From 3ebc2c2200d9dfbb398f6982b7e22da3bf662cb7 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Mon, 8 Jun 2026 21:36:36 +0200 Subject: [PATCH 4/7] Attempt to fix backward matching (instantiations) in an inefficient way for HOL --- Indexing/CodeTreeInterfaces.cpp | 16 ------ Indexing/CodeTreeInterfaces.hpp | 2 - Indexing/LiteralIndex.cpp | 3 +- Indexing/LiteralIndex.hpp | 39 +++++++------ Indexing/LiteralIndexingStructure.hpp | 57 ------------------- Indexing/LiteralSubstitutionTree.hpp | 31 ++++------ Indexing/SubstitutionTree.hpp | 8 --- Indexing/TermIndex.hpp | 18 +++++- Indexing/TermIndexingStructure.hpp | 2 - Indexing/TermSubstitutionTree.hpp | 3 - Inferences/BackwardDemodulation.cpp | 3 +- .../BackwardSubsumptionAndResolution.cpp | 17 ++++-- .../BackwardSubsumptionAndResolution.hpp | 1 + .../BackwardSubsumptionDemodulation.cpp | 2 +- Saturation/SaturationAlgorithm.cpp | 19 ++++--- ...ences_CodeTreeSubsumptionAndResolution.cpp | 5 +- .../tInferences_SubsumptionAndResolution.cpp | 5 +- cmake/sources.cmake | 1 - 18 files changed, 83 insertions(+), 149 deletions(-) delete mode 100644 Indexing/LiteralIndexingStructure.hpp diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index 0e973033f..e004379c1 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -163,22 +163,6 @@ VirtualIterator> CodeTreeTIS -bool CodeTreeTIS::generalizationExists(TermList t) -{ - if(_ct.isEmpty()) { - return false; - } - - static typename TermCodeTree::TermMatcher tm; - - tm.init(&_ct, t); - bool res=tm.next(); - tm.reset(); - - return res; -} - template class CodeTreeTIS; template class CodeTreeTIS; template class CodeTreeTIS; diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index db5b25fd0..cc505d492 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -50,8 +50,6 @@ class CodeTreeTIS : public TermIndexingStructure } VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) final ; - // TODO use TypedTermList here too - bool generalizationExists(TermList t) final ; // TODO: get rid of NOT_IMPLEMENTED VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration) override { NOT_IMPLEMENTED; } diff --git a/Indexing/LiteralIndex.cpp b/Indexing/LiteralIndex.cpp index d9404d5c2..39e53c081 100644 --- a/Indexing/LiteralIndex.cpp +++ b/Indexing/LiteralIndex.cpp @@ -21,7 +21,6 @@ #include "Kernel/MLVariant.hpp" #include "Kernel/Ordering.hpp" -#include "LiteralIndexingStructure.hpp" #include "LiteralSubstitutionTree.hpp" #include "Saturation/SaturationAlgorithm.hpp" @@ -332,7 +331,7 @@ void UnitIntegerComparisonLiteralIndex::handleClause(Clause* c, bool adding) Literal* lit = (*c)[0]; ASS(lit != nullptr); - _is->handle(LiteralClause{ lit, c }, adding); + _is.handle(LiteralClause{ lit, c }, adding); } } diff --git a/Indexing/LiteralIndex.hpp b/Indexing/LiteralIndex.hpp index edd53d770..6993635c3 100644 --- a/Indexing/LiteralIndex.hpp +++ b/Indexing/LiteralIndex.hpp @@ -21,7 +21,6 @@ #include "Lib/DHMap.hpp" #include "Index.hpp" -#include "LiteralIndexingStructure.hpp" namespace Indexing { @@ -30,34 +29,40 @@ class LiteralIndex : public Index { public: - VirtualIterator getAll() - { return _is->getAll(); } - VirtualIterator> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions = true) - { return _is->getUnifications(lit, complementary, retrieveSubstitutions); } + { return _is.getUnifications(lit, complementary, retrieveSubstitutions); } VirtualIterator> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) - { return _is->getUwa(lit, complementary, uwa, fixedPointIteration); } + { return _is.getUwa(lit, complementary, uwa, fixedPointIteration); } VirtualIterator> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions = true) - { return _is->getGeneralizations(lit, complementary, retrieveSubstitutions); } + { return _is.getGeneralizations(lit, complementary, retrieveSubstitutions); } + template VirtualIterator> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions = true) - { return _is->getInstances(lit, complementary, retrieveSubstitutions); } - - size_t getUnificationCount(Literal* lit, bool complementary) - { return _is->getUnificationCount(lit, complementary); } + { + if constexpr (higherOrder) { + // TODO(HOL): implement proper higher-order matching here + // we override retrieveSubstitutions because we need the substitution for the aftercheck + return pvi(iterTraits(_is.getInstances(lit, complementary, /*retrieveSubstitutions=*/true)) + .filter([lit](auto qr) { + return iterTraits(VariableIterator(lit)).all([&qr](TermList var) { + return !qr.unifier->applyToBoundQuery(var).containsLooseDBIndex(); + }); + })); + } else { + return _is.getInstances(lit, complementary, retrieveSubstitutions); + } + } - friend std::ostream& operator<<(std::ostream& out, LiteralIndex const& self) { return out << *self._is; } - friend std::ostream& operator<<(std::ostream& out, Output::Multilineconst& self) { return out << Output::multiline(*self.self._is, self.indent); } + friend std::ostream& operator<<(std::ostream& out, LiteralIndex const& self) { return out << self._is; } + friend std::ostream& operator<<(std::ostream& out, Output::Multilineconst& self) { return out << Output::multiline(self.self._is, self.indent); } protected: - LiteralIndex() : _is(new LiteralSubstitutionTree()) {} - void handle(Data data, bool add) - { _is->handle(std::move(data), add); } + { _is.handle(std::move(data), add); } - std::unique_ptr> _is; + LiteralSubstitutionTree _is; }; class BinaryResolutionIndex diff --git a/Indexing/LiteralIndexingStructure.hpp b/Indexing/LiteralIndexingStructure.hpp deleted file mode 100644 index b64e6480f..000000000 --- a/Indexing/LiteralIndexingStructure.hpp +++ /dev/null @@ -1,57 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file LiteralIndexingStructure.hpp - * Defines class LiteralIndexingStructure. - */ - - -#ifndef __LiteralIndexingStructure__ -#define __LiteralIndexingStructure__ - -#include "Forwards.hpp" -#include "Index.hpp" -#include "Kernel/UnificationWithAbstraction.hpp" -#include "Lib/VirtualIterator.hpp" -#include "Shell/Options.hpp" - -namespace Indexing { - -template -class LiteralIndexingStructure { -public: - using LeafData = LeafData_; - virtual ~LiteralIndexingStructure() {} - - virtual void handle(LeafData ld, bool insert) = 0; - void insert(LeafData ld) { handle(std::move(ld), /* insert = */ true ); } - void remove(LeafData ld) { handle(std::move(ld), /* insert = */ false); } - - virtual VirtualIterator getAll() { NOT_IMPLEMENTED; } - virtual VirtualIterator> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual VirtualIterator> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) = 0; - virtual VirtualIterator> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual VirtualIterator> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual VirtualIterator> getVariants(Literal* lit, bool complementary, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - - virtual size_t getUnificationCount(Literal* lit, bool complementary) - { - return countIteratorElements(getUnifications(lit, complementary, false)); - } - - virtual void output(std::ostream& out, Option multilineIndent) const = 0; - - friend std::ostream& operator<<(std::ostream& out, LiteralIndexingStructure const& self) { self.output(out, {} ); return out; } - friend std::ostream& operator<<(std::ostream& out, Output::Multilineconst& self) { self.self.output(out, some(self.indent)); return out; } -}; - -}; - -#endif /* __LiteralIndexingStructure__ */ diff --git a/Indexing/LiteralSubstitutionTree.hpp b/Indexing/LiteralSubstitutionTree.hpp index bad4a8dd5..5406a8ebe 100644 --- a/Indexing/LiteralSubstitutionTree.hpp +++ b/Indexing/LiteralSubstitutionTree.hpp @@ -21,16 +21,14 @@ #include "Kernel/UnificationWithAbstraction.hpp" #include "Lib/Metaiterators.hpp" #include "Lib/VirtualIterator.hpp" -#include "LiteralIndexingStructure.hpp" #include "SubstitutionTree.hpp" #include "Kernel/Signature.hpp" namespace Indexing { -/** A wrapper class around SubstitutionTree that makes it usable as a LiteralIndexingStructure */ +/** A wrapper class around SubstitutionTree that makes it usable a literal index */ template class LiteralSubstitutionTree -: public LiteralIndexingStructure { using SubstitutionTree = Indexing::SubstitutionTree; using LeafData = LeafData_; @@ -47,30 +45,22 @@ class LiteralSubstitutionTree : _trees(env.signature->predicates() * 2) { } - void handle(LeafData ld, bool insert) final + void handle(LeafData ld, bool insert) { getTree(ld.key(), /* complementary */ false).handle(std::move(ld), insert); } - VirtualIterator getAll() final - { - return pvi( - iterTraits(getRangeIterator((unsigned long)0, _trees.size())) - .flatMap([this](auto i) { return LeafIterator(_trees[i].get()); }) - .flatMap([](Leaf* l) { return l->allChildren(); }) - // TODO get rid of copying data here - .map([](LeafData const* ld) { return *ld; }) - ); - } + void insert(LeafData ld) { handle(std::move(ld), /* insert = */ true ); } + void remove(LeafData ld) { handle(std::move(ld), /* insert = */ false); } - VirtualIterator> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions) final + VirtualIterator> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions) { return pvi(getResultIterator>>(lit, complementary, retrieveSubstitutions)); } - VirtualIterator> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions) final + VirtualIterator> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions) { return pvi(getResultIterator(lit, complementary, retrieveSubstitutions)); } - VirtualIterator> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions) final + VirtualIterator> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions) { return pvi(getResultIterator(lit, complementary, retrieveSubstitutions)); } - VirtualIterator> getVariants(Literal* query, bool complementary, bool retrieveSubstitutions) final + VirtualIterator> getVariants(Literal* query, bool complementary, bool retrieveSubstitutions) { return pvi(iterTraits(getTree(query, complementary).getVariants(query, retrieveSubstitutions))); } @@ -104,7 +94,7 @@ class LiteralSubstitutionTree public: - VirtualIterator> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) final + VirtualIterator> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) { auto unif = Lib::make_shared(AbstractingUnifier::empty(AbstractionOracle(uwa))); return pvi(getResultIterator>>(lit, complementary, /* retrieveSubstitutions */ true, unif.get(), AbstractionOracle(uwa), fixedPointIteration) @@ -143,7 +133,7 @@ class LiteralSubstitutionTree return out << "} "; } - void output(std::ostream& out, Option multilineIndent) const override { + void output(std::ostream& out, Option multilineIndent) const { if (multilineIndent) { out << Output::multiline(*this, *multilineIndent); } else { @@ -151,7 +141,6 @@ class LiteralSubstitutionTree } } - private: SubstitutionTree& getTree(Literal* lit, bool complementary) { diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp index 97cba8424..50765b6c4 100644 --- a/Indexing/SubstitutionTree.hpp +++ b/Indexing/SubstitutionTree.hpp @@ -620,14 +620,6 @@ class SubstitutionTree final { out << "{ _query: " << _query << ", _result: " << _result << " }"; } }; - template - bool generalizationExists(Query query) - { - return _root == nullptr - ? false - : FastGeneralizationsIterator(this, _root, query, /* retrieveSubstitutions */ false, /* reversed */ false).hasNext(); - } - template VirtualIterator> getVariants(Query query, bool retrieveSubstitutions) { diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp index 95a0ad57e..f53a2ae40 100644 --- a/Indexing/TermIndex.hpp +++ b/Indexing/TermIndex.hpp @@ -26,8 +26,6 @@ class TermIndex : public Index { public: - ~TermIndex() override {} - VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) { return _is->getUwa(t, uwa, fixedPointIteration); } @@ -37,8 +35,22 @@ class TermIndex VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) { return _is->getGeneralizations(t, retrieveSubstitutions); } + template VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions = true) - { return _is->getInstances(t, retrieveSubstitutions); } + { + if constexpr (higherOrder) { + // TODO(HOL): implement proper higher-order matching here + // we override retrieveSubstitutions because we need the substitution for the aftercheck + return pvi(iterTraits(_is->getInstances(t, /*retrieveSubstitutions=*/true)) + .filter([t](auto qr) { + return iterTraits(VariableIterator(t)).all([&qr](TermList var) { + return !qr.unifier->applyToBoundQuery(var).containsLooseDBIndex(); + }); + })); + } else { + return _is->getInstances(t, retrieveSubstitutions); + } + } friend std::ostream& operator<<(std::ostream& out, TermIndex const& self) { return out << *self._is; } diff --git a/Indexing/TermIndexingStructure.hpp b/Indexing/TermIndexingStructure.hpp index e43d3a460..3181fc080 100644 --- a/Indexing/TermIndexingStructure.hpp +++ b/Indexing/TermIndexingStructure.hpp @@ -35,8 +35,6 @@ class TermIndexingStructure { virtual VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } virtual VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual bool generalizationExists(TermList t) { NOT_IMPLEMENTED; } - virtual void output(std::ostream& output) const = 0; friend std::ostream& operator<<(std::ostream& out, TermIndexingStructure const& self) diff --git a/Indexing/TermSubstitutionTree.hpp b/Indexing/TermSubstitutionTree.hpp index d3a97ea14..9ff404f14 100644 --- a/Indexing/TermSubstitutionTree.hpp +++ b/Indexing/TermSubstitutionTree.hpp @@ -67,9 +67,6 @@ class TermSubstitutionTree { return iterTraits(_inner.template iterator(query, retrieveSubstitutions, /* reversed */ false, std::move(args)...)) ; } - bool generalizationExists(TermList t) override - { return t.isVar() ? false : _inner.generalizationExists(TypedTermList(t.term())); } - void output(std::ostream& out) const final { out << *this; } friend std::ostream& operator<<(std::ostream& out, TermSubstitutionTree const& self) diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index 0f326bd2d..3d24ddbf3 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -178,7 +178,8 @@ void BackwardDemodulation::perform(Clause* cl, getMappingIterator( getMapAndFlattenIterator( EqHelper::getDemodulationLHSIterator(lit, _preordered, _ord).first, - [this](TypedTermList lhs){ return pvi( pushPairIntoRightIterator(lhs, _index->getInstances(lhs, true)) ); }), + [this](TypedTermList lhs) + { return pvi( pushPairIntoRightIterator(lhs, _index->template getInstances(lhs, true)) ); }), ResultFn(cl, *this, _helper)), [](BwSimplificationRecord arg){ return arg.toRemove!=0; })); diff --git a/Inferences/BackwardSubsumptionAndResolution.cpp b/Inferences/BackwardSubsumptionAndResolution.cpp index f43d443d4..a7177e5d6 100644 --- a/Inferences/BackwardSubsumptionAndResolution.cpp +++ b/Inferences/BackwardSubsumptionAndResolution.cpp @@ -38,7 +38,8 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; -BackwardSubsumptionAndResolution::BackwardSubsumptionAndResolution(SaturationAlgorithm& salg) +template +BackwardSubsumptionAndResolution::BackwardSubsumptionAndResolution(SaturationAlgorithm& salg) : _subsumption(salg.getOptions().backwardSubsumption() != Options::Subsumption::OFF), _subsumptionResolution(salg.getOptions().backwardSubsumptionResolution() != Options::Subsumption::OFF), _subsumptionByUnitsOnly(salg.getOptions().backwardSubsumption() == Options::Subsumption::UNIT_ONLY), @@ -48,7 +49,8 @@ BackwardSubsumptionAndResolution::BackwardSubsumptionAndResolution(SaturationAlg ASS(_subsumption || _subsumptionResolution); } -void BackwardSubsumptionAndResolution::perform(Clause *cl, +template +void BackwardSubsumptionAndResolution::perform(Clause *cl, BwSimplificationRecordIterator &simplifications) { ASSERT_VALID(*cl) @@ -76,7 +78,7 @@ void BackwardSubsumptionAndResolution::perform(Clause *cl, /***************************************************/ /* SUBSUMPTION UNIT CLAUSE */ /***************************************************/ - auto it = _bwIndex->getInstances(lit, false, false); + auto it = _bwIndex->getInstances(lit, false, false); while (it.hasNext()) { Clause *icl = it.next().data->clause; if (!_checked.insert(icl->number())) @@ -89,7 +91,7 @@ void BackwardSubsumptionAndResolution::perform(Clause *cl, /***************************************************/ /* SUBSUMPTION RESOLUTION UNIT CLAUSE */ /***************************************************/ - auto it = _bwIndex->getInstances(lit, true, false); + auto it = _bwIndex->getInstances(lit, true, false); while (it.hasNext()) { auto res = it.next(); Clause *icl = res.data->clause; @@ -135,7 +137,7 @@ void BackwardSubsumptionAndResolution::perform(Clause *cl, if (!_subsumptionByUnitsOnly) { // find the positively matched literals - auto it = _bwIndex->getInstances(lit, false, false); + auto it = _bwIndex->getInstances(lit, false, false); while (it.hasNext()) { Clause *icl = it.next().data->clause; if (!_checked.insert(icl->number())) @@ -167,7 +169,7 @@ void BackwardSubsumptionAndResolution::perform(Clause *cl, // find the negatively matched literals // We can use the same least matchable literal as before since our method is agnostic to the // flipped literal - auto it = _bwIndex->getInstances(lit, true, false); + auto it = _bwIndex->getInstances(lit, true, false); while (it.hasNext()) { Clause *icl = it.next().data->clause; if (!_checked.insert(icl->number())) @@ -185,4 +187,7 @@ void BackwardSubsumptionAndResolution::perform(Clause *cl, } } +template class BackwardSubsumptionAndResolution; +template class BackwardSubsumptionAndResolution; + } // namespace Inferences diff --git a/Inferences/BackwardSubsumptionAndResolution.hpp b/Inferences/BackwardSubsumptionAndResolution.hpp index 3aa8f1ac1..2057eb48b 100644 --- a/Inferences/BackwardSubsumptionAndResolution.hpp +++ b/Inferences/BackwardSubsumptionAndResolution.hpp @@ -22,6 +22,7 @@ namespace Inferences { +template class BackwardSubsumptionAndResolution : public BackwardSimplificationEngine { diff --git a/Inferences/BackwardSubsumptionDemodulation.cpp b/Inferences/BackwardSubsumptionDemodulation.cpp index 041c0872e..c4c2d2ede 100644 --- a/Inferences/BackwardSubsumptionDemodulation.cpp +++ b/Inferences/BackwardSubsumptionDemodulation.cpp @@ -141,7 +141,7 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* s bool mustPredActive = false; unsigned mustPred; - auto rit = _index->getInstances(candidateQueryLit, false, false); + auto rit = _index->getInstances(candidateQueryLit, false, false); while (rit.hasNext()) { auto qr = rit.next(); Clause* candidate = qr.data->clause; diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 7b8856358..c77e7d85f 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1657,14 +1657,15 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const } if (opt.forwardSubsumption()) { - if (opt.codeTreeSubsumption()) { - if (prb.isHigherOrder()) { - res->addForwardSimplifierToFront>(); - } else { + if (prb.isHigherOrder()) { + // Only use the code trees for HOL, as the other is not yet adapted + res->addForwardSimplifierToFront>(); + } else { + if (opt.codeTreeSubsumption()) { res->addForwardSimplifierToFront>(); + } else { + res->addForwardSimplifierToFront(); } - } else { - res->addForwardSimplifierToFront(); } } else if (opt.forwardSubsumptionResolution()) { @@ -1702,7 +1703,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const bool backSubsumption = opt.backwardSubsumption() != Options::Subsumption::OFF; bool backSR = opt.backwardSubsumptionResolution() != Options::Subsumption::OFF; if (backSubsumption || backSR) { - res->addBackwardSimplifierToFront(); + if (prb.isHigherOrder()) { + res->addBackwardSimplifierToFront>(); + } else { + res->addBackwardSimplifierToFront>(); + } } if (opt.mode() == Options::Mode::CONSEQUENCE_ELIMINATION) { diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp index 34b0c605b..d526e67db 100644 --- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp @@ -61,7 +61,10 @@ using namespace Test; namespace { inline auto tester() { - return FwdBwdSimplification::TestCase, BackwardSubsumptionAndResolution>() + return FwdBwdSimplification::TestCase< + CodeTreeForwardSubsumptionAndResolution, + BackwardSubsumptionAndResolution + >() .options({ { "backward_subsumption", "on" }, { "backward_subsumption_resolution", "on" } diff --git a/UnitTests/tInferences_SubsumptionAndResolution.cpp b/UnitTests/tInferences_SubsumptionAndResolution.cpp index d026af747..f77e028f5 100644 --- a/UnitTests/tInferences_SubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_SubsumptionAndResolution.cpp @@ -61,7 +61,10 @@ using namespace Test; namespace { inline auto tester() { - return FwdBwdSimplification::TestCase() + return FwdBwdSimplification::TestCase< + ForwardSubsumptionAndResolution, + BackwardSubsumptionAndResolution + >() .options({ { "backward_subsumption", "on" }, { "backward_subsumption_resolution", "on" } diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 15ccdc0f5..48d544918 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -183,7 +183,6 @@ set(SOURCES Indexing/InductionFormulaIndex.hpp Indexing/LiteralIndex.cpp Indexing/LiteralIndex.hpp - Indexing/LiteralIndexingStructure.hpp Indexing/LiteralMiniIndex.cpp Indexing/LiteralMiniIndex.hpp Indexing/LiteralSubstitutionTree.hpp From 4051eb5387dfa7dca86c48d1099bc1a8642e8566 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Tue, 9 Jun 2026 07:52:36 +0200 Subject: [PATCH 5/7] Use HO code trees in partial redundancy handler to avoid errors --- Shell/PartialRedundancyHandler.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 6947a3044..772539e36 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -245,7 +245,8 @@ class PartialRedundancyHandler::ConstraintIndex } struct SubstMatcher - : public Matcher + // TODO(HOL): consider turning higherOrder flag off for HOL + : public Matcher { void init(CodeTree* tree, const TermStack& ts) { From 6156ba4afcb0f1f75dd3ecc8f5bf213d21c80cc0 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Tue, 9 Jun 2026 17:08:13 +0200 Subject: [PATCH 6/7] Remove undescriptive comment --- Kernel/Formula.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/Kernel/Formula.cpp b/Kernel/Formula.cpp index e5a4b81fc..e1ff4dc75 100644 --- a/Kernel/Formula.cpp +++ b/Kernel/Formula.cpp @@ -451,7 +451,6 @@ Formula* Formula::quantify(Formula* f) return f; } -/** removes the leading universal quantifiers from a formula */ Formula* Formula::removeUniversalTypePrenex(Formula* f) { while (f->connective() == FORALL) { From af1db3e04c74cef326061d7446097badf9ac1f3a Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 11 Jun 2026 13:48:46 +0200 Subject: [PATCH 7/7] Add comment about different arg-containing variables --- Inferences/DefinitionIntroduction.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Inferences/DefinitionIntroduction.cpp b/Inferences/DefinitionIntroduction.cpp index 9cff2d008..eaaddbd92 100644 --- a/Inferences/DefinitionIntroduction.cpp +++ b/Inferences/DefinitionIntroduction.cpp @@ -113,8 +113,8 @@ void DefinitionIntroduction::introduceDefinitionFor(Term *t) { // reformat data TermStack domain_sort_vector; - std::vector variables; - TermStack term_variables; + std::vector variables; // contains type vars when in HOL, otherwise all vars + TermStack term_variables; // contains term vars when in HOL, needed by HOL::create::app unsigned term_arity = 0, type_arity = 0; // OperatorType expects a canonically-renamed type