projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Use example evaluation cache instead of sygus PBE (#3733)
2020-02-11
Andrew Reynolds
Use example evaluation cache instead of sygus PBE ...
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Fix rewrite rules sat regressions (#3734)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Split strings finite model finding strategy (#3727)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Split core solver from the theory of strings (#3713)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Interface for example evaluation cache utilities (...
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Refactor check-model handling in SmtEngine (#3723)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Statistics for fast enumerator (#3699)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Example evaluation cache utility (#3698)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Fix exact sqrt (#3721)
commit
|
commitdiff
|
tree
2020-02-06
Andrew Reynolds
Generalize containsQuantifiers to hasClosure (#3722)
commit
|
commitdiff
|
tree
2020-02-05
Andrew Reynolds
Fix QF_NIA smt comp script (#3715)
commit
|
commitdiff
|
tree
2020-02-04
Andrew Reynolds
Split base solver from the theory of strings (#3680)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Utility function for getting component types (#3703)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Minor fixes to regressions (#3702)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Split on model values when repaired model from non...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Fix invariant template inference for trivially infeasible...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Fix corner case of empty domains in bounded fmf (#3690)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Allow PBE symmetry breaking with sygus stream (#3686)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Refactor relevance vectors for asserted quantifiers...
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Update sygus grammar normalization to use node-level...
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Refactor sygus stats (#3684)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Minor refactoring of constructor classes in fast enumerator...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Fix rep set increment for empty domains (#3682)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Make eq chain an aggressive rewrite in extended rewriter...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invocation...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Weaken assertion for models with approximations (#3667)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Move disequality list to solver state in strings (...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Example minimize evaluation utility. (#3671)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
External cache argument for evaluator (#3672)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Modularize more steps in the strings strategy (#3676)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Minor updates to string utilities (#3675)
commit
|
commitdiff
|
tree
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithmetic...
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
commit
|
commitdiff
|
tree
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal representati...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix substitution in nl solver (#3638)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus default...
commit
|
commitdiff
|
tree
2020-01-17
Andrew Reynolds
Use axioms when checking goal entailment for abduction...
commit
|
commitdiff
|
tree
2020-01-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
commit
|
commitdiff
|
tree
2020-01-10
Andrew Reynolds
Fix side condition check in sygus core connective ...
commit
|
commitdiff
|
tree
2020-01-10
Andrew Reynolds
Track trivial cases in transition inference (#3598)
commit
|
commitdiff
|
tree
2020-01-08
Andrew Reynolds
Fix backtracking issue in sygus fast enumerator (#3593)
commit
|
commitdiff
|
tree
2020-01-07
Andrew Reynolds
Fix unary minus parse check (#3594)
commit
|
commitdiff
|
tree
2020-01-07
Andrew Reynolds
Update any-constant and normalization policies for...
commit
|
commitdiff
|
tree
2020-01-04
Andrew Reynolds
Fix finiteness check for bounded fmf (#3589)
commit
|
commitdiff
|
tree
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
commit
|
commitdiff
|
tree
2019-12-18
Andrew Reynolds
Increment Taylor degree for tangent and secant plane...
commit
|
commitdiff
|
tree
2019-12-17
Andrew Reynolds
Fix spurious parse error for rational real array constants...
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Use the evaluator utility in the function definition...
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Extend model construction with assignment exclusion...
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Move Datatype management to ExprManager (#3568)
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Fix evaluator for non-evaluatable nodes (#3575)
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Revert evaluate as node. (#3574)
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Minor improvement to evaluator (#3570)
commit
|
commitdiff
|
tree
2019-12-15
Andrew Reynolds
Simple optimizations for the core rewriter (#3569)
commit
|
commitdiff
|
tree
2019-12-13
Andrew Reynolds
Eliminate Expr-level calls in TypeNode (#3562)
commit
|
commitdiff
|
tree
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
commit
|
commitdiff
|
tree
2019-12-13
Andrew Reynolds
Disable check-synth-sol in regression with recursive...
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Use the node-level datatypes API (#3556)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Fixes for regressions (#3557)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Fix CEGIS refinement for recursive functions evaluation...
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Activate node-level datatype API (#3540)
commit
|
commitdiff
|
tree
2019-12-11
Andrew Reynolds
Do not substitute beneath arithmetic terms in the non...
commit
|
commitdiff
|
tree
2019-12-11
Andrew Reynolds
Support symbolic unfolding in UNIF+PI (#3553)
commit
|
commitdiff
|
tree
2019-12-10
Andrew Reynolds
Incorporate rewriting on demand in the evaluator (...
commit
|
commitdiff
|
tree
2019-12-10
Andrew Reynolds
Allow unsat cores with sygus inference (#3550)
commit
|
commitdiff
|
tree
2019-12-09
Andrew Reynolds
Disable sygus inference when combined with incremental...
commit
|
commitdiff
|
tree
2019-12-09
Andrew Reynolds
Fix case of uninterpreted constant instantiation in...
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
Throw exception instead of warning for approximate...
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
Optimize the rewriter for DT_SYGUS_EVAL (#3529)
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
Add ExprManager as argument to Datatype (#3535)
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
Introduce the Node-level Datatypes API (#3462)
commit
|
commitdiff
|
tree
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
commit
|
commitdiff
|
tree
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
commit
|
commitdiff
|
tree
2019-12-05
Andrew Reynolds
Fix the subtyping relation for functions (#3494)
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
Fix (#3530)
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
Fixes for SyGuS PBE + templated string concatenations...
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
Fix single invocation solution construction for multiple...
commit
|
commitdiff
|
tree
2019-12-03
Andrew Reynolds
Improve flexibility of lemma output in non-linear solver...
commit
|
commitdiff
|
tree
2019-12-02
Andrew Reynolds
Update ownership policy for dynamic quantifiers splitting...
commit
|
commitdiff
|
tree
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
commit
|
commitdiff
|
tree
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
commit
|
commitdiff
|
tree
2019-11-30
Andrew Reynolds
Fix fast SyGuS enumeration for interpreted constants...
commit
|
commitdiff
|
tree
2019-11-29
Andrew Reynolds
Check free variables in assertions when using SyGuS...
commit
|
commitdiff
|
tree
2019-11-27
Andrew Reynolds
Fix sygus inference for choice functions introduced...
commit
|
commitdiff
|
tree
2019-11-27
Andrew Reynolds
Fix indexof range lemma (#3499)
commit
|
commitdiff
|
tree
2019-11-25
Andrew Reynolds
Better front-end type checking for SyGuS (#3496)
commit
|
commitdiff
|
tree
2019-11-22
Andrew Reynolds
Minor refactoring of compute model value for nl (#3489)
commit
|
commitdiff
|
tree
2019-11-21
Andrew Reynolds
Evaluation unfolding for symbolic SyGuS constructors...
commit
|
commitdiff
|
tree
2019-11-18
Andrew Reynolds
Use standard sygus interface for abduction and rewrite...
commit
|
commitdiff
|
tree
2019-11-18
Andrew Reynolds
Improve interface for sygus datatype, fix utilities...
commit
|
commitdiff
|
tree
next