Compiling Psyche requires an OCaml compiler. We compile it with OCaml 4.02 (with ocamlbuild), and findlib 1.6.2.
Psyche 2.1 also uses Jane Street's Core and ASync libraries.
Change log since 2.02:
- New theory module for ground theory combination, as alternative to first-order unification theory
That module works as an orchestrator that can take a list of arbitrary theory solvers and combines them in an asynchronous way; this is using Jane Street's Async library, whose task scheduler we use to run the different theory solvers concurrently
- Reorganisation of code for the above
Change log since 2.01:
Change log since 2.0:
- better address system for plugins
Change log since 1.6:
- Psyche goes first-order
- kernel can treat quantifiers, propagate constraints from branch to branch (still about 800 lines)
- a theory module implements pure first-order logic
- the SMTLib2 parser can handle quantifiers
Change log since 1.5:
- added Congruence Closure among theories
- provided restart features
- provided additional python tools for monitoring runs
Change log since 1.4:
- removed Memoisation facility from kernel; LCF-style ensures this is safe
- gathered debug code in one module "Dump", where each component can dump information
- more generally, purified kernel code, now only 575 lines long (Psyche 1.5 is 4155 lines in total)
Change log since 1.3:
- reorganisation of code de-correlating parsers and theories (adding new theory does not require writing a new parser entirely)
- command-line option to treat input files from smaller to bigger or alphabetically
Change log since 1.2:
- input can be standard input or file or examples present in the code
- creation of a real command-line interface, where everything can be controlled (theory, plugin, latex output, input,...)
- addition of a decision procedure for linear rational arithmetic
- parser for SMTLib2, so that Psyche can parse linear rational arithmetic problems
The parser uses Alt-Ergo's SMTLib2 parser.
We compiled previous versions with OCaml 3.11.
Change log since 1.1:
- The plugin for DPLL with watched literals can now either branch on Decide or on the analysis of a clause that is not yet satisfied.
- The DIMACS parser is a bit more robust (considers tabs like spaces, better ignores comment lines,... but please finish each clause with a 0!)
Change log since 1.0:
- Kernel is now modularised by a decision procedure to be called for initial rule (axiom) and for consistency checks.
An src directory dec_procs has been created to place the decision procedures; it currently contains the interface (module type) that decision procedures are required to implement, and the decision procedure for the empty theory
- A new plugin has been added for DPLL, implementing the technique of watched literals; that technique allows fast detection of backtrack and unit propagation states (faster than the technique implemented in the previous plugin based on Patricia trees). Old DPLL plugin renamed DPLL_Pat, the new one is called DPLL_WL.