NOTES

======================================================================

 This file is part of the Yices SMT Solver.
 Copyright (C) 2017 SRI International.

 Yices is free software: you can redistribute it and/or modify
 it under the terms of the GNU General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 Yices is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU General Public License for more details.

 You should have received a copy of the GNU General Public License
 along with Yices.  If not, see <http://www.gnu.org/licenses/>.

======================================================================


SOURCE CODE OVERVIEW


The source code is organized as follows:
 
  src/utils:          Utilities and generic data structures

  src/terms:          Internal representation of terms and types, including functions and
                      data structures for building/normalizing/simplifying terms.

  src/models:         Data structures related to building, querying, and manipulating models.
                      (A model stores a mapping from terms to concreted values.)

  src/solvers:        CDCL-based SAT solvers + theory solvers

  src/mcsat:	      MCSAT-based solvers and plugins

  src/context:        Support for creating and manipulating contexts and for simplification
                      and preprocessing of assertions.

  src/exists_forall:  Solver for exists/forall problems

  
  src/api:            Functions and data structures needed to implement the Yices API.

  src/io:             Support for input output, including parsing and pretty printing.

  src/parser_utils:   Data structures common to all front-end tools, including support
                      for parsing and stack-based construction of terms and types.

  src/frontend:       Main binaries. Each front-end supports a different input language.

  src/include:        Header files that specify the Yices API.


src/solvers contains a subdirectory for each solver:

  src/solvers/cdcl:      SAT solver

  src/solvers/bv:        Bit-vector solver

  src/solvers/egraph:    E-graph/UF solver

  src/solvers/simplex:   Solver for linear arithmetic (based on Simplex)

  src/solvers/funs:      Solver for the theory of arrays

  src/solvers/floyd_warshall: Specialized solvers for difference logic


front_ends contains a subdirectory for each main binary

  src/frontend/yices:    Main binary (supports the Yices language and Exists/Forall solving)

  src/frontend/smt1:     yices-smt (supports SMT-LIB 1.2)

  src/frontend/smt2:     yices-smt2 (supports SMT-LIB 2.0)



MORE DETAILS


1) UTILITIES
   ---------

1.1) Memory management
     -----------------

arena.h:                region-based allocator with push/pop functions
arena.c                 (pop frees all objects allocated since the previous push)

int_stack.h:            stack for allocating integer arrays (freed in reverse order
int_stack.c             of allocation).

ptr_stack.h:            stack for allocating pointer arrays (same as int_stack
ptr_stack.c             but for arrays of (void*) objects).

memalloc.h:             wrappers around malloc/realloc/free
memalloc.c              NOTE: this imports 'yices_exit_codes.h'

object_stores.h:        special allocator for objects of a fixed size
object_stores.c



1.2) Miscellaneous utilities
     -----------------------

assert_utils.h:		Wrappers around assert to avoid compilation warnings

bit_tricks.h:           Low-level bit-mask operations (via GCC's __builtins or replacement
                        if they're not present).

command_line.h:         Support for parsing command-line arguments (passed via argc/argv)
command_line.c

cputime.h:              For measuring computing time
cputime.c

dprng.h:		Pseudo-random number generator (floating point implementation)

gcd.h:                  gcd of two integers
gcd.c

hash_functions.h:       various hash functions based on Bob Jenkins's public-domain code
hash_functions.c

int_powers.h:           exponentiation of 32bit or 64bit unsigned integers
int_powers.c

memsize.h:              For measuring memory usage of the current process (approximately)
memsize.c               this does not work on mingw but should work on all other platforms

prng.h:                 simple PRNG generator based on a linear congruence

tagged_pointers.h:      macros for tagging/untagging pointers

timeout.h:              interface to a timeout function (it's implemented using
timeout.c               signal/alarm on Unix or using timer queues on Windows/Mingw)



1.3) Sorting
     -------

int_array_sort.h:       sort an array of integers in increasing order
int_array_sort.c

int_array_sort2.h:      sort an array of integers, ordering supplied by the user
int_array_sort2.c

stable_sort.h:		stable sort: array of (void *) pointers, ordering supplied
stable_sort.c		by the user

ptr_array_sort.h:       sort an array of (void *) pointers in increasing address order
ptr_array_sort.c

ptr_array_sort2.h:      sort an array of pointers, ordering supplied by the user
ptr_array_sort2.c



1.4) Generic data structures
     -----------------------

bitvectors.h:           bit-vectors

dl_lists.h:             doubly-linked lists


1.4.a)  Vectors and Arrays
        ------------------

backtrack_arrays.h:     arrays of integers with support for update, push/pop
backtrack_arrays.c

