diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-06 09:37:48 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-06 09:37:48 -0800 |
commit | aa3807f28b47abaa26573439f4dafca0258e4b6b (patch) | |
tree | ec265cc8ff82df819d8c6acf49902f2be9317b1b /src/theory/arith/theory_arith_private.h | |
parent | 9bf97a2ac3c923d08cce93ca7eda4360b19dfdec (diff) | |
parent | e2d714a0839fb80d9a40e9b6fdd8a6fe325a1664 (diff) |
Merge branch 'master' into cleanup_outputcleanup_output
Diffstat (limited to 'src/theory/arith/theory_arith_private.h')
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 46 |
1 files changed, 32 insertions, 14 deletions
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 23712016d..af0012304 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -829,25 +829,43 @@ private: Statistics d_statistics; + enum ArithSkolemId + { + arith_skolem_div_by_zero, + arith_skolem_int_div_by_zero, + arith_skolem_mod_by_zero, + }; /** - * Function symbol used to implement uninterpreted division-by-zero - * semantics. Needed to deal with partial division function ("/"). + * Function symbols used to implement: + * (1) Uninterpreted division-by-zero semantics. Needed to deal with partial + * division function ("/"), + * (2) Uninterpreted int-division-by-zero semantics. Needed to deal with + * partial function "div", + * (3) Uninterpreted mod-zero semantics. Needed to deal with partial + * function "mod". + * + * If the option arithNoPartialFun() is enabled, then the range of this map + * stores Skolem constants instead of Skolem functions, meaning that the + * function-ness of e.g. division by zero is ignored. */ - Node d_divByZero; - - /** - * Function symbol used to implement uninterpreted - * int-division-by-zero semantics. Needed to deal with partial - * function "div". + std::map<ArithSkolemId, Node> d_arith_skolem; + /** get arithmetic skolem + * + * Returns the Skolem in the above map for the given id, creating it if it + * does not already exist. If a Skolem function is created, the logic is + * widened to include UF. */ - Node d_intDivByZero; - - /** - * Function symbol used to implement uninterpreted mod-zero - * semantics. Needed to deal with partial function "mod". + Node getArithSkolem(LogicRequest& logicRequest, ArithSkolemId asi); + /** get arithmetic skolem application + * + * By default, this returns the term f( n ), where f is the Skolem function + * for the identifier asi. + * + * If the option arithNoPartialFun is enabled, this returns f, where f is + * the Skolem constant for the identifier asi. */ - Node d_modZero; + Node getArithSkolemApp(LogicRequest& logicRequest, Node n, ArithSkolemId asi); /** * Maps for Skolems for to-integer, real/integer div-by-k, and inverse |