projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
(proof-new) Proofs for non-clausal simplification (#5409)
[cvc5.git]
/
src
/
preprocessing
/
passes
/
2020-11-14
Andrew Reynolds
(proof-new) Proofs for non-clausal simplification ...
tree
|
commitdiff
2020-10-22
Andrew Reynolds
(proof-new) Make theory preprocessor user-context depen...
tree
|
commitdiff
2020-10-21
Gereon Kremer
(proof-new) Make circuit propagator proof producing...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Update preprocessing pass context for proof...
tree
|
commitdiff
2020-10-16
yoni206
bv2int: caching introduced terms (#5283)
tree
|
commitdiff
2020-10-14
yoni206
bv2int: rewritings and unsat cores (#5263)
tree
|
commitdiff
2020-10-13
yoni206
bv2int: improving bvand tables (#5235)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
tree
|
commitdiff
2020-10-10
yoni206
bv2int: bvand translation code move (#5227)
tree
|
commitdiff
2020-10-09
Andres Noetzli
reset-assertions: Remove all non-global symbols in...
tree
|
commitdiff
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
tree
|
commitdiff
2020-10-01
Andrew Reynolds
(proof-new) Preprocessing passes use proper interfaces...
tree
|
commitdiff
2020-09-24
Andrew Reynolds
Function definition fmf preprocessing pass (#5064)
tree
|
commitdiff
2020-09-23
yoni206
bv2int: new options for bvand translation (#5096)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-18
yoni206
bv2int: quantifiers support (#5080)
tree
|
commitdiff
2020-09-16
yoni206
bv2int: support models in tests (#5068)
tree
|
commitdiff
2020-09-14
yoni206
bv2int: simpler translation for plus and times (#5055)
tree
|
commitdiff
2020-09-14
Andres Noetzli
Fix type for Windows build (#5062)
tree
|
commitdiff
2020-09-10
yoni206
bv2int: refactoring the main translation loop (#5051)
tree
|
commitdiff
2020-09-10
yoni206
bv2int: improvement in lazy failures (#5020)
tree
|
commitdiff
2020-09-03
yoni206
Changing the handled operators in bv2int preprocessing...
tree
|
commitdiff
2020-09-03
Andrew Reynolds
(proof-new) Support proofs of quantifier instantiation...
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-31
Gereon Kremer
Fix --ackermann in the presence on syntactically differ...
tree
|
commitdiff
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Updates not related to creation for eliminating Expr...
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Split dump manager from SmtEngine (#4824)
tree
|
commitdiff
2020-07-27
Andrew Reynolds
(proof-new) Proof production for term formula removal...
tree
|
commitdiff
2020-07-15
Andres Noetzli
Use Nodes for SmtEngine assertions (#4752)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Minor refactoring of subsolver initialization (#4731)
tree
|
commitdiff
2020-07-11
yoni206
Changing bv_to_int options (#4721)
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-06-24
Andres Noetzli
[unconstrained] Fix gathering of visited-once vars...
tree
|
commitdiff
2020-06-20
Alex Ozdemir
Use traversal iterators in IntToBv (#4169)
tree
|
commitdiff
2020-06-19
yoni206
Bv to int elimination bugfix (#4435)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifi...
tree
|
commitdiff
2020-05-21
Andrew Reynolds
Fix missing check for cardinality one in unconstrained...
tree
|
commitdiff
2020-05-05
Andrew Reynolds
Always introduce fresh variable for unconstrained APPLY...
tree
|
commitdiff
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
tree
|
commitdiff
2020-04-10
Andrew Reynolds
Towards proper use of resource managers (#4233)
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
tree
|
commitdiff
2020-03-25
Ahmed Irfan
bv2int : linear mult opt (#4142)
tree
|
commitdiff
2020-03-24
yoni206
Int2BV fail on demand (#4079)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Fix variable shadowing issue in sygus-inference (#4121)
tree
|
commitdiff
2020-03-19
yoni206
Bv2int fail on demand
tree
|
commitdiff
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Do not allow quantifiers over real variables in real...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Remove experimental symmetry breaker (#4005)
tree
|
commitdiff
2020-03-11
Aina Niemetz
bv-gauss-elim: Fix handling of inconsistent case. ...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix real to int for parameterized kinds (#4016)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix real as int for incremental (#3979)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Do not traverse quantifiers in nl ext purify (#3982)
tree
|
commitdiff
2020-03-10
Alex Ozdemir
Document bv-to-bool recursion (#3848)
tree
|
commitdiff
2020-03-10
makaimann
Enhancement: make the bool-to-bv pass more robust and...
tree
|
commitdiff
2020-03-06
Andres Noetzli
Remove --apply-to-const preprocessing pass (#3919)
tree
|
commitdiff
2020-03-05
Andrew Reynolds
Fix issues with real to int (#3918)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-25
yoni206
bv_to_int preprocessing pass
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Eliminate Expr-level calls in TypeNode (#3562)
tree
|
commitdiff
2019-12-02
makaimann
OpTerm Refactor: Allow retrieving OpTerm used to create...
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
tree
|
commitdiff
2019-11-27
Andrew Reynolds
Fix sygus inference for choice functions introduced...
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-18
Andrew Reynolds
Use standard sygus interface for abduction and rewrite...
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
tree
|
commitdiff
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
tree
|
commitdiff
2019-09-27
Andres Noetzli
Make substitution index context-independent (#2474)
tree
|
commitdiff
2019-08-20
Andrew Reynolds
Fixes for sygus inference on quantifier free problems...
tree
|
commitdiff
2019-08-02
Mathias Preiner
Fix BVGauss unit tests. (#3142)
tree
|
commitdiff
2019-08-01
Andrew Reynolds
Move some generic utilities out of quantifiers (#3139)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
tree
|
commitdiff
2019-07-26
Andrew Reynolds
Input user grammar in sygus abduct (#3119)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Add higher-order elimination preprocessing pass (#2865)
tree
|
commitdiff
2019-04-25
Aina Niemetz
Fix compiler warning. (#2975)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-17
Andrew Reynolds
More use of isClosure (#2959)
tree
|
commitdiff
2019-04-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-20
Andrew Reynolds
Sygus abduction feature (#2744)
tree
|
commitdiff
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
tree
|
commitdiff
2018-10-12
Andrew Reynolds
Improvements to rewrite rules from inputs (#2625)
tree
|
commitdiff
2018-10-11
Andrew Reynolds
Synthesize rewrite rules from inputs (#2608)
tree
|
commitdiff
2018-10-02
Andres Noetzli
Make registration of preprocessing passes explicit...
tree
|
commitdiff
2018-10-01
Andres Noetzli
Refactor preprocessing pass registration (#2468)
tree
|
commitdiff
2018-09-18
Andrew Reynolds
Improvements and fixes for symmetry detection and break...
tree
|
commitdiff
2018-09-15
Andres Noetzli
Refactor how assertions are added to decision engine...
tree
|
commitdiff
2018-09-11
yoni206
Avoid calling size() every iteration (#2450)
tree
|
commitdiff
2018-09-11
Andrew Reynolds
Fix global negate (#2449)
tree
|
commitdiff
2018-09-11
Aina Niemetz
Refactor non-clausal simplify preprocessing pass. ...
tree
|
commitdiff
next