diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-15 15:44:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-15 22:44:52 +0000 |
| commit | 4ca14e808d788ef9570dda1188645783c6a11e70 (patch) | |
| tree | da87ecaf3a9aa5d789eebda94923829652fff935 /src/api | |
| parent | 3fb45e059eff665ed5aaf23915f3434db1e60299 (diff) | |
pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736)
This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 2ec190360..2c5d2873e 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ IAND, + /** + * Operator for raising 2 to a non-negative integer power + * + * Create with: + * - `Solver::mkOp(Kind kind) const` + * + + * Parameters: + * - 1: Op of kind IAND + * - 2: Integer term + * + * Create with: + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` + */ + POW2, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, |