git.libre-soc.org Git - cvc5.git/commit

author	yoni206 <yoni206@users.noreply.github.com>
	Sat, 26 Jun 2021 02:42:43 +0000 (19:42 -0700)
committer	GitHub <noreply@github.com>
	Sat, 26 Jun 2021 02:42:43 +0000 (19:42 -0700)
commit	eefd31d2fe256bdee9a5c33105eced1a358bb378
tree	5b8d52bdfc288557bf6456ca315ad2862ab4669b	tree
parent	abd18eeb854047e13e38518c536afd16a1be448d	commit \| diff

pow2 -- final changes (#6800)

This commit adds the remaining changes for a working and integrated `pow2` solver.

In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.

The next steps are new rewrites and and more lemma schemas.

20 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/nl/ext_theory_callback.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/nl/pow2_solver.cpp		diff \| blob \| history
src/theory/arith/nl/strategy.cpp		diff \| blob \| history
src/theory/arith/nl/strategy.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/nl/pow2-native-0.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/pow2-native-1.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/pow2-native-2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/pow2-native-3.smt2	[new file with mode: 0644]	blob

RSS Atom