projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dd31ac0) | patch
pow2: Adding monotonicity lemma (#6793)
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 25 Jun 2021 03:09:06 +0000 (20:09 -0700)
committerGitHub <noreply@github.com>
Fri, 25 Jun 2021 03:09:06 +0000 (22:09 -0500)
commitabd18eeb854047e13e38518c536afd16a1be448d
treee12f69826feb922dc80f228ecbb78276ee3613a9tree
parentdd31ac04ed448358da613ab97a2a929df8cf8fd5commit | diff
pow2: Adding monotonicity lemma  (#6793)

We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver.
Additionally, some renaming of variables is introduced for better clarity.
src/theory/arith/nl/pow2_solver.cpp diff | blob | history
src/theory/arith/nl/pow2_solver.h diff | blob | history
src/theory/inference_id.h diff | blob | history