54 std::vector<std::string> argv;
68 argv = {
"smt2_solver"};
98 "-preprocessor.toplevel_propagation=true",
99 "-preprocessor.simplification=7",
100 "-dpll.branching_random_frequency=0.01",
101 "-dpll.branching_random_invalidate_phase_cache=true",
102 "-dpll.restart_strategy=3",
103 "-dpll.glucose_var_activity=true",
104 "-dpll.glucose_learnt_minimization=true",
105 "-theory.bv.eager=true",
106 "-theory.bv.bit_blast_mode=1",
107 "-theory.bv.delay_propagated_eqs=true",
109 "-theory.fp.bit_blast_mode=2",
110 "-theory.arr.mode=1"};
145 if(src.size() >= 2 && src.front() ==
'|' && src.back() ==
'|')
146 return std::string(src, 1, src.size() - 2);
159 typedef std::unordered_map<irep_idt, irept> valuest;
173 else if(
parsed.id()==
"unsat")
175 else if(
parsed.id() ==
"unknown")
178 log.error() <<
"SMT2 solver returned \"unknown\"" <<
messaget::eom;
183 parsed.get_sub().front().get_sub().size() == 2)
185 const irept &s0=
parsed.get_sub().front().get_sub()[0];
198 parsed.get_sub().front().id() ==
"error")
206 log.error() <<
"SMT2 solver returned error message:\n"
222 assignment.second.value =
parse_rec(value, assignment.second.type);
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
resultt
Result of running the decision procedure.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
std::size_t number_of_solver_calls
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
static std::string convert_identifier(const irep_idt &identifier)
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
exprt parse_rec(const irept &s, const typet &type)
std::vector< bool > boolean_assignment
identifier_mapt identifier_map
std::size_t no_boolean_variables
message_handlert & message_handler
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
resultt dec_solve() override
Run the decision procedure to solve the problem.
resultt read_result(std::istream &in)
std::stringstream cached_output
Everything except the footer is cached, so that output files can be rewritten with varying footers.
std::stringstream stringstream
const std::string & id2string(const irep_idt &d)
int run(const std::string &what, const std::vector< std::string > &argv)
static std::string drop_quotes(std::string src)
optionalt< irept > smt2irep(std::istream &in, message_handlert &message_handler)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
#define UNREACHABLE
This should be used to mark dead code.