projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
More precise includes of `Node` constants (#6617)
[cvc5.git]
/
src
/
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
tree
|
commitdiff
2021-05-25
Andres Noetzli
Replace deprecated calls to `std::allocator` (#6606)
tree
|
commitdiff
2021-05-25
Andres Noetzli
[Unit tests] Fix path of Java bindings (#6616)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Fix non-fixed length case in re-elim (#6612)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Implementation of the new justification heuristic ...
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Fix re-elim length requirement for symbolic RE membersh...
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Fix instance of no rewrite in extended rewriter (#6610)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Better formalization of regular expression unfolding...
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Fix tests of unsat cores (#6593)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Fix and refactor relevant domain (#6528)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Formalize shared selectors as skolem functions (#6591)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Minor simplification to boolean proof checker (#6590)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
(proof-new) Minor documentation sync (#6592)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Add utility to get all types occurring in a term (...
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Update to sygus standard output for check-synth respons...
tree
|
commitdiff
2021-05-21
Andres Noetzli
Support braced-init-lists with `mkNode()` (#6580)
tree
|
commitdiff
2021-05-21
makaimann
Use scikit-build CMake files for pycvc5 (#6543)
tree
|
commitdiff
2021-05-21
Gereon Kremer
Move option names out of struct (#6554)
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-20
Gereon Kremer
Properly initialize. (#6586)
tree
|
commitdiff
2021-05-20
Haniel Barbosa
Remove old unsat cores (#6581)
tree
|
commitdiff
2021-05-20
yoni206
Avoid using printSynthSolution in the python API and...
tree
|
commitdiff
2021-05-20
Gereon Kremer
Minor improvements to the API (#6585)
tree
|
commitdiff
2021-05-20
Aina Niemetz
Fix echo printing. (#6573)
tree
|
commitdiff
2021-05-20
Gereon Kremer
Add more getters for api::Term (#6496)
tree
|
commitdiff
2021-05-20
Alex Ozdemir
Expand arith's farkas lemma rule as a macro (#6577)
tree
|
commitdiff
2021-05-19
Andres Noetzli
Remove unused methods from `NodeManager` (#6578)
tree
|
commitdiff
2021-05-19
Mathias Preiner
Correctly handle negated assertions for assumption...
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Pass empty vector when constructing re empty, fixes...
tree
|
commitdiff
2021-05-19
Andres Noetzli
Make output list of `mkoptions.py` more accurate (...
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Make strings emp inference an unhandled inference for...
tree
|
commitdiff
2021-05-19
Haniel Barbosa
Change the default unsat cores (#6571)
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Fix strings rewriter for non-standard re range (#6570)
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Add more missing inference ids (#6313)
tree
|
commitdiff
2021-05-19
Mathias Preiner
bv: Add support for --bitblast=eager. (#6516)
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Fix positive contains indexof rewrites for empty string...
tree
|
commitdiff
2021-05-19
Gereon Kremer
Remove accidental print (#6568)
tree
|
commitdiff
2021-05-19
Gereon Kremer
Generate command line options for sphinx docs (#6555)
tree
|
commitdiff
2021-05-19
Andres Noetzli
Improve handling of `:named` attributes (#6549)
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Fix handling of non-standard re.range terms (#6563)
tree
|
commitdiff
2021-05-18
Abdalrhman Mohamed
Loop over terms to reconstruct instead of obligations...
tree
|
commitdiff
2021-05-18
Andres Noetzli
Fix `collectEmptyEqs()` in string utils (#6562)
tree
|
commitdiff
2021-05-18
Andrew Reynolds
(proof-new) Miscellaneous updates to strings from proof...
tree
|
commitdiff
2021-05-18
Andrew Reynolds
Fix smt2 printing (#6558)
tree
|
commitdiff
2021-05-18
mudathirmahgoub
Add Solver.java to the Java API (#6196)
tree
|
commitdiff
2021-05-17
Andres Noetzli
Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites...
tree
|
commitdiff
2021-05-17
Gereon Kremer
Replace smt_name by aliases (#6541)
tree
|
commitdiff
2021-05-17
Andres Noetzli
Include cinttypes instead of inttypes.h (#6548)
tree
|
commitdiff
2021-05-17
Gereon Kremer
Improve integration of CAD with nl-Ext (#6542)
tree
|
commitdiff
2021-05-14
Andres Noetzli
Decouple parser creation from input selection (#6533)
tree
|
commitdiff
2021-05-14
mudathirmahgoub
Add Result.java to the java API (#6385)
tree
|
commitdiff
2021-05-14
Mathias Preiner
bv: Assert input facts on user-level 0. (#6515)
tree
|
commitdiff
2021-05-13
Andres Noetzli
Always parse streams with line buffer (#6532)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-13
Gereon Kremer
Split options holder class (#6527)
tree
|
commitdiff
2021-05-13
yoni206
Adding functions to the python API and testing them...
tree
|
commitdiff
2021-05-13
Alex Ozdemir
Fix error message in toPythonObj (#6524)
tree
|
commitdiff
2021-05-12
Andrew Reynolds
Ensure sequences of Booleans generate Boolean term...
tree
|
commitdiff
2021-05-12
Gereon Kremer
Use signal(sig, SIG_DFL); raise(sig); instead of abort...
tree
|
commitdiff
2021-05-10
Gereon Kremer
Remove header for option modules (#6514)
tree
|
commitdiff
2021-05-10
Gereon Kremer
Remove read_only from options. (#6513)
tree
|
commitdiff
2021-05-10
Andrew Reynolds
Unify top-level substitutions and model substitutions...
tree
|
commitdiff
2021-05-10
mudathirmahgoub
Add doc to Kind.java (#6498)
tree
|
commitdiff
2021-05-08
yoni206
Adding functions to the python API and testing them...
tree
|
commitdiff
2021-05-08
Andrew Reynolds
Add support for datatype update (#6449)
tree
|
commitdiff
2021-05-07
Haniel Barbosa
Properly printing INST_PATTERN_LIST by itself (#6507)
tree
|
commitdiff
2021-05-07
Andrew Reynolds
Simplifications to expand definitions (#6487)
tree
|
commitdiff
2021-05-07
makaimann
Fix for toPythonObj of integer value with real sort...
tree
|
commitdiff
2021-05-06
Haniel Barbosa
[proof-new] Updating documentation for Subs/Rw ids...
tree
|
commitdiff
2021-05-06
Andrew Reynolds
Discard duplicate terms in patterns (#6501)
tree
|
commitdiff
2021-05-06
Andrew Reynolds
Use constant folding for evaluating BV eager atom ...
tree
|
commitdiff
2021-05-05
Andrew Reynolds
Do not have quantifiers model inherit from theory model...
tree
|
commitdiff
2021-05-05
makaimann
Save block comments associated with each kind when...
tree
|
commitdiff
2021-05-05
Ouyancheng
Add helper functions for multi-objective optimization...
tree
|
commitdiff
2021-05-05
Andrew Reynolds
Move current decision engine to decision engine old...
tree
|
commitdiff
2021-05-04
Andrew Reynolds
Move env into smt solver, theory engine, prop engine...
tree
|
commitdiff
2021-05-04
Haniel Barbosa
Do not use proof CNF stream with assumptions-based...
tree
|
commitdiff
2021-05-04
Gereon Kremer
Improve generation of python API documentation (#6482)
tree
|
commitdiff
2021-05-04
Aina Niemetz
FP: Move removal of generic to_fp operations to rewrite...
tree
|
commitdiff
2021-05-04
Aina Niemetz
FP: Move type check from expandDefinitions. (#6479)
tree
|
commitdiff
2021-05-03
Aina Niemetz
FP: Rewrite to_fp conversion from signed bit-vector...
tree
|
commitdiff
2021-04-30
Mathias Preiner
bv: Refactor ppAssert and move to TheoryBV. (#6470)
tree
|
commitdiff
2021-04-30
Aina Niemetz
Add parameter name for argument `isPreRewrite` for...
tree
|
commitdiff
2021-04-30
Ouyancheng
Refactor optimization result and objective classes...
tree
|
commitdiff
2021-04-30
Andrew Reynolds
Use substitutions for implementing defined functions...
tree
|
commitdiff
2021-04-29
Andrew Reynolds
Add assertion list utility for justification heuristic...
tree
|
commitdiff
2021-04-29
Gereon Kremer
Simplify generated code for getOption() and setOption...
tree
|
commitdiff
2021-04-29
Gereon Kremer
Add missing include. (#6463)
tree
|
commitdiff
2021-04-29
Gereon Kremer
Avoid exponential explosion of small constant in CEGQI...
tree
|
commitdiff
2021-04-28
Ouyancheng
Fix BV Optimization Boundary Condition when lower bound...
tree
|
commitdiff
2021-04-28
Gereon Kremer
Refactor resource manager options (#6446)
tree
|
commitdiff
2021-04-28
Gereon Kremer
Remove exception headers from options.h (#6456)
tree
|
commitdiff
2021-04-28
Gereon Kremer
Make sure reference stats are reset properly (#6457)
tree
|
commitdiff
2021-04-28
Gereon Kremer
Clean up options holder class (#6458)
tree
|
commitdiff
2021-04-28
Gereon Kremer
Cleanup DidYouMean (#6454)
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Add internal support for datatype update (#6450)
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Fix refutational soundness bug in quantifier prenexing...
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Simplify making function types (#6447)
tree
|
commitdiff
2021-04-27
Gereon Kremer
Initial setup for docs of python API (#6445)
tree
|
commitdiff
next