diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-10 07:43:19 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-10 07:43:19 -0600 |
| commit | c2757f0440c5d5b841e05c60d1fd93dc9ee3763a (patch) | |
| tree | dde6e588873a20c5bb9edf28f383f2eb00c39eb5 /src/theory/smt_engine_subsolver.h | |
| parent | 0df0954069d56e3323a225ffa72c5913d0333ac2 (diff) | |
Add proper support for the declare-heap command for separation logic (#5405)
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.
This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.
Fixes #5343, fixes #4926.
Work towards CVC4/cvc4-wishues#22.
Diffstat (limited to 'src/theory/smt_engine_subsolver.h')
| -rw-r--r-- | src/theory/smt_engine_subsolver.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index d34729dec..f68900ccc 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -31,7 +31,16 @@ namespace theory { /** * This function initializes the smt engine smte to check the satisfiability - * of the argument "query". + * 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 needsTimeout Whether we would like to set a timeout |