projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4d303b5) | patch
Eliminate partial operators in sygus grammar normalization (#2323)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 17 Aug 2018 07:48:22 +0000 (02:48 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Fri, 17 Aug 2018 07:48:22 +0000 (00:48 -0700)
commit29ae7d5ec0a73b90529e2200d948e6f4051099f1
treea9dcb7074a2e79b35e17f2c4483638cf91ea1093tree
parent4d303b5e6de8a3b963357a3c0238ffe81d36f766commit | diff
 Eliminate partial operators in sygus grammar normalization (#2323)

This corrects a bug that was introduced in #2266 (the hack removed there was necessary).

This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.

This also enables total semantics for BV div-by-zero for sygus.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress1/sygus/bvudiv-by-2.sy [new file with mode: 0644] blob