projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Simplify and fix check models (#5685)
[cvc5.git] / src / smt /
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
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) tree | commitdiff
2020-09-23 Andrew ReynoldsFix type issue with term formula removal (#5107) tree | commitdiff
2020-09-22 Mathias PreinerAdd simple BV solver (#5065) tree | commitdiff
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-18 Andrew ReynoldsFix assertion list for globally defined recursive funct... tree | commitdiff
2020-09-18 Andres NoetzliFix muzzled builds (#5093) tree | commitdiff
2020-09-18 Andrew Reynolds(proof-new) Updates to proof node updater algorithm... tree | commitdiff
2020-09-18 Andrew Reynolds(proof-new) Rewrites involving operators in term conver... tree | commitdiff
2020-09-17 Andrew ReynoldsReduce recursion in term formula removal (#5052) tree | commitdiff
2020-09-17 yoni206Dumping internal define-funs with no arguments (#5077) tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... tree | commitdiff
2020-09-12 Andrew Reynolds(proof-new) Add SMT proof manager (#5054) tree | commitdiff
2020-09-09 Andrew Reynolds(proof-new) Minor changes to proof node updater (#5011) tree | commitdiff
2020-09-09 Andrew Reynolds(proof-new) Make proofs in term formula removal term... tree | commitdiff
2020-09-08 Andres NoetzliMake CVC/API BV div/mod semantics match SMT-LIB (#4997) tree | commitdiff
2020-09-08 Andrew ReynoldsEliminate a custom use of TheorySep in quantifiers... tree | commitdiff
next