projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Introduce quantifiers inference manager (#5821)
[cvc5.git] / src / theory / quantifiers /
2021-01-26 Andrew ReynoldsIntroduce quantifiers inference manager (#5821) tree | commitdiff
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) tree | commitdiff
2021-01-26 Andrew ReynoldsRefactor quantifiers engine initialization (#5813) tree | commitdiff
2021-01-25 Andrew ReynoldsEnsure uses of ground terms in triggers are preprocesse... tree | commitdiff
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805) tree | commitdiff
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807) tree | commitdiff
2021-01-24 Andrew Reynolds Initial cleaning of e-matching instantiation strategy... tree | commitdiff
2021-01-24 Andrew ReynoldsInitial cleaning of triggers (#5795) tree | commitdiff
2021-01-24 Andrew ReynoldsInitial cleaning of inst match generator (#5794) tree | commitdiff
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) tree | commitdiff
2021-01-20 Andrew ReynoldsRefactoring the single invocation solver (#5706) tree | commitdiff
2021-01-20 Andrew ReynoldsFix type issues with relevant domain computation (... tree | commitdiff
2021-01-20 Andrew ReynoldsFix corner case of wrongly applied selector as trigger... tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-11 Andrew ReynoldsRemove extended rewrite for arithmetic (#5760) tree | commitdiff
2021-01-05 yoni206Adding str.len to triggers (#5746) tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-23 Haniel BarbosaDumping unsat cores after check-sat-assuming/QUERY... tree | commitdiff
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) tree | commitdiff
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) tree | commitdiff
2020-12-21 Andrew ReynoldsFix issue with selector triggers (#5689) tree | commitdiff
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687) tree | commitdiff
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679) tree | commitdiff
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680) tree | commitdiff
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678) tree | commitdiff
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... tree | commitdiff
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas... 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-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) tree | commitdiff
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... 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-12 Andrew Reynolds(proof-new) Proofs for skolemization (#5339) 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-23 Andrew ReynoldsApply alpha equivalence to annotated quantified formula... tree | commitdiff
2020-10-21 Abdalrhman MohamedAdd finishInit for getInterpol and getAbduct. (#5316) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-20 Andrew ReynoldsMake seq.nth a trigger kind (#5314) tree | commitdiff
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat... tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228) 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-03 Aina Niemetzsygus-inst: Add more special BV values. (#5191) tree | commitdiff
2020-10-02 Aina NiemetzSyGuS: Add min/max (sub)normal constants to FP default... tree | commitdiff
2020-10-01 Mathias PreinerAdd additional ground terms to SyGuS instantiation... tree | commitdiff
2020-10-01 Andrew ReynoldsMake SygusSolver use sygus attributes directly (#5172) tree | commitdiff
2020-09-28 Andrew ReynoldsMinor fixes to quantifiers proofs (#5151) 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-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) tree | commitdiff
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... 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 Andrew ReynoldsMove quantifiers engine private to own file (#5053) tree | commitdiff
2020-09-15 Andrew ReynoldsFix needsModel method for CEGQI (#5048) tree | commitdiff
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... tree | commitdiff
2020-09-11 Andrew ReynoldsMove finite model minimization to UF last call effort... tree | commitdiff
2020-09-09 Andrew ReynoldsFixes for regular expressions + sygus (#5044) tree | commitdiff
2020-09-03 Andrew ReynoldsMinor cleanup of quantifiers engine (#4994) tree | commitdiff
2020-09-03 Andrew Reynolds(proof-new) Support proofs of quantifier instantiation... tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) tree | commitdiff
2020-08-28 Andrew Reynolds(new theory) Update TheoryQuantifiers to the new interf... tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) tree | commitdiff
2020-08-20 Andrew ReynoldsSplit QuantElimSolver from SmtEngine (#4919) tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) 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-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-11 Andrew ReynoldsRemove instantiation model true option (#4861) tree | commitdiff
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying... 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-08-03 Andrew ReynoldsGeneralize interface for candidate rewrite database... 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-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
next