blob: c52614f744119f8545fcd32a09b3d297ae3c02c2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
/********************* */
/*! \file interpolation_solver.h
** \verbatim
** Top contributors (to current version):
** Ying Sheng, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The solver for interpolation queries
**/
#include "cvc4_private.h"
#ifndef CVC4__SMT__INTERPOLATION_SOLVER_H
#define CVC4__SMT__INTERPOLATION_SOLVER_H
#include "expr/node.h"
#include "expr/type_node.h"
namespace CVC4 {
class SmtEngine;
namespace smt {
/**
* A solver for interpolation queries.
*
* This class is responsible for responding to get-interpol commands. It spawns
* a subsolver SmtEngine for a sygus conjecture that captures the interpolation
* query, and implements supporting utility methods such as checkInterpol.
*/
class InterpolationSolver
{
public:
InterpolationSolver(SmtEngine* parent);
~InterpolationSolver();
/**
* This method asks this SMT engine to find an interpolant with respect to
* the current assertion stack (call it A) and the conjecture (call it B). If
* this method returns true, then interpolant is set to a formula I such that
* A ^ ~I and I ^ ~B are both unsatisfiable.
*
* @param conj The conjecture of the interpolation problem.
* @param grammarType A sygus datatype type that encodes the syntax
* restrictions on the shape of possible solutions.
* @param interpol This argument is updated to contain the solution to the
* interpolation problem.
*
* This method invokes a separate copy of the SMT engine for solving the
* corresponding sygus problem for generating such a solution.
*/
bool getInterpol(const Node& conj,
const TypeNode& grammarType,
Node& interpol);
/**
* Same as above, but without user-provided grammar restrictions. A default
* grammar is chosen internally using the sygus grammar constructor utility.
*/
bool getInterpol(const Node& conj, Node& interpol);
/**
* Check that a solution to an interpolation problem is indeed a solution.
*
* The check is made by determining that the assertions imply the solution of
* the interpolation problem (interpol), and the solution implies the goal
* (conj). If these criteria are not met, an internal error is thrown.
*/
void checkInterpol(Node interpol,
const std::vector<Node>& easserts,
const Node& conj);
private:
/** The parent SMT engine */
SmtEngine* d_parent;
};
} // namespace smt
} // namespace CVC4
#endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */
|
