diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 51eed32b2..3ef190447 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -497,6 +497,17 @@ class CVC4_EXPORT SmtEngine /*------------------------- end of sygus commands ------------------------*/ /** + * Declare pool whose initial value is the terms in initValue. A pool is + * a variable of type (Set T) that is used in quantifier annotations and does + * not occur in constraints. + * + * @param p The pool to declare, which should be a variable of type (Set T) + * for some type T. + * @param initValue The initial value of p, which should be a vector of terms + * of type T. + */ + void declarePool(const Node& p, const std::vector<Node>& initValue); + /** * Simplify a formula without doing "much" work. Does not involve * the SAT Engine in the simplification, but uses the current * definitions, assertions, and the current partial model, if one |