projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Enable -Wshadow and fix warnings. (#3909)
[cvc5.git] / src / smt /
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
2019-09-06 Andrew Reynolds Model API for domain elements (#3243) tree | commitdiff
2019-09-04 Andrew ReynoldsTowards incremental SyGuS in SMT engine (#3195) tree | commitdiff
2019-08-28 Andrew ReynoldsRemoving comments related to issues (#3232) tree | commitdiff
2019-08-28 Andrew ReynoldsFixes for get-abduct (#3229) tree | commitdiff
2019-08-19 Aina NiemetzNew C++ API: Add checks for Solver::checkValid and... tree | commitdiff
2019-08-14 Mathias PreinerRemove option --continued-execution. (#3189) tree | commitdiff
2019-08-14 Andrew ReynoldsCall separate SMT engine for single invocation sygus... tree | commitdiff
2019-08-14 Aina NiemetzSmtEngine: Reorganize class according to guidelines... tree | commitdiff
2019-08-13 Andrew Reynolds Track sygus variable to term relationship via attribut... tree | commitdiff
2019-08-13 Andrew ReynoldsImplement check abduct feature (#3152) tree | commitdiff
2019-08-07 Aina NiemetzNew C++ API: Add checks and tests for push/pop. (#3121) tree | commitdiff
2019-08-05 Andrew ReynoldsRemove forward declarations in quantifiers engine ... tree | commitdiff
2019-08-02 Andrew ReynoldsFlip the polarity of the argument of get-abduct (#3153) tree | commitdiff
2019-08-02 Andrew ReynoldsEnable sygus logic when produce-abducts is true (#3144) tree | commitdiff
2019-08-01 Andrew Reynolds Regular expression intersection modes (#3134) tree | commitdiff
2019-07-30 Andrew Reynolds Track solver execution mode (#3132) tree | commitdiff
2019-07-30 Haniel BarbosaCode to activate hoelim preprocessing pass (#3129) tree | commitdiff
2019-07-29 Andrew ReynoldsModel blocker feature (#3112) tree | commitdiff
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) tree | commitdiff
2019-07-01 Andrew ReynoldsSupport sygus version 2 format (#3066) tree | commitdiff
2019-06-21 Andres NoetzliFix and simplify handling of --force-logic (#3062) tree | commitdiff
2019-06-12 Andres NoetzliDisable dumping regression for non-dumping builds ... tree | commitdiff
2019-06-11 Andrew Reynolds Fix spurious assertion in get-value (#3052) tree | commitdiff
2019-06-05 Andres NoetzliAdd support for SWIG 4 (#3041) tree | commitdiff
2019-06-04 Andres NoetzliEnable proof checking for QF_LRA benchmarks (#2928) tree | commitdiff
2019-06-04 Andres NoetzliAdd check that result matches benchmark status (#3028) tree | commitdiff
2019-05-16 Andres NoetzliFix iterators in Java API (#3000) tree | commitdiff
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959) tree | commitdiff
2019-04-11 Andrew Reynolds Eliminate Boolean ITE within terms, fixes 2947 (#2949) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-22 makaimannUse empty vector instead of false in query with null... tree | commitdiff
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) tree | commitdiff
2019-03-16 Andres NoetzliLimit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ... tree | commitdiff
2019-03-14 makaimanncheck for null assumption in query and replace with... tree | commitdiff
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ... tree | commitdiff
2019-02-27 Andres NoetzliUse string stream for proofs instead of tmp files ... tree | commitdiff
2019-02-12 Andres NoetzliDelete temporary proof files when aborting CVC4 (#2834) tree | commitdiff
2019-01-18 Andres Noetzli Fix ABC build (#2808) tree | commitdiff
2019-01-15 Andres NoetzliStrings: Add option to change loop process mode (#2794) tree | commitdiff
2019-01-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,... tree | commitdiff
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) tree | commitdiff
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) tree | commitdiff
2018-12-06 Andres NoetzliFix use-after-free due to destruction order (#2739) tree | commitdiff
2018-11-29 Andrew ReynoldsCombine sygus stream with PBE (#2726) tree | commitdiff
2018-11-27 Andrew ReynoldsLazy model construction in TheoryEngine (#2633) tree | commitdiff
2018-11-21 Andrew ReynoldsQuickly recognize when PBE conjectures are infeasible... tree | commitdiff
2018-11-15 Andrew Reynolds Expand definitions prior to model core computation... tree | commitdiff
2018-10-31 Andres NoetzliRecord assumption info in AssertionPipeline (#2678) tree | commitdiff
2018-10-22 Andres NoetzliRecover from wrong use of get-info :reason-unknown... tree | commitdiff
2018-10-20 Andrew ReynoldsSygus streaming non-implied predicates (#2660) tree | commitdiff
2018-10-19 Andres NoetzliAdd OptionException handling during initialization... tree | commitdiff
next