summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-16Use the evaluator utility in the function definition evaluator (#3576)Andrew Reynolds
2019-12-16Fix evaluator for non-evaluatable nodes (#3575)Andrew Reynolds
2019-12-13Eliminate Expr-level calls in TypeNode (#3562)Andrew Reynolds
2019-12-12Make CEGIS sampling robust to non-vanilla CEGIS (#3559)Andrew Reynolds
2019-12-12Fix Unif+PI algorithm with symbolic unfolding (#3558)Haniel Barbosa
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-11Support symbolic unfolding in UNIF+PI (#3553)Andrew Reynolds
2019-12-09Fix case of uninterpreted constant instantiation in FMF (#3543)Andrew Reynolds
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-12-06Optimize the rewriter for DT_SYGUS_EVAL (#3529)Andrew Reynolds
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-12-04Fixes for SyGuS PBE + templated string concatenations + datatypes (#3492)Andrew Reynolds
2019-12-04Fix single invocation solution construction for multiple function case (#3516)Andrew Reynolds
2019-12-02 Update ownership policy for dynamic quantifiers splitting (#3493)Andrew Reynolds
2019-12-01Prevent ref count from reaching zero in BV instantiator (#3512)Andres Noetzli
2019-11-29Fix fast SyGuS enumeration for interpreted constants (#3501)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-25Better front-end type checking for SyGuS (#3496)Andrew Reynolds
2019-11-21hard limit for rec-fun eval (#3485)Haniel Barbosa
2019-11-21Evaluation unfolding for symbolic SyGuS constructors (#3483)Andrew Reynolds
2019-11-20Lazy evaluation via rec-funs of ITE expressions (#3482)Haniel Barbosa
2019-11-18Use standard sygus interface for abduction and rewrite rule synthesis (#3471)Andrew Reynolds
2019-11-18Improve interface for sygus datatype, fix utilities (#3473)Andrew Reynolds
2019-11-15Use standard interface for sygus default grammar construction (#3466)Andrew Reynolds
2019-11-15Introduce SyGuS datatype API (#3465)Andrew Reynolds
2019-11-10Fix bugs related to sygus higher-order + recursive functions (#3448)Andrew Reynolds
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-05Refactor type matcher utility (#3439)Andrew Reynolds
2019-11-04Make check synth solution robust to auxiliary assertions (#3432)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-11-04Eliminate deprecated utility function from sygus (#3431)Andrew Reynolds
2019-11-01Fix non-termination in datatype type enumerator (#3369)Andrew Reynolds
2019-11-01Eagerly beta reduce during sygus to builtin term conversion (#3418)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-17 Move datatype utility functions to own file (#3397)Andrew Reynolds
2019-10-14Support UF in default sygus grammars (#3319)Andrew Reynolds
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-10-14Ensure lemmas from sygus repair const are guarded (#3385)Andrew Reynolds
2019-10-10Warning instead of assertion for failing propagating instance (#3380)Andrew Reynolds
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-10-08Fix method for getting arithmetic function definition body (#3371)Andrew Reynolds
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
2019-09-17 Encapsulate relevant domain (#3293)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback