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.

Sign up for GitHub

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

Gleiss rapid final #223

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

Gleiss rapid final #223

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
3ccec0b
Recognize term algebra of natural numbers
JakobR May 1, 2019
f6e7295
add convenience functions for building nat-terms and nat-predicates
gleiss Dec 3, 2019
a9f1ff7
implement axiomatization for Nat
gleiss Dec 3, 2019
46f6cc7
fine-tune time-theory-axioms
gleiss Jan 14, 2020
adc3a0c
fix -tha some option value for Nat
gleiss Feb 26, 2020
ce3efce
hack: add additional integer-axiom: x!=x+1
gleiss Feb 26, 2020
f14ba67
hack: implement deletion-rule for clauses containing terms s(s(...)) …
gleiss Feb 27, 2020
a7a8723
add flag to symbols to mark lemma-predicates
gleiss Feb 21, 2020
1683905
extend smtlib2-parser to support marking of lemma-predicates
gleiss Feb 21, 2020
55fdfbf
implement ensureNonLemmaPredicateSelected()
gleiss Feb 21, 2020
8f41d9f
enforce selection of negative lemma-literals
gleiss Feb 21, 2020
e708d16
introduce option for lemma literal selection
gleiss Feb 21, 2020
6e142ae
Merge branch 'nat-theory' into rapid-final
gleiss Jul 17, 2020
0f2ac55
improve options used for trace logic domain
gleiss Jul 21, 2020
69f2210
Rapid Portfolio Mode
mina1604 Apr 14, 2021
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
3 changes: 3 additions & 0 deletions CASC/PortfolioMode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -394,6 +394,9 @@ void PortfolioMode::getSchedules(Property& prop, Schedule& quick, Schedule& fall
case Options::Schedule::LTB_DEFAULT_2017:
Schedules::getLtb2017DefaultSchedule(prop,quick);
break;
case Options::Schedule::RAPID:
Schedules::getRapidSchedule(prop,quick);
break;
default:
INVALID_OPERATION("Unknown schedule");
}
Expand Down
66 changes: 66 additions & 0 deletions CASC/Schedules.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14755,3 +14755,69 @@ void Schedules::getLtb2017DefaultSchedule(const Property& property, Schedule& sc
sched.push("lrs+11_3:1_bsr=unit_only:br=off:cond=on:ep=RST:fsr=off:gs=on:gsaa=from_current:gsem=off:nwc=3:stl=300:sd=2:ss=axioms:st=2.0:sac=on:add=large:afr=on:afp=100000:afq=1.4:amm=sco:anc=none:sp=reverse_arity:urr=on_60"); // MZR 30 (3)
sched.push("lrs+1003_4_bsr=unit_only:cond=fast:fsr=off:gsp=input_only:gs=on:gsaa=from_current:nm=0:nwc=1:stl=300:sos=on:sac=on:add=large:afp=10000:afq=1.1:anc=none:urr=ec_only:uhcvi=on_60"); // HLL 50 (1)
}

void Schedules::getRapidSchedule(const Shell::Property& property, Schedule& sched) {
property.getSMTLIBLogic();
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=off_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=off_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_10");


sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=off_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=off_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_300");
}
2 changes: 2 additions & 0 deletions CASC/Schedules.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,8 @@ class Schedules
static void getLtb2014Schedule(const Shell::Property& property, Schedule& sched);
static void getLtb2014MzrSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
static void getLtb2017DefaultSchedule(const Shell::Property& property, Schedule& sched);

static void getRapidSchedule(const Shell::Property& property, Schedule& quick);
};


Expand Down
37 changes: 37 additions & 0 deletions Inferences/TermAlgebraReasoning.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
#include "Kernel/SortHelper.hpp"
#include "Kernel/SubstHelper.hpp"
#include "Kernel/Substitution.hpp"
#include "Kernel/TermIterators.hpp"

#include "Lib/Environment.hpp"
#include "Lib/Metaiterators.hpp"
Expand Down Expand Up @@ -575,5 +576,41 @@ namespace Inferences {
auto it3 = getFlattenedIterator(it2);
return pvi(it3);
}

