Public interface of class 'InlineResult'. More...
#include <InlineResult.h>
Related Functions | |
(Note that these are not member functions.) | |
| InlineResult_ptr | InlineResult_copy (const InlineResult_ptr self) |
| The InlineResult class copy constructor. | |
| InlineResult_ptr | InlineResult_create (Rbc_Manager_t *mgr, Rbc_t *f) |
| The InlineResult class constructor. | |
| void | InlineResult_destroy (InlineResult_ptr self) |
| The InlineResult class destructor. | |
| Rbc_t * | InlineResult_get_c (InlineResult_ptr self) |
| Returns a formula representing the conjuction set. | |
| Rbc_t * | InlineResult_get_inlined_f (InlineResult_ptr self) |
| Returns the inlined formula, _without_ the conjuction set. | |
| Rbc_t * | InlineResult_get_inlined_f_and_c (InlineResult_ptr self) |
| Returns the inlined f conjucted with the conjuction set. | |
| Rbc_t * | InlineResult_get_original_f (InlineResult_ptr self) |
| Returns the original formula f that was submitted to the constructor. | |
Public interface of class 'InlineResult'.
Definition of the public accessor for class InlineResult
| InlineResult_ptr InlineResult_copy | ( | const InlineResult_ptr | self | ) | [related] |
The InlineResult class copy constructor.
The InlineResult class copy constructor
| InlineResult_ptr InlineResult_create | ( | Rbc_Manager_t * | mgr, | |
| Rbc_t * | f | |||
| ) | [related] |
The InlineResult class constructor.
AutomaticStart
The InlineResult class constructor
| void InlineResult_destroy | ( | InlineResult_ptr | self | ) | [related] |
| Rbc_t * InlineResult_get_c | ( | InlineResult_ptr | self | ) | [related] |
Returns a formula representing the conjuction set.
The conjuction set is made into a formula like:
foreach (v,exp) belonging to the conjuction set,
(\/ v <-> exp) \/ inlined_f
| Rbc_t * InlineResult_get_inlined_f | ( | InlineResult_ptr | self | ) | [related] |
Returns the inlined formula, _without_ the conjuction set.
A lazy approach to SAT can exploit the fact that if a model satisfies inlined f, then it satisfies f as well. If a counterexample must be shown though, inlined f must be conjuct with the conjuction set.
| Rbc_t * InlineResult_get_inlined_f_and_c | ( | InlineResult_ptr | self | ) | [related] |
Returns the inlined f conjucted with the conjuction set.
| Rbc_t * InlineResult_get_original_f | ( | InlineResult_ptr | self | ) | [related] |
Returns the original formula f that was submitted to the constructor.
1.6.1
