projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Do not normalize to representatives for variable equalities in conflict-based instant...
[cvc5.git] / test /
2020-04-15 Andrew ReynoldsDo not normalize to representatives for variable equali... 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 ReynoldsRemove a few spurious assertions (#4294) tree | commitdiff
2020-04-14 Andrew ReynoldsFix dump-unsat-cores-full (#4303) tree | commitdiff
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming... tree | commitdiff
2020-04-12 Andrew ReynoldsFixes for extended rewriter (#4278) tree | commitdiff
2020-04-12 Andrew ReynoldsMove slow nl regression to regress3 (#4276) tree | commitdiff
2020-04-11 Alex OzdemirAdd skip predicate to node traversal. (#4222) tree | commitdiff
2020-04-11 Andrew ReynoldsEnsure exported sygus solutions match grammar (#4270) tree | commitdiff
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233) tree | commitdiff
2020-04-09 Andrew ReynoldsDisable slow sygus regression (#4232) tree | commitdiff
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-08 Andrew ReynoldsFix dump models and dump proofs (#4230) tree | commitdiff
2020-04-07 Andrew ReynoldsDisable slow regression (#4221) tree | commitdiff
2020-04-05 Andres NoetzliAdd safe_print() support for Kind enum (#4213) tree | commitdiff
2020-04-04 Aina NiemetzNew C++ API: Remove Op::getSort(). (#4208) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-03 Andrew ReynoldsOnly rewrite lambdas via array representations when... tree | commitdiff
2020-04-03 Andrew ReynoldsSplit sequences rewriter (#4194) tree | commitdiff
2020-04-02 Andres NoetzliRemove undocumented/uncommon aliases (#4177) tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188) tree | commitdiff
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) tree | commitdiff
2020-03-31 Andrew ReynoldsFix fmf benchmark (#4193) tree | commitdiff
2020-03-31 Andrew ReynoldsFix strange bound regression (#4192) tree | commitdiff
2020-03-31 Andrew ReynoldsFixing regressions (#4189) tree | commitdiff
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) tree | commitdiff
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175) tree | commitdiff
2020-03-28 Abdalrhman MohamedChange is-cons to (_ is cons) in Sygus benchmarks.... tree | commitdiff
2020-03-28 Abdalrhman MohamedConvert the last few Sygus benchmarks to V2. (#4172) tree | commitdiff
2020-03-28 Alex OzdemirNode traversal iterator (#3845) tree | commitdiff
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... tree | commitdiff
2020-03-27 Andrew ReynoldsFix expected output on arith regression (#4162) tree | commitdiff
2020-03-27 Andrew ReynoldsMove string utility file (#4164) tree | commitdiff
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... tree | commitdiff
2020-03-26 AmaleeAdded unit-cube-like test for branch and bound (#3922) tree | commitdiff
2020-03-26 Andrew ReynoldsDisable slow regression (#4157) tree | commitdiff
2020-03-24 yoni206Int2BV fail on demand (#4079) tree | commitdiff
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141) tree | commitdiff
2020-03-22 Andrew ReynoldsSort inference does not handle APPLY_UF when higher... tree | commitdiff
2020-03-22 Abdalrhman MohamedConvert V1 Sygus files to V2. (#4136) tree | commitdiff
2020-03-21 Andres NoetzliDon't run bv_nat parse test with competition build... tree | commitdiff
2020-03-20 Andrew ReynoldsFix variable shadowing issue in sygus-inference (#4121) tree | commitdiff
2020-03-20 Andrew ReynoldsGuard cases of sort inference in quantifier free logics... tree | commitdiff
2020-03-20 Andrew ReynoldsSplit string-specific operators from TheoryStringsRewri... tree | commitdiff
2020-03-20 Andrew ReynoldsDo not assign higher-order representative if function... tree | commitdiff
2020-03-19 Andrew ReynoldsFix regression output related to sygus+bv-div-zero... tree | commitdiff
2020-03-19 yoni206Bv2int fail on demand tree | commitdiff
2020-03-19 Andres NoetzliOnly apply testConstStringInRegExp to const regexp... tree | commitdiff
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... tree | commitdiff
2020-03-19 Andrew ReynoldsFix issue with multiple infinities in CEGQI for LIRA... tree | commitdiff
2020-03-17 Aina NiemetzSmtEngine: Convert members owned by SmtEngine to unique... tree | commitdiff
2020-03-16 Aina NiemetzIssue 4077: Add unit test to reproduce issue. (#4107) tree | commitdiff
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... tree | commitdiff
2020-03-13 Andrew ReynoldsRemove regress for real to int (#4071) tree | commitdiff
2020-03-12 Andrew ReynoldsAdd options for nec regression (#4056) tree | commitdiff
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... tree | commitdiff
2020-03-12 Andrew ReynoldsDo not make models for quantified function variables... tree | commitdiff
2020-03-12 Aina NiemetzNew C++ API: Remove support for (reset). (#4037) tree | commitdiff
2020-03-12 Andrew ReynoldsFix double notify in equality engine (#4036) tree | commitdiff
2020-03-12 Andrew ReynoldsSimplifications to the Datatypes API (#4040) tree | commitdiff
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default... tree | commitdiff
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033) tree | commitdiff
2020-03-11 Andrew ReynoldsAdd missing datatype functions to new API (#3930) tree | commitdiff
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026) 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-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... tree | commitdiff
2020-03-11 Andrew ReynoldsFix duplicate variable issue in sygus-qe-preproc (... tree | commitdiff
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) tree | commitdiff
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016) tree | commitdiff
2020-03-10 Andrew ReynoldsFix options for regression: --sort-inference is incompa... tree | commitdiff
2020-03-10 Andrew ReynoldsFix sort inference for top-level Boolean variables... tree | commitdiff
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) tree | commitdiff
2020-03-10 Aina NiemetzUse fixed-width types in test/unit/context/contest_mm_b... tree | commitdiff
2020-03-10 Aina NiemetzFix -Wshadow warning in test/unit/context/context_mm_bl... tree | commitdiff
2020-03-10 Andrew ReynoldsFix assertion failure in sort inference for Boolean... tree | commitdiff
2020-03-10 Andrew ReynoldsDo not set values for non-linear mult terms in collectM... tree | commitdiff
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979) tree | commitdiff
2020-03-10 Andrew ReynoldsDo not traverse quantifiers in nl ext purify (#3982) tree | commitdiff
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and... tree | commitdiff
2020-03-10 Andrew ReynoldsRename sygus option name (#3977) tree | commitdiff
2020-03-10 Andrew ReynoldsRemove instantiation propagator infrastructure (#3975) tree | commitdiff
2020-03-10 Andrew ReynoldsEnsure standard miniscoping is applied before aggressiv... tree | commitdiff
2020-03-09 Andrew ReynoldsFix type issue in arith rewrite equality (#3972) tree | commitdiff
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965) tree | commitdiff
2020-03-09 Andrew ReynoldsRewrite again full for DIV rewrite (#3945) tree | commitdiff
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu... tree | commitdiff
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) tree | commitdiff
2020-03-06 Andres NoetzliIgnore model check warning in regression test (#3926) tree | commitdiff
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... tree | commitdiff
2020-03-06 Andres NoetzliMake output of regression script more readable (#3911) tree | commitdiff
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) tree | commitdiff
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers... tree | commitdiff
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) tree | commitdiff
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... tree | commitdiff
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... tree | commitdiff
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) tree | commitdiff
next