dep_tables.h:           dependency tables (map integer indices to arrays of
dep_tables.c            integer indices. Similar to use_vectors).

int_vectors.h:          vectors of signed 32bit integers
int_vectors.c

index_vectors.h:        vectors of int32_t integers (similar to int_vectors but
index_vectors.c         more efficient in some cases: use a hidden header)

mark_vectors.h:         arrays to map 32bit integer indices to unsigned 8bit integers,
mark_vectors.c          with a default value

tag_map.h:		maps 32bit to unsigned 8bit like mark_vector but is intended
tag_map.c               to be more efficient for sparse arrays

ptr_vectors.h:          vectors of (void*) pointers
ptr_vectors.c

pointer_vectors.h:      vectors of (void *) pointers: similar to ptr_vectors
pointer_vectors.c       but use the hidden header trick.

refcount_int_arrays.h:  arrays of integers, with reference counters
refcount_int_arrays.c

sparse_arrays.h:	arrays of integers (intended to be efficient if many
sparse_arrays.c		array elements are never read or written)

use_vectors.h:          vectors of tagged pointers (for implementing "use lists")
use_vectors.c


1.4.b)  Queues
        ------

int_queues.h:           queue of signed integers (implemented as a circular array)
int_queues.c

ptr_queues.h:           queue of (void*) pointers (implemented as a circular array)
ptr_queues.c


1.4.c)  Binary Heaps
        ------------

generic_heap.h:         heap of signed 32bit integers, with an ordering function
generic_heap.c          defined by the user.

int_heap.h:             heap of int32_t integers, sorted in increasing order
int_heap.c              (no duplicates, this stores a set)

int_heap2.h:            heap of int32_t integers, user-provided ordering
int_heap2.c             (duplicates are allowed. this stores a bag).
                        This is simpler than generic_heap: removal is not supported.

ptr_heap.h:             heap of (void*) pointers, user-supplied ordering
ptr_heap.c


1.4.d)  Sets/Collections
        ----------------

csets.h:                Sets of integers (all elements are in an interval [0 .. n-1]
csets.c                 where n is fixed when the set is created)

int_bags.h:             bags (multisets) of 32bit non-negative integers
int_bags.c              implemented using resizable arrays.

int_bv_sets.h:          sets of unsigned integers implemented using resizable bitvectors
int_bv_sets.c

ptr_sets.h:             sets of (void*) pointers
ptr_sets.c

ptr_sets2.h:            sets/bags of (void*) pointers (another implementation)
ptr_sets2.c

uint_rbtrees.h:         Red-black trees to store sets of unsigned, 32bit integers
uint_rbtrees.c



1.4.e)  Equivalence Relations/Partitions
        --------------------------------

int_partitions.h:       data structure to construct partitions of integers
int_partitions.c        based on an equivalence relation provided by the user.
                        each non-singleton class is represented as an array of integer.

ptr_partitions.h:       similar to int_partitions but for object represented by pointers
ptr_partitions.c        rather than integers.

union_find.h:           a union-find data structure for 32bit non-negative integers
union_find.c


1.4.f)  Character Strings
        -----------------

refcount_strings.h:     character strings with reference counter ('\0' terminated)
refcount_strings.c

string_buffers.h:       resizable string buffers
string_buffers.c

string_utils.h:         utilities for string parsing and binary search in arrays of strings
string_utils.c


1.4.g)  Hash tables
        -----------

cache.h:                a hash table that stores triples <tag, x, y>
cache.c                 also implements push/pop. It's used by the egraph and other solvers.

int_array_hsets.h:      support for storing and hash-consing arrays of 32bit integers
int_array_hsets.c

int_hash_classes.h:     hash table for maintaining equivalence classes of integers
int_hash_classes.c      the table stores one representative per class

int_hash_map.h:         maps int32 to int32, implemented as hash tables.
int_hash_map.c

int_hash_map2.h:        maps pairs of int32 to int32, implemented as hash tables.
int_hash_map2,c

int_hash_sets.h:        sets of unsigned integers (hash sets)
int_hash_sets.c

int_hash_tables.h:      hash map (maps integers to integers). Intended to support hash-consing.
int_hash_tables.c       more general than int_hash_map.h

pair_hash_map.h:        maps pairs of int32 to (void *) pointers (hash table)
pair_hash_map.c

pair_hash_map2.h:       maps pairs of int32 to int32  (more operations are supported than in
pair_hash_map2.c        int_hash_map2)

pair_hash_sets.h:       sets of pairs of integers (implemented as a hash table)
pair_hash_sets.c

ptr_hash_classes.h:     hash table for maintaining equivalence classes of objects (identified
ptr_hash_classes.c      by pointers). The table stores one representative per class

