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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* Utilities for initializing subsolvers (copies of SolverEngine) during
* solving.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H
#define CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H
#include <memory>
#include <vector>
#include "expr/node.h"
#include "smt/solver_engine.h"
namespace cvc5 {
namespace theory {
/**
* This function initializes the smt engine smte to check the satisfiability
* of the argument "query". It takes the logic and options of the current
* SMT engine in scope.
*
* Notice this method intentionally does not fully initialize smte. This means
* that the options of smte can still be modified after it is returned by
* this method.
*
* Notice that some aspects of subsolvers are not incoporated by this call.
* For example, the type of separation logic heaps is not set on smte, even
* if the current SMT engine has declared a separation logic heap.
*
* @param smte The smt engine pointer to initialize
* @param opts The options for the subsolver.
* @param logicInfo The logic info to set on the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
const Options& opts,
const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
/**
* Version that uses the options and logicInfo in an environment.
*/
void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
const Env& env,
bool needsTimeout = false,
unsigned long timeout = 0);
/**
* This returns the result of checking the satisfiability of formula query.
*
* If necessary, smte is initialized to the SMT engine that checked its
* satisfiability.
*/
Result checkWithSubsolver(std::unique_ptr<SolverEngine>& smte,
Node query,
const Options& opts,
const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
/**
* This returns the result of checking the satisfiability of formula query.
*
* In contrast to above, this is used if the user of this method is not
* concerned with the state of the SMT engine after the check.
*
* @param query The query to check
* @param opts The options for the subsolver
* @param logicInfo The logic info to set on the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
Result checkWithSubsolver(Node query,
const Options& opts,
const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
/**
* This returns the result of checking the satisfiability of formula query.
* Additionally, if the query is satisfiable, it adds the model values for vars
* into modelVars.
*
* @param query The query to check
* @param vars The variables we are interesting in getting a model for.
* @param modelVals A vector storing the model values of variables in vars.
* @param opts The options for the subsolver
* @param logicInfo The logic info to set on the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
Result checkWithSubsolver(Node query,
const std::vector<Node>& vars,
std::vector<Node>& modelVals,
const Options& opts,
const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
//--------------- utilities
/**
* Assuming smt has just been called to check-sat and returned "SAT", this
* method adds the model for d_vars to mvs.
*/
void getModelFromSubsolver(SolverEngine& smt,
const std::vector<Node>& vars,
std::vector<Node>& mvs);
/**
* Assuming smt has just been called to check-sat and returned "UNSAT", this
* method get the unsat core and adds it to uasserts.
*
* The assertions in the argument queryAsserts (which we are not interested
* in tracking in the unsat core) are excluded from uasserts.
* If one of the formulas in queryAsserts was in the unsat core, then this
* method returns true. Otherwise, this method returns false.
*/
bool getUnsatCoreFromSubsolver(SolverEngine& smt,
const std::unordered_set<Node>& queryAsserts,
std::vector<Node>& uasserts);
/** Same as above, without query asserts */
void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts);
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H */
|
