cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
decision_procedure.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Decision Procedure Interface
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
decision_procedure.h
"
13
14
#include <
util/std_expr.h
>
15
16
decision_proceduret::~decision_proceduret
()
17
{
18
}
19
20
decision_proceduret::resultt
decision_proceduret::operator()
()
21
{
22
return
dec_solve
(
nil_exprt
());
23
}
24
25
decision_proceduret::resultt
26
decision_proceduret::operator()
(
const
exprt
&assumption)
27
{
28
return
dec_solve
(assumption);
29
}
30
31
void
decision_proceduret::set_to_true
(
const
exprt
&expr)
32
{
33
set_to
(expr,
true
);
34
}
35
36
void
decision_proceduret::set_to_false
(
const
exprt
&expr)
37
{
38
set_to
(expr,
false
);
39
}
decision_proceduret::operator()
resultt operator()()
Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.
Definition
decision_procedure.cpp:20
decision_proceduret::set_to_false
void set_to_false(const exprt &)
For a Boolean expression expr, add the constraint 'not expr'.
Definition
decision_procedure.cpp:36
decision_proceduret::dec_solve
virtual resultt dec_solve(const exprt &assumption)=0
Implementation of the decision procedure.
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition
decision_procedure.h:45
decision_proceduret::set_to_true
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
Definition
decision_procedure.cpp:31
decision_proceduret::~decision_proceduret
virtual ~decision_proceduret()
Definition
decision_procedure.cpp:16
decision_proceduret::set_to
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
exprt
Base class for all expressions.
Definition
expr.h:57
nil_exprt
The NIL expression.
Definition
std_expr.h:3134
decision_procedure.h
Decision Procedure Interface.
std_expr.h
API to expression classes.
solvers
decision_procedure.cpp
Generated by
1.17.0