ptr_hash_map.h:         maps int32 to (void *) pointers (hash table)
ptr_hash_map.c

simple_cache.h:         fixed-size caches
simple_cache.c

string_hash_map.h:	map strings to 32bit integers
string_hash_map.c

symbol_tables.h:        symbol tables: hash map from strings to integers
symbol_tables.c		with support for scoping

tuple_hash_map.h:       hash map for arrays of int32 to int32 values
tuple_hash_map.c




2) TYPES AND TERMS
   ---------------

2.1) Rational and bitvector constants
     --------------------------------

mpq_aux.h:              GMP extensions: operations on multi-precision
mpq_aux.c               rational numbers (mpq_t)

rationals.h:            Yices rational numbers
rationals.c             - a rational is represented as an integer pair num/den
                        or a GMP rational if required

extended_rationals.h:   Extended rationals for dealing with strict inequalities in arithmetic solvers
extended_rationals.c    - an extended rational is a pair of rationals <a, b>, interpreted as a + b\delta
                        where \delta is infinitesimal

bv_constants.h:         Bitvector constants (of fixed size)
bv_constants.c

bv64_constants.h:       Bitvector constants that can fit in an unsigned 64bit integer
bv64_constants.c

rational_hash_maps.h:   Mappings from extended rationals to non-negative 32bit integers
rational_hash_maps.c    (implemented using hash tables)



2.2) Arithmetic and polynomials
     --------------------------

Arithmetic terms are represented as polynomials in fully-expanded form
(i.e.,  sums of  monomials).  Each monomial  is  a pair  (coefficient,
index) and the monomials are sorted in increasing index order. There's
an end-marker  monomial whose  coefficient is uninitialized  and whose
index is INT32_MAX.

There  are   three  types  of   polynomials,  depending  on   how  the
coefficients are represented:

  - polynomials: the coefficients are rationals

  - bv64 polynomials:  the coefficients are bitvector  constants of no
    more than 64bits

  - bv  polynomials:  the  coefficients  are  bitvector  constants  of
    arbitrary size

The  indices   occurring  in  monomials  and   polynomials  are  32bit
(non negative) signed integer:

  - the special index  const_idx = 0 is used  to identify the constant
    part of a polynomial

  - the special index max_idx = INT32_MAX is used for end marker

  - any other  index refers  to an arithmetic  or bitvector term  in a
    global term table

A term index  may be mapped to  a power product, which is  an array of
pairs <index,  exponent>.  The exponent  is an unsigned  32bit integer
and the  index refers to an  arithmetic or bitvector term  in a global
term table (as above).

There's a hard-coded  limit of 2^30-1 on the  degree of polynomials we
can represent/manipulate (this is a theoretical limit, most polynomial
construction will blow up well before that).

Many  arithmetic operations  require an  intermediate  object (buffer)
that  stores a  polynomial  as a  linked  list. Arithmetic  operations
modify the buffer, and the  final result can be extracted/converted to
a polynomial or term.



The relevant source files are:

power_products.h:               Power products = arrays of pairs (x_i, d_i)
power_products,c                - variable x_i is an integer
                                - exponent d_i is a non-negative integer
                                Special representations are used (tagged pointers) for
                                simple products (e.g, x_i^1).

pprod_table.h:                  Table for hash-consing of power products.
pprod_table.c

polynomial_common.h:            Types and constants common to all three types of polynomials.


polynomials.h:                  Polynomials with rational coefficients
polynomials.c

arith_buffers.h:                Buffers for constructing rational polynomials
arith_buffers.c                 (Obsolete: the linked list representation was too
                                inefficient on some benchmarks that have long
                                sums of terms. Replaced by balanced_arith_buffers).

balanced_arith_buffers.h:       Buffers for constructing rational polynomials.
balanced_arith_buffers.c        The implementation is based on red-black trees.

poly_buffer.h:                  Simplified buffer used by the arithmetic solver
poly_buffer.c                   (more specialized, more efficient than arith_buffer).

bv64_polynomials.h:             Polynomials with small bitvector coefficients
bv64_polynomials.c

bvarith64_buffers.h:            Buffers for constructing these polynomials
bvarith64_buffers.c


bv_polynomials.h:               Polynomials with arbitrary-size bitvector coefficients
bv_polynomials.c

bvarith_buffers.h:              Buffers for constructing these polynomials
bvarith_buffers.c

bvpoly_buffers.h:		Simplified buffer for polynomials with bitvector coefficients
bvpoly_buffers.c




2.3) Bit array expressions
     ---------------------

bit_expr.h:               Bit expressions (i.e., boolean expressions represented as DAGs
bit_expr.c                with nodes for XOR/OR and inverters) (variant of AIG).

