projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix unsoundness in IAND solver (#8053)
[cvc5.git]
/
src
/
smt
/
2022-02-07
Gereon Kremer
Improve combination of NRA and transcendentals (#8075)
tree
|
commitdiff
2022-02-04
Andrew Reynolds
Standardizing notifications for setting options in...
tree
|
commitdiff
2022-02-02
Andrew Reynolds
Remove more static calls to rewrite (#8025)
tree
|
commitdiff
2022-01-26
Andrew Reynolds
More fixes and improvements for query generator (#7988)
tree
|
commitdiff
2022-01-25
Andrew Reynolds
Add output -o post-asserts (#7987)
tree
|
commitdiff
2022-01-17
Andrew Reynolds
Refactor options related to rewriting and symmetry...
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Clean enumerative instantiation options (#7947)
tree
|
commitdiff
2022-01-14
Gereon Kremer
Preprare central model building for RANs (#7951)
tree
|
commitdiff
2022-01-13
Andres Noetzli
Unify abstract values and uninterpreted constants ...
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Add -o learned-lits to output learned literals (#7934)
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Ensure configuration of shared selectors is consistent...
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Eliminate use of subtyping from results of quantifier...
tree
|
commitdiff
2022-01-11
Andrew Reynolds
Tighten policy for unsat cores in sygus core connective...
tree
|
commitdiff
2022-01-11
Andrew Reynolds
Guard use of unsat core mode pp-only (#7899)
tree
|
commitdiff
2022-01-07
Andrew Reynolds
Fix eager string preprocessing in incremental mode...
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Make alpha equivalence user context dependent (#7889)
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Disallow separation logic in incremental mode (#7888)
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Minor cleaning of non-clausal simplification (#7886)
tree
|
commitdiff
2022-01-05
Andrew Reynolds
Track input list for atoms in difficulty manager (...
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Change default granularity of proofs to macro (#7855)
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Remove spurious call to applySubs (#7871)
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Remove unused shutdown infrastructure (#7872)
tree
|
commitdiff
2021-12-22
Andrew Reynolds
Add support for incremental + interpolants (#7853)
tree
|
commitdiff
2021-12-21
Andrew Reynolds
Support get-abduct-next (#7850)
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Allow SyGuS subsolver to be reused in incremental mode...
tree
|
commitdiff
2021-12-17
Andrew Reynolds
Refactoring initialization of proofs (#7834)
tree
|
commitdiff
2021-12-16
Andrew Reynolds
Fix get-model when sort constructors are present (...
tree
|
commitdiff
2021-12-16
Andrew Reynolds
Minor fix for print benchmark. (#7821)
tree
|
commitdiff
2021-12-15
Andrew Reynolds
Add trace to see inferences in final proof (#7813)
tree
|
commitdiff
2021-12-14
Andrew Reynolds
Connecting the core array solver in strings (#7800)
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
tree
|
commitdiff
2021-12-13
Gereon Kremer
Improve nonlinear solver (#7787)
tree
|
commitdiff
2021-12-10
Haniel Barbosa
[proofs] Add option to prune inputs from final proof...
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Remove a few static access to options in proof code...
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Do not make SyGuS subsolver in unsat state after solvin...
tree
|
commitdiff
2021-12-08
Gereon Kremer
Static options acceses again (#7771)
tree
|
commitdiff
2021-12-07
Gereon Kremer
Remove more static accesses to options (#7764)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Add proof annotation option (#7750)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Allow sygus in incremental mode (#7756)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Make data structures in relevance manager SAT-context...
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Towards support for incremental sygus (#7736)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Eliminate more static calls to Rewriter::rewrite (...
tree
|
commitdiff
2021-12-01
Andrew Reynolds
Improvements for get-difficulty (#7720)
tree
|
commitdiff
2021-11-24
Andres Noetzli
Minor fixes (#7691)
tree
|
commitdiff
2021-11-22
Gereon Kremer
Refactor IO stream manipulators (#7555)
tree
|
commitdiff
2021-11-17
Andres Noetzli
Fix binding of quoted symbols in `define-fun` (#7655)
tree
|
commitdiff
2021-11-16
Haniel Barbosa
[proofs] Make sure --proof-check=... is no-op when...
tree
|
commitdiff
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
tree
|
commitdiff
2021-11-11
Andrew Reynolds
Generalize front-end checks to check for shadowed varia...
tree
|
commitdiff
2021-11-11
Andrew Reynolds
Add lazy approach for handling lambdas in the HO extens...
tree
|
commitdiff
2021-11-09
Gereon Kremer
Remove command-verbosity option (#7581)
tree
|
commitdiff
2021-11-06
Abdalrhman Mohamed
Print `unsupported` for unrecognized flags. (#7384)
tree
|
commitdiff
2021-11-06
Gereon Kremer
Remove `Notice()` in favor of new `verbose()` (#7588)
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
Remove many static calls to rewrite (#7580)
tree
|
commitdiff
2021-11-05
Gereon Kremer
Eliminate `Warning` macro in favor of `EnvObj::warning...
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
Enable CDCAC solver for selected quantified logics...
tree
|
commitdiff
2021-11-04
Gereon Kremer
Minor cleanup in SolverEngine::setInfo() (#7566)
tree
|
commitdiff
2021-11-03
Aina Niemetz
api: Rename some separation logic functions for consist...
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Refactor skolem construction (#7561)
tree
|
commitdiff
2021-11-02
Abdalrhman Mohamed
Add printing methods for some commands. (#7557)
tree
|
commitdiff
2021-11-02
Mathias Preiner
Fix setDefaults() for proofs with bitblast-internal...
tree
|
commitdiff
2021-11-02
Andrew Reynolds
Make quant elimination robust to presence of other...
tree
|
commitdiff
2021-11-01
Mathias Preiner
bv: Remove layered solver. (#7455)
tree
|
commitdiff
2021-11-01
Gereon Kremer
Replace more static options accesses (#7531)
tree
|
commitdiff
2021-10-28
Abdalrhman Mohamed
Add a `define-fun` command for each `:named` term....
tree
|
commitdiff
2021-10-27
Andrew Reynolds
Deterministic variables for RE elim (#7489)
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Fix singleton check in MACRO_RES post-processi...
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-25
Andrew Reynolds
Add new method for enumerating unsat queries with SyGuS...
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Fix support for global declarations (#7480)
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Remove HOL/fmf bound messages in set defaults (#7487)
tree
|
commitdiff
2021-10-25
mudathirmahgoub
Add inference for count map (#7264)
tree
|
commitdiff
2021-10-22
Gereon Kremer
Remove options::X__name (#7414)
tree
|
commitdiff
2021-10-22
Haniel Barbosa
[proof] Fixing CHAIN_RESOLUTION checker (#7465)
tree
|
commitdiff
2021-10-22
Andrew Reynolds
Remove `--uf-ho` option (#7463)
tree
|
commitdiff
2021-10-20
Andrew Reynolds
Throw exception if checking model with separation logic...
tree
|
commitdiff
2021-10-20
Andrew Reynolds
Eliminate last static calls to rewriter from smt layer...
tree
|
commitdiff
2021-10-20
Abdalrhman Mohamed
Avoid escaping `double-quotes` twice. (#7409)
tree
|
commitdiff
2021-10-19
Andrew Reynolds
Fix expected conclusion for EQ_RESOLVE when expanding...
tree
|
commitdiff
2021-10-14
Gereon Kremer
Fix (get-info :authors) (#7373)
tree
|
commitdiff
2021-10-13
Andrew Reynolds
Eliminate uses of rewrite from datatypes theory (#7354)
tree
|
commitdiff
2021-10-12
Andrew Reynolds
Eliminate calls to currentResourceManager (#7350)
tree
|
commitdiff
2021-10-12
Aina Niemetz
Clean up occurrences of SmtEngine in comments. (#7349)
tree
|
commitdiff
2021-10-12
Aina Niemetz
Get rid of unused member d_smtStats in ExpandDefs....
tree
|
commitdiff
2021-10-12
Aina Niemetz
Rename SmtEngineState to SolverEngineState. (#7344)
tree
|
commitdiff
2021-10-12
Andrew Reynolds
Provide a non-traversal interface to term formula remov...
tree
|
commitdiff
2021-10-11
Aina Niemetz
Rename SmtEngineStatistics to SolverEngineStatistics...
tree
|
commitdiff
2021-10-11
Aina Niemetz
Rename SmtScope to SolverEngineScope. (#7284)
tree
|
commitdiff
2021-10-11
Andrew Reynolds
Connect the LFSC printer (#7323)
tree
|
commitdiff
2021-10-09
Gereon Kremer
Remove static accesses to options where EnvObj is used...
tree
|
commitdiff
2021-10-08
Andrew Reynolds
A few more miscellaneous uses of EnvObj (#7325)
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Move preprocessor to smt solver (#7321)
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Use skolem lemma in prop layer interfaces (#7320)
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Make the cardinality of the alphabet of strings configu...
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Eliminate more circular dependencies on solver engine...
tree
|
commitdiff
next