projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2020-03-10
Andrew Reynolds
Fix assertion failure in sort inference for Boolean...
commit
|
commitdiff
|
tree
2020-03-10
Aina Niemetz
Fix -Wshadow warnings in sygus_grammar_cons.cpp. (...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Do not set values for non-linear mult terms in collectM...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Fix real as int for incremental (#3979)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Do not traverse quantifiers in nl ext purify (#3982)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Only register sygus terms to unfold if option is set...
commit
|
commitdiff
|
tree
2020-03-10
Alex Ozdemir
Document bv-to-bool recursion (#3848)
commit
|
commitdiff
|
tree
2020-03-10
makaimann
Enhancement: make the bool-to-bv pass more robust and...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Rename sygus option name (#3977)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Remove instantiation propagator infrastructure (#3975)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Ensure standard miniscoping is applied before aggressiv...
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Eliminate spurious assertion (#3976)
commit
|
commitdiff
|
tree
2020-03-09
Aina Niemetz
DecisionEngine: Use unique_ptr for enabled strategies...
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Fix type issue in arith rewrite equality (#3972)
commit
|
commitdiff
|
tree
2020-03-09
Andres Noetzli
Make registration of unit clauses more robust (#3965)
commit
|
commitdiff
|
tree
2020-03-09
Andres Noetzli
Increase stack size for Windows builds to 100 MB (...
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Clean up more uses of ExprManager in parsers (#3932)
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Convert more uses of strings to words (#3921)
commit
|
commitdiff
|
tree
2020-03-09
Andres Noetzli
Fix quoting of options on Travis (#3981)
commit
|
commitdiff
|
tree
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
next