bvlogic_buffers.h:        Buffers for constructing the bitwise operation on bitvectors
bvlogic_buffers.c         (e.g., bit masking, shifts, sign/zero extension). The buffer
                          stores the result of such operations as an array of n
                          bit expressions.




2.4) Term and type tables
     --------------------

Types  and terms are  identified by  an integer  index.  The  index is
mapped to a  descriptor stored in a global type or  term table. We use
hash   consing:  distinct   term  indices   refer  to   distinct  term
descriptors; distinct type indices have distinct type descriptors.

There's support  for attaching a  name to each  term or type,  and for
garbage collection of unused types and terms.


types.h:                       Table of types + type constructors
types.c

terms.h:                       Table of terms and basic term constructors
terms.c

arith_buffer_terms.h:          Operations involving arith_buffers and terms
arith_buffer_terms.c           Obsolete: arith_buffers are replaced by
                               balanced_arith_buffers.

bvarith64_buffer_terms.h:      Operations involving bvarith64_buffers and terms
bvarith64_buffer_terms.c

bvarith_buffer_terms.h:        Operations involving bvarith_buffers and terms
bvarith_buffer_terms.c

bit_term_conversion.h:         Conversion between bit_expr DAGs and term descriptors
bit_term_conversion.c

poly_buffer_terms.h:           Operation involving poly_buffers and terms
poly_buffer_terms.c

rba_buffer_terms.h:            Operation involving balanced arithmetic buffers
rba_buffer_terms.c             (implemented as red-black trees) and terms.

term_utils.h:                  Utilities to help normalizing/simplifying terms
term_utils.c

conditionals.h:                Generalization of if-then-else
conditionals.c



2.5) Auxiliary data structures for substitutions
     -------------------------------------------

subst_context.h          Store a mapping from int32 to int32 indices
subst_context.c          with a scoping mechanism and hash consing

variable_renaming.h      To rename bound variables by fresh variables
variable_renaming.c

renaming_context.h       Subst context + variable renaming
renaming_context.c

subst_cache.h            Store mapping (term, context) --> term
subst_cache.c

free_var_collector.h     To compute the free variables of a term
free_var_collector.c

term_sets.h:             Sets of terms (represented as hash-sets) to be
term_sets.c              used by the elim_subst code.



5.5) Term and type management API
     ----------------------------

All  operations available  at  the  API are  declared  in yices.h  and
implemented  in   yices_api.c.   In  particular  all   type  and  term
constructors are there.

The  constructors   check  for  well-formedness   of  their  arguments
(including  type  checking)   and  implement  term  normalization  and
simplification.

Main modules for this purpose:

term_manager.h:          Main term-construction module. This is where most term
term_manager.c           simplification/normalization functions are implemented.

term_substitution.h      Stores a substitution + cache + renaming
term_substitution.c      context + free variable collector (also implement
                         beta-reduction).

full_subst.h:            Recursive substitutions: The full substitution
full_subst.c               [x --> f(y), y --> a + b] removes both x and y. It's
                         equivalent to the term_substitution: [x --> f(a+b), y--> a+b].
                         full_subst includes support for building this type of substitution,
                         and for detecting/removing substitution cycles.

elim_subst.h:            Extends full_subst: it builds a full_subst object from
elim_subst.c             a set of literals and a set of variables to eliminates.

term_explorer.h:	 Make the internal term representation accessible via
term_explorer.c          the API.



3) MODELS
   ------

3.1) Basics
     ------

abstract_values.h:      Intermediate objects used by the function/array solver to
abstract_values.c       construct models. The egraph converts these abstract values
                        to constants (concrete values) of appropriate types.

fun_maps.h:             Maps built by the array solver using abstract values. A map
fun_maps.c              has a default value + a finite list of pair (element -> val)

fun_trees.h:            Tree structure used to force maps with infinite domain
fun_trees.c             to be all distinct (cf. fun_solver.c).

concrete_values.h:      Hash-consing + tagging of constants used in models.
concrete_values.c       - concrete values include booleans, rationals, bitvectors, tuples,
                          functions and function updates

fresh_value_maker.h:	Support for building fresh objects (concrete values) of a given
fresh_value_maker.c     type.

small_bvsets.h:         Set of bit-vector constants. Used by the bvsolver to create
small_bvsets.c          fresh values when requested by the egraph. Compact representation
                        that works for small bit-vector width.

large_bvsets.h:         Variant representation for larger bit width (not used).
large_bvsets.c          - sets are stored in an inexact form using Bloom filter ideas

