projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Set incomplete if not applying ho extensionality (#6281)
[cvc5.git] / src / preprocessing /
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-25 Gereon KremerAdd missing includes. (#6207) tree | commitdiff
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... tree | commitdiff
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126) tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-09 Andrew ReynoldsRemove logic request (#6089) tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Mathias PreinerRemove non-ASCII characters from source files. (#6039) tree | commitdiff
2021-03-02 Mathias PreinerFix nightly errors. (#6034) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-25 Gereon KremerMove (optional) rewrite from TrustSubstitutionMap to... tree | commitdiff
2021-02-25 Mathias PreinerEnable -Werror. (#5969) tree | commitdiff
2021-02-24 Gereon KremerEnsure static-learning adds rewritten assertions. ... tree | commitdiff
2021-02-24 Andrew ReynoldsAdd interface to TheoryState for sort inference and... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry... tree | commitdiff
2021-02-12 Andrew ReynoldsSimplify and fix decision engine's handling of skolem... tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) tree | commitdiff
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811) tree | commitdiff
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... tree | commitdiff
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-09 yoni206Strings arith checks preprocessing pass: step 2 (#5750) tree | commitdiff
2021-01-08 yoni206bv-to-int: avoid binarizing nodes twice (#5749) tree | commitdiff
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747) tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy... tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) tree | commitdiff
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro... tree | commitdiff
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... tree | commitdiff
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ... tree | commitdiff
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) tree | commitdiff
2020-11-14 Andrew Reynolds(proof-new) Proofs for non-clausal simplification ... tree | commitdiff
2020-10-22 Andrew Reynolds(proof-new) Make theory preprocessor user-context depen... tree | commitdiff
2020-10-21 Gereon Kremer(proof-new) Make circuit propagator proof producing... tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-19 Andrew Reynolds(proof-new) Updates to assertions pipeline and preproce... tree | commitdiff
2020-10-19 Andrew Reynolds(proof-new) Update preprocessing pass context for proof... tree | commitdiff
2020-10-16 yoni206bv2int: caching introduced terms (#5283) tree | commitdiff
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) tree | commitdiff
2020-10-13 yoni206bv2int: improving bvand tables (#5235) tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-10 yoni206bv2int: bvand translation code move (#5227) tree | commitdiff
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... tree | commitdiff
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces... tree | commitdiff
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and... tree | commitdiff
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) tree | commitdiff
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-18 yoni206bv2int: quantifiers support (#5080) tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-16 yoni206bv2int: support models in tests (#5068) tree | commitdiff
2020-09-14 yoni206bv2int: simpler translation for plus and times (#5055) tree | commitdiff
2020-09-14 Andres NoetzliFix type for Windows build (#5062) tree | commitdiff
2020-09-12 Andrew Reynolds(proof-new) Add SMT proof manager (#5054) tree | commitdiff
2020-09-10 yoni206bv2int: refactoring the main translation loop (#5051) tree | commitdiff
2020-09-10 yoni206bv2int: improvement in lazy failures (#5020) tree | commitdiff
2020-09-03 yoni206Changing the handled operators in bv2int preprocessing... 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-31 Gereon KremerFix --ackermann in the presence on syntactically differ... tree | commitdiff
2020-08-28 yoni206Incremental support for bv_to_int (#4967) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) tree | commitdiff
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... tree | commitdiff
2020-08-03 Andrew ReynoldsSplit dump manager from SmtEngine (#4824) tree | commitdiff
2020-07-27 Andrew Reynolds(proof-new) Proof production for term formula removal... tree | commitdiff
2020-07-18 Andrew Reynolds(proof-new) Proof recording for assertions pipeline... 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 ReynoldsMinor refactoring of subsolver initialization (#4731) tree | commitdiff
2020-07-11 yoni206Changing bv_to_int options (#4721) tree | commitdiff
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-06-24 Andres Noetzli[unconstrained] Fix gathering of visited-once vars... tree | commitdiff
2020-06-20 Alex OzdemirUse traversal iterators in IntToBv (#4169) tree | commitdiff
2020-06-19 yoni206Bv to int elimination bugfix (#4435) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-03 Andrew ReynoldsDo not apply unconstrained simplification when quantifi... tree | commitdiff
2020-05-21 Andrew ReynoldsFix missing check for cardinality one in unconstrained... tree | commitdiff
2020-05-05 Andrew ReynoldsAlways introduce fresh variable for unconstrained APPLY... tree | commitdiff
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) tree | commitdiff
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233) tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... tree | commitdiff
next