From 3ccec0be0cdaa94e91af21551450c2d21792c2eb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 May 2019 11:11:32 +0200 Subject: [PATCH 01/14] Recognize term algebra of natural numbers --- Kernel/Signature.hpp | 6 ++++++ Parse/SMTLIB2.cpp | 48 +++++++++++++++++++++++++++++++++++++++++++ Parse/SMTLIB2.hpp | 1 + Shell/TermAlgebra.cpp | 21 +++++++++++++++++++ Shell/TermAlgebra.hpp | 30 +++++++++++++++++++++++++++ 5 files changed, 106 insertions(+) diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index eb76bd100e..a899ddcee0 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -514,6 +514,10 @@ class Signature VirtualIterator 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); } @@ -585,6 +589,8 @@ class Signature */ DHMap _termAlgebras; + Shell::NatTermAlgebra* _natTermAlgebra = nullptr; + void defineOptionTermAlgebra(unsigned optionSort); void defineEitherTermAlgebra(unsigned eitherSort); }; // class Signature diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index baf7877d0a..46f08dbaaf 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -180,6 +180,21 @@ void SMTLIB2::readBenchmark(LExprList* bench) continue; } + if (ibRdr.tryAcceptAtom("declare-nat")) + { + vstring nat = ibRdr.readAtom(); + vstring zero = ibRdr.readAtom(); + vstring succ = ibRdr.readAtom(); + vstring pred = ibRdr.readAtom(); + vstring less = ibRdr.readAtom(); + + readDeclareNat(nat, zero, succ, pred, less); + + ibRdr.acceptEOL(); + + continue; + } + if (ibRdr.tryAcceptAtom("declare-codatatypes")) { LExprList* sorts = ibRdr.readList(); LExprList* datatypes = ibRdr.readList(); @@ -996,6 +1011,39 @@ void SMTLIB2::readDeclareDatatypes(LExprList* sorts, LExprList* datatypes, bool } } +void SMTLIB2::readDeclareNat(const vstring& nat, const vstring& zero, const vstring& succ, const vstring& pred, const vstring& less) +{ + _declaredSorts.insert(nat, 0); + bool added; + unsigned natSort = env.sorts->addSort(nat + "()", added, false); // TODO: why false? shouldn't it be interpreted? + + ASS(added); + + Stack constructors; + + Stack destructorNamesZero; + Stack destructorArgSortsZero; + auto zeroConstructor = buildTermAlgebraConstructor(zero, natSort, destructorNamesZero, destructorArgSortsZero); + constructors.push(zeroConstructor); + + Stack destructorNamesSucc; + destructorNamesSucc.push(pred); + Stack destructorArgSortsSucc; + destructorArgSortsSucc.push(natSort); + auto succConstructor = buildTermAlgebraConstructor(succ, natSort, destructorNamesSucc, destructorArgSortsSucc); + constructors.push(succConstructor); + + TermAlgebra* ta = new TermAlgebra(natSort, constructors.size(), constructors.begin(), false); + env.signature->addTermAlgebra(ta); + + Stack argSorts; + argSorts.push(natSort); + argSorts.push(natSort); + auto pair = declareFunctionOrPredicate(less, Sorts::SRT_BOOL, argSorts); + NatTermAlgebra* nta = new NatTermAlgebra(ta, pair.first); + env.signature->setNat(nta); +} + TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName, unsigned taSort, Stack destructorNames, Stack argSorts) { CALL("SMTLIB2::buildTermAlgebraConstructor"); diff --git a/Parse/SMTLIB2.hpp b/Parse/SMTLIB2.hpp index 337ba975e8..2d511e8b54 100644 --- a/Parse/SMTLIB2.hpp +++ b/Parse/SMTLIB2.hpp @@ -271,6 +271,7 @@ class SMTLIB2 { void readDeclareDatatypes(LExprList* sorts, LExprList* datatypes, bool codatatype = false); + void readDeclareNat(const vstring& nat, const vstring& zero, const vstring& succ, const vstring& pred, const vstring& less); TermAlgebraConstructor* buildTermAlgebraConstructor(vstring constrName, unsigned taSort, Stack destructorNames, Stack argSorts); diff --git a/Shell/TermAlgebra.cpp b/Shell/TermAlgebra.cpp index 89d655ae70..89c3f357d5 100644 --- a/Shell/TermAlgebra.cpp +++ b/Shell/TermAlgebra.cpp @@ -147,4 +147,25 @@ unsigned TermAlgebra::getSubtermPredicate() { return s; } +NatTermAlgebra::NatTermAlgebra(TermAlgebra* ta, unsigned lessPredicate) + : _ta(ta), _lessPredicate(lessPredicate) +{ + if (ta->nConstructors() != 2) { + throw BadNatTermAlgebra("nat must have two constructors"); + } + if (ta->allowsCyclicTerms()) { + throw BadNatTermAlgebra("nat must not allow cyclic terms (use datatype instead of codatatype)"); + } + + _zero = ta->constructor(0); + _succ = ta->constructor(1); + if (_zero->arity() != 0) { + std::swap(_zero, _succ); + } + if (_zero->arity() != 0 || _succ->arity() != 1) { + throw BadNatTermAlgebra("nat constructors must have arity 0 and 1"); + } +} + + } diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index 3b4f0fad6d..c82c2e1f52 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -114,6 +114,36 @@ namespace Shell { bool _allowsCyclicTerms; ConstructorArray _constrs; }; + + class BadNatTermAlgebra : public Lib::Exception { + public: + explicit BadNatTermAlgebra(char const* msg) + : Lib::Exception(msg) + { } + }; + + class NatTermAlgebra { + public: + CLASS_NAME(NatTermAlgebra); + USE_ALLOCATOR(NatTermAlgebra); + + /** May throw BadNatTermAlgebra */ + NatTermAlgebra(TermAlgebra* ta, unsigned lessPredicate); + + TermAlgebra* termAlgebra() { return _ta; } + TermAlgebraConstructor* getZeroConstructor() { return _zero; } + TermAlgebraConstructor* getSuccConstructor() { return _succ; } + + /** $less for nat */ + unsigned getLessPredicate() { return _lessPredicate; } + + private: + TermAlgebra* _ta; + TermAlgebraConstructor* _zero; + TermAlgebraConstructor* _succ; + unsigned _lessPredicate; + }; + } #endif From f6e7295dc2a91a515fe9f62de909c1d00239ce83 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Tue, 3 Dec 2019 13:06:31 +0100 Subject: [PATCH 02/14] add convenience functions for building nat-terms and nat-predicates --- Shell/TermAlgebra.hpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index c82c2e1f52..ac40b50dcc 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -26,6 +26,7 @@ #include "Lib/Array.hpp" #include "Lib/VString.hpp" #include "Kernel/Sorts.hpp" +#include "Kernel/Term.hpp" namespace Shell { class TermAlgebraConstructor { @@ -133,10 +134,25 @@ namespace Shell { TermAlgebra* termAlgebra() { return _ta; } TermAlgebraConstructor* getZeroConstructor() { return _zero; } TermAlgebraConstructor* getSuccConstructor() { return _succ; } - /** $less for nat */ unsigned getLessPredicate() { return _lessPredicate; } + /* + * Convenience methods for generating interpreted terms and predicates + */ + Kernel::TermList createZero() + { + return Kernel::TermList(Kernel::Term::create(_zero->functor(), 0, 0)); + } + Kernel::TermList createSucc(Kernel::TermList arg) + { + return Kernel::TermList(Kernel::Term::create1(_succ->functor(), arg)); + } + Kernel::Literal* createLess(bool polarity, Kernel::TermList lhs, Kernel::TermList rhs) + { + return Kernel::Literal::create2(_lessPredicate, polarity, lhs, rhs); + } + private: TermAlgebra* _ta; TermAlgebraConstructor* _zero; From a9f1ff78c25e9b91cb517c7b689f3c248bb5a06d Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Tue, 3 Dec 2019 13:12:14 +0100 Subject: [PATCH 03/14] implement axiomatization for Nat --- Shell/TheoryAxioms.cpp | 166 +++++++++++++++++++++++++++++++++++++++++ Shell/TheoryAxioms.hpp | 10 +++ 2 files changed, 176 insertions(+) diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp index 26461ab070..168acd4ffa 100644 --- a/Shell/TheoryAxioms.cpp +++ b/Shell/TheoryAxioms.cpp @@ -1137,6 +1137,17 @@ void TheoryAxioms::apply() modified = true; } + auto nat = env.signature->getNat(); + if (nat != nullptr) { + addZeroSmallestElementAxiom(nat); + addDefineSubEqAxiom(nat); + addDefineSubEqDualAxiom(nat); + addMonotonicityAxiom(nat); + addTransitivityAxioms(nat); + addTotalityAxiom(nat); + addDisjointnessAxioms(nat); + } + if(modified) { _prb.reportEqualityAdded(false); } @@ -1376,3 +1387,158 @@ bool TheoryAxioms::addSubtermDefinitions(unsigned subtermPredicate, TermAlgebraC } return added; } + +void TheoryAxioms::addZeroSmallestElementAxiom(NatTermAlgebra* nat) +{ + TermList x(0, false); + auto zero = nat->createZero(); + auto sx = nat->createSucc(x); + + // forall x. 0 < s(x) + auto lit = nat->createLess(true, zero, sx); + + addTheoryClauseFromLits({lit}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); +} + +void TheoryAxioms::addDefineSubEqAxiom(NatTermAlgebra* nat) +{ + // forall x,y. x (x=y or xcreateSucc(y); + auto natSort = nat->termAlgebra()->sort(); + + // clause 1: x!createLess(false, x, sy); + auto clause1Lit2 = Literal::createEquality(true, x, y, natSort); + auto clause1Lit3 = nat->createLess(true, x,y); + + addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // clause 2: x!=y or xcreateLess(true, x, sy); + + addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // clause 3: x!createLess(false, x, y); + auto clause3Lit2 = nat->createLess(true, x, sy); + + addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); +} + +void TheoryAxioms::addDefineSubEqDualAxiom(NatTermAlgebra* nat) +{ + // forall x,y. s(x)! (s(x)=y or x!createSucc(x); + auto natSort = nat->termAlgebra()->sort(); + + // clause 1: s(x)createLess(true, sx, y); + auto clause1Lit2 = Literal::createEquality(true, sx, y, natSort); + auto clause1Lit3 = nat->createLess(false, x, y); + + addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // clause 2: s(x)!=y or s(x)!createLess(false, sx, y); + + addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // clause 3: xcreateLess(true, x,y); + auto clause3Lit2 = nat->createLess(false, sx, y); + + addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); +} + +void TheoryAxioms::addMonotonicityAxiom(NatTermAlgebra* nat) +{ + // forall x,y. x s(x)createSucc(x); + auto sy = nat->createSucc(y); + + // clause 1: x!createLess(false, x, y); + auto clause1Lit2 = nat->createLess(true, sx, sy); + + addTheoryClauseFromLits({clause1Lit1, clause1Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // clause 2: s(x)!createLess(false, sx, sy); + auto clause2Lit2 = nat->createLess(true, x, y); + + addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); +} + +void TheoryAxioms::addTransitivityAxioms(NatTermAlgebra* nat) +{ + TermList x(0, false); + TermList y(1, false); + TermList z(2, false); + auto sy = nat->createSucc(y); + auto sz = nat->createSucc(z); + + auto strict1 = nat->createLess(false, x, y); + auto strict2 = nat->createLess(false, y, z); + auto strict3 = nat->createLess(true, x, z); + auto nonStrict1 = nat->createLess(false, x, sy); + auto nonStrict2 = nat->createLess(false, y, sz); + auto nonStrict3 = nat->createLess(true, x, sz); + + // variant 1: forall x,y,z. x!termAlgebra()->sort(); + + // forall x,y. xy + auto lit1 = nat->createLess(true, x, y); + auto lit2 = Literal::createEquality(true, x, y, natSort); + auto lit3 = nat->createLess(true, y, x); + + addTheoryClauseFromLits({lit1, lit2, lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); +} + +void TheoryAxioms::addDisjointnessAxioms(NatTermAlgebra* nat) +{ + TermList x(0, false); + TermList y(1, false); + auto natSort = nat->termAlgebra()->sort(); + + // Clause 1: x!createLess(false, x, y); + auto clause1Lit2 = Literal::createEquality(false, x, y, natSort); + + addTheoryClauseFromLits({clause1Lit1, clause1Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // Clause 2: x!createLess(false, x, y); + auto clause2Lit2 = nat->createLess(false, y, x); + + addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + + // Clause 3: x!createLess(false, x, x); + + addTheoryClauseFromLits({clause3Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); +} \ No newline at end of file diff --git a/Shell/TheoryAxioms.hpp b/Shell/TheoryAxioms.hpp index 7c0f7de7b8..362cde4a56 100644 --- a/Shell/TheoryAxioms.hpp +++ b/Shell/TheoryAxioms.hpp @@ -28,6 +28,7 @@ #include "Kernel/Theory.hpp" #include "Options.hpp" +#include "Shell/TermAlgebra.hpp" #include @@ -117,6 +118,15 @@ static unsigned const EXPENSIVE = 1; recursive) */ bool addSubtermDefinitions(unsigned subtermPredicate, TermAlgebraConstructor* c); + // nat axioms + void addZeroSmallestElementAxiom(NatTermAlgebra* nat); + void addDefineSubEqAxiom(NatTermAlgebra* nat); + void addDefineSubEqDualAxiom(NatTermAlgebra* nat); + void addMonotonicityAxiom(NatTermAlgebra* nat); + void addTransitivityAxioms(NatTermAlgebra* nat); + void addTotalityAxiom(NatTermAlgebra* nat); + void addDisjointnessAxioms(NatTermAlgebra* nat); + void addTheoryClauseFromLits(std::initializer_list lits, Inference::Rule rule, unsigned level); void addAndOutputTheoryUnit(Unit* unit, unsigned level); }; From 46f6cc74c5aff77ce26d6e06c5508dd55e00ef25 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Tue, 14 Jan 2020 11:38:17 +0100 Subject: [PATCH 04/14] fine-tune time-theory-axioms - remove SubEqDualAxiom, since redundant - simplify clauses using equality resolution with deletion - remove redundant clauses --- Shell/TheoryAxioms.cpp | 66 ++++++++++++------------------------------ Shell/TheoryAxioms.hpp | 1 - 2 files changed, 19 insertions(+), 48 deletions(-) diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp index 168acd4ffa..42e0a382f0 100644 --- a/Shell/TheoryAxioms.cpp +++ b/Shell/TheoryAxioms.cpp @@ -1141,7 +1141,6 @@ void TheoryAxioms::apply() if (nat != nullptr) { addZeroSmallestElementAxiom(nat); addDefineSubEqAxiom(nat); - addDefineSubEqDualAxiom(nat); addMonotonicityAxiom(nat); addTransitivityAxioms(nat); addTotalityAxiom(nat); @@ -1406,6 +1405,7 @@ void TheoryAxioms::addDefineSubEqAxiom(NatTermAlgebra* nat) TermList x(0, false); TermList y(1, false); + auto sx = nat->createSucc(x); auto sy = nat->createSucc(y); auto natSort = nat->termAlgebra()->sort(); @@ -1416,11 +1416,10 @@ void TheoryAxioms::addDefineSubEqAxiom(NatTermAlgebra* nat) addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); - // clause 2: x!=y or xcreateLess(true, x, sy); + // clause 2: x!=y or xcreateLess(true, x, sx); - addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause2Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); // clause 3: x!createLess(false, x, y); @@ -1429,35 +1428,6 @@ void TheoryAxioms::addDefineSubEqAxiom(NatTermAlgebra* nat) addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); } -void TheoryAxioms::addDefineSubEqDualAxiom(NatTermAlgebra* nat) -{ - // forall x,y. s(x)! (s(x)=y or x!createSucc(x); - auto natSort = nat->termAlgebra()->sort(); - - // clause 1: s(x)createLess(true, sx, y); - auto clause1Lit2 = Literal::createEquality(true, sx, y, natSort); - auto clause1Lit3 = nat->createLess(false, x, y); - - addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); - - // clause 2: s(x)!=y or s(x)!createLess(false, sx, y); - - addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); - - // clause 3: xcreateLess(true, x,y); - auto clause3Lit2 = nat->createLess(false, sx, y); - - addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); -} - void TheoryAxioms::addMonotonicityAxiom(NatTermAlgebra* nat) { // forall x,y. x s(x)termAlgebra()->sort(); - // Clause 1: x!createLess(false, x, y); - auto clause1Lit2 = Literal::createEquality(false, x, y, natSort); + // Clause 1: x!createLess(false, x, x); - addTheoryClauseFromLits({clause1Lit1, clause1Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause1Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); // Clause 2: x!createLess(false, x, y); - auto clause2Lit2 = nat->createLess(false, y, x); - - addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); - - // Clause 3: x!createLess(false, x, x); - - addTheoryClauseFromLits({clause3Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); + // already subsumed by other theory axioms, therefore omitted: + // The standard transitivity axiom is + // x xx gives + // x x false + // which is equivalent (using modus tollens) to + // x y! Date: Wed, 26 Feb 2020 11:08:30 +0100 Subject: [PATCH 05/14] fix -tha some option value for Nat This commit refactors the theory axioms for natural numbers, so that they are included not only if -tha is set to on, but also for -tha some. It is motivated by the idea that we sometimes want to exclude expensive integer-theory axioms (by setting -tha to some). In that case, we still want to include all theory axioms for natural numbers, since they are much more likely than integer axioms to contribute to a proof in the setting of Rapid. --- Shell/TheoryAxioms.cpp | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp index 42e0a382f0..c6d38a1ba6 100644 --- a/Shell/TheoryAxioms.cpp +++ b/Shell/TheoryAxioms.cpp @@ -1414,18 +1414,18 @@ void TheoryAxioms::addDefineSubEqAxiom(NatTermAlgebra* nat) auto clause1Lit2 = Literal::createEquality(true, x, y, natSort); auto clause1Lit3 = nat->createLess(true, x,y); - addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); // clause 2: x!=y or xcreateLess(true, x, sx); - addTheoryClauseFromLits({clause2Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause2Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); // clause 3: x!createLess(false, x, y); auto clause3Lit2 = nat->createLess(true, x, sy); - addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); } void TheoryAxioms::addMonotonicityAxiom(NatTermAlgebra* nat) @@ -1441,13 +1441,13 @@ void TheoryAxioms::addMonotonicityAxiom(NatTermAlgebra* nat) auto clause1Lit1 = nat->createLess(false, x, y); auto clause1Lit2 = nat->createLess(true, sx, sy); - addTheoryClauseFromLits({clause1Lit1, clause1Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause1Lit1, clause1Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); // clause 2: s(x)!createLess(false, sx, sy); auto clause2Lit2 = nat->createLess(true, x, y); - addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); } void TheoryAxioms::addTransitivityAxioms(NatTermAlgebra* nat) @@ -1466,13 +1466,13 @@ void TheoryAxioms::addTransitivityAxioms(NatTermAlgebra* nat) auto nonStrict3 = nat->createLess(true, x, sz); // variant 1: forall x,y,z. x!createLess(true, y, x); - addTheoryClauseFromLits({lit1, lit2, lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({lit1, lit2, lit3}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); } void TheoryAxioms::addDisjointnessAxioms(NatTermAlgebra* nat) @@ -1498,7 +1498,7 @@ void TheoryAxioms::addDisjointnessAxioms(NatTermAlgebra* nat) // Clause 1: x!createLess(false, x, x); - addTheoryClauseFromLits({clause1Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, EXPENSIVE); + addTheoryClauseFromLits({clause1Lit1}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); // Clause 2: x! Date: Wed, 26 Feb 2020 19:08:55 +0100 Subject: [PATCH 06/14] hack: add additional integer-axiom: x!=x+1 Allows simplification of clauses: t=t+1 or C => C, where t is an arbitrary term. --- Shell/TheoryAxioms.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp index c6d38a1ba6..8f29c50df4 100644 --- a/Shell/TheoryAxioms.cpp +++ b/Shell/TheoryAxioms.cpp @@ -647,8 +647,12 @@ void TheoryAxioms::addExtraIntegerOrderingAxiom(Interpretation plus, TermList on Literal* nyLxPOne = Literal::create2(lessPred, false, y,xPOne); addTheoryClauseFromLits({nxLy,nyLxPOne}, Inference::Rule::THEORY_AXIOM_EXTRA_INTEGER_ORDERING, EXPENSIVE); + + // hack: add additional axiom x!=x+1 to enable simplification using subsumption-resolution + Literal* notXIsXPlusOne = Literal::createEquality(false, x, xPOne, theory->getOperationSort(plus)); + addTheoryClauseFromLits({notXIsXPlusOne}, Inference::Rule::GENERIC_THEORY_AXIOM, CHEAP); } - + /** * Add axioms defining floor function * @author Giles From f14ba67cebcef25f1bd97fcf3552b913aa204ecf Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Thu, 27 Feb 2020 11:01:59 +0100 Subject: [PATCH 07/14] hack: implement deletion-rule for clauses containing terms s(s(...)) and s(0) This hack is motivated by the observation that there is no example known which is only provable using one of these terms. --- Inferences/TermAlgebraReasoning.cpp | 37 +++++++++++++++++++++++++++++ Inferences/TermAlgebraReasoning.hpp | 13 ++++++++++ Kernel/MainLoop.cpp | 3 +++ 3 files changed, 53 insertions(+) diff --git a/Inferences/TermAlgebraReasoning.cpp b/Inferences/TermAlgebraReasoning.cpp index 4a3000a3d0..0c53b9525b 100644 --- a/Inferences/TermAlgebraReasoning.cpp +++ b/Inferences/TermAlgebraReasoning.cpp @@ -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" @@ -584,5 +585,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; + } } diff --git a/Inferences/TermAlgebraReasoning.hpp b/Inferences/TermAlgebraReasoning.hpp index 5ca2674814..023590de3f 100644 --- a/Inferences/TermAlgebraReasoning.hpp +++ b/Inferences/TermAlgebraReasoning.hpp @@ -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 diff --git a/Kernel/MainLoop.cpp b/Kernel/MainLoop.cpp index 719e9874c7..9f47c36bde 100644 --- a/Kernel/MainLoop.cpp +++ b/Kernel/MainLoop.cpp @@ -156,6 +156,9 @@ ImmediateSimplificationEngine* MainLoop::createISE(Problem& prb, const Options& res->addFront(new TautologyDeletionISE()); res->addFront(new DuplicateLiteralRemovalISE()); + if(prb.hasEquality() && env.signature->getNat() != nullptr) { + res->addFront(new TwoSuccessorsISE()); + } return res; } From a7a872399c0d20098ec73165f3192250bdb492e0 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Fri, 21 Feb 2020 09:30:32 +0100 Subject: [PATCH 08/14] add flag to symbols to mark lemma-predicates --- Kernel/Signature.cpp | 1 + Kernel/Signature.hpp | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index b8f388cdb5..0e46cda43c 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -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), diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index eb76bd100e..351476ce78 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -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 */ From 1683905f1d12379f9e2cc994368b9915b0ff33a1 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Fri, 21 Feb 2020 09:52:39 +0100 Subject: [PATCH 09/14] extend smtlib2-parser to support marking of lemma-predicates --- Parse/SMTLIB2.cpp | 26 +++++++++++++++++++++++--- Parse/SMTLIB2.hpp | 4 ++-- 2 files changed, 25 insertions(+), 5 deletions(-) diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index aa3ac6ddea..5798d3e3f5 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -157,6 +157,19 @@ void SMTLIB2::readBenchmark(LExprList* bench) continue; } + // custom hack to mark lemma-predicates + if (ibRdr.tryAcceptAtom("declare-lemma-predicate")) { + vstring name = ibRdr.readAtom(); + LExprList* iSorts = ibRdr.readList(); + LExpr* oSort = ibRdr.readNext(); + + readDeclareFun(name,iSorts,oSort, true); + + ibRdr.acceptEOL(); + + continue; + } + if (ibRdr.tryAcceptAtom("declare-fun")) { vstring name = ibRdr.readAtom(); LExprList* iSorts = ibRdr.readList(); @@ -777,7 +790,7 @@ bool SMTLIB2::isAlreadyKnownFunctionSymbol(const vstring& name) return false; } -void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort) +void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort, bool isLemmaPredicate) { CALL("SMTLIB2::readDeclareFun"); @@ -796,10 +809,10 @@ void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSor argSorts.push(declareSort(isRdr.next())); } - declareFunctionOrPredicate(name,rangeSort,argSorts); + declareFunctionOrPredicate(name,rangeSort,argSorts, isLemmaPredicate); } -SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack& argSorts) +SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack& argSorts, bool isLemmaPredicate) { CALL("SMTLIB2::declareFunctionOrPredicate"); @@ -808,11 +821,18 @@ SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& nam Signature::Symbol* sym; OperatorType* type; + ASS(!isLemmaPredicate || rangeSort == Sorts::SRT_BOOL); if (rangeSort == Sorts::SRT_BOOL) { // predicate symNum = env.signature->addPredicate(name, argSorts.size(), added); sym = env.signature->getPredicate(symNum); + ASS(added); + if (isLemmaPredicate) + { + sym->isLemmaPredicate = 1; + } + type = OperatorType::getPredicateType(argSorts.size(),argSorts.begin()); LOG1("declareFunctionOrPredicate-Predicate"); diff --git a/Parse/SMTLIB2.hpp b/Parse/SMTLIB2.hpp index 85a04bfda5..e9358f6d4a 100644 --- a/Parse/SMTLIB2.hpp +++ b/Parse/SMTLIB2.hpp @@ -257,14 +257,14 @@ class SMTLIB2 { * store the ensuing DeclaredFunction in _declaredFunctions * and return it. */ - DeclaredFunction declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack& argSorts); + DeclaredFunction declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack& argSorts, bool isLemmaPredicate = false); /** * Handle "declare-fun" entry. * * Declaring a function just extends the signature. */ - void readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort); + void readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort, bool isLemmaPredicate = false); /** * Handle "define-fun" entry. From 55fdfbfacf35578da1c7a65b3c4b3dd81749dbbf Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Fri, 21 Feb 2020 10:42:44 +0100 Subject: [PATCH 10/14] implement ensureNonLemmaPredicateSelected() --- Kernel/BestLiteralSelector.hpp | 3 +++ Kernel/ELiteralSelector.cpp | 1 + Kernel/LiteralSelector.cpp | 28 ++++++++++++++++++++++++++++ Kernel/LiteralSelector.hpp | 1 + Kernel/LookaheadLiteralSelector.cpp | 1 + Kernel/MaximalLiteralSelector.cpp | 1 + Kernel/SpassLiteralSelector.cpp | 1 + 7 files changed, 36 insertions(+) diff --git a/Kernel/BestLiteralSelector.hpp b/Kernel/BestLiteralSelector.hpp index 827786fbac..20d4818eed 100644 --- a/Kernel/BestLiteralSelector.hpp +++ b/Kernel/BestLiteralSelector.hpp @@ -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: @@ -237,6 +239,7 @@ class CompleteBestLiteralSelector LiteralList::destroy(maximals); ensureSomeColoredSelected(c, eligible); + ensureNonLemmaPredicateSelected(c, eligible); } private: diff --git a/Kernel/ELiteralSelector.cpp b/Kernel/ELiteralSelector.cpp index f421f09220..ea5a4d48d5 100644 --- a/Kernel/ELiteralSelector.cpp +++ b/Kernel/ELiteralSelector.cpp @@ -186,4 +186,5 @@ void ELiteralSelector::doSelection(Clause* c, unsigned eligible) c->setSelected(selCnt); ensureSomeColoredSelected(c, eligible); + ensureNonLemmaPredicateSelected(c, eligible); } diff --git a/Kernel/LiteralSelector.cpp b/Kernel/LiteralSelector.cpp index b2faace3be..0d906b8f42 100644 --- a/Kernel/LiteralSelector.cpp +++ b/Kernel/LiteralSelector.cpp @@ -207,6 +207,34 @@ 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"); + + unsigned selCnt=c->numSelected(); + + for(unsigned i=0;igetPredicate(((*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;igetPredicate(((*c)[i]->functor())); + if(!psym->isLemmaPredicate) + { + swap((*c)[selCnt], (*c)[i]); + c->setSelected(selCnt+1); + return; + } + } +} + /** * Perform literal selection on clause @b c * diff --git a/Kernel/LiteralSelector.hpp b/Kernel/LiteralSelector.hpp index 3a24806105..6a90defcbc 100644 --- a/Kernel/LiteralSelector.hpp +++ b/Kernel/LiteralSelector.hpp @@ -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 diff --git a/Kernel/LookaheadLiteralSelector.cpp b/Kernel/LookaheadLiteralSelector.cpp index 88d6b252c0..9b65eda603 100644 --- a/Kernel/LookaheadLiteralSelector.cpp +++ b/Kernel/LookaheadLiteralSelector.cpp @@ -352,6 +352,7 @@ void LookaheadLiteralSelector::doSelection(Clause* c, unsigned eligible) c->setSelected(selCnt); ensureSomeColoredSelected(c, eligible); + ensureNonLemmaPredicateSelected(c, eligible); } } diff --git a/Kernel/MaximalLiteralSelector.cpp b/Kernel/MaximalLiteralSelector.cpp index 7c2bbbffa7..c38fdc5964 100644 --- a/Kernel/MaximalLiteralSelector.cpp +++ b/Kernel/MaximalLiteralSelector.cpp @@ -91,4 +91,5 @@ void MaximalLiteralSelector::doSelection(Clause* c, unsigned eligible) c->setSelected(selCnt); ensureSomeColoredSelected(c, eligible); + ensureNonLemmaPredicateSelected(c, eligible); } diff --git a/Kernel/SpassLiteralSelector.cpp b/Kernel/SpassLiteralSelector.cpp index 34dcea71ac..0e3baa175b 100644 --- a/Kernel/SpassLiteralSelector.cpp +++ b/Kernel/SpassLiteralSelector.cpp @@ -106,4 +106,5 @@ void SpassLiteralSelector::doSelection(Clause* c, unsigned eligible) c->setSelected(selCnt); ensureSomeColoredSelected(c, eligible); + ensureNonLemmaPredicateSelected(c, eligible); } From 8f41d9f00ddaf2ce59217567cf537dcbd507ad57 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Fri, 21 Feb 2020 11:00:18 +0100 Subject: [PATCH 11/14] enforce selection of negative lemma-literals --- Kernel/LiteralSelector.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Kernel/LiteralSelector.cpp b/Kernel/LiteralSelector.cpp index 0d906b8f42..013af0cb44 100644 --- a/Kernel/LiteralSelector.cpp +++ b/Kernel/LiteralSelector.cpp @@ -288,6 +288,18 @@ 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). + for(unsigned i=0;igetPredicate(((*c)[i]->functor())); + if(psym->isLemmaPredicate && isNegativeForSelection((*c)[i])) + { + swap((*c)[i], (*c)[0]); + c->setSelected(1); + return; + } + } + doSelection(c, eligible); } From e708d16a8ff994e2fa47d7fd9d6771c900057d16 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Fri, 21 Feb 2020 11:13:26 +0100 Subject: [PATCH 12/14] introduce option for lemma literal selection --- Kernel/LiteralSelector.cpp | 22 +++++++++++++++------- Shell/Options.cpp | 5 +++++ Shell/Options.hpp | 2 ++ 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/Kernel/LiteralSelector.cpp b/Kernel/LiteralSelector.cpp index 013af0cb44..8d23e07d77 100644 --- a/Kernel/LiteralSelector.cpp +++ b/Kernel/LiteralSelector.cpp @@ -212,6 +212,11 @@ void LiteralSelector::ensureNonLemmaPredicateSelected(Clause* c, unsigned eligib { CALL("LiteralSelector::ensureNonLemmaPredicateSelected"); + if (!env.options->useLemmaPredicateLiteralSelection()) + { + return; + } + unsigned selCnt=c->numSelected(); for(unsigned i=0;igetPredicate(((*c)[i]->functor())); - if(psym->isLemmaPredicate && isNegativeForSelection((*c)[i])) - { - swap((*c)[i], (*c)[0]); - c->setSelected(1); - return; + if (_opt.useLemmaPredicateLiteralSelection()) + { + for(unsigned i=0;igetPredicate(((*c)[i]->functor())); + if(psym->isLemmaPredicate && isNegativeForSelection((*c)[i])) + { + swap((*c)[i], (*c)[0]); + c->setSelected(1); + return; + } } } diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 332046732c..752781b6bd 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -902,6 +902,11 @@ void Options::Options::init() _lookup.insert(&_ageWeightRatioShapeFrequency); _ageWeightRatioShapeFrequency.tag(OptionTag::SATURATION); + _useLemmaPredicateLiteralSelection = BoolOptionValue("lemma_literal_selection","lls",true); + _useLemmaPredicateLiteralSelection.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)"; + _lookup.insert(&_useLemmaPredicateLiteralSelection); + _useLemmaPredicateLiteralSelection.tag(OptionTag::SATURATION); + _useTheorySplitQueues = BoolOptionValue("theory_split_queue","thsq",false); _useTheorySplitQueues.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)"; _lookup.insert(&_useTheorySplitQueues); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 5eee1f12d5..7dd1a47d26 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -2067,6 +2067,7 @@ bool _hard; int ageRatio() const { return _ageWeightRatio.actualValue; } void setAgeRatio(int v){ _ageWeightRatio.actualValue = v; } int weightRatio() const { return _ageWeightRatio.otherValue; } + bool useLemmaPredicateLiteralSelection() const { return _useLemmaPredicateLiteralSelection.actualValue; } bool useTheorySplitQueues() const { return _useTheorySplitQueues.actualValue; } Lib::vvector theorySplitQueueRatios() const; Lib::vvector theorySplitQueueCutoffs() const; @@ -2345,6 +2346,7 @@ bool _hard; RatioOptionValue _ageWeightRatio; ChoiceOptionValue _ageWeightRatioShape; UnsignedOptionValue _ageWeightRatioShapeFrequency; + BoolOptionValue _useLemmaPredicateLiteralSelection; BoolOptionValue _useTheorySplitQueues; StringOptionValue _theorySplitQueueRatios; StringOptionValue _theorySplitQueueCutoffs; From 0f2ac55758b526d2b3cedf2000728e49bf9d657e Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Tue, 21 Jul 2020 10:23:49 +0200 Subject: [PATCH 13/14] improve options used for trace logic domain - turn off the lemma literal option -lls by default - add a new option -csd (off by default) to control the deletion inference rule for successor terms --- Saturation/SaturationAlgorithm.cpp | 2 +- Shell/Options.cpp | 7 ++++++- Shell/Options.hpp | 2 ++ 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index b85fe5590b..549e07fd61 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1636,7 +1636,7 @@ ImmediateSimplificationEngine* SaturationAlgorithm::createISE(Problem& prb, cons res->addFront(new TautologyDeletionISE()); res->addFront(new DuplicateLiteralRemovalISE()); - if(prb.hasEquality() && env.signature->getNat() != nullptr) { + if(prb.hasEquality() && env.signature->getNat() != nullptr && env.options->useSuccessorDeletionRule()) { res->addFront(new TwoSuccessorsISE()); } diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 752781b6bd..7e58acc318 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -902,11 +902,16 @@ void Options::Options::init() _lookup.insert(&_ageWeightRatioShapeFrequency); _ageWeightRatioShapeFrequency.tag(OptionTag::SATURATION); - _useLemmaPredicateLiteralSelection = BoolOptionValue("lemma_literal_selection","lls",true); + _useLemmaPredicateLiteralSelection = BoolOptionValue("lemma_literal_selection","lls",false); _useLemmaPredicateLiteralSelection.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)"; _lookup.insert(&_useLemmaPredicateLiteralSelection); _useLemmaPredicateLiteralSelection.tag(OptionTag::SATURATION); + _useSuccessorDeletionRule = BoolOptionValue("custom_successor_deletion","csd",false); + _useSuccessorDeletionRule.description = "Turn on custom deletion rule for the trace logic domain, which deletes all clauses containing terms of the form s(0) and terms of the form s(s(t)), for arbitrary subterms t"; + _lookup.insert(&_useSuccessorDeletionRule); + _useSuccessorDeletionRule.tag(OptionTag::INFERENCES); + _useTheorySplitQueues = BoolOptionValue("theory_split_queue","thsq",false); _useTheorySplitQueues.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)"; _lookup.insert(&_useTheorySplitQueues); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 7dd1a47d26..a655c397a2 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -2068,6 +2068,7 @@ bool _hard; void setAgeRatio(int v){ _ageWeightRatio.actualValue = v; } int weightRatio() const { return _ageWeightRatio.otherValue; } bool useLemmaPredicateLiteralSelection() const { return _useLemmaPredicateLiteralSelection.actualValue; } + bool useSuccessorDeletionRule() const { return _useSuccessorDeletionRule.actualValue; } bool useTheorySplitQueues() const { return _useTheorySplitQueues.actualValue; } Lib::vvector theorySplitQueueRatios() const; Lib::vvector theorySplitQueueCutoffs() const; @@ -2347,6 +2348,7 @@ bool _hard; ChoiceOptionValue _ageWeightRatioShape; UnsignedOptionValue _ageWeightRatioShapeFrequency; BoolOptionValue _useLemmaPredicateLiteralSelection; + BoolOptionValue _useSuccessorDeletionRule; BoolOptionValue _useTheorySplitQueues; StringOptionValue _theorySplitQueueRatios; StringOptionValue _theorySplitQueueCutoffs; From 69f221032c4b98446275a0f66be2ca8580ae50c2 Mon Sep 17 00:00:00 2001 From: Pamina Georgiou Date: Wed, 14 Apr 2021 10:15:30 +0200 Subject: [PATCH 14/14] Rapid Portfolio Mode --- CASC/PortfolioMode.cpp | 3 ++ CASC/Schedules.cpp | 66 ++++++++++++++++++++++++++++++++++++++++++ CASC/Schedules.hpp | 2 ++ Shell/Options.cpp | 3 +- Shell/Options.hpp | 4 ++- 5 files changed, 76 insertions(+), 2 deletions(-) diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp index e7ca7e3781..bc863a3b89 100644 --- a/CASC/PortfolioMode.cpp +++ b/CASC/PortfolioMode.cpp @@ -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"); } diff --git a/CASC/Schedules.cpp b/CASC/Schedules.cpp index a466411d7a..3fb3edc5b7 100644 --- a/CASC/Schedules.cpp +++ b/CASC/Schedules.cpp @@ -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"); +} diff --git a/CASC/Schedules.hpp b/CASC/Schedules.hpp index 2b437627ab..24e5757d9a 100644 --- a/CASC/Schedules.hpp +++ b/CASC/Schedules.hpp @@ -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); }; diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 7e58acc318..961f6db45a 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -176,7 +176,8 @@ void Options::Options::init() "smtcomp", "smtcomp_2016", "smtcomp_2017", - "smtcomp_2018"}); + "smtcomp_2018", + "rapid"}); _schedule.description = "Schedule to be run by the portfolio mode. casc and smtcomp usually point to the most recent schedule in that category. Note that some old schedules may contain option values that are no longer supported - see ignore_missing."; _lookup.insert(&_schedule); _schedule.reliesOnHard(Or(_mode.is(equal(Mode::CASC)),_mode.is(equal(Mode::CASC_SAT)),_mode.is(equal(Mode::SMTCOMP)),_mode.is(equal(Mode::PORTFOLIO)))); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index a655c397a2..708269984f 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -472,7 +472,9 @@ class Options SMTCOMP, SMTCOMP_2016, SMTCOMP_2017, - SMTCOMP_2018 + SMTCOMP_2018, + + RAPID };