Code

Gleiss rapid final#223

Code

Open

selig wants to merge 15 commits intomastervprover/vampire:masterfrom gleiss-rapid-finalvprover/vampire:gleiss-rapid-finalCopy head branch name to clipboard

+504-8

Commits

Commits on Apr 17, 2020

• Recognize term algebra of natural numbers

  

  JakobR

  authored and

  gleiss

  committed
  3ccec0b

• add convenience functions for building nat-terms and nat-predicates

  gleiss

  committed
  f6e7295

• implement axiomatization for Nat

  gleiss

  committed
  a9f1ff7

• fine-tune time-theory-axioms

  Show description for 46f6cc7
  gleiss

  committed
  46f6cc7

• fix -tha some option value for Nat

  Show description for adc3a0c
  gleiss

  committed
  adc3a0c

• hack: add additional integer-axiom: x!=x+1

  Show description for ce3efce
  gleiss

  committed
  ce3efce

• hack: implement deletion-rule for clauses containing terms s(s(...)) and s(0)

  Show description for f14ba67
  gleiss

  committed
  f14ba67

Commits on Jul 17, 2020

• add flag to symbols to mark lemma-predicates

  gleiss

  committed
  a7a8723

• extend smtlib2-parser to support marking of lemma-predicates

  gleiss

  committed
  1683905

• implement ensureNonLemmaPredicateSelected()

  gleiss

  committed
  55fdfbf

• enforce selection of negative lemma-literals

  gleiss

  committed
  8f41d9f

• introduce option for lemma literal selection

  gleiss

  committed
  e708d16

• Merge branch 'nat-theory' into rapid-final

  Show description for 6e142ae
  gleiss

  committed
  6e142ae

Commits on Jul 21, 2020

• improve options used for trace logic domain

  Show description for 0f2ac55
  gleiss

  committed
  0f2ac55

Commits on Apr 14, 2021

• Rapid Portfolio Mode

  mina1604

  committed
  69f2210