projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Update theory rewriter ownership, add stats to strings (#4202)
2020-04-03
Andrew Reynolds
Only rewrite lambdas via array representations when...
commit
|
commitdiff
|
tree
2020-04-03
Andrew Reynolds
Split sequences rewriter (#4194)
commit
|
commitdiff
|
tree
2020-04-02
Andrew Reynolds
Introduce enums for all string inferences, excluding...
commit
|
commitdiff
|
tree
2020-04-01
Andrew Reynolds
Support char smt-lib syntax (#4188)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Fix fmf benchmark (#4193)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Remove replay and use-theory options and idl (#4186)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Fix strange bound regression (#4192)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Convert more uses of string-specific functions (#4158)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Fixing regressions (#4189)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Rewrites for all remaining return statements in strings...
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Support indexed operators re.loop and re.^ (#4167)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Remove ref skolem datatype option (#4185)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Fix arguments to print callback (#4171)
commit
|
commitdiff
|
tree
2020-03-29
Andrew Reynolds
Enumeration for String rewrites (#4173)
commit
|
commitdiff
|
tree
2020-03-28
Andrew Reynolds
Split transcendental solver to its own file (#4156)
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Fix expected output on arith regression (#4162)
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Move string utility file (#4164)
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Do not require that function sorts are first class...
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Move set defaults function to its own file (#4154)
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Disable slow regression (#4157)
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Add stats for string reductions, lemmas and conflicts...
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Generalize more string-specific functions (#4152)
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Care graphs based on polymorphic operators in strings...
commit
|
commitdiff
|
tree
2020-03-25
Andrew Reynolds
Generalize more uses of string-specific functions...
commit
|
commitdiff
|
tree
2020-03-24
Andrew Reynolds
Restrict partial triggers to standard quantified formulas...
commit
|
commitdiff
|
tree
2020-03-24
Andrew Reynolds
Restrict cases of sygus grammar reduction based on...
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Infer when sygus operators are equivalent to builtin...
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Simplify auxiliary variable handling in CEGQI (#4141)
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Throw exception for non-well-founded unimplemented...
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Change transcendental function app slave list to unordered_s...
commit
|
commitdiff
|
tree
2020-03-22
Andrew Reynolds
Sort inference does not handle APPLY_UF when higher...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Generalize mkConcat for types (#4123)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Fix variable shadowing issue in sygus-inference (#4121)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Fix sort comparison within assertion in cegis (#4113)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Guard cases of sort inference in quantifier free logics...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Split string-specific operators from TheoryStringsRewriter...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Do not assign higher-order representative if function...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Handle failures for sygus QE preprocess (#4072)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Parse error for SyGuS version 1.0 vs 2.0 (#4057)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Make handling of illegal internal representatives in...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Refactor enumerator for strings (#4014)
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
Fix regression output related to sygus+bv-div-zero...
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
SyGuS must use total bitvector division (#4119)
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
Remove spurious assertion (#4117)
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
Explicitly handle isFinite for rounding modes (#4115)
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
Always enable cbqi literal dependency (#4116)
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
Fix issue with multiple infinities in CEGQI for LIRA...
commit
|
commitdiff
|
tree
2020-03-16
Andrew Reynolds
Handle cases in --sygus-rr where evaluation is not...
commit
|
commitdiff
|
tree
2020-03-13
Andrew Reynolds
Removing a few deprecated options (#4052)
commit
|
commitdiff
|
tree
2020-03-13
Andrew Reynolds
Remove regress for real to int (#4071)
commit
|
commitdiff
|
tree
2020-03-13
Andrew Reynolds
Generalize type rules for strings to sequences (#3987)
commit
|
commitdiff
|
tree
2020-03-13
Andrew Reynolds
Fix case of non-constant value for sygus sampling ...
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Add options for nec regression (#4056)
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Convert most instances of dataypes in parsers to the...
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Do not allow quantifiers over real variables in real...
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Remove local theory extension option (#4048)
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Do not make models for quantified function variables...
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Ensure legal candidate equalities when using relational...
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Fix double notify in equality engine (#4036)
commit
|
commitdiff
|
tree
2020-03-12
Andrew Reynolds
Simplifications to the Datatypes API (#4040)
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Do not enable some SMT-COMP specific options by default...
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Guard against null relevancy condition in SyGuS (#4033)
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Add missing datatype functions to new API (#3930)
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Switch to Nodes for conjecture generator (#4026)
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Remove experimental symmetry breaker (#4005)
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Fix non-parametrized operators in subgoal generation...
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Remove partial instantiation for local theory extensions...
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Fix (#4017)
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Fix duplicate variable issue in sygus-qe-preproc (...
commit
|
commitdiff
|
tree
2020-03-11
Andrew Reynolds
Fix real to int for parameterized kinds (#4016)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Fix options for regression: --sort-inference is incompatible...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Fix sort inference for top-level Boolean variables...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Logic exception instead of assertion failure for instantiate...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Remove assertion in resolution bound inferences (#3980)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Consolidate options that disable produceModels (#3973)
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Fix assertion failure in sort inference for Boolean...
commit
|
commitdiff
|
tree
2020-03-10
Andrew Reynolds
Do not set values for non-linear mult terms in collectModelI...
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
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 aggressive...
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Eliminate spurious assertion (#3976)
commit
|
commitdiff
|
tree
2020-03-09
Andrew Reynolds
Fix type issue in arith rewrite equality (#3972)
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
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-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
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-05
Andrew Reynolds
Migrate a majority of the functionality in parsers...
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-03
Andrew Reynolds
Standardize the interface for SMT engine subsolvers...
commit
|
commitdiff
|
tree
2020-03-02
Andrew Reynolds
Split collect model info by types in strings (#3847)
commit
|
commitdiff
|
tree
next