projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Fix component contains for splicing due to substring. (#4705)
[cvc5.git]
/
test
/
regress
/
CMakeLists.txt
2020-03-11
Andres Noetzli
Set assertion in `CnfStream::ensureLiteral()` (#3927)
blob
|
commitdiff
|
raw
2020-03-11
Andrew Reynolds
Fix real to int for parameterized kinds (#4016)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Fix sort inference for top-level Boolean variables...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Aina Niemetz
Fix issue with reset-assertions. (#3988)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Fix assertion failure in sort inference for Boolean...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Do not set values for non-linear mult terms in collectM...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Fix real as int for incremental (#3979)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Do not traverse quantifiers in nl ext purify (#3982)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
makaimann
Enhancement: make the bool-to-bv pass more robust and...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Ensure standard miniscoping is applied before aggressiv...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-09
Andrew Reynolds
Fix type issue in arith rewrite equality (#3972)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-09
Andres Noetzli
Make registration of unit clauses more robust (#3965)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-09
Andrew Reynolds
Rewrite again full for DIV rewrite (#3945)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-08
Ying Sheng
Explicit end marker for models printed in the CVC langu...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-06
Andrew Reynolds
Support default sygus grammar construction for sets...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Andrew Reynolds
Fix issues with real to int (#3918)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-29
Andrew Reynolds
Throw warning instead of error for non-constant values...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-29
Andrew Reynolds
Fix assertion related to assignability in the model...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-29
Andrew Reynolds
Replace conditional rewrite pass in quantifiers with...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-27
Andrew Reynolds
Fix large models for strings (#3835)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-27
Andrew Reynolds
Add support for is_digit and regular expression differe...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-27
Andrew Reynolds
Disable regression that times out on debug (#3833)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Use side effect utility for non-linear lemmas (#3780)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Use default consts when not using any const during...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Fix node arity issue in reduction of int2bv (#3777)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Support for witnessing choice in models (#3781)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-25
yoni206
bv_to_int preprocessing pass
blob
|
commitdiff
|
raw
|
diff to current
2020-02-24
Andres Noetzli
Make lambda rewriter more robust (#3806)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-22
Alex Ozdemir
Switch to th_lira.plf (#3741)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-21
Andrew Reynolds
Simple changes towards unicode string standard (#3791)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-19
Andrew Reynolds
Delay enumerative instantiation if theory engine does...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-17
Andrew Reynolds
Fix soundness bug in reduction of integer div/mod...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-16
Andrew Reynolds
Disable regression (#3761)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-12
Andrew Reynolds
Ensure ext rewrites for associative ops dont throw...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-11
Andrew Reynolds
Fix term simplification based on entailment in quantifi...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-08
Andres Noetzli
Make "unknown" non-critical for unsat cores check ...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-07
mudathirmahgoub
Univeset Cardinality constraints for infinite types...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-07
Andrew Reynolds
Refactor check-model handling in SmtEngine (#3723)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-07
Andrew Reynolds
Fix exact sqrt (#3721)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-04
Alex Ozdemir
Regression tests for arithmetic proofs. (#3701)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
mudathirmahgoub
Fix cardinality of uninterpreted types when univset...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
Andrew Reynolds
Split on model values when repaired model from non...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
Andrew Reynolds
Fix invariant template inference for trivially infeasib...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
Andrew Reynolds
Fix corner case of empty domains in bounded fmf (#3690)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-31
Andrew Reynolds
Refactor relevance vectors for asserted quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Fix rep set increment for empty domains (#3682)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Make eq chain an aggressive rewrite in extended rewrite...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invoc...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Weaken assertion for models with approximations (#3667)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithme...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal represe...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus defau...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-10
Andrew Reynolds
Fix side condition check in sygus core connective ...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-10
Andres Noetzli
Fix printing of models of uninterpreted sorts (#3597)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-10
Andrew Reynolds
Track trivial cases in transition inference (#3598)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-08
Andrew Reynolds
Fix backtracking issue in sygus fast enumerator (#3593)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-08
mudathirmahgoub
Universe set cardinality for finite types with finite...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-07
Andrew Reynolds
Update any-constant and normalization policies for...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-04
Andrew Reynolds
Fix finiteness check for bounded fmf (#3589)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-18
Andrew Reynolds
Increment Taylor degree for tangent and secant plane...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-18
Andres Noetzli
Avoid calling rewriter from type checker (#3548)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-17
Andrew Reynolds
Fix spurious parse error for rational real array consta...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Andrew Reynolds
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Haniel Barbosa
Fix Unif+PI algorithm with symbolic unfolding (#3558)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Andrew Reynolds
Fixes for regressions (#3557)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Andrew Reynolds
Fix CEGIS refinement for recursive functions evaluation...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-11
Andrew Reynolds
Do not substitute beneath arithmetic terms in the non...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-09
Andrew Reynolds
Fix case of uninterpreted constant instantiation in...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andres Noetzli
Bi-directional unrolling of R* regular expressions...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andrew Reynolds
Fix the subtyping relation for functions (#3494)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-04
Andrew Reynolds
Fix single invocation solution construction for multipl...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andres Noetzli
[SMT2 Printer] Quote symbols starting with digit (...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andrew Reynolds
Update ownership policy for dynamic quantifiers splitt...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-30
Andrew Reynolds
Fix fast SyGuS enumeration for interpreted constants...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Andrew Reynolds
Fix sygus inference for choice functions introduced...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Haniel Barbosa
Enable sygusRecFun by default and fixes SyGuS+RecFun...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Andrew Reynolds
Fix indexof range lemma (#3499)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-25
Andrew Reynolds
Better front-end type checking for SyGuS (#3496)
blob
|
commitdiff
|
raw
|
diff to current
next