Decision procedure with incremental solving with contexts and assumptions. More...

#include <vector>
#include "decision_procedure.h"

Include dependency graph for stack_decision_procedure.h:

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

Classes
class	stack_decision_proceduret

Detailed Description

Decision procedure with incremental solving with contexts and assumptions.

Normally, solvers allow you only to add new conjuncts to the formula, but not to remove parts of the formula once added.

Solvers that offer pushing/popping of contexts or 'solving under assumptions' offer some ways to emulate removing parts of the formula.

Example 1: push/pop contexts:

dp.set_to_true(a);     // added permanently
resultt result = dp(); // solves formula 'a'
stack_decision_procedure.set_to_true(b); // added permanently
resultt result = dp(); // solves 'a && b'
dp.push();
dp.set_to_true(c);     // added inside a context: we can remove it later
resultt result = dp(); // solves 'a && b && c'
dp.pop();              // 'removes' c
dp.push();
dp.set_to_true(d);     // added inside a context: we can remove it later
resultt result = dp(); // solves 'a && b && d'

Example 2: solving under assumptions:

dp.set_to_true(a);     // added permanently
resultt result = dp(); // solves formula 'a'
h1 = dp.handle(c);
h2 = dp.handle(d)
dp.push({h1, h2});
resultt result = dp(); // solves formula 'a && c && d'
dp.pop();              // clear assumptions h1, h2
h1 = dp.handle(not_exprt(c)); // get negated handle for 'c'
dp.push({h1, h2});
resultt result = dp(); // solves formula 'a && !c && d'

Definition in file stack_decision_procedure.h.

Classes

Detailed Description