projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Bump version to 1.0.1
2022-07-19
Andrew Reynolds
Fix bug in strict symbolic length strip (#8973)
commit
|
commitdiff
|
tree
2022-07-19
Andrew Reynolds
Global negate requires quantifiers (#8957)
commit
|
commitdiff
|
tree
2022-07-18
Andrew Reynolds
Fix global-declarations with abduction (#8961)
commit
|
commitdiff
|
tree
2022-07-11
Andrew Reynolds
Move bv arith conversions to arith (#8945)
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Eliminate static options accesses in sygus (#8943)
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Add scripts for casc j11 (#8941)
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Eliminate static options access in proof utilities...
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Fix issues with mixed types in relevant domain (#8901)
commit
|
commitdiff
|
tree
2022-07-08
Andrew Reynolds
Do not use sygus-inst for internal bounded quantifiers...
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Fix casting for arith msum (#8940)
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Fix mod elimination in learned rewrite preprocessing...
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Do not eagerly preprocess seq.nth (#8937)
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Revert usage of seq.nth in reductions (#8939)
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Fix pto handling for heaps that are not a subset of...
commit
|
commitdiff
|
tree
2022-06-30
Andrew Reynolds
Remove spurious pto singleton inference (#8925)
commit
|
commitdiff
|
tree
2022-06-30
Andrew Reynolds
Fix injectivity inferences for seq.nth applied to strings...
commit
|
commitdiff
|
tree
2022-06-30
Andrew Reynolds
Fix type issue in substitutions from covering solver...
commit
|
commitdiff
|
tree
2022-06-29
Andrew Reynolds
Fix reduction for seq.nth for strings (#8919)
commit
|
commitdiff
|
tree
2022-06-29
Andrew Reynolds
Fix model construction for str.unit (#8917)
commit
|
commitdiff
|
tree
2022-06-27
Andrew Reynolds
Revert change in lemma order in prop engine (#8911)
commit
|
commitdiff
|
tree
2022-06-23
Andrew Reynolds
Fix explanation for strings unit oob inference (#8908)
commit
|
commitdiff
|
tree
2022-06-23
Andrew Reynolds
Fix handling of injectivity for str.unit (#8899)
commit
|
commitdiff
|
tree
2022-06-22
Andrew Reynolds
Fix sort inference for equality over finite types ...
commit
|
commitdiff
|
tree
2022-06-07
Andrew Reynolds
Allow mixed int/real equalities in non-strict parsing...
commit
|
commitdiff
|
tree
2022-06-07
Andrew Reynolds
Add str.unit to LFSC signature (#8862)
commit
|
commitdiff
|
tree
2022-06-07
Andrew Reynolds
Use STRING_NTH in strings reductions and eliminate...
commit
|
commitdiff
|
tree
2022-06-06
Andrew Reynolds
Add MBQI to SMT comp script (#8858)
commit
|
commitdiff
|
tree
2022-06-05
Andrew Reynolds
Disable LFSC for regression with learned rewrite (...
commit
|
commitdiff
|
tree
2022-06-04
Andrew Reynolds
Fix corner case of interpolants from conjectures with...
commit
|
commitdiff
|
tree
2022-06-03
Andrew Reynolds
Fix check for whether a term contains an uninterpreted...
commit
|
commitdiff
|
tree
2022-06-03
Andrew Reynolds
Disable arithmetic static learning when unsat cores...
commit
|
commitdiff
|
tree
2022-06-03
Andrew Reynolds
Eliminate static options access from pattern term selector...
commit
|
commitdiff
|
tree
2022-06-02
Andrew Reynolds
Preparation for SEQ_NTH applied to strings (#8779)
commit
|
commitdiff
|
tree
2022-06-02
Andrew Reynolds
Fix missing conclusion for sep pto neg prop (#8844)
commit
|
commitdiff
|
tree
2022-06-01
Andrew Reynolds
Make interpolation robust to conjectures with no shared...
commit
|
commitdiff
|
tree
2022-05-31
Andrew Reynolds
Make subs minimize utility robust to non-constant evaluation...
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate more static options accesses (#8832)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate static options access for central ee (#8823)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate static options access in skolemize (#8831)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Fix mixed arithmetic issue in relevant domain (#8826)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate static options access in BV inverter (#8829)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Make Rewriter::rewrite non-static (#8828)
commit
|
commitdiff
|
tree
2022-05-26
Andrew Reynolds
Use function array constants in HO solver (#8818)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Eliminate some static options access (#8795)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Add model-based quantifier instantiation (#8729)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Eliminate static access to dtSharedSelectors (#8804)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Eliminate more static options accesses (#8802)
commit
|
commitdiff
|
tree
2022-05-24
Andrew Reynolds
Introduce function array constant (#8793)
commit
|
commitdiff
|
tree
2022-05-24
Andrew Reynolds
Fix subtype issues in proofs for nonlinear solver ...
commit
|
commitdiff
|
tree
2022-05-24
Andrew Reynolds
Add declareOracleFun to API (#8794)
commit
|
commitdiff
|
tree
2022-05-23
Andrew Reynolds
Remove spurious assertion in isLegalElimination (#8812)
commit
|
commitdiff
|
tree
2022-05-23
Andrew Reynolds
Make model core robust to when we cannot show the model...
commit
|
commitdiff
|
tree
2022-05-22
Andrew Reynolds
Simplification of smt2 printer for type ascriptions...
commit
|
commitdiff
|
tree
2022-05-21
Andrew Reynolds
Move smt_util to preprocessing/util (#8799)
commit
|
commitdiff
|
tree
2022-05-21
Andrew Reynolds
Reenable assertion in skolem definition manager (#8797)
commit
|
commitdiff
|
tree
2022-05-21
Andrew Reynolds
Add option to send all instantiations in a bounded...
commit
|
commitdiff
|
tree
2022-05-20
Andrew Reynolds
More removing of unused code (#8806)
commit
|
commitdiff
|
tree
2022-05-19
Andrew Reynolds
Minor deleting of unused code (#8800)
commit
|
commitdiff
|
tree
2022-05-19
Andrew Reynolds
Add options and regressions to increase coverage (...
commit
|
commitdiff
|
tree
2022-05-18
Andrew Reynolds
Basic cleanup of sep theory (#8790)
commit
|
commitdiff
|
tree
2022-05-18
Andrew Reynolds
Make skolem definition manager robust to definitions...
commit
|
commitdiff
|
tree
2022-05-18
Andrew Reynolds
Eliminate subtypes (#8783)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Refactor declare oracle command (#8742)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Minor cleanup of datatypes theory (#8791)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Fix LFSC proof construction for concat clash of sequences...
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Generalize pto constraint tracking for multiple heaps...
commit
|
commitdiff
|
tree
2022-05-16
Andrew Reynolds
Last remaining fixes for eliminating subtyping (#8772)
commit
|
commitdiff
|
tree
2022-05-15
Andrew Reynolds
Eliminate the use of CAST_TO_REAL (#8759)
commit
|
commitdiff
|
tree
2022-05-15
Andrew Reynolds
Eliminate ops for parameterized type constructors ...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Make arith substitute its own utility (#8765)
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Fixes and improvement for IAND solver (#8771)
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Eliminate use of getBaseType (#8764)
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Add utilities in preparation for supporting str.nth...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Fix debug failures in LFSC proofs due to curried arithmetic...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Refactor logic exceptions during preregistration for...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Minor refactoring for sep theory (#8753)
commit
|
commitdiff
|
tree
2022-05-12
Andrew Reynolds
Fix type of null terminator for ADD/MULT for LFSC ...
commit
|
commitdiff
|
tree
2022-05-12
Andrew Reynolds
Eliminate use of subtypes from remainder of type rules...
commit
|
commitdiff
|
tree
2022-05-12
Andrew Reynolds
Preserve types in rewriter and make core type rules...
commit
|
commitdiff
|
tree
2022-05-11
Andrew Reynolds
Relax an assertion in the evaluator (#8751)
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Improvements for evaluation in model (#8738)
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Do not depend on subtyping for APPLY_UF in TPTP parser...
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Add unit tests for getInstantiations (#8741)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
Do not rely on subtyping in real-to-int preprocessing...
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
More preparation for strict type rules (#8733)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
Fix proofs for ppAssert for theory Bool (#8708)
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Fallback for sequential substitution proof reconstruction...
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Eliminate arithmetic subtyping for (dis)equalities...
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Separate ill-typed portion of arith models (#8734)
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Fix LFSC side condition for matching premise of concat_unify...
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Preparation for making equality strictly typed (#8728)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Fix cache in learned rewrite preprocessing pass (#8725)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Fix more issues with subtypes in regressions (#8727)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Use purification for set comprehension reduction (...
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Make equality solver the entry point for all equality...
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Add declareOracleFun interface to SolverEngine (#8622)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Refactor oracles using new std::function backend (...
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Remove unecessary calls to equality engine from congruence...
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Fix rewrite for to_real in division by zero (#8714)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Add support for oracle constant nodes (#8707)
commit
|
commitdiff
|
tree
next