summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-12-16Trace tags for dumping the decision tree in org-mode format (#2871)makaimann
2019-12-15Minor improvement to evaluator (#3570)Andrew Reynolds
2019-12-14Simple optimizations for the core rewriter (#3569)Andrew Reynolds
2019-12-13Eliminate Expr-level calls in TypeNode (#3562)Andrew Reynolds
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-13Disable check-synth-sol in regression with recursive functions (#3560)Andrew Reynolds
2019-12-12 FP converter: convert: Use std::vector as instead of std::stack. (#3563)Aina Niemetz
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-12Fixes for regressions (#3557)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-11Activate node-level datatype API (#3540)Andrew Reynolds
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-11Support symbolic unfolding in UNIF+PI (#3553)Andrew Reynolds
2019-12-10Incorporate rewriting on demand in the evaluator (#3549)Andrew Reynolds
2019-12-10Fix ufho issues (#3551)Haniel Barbosa
2019-12-10Allow unsat cores with sygus inference (#3550)Andrew Reynolds
2019-12-09Disable sygus inference when combined with incremental and proofs (#3539)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-08[Regressions] Require proof support for abduction (#3546)Andres Noetzli
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06Use str.subtr in str.to.int/int.to.str reduction (#3544)Andres Noetzli
2019-12-06Throw exception instead of warning for approximate models (#3542)Andrew Reynolds
2019-12-06Add lemma for str.to.int/int.to.str (#3541)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-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-12-06[proof] Eliminate side-condition from ER signature (#3230)Alex Ozdemir
2019-12-06contrib: Setup all dependencies in deps/ directory. (#3534)Mathias Preiner
2019-12-05Introduce the Node-level Datatypes API (#3462)Andrew Reynolds
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ...Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-04Add mkOp for a single Kind (#3522)makaimann
2019-12-04Fix the subtyping relation for functions (#3494)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-12-04Fix (#3530)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-03Fix corner case in model construction of strings (#3524)Andres Noetzli
2019-12-03Improve flexibility of lemma output in non-linear solver (#3518)Andrew Reynolds
2019-12-03Fix clang-format file for brace wrapping with case labels. (#3523)Aina Niemetz
2019-12-03Rewrite `str.contains` used for character matching (#3519)Andres Noetzli
2019-12-03Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT...makaimann
2019-12-02Minor refactor: rename opterm_black to op_black (#3521)makaimann
2019-12-02[SMT2 Printer] Quote symbols starting with digit (#3517)Andres Noetzli
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ AP...makaimann
2019-12-02 Update ownership policy for dynamic quantifiers splitting (#3493)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback