projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Modify the smt2 parser to use the Sygus grammar. (#4829)
[cvc5.git] / src / smt /
2020-08-04 Abdalrhman MohamedModify the smt2 parser to use the Sygus grammar. (... tree | commitdiff
2020-08-04 Gereon KremerProperly initialize d_fullyInited. (#4840) tree | commitdiff
2020-08-03 Andrew ReynoldsSplit expression names from SmtEngine (#4832) tree | commitdiff
2020-08-03 Andrew ReynoldsSplit dump manager from SmtEngine (#4824) tree | commitdiff
2020-08-02 Andrew ReynoldsAdd methods for constructing datatype types from NodeMa... tree | commitdiff
2020-07-31 Andrew ReynoldsSplit listener classes from SmtEngine (#4816) tree | commitdiff
2020-07-28 Andrew ReynoldsRemove arrays lazy rintro option (#4806) tree | commitdiff
2020-07-28 Andres NoetzliReplace Expr with Node in Term/Op (#4781) tree | commitdiff
2020-07-28 yoni206Supporting seq.nth (#4723) tree | commitdiff
2020-07-27 Andrew Reynolds(proof-new) Proof production for term formula removal... tree | commitdiff
2020-07-17 Andrew ReynoldsReplace options listener infrastructure (#4764) tree | commitdiff
2020-07-17 Andrew ReynoldsAdd option manager and simpler option listener (#4745) tree | commitdiff
2020-07-16 Gereon KremerResource manager cleanup (#4732) tree | commitdiff
2020-07-16 Andrew ReynoldsSplit abstract values utility from SmtEngine (#4754) tree | commitdiff
2020-07-16 Gereon KremerRemove cumulative time limits and cpu time limits ... tree | commitdiff
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752) tree | commitdiff
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733) tree | commitdiff
2020-07-14 Andrew ReynoldsMake use of options in setDefaults more consistent... tree | commitdiff
2020-07-13 Andrew Reynolds (proof-new) SMT Preprocess proof generator (#4708) tree | commitdiff
2020-07-11 yoni206Changing bv_to_int options (#4721) tree | commitdiff
2020-07-11 Andrew V. JonesAdd support for printing 'get-abduct' in verbose mode... tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-08 Andrew ReynoldsAlways interleave theory combination with quantifiers... tree | commitdiff
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-07-03 Andres NoetzliRemove SWIG bindings (#4683) tree | commitdiff
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
next