rb_bvsets.h:            Another variant representation. Sets of bit-vector constants
rb_bvsets.c             are stored in red-black trees. (That's what's currently used
                        in bv_solver)

models.h:               Model representation: map terms to concrete values
models.c                - optionally: a model can also include a substitution table
                        that map uninterpreted terms to other terms.

model_eval.h:           Evaluator: compute the (concrete) value of a term in a model
model_eval.c

model_queries.h:        Queries: get the values of one or more terms in a model,
model_queries.c         also implement more efficient functions to check whether
                        a formula or set of formulas is true in a model.

val_to_term.h:		Convert concrete values to constant terms (in terms.h)
val_to_term.c

term_to_val.h:		Convert constant terms to concrete values
term_to_val.c

map_to_model.h:		Convert a mapping to a model
map_to_model.c          - the mapping assigns constant terms to uninterpreted term
                        - this module converts it to the model data structure



3.2) Implicants and Quantifier Elimination
     -------------------------------------

literal_collector.h:	Compute an implicant for a formula based on a model
literal_collector.c     that satisfies the formula.

arith_projection.h:	Model-based Quantifier Elimination for arithmetic
arith_projection.c      (Fourier-Motzkin + a specialized form of Virtual
                        Term Substitution)

projection.h:		Model-based Quantifier Elimination (general)
projection.c

generalization.h:       Generalize from a model/counterexample.
generalization.c



4) SOLVERS
   -------

4.1) Core/SAT solver
     ----------------

smt_core.h:             CDCL-based SAT solver with support for connection to a theory solver
smt_core.c

smt_core_base_types.h:	Type definitions (boolean variables, literals, truth values)

smt_core_printer.h:     Print functions for the core
smt_core_printer.c

gates_hash_table.h:     Support for hash-consing of boolean gates
gates_hash_table.c

gates_manager.h:        Create/assert boolean gates and translate them to clauses
gates_manager.c

gates_printer.h:        Print functions for Boolean gates
gates_printer.c

sat_solver.h:           A separate SAT solver similar to core but without theory solver
sat_solver.c           (it's used to build the yices_sat standalone SAT solver)

sat_parameters.h:	Parameters for sat_solver.c



4.2) Egraph
     ------

egraph_base_types.h:        Types used by the egraph.

egraph_types.h:             Datatypes shared by all the egraph-related modules:
                            - egraph_utils.h/egraph_utils.c
                            - composites.h/composites.c
                            - egraph_explanations.h/egraph_explanations.c
                            - egraph.h/egraph.c

egraph_utils.h:             Utilities to access the egraph_t structure
egraph_utils.c

composites.h:               Support for construction of composite terms (for the egraph)
composites.c                and implementation of a congruence table.

egraph_eq_stats.h:          Data structure to collect statistics about the egraph
egraph_eq_stats.c           (not used).

egraph_explanations.h:      Generation of explanations from the egraph
egraph_explanations.c

egraph_assertion_queues.h:  Queues to store equalities/disequalities/distinct predicate
egraph_assertion_queues.c   that are propagated by the egraph to the satellite solvers.

theory_explanations.h:      Data structure to store explanations produced by satellite solvers
theory_explanations.c

diseq_stacks.h:             Stack that can be used by satellite solvers to store disequalities
diseq_stacks.c              they receive from the egraph.


egraph.h:                   Main egraph functions
egraph.c

egraph_printer.h:           Print functions
egraph_printer.c




4.3) Arithmetic solvers
     ------------------

4.3.a)  Difference Logic Solvers
        ------------------------

dl_vartable.h:          Table that stores variable descriptors for difference logic solvers
dl_vartable.c           - each variable is mapped to a triple [x, y, c] (which denotes
                          the term x - y + c)

idl_floyd_warshall.h:   Solver for integer difference logic problems, implemented using an
idl_floyd_warshall.c    incremental form of the Floyd-Warshall algorithm (for dense problems)

idl_fw_printer.h:       Print functions for the idl_floydwarshall solver
idl_fw_printer.c

rdl_floyd_warshall.h:   Solver for real difference logic problems, implemented using an
rdl_floyd_warshall.c    incremental form of the Floyd-Warshall algorithm (for dense problems)

rdl_fw_printer.h:       Print functions for the rdl_floydwarshall solver
rdl_fw_printer.c



4.3.b)  Simplex Solver
        --------------

arith_vartable.h:       Table of arithmetic variables: maps variables to a definition
arith_vartable.c        - uses hash-consing, has support for push/pop/reset, supports 
                        non-linear polynomials as definitions

arith_atomtable.h:      Table of arithmetic atoms: supported atoms are (x >= c), (x <= c) or (x == c)
arith_atomtable.c       where x is a variable and c is a rational constant
                        - uses hash-consing, has support for push/pop/reset


