diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-06-23 09:55:01 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-23 09:55:01 -0700 |
| commit | 0539b0342b46e9fb96467a23f703bf2317692bb2 (patch) | |
| tree | 1c2d54f7791ee472daa40efc63ce88e13b9e4cc8 /src/parser | |
| parent | bea30aa5dd6b36fc5a206c4742abadf8c3fab5c1 (diff) | |
Add support for eqrange predicate (#4562)
This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bf4e489bb..a7eb218af 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -642,6 +642,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { addOperator(api::SELECT, "select"); addOperator(api::STORE, "store"); + addOperator(api::EQ_RANGE, "eqrange"); } if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { @@ -1824,6 +1825,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } + if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true") + { + parseError( + "eqrange predicate requires option --arrays-exp to be enabled."); + } api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; |