projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)
[cvc5.git] / src / smt /
2021-01-22 Haniel Barbosa[proof-new] Expanding MACRO_RESOLUTION in post-processi... tree | commitdiff
2021-01-20 Andrew ReynoldsDo not track processed in remove term formulas loop... 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-12 yoni206Foreign theory rewrite option (#5763) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-08 Haniel Barbosa[proof-new] Implementing getProof in the API and SMT... tree | commitdiff
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory... tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) tree | commitdiff
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores... tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) tree | commitdiff
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy... tree | commitdiff
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula... tree | commitdiff
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687) tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify term formula removal interface (#5695) tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) tree | commitdiff
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro... tree | commitdiff
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine... tree | commitdiff
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ... tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) 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 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... tree | commitdiff
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) 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 Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) tree | commitdiff
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) tree | commitdiff
2020-11-30 Abdalrhman MohamedEliminate uses of SExpr from the parser. (#5496) tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527) tree | commitdiff
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) tree | commitdiff
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) tree | commitdiff
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model... tree | commitdiff
2020-11-23 Andrew Reynolds(proof-new) Miscellaneous changes from proof-new (... tree | commitdiff
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and... tree | commitdiff
2020-11-23 Gereon KremerAdd get-info :time. (#5485) tree | commitdiff
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... tree | commitdiff
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... tree | commitdiff
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-12 Andrew ReynoldsFix printing of define named function (#5425) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Improve printing and debugging for pedantic... tree | commitdiff
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... 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-27 Gereon KremerDisable --nl-cad option by default (#5350) tree | commitdiff
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) tree | commitdiff
2020-10-22 Gereon KremerUse theoryof-mode=type for QF_NRA (#5326) tree | commitdiff
2020-10-21 Abdalrhman MohamedAdd finishInit for getInterpol and getAbduct. (#5316) tree | commitdiff
2020-10-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-20 Abdalrhman MohamedRemove some Commands from the API. (#5268) tree | commitdiff
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256) tree | commitdiff
2020-10-20 Andrew ReynoldsSplit CheckModels utility to its own file (#5303) 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-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat... tree | commitdiff
2020-10-18 Andrew Reynolds(proof-new) More features for SMT proof post-processor... tree | commitdiff
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277) tree | commitdiff
2020-10-14 Andrew Reynolds(proof-new) Generalize preprocess proof generator ... tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit... tree | commitdiff
2020-10-10 Abdalrhman MohamedProvide API version of some SMT Commands. (#5222) tree | commitdiff
2020-10-09 Andrew Reynolds(proof-new) Theory engine proof producing (#5195) tree | commitdiff
2020-10-08 Andrew Reynolds(proof-new) Fixes and improvements for smt proof postpr... tree | commitdiff
2020-10-06 yoni206bv-to-int: change order of passes (#5208) tree | commitdiff
2020-10-06 Abdalrhman MohamedRecover from some exceptions. (#5203) tree | commitdiff
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution... tree | commitdiff
2020-10-02 Andrew Reynolds(proof-new) Fixes for theory preprocessing proofs ... tree | commitdiff
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear... tree | commitdiff
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces... tree | commitdiff
2020-10-01 Andrew ReynoldsMake SygusSolver use sygus attributes directly (#5172) tree | commitdiff
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate... tree | commitdiff
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Updates to proof node updater (#5156) tree | commitdiff
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153) tree | commitdiff
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) tree | commitdiff
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) tree | commitdiff
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... tree | commitdiff
next