projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2020-03-09
Andrew Reynolds
Fixes for bounds on transcendental functions (#3832)
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Rewrite again full for DIV rewrite (#3945)
commit
|
commitdiff
|
tree
2020-03-08
Ying Sheng
Explicit end marker for models printed in the CVC langu...
commit
|
commitdiff
|
tree
2020-03-06
Andrew Reynolds
Minor refactor for theory of sets (#3924)
commit
|
commitdiff
|
tree
2020-03-06
Andrew Reynolds
Simplify DatatypeDeclarationCommand command (#3928)
commit
|
commitdiff
|
tree
2020-03-06
Andrew Reynolds
Remove tester name from APIs (#3929)
commit
|
commitdiff
|
tree
2020-03-06
Andres Noetzli
Ignore model check warning in regression test (#3926)
commit
|
commitdiff
|
tree
2020-03-06
Andrew Reynolds
Make sygus datatype building independent of parser...
commit
|
commitdiff
|
tree
2020-03-06
Andrew Reynolds
Support default sygus grammar construction for sets...
commit
|
commitdiff
|
tree
2020-03-06
Andres Noetzli
Make output of regression script more readable (#3911)
commit
|
commitdiff
|
tree
2020-03-06
Andres Noetzli
Remove --apply-to-const preprocessing pass (#3919)
commit
|
commitdiff
|
tree
2020-03-05
Alex Ozdemir
Add a new arith constraint proof rule: IntTightenAP...
commit
|
commitdiff
|
tree
2020-03-05
Alex Ozdemir
Revert "Add a new arith constraint proof rule: IntTight...
commit
|
commitdiff
|
tree
2020-03-05
Andres Noetzli
Add a new arith constraint proof rule: IntTightenAP...
commit
|
commitdiff
|
tree
2020-03-05
Andrew Reynolds
Migrate a majority of the functionality in parsers...
commit
|
commitdiff
|
tree
2020-03-05
Aina Niemetz
Move ownership of DecisionEngine into PropEngine. ...
commit
|
commitdiff
|
tree
2020-03-05
Aina Niemetz
Revert "Move ownership of DecisionEngine into PropEngin...
commit
|
commitdiff
|
tree
2020-03-05
Andrew Reynolds
Move ownership of DecisionEngine into PropEngine. ...
commit
|
commitdiff
|
tree
2020-03-05
Andrew Reynolds
Fix issues with real to int (#3918)
commit
|
commitdiff
|
tree
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
commit
|
commitdiff
|
tree
2020-03-03
mudathirmahgoub
Refactoring and cleaning the type enumerator for sets...
commit
|
commitdiff
|
tree
2020-03-03
Andrew Reynolds
Standardize the interface for SMT engine subsolvers...
commit
|
commitdiff
|
tree
2020-03-03
Andres Noetzli
Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
commit
|
commitdiff
|
tree
2020-03-03
Mathias Preiner
Fix variable shadowing bug in sets. (#3898)
commit
|
commitdiff
|
tree
2020-03-02
Andrew Reynolds
Split collect model info by types in strings (#3847)
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Convert more uses of string to word (#3834)
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Throw warning instead of error for non-constant values...
commit
|
commitdiff
|
tree
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
commit
|
commitdiff
|
tree
2020-02-29
Aina Niemetz
propEngine: Reorder class declaration according to...
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Fix assertion related to assignability in the model...
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Replace conditional rewrite pass in quantifiers with...
commit
|
commitdiff
|
tree
2020-02-28
Andrew Reynolds
Use enum for quantifiers rewrite steps (#3840)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Refactor operator applications in the parser (#3831)
commit
|
commitdiff
|
tree
2020-02-27
Haniel Barbosa
Changing TPTP parser to accomodate new API (#3837)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Update purifySygusGTerm to the new API (#3830)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Fix large models for strings (#3835)
commit
|
commitdiff
|
tree
2020-02-27
Andres Noetzli
Fix -Wshadow warnings in common headers (#3826)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Add support for is_digit and regular expression differe...
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Disable regression that times out on debug (#3833)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Move fix for vacuous sygus types out of the parser...
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Some initial work on using words (#3819)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Infrastructure for tautological literals in nonlinear...
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Use side effect utility for non-linear lemmas (#3780)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Fix regression (#3827)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
More fixes for printing sygus commands (#3812)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Refactor type ascriptions in the parser (#3825)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Minor improvement to ParseOp (#3808)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Use default consts when not using any const during...
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Fix node arity issue in reduction of int2bv (#3777)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Move equivalence class info to its own file in strings...
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Support for witnessing choice in models (#3781)
commit
|
commitdiff
|
tree
2020-02-26
Andres Noetzli
Remove portfolio leftovers (#3821)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Minor cleaning of smt2 parser (#3823)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Embed mkAssociative utilities within the API. (#3801)
commit
|
commitdiff
|
tree
2020-02-25
mudathirmahgoub
Sets & Relations Java example (#3816)
commit
|
commitdiff
|
tree
2020-02-25
mudathirmahgoub
Sets & Relations Java example (#3816)
commit
|
commitdiff
|
tree
2020-02-25
yoni206
remove redundant includes (#3815)
commit
|
commitdiff
|
tree
2020-02-25
yoni206
bv_to_int preprocessing pass
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Fixes for quantifiers documentation (#3811)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Utilities for words (#3797)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Convert parser input interface to api::Term (#3809)
commit
|
commitdiff
|
tree
2020-02-24
Abdalrhman...
Fix bugs related to printing Sygus commands (#3804)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Add missing functions to new C++ API (#3769)
commit
|
commitdiff
|
tree
2020-02-24
Andres Noetzli
Make lambda rewriter more robust (#3806)
commit
|
commitdiff
|
tree
2020-02-23
Andrew Reynolds
Minor refactoring of equality notifications (#3798)
commit
|
commitdiff
|
tree
2020-02-22
Alex Ozdemir
RIP th_lra.plf (#3796)
commit
|
commitdiff
|
tree
2020-02-22
Andrew Reynolds
Move check memberships to reg exp solver (#3793)
commit
|
commitdiff
|
tree
2020-02-22
Andrew Reynolds
Move cardinality inference scheme to base solver in...
commit
|
commitdiff
|
tree
2020-02-22
makaimann
Dump boolean propagations and conflicts for decision...
commit
|
commitdiff
|
tree
2020-02-22
Alex Ozdemir
Switch to th_lira.plf (#3741)
commit
|
commitdiff
|
tree
2020-02-21
Aina Niemetz
New C++ API: Remove TOTAL kinds. (#3794)
commit
|
commitdiff
|
tree
2020-02-21
Andrew Reynolds
Simple changes towards unicode string standard (#3791)
commit
|
commitdiff
|
tree
2020-02-21
Andrew V. Jones
Adding checks to the validation of 'bv-sat-solver'...
commit
|
commitdiff
|
tree
2020-02-21
Andrew Reynolds
Split extended functions solver in strings (#3768)
commit
|
commitdiff
|
tree
2020-02-21
Alex Ozdemir
Remove IntReal tightening axioms from th_lira.plf ...
commit
|
commitdiff
|
tree
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
commit
|
commitdiff
|
tree
2020-02-20
Andres Noetzli
Remove unused code (#3782)
commit
|
commitdiff
|
tree
2020-02-20
Andrew Reynolds
Minor removals (#3786)
commit
|
commitdiff
|
tree
2020-02-20
Andres Noetzli
Remove parser from bindings (#3779)
commit
|
commitdiff
|
tree
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Fix symmetry breaking for multiple sygus types (#3775)
commit
|
commitdiff
|
tree
2020-02-19
makaimann
Add Python bindings using Cython -- see below for more...
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Delay enumerative instantiation if theory engine does...
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Change Record to shared_ptr (#3778)
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Fix approximate bounds for transcendental functions...
commit
|
commitdiff
|
tree
2020-02-19
makaimann
Change datatype selector/constructor/tester to terms...
commit
|
commitdiff
|
tree
2020-02-18
Andrew Reynolds
Add missing kinds for the new API (#3757)
commit
|
commitdiff
|
tree
2020-02-17
Andrew Reynolds
Option to limit the number of rounds of enumerative...
commit
|
commitdiff
|
tree
2020-02-17
Andrew Reynolds
Fix soundness bug in reduction of integer div/mod...
commit
|
commitdiff
|
tree
2020-02-17
Haniel Barbosa
Using ParseOp in TPTP (#3764)
commit
|
commitdiff
|
tree
2020-02-17
Abdalrhman...
Support dumping Sygus commands. (#3763)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Fix simple issue with cache (#3762)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Add temporary global API conversion utilities. (#3759)
commit
|
commitdiff
|
tree
2020-02-16
Andres Noetzli
Activate reverse variant of F-Split inference (#3745)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Disable regression (#3761)
commit
|
commitdiff
|
tree
2020-02-15
Andrew Reynolds
Move proxy variables to InferenceManager in strings...
commit
|
commitdiff
|
tree
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
commit
|
commitdiff
|
tree
2020-02-14
Andrew Reynolds
Update sygus v1 parser to use ParseOp utility (#3756)
commit
|
commitdiff
|
tree
next