projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add documentation for QuickStart.java (#7730)
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
2021-11-23
Andrew Reynolds
Make difficulty manager only consider lemmas at full...
commit
|
commitdiff
|
tree
2021-11-23
Andrew Reynolds
Enable model-based reduction technique for strings...
commit
|
commitdiff
|
tree
2021-11-22
Andrew Reynolds
Add rewrite for repeated re.allchar (#7681)
commit
|
commitdiff
|
tree
2021-11-22
Andrew Reynolds
Improve error for check theory assertions with model...
commit
|
commitdiff
|
tree
2021-11-22
Andrew Reynolds
Fix const RE test for internal regexp rv kind (#7678)
commit
|
commitdiff
|
tree
2021-11-19
Andrew Reynolds
Remove n-ary builder (#7671)
commit
|
commitdiff
|
tree
2021-11-17
Andrew Reynolds
Preparations for eliminating arithmetic subtyping ...
commit
|
commitdiff
|
tree
2021-11-17
Andrew Reynolds
Revert change and clean datatypes cons candidate generator...
commit
|
commitdiff
|
tree
2021-11-12
Andrew Reynolds
[proofs] Cancel SYMM in CDProof, throw an error for...
commit
|
commitdiff
|
tree
2021-11-12
Andrew Reynolds
Add some basic rewrites for regular expression intersection...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Generalize front-end checks to check for shadowed variables...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Add lazy approach for handling lambdas in the HO extension...
commit
|
commitdiff
|
tree
2021-11-11
Andrew Reynolds
Fixes for update/nth over constant sequences (#7631)
commit
|
commitdiff
|
tree
2021-11-10
Andrew Reynolds
Fix parsing array constants (#7617)
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Only eliminate lambdas in higher-order elimination...
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Minor optimizations for term database (#7600)
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Preparation for non-constant lambda models (#7604)
commit
|
commitdiff
|
tree
2021-11-09
Andrew Reynolds
Add LFSC signature for strings (#7523)
commit
|
commitdiff
|
tree
2021-11-08
Andrew Reynolds
Add lambda lift utility (#7601)
commit
|
commitdiff
|
tree
2021-11-08
Andrew Reynolds
Evaluate cast-to-real operator (#7599)
commit
|
commitdiff
|
tree
2021-11-06
Andrew Reynolds
Do not use extended rewrites on recursive function...
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Fix exclusion criteria for codatatype model values...
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Eliminate a level of nesting of traversals in theory...
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Move functions and lambdas from builtin to uf (#7570)
commit
|
commitdiff
|
tree
2021-11-05
Andrew Reynolds
Remove many static calls to rewrite (#7580)
commit
|
commitdiff
|
tree
2021-11-04
Andrew Reynolds
Add -o sygus-grammar to print auto-generated SyGuS...
commit
|
commitdiff
|
tree
2021-11-04
Andrew Reynolds
Improve defaults for sygus default grammars (#7553)
commit
|
commitdiff
|
tree
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Fix debug trace for miplib (#7563)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Refactor skolem construction (#7561)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Formalize more string skolems (#7554)
commit
|
commitdiff
|
tree
2021-11-03
Andrew Reynolds
Fix preregistration for floating point theory (#7558)
commit
|
commitdiff
|
tree
2021-11-02
Andrew Reynolds
Improve syntax for fmf cardinality constraints (#7556)
commit
|
commitdiff
|
tree
2021-11-02
Andrew Reynolds
Add LFSC signature for quantifiers (#7540)
commit
|
commitdiff
|
tree
2021-11-02
Andrew Reynolds
Make quant elimination robust to presence of other...
commit
|
commitdiff
|
tree
2021-11-01
Andrew Reynolds
Eliminate calls to Rewriter::rewrite and options::...
commit
|
commitdiff
|
tree
2021-11-01
Andrew Reynolds
Weaken assertion in CEGQI (#7548)
commit
|
commitdiff
|
tree
2021-11-01
Andrew Reynolds
Fix upwards closure for relations (#7515)
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Minor cleanup of proof messages (#7494)
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Fix model construction for higher order involving irrelevant...
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Add PfRule ARITH_POLY_NORM (#7501)
commit
|
commitdiff
|
tree
2021-10-29
Andrew Reynolds
Improvements for LFSC proof conversion (#7524)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
Properly guard proof construction for STRINGS_EXTF_EQ_REW...
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for linear arithmetic (#7445)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for CNF (#7444)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for Booleans (#7443)
commit
|
commitdiff
|
tree
2021-10-28
Andrew Reynolds
LFSC signature for equality (#7442)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Add missing API checks to getValue (#7475)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix care graph computation for higher-order (#7474)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix model unsoundness for relation join (#7511)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Avoid non-terminating check with assumptions in strings...
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Deterministic variables for RE elim (#7489)
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable automatic symmetry in proofs of theory explanations...
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Add regressions for fixed issues (#7495)
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable sygus-inst when incremental (#7485)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Add new method for enumerating unsat queries with SyGuS...
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix spurious checks to closed proofs (#7484)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Java and python unit tests for mkCardinalityConstraint...
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix more missing uses of CDProof::isSame (#7491)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix support for global declarations (#7480)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Remove HOL/fmf bound messages in set defaults (#7487)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Reenable proofs on some regressions (#7483)
commit
|
commitdiff
|
tree
2021-10-24
Andrew Reynolds
Add new eager conflict detection in strings for integer...
commit
|
commitdiff
|
tree
2021-10-23
Andrew Reynolds
Remove spurious assertoin (#7458)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Add requires libpoly to regression (#7467)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Remove stale pointer to proof node manager from skolemize...
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Remove `--uf-ho` option (#7463)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Fix symmetry issue in theory engine conflicts (#7469)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Add more abduction regressions (#7461)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Refactor theory inference manager constructor (#7457)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Do not use global proxy variable attribute for strings...
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Make expression mining use configurable options and...
commit
|
commitdiff
|
tree
2021-10-21
Andrew Reynolds
Split utilites from CEGIS core connective module (...
commit
|
commitdiff
|
tree
2021-10-21
Andrew Reynolds
Make cardinality constraint a nullary operator (#7333)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Enable some previously failing regressions (#7434)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Move variadic trie utility to its own file (#7410)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add regressions for fixed issues (#7421)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Throw exception if checking model with separation logic...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Check for higher-order variables in TheoryUF::ppRewrite...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Eliminate last static calls to rewriter from smt layer...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Make SyGuS solver robust to non-closed enumerable sorts...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Do not construct instantiation for checking propagating...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Check whether abduct option is enabled (#7418)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add LFSC signature for n-ary programs (#7360)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Use codatatype bound variables for codatatype values...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Reimplement support for relational triggers (#7063)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Do not make assumption about model for Boolean variables...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Correctly parse uninterpreted constant values in get...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Make proofs of rewrites robust to use in internal subsolvers...
commit
|
commitdiff
|
tree
next