projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix rewrite rules sat regressions (#3734)
2020-02-08 Andrew ReynoldsFix rewrite rules sat regressions (#3734)
 commit | commitdiff | tree
2020-02-08 Andrew ReynoldsSplit strings finite model finding strategy (#3727)
 commit | commitdiff | tree
2020-02-08 Andrew ReynoldsSplit core solver from the theory of strings (#3713)
 commit | commitdiff | tree
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (...
commit | commitdiff | tree
2020-02-07 Andrew ReynoldsRefactor check-model handling in SmtEngine (#3723)
 commit | commitdiff | tree
2020-02-07 Andrew ReynoldsStatistics for fast enumerator (#3699)
 commit | commitdiff | tree
2020-02-07 Andrew ReynoldsExample evaluation cache utility (#3698)
 commit | commitdiff | tree
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721)
 commit | commitdiff | tree
2020-02-06 Andrew ReynoldsGeneralize containsQuantifiers to hasClosure (#3722)
 commit | commitdiff | tree
2020-02-05 Andrew ReynoldsFix QF_NIA smt comp script (#3715)
 commit | commitdiff | tree
2020-02-04 Andrew ReynoldsSplit base solver from the theory of strings (#3680)
 commit | commitdiff | tree
2020-02-03 Andrew ReynoldsUtility function for getting component types (#3703)
 commit | commitdiff | tree
2020-02-03 Andrew ReynoldsMinor fixes to regressions (#3702)
 commit | commitdiff | tree
2020-02-03 Andrew ReynoldsSplit on model values when repaired model from non...
commit | commitdiff | tree
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasible...
commit | commitdiff | tree
2020-02-03 Andrew ReynoldsFix corner case of empty domains in bounded fmf (#3690)
 commit | commitdiff | tree
2020-02-03 Andrew ReynoldsExample inference utility (#3670)
 commit | commitdiff | tree
2020-01-31 Andrew ReynoldsAllow PBE symmetry breaking with sygus stream (#3686)
 commit | commitdiff | tree
2020-01-31 Andrew ReynoldsRefactor relevance vectors for asserted quantifiers...
commit | commitdiff | tree
2020-01-31 Andrew ReynoldsUpdate sygus grammar normalization to use node-level...
commit | commitdiff | tree
2020-01-31 Andrew ReynoldsRefactor sygus stats (#3684)
 commit | commitdiff | tree
2020-01-31 Andrew ReynoldsMinor refactoring of constructor classes in fast enumerator...
commit | commitdiff | tree
2020-01-30 Andrew ReynoldsFix rep set increment for empty domains (#3682)
 commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMake eq chain an aggressive rewrite in extended rewriter...
commit | commitdiff | tree
2020-01-30 Andrew ReynoldsEliminate spurious postprocessing step for single invocation...
commit | commitdiff | tree
2020-01-30 Andrew ReynoldsEnsure literals in FMF decision strategies are in the...
commit | commitdiff | tree
2020-01-30 Andrew ReynoldsWeaken assertion for models with approximations (#3667)
 commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMove disequality list to solver state in strings (...
commit | commitdiff | tree
2020-01-30 Andrew ReynoldsExample minimize evaluation utility. (#3671)
 commit | commitdiff | tree
2020-01-30 Andrew ReynoldsExternal cache argument for evaluator (#3672)
 commit | commitdiff | tree
2020-01-30 Andrew ReynoldsDo not debug check model for models with approximations...
commit | commitdiff | tree
2020-01-30 Andrew ReynoldsModularize more steps in the strings strategy (#3676)
 commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMinor updates to string utilities (#3675)
 commit | commitdiff | tree
2020-01-29 Andrew ReynoldsFix isLeq function in String utility (#3659)
 commit | commitdiff | tree
2020-01-28 Andrew ReynoldsDo not insist on bound values being constant in arithmetic...
commit | commitdiff | tree
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (...
commit | commitdiff | tree
2020-01-23 Andrew ReynoldsFix trivial solve method for single invocation (#3650)
 commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix subtyping for instantiations where internal representati...
commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix substitution in nl solver (#3638)
 commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix single invocation partition for non-function non...
commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix check for subtypes in sygus PBE (#3640)
 commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus default...
commit | commitdiff | tree
2020-01-17 Andrew ReynoldsUse axioms when checking goal entailment for abduction...
commit | commitdiff | tree
2020-01-14 Andrew ReynoldsGeneralize example-based sym breaking to conjectures...
commit | commitdiff | tree
2020-01-10 Andrew ReynoldsFix side condition check in sygus core connective ...
commit | commitdiff | tree
2020-01-10 Andrew ReynoldsTrack trivial cases in transition inference (#3598)
 commit | commitdiff | tree
2020-01-08 Andrew ReynoldsFix backtracking issue in sygus fast enumerator (#3593)
 commit | commitdiff | tree
2020-01-07 Andrew ReynoldsFix unary minus parse check (#3594)
 commit | commitdiff | tree
2020-01-07 Andrew ReynoldsUpdate any-constant and normalization policies for...
commit | commitdiff | tree
2020-01-04 Andrew ReynoldsFix finiteness check for bounded fmf (#3589)
 commit | commitdiff | tree
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581)
 commit | commitdiff | tree
2019-12-18 Andrew ReynoldsIncrement Taylor degree for tangent and secant plane...
commit | commitdiff | tree
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array constants...
commit | commitdiff | tree
2019-12-16 Andrew ReynoldsUse the evaluator utility in the function definition...
commit | commitdiff | tree
2019-12-16 Andrew ReynoldsExtend model construction with assignment exclusion...
commit | commitdiff | tree
2019-12-16 Andrew ReynoldsMove Datatype management to ExprManager (#3568)
 commit | commitdiff | tree
2019-12-16 Andrew ReynoldsFix evaluator for non-evaluatable nodes (#3575)
 commit | commitdiff | tree
2019-12-16 Andrew ReynoldsRevert evaluate as node. (#3574)
 commit | commitdiff | tree
2019-12-16 Andrew ReynoldsMinor improvement to evaluator (#3570)
 commit | commitdiff | tree
2019-12-15 Andrew ReynoldsSimple optimizations for the core rewriter (#3569)
 commit | commitdiff | tree
2019-12-13 Andrew ReynoldsEliminate Expr-level calls in TypeNode (#3562)
 commit | commitdiff | tree
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312)
 commit | commitdiff | tree
2019-12-13 Andrew ReynoldsDisable check-synth-sol in regression with recursive...
commit | commitdiff | tree
2019-12-12 Andrew ReynoldsMake CEGIS sampling robust to non-vanilla CEGIS (#3559)
 commit | commitdiff | tree
2019-12-12 Andrew ReynoldsUse the node-level datatypes API (#3556)
 commit | commitdiff | tree
2019-12-12 Andrew ReynoldsFixes for regressions (#3557)
 commit | commitdiff | tree
2019-12-12 Andrew ReynoldsFix CEGIS refinement for recursive functions evaluation...
commit | commitdiff | tree
2019-12-12 Andrew ReynoldsActivate node-level datatype API (#3540)
 commit | commitdiff | tree
2019-12-11 Andrew ReynoldsDo not substitute beneath arithmetic terms in the non...
commit | commitdiff | tree
2019-12-11 Andrew ReynoldsSupport symbolic unfolding in UNIF+PI (#3553)
 commit | commitdiff | tree
2019-12-10 Andrew ReynoldsIncorporate rewriting on demand in the evaluator (...
commit | commitdiff | tree
2019-12-10 Andrew ReynoldsAllow unsat cores with sygus inference (#3550)
 commit | commitdiff | tree
2019-12-09 Andrew ReynoldsDisable sygus inference when combined with incremental...
commit | commitdiff | tree
2019-12-09 Andrew ReynoldsFix case of uninterpreted constant instantiation in...
commit | commitdiff | tree
2019-12-06 Andrew ReynoldsThrow exception instead of warning for approximate...
commit | commitdiff | tree
2019-12-06 Andrew ReynoldsOptimize the rewriter for DT_SYGUS_EVAL (#3529)
 commit | commitdiff | tree
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based...
commit | commitdiff | tree
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535)
 commit | commitdiff | tree
2019-12-06 Andrew ReynoldsIntroduce the Node-level Datatypes API (#3462)
 commit | commitdiff | tree
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from...
commit | commitdiff | tree
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531)
 commit | commitdiff | tree
2019-12-05 Andrew ReynoldsFix the subtyping relation for functions (#3494)
 commit | commitdiff | tree
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486)
 commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFix (#3530)
 commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFixes for SyGuS PBE + templated string concatenations...
commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFix single invocation solution construction for multiple...
commit | commitdiff | tree
2019-12-03 Andrew ReynoldsImprove 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 ReynoldsFix case of higher-order + sygus inference (#3509)
 commit | commitdiff | tree
2019-12-02 Andrew ReynoldsEnsure quantifiers options are set with --no-strings...
commit | commitdiff | tree
2019-11-30 Andrew ReynoldsFix fast SyGuS enumeration for interpreted constants...
commit | commitdiff | tree
2019-11-29 Andrew ReynoldsCheck free variables in assertions when using SyGuS...
commit | commitdiff | tree
2019-11-27 Andrew ReynoldsFix 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 ReynoldsBetter front-end type checking for SyGuS (#3496)
 commit | commitdiff | tree
2019-11-22 Andrew ReynoldsMinor refactoring of compute model value for nl (#3489)
 commit | commitdiff | tree
2019-11-21 Andrew ReynoldsEvaluation unfolding for symbolic SyGuS constructors...
commit | commitdiff | tree
2019-11-18 Andrew ReynoldsUse standard sygus interface for abduction and rewrite...
commit | commitdiff | tree
2019-11-18 Andrew ReynoldsImprove interface for sygus datatype, fix utilities...
commit | commitdiff | tree
2019-11-18 Andrew ReynoldsUpdates to the unit tests, api, and examples for datatypes...
commit | commitdiff | tree
next