* Adds stats collection and updates in PSymbolic

Adds StatsLogger to print different statistics to a separate file in output/stats-*.log

Adds command line option to specify project name

Adds additional stats for BDD operations

* Support for SMT solving

Working on adding support for SAT/SMT solving using JavaSMT

Minor update in concretizer

* Cleanup solver backends

Merges solver backends into a single class to easily switch solver engines

* Adds solver option -st

Adds option to choose backend solver

Cleans up solver backend

* Adds Yices smt solver

Adds new backend for Yices SMT solver

Adds yices.jar from yices2_java_bindings (needs libyices2java.* in Java path)

Use option -st yices2 to use Yices backend instead of bdd

* Adds caching in Yices solver result

Now caching the result of a Yices solver query

Comments out stats collection by enumeration through concretizer

* Corrects solver backends

Corrects querying isTrue in solver backends

Adds printing/logging changes

* Updates solver backends

Adds result caching in solver guard

TODO: canonical representation for SAT/SMT backends

* Minor update

Corrects parentheses in symbolic compiler

* Adds CVC5 backend

* Adds Z3 backend

* Adds multiple stats collection modes

Changes stats collection from boolean to: 0: no collection, 1: basic stats printing at the end, 2: stats printing after each step, 3: stats printing with transitions counting using concretizer

* Adds solver query printing through Z3

Adds solver query printing in the SearchLogger through Z3 (using CLI option -v 3)

Minor changes to solver backends

* Major changes to SAT backend

Adds an expression library for SAT-based backends (currently using jbool_expressions)

* Adds dedicated expression library for SAT backends

Adds in-house library to expression boolean expressions for SAT/SMT backends

Adds basic (mostly unoptimized) simplifications and AIG mode

* Minor changes

* Adds basic AIG support through ABC

Adds basic support for creating AIGs using ABC's java bindings (under development)

Removes native Expr library

* Adds using FRAIG instead of AIG

Adds using fraig api from ABC to generate functionally-reduced AIGs

Updates abc java bindings to add fraig commands

* Improves FRAIG backend

Adds SAT checking directly via ABC

Adds mode to perform light-weight SAT checking via AIG, followed by checking through independent SAT/SMT solver

Adds setting parameters to FRAIG

* Adds SimpleClientServer example

Minor updates to AIG backend

* Adds option -et to choose expression type

Adds option -et to choose expression type when using sat-based backends

Enables fraigs and native expression library

Major restructuring to expression interface

* Adds aig support without functional reduction

* Setting up stage for switching guard backend

* Minor correction

* Adds ability to switch from bdd to fraig

Adds experimental ability to switch from BDD to Fraig

Adds basic backend for Ivy Aig

* Caching experiments with Iaig

Caching attempts for fraiging with Ivy Aig in ABC

* Cleanup

* Adds commandline option -tl and -ml for specifying time and memory limits

Adds option to specify time and memory limits

Adds option -et auto to auto-switch from Bdd to Fraig on reaching 80% memory consumption

Other minor changes

* Adds more stats collection

Adds recording time stats for creation and solving guards

* Modifies mvn

* Minor change

* Updates pom

* Updates handling timeout

* Minor update

* Minor change

* Update log4j version

* Changes to fraiging

Changes fraiging parameters

Minor other updates

* Adds PSym option -ib

Adds PSym option to limit the number of iterations explored

Minor changes to stats collection for PSym

* New branch exp

* Restore PSym to without fp

Removes symbolic state comparison for now

Adds stats for counting the number of concrete states

* Update PSym's concrete counting

* Adds option to read and write program state

Adds command-line options -r and -w

Option -r enables reading the complete program state (excluding solver backend data structures) from a program state file

Option -w enables writing the complete program state (excluding solver backend data structures) to a program state file as a serialized output

Minor other changes

* Adds setting machine's state

Adds functions to set a machine state

Minor other changes

* Caching recent changes for incremental backtracking

* Adds supporting incremental backtracking

Adds initial support for performing incremental backtracking directly to the backtrack point in depth-first exploration without retracing from the start to reconstruct the state at backtrack point

* Minor correction

* Adds commandline options -nb, -nr, -rs

Adds CLI options for disabling incremental backtracking (-nb), for disabling randomization (-nr), and for specifying a random seed (-rs)

Updates stats collection to report the search result and metrics on number of choices explored/remaining

Minor other changes

* Minor correction to resuming program state

* Minor updates to replaying cex

* Minor update

* Updates to allow serialization

Adds support for writing receives and continuations in PSym in file through serialization

* Adds java bindings for solvers

* Update PSym maven

* Minor change

* Update PSym dependencies

* Adds coverage reporting in PSym

* Reorganize PSym dependencies

* Reorganize PSym dependencies

* Updating jars from AL2

* Minor update

* Removes SimpleClientServer example from tutorial

* Update solver defaults

* Update solver scripts for PSym

* Adds PSym README

* Adds printing backtrack states in file

Adds printing of each backtrack state individually to a file

Cleans up stats to be non-accumulative for resumed runs

Other minor changes relating to writing and resuming run from file

* Minor printing changes

* Minor corrections post removing commits from fp branch

* Adds getting local machine state in Symbolic compiler

* Update backtrack printing in PSym

* Updates concretizer printing in PSym

* Updates pjbdd, cleans concretizer printing

Updates PjBDD to latest version from https://www.sosy-lab.org/ivy/org.sosy_lab/pjbdd/

Cleans up printing in concrete values enumerator

* Minor change