projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Support UF in default sygus grammars (#3319)
[cvc5.git]
/
test
/
regress
/
CMakeLists.txt
2019-10-14
Andrew Reynolds
Support UF in default sygus grammars (#3319)
blob
|
commitdiff
|
raw
2019-10-14
Andrew Reynolds
Apply sygus repair constant techniques restricted to...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-14
Andrew Reynolds
Ensure lemmas from sygus repair const are guarded ...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-13
Andrew Reynolds
Eliminate negative constant coefficients in div/mod...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andrew Reynolds
Fix method for getting arithmetic function definition...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andres Noetzli
[CVC Parser] Add support for regular expressions (...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andres Noetzli
Disallow --proof and --incremental (#3332)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-06
Andrew Reynolds
Fix str to int reduction (#3358)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-03
yoni206
Disable proofs for unsupported logics (#3327)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-30
Andrew Reynolds
Avoid cases of empty sygus grammars (#3301)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-29
Andrew Reynolds
Fail single invocation techniques when utility inferenc...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-27
Andrew Reynolds
Fix case of disjunctive conclusion in strings (#3254)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Andrew Reynolds
Fix off by one error in strings flat form explanation...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Andrew Reynolds
Add isParameterized function to Expr (#3303)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
blob
|
commitdiff
|
raw
|
diff to current
2019-09-17
Andrew Reynolds
Avoid computing cardinality when constructing models...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-16
Andrew Reynolds
Fix HO model construction for functions having Boolean...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Fix default grammar construction for arrays when no...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-11
Andrew Reynolds
Fix constructor type printing (#3246)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-04
Mathias Preiner
Remove duplicate regression tests. (#3227)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Infer emptiness instead of splitting when a string...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Exclude redundant lemmas when tracking inst lemmas...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Update dynamic splitting strategy for quantifiers ...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-22
Andrew Reynolds
Local substitutions for context-depdendent simplificat...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-20
Andrew Reynolds
Fixes for sygus inference on quantifier free problems...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-18
Andrew Reynolds
Context-independent regular expression unfolding (...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-14
Andrew Reynolds
Update to standard implementation of getting free...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-13
Andrew Reynolds
Add string rewrite involving allchar stars (#3167)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-08
Mathias Preiner
Fix issues with Ninja build system and add configure...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-06
Andrew Reynolds
Properly parse qualified identifiers (#3111)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Andrew Reynolds
Remove simplification specialized for sygus si solution...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Andrew Reynolds
Support default sygus grammar for strings (#3148)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Andrew Reynolds
Fix solution filtering for streaming abducts (#3143)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Andrew Reynolds
Enable sygus logic when produce-abducts is true (#3144)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-01
Andrew Reynolds
Regular expression intersection modes (#3134)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-31
Haniel Barbosa
Parsing THF and adding several regressions (#3131)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-30
Andrew Reynolds
Minor improvement for rewriter for str.replace (#3124)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-30
Andrew Reynolds
Handle RE intersections modulo equality (#3120)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-29
Andrew Reynolds
Model blocker feature (#3112)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-24
Andrew Reynolds
Fix null node when using no-strings-lazy-pp (#3114)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-23
Andrew Reynolds
Fix sygus datatype parsing in sygus v1 format (#3113)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-19
Andrew Reynolds
Fixes for sygus with datatypes (#3103)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-19
Andrew Reynolds
Fix case of unfolding negative membership in reg exp...
blob
|
commitdiff
|
raw
|
diff to current
2019-07-18
Andrew Reynolds
Basic rewrites for tolower/toupper (#3095)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-16
Andrew Reynolds
Add support for str.tolower and str.toupper (#3092)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-15
Andrew Reynolds
Add string rewrite to distribute character stars over...
blob
|
commitdiff
|
raw
|
diff to current
2019-06-27
Andrew Reynolds
Variable elimination rewrite for quantified strings...
blob
|
commitdiff
|
raw
|
diff to current
2019-06-24
Andrew Reynolds
Stratify unfolding of regular expressions based on...
blob
|
commitdiff
|
raw
|
diff to current
2019-06-21
Andres Noetzli
Fix and simplify handling of --force-logic (#3062)
blob
|
commitdiff
|
raw
|
diff to current
2019-06-10
Andrew Reynolds
Optimization for negative concatenation membership...
blob
|
commitdiff
|
raw
|
diff to current
2019-06-05
Andres Noetzli
Prevent letification from shadowing variables (#3042)
blob
|
commitdiff
|
raw
|
diff to current
2019-06-04
Andres Noetzli
Add check that result matches benchmark status (#3028)
blob
|
commitdiff
|
raw
|
diff to current
2019-06-01
Andrew Reynolds
Fix rewriter for regular expression consume (#3029)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-30
Andres Noetzli
Quote symbol when printing empty symbol name (#3025)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-27
Andres Noetzli
Avoid substituting Boolean term variables (#3022)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-21
Martin
Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-17
Martin
Add the problematic input from issue 2183 as a regressi...
blob
|
commitdiff
|
raw
|
diff to current
2019-05-15
Andres Noetzli
Fix model of Boolean vars with eager bit-blaster (...
blob
|
commitdiff
|
raw
|
diff to current
2019-05-15
Andrew Reynolds
Fix printing of bvurem (#2963)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-09
Andrew Reynolds
Fixes for relational triggers (#2967)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-06
Andres Noetzli
Add support for re.all (#2980)
blob
|
commitdiff
|
raw
|
diff to current
2019-05-01
Andrew Reynolds
Use total versions of div/mod in re-elim-agg (#2986)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-30
Andres Noetzli
Fix concat-find regexp elimination (#2983)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-30
Andrew Reynolds
Remove stoi solve rewrite (#2985)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-30
Andrew Reynolds
Eliminate APPLY kind (#2976)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-17
Andrew Reynolds
Fix extended function decomposition (#2960)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-16
Andres Noetzli
Make bv{add,mul,and,or,xor,xnor} left-associative ...
blob
|
commitdiff
|
raw
|
diff to current
2019-04-16
Andrew Reynolds
Stratify enumerative instantiation (#2954)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-11
Andrew Reynolds
Eliminate Boolean ITE within terms, fixes 2947 (#2949)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-05
Andrew Reynolds
Fix another corner case of datatypes+PBE (#2938)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-03
Andrew Reynolds
Fix combination of datatypes + strings in PBE (#2930)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-01
Andres Noetzli
FP: Fix wrong model due to partial assignment (#2910)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-01
Andres Noetzli
Move slow string regression to regress3 (#2913)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-29
Andrew Reynolds
Apply empty splits more aggressively in sets+cardinalit...
blob
|
commitdiff
|
raw
|
diff to current
2019-03-22
Andrew Reynolds
More fixes for PBE with datatypes (#2882)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-21
Andrew Reynolds
Rewrite selectors correctly applied to constructors...
blob
|
commitdiff
|
raw
|
diff to current
2019-03-20
Andrew Reynolds
Sygus abduction feature (#2744)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-19
Andrew Reynolds
Fix fairness issue with fast sygus enumerator (#2873)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-15
Haniel Barbosa
New beta-reduction for HOL solving (#2869)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-14
Andrew Reynolds
Use zero slope tangent planes for transcendental functi...
blob
|
commitdiff
|
raw
|
diff to current
2019-03-14
Andrew Reynolds
Implement proper semantics for TPTP predicate is_rat...
blob
|
commitdiff
|
raw
|
diff to current
2019-03-12
Andrew Reynolds
Move tuple/record update elimination from ppRewrite...
blob
|
commitdiff
|
raw
|
diff to current
2019-01-22
Andrew Reynolds
Fix tuple and record CVC printing (#2818)
blob
|
commitdiff
|
raw
|
diff to current
2019-01-22
Andrew Reynolds
Fix parsing of overloaded parametric datatype selector...
blob
|
commitdiff
|
raw
|
diff to current
2019-01-17
Andres Noetzli
Add option to print BV constants in binary (#2805)
blob
|
commitdiff
|
raw
|
diff to current
2019-01-16
Andrew Reynolds
Fix constant contains ITOS rewrite (#2799)
blob
|
commitdiff
|
raw
|
diff to current
2019-01-15
Andrew Reynolds
Fix unsound double abs rewrite rule for FP (#2792)
blob
|
commitdiff
|
raw
|
diff to current
2019-01-09
Andrew Reynolds
Do not rewrite 1-constructor sygus testers to true...
blob
|
commitdiff
|
raw
|
diff to current
next