projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Move ownership of theory preprocessor to TheoryProxy (#5690)
[cvc5.git]
/
src
/
preprocessing
/
2020-12-21
Andrew Reynolds
Move ownership of theory preprocessor to TheoryProxy...
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Simplify preprocessing (#5647)
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Move ownership of term formula removal to theory prepro...
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Consolidate basic sygus utilities regarding sygus conje...
tree
|
commitdiff
2020-12-09
Aina Niemetz
ite_utilities: Fix infinite loop in compressTerm. ...
tree
|
commitdiff
2020-12-08
yoni206
bv-to-int: Expand definitions of bvudiv and bvurem...
tree
|
commitdiff
2020-12-07
makaimann
Add bitwise refinement mode for IAND (#5328)
tree
|
commitdiff
2020-12-04
Alex Ozdemir
Use NodeDfsIterable for makeBinary (#5595)
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Minor cleanup of SmtEngine (#5450)
tree
|
commitdiff
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-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDPro...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Updates to assertions pipeline and preproce...
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-29
Andrew Reynolds
(proof-new) Fixes for preprocess proof generator and...
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
Abdalrhman Mohamed
Dump commands in internal code using command printing...
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-12
Andrew Reynolds
(proof-new) Add SMT proof manager (#5054)
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-18
Andrew Reynolds
(proof-new) Proof recording for assertions pipeline...
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-17
Aina Niemetz
SmtEngine: Convert members owned by SmtEngine to unique...
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
Aina Niemetz
Fix issue with reset-assertions. (#3988)
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
Aina Niemetz
Move ownership of DecisionEngine into PropEngine. ...
tree
|
commitdiff
2020-03-05
Aina Niemetz
Revert "Move ownership of DecisionEngine into PropEngin...
tree
|
commitdiff
2020-03-05
Andrew Reynolds
Move ownership of DecisionEngine into PropEngine. ...
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
next