projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
cvc5.git
2020-09-23
Andrew Reynolds
Fix type issue with term formula removal (#5107)
commit
|
commitdiff
|
tree
2020-09-23
Andres Noetzli
[Python API] Conversion to/from Unicode strings (#5120)
commit
|
commitdiff
|
tree
2020-09-22
Aina Niemetz
FP: Use Assert instead of PRECONDITION macro in convert...
commit
|
commitdiff
|
tree
2020-09-22
Mathias Preiner
Add simple BV solver (#5065)
commit
|
commitdiff
|
tree
2020-09-22
mudathirmahgoub
Add skeleton for theory of bags (multisets) (#5100)
commit
|
commitdiff
|
tree
2020-09-22
Andres Noetzli
Fix compilation without LibPoly (#5118)
commit
|
commitdiff
|
tree
2020-09-22
makaimann
Add method to get Python object from constant value...
commit
|
commitdiff
|
tree
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
commit
|
commitdiff
|
tree
2020-09-22
Gereon Kremer
ICP-based solver for nonlinear arithmetic (#5017)
commit
|
commitdiff
|
tree
2020-09-22
yoni206
Require dumping in a dumping test (#5108)
commit
|
commitdiff
|
tree
2020-09-21
Andrew Reynolds
(proof-new) Add the arrays proof checker (#5047)
commit
|
commitdiff
|
tree
2020-09-20
Andrew Reynolds
More flexible design for model manager distributed...
commit
|
commitdiff
|
tree
2020-09-19
Andrew Reynolds
Standardize equality engine notifications in sets ...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Fix assertion list for globally defined recursive funct...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Add the shared solver (#4982)
commit
|
commitdiff
|
tree
2020-09-18
yoni206
bv2int: quantifiers support (#5080)
commit
|
commitdiff
|
tree
2020-09-18
Andres Noetzli
Fix muzzled builds (#5093)
commit
|
commitdiff
|
tree
2020-09-18
Haniel Barbosa
[proof-new] Proof utilities for normalizing clauses...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Logic exception for arrays indexed by arrays (#5073)
commit
|
commitdiff
|
tree
2020-09-18
Andres Noetzli
[Strings] Fix extended equality rewriter (#5092)
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
(proof-new) Updates to proof node updater algorithm...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
(proof-new) Rewrites involving operators in term conver...
commit
|
commitdiff
|
tree
2020-09-17
Andrew Reynolds
(proof-new) Fixes for theory engine proof generator...
commit
|
commitdiff
|
tree
2020-09-17
Haniel Barbosa
[proof-new] Have mkScope agnostic to True assumptions...
commit
|
commitdiff
|
tree
2020-09-17
Gereon Kremer
(cad-solver) Fix square-free-basis computation (#5085)
commit
|
commitdiff
|
tree
2020-09-17
Andrew Reynolds
Reduce recursion in term formula removal (#5052)
commit
|
commitdiff
|
tree
2020-09-17
Gereon Kremer
Use new inference manager in transcendental solver...
commit
|
commitdiff
|
tree
2020-09-17
Andrew V. Jones
Do not allow to build Python bindings if building stati...
commit
|
commitdiff
|
tree
2020-09-17
Andrew Reynolds
Further standardization of datatypes (#5076)
commit
|
commitdiff
|
tree
2020-09-17
yoni206
Dumping internal define-funs with no arguments (#5077)
commit
|
commitdiff
|
tree
2020-09-16
Andres Noetzli
Only rewrite replace_re(_all) if regexp is const (...
commit
|
commitdiff
|
tree
2020-09-16
Abdalrhman...
Dump commands in internal code using command printing...
commit
|
commitdiff
|
tree
2020-09-16
Andrew Reynolds
Add buffered inference manager to TheorySep (#5038)
commit
|
commitdiff
|
tree
2020-09-16
Haniel Barbosa
[proof-new] Adds Lazy CDProof chain data-structure...
commit
|
commitdiff
|
tree
2020-09-16
Andrew Reynolds
Refactor collectModelInfo in TheoryArith (#5027)
commit
|
commitdiff
|
tree
2020-09-16
yoni206
bv2int: support models in tests (#5068)
commit
|
commitdiff
|
tree
2020-09-16
Haniel Barbosa
[proof-new] Extending eqproof conversion to HO congruen...
commit
|
commitdiff
|
tree
2020-09-16
Haniel Barbosa
[proof-new] Resolution rules and checkers (#5070)
commit
|
commitdiff
|
tree
2020-09-16
Haniel Barbosa
[proof-new] A simple proof generator for buffered proof...
commit
|
commitdiff
|
tree
2020-09-16
Andrew Reynolds
(proof-new) Make proofs mandatory in proof equality...
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Move sets member propagation to SolverState (#5045)
commit
|
commitdiff
|
tree
2020-09-15
Aina Niemetz
Rename system tests to api tests and remove obsolete...
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Move quantifiers engine private to own file (#5053)
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Fix needsModel method for CEGQI (#5048)
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Standard equality engine notify class for Theory (...
commit
|
commitdiff
|
tree
2020-09-15
Andres Noetzli
Fix ABC build (#5061)
commit
|
commitdiff
|
tree
2020-09-15
Ying Sheng
Interpolation: Add implementation for SyGuS interpolati...
commit
|
commitdiff
|
tree
2020-09-14
yoni206
bv2int: simpler translation for plus and times (#5055)
commit
|
commitdiff
|
tree
2020-09-14
Andrew Reynolds
Refactoring the rewriter of sets (#4856)
commit
|
commitdiff
|
tree
2020-09-14
Andres Noetzli
Fix type for Windows build (#5062)
commit
|
commitdiff
|
tree
2020-09-14
Andrew Reynolds
Standardize uses of inference manager in datatypes...
commit
|
commitdiff
|
tree
2020-09-12
Andrew Reynolds
(proof-new) Add SMT proof manager (#5054)
commit
|
commitdiff
|
tree
2020-09-12
Andrew Reynolds
(proof-new) Update TheoryEngine lemma and conflict...
commit
|
commitdiff
|
tree
2020-09-11
Andrew Reynolds
Move finite model minimization to UF last call effort...
commit
|
commitdiff
|
tree
2020-09-11
Andrew Reynolds
(proof-new) Handle mismatched assumptions in proof...
commit
|
commitdiff
|
tree
2020-09-11
Andrew Reynolds
(proof-new) Use deep copy for final lemma step in proof...
commit
|
commitdiff
|
tree
2020-09-11
Andrew Reynolds
Add witness to cvc printer. (#5057)
commit
|
commitdiff
|
tree
2020-09-10
yoni206
bv2int: refactoring the main translation loop (#5051)
commit
|
commitdiff
|
tree
2020-09-10
Andrew Reynolds
Parser error for wrong number of datatypes (#5049)
commit
|
commitdiff
|
tree
2020-09-10
yoni206
bv2int: improvement in lazy failures (#5020)
commit
|
commitdiff
|
tree
2020-09-10
Andrew Reynolds
Use state and inference manager in UF CardinalityExtens...
commit
|
commitdiff
|
tree
2020-09-09
Andrew Reynolds
(proof-new) Minor changes to proof node updater (#5011)
commit
|
commitdiff
|
tree
2020-09-09
Andrew Reynolds
(proof-new) Make proofs in term formula removal term...
commit
|
commitdiff
|
tree
2020-09-09
Andrew Reynolds
(proof-new) Generalize single step helper in eager...
commit
|
commitdiff
|
tree
2020-09-09
Andrew Reynolds
Fixes for regular expressions + sygus (#5044)
commit
|
commitdiff
|
tree
2020-09-09
mudathirmahgoub
Add is_singleton operator to the theory of sets (#5033)
commit
|
commitdiff
|
tree
2020-09-09
Andrew Reynolds
Split term registry from theory state in sets (#5037)
commit
|
commitdiff
|
tree
2020-09-08
Mathias Preiner
Fix printing of fp values. (#5041)
commit
|
commitdiff
|
tree
2020-09-08
Andres Noetzli
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)
commit
|
commitdiff
|
tree
2020-09-08
Andrew Reynolds
Eliminate a custom use of TheorySep in quantifiers...
commit
|
commitdiff
|
tree
2020-09-04
Andrew Reynolds
Add asLemma flag to theory inference process (#5030)
commit
|
commitdiff
|
tree
2020-09-04
Haniel Barbosa
[Regressions] Fix regression issues related to BV proof...
commit
|
commitdiff
|
tree
2020-09-04
Andrew Reynolds
(new theory) Update TheoryBV to new standard for collec...
commit
|
commitdiff
|
tree
2020-09-04
Haniel Barbosa
Fix non-lib-poly-build issues (#5028)
commit
|
commitdiff
|
tree
2020-09-04
Abdalrhman...
Use Result::Sat instead of BenchmarkStatus in printers...
commit
|
commitdiff
|
tree
2020-09-04
Gereon Kremer
Use arith::InferenceManager for CAD lemmas (#5015)
commit
|
commitdiff
|
tree
2020-09-04
Malte Mues
Change the unavailable ABC mercury repository for the...
commit
|
commitdiff
|
tree
2020-09-04
Mathias Preiner
Split lazy bit-vector solver from TheoryBV (#5009)
commit
|
commitdiff
|
tree
2020-09-04
Andrew Reynolds
Add interfaces for making trust nodes in TheoryInferenc...
commit
|
commitdiff
|
tree
2020-09-03
Andrew Reynolds
Update sets inference manager to inherit from Inference...
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Added a new rule to simplify (bvugt (bvurem T x) x...
commit
|
commitdiff
|
tree
2020-09-03
Andrew Reynolds
Minor cleanup of quantifiers engine (#4994)
commit
|
commitdiff
|
tree
2020-09-03
yoni206
Changing the handled operators in bv2int preprocessing...
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Basic integration of arith::InferenceManager (#4999)
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Make nonlinear extension (more) deterministic (#4996)
commit
|
commitdiff
|
tree
2020-09-03
FabianWolff
Drop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables...
commit
|
commitdiff
|
tree
2020-09-03
Andrew Reynolds
Make ExtTheory independent of Theory (#5010)
commit
|
commitdiff
|
tree
2020-09-03
Andrew Reynolds
(proof-new) Support proofs of quantifier instantiation...
commit
|
commitdiff
|
tree
2020-09-03
Andrew Reynolds
(proof-new) Improve debugging infrastructure for open...
commit
|
commitdiff
|
tree
2020-09-02
Andres Noetzli
Fix CryptoMiniSat build, regression (#5006)
commit
|
commitdiff
|
tree
2020-09-02
Andres Noetzli
[Python API] Add missing methods to Datatype/Term ...
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Remove #line directives from generated files. (#5005)
commit
|
commitdiff
|
tree
2020-09-02
Andrew Reynolds
(proof-new) Updates to builtin proof checker (#4962)
commit
|
commitdiff
|
tree
2020-09-02
Andrew Reynolds
(proof-new) Add proof support in TheoryUF (#5002)
commit
|
commitdiff
|
tree
2020-09-02
Andres Noetzli
Use SMT-COMP configuration for competition build (...
commit
|
commitdiff
|
tree
2020-09-02
Andrew Reynolds
(proof-new) Make term conversion proof generator option...
commit
|
commitdiff
|
tree
2020-09-02
Andrew V. Jones
Migrating from using the 'glpk-cut-log' repo to using...
commit
|
commitdiff
|
tree
2020-09-02
Abdalrhman...
Introduce an internal version of Commands. (#4988)
commit
|
commitdiff
|
tree
2020-09-02
Andrew Reynolds
Minor updates to theory inference manager (#5004)
commit
|
commitdiff
|
tree
2020-09-02
Andrew Reynolds
(new theory) Update TheoryArrays to the new standard...
commit
|
commitdiff
|
tree
next