projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Minor refactoring of constructor classes in fast enumerator (#3685)
[cvc5.git]
/
src
/
2020-01-31
Andrew Reynolds
Minor refactoring of constructor classes in fast enumer...
tree
|
commitdiff
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Fix rep set increment for empty domains (#3682)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Make eq chain an aggressive rewrite in extended rewrite...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invoc...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Weaken assertion for models with approximations (#3667)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Move disequality list to solver state in strings (...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Example minimize evaluation utility. (#3671)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
External cache argument for evaluator (#3672)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
tree
|
commitdiff
2020-01-30
Andres Noetzli
Better heuristics for marking congruent variables ...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Modularize more steps in the strings strategy (#3676)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Minor updates to string utilities (#3675)
tree
|
commitdiff
2020-01-30
Alex Ozdemir
expectedType in proof-printing code (#3665)
tree
|
commitdiff
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
tree
|
commitdiff
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithme...
tree
|
commitdiff
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
tree
|
commitdiff
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal represe...
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix substitution in nl solver (#3638)
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus defau...
tree
|
commitdiff
2020-01-17
Andrew Reynolds
Use axioms when checking goal entailment for abduction...
tree
|
commitdiff
2020-01-15
Aina Niemetz
New C++ API: Add nullary constructor for Result. (...
tree
|
commitdiff
2020-01-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
tree
|
commitdiff
2020-01-13
Andres Noetzli
Support arbitrary unsigned integer attributes (#3591)
tree
|
commitdiff
2020-01-10
Andrew Reynolds
Fix side condition check in sygus core connective ...
tree
|
commitdiff
2020-01-10
Mathias Preiner
Fix enum names in AIG bitblaster. (#3599)
tree
|
commitdiff
2020-01-10
Andres Noetzli
Fix printing of models of uninterpreted sorts (#3597)
tree
|
commitdiff
2020-01-10
Andrew Reynolds
Track trivial cases in transition inference (#3598)
tree
|
commitdiff
2020-01-10
Andres Noetzli
Optimize str.substr reduction (#3595)
tree
|
commitdiff
2020-01-08
Andrew Reynolds
Fix backtracking issue in sygus fast enumerator (#3593)
tree
|
commitdiff
2020-01-08
mudathirmahgoub
Universe set cardinality for finite types with finite...
tree
|
commitdiff
2020-01-07
Andrew Reynolds
Fix unary minus parse check (#3594)
tree
|
commitdiff
2020-01-07
Andrew Reynolds
Update any-constant and normalization policies for...
tree
|
commitdiff
2020-01-04
Andrew Reynolds
Fix finiteness check for bounded fmf (#3589)
tree
|
commitdiff
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
tree
|
commitdiff
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
tree
|
commitdiff
2019-12-19
Mathias Preiner
Fix typo in smt_options.toml. (#3579)
tree
|
commitdiff
2019-12-18
Andrew Reynolds
Increment Taylor degree for tangent and secant plane...
tree
|
commitdiff
2019-12-18
Andres Noetzli
Avoid calling rewriter from type checker (#3548)
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-17
Andrew Reynolds
Fix spurious parse error for rational real array consta...
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Use the evaluator utility in the function definition...
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Extend model construction with assignment exclusion...
tree
|
commitdiff
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Move Datatype management to ExprManager (#3568)
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Fix evaluator for non-evaluatable nodes (#3575)
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Revert evaluate as node. (#3574)
tree
|
commitdiff
2019-12-16
makaimann
Trace tags for dumping the decision tree in org-mode...
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Minor improvement to evaluator (#3570)
tree
|
commitdiff
2019-12-15
Andrew Reynolds
Simple optimizations for the core rewriter (#3569)
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Eliminate Expr-level calls in TypeNode (#3562)
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
tree
|
commitdiff
2019-12-13
Aina Niemetz
FP converter: convert: Use std::vector as instead...
tree
|
commitdiff
2019-12-12
Andrew Reynolds
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
tree
|
commitdiff
2019-12-12
Haniel Barbosa
Fix Unif+PI algorithm with symbolic unfolding (#3558)
tree
|
commitdiff
2019-12-12
Andrew Reynolds
Use the node-level datatypes API (#3556)
tree
|
commitdiff
2019-12-12
Andrew Reynolds
Fix CEGIS refinement for recursive functions evaluation...
tree
|
commitdiff
2019-12-12
Andrew Reynolds
Activate node-level datatype API (#3540)
tree
|
commitdiff
2019-12-11
Andrew Reynolds
Do not substitute beneath arithmetic terms in the non...
tree
|
commitdiff
2019-12-11
Andrew Reynolds
Support symbolic unfolding in UNIF+PI (#3553)
tree
|
commitdiff
2019-12-10
Andrew Reynolds
Incorporate rewriting on demand in the evaluator (...
tree
|
commitdiff
2019-12-10
Haniel Barbosa
Fix ufho issues (#3551)
tree
|
commitdiff
2019-12-10
Andrew Reynolds
Allow unsat cores with sygus inference (#3550)
tree
|
commitdiff
2019-12-09
Andrew Reynolds
Disable sygus inference when combined with incremental...
tree
|
commitdiff
2019-12-09
Andrew Reynolds
Fix case of uninterpreted constant instantiation in...
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-12-07
Andres Noetzli
Simplify rewrite for character matching (#3545)
tree
|
commitdiff
2019-12-07
Andres Noetzli
Use str.subtr in str.to.int/int.to.str reduction (...
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Throw exception instead of warning for approximate...
tree
|
commitdiff
2019-12-06
Andres Noetzli
Add lemma for str.to.int/int.to.str (#3541)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Optimize the rewriter for DT_SYGUS_EVAL (#3529)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Add ExprManager as argument to Datatype (#3535)
tree
|
commitdiff
2019-12-06
Alex Ozdemir
[proof] Eliminate side-condition from ER signature...
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Introduce the Node-level Datatypes API (#3462)
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
tree
|
commitdiff
2019-12-05
Andres Noetzli
Bi-directional unrolling of R* regular expressions...
tree
|
commitdiff
2019-12-05
makaimann
Add mkOp for a single Kind (#3522)
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Fix the subtyping relation for functions (#3494)
tree
|
commitdiff
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
tree
|
commitdiff
2019-12-04
Andrew Reynolds
Fixes for SyGuS PBE + templated string concatenations...
tree
|
commitdiff
2019-12-04
Andrew Reynolds
Fix single invocation solution construction for multipl...
tree
|
commitdiff
2019-12-04
Andres Noetzli
Fix corner case in model construction of strings (...
tree
|
commitdiff
2019-12-03
Andrew Reynolds
Improve flexibility of lemma output in non-linear solve...
tree
|
commitdiff
2019-12-03
Andres Noetzli
Rewrite `str.contains` used for character matching...
tree
|
commitdiff
2019-12-03
makaimann
Add isNullHelper to avoid calling API function isNull...
tree
|
commitdiff
2019-12-02
Andres Noetzli
[SMT2 Printer] Quote symbols starting with digit (...
tree
|
commitdiff
2019-12-02
makaimann
OpTerm Refactor: Allow retrieving OpTerm used to create...
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Update ownership policy for dynamic quantifiers splitt...
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
tree
|
commitdiff
2019-12-01
Andres Noetzli
Prevent ref count from reaching zero in BV instantiator...
tree
|
commitdiff
2019-11-30
Haniel Barbosa
improving parsing error messages related to HOL (#3510)
tree
|
commitdiff
2019-11-30
Andrew Reynolds
Fix fast SyGuS enumeration for interpreted constants...
tree
|
commitdiff
2019-11-29
Andrew Reynolds
Check free variables in assertions when using SyGuS...
tree
|
commitdiff
next