Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Nov 24, 2017

• but InterpretedNormalizer only after FoolElimination

  

  Martin Suda

  committed
  8fcb55e

• eleminate fool only after axioms have been added (term algebra ones may add fool)

  

  Martin Suda

  committed
  14c4d38

Commits on Nov 22, 2017

• the forgotten case

  

  Martin Suda

  committed
  47d5450

Commits on Nov 21, 2017

• stop checking for allocator bypasses in children

  

  Martin Suda

  committed
  99e300b

Commits on Nov 20, 2017

• one more case

  

  Martin Suda

  committed
  c5426fb

• EQUAL is back and it doesn't not make much difference

  

  Martin Suda

  committed
  b1eaec2

Commits on Nov 18, 2017

• paying for having made equality interpreted yet not-interpreted

  

  Martin Suda

  committed
  623b250

• printing glitch in TheoryInstAndSimp

  

  Martin Suda

  committed
  087dc6d

Commits on Nov 17, 2017

• fixed ordering assert

  

  Martin Suda

  committed
  fb75e79

Commits on Nov 16, 2017

• more fun with equality evaluation

  

  Martin Suda

  committed
  bca75e9

• debugging non-polymorphic equality

  

  Martin Suda

  committed
  64e76c4

• new rules for quoting symbols - for new equality

  

  Martin Suda

  committed
  cdcffd9

• Merge pull request vprover#43 from easychair/temp_redo_theory_related_stuff

  Show description for 49b07b4
  

  Martin Suda

  authored
  49b07b4

Commits on Nov 15, 2017

• don't count bool sort equality as interpreted

  

  Martin Suda

  committed
  83e7191

• rename variable

  

  Martin Suda

  committed
  9433a03

• indexed interpretations, first step

  

  Martin Suda

  committed
  03643b4

• remove Theory::Equalit from Interpretations

  

  Martin Suda

  committed
  b1b0db6

• haveInterpretingSymbol overload should be of bool return type

  

  Martin Suda

  committed
  edecd6c

• no interpreted distinct groups; should be done by InterpretedEvaluation + some polishing

  

  Martin Suda

  committed
  81ffc0e

• unhack equality a bit (is it polymorphic or isn't it?)

  

  Martin Suda

  committed
  f63f373

• make Z3 compatible

  

  Martin Suda

  committed
  574e74b

• types are shared, don't delete Symbol's types

  

  Martin Suda

  committed
  23ea087

• debugging the new way of doing Interpreted polymorphism

  

  Martin Suda

  committed
  b12d36b

• nobody used DefaultEq anyway

  

  Martin Suda

  committed
  101bb4a

• make Map use equals from Hash (defaults to operator== anyway)

  

  Martin Suda

  committed
  6cd9650

• make Vectore == comparable

  

  Martin Suda

  committed
  5c17f89

• structured inpretretations done differently

  

  Martin Suda

  committed
  5acc529

• removed support for the old smtlib dialect

  

  Martin Suda

  committed
  44240ce

• simplified bool array axiom

  

  Martin Suda

  committed
  3f2656e

• ASSERT(Cond) was obsolete

  

  Martin Suda

  committed
  abd427d

• why not make Lib/DHSet copy constructible? It's inherited from DHMap and it works for free

  

  Martin Suda

  committed
  0ef40b1

• OperatorType class for types of predicate and function symbols; perfectly hashed

  

  Martin Suda

  committed
  3e3ed11

• removed VarSymbol from Signature -- a weird bound propagation leftover

  

  Martin Suda

  committed
  6e6fc6c

• some renamings in Sorts

  

  Martin Suda

  committed
  fd61fa2

• InterpretedSymbol does not need a weird constructor

  

  Martin Suda

  committed
  04c4017

Pagination

PreviousNext