projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)
2022-02-02
Andrew Reynolds
Fix rewrite for eliminating constant factors of PI...
commit
|
commitdiff
|
tree
2022-02-02
Andrew Reynolds
Fix invalid rewrite involving iand (#8026)
commit
|
commitdiff
|
tree
2022-02-02
Andrew Reynolds
Fix printing of re.loop as an operator in LFSC (#8029)
commit
|
commitdiff
|
tree
2022-02-02
Andrew Reynolds
Make LFSC side condition for concat unify robust to...
commit
|
commitdiff
|
tree
2022-02-02
Andrew Reynolds
Add missing null terminators for regexp (#8027)
commit
|
commitdiff
|
tree
2022-02-02
Andrew Reynolds
Remove more static calls to rewrite (#8025)
commit
|
commitdiff
|
tree
2022-02-02
Andrew Reynolds
Extend proof step buffer to optionally ensure unique...
commit
|
commitdiff
|
tree
2022-02-01
Andrew Reynolds
Add variant of get-difficulty for full effort lemmas...
commit
|
commitdiff
|
tree
2022-01-27
Andrew Reynolds
Document substitute in API (#7904)
commit
|
commitdiff
|
tree
2022-01-26
Andrew Reynolds
Initial refactoring of conflict-based instantiation...
commit
|
commitdiff
|
tree
2022-01-26
Andrew Reynolds
More fixes and improvements for query generator (#7988)
commit
|
commitdiff
|
tree
2022-01-25
Andrew Reynolds
Add output -o post-asserts (#7987)
commit
|
commitdiff
|
tree
2022-01-25
Andrew Reynolds
Fixes and improvements to sygus satisfiable query generation...
commit
|
commitdiff
|
tree
2022-01-21
Andrew Reynolds
Ref count nodes in trigger trie (#7972)
commit
|
commitdiff
|
tree
2022-01-21
Andrew Reynolds
Fix trivial explantions in sequences array solver ...
commit
|
commitdiff
|
tree
2022-01-20
Andrew Reynolds
Fix proofs for trivial cases of datatypes tester merge...
commit
|
commitdiff
|
tree
2022-01-18
Andrew Reynolds
Distinguish purification types for strings proof reconstruct...
commit
|
commitdiff
|
tree
2022-01-18
Andrew Reynolds
Print original form for substitutions and learned literals...
commit
|
commitdiff
|
tree
2022-01-17
Andrew Reynolds
Refactor options related to rewriting and symmetry...
commit
|
commitdiff
|
tree
2022-01-15
Andrew Reynolds
Add inverse inference for update-over-concat (#7954)
commit
|
commitdiff
|
tree
2022-01-14
Andrew Reynolds
Improve names for sygus enumeration option (#7945)
commit
|
commitdiff
|
tree
2022-01-14
Andrew Reynolds
Clean enumerative instantiation options (#7947)
commit
|
commitdiff
|
tree
2022-01-14
Andrew Reynolds
Implement -o subs to show learned top-level substitutions...
commit
|
commitdiff
|
tree
2022-01-14
Andrew Reynolds
Fix learned rewrite pass for non-real equalties (#7936)
commit
|
commitdiff
|
tree
2022-01-14
Andrew Reynolds
Weaken assertion in relevance manager (#7943)
commit
|
commitdiff
|
tree
2022-01-13
Andrew Reynolds
Fix bug in evaluator for division by zero (#7942)
commit
|
commitdiff
|
tree
2022-01-12
Andrew Reynolds
Add -o learned-lits to output learned literals (#7934)
commit
|
commitdiff
|
tree
2022-01-12
Andrew Reynolds
Ensure configuration of shared selectors is consistent...
commit
|
commitdiff
|
tree
2022-01-12
Andrew Reynolds
Always use partial function for sqrt (#7926)
commit
|
commitdiff
|
tree
2022-01-12
Andrew Reynolds
Eliminate use of subtyping from results of quantifier...
commit
|
commitdiff
|
tree
2022-01-11
Andrew Reynolds
Tighten policy for unsat cores in sygus core connective...
commit
|
commitdiff
|
tree
2022-01-11
Andrew Reynolds
Guard use of unsat core mode pp-only (#7899)
commit
|
commitdiff
|
tree
2022-01-10
Andrew Reynolds
Fix internal type error when printing lambdas with...
commit
|
commitdiff
|
tree
2022-01-10
Andrew Reynolds
Check arity in Sort::instantiate (#7897)
commit
|
commitdiff
|
tree
2022-01-07
Andrew Reynolds
Fix eager string preprocessing in incremental mode...
commit
|
commitdiff
|
tree
2022-01-07
Andrew Reynolds
Add regressions for array sequence solver (#7874)
commit
|
commitdiff
|
tree
2022-01-06
Andrew Reynolds
Make alpha equivalence user context dependent (#7889)
commit
|
commitdiff
|
tree
2022-01-06
Andrew Reynolds
Disallow separation logic in incremental mode (#7888)
commit
|
commitdiff
|
tree
2022-01-06
Andrew Reynolds
Fix non-idempotent rewrite in arrays (#7887)
commit
|
commitdiff
|
tree
2022-01-06
Andrew Reynolds
Minor cleaning of non-clausal simplification (#7886)
commit
|
commitdiff
|
tree
2022-01-05
Andrew Reynolds
Properly parse arithmetic values (#7876)
commit
|
commitdiff
|
tree
2022-01-05
Andrew Reynolds
Track input list for atoms in difficulty manager (...
commit
|
commitdiff
|
tree
2022-01-04
Andrew Reynolds
Fix proofs for datatype purify (#7841)
commit
|
commitdiff
|
tree
2022-01-04
Andrew Reynolds
Change default granularity of proofs to macro (#7855)
commit
|
commitdiff
|
tree
2022-01-04
Andrew Reynolds
Add utility expr::isBooleanConnective (#7869)
commit
|
commitdiff
|
tree
2022-01-04
Andrew Reynolds
Remove spurious call to applySubs (#7871)
commit
|
commitdiff
|
tree
2022-01-04
Andrew Reynolds
Remove unused shutdown infrastructure (#7872)
commit
|
commitdiff
|
tree
2022-01-04
Andrew Reynolds
Fix int blaster (#7856)
commit
|
commitdiff
|
tree
2022-01-03
Andrew Reynolds
Update quantifiers compute elim symbols to be iterative...
commit
|
commitdiff
|
tree
2021-12-22
Andrew Reynolds
Remove most uses of mkRationalNode (#7854)
commit
|
commitdiff
|
tree
2021-12-22
Andrew Reynolds
Add support for incremental + interpolants (#7853)
commit
|
commitdiff
|
tree
2021-12-21
Andrew Reynolds
Support get-abduct-next (#7850)
commit
|
commitdiff
|
tree
2021-12-21
Andrew Reynolds
Eliminate remaining calls to callExtendedRewrite (...
commit
|
commitdiff
|
tree
2021-12-21
Andrew Reynolds
Connect sequences array solver to strategy in theory...
commit
|
commitdiff
|
tree
2021-12-20
Andrew Reynolds
Eliminating some uses of const rational in arithmetic...
commit
|
commitdiff
|
tree
2021-12-20
Andrew Reynolds
Updates to LFSC signatures (#7840)
commit
|
commitdiff
|
tree
2021-12-20
Andrew Reynolds
Allow SyGuS subsolver to be reused in incremental mode...
commit
|
commitdiff
|
tree
2021-12-17
Andrew Reynolds
Simplify contrib/get-lfsc-checker and use cvc5 repo...
commit
|
commitdiff
|
tree
2021-12-17
Andrew Reynolds
Minor refactoring of API for eliminating arithmetic...
commit
|
commitdiff
|
tree
2021-12-17
Andrew Reynolds
Refactoring initialization of proofs (#7834)
commit
|
commitdiff
|
tree
2021-12-17
Andrew Reynolds
Get getRealOrIntegerValueSign to the API (#7832)
commit
|
commitdiff
|
tree
2021-12-17
Andrew Reynolds
Implement model construction for the array extension...
commit
|
commitdiff
|
tree
2021-12-17
Andrew Reynolds
Eliminate more uses of CONST_RATIONAL (#7816)
commit
|
commitdiff
|
tree
2021-12-16
Andrew Reynolds
Eliminate most static calls to rewrite in quantifiers...
commit
|
commitdiff
|
tree
2021-12-16
Andrew Reynolds
Fix get-model when sort constructors are present (...
commit
|
commitdiff
|
tree
2021-12-16
Andrew Reynolds
Minor fix for print benchmark. (#7821)
commit
|
commitdiff
|
tree
2021-12-15
Andrew Reynolds
Ensure match terms are exhaustive in its type rule...
commit
|
commitdiff
|
tree
2021-12-15
Andrew Reynolds
Add trace to see inferences in final proof (#7813)
commit
|
commitdiff
|
tree
2021-12-14
Andrew Reynolds
Eliminate static calls to rewrite in strings (#7803)
commit
|
commitdiff
|
tree
2021-12-14
Andrew Reynolds
Connecting the core array solver in strings (#7800)
commit
|
commitdiff
|
tree
2021-12-14
Andrew Reynolds
Minor fix for sygus unsat query generator (#7811)
commit
|
commitdiff
|
tree
2021-12-14
Andrew Reynolds
Throw exception for getting value of non-well-founded...
commit
|
commitdiff
|
tree
2021-12-14
Andrew Reynolds
Eliminate use of rewrite, CONST_RATIONAL in ArithMSum...
commit
|
commitdiff
|
tree
2021-12-13
Andrew Reynolds
Distinguishing more uses of CONST_RATIONAL (#7802)
commit
|
commitdiff
|
tree
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
commit
|
commitdiff
|
tree
2021-12-13
Andrew Reynolds
Fixes and additions for API for parametric datatypes...
commit
|
commitdiff
|
tree
2021-12-10
Andrew Reynolds
Refactor and fixes related to getSpecializedConstructorTerm...
commit
|
commitdiff
|
tree
2021-12-09
Andrew Reynolds
Consider polarity in relevance manager (#7768)
commit
|
commitdiff
|
tree
2021-12-09
Andrew Reynolds
Remove a few static access to options in proof code...
commit
|
commitdiff
|
tree
2021-12-09
Andrew Reynolds
Do not make SyGuS subsolver in unsat state after solving...
commit
|
commitdiff
|
tree
2021-12-08
Andrew Reynolds
Return bool for lemmaTheoryInference (#7773)
commit
|
commitdiff
|
tree
2021-12-08
Andrew Reynolds
Make several regressions faster (#7769)
commit
|
commitdiff
|
tree
2021-12-08
Andrew Reynolds
Fix type rule for datatype updater for parametric sorts...
commit
|
commitdiff
|
tree
2021-12-07
Andrew Reynolds
Add proof annotation option (#7750)
commit
|
commitdiff
|
tree
2021-12-07
Andrew Reynolds
Allow sygus in incremental mode (#7756)
commit
|
commitdiff
|
tree
2021-12-07
Andrew Reynolds
Make data structures in relevance manager SAT-context...
commit
|
commitdiff
|
tree
2021-12-07
Andrew Reynolds
Eliminate more static calls to Rewriter::rewrite (...
commit
|
commitdiff
|
tree
2021-12-07
Andrew Reynolds
Towards support for incremental sygus (#7736)
commit
|
commitdiff
|
tree
2021-12-07
Andrew Reynolds
Eliminate more static calls to Rewriter::rewrite (...
commit
|
commitdiff
|
tree
2021-12-06
Andrew Reynolds
Add regressions for fixed projects issues (#7739)
commit
|
commitdiff
|
tree
2021-12-03
Andrew Reynolds
Check constructor is used in APPLY_CONSTRUCTOR (#7737)
commit
|
commitdiff
|
tree
2021-12-03
Andrew Reynolds
Proper error for using constructor in multiple datatypes...
commit
|
commitdiff
|
tree
2021-12-02
Andrew Reynolds
Fixes for sygus-rr-synth-input (#7716)
commit
|
commitdiff
|
tree
2021-12-01
Andrew Reynolds
Improvements for get-difficulty (#7720)
commit
|
commitdiff
|
tree
2021-12-01
Andrew Reynolds
Remove spurious assertion in parser (#7713)
commit
|
commitdiff
|
tree
2021-12-01
Andrew Reynolds
Define sort undeclared (#7714)
commit
|
commitdiff
|
tree
2021-11-30
Andrew Reynolds
Add rewrite for is_int pi (#7711)
commit
|
commitdiff
|
tree
2021-11-30
Andrew Reynolds
Generalize eager length bound conflicts for regular...
commit
|
commitdiff
|
tree
2021-11-30
Andrew Reynolds
Proper check for first-class types in datatype subfields...
commit
|
commitdiff
|
tree
2021-11-24
Andrew Reynolds
Fix potential for cycles in trust substitutions (#7687)
commit
|
commitdiff
|
tree
next