projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix corner case of wrongly applied selector as trigger (#5786)
[cvc5.git]
/
src
/
theory
/
quantifiers
/
sygus
/
2021-01-11
Andrew Reynolds
Further simplifications in preparation for removing...
tree
|
commitdiff
2020-12-23
Haniel Barbosa
Dumping unsat cores after check-sat-assuming/QUERY...
tree
|
commitdiff
2020-12-18
Andrew Reynolds
Simplify internal API for sygus (#5687)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Consolidate basic sygus utilities regarding sygus conje...
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-11-30
Andrew Reynolds
Remove includes for old API from internal code (#5536)
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Fix for sygusToBuiltinEval for non-ground composite...
tree
|
commitdiff
2020-11-20
Aina Niemetz
RoundingMode: Rename enum values to conform to code...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
tree
|
commitdiff
2020-11-12
Andrew Reynolds
Simplify sygus solver and sygus stream (#5389)
tree
|
commitdiff
2020-11-12
Andrew Reynolds
Fix redundant refinement lemma in sygus solver (#5399)
tree
|
commitdiff
2020-11-06
Andrew Reynolds
Split sygus template inference to its own file (#5388)
tree
|
commitdiff
2020-11-03
Andrew Reynolds
Move sygus qe preproc to its own file (#5375)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
tree
|
commitdiff
2020-10-27
Abdalrhman Mohamed
Refactor DeclareSygusVarCommand and SynthFunCommand...
tree
|
commitdiff
2020-10-21
Abdalrhman Mohamed
Add finishInit for getInterpol and getAbduct. (#5316)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
tree
|
commitdiff
2020-10-05
Aina Niemetz
SyGuS: Add fp.sub to default FP grammar. (#5206)
tree
|
commitdiff
2020-10-05
Andrew Reynolds
Make sygus more robust to unknown responses in solution...
tree
|
commitdiff
2020-10-04
mudathirmahgoub
Remove subtyping for sets theory (#5179)
tree
|
commitdiff
2020-10-02
Aina Niemetz
SyGuS: Add min/max (sub)normal constants to FP default...
tree
|
commitdiff
2020-09-27
Andrew Reynolds
Fix sygus quantifier elimination preprocess for multipl...
tree
|
commitdiff
2020-09-26
Andrew Reynolds
Use original quantified formula for single invocation...
tree
|
commitdiff
2020-09-25
Andrew Reynolds
Make sygus refinement step more robust to unevaluatable...
tree
|
commitdiff
2020-09-24
Aina Niemetz
SyGuS: Add default grammar for FP. (#5133)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-16
Abdalrhman Mohamed
Dump commands in internal code using command printing...
tree
|
commitdiff
2020-09-15
Ying Sheng
Interpolation: Add implementation for SyGuS interpolati...
tree
|
commitdiff
2020-09-03
Andrew Reynolds
Minor cleanup of quantifiers engine (#4994)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Split QuantElimSolver from SmtEngine (#4919)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Fixes for corner case of decision tree learning with...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Fixes for degenerate case of sygus decision tree learni...
tree
|
commitdiff
2020-08-08
Andrew Reynolds
Move datatype index constant to its own file (#4859)
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Split preprocessor from SmtEngine (#4854)
tree
|
commitdiff
2020-08-03
Ying Sheng
Add implementation for SyGuS interpolation module ...
tree
|
commitdiff
2020-07-30
Andrew Reynolds
Fix null case for sygus printing (#4793)
tree
|
commitdiff
2020-07-28
Ying Sheng
fixing issue #4808. (#4810)
tree
|
commitdiff
2020-07-28
Ying Sheng
Interpolation: Add interface for SyGuS interpolation...
tree
|
commitdiff
2020-07-18
Andrew Reynolds
Enumerate shapes feature in fast sygus enumerator ...
tree
|
commitdiff
2020-07-15
Andres Noetzli
Use Nodes for SmtEngine assertions (#4752)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Minor refactoring of subsolver initialization (#4731)
tree
|
commitdiff
2020-07-13
Andrew Reynolds
User-facing print debug option for sygus candidates...
tree
|
commitdiff
2020-07-10
Ying Sheng
[Interpolation] Add interface for SyGuS interpolation...
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
tree
|
commitdiff
2020-06-29
Andres Noetzli
Make ExprManager constructor private (#4669)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
tree
|
commitdiff
2020-06-17
Haniel Barbosa
Improve polynomial anyterm grammar (#3566)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-13
Andrew Reynolds
Move sygus datatype utility functions to their own...
tree
|
commitdiff
2020-06-04
Andrew Reynolds
Add sygus datatype substitution utility method (#4390)
tree
|
commitdiff
2020-06-04
Andrew Reynolds
Fix abduction with datatypes (#4566)
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Fix cached free variable identifiers in sygus term...
tree
|
commitdiff
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
tree
|
commitdiff
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Convert more cases of strings to words (#4206)
tree
|
commitdiff
2020-04-14
Andrew Reynolds
Remove a few spurious assertions (#4294)
tree
|
commitdiff
2020-04-12
Andrew Reynolds
Fixes for extended rewriter (#4278)
tree
|
commitdiff
2020-04-11
Andrew Reynolds
Ensure exported sygus solutions match grammar (#4270)
tree
|
commitdiff
2020-03-25
Andrew Reynolds
Generalize more uses of string-specific functions...
tree
|
commitdiff
2020-03-24
Andrew Reynolds
Restrict cases of sygus grammar reduction based on...
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Infer when sygus operators are equivalent to builtin...
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Simplify auxiliary variable handling in CEGQI (#4141)
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Throw exception for non-well-founded unimplemented...
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Fix sort comparison within assertion in cegis (#4113)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Handle failures for sygus QE preprocess (#4072)
tree
|
commitdiff
2020-03-13
Andrew Reynolds
Removing a few deprecated options (#4052)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Guard against null relevancy condition in SyGuS (#4033)
tree
|
commitdiff
2020-03-10
Aina Niemetz
Fix -Wshadow warnings in sygus_grammar_cons.cpp. (...
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Support default sygus grammar construction for sets...
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-03-03
Andrew Reynolds
Standardize the interface for SMT engine subsolvers...
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Use default consts when not using any const during...
tree
|
commitdiff
2020-02-24
Andrew Reynolds
Fixes for quantifiers documentation (#3811)
tree
|
commitdiff
2020-02-19
Andrew Reynolds
Fix symmetry breaking for multiple sygus types (#3775)
tree
|
commitdiff
2020-02-19
Andrew Reynolds
Delay enumerative instantiation if theory engine does...
tree
|
commitdiff
2020-02-16
Andrew Reynolds
Fix simple issue with cache (#3762)
tree
|
commitdiff
2020-02-11
Andrew Reynolds
Use example evaluation cache instead of sygus PBE ...
tree
|
commitdiff
2020-02-08
Andrew Reynolds
Interface for example evaluation cache utilities (...
tree
|
commitdiff
2020-02-07
Andrew Reynolds
Statistics for fast enumerator (#3699)
tree
|
commitdiff
2020-02-07
Andrew Reynolds
Example evaluation cache utility (#3698)
tree
|
commitdiff
2020-02-03
Andrew Reynolds
Fix invariant template inference for trivially infeasib...
tree
|
commitdiff
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
tree
|
commitdiff
2020-01-31
Andrew Reynolds
Update sygus grammar normalization to use node-level...
tree
|
commitdiff
2020-01-31
Andrew Reynolds
Refactor sygus stats (#3684)
tree
|
commitdiff
2020-01-31
Andrew Reynolds
Minor refactoring of constructor classes in fast enumer...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invoc...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Example minimize evaluation utility. (#3671)
tree
|
commitdiff
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
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-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
tree
|
commitdiff
2020-01-10
Andrew Reynolds
Fix side condition check in sygus core connective ...
tree
|
commitdiff
2020-01-10
Andrew Reynolds
Track trivial cases in transition inference (#3598)
tree
|
commitdiff
next