projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Consolidate extended rewrite preprocessing modes (#8156)
2022-02-25
Andrew Reynolds
Consolidate extended rewrite preprocessing modes (...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Ensure variables are constrained in model when equal...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Make model builder robust to multiple value-like terms...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Make sine solver sound with respect to region boundaries...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Check for free variables in several SolverEngine calls...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Make uninterpreted sort owner non-static (#8144)
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Add regression for some fixed array issues (#8145)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Allow elimination of unevaluated terms by default ...
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Further relax what is considered a value in the model...
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Do not insist that entries for UF are constant in FMF...
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Eliminate match from LFSC proofs (#8090)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Option exception when incompatible with proofs (#8064)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Properly sanatize user names in LFSC (#8080)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Fix issue in datatypes care graph computation involving...
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Support some cases of isConst for regular expressions...
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Remove refineConflicts option (#8129)
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Change inference scheme in transcendentals to rewrite...
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Relax what is generated in the model from NL (#8113)
commit
|
commitdiff
|
tree
2022-02-21
Andrew Reynolds
Fixes and additions for LFSC signatures (#8120)
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Add unit test for fixed issue with get-difficulty ...
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Throw option exceptions when combining input conversion...
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Add well formed term check to solver engine (#8056)
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Make spurious assertion into warning (#8051)
commit
|
commitdiff
|
tree
2022-02-17
Andrew Reynolds
Introduce skolem function to make transcendental function...
commit
|
commitdiff
|
tree
2022-02-17
Andrew Reynolds
Missing ids for arith conflicts (#8108)
commit
|
commitdiff
|
tree
2022-02-17
Andrew Reynolds
Remove some irrelevant node kinds from the model (...
commit
|
commitdiff
|
tree
2022-02-17
Andrew Reynolds
[proofs] Consolidate multiple substitutions to single...
commit
|
commitdiff
|
tree
2022-02-16
Andrew Reynolds
[proofs] Make cache (optionally) persistent in lazy...
commit
|
commitdiff
|
tree
2022-02-16
Andrew Reynolds
Only consider relevant terms in the array-inspired...
commit
|
commitdiff
|
tree
2022-02-11
Andrew Reynolds
Ensure proofs are fully disabled when incompatible...
commit
|
commitdiff
|
tree
2022-02-11
Andrew Reynolds
Fix for lambda-to-array constant conversion for unused...
commit
|
commitdiff
|
tree
2022-02-10
Andrew Reynolds
Add assertion to require inference ids (#8091)
commit
|
commitdiff
|
tree
2022-02-10
Andrew Reynolds
Use witness terms to represent values for large strings...
commit
|
commitdiff
|
tree
2022-02-08
Andrew Reynolds
Simplify formalism of introduced arithmetic skolems...
commit
|
commitdiff
|
tree
2022-02-08
Andrew Reynolds
Distinguish proof mode from unsat core mode (#8062)
commit
|
commitdiff
|
tree
2022-02-08
Andrew Reynolds
Fix LFSC node conversion for non-shared selectors ...
commit
|
commitdiff
|
tree
2022-02-08
Andrew Reynolds
Always produce assertions (#8041)
commit
|
commitdiff
|
tree
2022-02-08
Andrew Reynolds
Make witness form visited ref counted (#8081)
commit
|
commitdiff
|
tree
2022-02-07
Andrew Reynolds
Generalize LFSC concat unify for splitting constants...
commit
|
commitdiff
|
tree
2022-02-07
Andrew Reynolds
Fix unsoundness in IAND solver (#8053)
commit
|
commitdiff
|
tree
2022-02-07
Andrew Reynolds
Fix indexof_re reduction (#8065)
commit
|
commitdiff
|
tree
2022-02-05
Andrew Reynolds
Fix another rewrite involving iand (#8054)
commit
|
commitdiff
|
tree
2022-02-04
Andrew Reynolds
Standardizing notifications for setting options in...
commit
|
commitdiff
|
tree
2022-02-03
Andrew Reynolds
Simplify handling of disequalities in strings (#8047)
commit
|
commitdiff
|
tree
2022-02-03
Andrew Reynolds
Eliminate even more static uses of rewrite (#8044)
commit
|
commitdiff
|
tree
2022-02-03
Andrew Reynolds
Test proof granularity theory-rewrite by default (...
commit
|
commitdiff
|
tree
2022-02-03
Andrew Reynolds
Eliminate more static uses of rewrite (#8040)
commit
|
commitdiff
|
tree
2022-02-03
Andrew Reynolds
Add miscellaneous missing theory definitions for LFSC...
commit
|
commitdiff
|
tree
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
next