projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix regression option (#4680)
[cvc5.git] / src / smt /
2020-06-30 Ying ShengInterpolation step 1 (#4638) tree | commitdiff
2020-06-25 Andrew ReynoldsRemove sygus1 parser (#4651) tree | commitdiff
2020-06-25 Andrew ReynoldsUpdate option --nl-ext to enable/disable incremental... tree | commitdiff
2020-06-23 Mathias PreinerAdd support for eqrange predicate (#4562) tree | commitdiff
2020-06-22 Andrew Reynolds(proof-new) Add proof-new to options file (#4641) tree | commitdiff
2020-06-19 yoni206Bv to int elimination bugfix (#4435) tree | commitdiff
2020-06-19 Andres NoetzliAdd logic check for define-fun(s)-rec (#4577) tree | commitdiff
2020-06-18 Andres NoetzliImprove memory management in Java bindings (#4629) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-12 Andrew ReynoldsUpdate to consistent policy for removed terms in quanti... tree | commitdiff
2020-06-06 Andres NoetzliKeep definitions when global-declarations enabled ... tree | commitdiff
2020-06-04 Aina NiemetzNew C++ Api: Second and last batch of API guards. ... tree | commitdiff
2020-06-03 Andrew ReynoldsUse prenex normal form when using cegqi-nested-qe ... tree | commitdiff
2020-06-01 Andres NoetzliSet theoryof-mode after theory widening (#4545) tree | commitdiff
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) tree | commitdiff
2020-05-20 Andrew ReynoldsUse debug-check-model to enable internal debugging... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-05-12 Andrew ReynoldsDo not enable unconstrained simplification if arithmeti... tree | commitdiff
2020-04-28 Andrew ReynoldsSupport the SMT-LIB Unicode string standard by default... tree | commitdiff
2020-04-22 Andrew ReynoldsAllow eager bitblasting with solve bv as int in QF_NIA... 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 ReynoldsAlways assign function values in higher order (#4279) tree | commitdiff
2020-04-15 Andrew ReynoldsDisable preregistration of instantiations for cegqi... tree | commitdiff
2020-04-14 Andrew ReynoldsDisable macros when higher-order (#4266) tree | commitdiff
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233) tree | commitdiff
2020-04-09 Andrew ReynoldsSplit ProcessAssertions module from SmtEngine (#4210) tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-06 Andrew ReynoldsRemove links field in all toml files (#4201) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) tree | commitdiff
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186) tree | commitdiff
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... tree | commitdiff
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154) tree | commitdiff
2020-03-24 yoni206Int2BV fail on demand (#4079) tree | commitdiff
2020-03-20 Andrew ReynoldsHandle failures for sygus QE preprocess (#4072) tree | commitdiff
2020-03-19 yoni206Bv2int fail on demand tree | commitdiff
2020-03-19 Andrew ReynoldsSyGuS must use total bitvector division (#4119) tree | commitdiff
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) tree | commitdiff
2020-03-17 Aina NiemetzSmtEngine: Convert members owned by SmtEngine to unique... tree | commitdiff
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... tree | commitdiff
2020-03-12 Andrew ReynoldsRemove local theory extension option (#4048) tree | commitdiff
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default... tree | commitdiff
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine... tree | commitdiff
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) tree | commitdiff
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) tree | commitdiff
2020-03-10 Andrew ReynoldsConsolidate options that disable produceModels (#3973) tree | commitdiff
2020-03-10 Andrew ReynoldsRename sygus option name (#3977) tree | commitdiff
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928) tree | commitdiff
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) tree | commitdiff
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin... tree | commitdiff
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... tree | commitdiff
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) tree | commitdiff
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-24 Abdalrhman MohamedFix bugs related to printing Sygus commands (#3804) tree | commitdiff
2020-02-20 Andres NoetzliRemove unused code (#3782) tree | commitdiff
2020-02-20 Andres NoetzliRemove parser from bindings (#3779) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-02-17 Abdalrhman MohamedSupport dumping Sygus commands. (#3763) tree | commitdiff
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) tree | commitdiff
2020-02-14 Haniel BarbosaForcing rewrite pass rather than asserting if formula... tree | commitdiff
2020-02-12 Andres NoetzliRename Java package to edu.stanford.CVC4 (#3752) tree | commitdiff
2020-02-08 Andres NoetzliMake "unknown" non-critical for unsat cores check ... tree | commitdiff
2020-02-07 Andrew ReynoldsRefactor check-model handling in SmtEngine (#3723) tree | commitdiff
2020-02-06 Andrew ReynoldsGeneralize containsQuantifiers to hasClosure (#3722) tree | commitdiff
2020-01-31 Andrew ReynoldsAllow PBE symmetry breaking with sygus stream (#3686) tree | commitdiff
2020-01-30 Andrew ReynoldsWeaken assertion for models with approximations (#3667) tree | commitdiff
2020-01-15 Aina NiemetzNew C++ API: Add nullary constructor for Result. (... tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... tree | commitdiff
2019-12-16 makaimannTrace tags for dumping the decision tree in org-mode... tree | commitdiff
2019-12-10 Andrew ReynoldsAllow unsat cores with sygus inference (#3550) tree | commitdiff
2019-12-09 Andrew ReynoldsDisable sygus inference when combined with incremental... tree | commitdiff
2019-12-06 Andrew ReynoldsThrow exception instead of warning for approximate... tree | commitdiff
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... tree | commitdiff
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) tree | commitdiff
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... tree | commitdiff
2019-12-02 Andrew ReynoldsEnsure quantifiers options are set with --no-strings... tree | commitdiff
2019-11-29 Andrew ReynoldsCheck free variables in assertions when using SyGuS... tree | commitdiff
2019-11-27 Haniel BarbosaEnable sygusRecFun by default and fixes SyGuS+RecFun... tree | commitdiff
2019-11-13 Andrew ReynoldsDistinguish unknown status for model printing (#3454) tree | commitdiff
2019-11-08 Mathias Preinercmake: Disable C++ GNU extensions. (#3446) tree | commitdiff
2019-11-04 Andrew ReynoldsMake check synth solution robust to auxiliary assertion... tree | commitdiff
2019-11-04 Andrew ReynoldsMake getSynthSolution return a Bool (#3306) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-14 Andrew ReynoldsApply sygus repair constant techniques restricted to... tree | commitdiff
2019-10-08 Piotr Trojanekpass parameters by reference where it affects performance tree | commitdiff
2019-10-08 Andres NoetzliDisallow --proof and --incremental (#3332) tree | commitdiff
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... tree | commitdiff
2019-10-03 yoni206Disable proofs for unsupported logics (#3327) tree | commitdiff
2019-09-27 Andres NoetzliMake substitution index context-independent (#2474) tree | commitdiff
2019-09-25 Andrew ReynoldsReturn choice functions for approximate values in get... tree | commitdiff
2019-09-18 Andrew ReynoldsDecouple fmf-bound and finite-model-find (#3297) tree | commitdiff
2019-09-16 Andrew ReynoldsReturn RecoverableModalException when model is not... tree | commitdiff
2019-09-12 Andrew ReynoldsEncapsulate synth engine (#3271) tree | commitdiff
2019-09-07 Andrew ReynoldsRemove portfolio (#3236) tree | commitdiff
next