cprover
|
#include <fstream>
#include <iostream>
#include "smt2_parser.h"
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <util/cout_message.h>
#include <util/simplify_expr.h>
#include <util/replace_symbol.h>
#include <solvers/sat/satcheck.h>
#include <solvers/flattening/boolbv.h>
Go to the source code of this file.
Classes | |
class | smt2_solvert |
Functions | |
int | solver (std::istream &in) |
int | main (int argc, const char *argv[]) |
int main | ( | int | argc, |
const char * | argv[] | ||
) |
Definition at line 247 of file smt2_solver.cpp.
References solver().
int solver | ( | std::istream & | in | ) |
Definition at line 220 of file smt2_solver.cpp.
References messaget::M_STATISTICS, message_handler, smt2_parsert::parse(), and messaget::set_message_handler().
Referenced by satcheck_glucose_baset< Glucose::SimpSolver >::add_variables(), satcheck_minisat2_baset< Minisat::Solver >::add_variables(), bmct::all_properties(), bv_refinementt::arrays_overapproximated(), cannot_be_neg(), satcheck_minisat2_baset< Minisat::Solver >::clear_interrupt(), find_counter_example(), generate_symbol_resolution_from_equations(), cbmc_solverst::get_default(), cbmc_solverst::get_smt2(), satcheck_minisat2_baset< Minisat::Solver >::interrupt(), satcheck_glucose_baset< Glucose::SimpSolver >::is_in_conflict(), satcheck_minisat2_baset< Minisat::Solver >::is_in_conflict(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), satcheck_minisat2_baset< Minisat::Solver >::lcnf(), satcheck_glucose_baset< Glucose::SimpSolver >::lcnf(), main(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), satcheck_glucose_baset< Glucose::SimpSolver >::prop_solve(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity(), and satcheck_minisat2_baset< Minisat::Solver >::set_polarity().