diophantine_systems.h:  Subsolver (used by Simplex) to deal with linear diophantine equations
diophantine_systems.c

dsolver_printer.h:      Print functions for the diophantine system solver.
dsolver_printer.c

matrices.h:             Matrix representation used by the Simplex solver
matrices.c

offset_equalities.h:    Support for processing equalities of the form x = y + k (where k is a constant)
offset_equalities.c     (intended to be propagate equalities to the egraph)

simplex_types.h:        Simplex-related type definitions

simplex_propagator0.h:  Experimental code to implement theory propagation in the Simplex solver
simplex_propagator1.h

simplex_prop_table.h
simplex_prop_table.c

simplex.h:              Simplex solver
simplex.c

simplex_printer.h:      Print functions for the simplex solver
simplex_printer.c



4.4) Function/Array solver
     ---------------------

fun_solver.h:           Solver for the function/array theory
fun_solver.c            - deals with extensionality and array updates

fun_solver_printer.h:   Print functions for the array solver
fun_solver_printer.c



7.5) Bit vector solver
     -----------------

merge_table.h:          Table for representing equivalence classes of variables
merge_table.c           (union-find with support for push/pop)

remap_table.h:          Support for building equivalence classes of pseudo literals
remap_table.c           and for mapping these to real literals in the SAT solver

bit_blaster.h:          Conversion of bit-vector operations to CNF
bit_blaster.c


bv_vartable.h:          Table of bit-vector variables
bv_vartable.c

bv_atomtable.h:         Table of bit-vector atoms
bv_atomtable.c

bvbound_cache.h:        Hash table that stores lower and upper bounds on a variable x
bvbound_cache.c         (if known).

bvconst_hmap.h:         Mapping from variables to bit-vector constants (used by bvsolver during
bvconst_hmap.c          model construction).

bvexp_table.h:          Table that stores bitvector polynomials in fully expanded form.
bvexp_table.c           (Used for simplification).

bv64_intervals.h:       Data structure to store intervals defined by two bit-vector constants
bv64_intervals.c        of no more than 64 bits. (Used by bvsolver for simplification)

bv_intervals.h:         More general version: intervals defined by two bit-vector constants
bv_intervals.c          with more than 64bits. (Used by bvsolver for simplification)

bvpoly_compiler.h:      Support for converting bit-vector polynomials to more elementary
bvpoly_compiler.c       terms built using binary add, binary product, etc.

bvpoly_dag.h:           DAG of elementary bit-vector arithmetic operation (used
bvpoly_dag.c            by bvpoly_compiler)

bvsolver_types.h:       Data types used by the bitvector solver

bvsolver.h:             Bit-vector solver
bvsolver.c

bvsolver_printer.h:     Print functions for the bitvector solver
bvsolver_printer.c

dimacs_printer.h:	Export a bitvector problem to the DIMACS format.
dimacs_printer.c        (also works for pure Boolean problems).




5) CONTEXT
   -------

A context stores  a set of assertions and one or  more solvers to deal
with  these assertions. Processing  formulas requires  converting them
from  the term representation  used in  the term  table into  the term
representation used by the  solvers (we call that internalization).

Also the context performs formula simplification and supports push/pop,
and implements the toplevel solver and model construction procedures.


5.1) Internalization
     ----------------

internalization_codes.h:      Utilities for tagging/untagging internalization codes
                              each code is 32bit and represents different objects
                              depending on its sign bit and low-order bits.

internalization_table.h:      Table that maps external objects (terms) to
internalization_table.c       solver objects (literals/theory variables).
                              The table can also store a variable substitution
                              (i.e., mapping form uninterpreted terms to other terms).
                              It supports push and pop.

internalization_printer.h:    Print functions to display the internalization table.
internalization_printer.c


pseudo_subst.h:               Store a candidate variable substitution.
pseudo_subst.c                This is a mapping from uninterpreted term to other terms.
                              It can be turned into a real substitution after substitution
                              cycles are removed.

eq_abstraction.h:             Equality abstraction: the abstraction of a formula F is
eq_abstraction.c              the set of equalities implied by F (over a fixed set of terms)
                              - eq_abstraction implements the abstract domain (i.e. a term partition)
                              and the associated meet/join operations.

eq_learner.h:                 Computation of equality abstraction for a formula F
eq_learner.c

symmetry_breaking.h:          Add constraints to break symmetries in QF_UF problems
symmetry_breaking.c

conditional_definitions.h:    Data structures to reconstruct hidden conditional definitions
conditional_definitions.c     in QF_LIA encodings.

