CHANGELOG.md

Changelog

2.1

• add logtk.arith sub-library, using either zarith or num
• implemented two new calculi (with corresponding term orders):
  1. Superposition with first-class Booleans [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_22]
  2. Superposition for full HOL [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_23]
• old 'Case' rules are removed and replaced with corresponding 'BoolHoist' rules
• a new system for selection of Boolean subterms (--bool-select)
• many modes for Boolean reasoning (--boolean-reasoning)
• a whole set of SAT-inspired pre- and inprocessing techniques:
  1. Blocked clause elimination
  2. Nonsingular predicate elimination with definition set recognition
  3. Hidden literal elimination
  4. Quasipure literal elimination
• fixed various issues in handling clause weight, priority and literal selection heuristics
• improved communication with backend
• better (complete) support for renaming common subformulas
• profiling that emits catapult traces (if env contains TEF=1)

2.0

• new complete HO unification algorithm [https://drops.dagstuhl.de/opus/volltexte/2020/12327]
• new system for handling dynamic clausification (--lazy-cnf options)
• many new clause weight, clause priority and literal heuristics (see help for full list)
• added SinE algorithm and made it work with higher-order problems
• added triggered Boolean instantiation (--trigger-bool-inst)
• added support for Bhayat and Reger's combinatory calculus (with corresponding order) [https://link.springer.com/chapter/10.1007%2F978-3-030-51074-9_16]
• improved Leibniz and Andrews equality elimination
• new modes for primitive instantiation
• added support for "Boolean" equality resolution and factoring [https://matryoshka-project.github.io/pubs/ho_bools_paper.pdf]
• added support for non-native treatment of equality predicate (--eq-encode)
• added "early bird" modes (during dynamic clausification) for primitive instantiation (--ho-prim-enum-early-bird)
• require at least OCaml 4.07 (for seq functions)
• remove all arithmetic handling from [Cru 2015]
• in type inference, enforce that type declarations are prenex polymorphic

1.5.1

• compatibility with ocaml 4.08

• move to sneeuwballen organization

• migrate to dune

• changes in HO

• use msat.0.8

• migrate to iter instead of sequence

• make build a bit more robust wrt warn-error

• add travis CI

• perf improvements

• perf: use profile=release

• make floor (and co) a function from real to real

• two bugfixes for polymorphic function types

• fix(demo): update resolution demo so it builds again

• fix(superposition): do not try to rewrite type arguments

• chore: update opam files to 2.0

• move to alcotest for tests

• improve ho selection restrictions

• perf: optimize debugf function (closes #21)

• support more cases in THF parser

• less selection restrictions for lfhol-calculi

• cli option for fool

• bugfix: KBO variable balance for applied variables

• In TPTP, interpret untyped variables as $i, not as a fresh type variable

• Don't rewrite heads in subsumption module

• complete variables one-by-one in complete_eq_args (ArgCong)

• dont rewrite heads in the presence of type variables or nonmonotonicity

• loosen assertion in whnf_deref_rec

• Use type arguments in orderings

• missing supatvars flag should switch off hidden supatvars

1.5

• be compatible with sequence >= 1.0

• cli option to switch off maximal number of variables per clause

• Dockerfile and instructions to build a docker image

• add eta-reduction to LLTerm

• update phases API + params so it's easier to use from utop

• move to jbuilder

• fail early when unifying a variable and a polymorphic constant

• More realistic test to expose a bug in unification of polymorphic terms

• upper bound on msat and deps on logtk

• fix for llprover (use congruence correctly for poly equalities)

• printer for congruence

• cache llproof checking result, display it in llproof-printing

• refactor proof checker to look more like a tableaux prover + dot printing

• llprover: hack to allow checking of rewriting steps that occur under binders

• split proof checker into its own module LLProver

• add linear expressions and arith predicates in LLTerm

• make demodulation more robust

• bugfix in Type.apply for polymorphic type arguments

• stop positive extensionality rule from removing type arguments

• moved detection for "distinct object" syntax into TypeInference

• omit type declarations for distinct objects in TPTP output

• bugfix restrict_to_scope: recursive call when variable already in scope

• bugfix: type of polymorphic application in app_encode tool

• bugfix: app_encode extensionality axiom needs type arguments

• fo_detector tool to count problems with applied variables

• clean up Subst module

• bugfix: wrong polymorphic types in returned unifier

• remove hornet from makefile, improve logitest targets

• remove hornet

• better type error messages

• make Subst.apply tailrec

• "int" mode for variable purification

• bugfix: unquote identifiers in TPTP parser

1.4

• remove inlining on parsers

• cli option for ext-neg rule

• add --check-types for checking types deeply in new clauses

• Add ExistsConst (??) and ForallConst (!!) to TPTP parser

• TPTP parser: allow function types as THF terms

• add cli option -bt (alias for --backtraces)

• completion of equalities with λ-abstractions as RHS in type inference

• THF parser: allow for @ applications in types

• cli flag for ext_pos

• App encode: binary for app-encoding HO applications into FO

• bugfix in ho unification

• in unification, fix order in which bound variables are added to env

• bugfix in unification (would produce wrong type)

• do not simplify in demodulation

• Add StarExec instructions to readme

• bugfixes app_encode

• β-normalize rewrite rules that are eq-completed

• uniform output of “SZS status” instead of “SZS Status”

• auto flattening of applications in STerm

• fix examples/ho/extensionality1.zf by forbidding some HO demodulations

• fix tag managing (and therefore proof checking) for Lit.is_absurd

• bugfix in proof checking related to instantiation

• bugfix in NPDtree

• more elegant and robust sup-at-var condition

• sup-at-var condition with polymorphism

• remove literal comparison by constraint

• no selection of literals containing ho variables

• Stricter sup-at-vars condition

• purify naked variables

1.3

• experimental proof checking with --check (and --dot-llproof <file>) does not work on all proofs, ignores arith and fails on demodulation under lambdas, for now.
• experimental HO branches from Alex Bentkamp (@benti), including advanced term orderings and variations on higher-order lambda-free superposition
• parser for a fragment of dedukti
• end-to-end proof output, starting from input statements
• large refactoring of Proof, with Proof.result being object-like
• get rid of dependency on tip-parser
• bugfix: prevent superposition on non-closed terms (from Geoff)
• Rename --purify to --ho-purify
• don't do sup at vars by default
• Replace kbo and rpo6 by their lambda-free counter-parts
  • Length-Lexicographic symbol status; Merge redundant term_to_head definitions
  • length-lexicographic comparison for lfhokbo
  • mandatory args for skolem constants (to not depend on choice)
• KBO with argument coefficients
• Blanchette's lambda-free higher order KBO (by @benti)
• Rename IDOrBuiltin to Head
• Blanchette's lambda-free higher-order RPO (by @benti)

1.2

• some HO support (with pattern unification)
• only ignore positive version of x=y → …, not other equational rules
• remove remnants of orphan criterion
• add pp_in signature in many modules
• demodulation under lambdas
• HO pattern unification
• add positive extensionality rule in HO
• add eta-reduction, enabled by default
• allow superposition to operate on non-closed terms
• better random generator for HO terms
• only perform primitive enum on clauses with low penalty
• primitive enumeration of predicate variables
• in FOOL, only extract closed terms to toplevel
• add Lambda module with WHNF and SNF
• proper skolemization in negative extensionality rule
• bugfixes for Multiset
• use logitest for tests
• remove orient tool
• full ZF printing, with proof output and proper commenting
• better stats and options for arith; cli option for redundant_by_ineq
• add polarized rewriting rewrite foo => bar
• fix bug in AC for non-FO terms (closes #13)
• introduce attribute for SOS (set of support)
• propagate attributes properly in CNF and type inference
• in induction, only keep inductive clusters(!)
• basic TPTP THF parser; update TPTP parser to support THF, remove ambiguities
• update literal ordering to have a basic approximation for rational lits
• add ho-complete-eq for completing positive equations
• block eq-resolution and destr-eq-res on shielded variables
• in induction, x=y puts x and y in same cluster
• branch using full HO unification
• branch using combinators for HO functions
• detect .tptp files as TPTP
• in Cnf, rewrite f=λ x.t into ∀x. f x=t
• add calculi/Higher_order module; disable completeness if HO
• declare missing rule C (proj-1 x)…(proj-n x) --> x for cstors
• associate a rewrite rule to inductive type's projectors
• option for dumping sat solver logs into a file

1.1

• calculus for rational arith

• do not simplify too eagerly before trying induction

• add optional fuel limit on term rewriting

• disable orphan criterion by default

• remove age in clause queues; make FIFO queue simpler

• re-strenghten again eq-subsumption, by using anti-unification

• generalization on variables occurring both in active and passive pos in induction

• add ArLiteral to generate arbitrary literals

• disable trivial-ineq for arith, by default

• new clause queue, "almost-bfs"

• induction: simplify goals before doing cut on them

• apply exhaustiveness only for non-rec datatypes

• refactor Test_prop to use narrowing, instead of smallcheck

• in arith, remove completeness in case of --no-arith, too

• use a weight α·ω+β in (T)KBO precedence; use classify_cst for weights

• have some warnings in .zf files if identifiers are used undeclared

• normalize term a=b into the corresponding literal

• do not do sub-inductions in clauses with positive lemma(s) in trail

• only do induction on active positions (or under uninterpreted syms)

• add pattern-matching and if/then/else to .zf native format

• add Test_prop in core library, with basic smallcheck

• add arithmetic to ZF parser

• bugfix in zipper: stornger purification avoid some spurious saturations

• in induction, only perform sub-induction in an already inductive clause

• rename libzipperposition back into logtk, fix some compat issues

• improvements in Unif.unif_list_com and IArray

• use new FV_tree in zipperposition

• add FV_tree structure, a new implem of feature vectors

• skolemization re-uses variables names, but lowercase

• add warn-error @8

• add dimacs dump for the SAT solver

• extract proof from SAT solver

• update to containers 1.0

• use a simpler Hash module

• use result everywhere, ditch variant-based error type

• add forall (x y : ty). … syntax (close #4 again)

• more concise syntax for pi (a:type)(b:type).… (close #4)

• collapse Πx:type.… → type into type→…→type

• lambda-lifting in Cnf.flatten to deal with anonymous functions

• fix type inference for higher-order applications (var args)

• basic parsing of arith operators and constants for TIP

• end-to-end proof tracing, simpler Statement, remove StatementSrc

• make def-as-rewrite true by default

• add let to core terms

• add ite and match in STerm and TypedSTerm

• add Fool calculus for dealing with boolean subterms

• more rules in basic_simplification

• remove everything about the meta-prover

• bugfix in sat_solver for evaluating 0-level lits

• allow boolean rewrite rules of the form t or ~ t

• automatic re-generalization of non-induction variables in strengthening

1.0

• rewrite induction
• rewrite typechecking and CNF with new intermediate typed AST
• merge logtk into zipperposition again
• TIP parser
• remove hashconsed strings, use ID instead
• in TPTP, role "lemma" will be considered as a proper lemma
• share subproofs obtained from SAT solver
• better heuristic in ClauseQueue for deep inductive clauses
• add an include statement for ZF
• properly use Msat proofs in Avatar.simplify_trail
• make proof handling in Sat_solver transparent
• make Dtree bounded in depth
• add a new "AC" attribute in ZF, extend attribute system
• add SClause, unfunctorize BBox,ProofStep,Trail, use Msat proofs
• implement term narrowing (+ add some profiling)
• term and clause rewriting (deduction modulo)
• tests: use OUnit2
• Cnf: conversion of prop rewrite rules requires polarization
• optimize injectivity_destruct{+,-}: disregard type (dis)equations
• move almost everything from Zipperposition to Phases_impl
• introduce Phases, a monadic description of the steps taken by main
• make induction enabled by default
• add translation of inductive problems in .zf
• rename type_check_tptp into type_check (several input formats)
• conditional compilation of the prover itself (for debugging the library)
• add warn in Util, add colors in Util.debug
• update Hashcons, with global state, and alternative impl with Hashtbl
• move printing exception, factor code, rename cnf_of_tptp
• options for choosing the input format (zf/tptp)
• new parser and lexer for a ML-like format, ZF
• simpler, more efficient Superposition.compare_literals_subsumption
• change FOTerm.Classic so that App merges type and term arguments
• introduce TypedSTerm.Meta for destructive unification
• add a Binder module
• split Symbol into Symbol and Builtin
• distinction debug/debugf
• big change: use a pack again for core library
• refactor: rename PrologTerm into STerm (simple term)
• move src/base to src/core
• refactor: use equal and compare
• refactoring: change some types, fix warning, Format everywhere
• move pelletier_problems into examples; add tests/ dir with script

0.8

breaking

• breaking: remove Type.tType, makes no sense in the end
• breaking: HOterm: replace TyAt with TyLift (lifts a type to a term)
• breaking: add explicit forall/exists to HOTerm, remove rigid var case

non-breaking

• fix bug in Type Inference
• more error reporting using Printexc and backtraces (requires ocaml >= 4.01)
• improve printers
• fix bug in HOterm.open_at
• convert @τ into τ in type inference, if required (application)
• parser_ho:
  • accept (var:type) as a term
  • fix ambiguities, parse @a (type lifted to term)
  • now lifts types to terms
  • fix parser so it handles forall/exists and has no ambiguity
• rename some constructors (prefixed with 'Logtk' because of overkill sed)
• bugfix in builtin.theory
• meta-prover: remove rigidification, use explicit quantifiers, udpdate builtin.theory
• meta-prover: use sections for debug, forbid rigid vars in axioms/theories
• add function in meta-prover encoding
• update vim syntax for theory files
• add a few functions to HOTerm
• printer in meta/encoding
• enable logtk.meta by default

0.7

• breaking: remove array utils from LogktUtil, use CCArray instead
• breaking: remove list utils from LogktUtil, use CCList instead
• vim support for theory files
• fix bug in solving/Lpo (fresh names collision)
• fix logtk.solving, using Msat rather than (patched) aez
• Skolem.clear_skolem_cache
• Util.debugf for Format-based debugging
• small fixes post-0.6.2

0.6.2

• fix the list of modules in API doc
• fix in Precedence: use symbol equality
• add general info in two cases of parsers.ast_tptp: TypeDecl and NewType
• fix quick tests
• more recent opam file
• Skolem: instantiation functions
• better printing of types (de Bruijn) in foterms
• use Sequence rather than CCSequence

0.6.1

breaking

• remove -pack for Logtk, renamed modules from <Foo> to Logtk<Foo> (to use 4.02s module aliasing)
• remove useless -def-limit argument to the CNF
• use -no-alias-deps when compiling

non-breaking

• fix parsers/Util_tptp.find_file behavior w.r.t $TPTP env variable
• do not rename atomic formulas in CNF (close #1)
• FeatureVector.{iter,fold} implemented
• flush stdout on debug
• add Options.mk_global_opts, deprecating Options.global_opts
• section mechanism for Util.debug (in Util.Section) with inheritance
• bugfix in Precedence.Constr.invfreq
• update arbitrary instances to use qcheck-0.3's fix_fuel combinator
• PartialOrder (and Precedence) give more details when the ordering is not total
• new functions in the precedence
• new modules Precedence_intf, Ordering_intf, PartialOrder_intf

0.6

• do not depend on CCError.t arity
• require bytes to keep compatibility with < 4.02 (String.init too recent)
• Skolem: at creation, now possible to specify prefix for Tseitin atoms
• Util: removed a String.create deprecation warning
• FeatureVector.Make.retrieve_alpha_equiv
• opam file (for easy development version)

0.5.4

• better CNF (with more accurate criterion to choose whether to rename formulas)
• Util.set_{memory,time}_limit
• remove old files

0.5.3

• FOTerm.weight
• Type.depth
• KBO checks that weights are > 0
• use a flag in Formula.simplify, for memoization; makes CNF fast again on some examples
• expose ScopedTerm.flags
• Precedence: make it possible to choose/change the weight fun
• updated README to favor opam

0.5.2

• demo program resolution1.ml
• oasis: --enable-demo flag
• arithmetic binary predicates are polymorphic ($sum, etc)
• target in Makefile to update @next_release tags
• refactor:
  • unification now works with two (optional) DB environments in which bound variables of both terms live.
  • matching: parameter ?allow_open is now used properly in rewriting and indexing
• unif.res_head
• N-ary unification now uses Sequence (simpler, more efficient)

0.5.1

• sort list of modules in doc/api_intro.txt
• code cleanup in ScopedTerm.Seq, less closures, simpler
• bugfix in scopedTerm.DB.open_vars (shift variables!)
• profiling information in CNF
• safety check in CNF: clauses must be closed (!)
• bugfix: Formula.is_closed
• fix printing of Type in TPTP
• add PrologTerm.Syntactic constructor (in place of SimpleApp which doesn't make much sense)
• cleanup: check i>=0 for bvar/var in ScopedTerm, share a common fresh_var generator
• simplified and factorized some code (share term containers)

0.5

• module Sourced; removed Formula.sourced and the likes
• changed printing of arith variables
• simplify interface for De Bruijn in ScopedTerm; more compact implementation using iterators
• safe API for type inference, using the error monad CCError.t everywhere (also in Util_tptp)

0.4

• cleanup:
  • remove submodules, lib/Monad, and many symlinks
  • replace Monad.Err with CCError
• explicit dependency of logtk on sequence and containers
• logtk_parsers depends on menhir as a build tool
• fix issues with build system (solving flag)
• substitution membership for views
• changed hash function
• use lib benchmark rather than bench
• use the new CCHash api for hash functions that take and return int64 values
• add Signature.is_empty
• profiling annotations
• printing of NPDtree into dot
• use CCList and CCKList (in unification)
• allow to protect some variables in Unif.Unary.match_same_scope
• perf improvement: useless buffer allocation in Util.debug
• Multiset:
  • printer, qtest, and new comparison function
  • API change, now a functor dealing with very large multiplicities of elements using Zarith
• ForallTy constructor
• function Comparison.dominates
• bugfixes:
  • do not rename variables for skolemized formulas (otherwise variables won't match)
  • Formula.simplify
  • Unif.Unary.eq
  • Comparison.@>>
  • FOTerm.head
  • arith_hook printer in FOTerm
• enable bin_annot
• printer hooks in formulas
• Unif: equality up to substitution implemented
• in NPDTree, do not capture Not_found that could be raised by the user callback
• lexicographic combinators in Comparison
• module lib/IArray for immutable arrays (previously used in Multiset)
• more abstract requirement for Clause index (feature vector...)
• cli flag to disable ordering generation in hysteresis
• hooks for Cnf

note: git log --no-merges previous_version..HEAD --pretty=%s