diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-01-20 07:28:29 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-20 09:28:29 -0600 |
commit | e2ec4e5401eba4ef63539ddb7c1f3a54301de4b1 (patch) | |
tree | d17d5a42599eec5699d646e2ffe3150771ff7aff /src/parser | |
parent | c8e8acd26b4bd5c47110b9448a74a45913b5518f (diff) |
SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)
This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.
More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 36703fd6d..0c67299ab 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -550,9 +550,12 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.areIntegersUsed()) { defineType("Int", d_solver->getIntegerSort(), true, true); addArithmeticOperators(); - addOperator(api::INTS_DIVISION, "div"); - addOperator(api::INTS_MODULUS, "mod"); - addOperator(api::ABS, "abs"); + if (!d_logic.isLinear()) + { + addOperator(api::INTS_DIVISION, "div"); + addOperator(api::INTS_MODULUS, "mod"); + addOperator(api::ABS, "abs"); + } addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible"); } |