projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[proofs] Adding NoSubtype node converter to Alethe (#7587)
[cvc5.git]
/
src
/
2021-11-08
Haniel Barbosa
[proofs] Adding NoSubtype node converter to Alethe...
tree
|
commitdiff
2021-11-08
Haniel Barbosa
[proofs] Method to convert node representation of Aleth...
tree
|
commitdiff
2021-11-06
Gereon Kremer
Integrate java unit tests into ctest (#7593)
tree
|
commitdiff
2021-11-06
Abdalrhman Mohamed
Print `unsupported` for unrecognized flags. (#7384)
tree
|
commitdiff
2021-11-06
Haniel Barbosa
better traces in node converter (#7590)
tree
|
commitdiff
2021-11-06
Andrew Reynolds
Do not use extended rewrites on recursive function...
tree
|
commitdiff
2021-11-06
Gereon Kremer
Remove `Notice()` in favor of new `verbose()` (#7588)
tree
|
commitdiff
2021-11-05
Andrew Reynolds
Fix exclusion criteria for codatatype model values...
tree
|
commitdiff
2021-11-05
Haniel Barbosa
[proofs] Fix open sat proof (#7509)
tree
|
commitdiff
2021-11-05
Andrew Reynolds
Eliminate a level of nesting of traversals in theory...
tree
|
commitdiff
2021-11-05
Gereon Kremer
Remove `Chat()` in favor of new `verbose()` (#7586)
tree
|
commitdiff
2021-11-05
Andrew Reynolds
Move functions and lambdas from builtin to uf (#7570)
tree
|
commitdiff
2021-11-05
Andres Noetzli
[FP] Do not assert that model has shared term (#7585)
tree
|
commitdiff
2021-11-05
Gereon Kremer
Fix some issues with the java api (#7583)
tree
|
commitdiff
2021-11-05
Lachnitt
Alethe: Translate CNF rules (#7532)
tree
|
commitdiff
2021-11-05
Haniel Barbosa
Minor changes to circuit propagator (#7584)
tree
|
commitdiff
2021-11-05
Andrew Reynolds
Remove many static calls to rewrite (#7580)
tree
|
commitdiff
2021-11-05
Gereon Kremer
Remove quadratic solving in NlModel (#7542)
tree
|
commitdiff
2021-11-05
Gereon Kremer
Eliminate `Warning` macro in favor of `EnvObj::warning...
tree
|
commitdiff
2021-11-05
Gereon Kremer
Remove a bunch of debugging/logging code from the linea...
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Add -o sygus-grammar to print auto-generated SyGuS...
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Improve defaults for sygus default grammars (#7553)
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
tree
|
commitdiff
2021-11-04
Gereon Kremer
Start refactoring of `-o` and `-v` (#7449)
tree
|
commitdiff
2021-11-04
Gereon Kremer
Refactor cmake to build either static or shared (#7534)
tree
|
commitdiff
2021-11-04
Gereon Kremer
Enable CDCAC solver for selected quantified logics...
tree
|
commitdiff
2021-11-04
Gereon Kremer
Add support for special tag collectors (#7562)
tree
|
commitdiff
2021-11-04
Gereon Kremer
Minor cleanup in SolverEngine::setInfo() (#7566)
tree
|
commitdiff
2021-11-04
Andres Noetzli
Make `Theory::get()` private (#7518)
tree
|
commitdiff
2021-11-03
Aina Niemetz
api: Rename some separation logic functions for consist...
tree
|
commitdiff
2021-11-03
mudathirmahgoub
Enable CI for Junit tests (#7436)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Fix debug trace for miplib (#7563)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Refactor skolem construction (#7561)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Formalize more string skolems (#7554)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Fix preregistration for floating point theory (#7558)
tree
|
commitdiff
2021-11-02
Mathias Preiner
bv: Disable equality engine for --bitblast=eager and...
tree
|
commitdiff
2021-11-02
Abdalrhman Mohamed
Move `fmf.card` printing code. (#7559)
tree
|
commitdiff
2021-11-02
Abdalrhman Mohamed
Add printing methods for some commands. (#7557)
tree
|
commitdiff
2021-11-02
Andrew Reynolds
Improve syntax for fmf cardinality constraints (#7556)
tree
|
commitdiff
2021-11-02
Mathias Preiner
Fix setDefaults() for proofs with bitblast-internal...
tree
|
commitdiff
2021-11-02
Mathias Preiner
bv: Remove remaining Rewriter::rewrite calls. (#7545)
tree
|
commitdiff
2021-11-02
Andrew Reynolds
Make quant elimination robust to presence of other...
tree
|
commitdiff
2021-11-01
Andrew Reynolds
Eliminate calls to Rewriter::rewrite and options::...
tree
|
commitdiff
2021-11-01
Andrew Reynolds
Weaken assertion in CEGQI (#7548)
tree
|
commitdiff
2021-11-01
Gereon Kremer
Add explicit option enum value __MAX_VALUE (#7547)
tree
|
commitdiff
2021-11-01
Mathias Preiner
bv: Remove layered solver. (#7455)
tree
|
commitdiff
2021-11-01
Aina Niemetz
api: Fix documentation for kind IAND. (#7536)
tree
|
commitdiff
2021-11-01
Gereon Kremer
Clean up CLN includes (#7544)
tree
|
commitdiff
2021-11-01
Andrew Reynolds
Fix upwards closure for relations (#7515)
tree
|
commitdiff
2021-11-01
Gereon Kremer
Replace more static options accesses (#7531)
tree
|
commitdiff
2021-11-01
Gereon Kremer
Refactor DidYouMean (#7535)
tree
|
commitdiff
2021-10-31
Mathias Preiner
api: Add guard against querying value from term with...
tree
|
commitdiff
2021-10-31
mudathirmahgoub
Fix soundess issue for bags with negative multiplicity...
tree
|
commitdiff
2021-10-31
mudathirmahgoub
Remove assertSkeleton for bag elements during model...
tree
|
commitdiff
2021-10-29
Gereon Kremer
Fix proof of nl lemma for a corner case (#7530)
tree
|
commitdiff
2021-10-29
Gereon Kremer
Remove options::X__numValues (#7419)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Minor cleanup of proof messages (#7494)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Fix model construction for higher order involving irrel...
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Add PfRule ARITH_POLY_NORM (#7501)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Improvements for LFSC proof conversion (#7524)
tree
|
commitdiff
2021-10-29
Gereon Kremer
Remove static access to options in decision folder...
tree
|
commitdiff
2021-10-28
Gereon Kremer
Fix proof for xor in circuit propagator (#7525)
tree
|
commitdiff
2021-10-28
Gereon Kremer
Combine `--static` and `--static-binary` (#7520)
tree
|
commitdiff
2021-10-28
Haniel Barbosa
[proofs] Fix assertion in EqProof conversion (#7522)
tree
|
commitdiff
2021-10-28
Andrew V. Jones
Add support for checking if a `-Wno` flag exists before...
tree
|
commitdiff
2021-10-28
Abdalrhman Mohamed
Add a `define-fun` command for each `:named` term....
tree
|
commitdiff
2021-10-28
Andrew Reynolds
Properly guard proof construction for STRINGS_EXTF_EQ_R...
tree
|
commitdiff
2021-10-28
Abdalrhman Mohamed
Fix `(set-info <sexpr>)` parsing and printing bugs...
tree
|
commitdiff
2021-10-28
Gereon Kremer
Remove separate cpp docs for UnknownExplanation (#7516)
tree
|
commitdiff
2021-10-27
Andrew Reynolds
Add missing API checks to getValue (#7475)
tree
|
commitdiff
2021-10-27
Gereon Kremer
Add comments for arith type rules. (#7488)
tree
|
commitdiff
2021-10-27
Gereon Kremer
Add documentation on output tags (#7499)
tree
|
commitdiff
2021-10-27
Andres Noetzli
Require ITE branches to be first class types (#7508)
tree
|
commitdiff
2021-10-27
Andrew Reynolds
Fix care graph computation for higher-order (#7474)
tree
|
commitdiff
2021-10-27
Andrew Reynolds
Fix model unsoundness for relation join (#7511)
tree
|
commitdiff
2021-10-27
yoni206
Python api documentation for sorts (#7440)
tree
|
commitdiff
2021-10-27
Andrew Reynolds
Avoid non-terminating check with assumptions in strings...
tree
|
commitdiff
2021-10-27
Andrew Reynolds
Deterministic variables for RE elim (#7489)
tree
|
commitdiff
2021-10-27
mudathirmahgoub
Fix mac compile errors in sort.cpp (#7507)
tree
|
commitdiff
2021-10-27
Gereon Kremer
Make --version exit (#7506)
tree
|
commitdiff
2021-10-27
Gereon Kremer
Fix libpoly build on windows (#7502)
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Fix singleton check in MACRO_RES post-processi...
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Modularize check for whether a clause is singl...
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Reset local var in SatProofManager since incre...
tree
|
commitdiff
2021-10-26
Andrew Reynolds
Disable automatic symmetry in proofs of theory explanat...
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Fix and simplify CHAIN_RESOLUTION checker...
tree
|
commitdiff
2021-10-26
Andrew Reynolds
Disable sygus-inst when incremental (#7485)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate Block of clause pattern...
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate AND_INTRO rule (#7405)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate AND_ELIM rule (#7404)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate CONTRA rule (#7403)
tree
|
commitdiff
2021-10-26
Gereon Kremer
Fix frequent rebuild of options target (#7450)
tree
|
commitdiff
2021-10-26
Gereon Kremer
Fix Configuration::isStaticBuild (#7456)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)
tree
|
commitdiff
2021-10-25
Lachnitt
[proofs] Alethe: Translate MODUS_PONENS rule (#7401)
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Add new method for enumerating unsat queries with SyGuS...
tree
|
commitdiff
2021-10-25
Lachnitt
[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Fix spurious checks to closed proofs (#7484)
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Java and python unit tests for mkCardinalityConstraint...
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Fix more missing uses of CDProof::isSame (#7491)
tree
|
commitdiff
next