context_simplifier.c:         Simplification and preprocessing procedures used by context.c
                              - implements simplifications that are independent of the solvers

context.h:                    Top-level context module, intended to provide assert/push/pop/reset
context.c                     - implements the translation of yices terms (as provided by yices.h API)
                                into the egraph and solver(s) data structures

context_printer.h:            Print internal context structures
context_printer.c

dump_context.h:		      Print context details (mostly for debugging).
dump_context.c


5.2) Solving
     -------

context_solver.c:            Global search algorithm for formulas asserted in a context

context_statistics.h:	     Print statistics on the search + others
context_statistics.c





6) EXISTS/FORALL SOLVER
   --------------------

An exists/forall solver is intended to solve problems of the form (EXISTS x. FORALL y. P(x, y)).
The solution (if any) is an assignment for the variables x such that FORALL y. P(.., y) holds.
We implement this using two contexts: one search for candidate assignments for x, the other
tries to refute such candidates by finding counterexamples (i.e., assignments for y that
make P(..,y) false).

ef_problem.h:               Data structure to store a problem of this form..
ef_problem.c

ef_analyze.h:               Preprocessing, simplification, and construction of an ef_problem
ef_analyze.c                structure from a set of assertions. This takes input of the
                            form FORALL y. P(x, y) and builds an ef_problem from this.

efsolver.h:                 Solver for an EF problem.
efsolver.c




7) API
   ---

yices_types.h:	            Types visible at the external API

yices_limits.h:             Hardcoded limits on term/type representations

yices.h:                    (public) API

yices_exit_codes.h:         Constants passed to the 'exit' system call on unrecoverable errors

yices_api.c:                Implements all API functions and more

yices_error.h:              Error messages based on an error_report structure
yices_error.c               maintained by yices_api.c

yices_extensions.h:         Functions defined in yices_api.c that are not part
                            of the API. These are variants of functions declared
                            in 'yices.h'.

yices_globals.h:	    Declare a global structure (maintained in yices.c) that
			    store pointers to the global tables and other global variables
			    maintained by yices.c.

yices_iterators.h:          Functions to iterate over all contexts, models, etc.
                            (these functions are defined in yices_api.c)


yices_version_template.txt:
yices_version.c             Version number + compilation + architecture.
                            yices_version.c is generated from yices_version_template.txt
                            when compiling (cf. src/Makefile).


context_config.h:           Data structure to store context configuration info
context_config.c            (logic + optional features + solvers)

search_parameters.h:        Data structure to store options/settings used by the main
search_parameters.c         solver functions.


smt_logic_codes.h:          Convert the known SMT-LIB logic names (e.g., "QF_AUFLIA")
smt_logic_codes.c           into a numerical code.


yval.h:			    DAG data structures to examine non-atomic values in a model
yval.c



8) INPUT/OUTPUT
   ------------

reader.h:               Object for reading from files or strings
reader.c                keeps track of position (line/column number) and stores
                        a current character.

writer.h:		Wrapper that provide uniform functions to write to
writer.c                a file or a string buffer.

pretty_printer.h:       Pretty printer core (Oppen-style implementation).
pretty_printer.c

yices_pp.h:             Yices pretty printer (extends pretty_printer)
yices_pp.c

term_printer.h:         Print functions for the terms
term_printer.c

type_printer.h:         Print functions for the types
type_printer.c

tracer.h:               To print messages depending on a verbosity level
tracer.c

concrete_value_printer.h:   Print functions for concrete values
concrete_value_printer.c

model_printer.h:         Code to display a model
model_printer.c




9) PARSING SUPPORT
   ---------------

We currently  support three  input languages for  defining terms/types
and interactive with Yices:
- the Yices language itself
- enough of the SMT-LIB notation version 1.2 to deal with the official
  SMT-LIB benchmarks used in the SMT Solver Competition in 2009.
- the SMT-LIB notation version 2.0 (support is not complete yet)

All parsers rely on the following modules

lexer.h:                Data structure shared by the yices and smt lexers
lexer.c                 includes a reader object and stores a current token.

parser.h:               Data structure shared by the Yices and SMT-LIB parsers.
parser.c                It provides support for implementing recursive-descent parsers
                        Also maintains a stack of lexers (for nested includes).

term_stack2.h:           Stack-based term builder. New implementation of term_stack
term_stack2.c             (removed the commands that were specific to Yices).

term_stack_error.h:      Error messages and diagnosis when the
term_stack_error.c       term stack module raises an exception.

tstack_internals.h:      Term-stack operations for specializing/extending the default
                         term_stack.




10) FRONT ENDS
    ----------

10.1) Yices solver
     ------------

yices_keywords.txt          Input for gperf (to construct a perfect hash for the
                            Yices keywords)

yices_hash_keywords.h       Perfect hash function for the Yices keywords. Generated by
                            gperf from yices_keywords.txt

yices_lexer.h:              Yices lexing functions
yices_lexer.c

yices_parse_tables.h:       Tables used for parsing the Yices language
                            (see utils/yices_parser.txt and utils/table_builder.c)

yices_parser.h:             Parser for the Yices language
yices_parser.c

yices_tstack_ops.h          Opcodes used by Yices version of term_stack

yices_help.h:               On-line help for the solver (Yices language)
yices_help.c

arith_solver_codes.h:       Used to process command line options
arith_solver_codes.c        - convert a solver name (e.g., "simplex") to a numerical code

yices_reval.h:              Read-eval-print loop. Accepts input in the Yices language
yices_reval.c               - this is separated so that the reval functions can be called
                              from LISP

yices_main.c:              Top-level Yices module for problems in the Yices language
                           - just calls yices_reval



10.2) SMT 1.2 solvers
      ---------------

smt_keywords.txt           Input for gperf (to construct a perfect hash for the
                           smt-lib keywords)

smt_hash_keywords.h        Perfect hash function for the SMT-LIB keywords. Generated by
                           gperf from smt_keywords.txt

smt_lexer.h:               SMT-LIB lexing functions
smt_lexer.c

smt_parse_tables.h:        Tables for SMT-LIB parsing (see utils/smt_parser.txt)

smt_parser.h:              SMT-LIB parser
smt_parser.c

smt_term_stack.c:	   Variant of term_stack for SMT-LIB 1.2
smt_term_stack.h

yices_smt.c:               Solver for problems in the SMT-LIB notation
                           - support for command-line options for benchmarking/testing

yices_smtcomp.c:           Solver for problems in the SMT-LIB notation
                           - competition version: no parameter setting available
                           on the command line.


10.3) SMT-LIB 2 solver
     -----------------

smt2_tokens.txt:           All tokens + reserved symbols used in SMT-LIB 2.0 (including
                           command names).

smt2_hash_tokens.h:        Perfect hash function, generated by gperf from smt2_tokens.txt

smt2_keywords.txt:         All predefined keywords in SMT-LIB 2.0 (e.g., :print-success)

smt2_hash_keywords.h:      Perfect hash function, generated by gperf from smt2_keywords.txt

smt2_symbols.txt:          All theory symbols (for all theories defined as of Aug. 2011)

smt2_hash_symbols.h:       Generated by gperf from smt2_symbols.txt

smt2_lexer.h:              Lexical analysis
smt2_lexer.c

smt2_parse_tables.h:       Tables for parsing the SMT-LIB 2.0 language
                           (see utils/smt2_parser.txt and utils/table_builder.c)

smt2_parser.h:             Parser for SMT-LIB 2.0
smt2_parser.c

attribute_values.c         Support for storing attributes (as defined in the SMT-LIB 2 notation)
attribute_values.h

parenthesized_expr.h:      Support to store expressions in the SMT-LIB 2.0 notation
parenthesized_expr.c       - for this purpose, an expression is any well-parenthesized sequence
                             of tokens

smt2_expressions.h:        Store then pretty-print input expressions in the SMT-LIB 2.0 notation
smt2_expressions.c         (this uses the parenthesized_expr representation).

smt2_printer.h:		   Pretty printer for concrete_values in the SMT-LIB 2.0 syntax
smt2_printer.c

smt2_model_printer.h:	   Pretty print models using the SMT-LIB 2.0 syntax
smt2_model_printer.c


smt2_term_stack.h:         Built on top of term_stack2: with variant implementation of
smt2_term_stack.c          several operations to follow the SMT-LIB 2.0 conventions, and
                           new operations that are specific to SMT-LIB 2.0.


smt2_commands.h:           Commands defined in SMT-LIB 2.0 (not complete yet)
smt2_commands.c

yices_smt2.c:		   Solver for problems in the SMT-LIB 2.0 notation



10.4) SAT solver
     ----------

yices_sat.c:               SAT solver: reads DIMACS CNF input








11) EXPERIMENTAL MODULES
    --------------------

update_graph.h:            Incomplete: new module intended to replace the array solver
update_graph.c             (including support for simple lambda terms)

bool_vartable.h:	   Intended to simplify and improve bitblasting
bool_vartable.c

booleq_table.h:		   Store Boolean variables that are defined as (xor x y)
booleq_table.c

flattening.h:              Flattening of conjuncts/disjuncts with optional
flattening.c               flattening of iff and Boolean ite. Most of this
                           functionality is implemented in ef_analyze.