Clause* TwoSuccessorsISE::simplify(Clause* c)
{
CALL("TwoSuccessorsISE::simplify");

auto natTA = env.signature->getNat();
auto zero = natTA->getZeroConstructor()->functor();
auto succ = natTA->getSuccConstructor()->functor();

int length = c->length();
for (int i = 0; i < length; i++)
{
Literal *lit = (*c)[i];
NonVariableIterator nvi(lit);
while (nvi.hasNext()) {
TermList tl = nvi.next();
ASS(tl.isTerm());
auto t1 = tl.term();
if (t1->functor() == succ && t1->nthArgument(0)->isTerm())
{
auto t2 = t1->nthArgument(0)->term();
if (t2->functor() == succ) {
// found an occurence s(s(...)), so remove clause
return 0;
}
else if (t2->functor() == zero) {
// found an occurence s(0), so remove clause
return 0;
}
}
}
}

// no occurences s(s(...)) found, so keep clause
return c;
}

}
13 changes: 13 additions & 0 deletions Inferences/TermAlgebraReasoning.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,20 @@ class AcyclicityGIE1
struct LiteralIterator;
struct SubtermDisequalityIterator;
};

// hack: deletion rule which removes each clause containing at least one term of either the form s(s(...)) or the form s(0).
class TwoSuccessorsISE
: public ImmediateSimplificationEngine
{

public:
CLASS_NAME(TwoSuccessorsISE);
USE_ALLOCATOR(TwoSuccessorsISE);

Kernel::Clause* simplify(Kernel::Clause* c);
};


};

#endif
3 changes: 3 additions & 0 deletions Kernel/BestLiteralSelector.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,8 @@ class BestLiteralSelector
ensureSomeColoredSelected(c, eligible);
ASS_EQ(c->numSelected(), 1); //if there is colored, it should be selected by the QComparator
#endif

ensureNonLemmaPredicateSelected(c, eligible);
}

private:
Expand Down Expand Up @@ -237,6 +239,7 @@ class CompleteBestLiteralSelector
LiteralList::destroy(maximals);

ensureSomeColoredSelected(c, eligible);
ensureNonLemmaPredicateSelected(c, eligible);
}

private:
Expand Down
1 change: 1 addition & 0 deletions Kernel/ELiteralSelector.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,4 +186,5 @@ void ELiteralSelector::doSelection(Clause* c, unsigned eligible)
c->setSelected(selCnt);

ensureSomeColoredSelected(c, eligible);
ensureNonLemmaPredicateSelected(c, eligible);
}
48 changes: 48 additions & 0 deletions Kernel/LiteralSelector.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,6 +207,39 @@ void LiteralSelector::ensureSomeColoredSelected(Clause* c, unsigned eligible)
c->splits()); // .. unless the color comes from the propositional part
}

// hack: make sure that at least one non-lemma-predicate is selected
void LiteralSelector::ensureNonLemmaPredicateSelected(Clause* c, unsigned eligible)
{
CALL("LiteralSelector::ensureNonLemmaPredicateSelected");

if (!env.options->useLemmaPredicateLiteralSelection())
{
return;
}

unsigned selCnt=c->numSelected();

for(unsigned i=0;i<selCnt;i++) {
Signature::Symbol* psym=env.signature->getPredicate(((*c)[i]->functor()));
if(!psym->isLemmaPredicate)
{
// the literal selection already contains a non-lemma-literal
return;
}
}

// we know that no non-lemma-literal is selected, so select some non-lemma-literal if there is one
for(unsigned i=selCnt;i<eligible;i++) {
Signature::Symbol* psym=env.signature->getPredicate(((*c)[i]->functor()));
if(!psym->isLemmaPredicate)
{
swap((*c)[selCnt], (*c)[i]);
c->setSelected(selCnt+1);
return;
}
}
}

