diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-20 14:49:55 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 14:49:55 -0600 |
| commit | 798524d033f69153d4bf6604e08c69a571771ae8 (patch) | |
| tree | d00e5a0f67a2b03f1cdbd289d3d3ae2ba7146c63 /src/api/cvc4cpp.h | |
| parent | 89420525dd8417f32446aa9cd9a18ecd211cc119 (diff) | |
Updates to API in preparation for using symbol manager for model (#5481)
printModel no longer makes sense if the list of declared symbols is managed outside the solver.
Also, mkConst needs a variant to distinguish a provided name of "" vs. a name that is not provided.
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index db57af121..eb55e4007 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2829,7 +2829,15 @@ class CVC4_PUBLIC Solver * @param symbol the name of the constant * @return the first-order constant */ - Term mkConst(Sort sort, const std::string& symbol = std::string()) const; + Term mkConst(Sort sort, const std::string& symbol) const; + /** + * Create (first-order) constant (0-arity function symbol), with a default + * symbol name. + * + * @param sort the sort of the constant + * @return the first-order constant + */ + Term mkConst(Sort sort) const; /** * Create a bound variable to be used in a binder (i.e. a quantifier, a @@ -3234,13 +3242,6 @@ class CVC4_PUBLIC Solver bool getAbduct(Term conj, Grammar& g, Term& output) const; /** - * Print the model of a satisfiable query to the given output stream. - * Requires to enable option 'produce-models'. - * @param out the output stream - */ - void printModel(std::ostream& out) const; - - /** * Block the current model. Can be called only if immediately preceded by a * SAT or INVALID query. * SMT-LIB: ( block-model ) |