summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-19Fix symmetry breaking for multiple sygus types (#3775)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
2020-02-07Example evaluation cache utility (#3698)Andrew Reynolds
2020-02-06Generalize containsQuantifiers to hasClosure (#3722)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-31Update sygus grammar normalization to use node-level datatype. (#3567)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-30Example minimize evaluation utility. (#3671)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix subtyping for instantiations where internal representatives are chosen (#...Andrew Reynolds
2020-01-22Fix single invocation partition for non-function non-atomic types (#3642)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-17Use axioms when checking goal entailment for abduction algorithm (#3611)Andrew Reynolds
2020-01-14Generalize example-based sym breaking to conjectures with constant function a...Andrew Reynolds
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2020-01-04Fix finiteness check for bounded fmf (#3589)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback