projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Refactor transcendental solver (#5514)
[cvc5.git] / src / theory / datatypes /
2020-11-23 Andrew ReynoldsFix for sygusToBuiltinEval for non-ground composite... tree | commitdiff
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Add datatypes inference to proof constructo... tree | commitdiff
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-26 Andrew Reynolds(proof-new) Add datatypes proof checker (#5340) tree | commitdiff
2020-10-26 Andrew ReynoldsSend external equalities from collapse selector as... tree | commitdiff
2020-10-23 Andrew ReynoldsChange datatypes lemma policy for equalities not coming... tree | commitdiff
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ... tree | commitdiff
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275) tree | commitdiff
2020-10-09 Andrew ReynoldsSimplify approach for collapsed selectors over non... tree | commitdiff
2020-10-07 Andrew ReynoldsProcess pending inferences at the beginning of datatype... tree | commitdiff
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-17 Andrew ReynoldsFurther standardization of datatypes (#5076) tree | commitdiff
2020-09-14 Andrew ReynoldsStandardize uses of inference manager in datatypes... tree | commitdiff
2020-09-04 Andrew ReynoldsAdd asLemma flag to theory inference process (#5030) tree | commitdiff
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) tree | commitdiff
2020-09-02 Andrew ReynoldsMinor updates to theory inference manager (#5004) tree | commitdiff
2020-09-02 Gereon KremerUse std::unique_ptr instead of std::shared_ptr for... tree | commitdiff
2020-09-01 Andrew Reynolds (new theory) Update TheoryDatatypes to the new standar... tree | commitdiff
2020-09-01 Andrew ReynoldsAdd TheoryInference base class (#4990) tree | commitdiff
2020-09-01 Andrew ReynoldsAdd the inference manager for datatypes (#4968) tree | commitdiff
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (... tree | commitdiff
2020-08-28 Andrew ReynoldsDo not delay processing equivalence class merges in... tree | commitdiff
2020-08-27 Andrew ReynoldsAdd irrelevant kinds infrastructure to TheoryModel... tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... tree | commitdiff
2020-08-21 Andrew ReynoldsRemove spurious theory methods calls (#4931) tree | commitdiff
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-18 Andrew ReynoldsStandardize collectModelInfo and theory-specific collec... tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) tree | commitdiff
2020-08-08 Andrew ReynoldsMove datatype index constant to its own file (#4859) tree | commitdiff
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... tree | commitdiff
2020-08-02 Andrew ReynoldsUpdates to dtype constructor in preparation for elimina... tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-18 Andrew ReynoldsEnumerate shapes feature in fast sygus enumerator ... tree | commitdiff
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733) tree | commitdiff
2020-07-15 Andres NoetzliUse TypeNode in UninterpretedConstant (#4748) tree | commitdiff
2020-07-15 Andrew ReynoldsSimplify entailment check interface (#4744) tree | commitdiff
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-06-30 Ying ShengInterpolation step 1 (#4638) 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-06 Andrew ReynoldsSmt2 parsing support for nested recursive datatypes... tree | commitdiff
2020-06-05 Andrew ReynoldsDatatypes with nested recursion are not handled in... tree | commitdiff
2020-06-04 Andrew ReynoldsAdd sygus datatype substitution utility method (#4390) 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-11 Andrew ReynoldsEnsure exported sygus solutions match grammar (#4270) tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-30 Andrew ReynoldsRemove ref skolem datatype option (#4185) 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 Andrew ReynoldsRename sygus option name (#3977) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-20 Andrew ReynoldsMinor removals (#3786) tree | commitdiff
2020-02-19 Andrew ReynoldsFix symmetry breaking for multiple sygus types (#3775) tree | commitdiff
2020-02-11 Andrew ReynoldsUse example evaluation cache instead of sygus PBE ... tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-13 Andrew ReynoldsEliminate Expr-level calls in TypeNode (#3562) tree | commitdiff
2019-12-12 Andrew ReynoldsUse the node-level datatypes API (#3556) tree | commitdiff
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) tree | commitdiff
2019-12-06 Andrew ReynoldsOptimize the rewriter for DT_SYGUS_EVAL (#3529) tree | commitdiff
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486) tree | commitdiff
2019-11-15 Andrew ReynoldsIntroduce SyGuS datatype API (#3465) tree | commitdiff
2019-11-11 Andrew ReynoldsEliminate remaining references to type/expr in datatype... tree | commitdiff
2019-11-06 Andrew ReynoldsMigrate more datatype methods to the Node level (#3443) tree | commitdiff
2019-11-05 Andrew ReynoldsRefactor type matcher utility (#3439) tree | commitdiff
2019-11-01 Andrew ReynoldsFix non-termination in datatype type enumerator (#3369) tree | commitdiff
2019-11-01 Andrew ReynoldsEagerly beta reduce during sygus to builtin term conver... tree | commitdiff
2019-11-01 Andrew ReynoldsRename datatypes sygus solver (#3417) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-17 Andrew Reynolds Move datatype utility functions to own file (#3397) tree | commitdiff
2019-10-04 Andrew ReynoldsAvoid duplicate lemmas in datatypes (#3310) tree | commitdiff
2019-09-28 Andrew ReynoldsSupport smt2 language "match" term (#3258) tree | commitdiff
2019-09-16 Andrew ReynoldsSygus type info class (#3187) tree | commitdiff
2019-08-05 Andrew ReynoldsRemove forward declarations in quantifiers engine ... tree | commitdiff
2019-06-11 Andrew ReynoldsDo not require sygus constructors to be flattened ... tree | commitdiff
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-26 Andrew ReynoldsFix a few warnings (#2898) tree | commitdiff
2019-03-21 Andrew ReynoldsRewrite selectors correctly applied to constructors... tree | commitdiff
2019-03-14 Andrew ReynoldsGeneralize sygus-rr-verify for fast enumerator (#2829) tree | commitdiff
2019-03-12 Andrew Reynolds Move tuple/record update elimination from ppRewrite... tree | commitdiff
2019-01-15 Andrew Reynolds Only check disequal terms with sygus-rr-verify (#2793) tree | commitdiff
2019-01-09 Andrew ReynoldsDo not rewrite 1-constructor sygus testers to true... tree | commitdiff
2018-12-20 Aina NiemetzAdd missing type rules for parameterized operator kinds... tree | commitdiff
2018-11-27 Andrew ReynoldsMake (T)NodeTrie a general utility (#2489) tree | commitdiff
2018-11-27 Andrew ReynoldsFix coverity warnings in datatypes (#2553) tree | commitdiff
2018-11-21 Andrew ReynoldsSupport string replace all (#2704) tree | commitdiff
2018-11-06 Andrew ReynoldsIncorporate static PBE symmetry breaking lemmas into... tree | commitdiff
2018-10-23 Andrew ReynoldsDo not use lazy trie for sygus-rr-verify (#2668) tree | commitdiff
next