projects / cvc5.git / history
? search:
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 ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2020-12-23 Haniel BarbosaDumping unsat cores after check-sat-assuming/QUERY... tree | commitdiff
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687) tree | commitdiff
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-23 Andrew ReynoldsFix for sygusToBuiltinEval for non-ground composite... tree | commitdiff
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-12 Andrew ReynoldsSimplify sygus solver and sygus stream (#5389) tree | commitdiff
2020-11-12 Andrew ReynoldsFix redundant refinement lemma in sygus solver (#5399) tree | commitdiff
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388) tree | commitdiff
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375) tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) tree | commitdiff
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... tree | commitdiff
2020-10-21 Abdalrhman MohamedAdd finishInit for getInterpol and getAbduct. (#5316) tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-05 Aina NiemetzSyGuS: Add fp.sub to default FP grammar. (#5206) tree | commitdiff
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution... tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-10-02 Aina NiemetzSyGuS: Add min/max (sub)normal constants to FP default... tree | commitdiff
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl... tree | commitdiff
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation... tree | commitdiff
2020-09-25 Andrew ReynoldsMake sygus refinement step more robust to unevaluatable... tree | commitdiff
2020-09-24 Aina NiemetzSyGuS: Add default grammar for FP. (#5133) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... tree | commitdiff
2020-09-03 Andrew ReynoldsMinor cleanup of quantifiers engine (#4994) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-20 Andrew ReynoldsSplit QuantElimSolver from SmtEngine (#4919) tree | commitdiff
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) tree | commitdiff
2020-08-13 Andrew ReynoldsFixes for corner case of decision tree learning with... tree | commitdiff
2020-08-12 Andrew ReynoldsFixes for degenerate case of sygus decision tree learni... tree | commitdiff
2020-08-08 Andrew ReynoldsMove datatype index constant to its own file (#4859) tree | commitdiff
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854) tree | commitdiff
2020-08-03 Ying ShengAdd implementation for SyGuS interpolation module ... tree | commitdiff
2020-07-30 Andrew ReynoldsFix null case for sygus printing (#4793) tree | commitdiff
2020-07-28 Ying Shengfixing issue #4808. (#4810) tree | commitdiff
2020-07-28 Ying ShengInterpolation: Add interface for SyGuS interpolation... tree | commitdiff
2020-07-18 Andrew ReynoldsEnumerate shapes feature in fast sygus enumerator ... tree | commitdiff
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752) tree | commitdiff
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) tree | commitdiff
2020-07-14 Andrew ReynoldsMinor 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 ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) tree | commitdiff
2020-06-29 Andres NoetzliMake ExprManager constructor private (#4669) tree | commitdiff
2020-06-19 Andrew ReynoldsConvert more uses of strings to words (#4584) tree | commitdiff
2020-06-17 Haniel BarbosaImprove polynomial anyterm grammar (#3566) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-13 Andrew ReynoldsMove sygus datatype utility functions to their own... tree | commitdiff
2020-06-04 Andrew ReynoldsAdd sygus datatype substitution utility method (#4390) tree | commitdiff
2020-06-04 Andrew ReynoldsFix abduction with datatypes (#4566) tree | commitdiff
2020-05-20 Andrew ReynoldsFix cached free variable identifiers in sygus term... tree | commitdiff
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) tree | commitdiff
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) tree | commitdiff
2020-04-15 Andrew ReynoldsConvert more cases of strings to words (#4206) tree | commitdiff
2020-04-14 Andrew ReynoldsRemove a few spurious assertions (#4294) tree | commitdiff
2020-04-12 Andrew ReynoldsFixes for extended rewriter (#4278) tree | commitdiff
2020-04-11 Andrew ReynoldsEnsure 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 ReynoldsRestrict cases of sygus grammar reduction based on... tree | commitdiff
2020-03-23 Andrew ReynoldsInfer when sygus operators are equivalent to builtin... tree | commitdiff
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141) tree | commitdiff
2020-03-23 Andrew ReynoldsThrow exception for non-well-founded unimplemented... tree | commitdiff
2020-03-20 Andrew ReynoldsFix sort comparison within assertion in cegis (#4113) tree | commitdiff
2020-03-20 Andrew ReynoldsHandle failures for sygus QE preprocess (#4072) tree | commitdiff
2020-03-13 Andrew ReynoldsRemoving a few deprecated options (#4052) tree | commitdiff
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033) tree | commitdiff
2020-03-10 Aina NiemetzFix -Wshadow warnings in sygus_grammar_cons.cpp. (... tree | commitdiff
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-03-03 Andrew ReynoldsStandardize the interface for SMT engine subsolvers... tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-26 Andrew ReynoldsUse default consts when not using any const during... tree | commitdiff
2020-02-24 Andrew ReynoldsFixes for quantifiers documentation (#3811) tree | commitdiff
2020-02-19 Andrew ReynoldsFix symmetry breaking for multiple sygus types (#3775) tree | commitdiff
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does... tree | commitdiff
2020-02-16 Andrew ReynoldsFix simple issue with cache (#3762) tree | commitdiff
2020-02-11 Andrew ReynoldsUse example evaluation cache instead of sygus PBE ... tree | commitdiff
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (... tree | commitdiff
2020-02-07 Andrew ReynoldsStatistics for fast enumerator (#3699) tree | commitdiff
2020-02-07 Andrew ReynoldsExample evaluation cache utility (#3698) tree | commitdiff
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasib... tree | commitdiff
2020-02-03 Andrew ReynoldsExample inference utility (#3670) tree | commitdiff
2020-01-31 Andrew ReynoldsUpdate sygus grammar normalization to use node-level... tree | commitdiff
2020-01-31 Andrew ReynoldsRefactor sygus stats (#3684) tree | commitdiff
2020-01-31 Andrew ReynoldsMinor refactoring of constructor classes in fast enumer... tree | commitdiff
2020-01-30 Andrew ReynoldsEliminate spurious postprocessing step for single invoc... tree | commitdiff
2020-01-30 Andrew ReynoldsExample minimize evaluation utility. (#3671) tree | commitdiff
2020-01-23 Andrew ReynoldsFix trivial solve method for single invocation (#3650) tree | commitdiff
2020-01-22 Andrew ReynoldsFix check for subtypes in sygus PBE (#3640) tree | commitdiff
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus defau... tree | commitdiff
2020-01-17 Andrew ReynoldsUse axioms when checking goal entailment for abduction... tree | commitdiff
2020-01-14 Andrew ReynoldsGeneralize example-based sym breaking to conjectures... tree | commitdiff
2020-01-10 Andrew ReynoldsFix side condition check in sygus core connective ... tree | commitdiff
2020-01-10 Andrew ReynoldsTrack trivial cases in transition inference (#3598) tree | commitdiff
next