smt2_incremental_decision_procedure.h File Reference

Decision procedure with incremental SMT2 solving. More...

#include <util/expr.h>
#include <util/message.h>
#include <solvers/smt2_incremental/ast/smt_terms.h>
#include <solvers/smt2_incremental/encoding/struct_encoding.h>
#include <solvers/smt2_incremental/object_tracking.h>
#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
#include <solvers/smt2_incremental/smt_object_size.h>
#include <solvers/smt2_incremental/type_size_mapping.h>
#include <solvers/stack_decision_procedure.h>
#include <memory>
#include <unordered_map>

Include dependency graph for smt2_incremental_decision_procedure.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	smt2_incremental_decision_proceduret
class	smt2_incremental_decision_proceduret::sequencet
	Generators of sequences of uniquely identifying numbers used for naming SMT functions introduced by the decision procedure. More...

Detailed Description

Decision procedure with incremental SMT2 solving.

Definition in file smt2_incremental_decision_procedure.h.