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

2021-09-10	Mathias Preiner	bv: Use EnvObj::rewrite() and EnvObj::options() in...	commit \| commitdiff \| tree
2021-09-10	Mathias Preiner	bv: Use EnvObj::rewrite() and EnvObj::options() in...	commit \| commitdiff \| tree
2021-08-26	Mathias Preiner	int2bv: Fix conversion of signed bit-vector values...	commit \| commitdiff \| tree
2021-08-04	Mathias Preiner	syqi: Add debug information for dumping instantiations...	commit \| commitdiff \| tree
2021-08-02	Mathias Preiner	bv: Enable equality engine for bitblast-internal. ...	commit \| commitdiff \| tree
2021-07-27	Mathias Preiner	bv: Refactor getEqualityStatus and use for both bitblasting...	commit \| commitdiff \| tree
2021-07-27	Mathias Preiner	proof: Add eqrange expansion rule. (#6936)	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Disable bv-assert-input if proofs are enabled....	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Rename BBSimple to NodeBitblaster. (#6891)	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Rename lazy solver to layered solver. (#6889)	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Rename simple solver to bitblast-internal. (#6888)	commit \| commitdiff \| tree
2021-07-14	Mathias Preiner	Add missing space for check macro error messages. ...	commit \| commitdiff \| tree
2021-07-14	Mathias Preiner	bv: Add missing BV_EAGER_ATOM proof rule. (#6874)	commit \| commitdiff \| tree
2021-07-13	Mathias Preiner	bv: Simplify BV_BITBLAST_* proof rules. (#6871)	commit \| commitdiff \| tree
2021-07-13	Mathias Preiner	bv: Do not rewrite below BV leafs in BBProof's TConvProofGen...	commit \| commitdiff \| tree
2021-07-13	Mathias Preiner	bv: Expand bitblast proof steps in the proof post processor...	commit \| commitdiff \| tree
2021-07-03	Mathias Preiner	Add output tags -o, --output. (#6826)	commit \| commitdiff \| tree
2021-07-02	Mathias Preiner	Fix bv assert input reset assertions (#6820)	commit \| commitdiff \| tree
2021-06-30	Mathias Preiner	Use SAT context level for --bv-assert-input instead...	commit \| commitdiff \| tree
2021-06-29	Mathias Preiner	Fix statistics in AigBitblaster. (#6810)	commit \| commitdiff \| tree
2021-06-24	Mathias Preiner	cmake: Add new code coverage targets. (#6796)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Update to CaDiCaL 1.4.1. (#6780)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Fix model issues with --bitblast=eager. (#6753)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Move cnfConversionTime statistic to CnfStream. (#6769)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Make CaDiCaL a required dependency. (#6761)	commit \| commitdiff \| tree
2021-06-18	Mathias Preiner	Make CnfStream::toCNF iterative (#6757)	commit \| commitdiff \| tree
2021-06-10	Mathias Preiner	smtcomp: Change some BV configs for SQ and INC track...	commit \| commitdiff \| tree
2021-06-04	Mathias Preiner	bv: Enable bitblast solver by default. (#6660)	commit \| commitdiff \| tree
2021-05-20	Mathias Preiner	Update version of CaDiCaL. (#6583)	commit \| commitdiff \| tree
2021-05-19	Mathias Preiner	Correctly handle negated assertions for assumption...	commit \| commitdiff \| tree
2021-05-19	Mathias Preiner	bv: Add support for --bitblast=eager. (#6516)	commit \| commitdiff \| tree
2021-05-14	Mathias Preiner	bv: Assert input facts on user-level 0. (#6515)	commit \| commitdiff \| tree
2021-05-13	Mathias Preiner	Add std::hash overloads for Node, TNode and TypeNode...	commit \| commitdiff \| tree
2021-05-06	Mathias Preiner	Update README.md and remove last CVC4 references. ...	commit \| commitdiff \| tree
2021-05-04	Mathias Preiner	cmake: Fix ninja build. (#6481)	commit \| commitdiff \| tree
2021-04-30	Mathias Preiner	bv: Refactor ppAssert and move to TheoryBV. (#6470)	commit \| commitdiff \| tree
2021-04-24	Mathias Preiner	Add assumption-based unsat cores. (#6427)	commit \| commitdiff \| tree
2021-04-22	Mathias Preiner	cmake: Do not require --auto-download for already downloaded...	commit \| commitdiff \| tree
2021-04-21	Mathias Preiner	Goodbye CVC4, hello cvc5! (#6371)	commit \| commitdiff \| tree
2021-04-21	Mathias Preiner	cmake: Add optional module name argument for check_python_mo...	commit \| commitdiff \| tree
2021-04-16	Mathias Preiner	cmake: Build object libraries for base and context...	commit \| commitdiff \| tree
2021-04-15	Mathias Preiner	Build support library from base and context. (#6368)	commit \| commitdiff \| tree
2021-04-13	Mathias Preiner	ci: Use CVC5_REGRESSION_ARGS. (#6347)	commit \| commitdiff \| tree
2021-04-07	Mathias Preiner	cmake: Do not always regenerate cvc4kinds.{pxi,pxd...	commit \| commitdiff \| tree
2021-04-06	Mathias Preiner	cmake: Add helper to check if a given Python module...	commit \| commitdiff \| tree
2021-04-06	Mathias Preiner	genkinds: Do not use relative paths to find src directory...	commit \| commitdiff \| tree
2021-04-06	Mathias Preiner	parsekinds: Remove DEFAULT_HEADER. (#6294)	commit \| commitdiff \| tree
2021-04-02	Mathias Preiner	cmake: Do not link against main object library. (#6269)	commit \| commitdiff \| tree
2021-03-25	Mathias Preiner	Do not use Configuration class in API black tests....	commit \| commitdiff \| tree
2021-03-16	Mathias Preiner	ci: Enable checking of proofs + unsat cores. (#6088)	commit \| commitdiff \| tree
2021-03-16	Mathias Preiner	cmake: Generate cvc4_export.h and set visibility to...	commit \| commitdiff \| tree
2021-03-12	Mathias Preiner	cmake: Remove install rules for old API headers. (...	commit \| commitdiff \| tree
2021-03-12	Mathias Preiner	ci: Replace debug builds with assertion enabled production...	commit \| commitdiff \| tree
2021-03-11	Mathias Preiner	Fix compile warnings when compiling with GLPK. (#6115)	commit \| commitdiff \| tree
2021-03-11	Mathias Preiner	Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)	commit \| commitdiff \| tree
2021-03-11	Mathias Preiner	Add GitHub action to automatically update approved...	commit \| commitdiff \| tree
2021-03-10	Mathias Preiner	Use Assert instead of assert. (#6095)	commit \| commitdiff \| tree
2021-03-10	Mathias Preiner	cmake: Fix optimization level for debug builds. (#6097)	commit \| commitdiff \| tree
2021-03-10	Mathias Preiner	test: Fix missing std::. (#6096)	commit \| commitdiff \| tree
2021-03-08	Mathias Preiner	contrib: Do not use HOST env variable for cross-compilation...	commit \| commitdiff \| tree
2021-03-06	Mathias Preiner	Remove partial UDIV/UREM operators. (#6069)	commit \| commitdiff \| tree
2021-03-06	Mathias Preiner	Remove SMT-LIB 2.5 and 2.0 support. (#6068)	commit \| commitdiff \| tree
2021-03-02	Mathias Preiner	Remove non-ASCII characters from source files. (#6039)	commit \| commitdiff \| tree
2021-03-02	Mathias Preiner	Add aarch64 (ARM64) cross-compile support. (#6033)	commit \| commitdiff \| tree
2021-03-02	Mathias Preiner	Fix nightly errors. (#6034)	commit \| commitdiff \| tree
2021-03-01	Mathias Preiner	Make -Werror optional but enable it for CI. (#6032)	commit \| commitdiff \| tree
2021-02-26	Mathias Preiner	Fix -Werror issues with clang and use clang for debug...	commit \| commitdiff \| tree
2021-02-25	Mathias Preiner	Enable -Werror. (#5969)	commit \| commitdiff \| tree
2021-02-23	Mathias Preiner	Switch to C++17. (#5959)	commit \| commitdiff \| tree
2021-02-17	Mathias Preiner	Add bit-level propagation support to BV bitblast solver...	commit \| commitdiff \| tree
2021-02-13	Mathias Preiner	Properly set up equality engine for BV bitblast solver...	commit \| commitdiff \| tree
2021-02-09	Mathias Preiner	cmake: Make Python3 default and improve toml error...	commit \| commitdiff \| tree
2021-02-03	Mathias Preiner	Add BV solver bitblast. (#5851)	commit \| commitdiff \| tree
2020-12-08	Mathias Preiner	Add support for BV proofs with the simple bitblasting...	commit \| commitdiff \| tree
2020-12-08	Mathias Preiner	Disable algebraic BV subtheory by default and make...	commit \| commitdiff \| tree
2020-12-04	Mathias Preiner	update-copyright: Preserve file permissions. (#5597)	commit \| commitdiff \| tree
2020-11-18	Mathias Preiner	Add -> operator overload for cd* iterators. (#5464)	commit \| commitdiff \| tree
2020-11-18	Mathias Preiner	ci: Simplify Python dependency installs for Linux and...	commit \| commitdiff \| tree
2020-10-27	Mathias Preiner	run_regression: Add --skip-timeout option, lower timeout...	commit \| commitdiff \| tree
2020-10-11	Mathias Preiner	SyGuS instantiation modes (#5228)	commit \| commitdiff \| tree
2020-10-09	Mathias Preiner	Remove deprecated add-path commands and use $GITHUB_PATH...	commit \| commitdiff \| tree
2020-10-03	Mathias Preiner	Fix CI builds and add cancel workflow.	commit \| commitdiff \| tree
2020-10-01	Mathias Preiner	Add additional ground terms to SyGuS instantiation...	commit \| commitdiff \| tree
2020-10-01	Mathias Preiner	Add GH action to cancel previous pending/running CI...	commit \| commitdiff \| tree
2020-09-22	Mathias Preiner	Add simple BV solver (#5065)	commit \| commitdiff \| tree
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	commit \| commitdiff \| tree
2020-09-08	Mathias Preiner	Fix printing of fp values. (#5041)	commit \| commitdiff \| tree
2020-09-04	Mathias Preiner	Split lazy bit-vector solver from TheoryBV (#5009)	commit \| commitdiff \| tree
2020-08-29	Mathias Preiner	New C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in...	commit \| commitdiff \| tree
2020-08-24	Mathias Preiner	Increase regress level to 2 for production build. ...	commit \| commitdiff \| tree
2020-08-04	Mathias Preiner	Add documentation and build instructions for recompilation...	commit \| commitdiff \| tree
2020-07-08	Mathias Preiner	Add getName() method to options. (#4704)	commit \| commitdiff \| tree
2020-06-30	Mathias Preiner	Fix GMP compilation for win64. (#4675)	commit \| commitdiff \| tree
2020-06-30	Mathias Preiner	contrib: Update to GMP 6.2.0, compile static and shared...	commit \| commitdiff \| tree
2020-06-23	Mathias Preiner	Add support for eqrange predicate (#4562)	commit \| commitdiff \| tree
2020-06-03	Mathias Preiner	Fix normalization of author names in contrib/get-authors...	commit \| commitdiff \| tree
2020-05-26	Mathias Preiner	Fix mismatched iterators (CID 1493892). (#4531)	commit \| commitdiff \| tree
2020-05-26	Mathias Preiner	Update to CaDiCaL version 1.2.1. (#4530)	commit \| commitdiff \| tree
2020-04-27	Mathias Preiner	Fix examples instructions in INSTALL.md. (#4397)	commit \| commitdiff \| tree
2020-04-17	Mathias Preiner	antlr: Use relative path in ANTLR script. (#4324)	commit \| commitdiff \| tree
next

RSS Atom