projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Refactor transcendental solver (#5514)
[cvc5.git] / src / theory / quantifiers /
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
2020-07-18 Andrew ReynoldsEnumerate shapes feature in fast sygus enumerator ... tree | commitdiff
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752) tree | commitdiff
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) tree | commitdiff
2020-07-14 Andrew ReynoldsDebug instantiations output (#4739) tree | commitdiff
2020-07-14 Andrew ReynoldsMinor refactoring of subsolver initialization (#4731) tree | commitdiff
2020-07-14 Andrew ReynoldsFix whitespace issue in instantiations output. (#4737) tree | commitdiff
2020-07-13 Andrew Reynolds User-facing print debug option for sygus candidates... tree | commitdiff
2020-07-13 Andrew ReynoldsStatistics on instantiations per quantified formula... tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-10 Ying Sheng[Interpolation] Add interface for SyGuS interpolation... tree | commitdiff
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) tree | commitdiff
2020-06-29 Andres NoetzliMake ExprManager constructor private (#4669) tree | commitdiff
2020-06-19 Andrew ReynoldsConvert more uses of strings to words (#4584) tree | commitdiff
2020-06-17 Andrew ReynoldsDo not traverse WITNESS for partial substitutions in... tree | commitdiff
2020-06-17 Haniel BarbosaImprove polynomial anyterm grammar (#3566) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-16 Andrew Reynolds(proof-new) Add quantifiers proof checker (#4593) tree | commitdiff
2020-06-13 Andrew ReynoldsMove sygus datatype utility functions to their own... tree | commitdiff
2020-06-04 Andrew ReynoldsAdd sygus datatype substitution utility method (#4390) tree | commitdiff
2020-06-04 Andrew ReynoldsFix abduction with datatypes (#4566) tree | commitdiff
2020-06-03 Andrew ReynoldsUpdate CEGQI to use lemma status instead of forcing... tree | commitdiff
2020-06-03 Andrew ReynoldsUse prenex normal form when using cegqi-nested-qe ... tree | commitdiff
2020-06-02 Andrew ReynoldsFix scope issue with pulling ITEs in extended rewriter... tree | commitdiff
2020-06-02 Andrew ReynoldsDo not handle universal quantification on functions... tree | commitdiff
2020-05-20 Aina NiemetzCegqiBv: Clean up after renaming options. (#4487) tree | commitdiff
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... tree | commitdiff
2020-05-20 Andrew ReynoldsFix cached free variable identifiers in sygus term... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-05-19 Andrew ReynoldsUse fresh variables when miniscoping (#4296) 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-15 Andrew ReynoldsFix assertion in enumerative instantiation (#4313) tree | commitdiff
2020-04-15 Andrew ReynoldsConvert more cases of strings to words (#4206) tree | commitdiff
2020-04-15 Andrew ReynoldsAbort if in conflict in enumerative instantiation ... tree | commitdiff
next