/**
* Perform literal selection on clause @b c
*
Expand Down Expand Up @@ -260,6 +293,21 @@ void LiteralSelector::select(Clause* c, unsigned eligibleInp)
}

ASS_G(eligible,1);

// hack: if there is a negative lemma-literal, select this literal (and no other literal).
if (_opt.useLemmaPredicateLiteralSelection())
{
for(unsigned i=0;i<eligible;i++) {
Signature::Symbol* psym=env.signature->getPredicate(((*c)[i]->functor()));
if(psym->isLemmaPredicate && isNegativeForSelection((*c)[i]))
{
swap((*c)[i], (*c)[0]);
c->setSelected(1);
return;
}
}
}

doSelection(c, eligible);
}

Expand Down
1 change: 1 addition & 0 deletions Kernel/LiteralSelector.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ class LiteralSelector
static LiteralSelector* getSelector(const Ordering& ordering, const Options& options, int selectorNumber);

static void ensureSomeColoredSelected(Clause* c, unsigned eligible);
static void ensureNonLemmaPredicateSelected(Clause* c, unsigned eligible);

/**
* Return true if literal @b l is positive for the purpose of
Expand Down
1 change: 1 addition & 0 deletions Kernel/LookaheadLiteralSelector.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -352,6 +352,7 @@ void LookaheadLiteralSelector::doSelection(Clause* c, unsigned eligible)
c->setSelected(selCnt);

ensureSomeColoredSelected(c, eligible);
ensureNonLemmaPredicateSelected(c, eligible);
}

}
1 change: 1 addition & 0 deletions Kernel/MaximalLiteralSelector.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,4 +91,5 @@ void MaximalLiteralSelector::doSelection(Clause* c, unsigned eligible)
c->setSelected(selCnt);

ensureSomeColoredSelected(c, eligible);
ensureNonLemmaPredicateSelected(c, eligible);
}
1 change: 1 addition & 0 deletions Kernel/Signature.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ Signature::Symbol::Symbol(const vstring& nm,unsigned arity, bool interpreted, bo
_protected(0),
_skip(0),
_label(0),
isLemmaPredicate(0),
_equalityProxy(0),
_color(COLOR_TRANSPARENT),
_stringConstant(stringConstant ? 1: 0),
Expand Down
10 changes: 10 additions & 0 deletions Kernel/Signature.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,10 @@ class Signature
/** marks propositional predicate symbols that are labels to
be used as names during consequence finding or function relationship finding */
unsigned _label : 1;
public:
/** marks predicate symbols which are annotated by the user as lemma predicates*/
unsigned isLemmaPredicate : 1;
protected:
/** marks predicates that are equality proxy */
unsigned _equalityProxy : 1;
/** used in coloured proofs and interpolation */
Expand Down Expand Up @@ -514,6 +518,10 @@ class Signature
VirtualIterator<Shell::TermAlgebra*> termAlgebrasIterator() const { return _termAlgebras.range(); }
Shell::TermAlgebraConstructor* getTermAlgebraConstructor(unsigned functor);

/** Returns nullptr if nat is not used */
Shell::NatTermAlgebra* getNat() { return _natTermAlgebra; }
void setNat(Shell::NatTermAlgebra* nta) { ASS(!_natTermAlgebra); _natTermAlgebra = nta; }

void recordDividesNvalue(TermList n){
_dividesNvalues.push(n);
}
Expand Down Expand Up @@ -585,6 +593,8 @@ class Signature
*/
DHMap<unsigned, Shell::TermAlgebra*> _termAlgebras;

Shell::NatTermAlgebra* _natTermAlgebra = nullptr;

void defineOptionTermAlgebra(unsigned optionSort);
void defineEitherTermAlgebra(unsigned eitherSort);
}; // class Signature
Expand Down
1 change: 1 addition & 0 deletions Kernel/SpassLiteralSelector.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,4 +106,5 @@ void SpassLiteralSelector::doSelection(Clause* c, unsigned eligible)
c->setSelected(selCnt);

ensureSomeColoredSelected(c, eligible);
ensureNonLemmaPredicateSelected(c, eligible);
}
Loading