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